(* AUTEURS / AUTHORS :                          *)
(* Judicaël Courant,   Jean-François Monin      *)
(* VERIMAG, Université Joseph Fourier, Grenoble *)
(*                                         2006 *)

Require Omega.

(* A repeat tactical for one-argument tactics. Unlike repeat, the
   tactic is applied at least once.
*)
Ltac repeat1 t g := t g; repeat (t g).

Ltac tacsum t1 t2 g := (t1 g; try t2 g) || t2 g.

(* A tactic is said invertible whenever its application does not change
   the provability of the goal.

   In the following we use the following terminology:
   * progressing tactics: invertible tactics generating at most one subgoal  
   * splitting tactics: invertible tactics potentially generating several
                        subgoal
   * solving tactics: solve the goal or fail
   * non-invertible tactics.
   * non-invertible mapping: a parameterized tactic [t], taking as argument a
       solver [s], apply some non-invertible tactic followed by [s] on the
       generated subgoals.
*)

(* [rsplit pro spl] tries to solve the goal, using the progressing tactic
   [pro] and the splitting tactic [spl]. [g] is a dummy argument. This tactic
   is splitting.
*)
Ltac rsplit pro spl g :=
  let t g := (spl g; try repeat1 pro g) in
  let rt g := repeat1 t g in
  let t2 g := repeat1 pro g in
  tacsum t2 rt g.

Ltac myfail g := fail.

(* [solver_dfs pro spl noni n g] is a depth-first search solving tactic, where
   * [pro] is progressing
   * [spl] is splitting
   * [noni] is a non-invertible mapping
   * n is the depth of search
   * g is a dummy argument
*)
Ltac solver_dfs pro spl noni n g :=
  try rsplit pro spl g;
  let t := match n with
           | O => myfail
           | S ?k => noni ltac:(solver_dfs pro spl noni k)
           end
  in t g.

(* [solver pro spl noni n g] is an iterative deepening search solving tactic,
   where:
   * [pro] is progressing
   * [spl] is splitting
   * [noni] is a non-invertible mapping
   * n is the depth of search
   * g is a dummy argument
*)
Ltac solver pro spl noni n g :=
  let t :=
    match n with
    | O => solver_dfs pro spl noni 0
    | S ?k =>
      let u g := (solver pro spl noni k g || solver_dfs pro spl noni n g) in u
    end
  in t g.

(* [splitsolve pro spl noni n g] is a splitting tactic trying to solve the
   generated subgoals with [solver]
*)
Ltac splitsolve pro spl noni n g :=
  try rsplit pro spl g; try solver pro spl noni n g.


(* [everywhere t g] generalizes the whole goal, then applies g, then intros
   generalized hyps and variable back.
*)
(* NB: we have to take care of match goal non-determinism since we want a
   deterministic behaviour here: the first case must apply only on the last
   hypothesis of the context *)
Ltac everywhere t g := match goal with
| [ H : _ |- _ ] => generalize H; clear H; (everywhere t g || fail 1); intro H
| [ |- _ ] => match goal with
            | [ H : _ |- _ ] => fail 1
            | [ |- _ ] => t g
            end
end.

(* apply [t] on some hyp [H] by generalizing [H], applying [t] (and verifying
   it is progressing), then introducing [H] back.
*)
Ltac on_one_hyp t g := match goal with
| [ H : _ |- _ ] => generalize H; clear H;
                    (progress (t g) || on_one_hyp t g || fail 1);
		    intro H
end.

(* our generic rewrite database is named rew_db *)
Ltac autorew g := autorewrite with rew_db.

Require Import ZArith.

Open Local Scope Z_scope.
Lemma leq_dec : forall x y, (x <= y -> { x = y }+{ x < y })%Z.
intros x y.
generalize (ZArith_dec.Z_dec x y).
intuition.
Qed.


(* The base progress, splitting and non-invertible tactics I use. I do not
   pretend they have nice theoretical properties (besides being progressing,
   splitting and non-invertible) but they do the job for me. (I call them
   using [splitsolve0] below.)
*)
Ltac progress0 g := match goal with
| [ |- _ ] => omega || elimtype False;omega
| [ |- _ ] => progress (autorew g)
| [ |- _ ] => on_one_hyp ltac:autorew g
| [ H : ?t = ?t |- _ ] => clear H
| [ H : ?x = ?t |- _ ] => subst x
| [ H : ?t = ?x |- _ ] => subst x
| [ H : ?a = ?b |- _ ] => discriminate H
| [ H : ?a = ?b |- _ ] => injection H;
        match goal with
        | [ |- ?q -> ?p ] => clear H; intro H; change (a = b) in H; fail 1
        | [ |- _ ] => idtac
        end;
        clear H;intros
| [ H : (exists x, _) |- _ ] => elim H; clear H; intros
| [ H : (sig _) |- _ ] => elim H; clear H; intros
| [ H : (sigS _) |- _ ] => elim H; clear H; intros

| [ H : _ |- _ ] => inversion H;fail
| [ |- _ ] => assumption
| [ H : ?p, H2 : ?p |- _ ] => clear H || clear H2
| [ H1 : ?a -> ?b, H2 : ?a |- _ ] => assert b; [ exact (H1 H2) | clear H1 ]
| [ H : ?a /\ ?b |- _ ] =>
  generalize (proj1 H) (proj2 H);clear H; intro; intro
| [ |- ?a -> ?b ] => intro
| [ H : ?a /\ ?b -> ?c |- _ ] => cut (a -> b -> c) ;
                                 [ clear H; intro H
                                 | intro; intro; apply H;split; assumption ]
| [ |- forall x, _ ] => intro
| [ |- ?t = ?u ] => congruence
| [ |- False ] => congruence
| [ |- ?t <> ?u ] => intro
| [ |- ?t = ?u ] => ring;fail
(*| [ |- _ ] => everywhere ltac:(fun g => (progress simpl)) g*)
| [ |- True ] => trivial
| [ H : ?a >= ?b |- _ ] => cut (a > b \/ a = b); [clear H;intro H| omega]
| [ H : ?a = ?a -> ?b |- _ ] => cut b ;
                                [ clear H; intro H | apply H; reflexivity]
| [ |- ({ ?x = ?y }+{ ?x < ?y })%Z ] => apply leq_dec
end.

Ltac split0 g := match goal with
  | [ H : ?a \/ ?b |- _ ] => elim H;clear H
  | [ H : (?a +{ ?b }) |- _ ] => elim H; clear H;intro
  | [ H : ({ ?a }+{ ?b }) |- _ ] => elim H; clear H;intro
  | [ |- ?a /\ ?b ] => assert a ; [ idtac | split ; [ assumption | idtac ] ]
  | [ |- _ ] => everywhere ltac:(fun g => (progress simpl)) g
end.

Ltac noni0 t g := match goal with
  | [ |- _ ] => econstructor; t g
(*  | [ |- _ ] => left; t g subsummed by constructor above *)
  | [ |- _ ] => constructor 2; t g
  | [ x : _ |- exists y, _ ] => exists x;t g
  | [ |- ?f1 ?x1 = ?f2 ?x2 ] =>
    cut (f1 = f2);
     [ cut (x1 = x2); [ intros;congruence
                        | idtac ]
     | idtac ]; t g
  | [ H : (forall x, _), x0 : _ |- _ ] => generalize (H x0);clear H;t g
  | [ H : (?f ?u) <> (?f ?v) |- _ ] =>
        cut (u <> v); [ clear H; intro H; t g | congruence ]
  | [ |- _ ] => 
      (apply Zorder.Zmult_le_compat_l
       || apply Zorder.Zmult_ge_compat_l
       || apply Zorder.Zplus_le_0_compat
       || apply Zorder.Zmult_le_0_compat);
      t g
  | [ H : _ |- _ ] => apply H; t g
  | [ |- { ?a }+{ ?b } ] => (left; t g) || (right; t g)
  | [ |- ?a + { ?b } ] => (left; t g) || (right; t g)
  | [ |- _ ] => solve [eauto]
end.

Ltac splitsolve0 n := splitsolve progress0 split0 noni0 n 0.
Ltac solver0 n := solver progress0 split0 noni0 n 0.

(*Hint Extern 2 (?x=?y) => congruence.

(* ensure [t] generates a given a number of subgoals *)
Ltac ensure0 t g := t g;fail.
Ltac ensure1 t g := t g ; [idtac].
Ltac ensure2 t g := t g;[idtac | idtac].
Ltac ensure1atmost t g := (t g;fail)||(t g;[idtac]).

(* a progressing tactic potentially better than repeat1 as it uses
   splitting tactics, provided all of their subgoal except one are solved.
   To be improved, though.
*)
Ltac prosolve pro spl noni n g :=
  let splsol k g := spl g; solver pro spl noni k g in
  (try repeat1 pro g; ensure1atmost ltac:(splsol n g)).

*)