Fix a naming bug reported by Arnaud Spiwack, allow instance search to create evars and try to solve them too.

Finally, rework tactics on setoids and design a saturating tactic to help solve goals on any setoid.



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10428 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 126 insertions, 4 deletions

diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index 851579e125..7963a307b7 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.v
@@ -29,18 +29,28 @@ Require Export Coq.Relations.Relations.
 Class Setoid (carrier : Type) (equiv : relation carrier) :=
   equiv_prf : equivalence carrier equiv.
 
-(** Overloaded notation for setoid equivalence. Not to be confused with [eq] and [=]. *)
+(** Overloaded notations for setoid equivalence and inequivalence. Not to be confused with [eq] and [=]. *)
 
 Definition equiv [ Setoid A R ] : _ := R.
 
 Infix "==" := equiv (at level 70, no associativity) : type_scope.
 
+Notation " x =!= y " := (~ x == y) (at level 70, no associativity).
+
 Definition equiv_refl [ s : Setoid A R ] : forall x : A, R x x := equiv_refl _ _ equiv_prf.
 Definition equiv_sym [ s : Setoid A R ] : forall x y : A, R x y -> R y x := equiv_sym _ _ equiv_prf.
 Definition equiv_trans [ s : Setoid A R ] : forall x y z : A, R x y -> R y z -> R x z := equiv_trans _ _ equiv_prf.
 
+Lemma nequiv_sym : forall [ s : Setoid A R ] (x y : A), x =!= y -> y =!= x.
+Proof.
+  intros ; red ; intros.
+  apply equiv_sym in H0...
+  apply (H H0).
+Qed.
 
-Ltac refl :=
+(** Tactics to do some progress on the goal, called by the user. *)
+
+Ltac do_setoid_refl :=
   match goal with
     | [ |- @equiv ?A ?R ?s ?X _ ] => apply (equiv_refl (A:=A) (R:=R) (s:=s) X)
     | [ |- ?R ?X _ ] => apply (equiv_refl (R:=R) X)
@@ -49,16 +59,21 @@ Ltac refl :=
     | [ |- ?R ?A ?B ?C ?X _ ] => apply (equiv_refl (R:=R A B C) X)
   end.
 
-Ltac sym := 
+Ltac refl := do_setoid_refl.
+
+Ltac do_setoid_sym := 
   match goal with
     | [ |- @equiv ?A ?R ?s ?X ?Y ] => apply (equiv_sym (A:=A) (R:=R) (s:=s) (x:=X) (y:=Y))
+    | [ |- not (@equiv ?A ?R ?s ?X ?Y) ] => apply (nequiv_sym (A:=A) (R:=R) (s:=s) (x:=X) (y:=Y))
     | [ |- ?R ?X ?Y ] => apply (equiv_sym (R:=R) (x:=Y) (y:=X))
     | [ |- ?R ?A ?X ?Y ] => apply (equiv_sym (R:=R A) (x:=Y) (y:=X))
     | [ |- ?R ?A ?B ?X ?Y ] => apply (equiv_sym (R:=R A B) (x:=Y) (y:=X))
     | [ |- ?R ?A ?B ?C ?X ?Y ] => apply (equiv_sym (R:=R A B C) (x:=Y) (y:=X))
   end.
 
-Ltac trans Y := 
+Ltac sym := do_setoid_sym.
+
+Ltac do_setoid_trans Y := 
   match goal with
     | [ |- @equiv ?A ?R ?s ?X ?Z ] => apply (equiv_trans (A:=A) (R:=R) (s:=s) (x:=X) (y:=Y) (z:=Z))
     | [ |- ?R ?X ?Z ] => apply (equiv_trans (R:=R) (x:=X) (y:=Y) (z:=Z))
@@ -67,6 +82,72 @@ Ltac trans Y :=
     | [ |- ?R ?A ?B ?C ?X ?Z ] => apply (equiv_trans (R:=R A B C) (x:=X) (y:=Y) (z:=Z))
   end.
 
+Ltac trans y := do_setoid_trans y.
+
+(** Tactics to immediately solve the goal without user help. *)
+
+Ltac setoid_refl :=
+  match goal with
+    | [ |- @equiv ?A ?R ?s ?X _ ] => apply (equiv_refl (A:=A) (R:=R) (s:=s) X)
+    | [ |- ?R ?X _ ] => apply (equiv_refl (R:=R) X)
+    | [ |- ?R ?A ?X _ ] => apply (equiv_refl (R:=R A) X)
+    | [ |- ?R ?A ?B ?X _ ] => apply (equiv_refl (R:=R A B) X)
+    | [ |- ?R ?A ?B ?C ?X _ ] => apply (equiv_refl (R:=R A B C) X)
+  end.
+
+Ltac setoid_sym := 
+  match goal with
+    | [ H : ?X == ?Y |- ?Y == ?X ] => apply (equiv_sym (x:=X) (y:=Y) H)
+    | [ H : ?X =!= ?Y |- ?Y =!= ?X ] => apply (nequiv_sym (x:=X) (y:=Y) H)
+  end.
+
+Ltac setoid_trans := 
+  match goal with
+    | [ H : ?X == ?Y, H' : ?Y == ?Z |- @equiv ?A ?R ?s ?X ?Z ] => apply (equiv_trans (A:=A) (R:=R) (s:=s) (x:=X) (y:=Y) (z:=Z) H H')
+  end.
+
+(** To immediatly solve a goal on setoid equality. *)
+
+Ltac setoid_tac := setoid_refl || setoid_sym || setoid_trans.
+
+Lemma nequiv_equiv : forall [ Setoid A ] (x y z : A), x =!= y -> y == z -> x =!= z.
+Proof.
+  intros; intro. 
+  assert(z == y) by setoid_sym.
+  assert(x == y) by setoid_trans.
+  contradiction.
+Qed.
+
+Lemma equiv_nequiv : forall [ Setoid A ] (x y z : A), x == y -> y =!= z -> x =!= z.
+Proof.
+  intros; intro. 
+  assert(y == x) by setoid_sym.
+  assert(y == z) by setoid_trans.
+  contradiction.
+Qed.
+
+Open Scope type_scope.
+
+Ltac setoid_sat :=
+  let add H t := let name := fresh H in add_hypothesis name t in
+    match goal with
+      | [ H : ?x == ?y |- _ ] => let name:=fresh "Heq" y x in add name (equiv_sym H)
+      | [ H : ?x =!= ?y |- _ ] => let name:=fresh "Hneq" y x in add name (nequiv_sym H)
+      | [ H : ?x == ?y, H' : ?y == ?z |- _ ] => let name:=fresh "Heq" x z in add name (equiv_trans H H')
+      | [ H : ?x == ?y, H' : ?y =!= ?z |- _ ] => let name:=fresh "Hneq" x z in add name (equiv_nequiv H H')
+      | [ H : ?x =!= ?y, H' : ?y == ?z |- _ ] => let name:=fresh "Hneq" x z in add name (nequiv_equiv H H')
+    end.
+
+Ltac setoid_saturate := repeat setoid_sat.
+
+Ltac setoidify_tac :=
+  match goal with
+    | [ s : Setoid ?A ?R, H : ?R ?x ?y |- _ ] => change R with (@equiv A R s) in H
+    | [ s : Setoid ?A ?R |- ?R ?x ?y ] => change R with (@equiv A R s)
+  end.
+
+Ltac setoidify := repeat setoidify_tac.
+
 Definition respectful [ sa : Setoid a eqa, sb : Setoid b eqb ] (m : a -> b) : Prop :=
   forall x y, eqa x y -> eqb (m x) (m y).
 
diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v
index 4832f1d72f..7be5141697 100644
--- a/theories/Classes/SetoidTactics.v
+++ b/theories/Classes/SetoidTactics.v
@@ -35,3 +35,31 @@ Ltac setoideq :=
     [ |- @eq ?A ?X ?Y ] => apply (setoideq_eq (a:=A) X Y)
   end.
 
+Ltac setoid_tactic :=
+  match goal with
+    | [ H : ?eq ?x ?y |- ?eq ?y ?x ] => sym ; apply H
+    | [ |- ?eq ?x ?x ] => refl
+    | [ H : ?eq ?x ?y, H' : ?eq ?y ?z |- ?eq' ?x ?z ] => trans y ; [ apply H | apply H' ]
+    | [ H : ?eq ?x ?y, H' : ?eq ?z ?y |- ?eq' ?x ?z ] => trans y ; [ apply H | sym ; apply H' ]
+    | [ H : ?eq ?y ?x, H' : ?eq ?z ?y |- ?eq' ?x ?z ] => trans y ; [ sym ; apply H | sym ; apply H' ]
+    | [ H : ?eq ?y ?x, H' : ?eq ?y ?z |- ?eq' ?x ?z ] => trans y ; [ sym ; apply H | apply H' ]
+      
+    | [ H : ?eq ?x ?y |- @equiv _ _ _ ?y ?x ] => sym ; apply H
+    | [ |- @equiv _ _ _ ?x ?x ] => refl
+    | [ H : ?eq ?x ?y, H' : ?eq ?y ?z |- @equiv _ _ _ ?x ?z ] => trans y ; [ apply H | apply H' ]
+    | [ H : ?eq ?x ?y, H' : ?eq ?z ?y |- @equiv _ _ _ ?x ?z ] => trans y ; [ apply H | sym ; apply H' ]
+    | [ H : ?eq ?y ?x, H' : ?eq ?z ?y |- @equiv _ _ _ ?x ?z ] => trans y ; [ sym ; apply H | sym ; apply H' ]
+    | [ H : ?eq ?y ?x, H' : ?eq ?y ?z |- @equiv _ _ _ ?x ?z ] => trans y ; [ sym ; apply H | apply H' ]
+
+    | [ H : @equiv ?A ?R ?s ?x ?y |- @equiv _ _ _ ?y ?x ] => sym ; apply H
+    | [ |- @equiv _ _ _ ?x ?x ] => refl
+    | [ H : @equiv ?A ?R ?s ?x ?y, H' : @equiv ?A ?R ?s ?y ?z |- @equiv _ _ _ ?x ?z ] => trans y ; [ apply H | apply H' ]
+    | [ H : @equiv ?A ?R ?s ?x ?y, H' : @equiv ?A ?R ?s ?z ?y |- @equiv _ _ _ ?x ?z ] => trans y ; [ apply H | sym ; apply H' ]
+    | [ H : @equiv ?A ?R ?s ?y ?x, H' : @equiv ?A ?R ?s ?z ?y |- @equiv _ _ _ ?x ?z ] => trans y ; [ sym ; apply H | sym ; apply H' ]
+    | [ H : @equiv ?A ?R ?s ?y ?x, H' : @equiv ?A ?R ?s ?y ?z |- @equiv _ _ _ ?x ?z ] => trans y ; [ sym ; apply H | apply H' ]
+
+    | [ H : not (@equiv ?A ?R ?s ?X ?X) |- _ ] => elim H ; refl
+    | [ H : not (@equiv ?A ?R ?s ?X ?Y), H' : @equiv ?A ?R ?s ?Y ?X |- _ ] => elim H ; sym ; apply H
+    | [ H : not (@equiv ?A ?R ?s ?X ?Y), H' : ?R ?Y ?X |- _ ] => elim H ; sym ; apply H
+    | [ H : not (@equiv ?A ?R ?s ?X ?Y) |- False ] => elim H ; clear H ; setoid_tac
+  end.
diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v
index b7b62f394a..c3870e6bda 100644
--- a/theories/Program/Tactics.v
+++ b/theories/Program/Tactics.v
@@ -154,6 +154,19 @@ Ltac bang :=
 Tactic Notation "contradiction" "by" constr(t) := 
   let H := fresh in assert t as H by auto with * ; contradiction.
 
+(** A tactic that adds [H:=p:typeof(p)] to the context if no hypothesis of the same type appears in the goal.
+   Useful to do saturation using tactics. *)
+
+Ltac add_hypothesis H' p := 
+  match type of p with
+    ?X => 
+    match goal with 
+      | [ H : X |- _ ] => fail 1
+      | _ => set (H':=p) ; try (change p with H') ; clearbody H'
+    end
+  end.
+
+
 (** The default simplification tactic used by Program is defined by [program_simpl], sometimes [auto with *]
    is overkill and slows things down, better rebind using [Obligations Tactic := tac] in this case, 
    possibly using [program_simplify] to use standard goal-cleaning tactics. *)