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

6 files changed, 140 insertions, 12 deletions

diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index c029550a1..4799eb7b3 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -99,7 +99,7 @@ let combine_params avoid applied needed =
     match app, need with
 	[], need -> 
 	  let need', avoid = ids_of_named_context_avoiding avoid (List.map snd need) in
-	    List.rev ids @ (List.map mkIdentC need'), avoid
+	    List.rev ids @ (List.rev_map mkIdentC need'), avoid
       | _, (true, (id, _, _)) :: need -> 
 	  let id' = next_ident_away_from id avoid in
 	    aux (CRef (Ident (dummy_loc, id')) :: ids) (Idset.add id' avoid) app need
@@ -130,7 +130,9 @@ let full_class_binders env l =
 	      (try
 		  let c = class_info (snd id) in
 		  let args, avoid = combine_params avoid l 
-		    (List.rev_map (fun x -> false, x) c.cl_context @ List.rev_map (fun x -> true, x) c.cl_super @ List.rev_map (fun x -> false, x) c.cl_params) 
+		    (List.rev_map (fun x -> false, x) c.cl_context @ 
+			List.rev_map (fun x -> true, x) c.cl_super @ 
+			List.rev_map (fun x -> false, x) c.cl_params) 
 		  in
 		    (iid, bk, CAppExpl (fst id, (None, Ident id), args)) :: l', avoid
 		with Not_found -> unbound_class (Global.env ()) id)
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index 3b9d98652..d687fe640 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -49,3 +49,7 @@ val nf_named_context : evar_map -> named_context -> named_context
 val nf_rel_context : evar_map -> rel_context -> rel_context
 val nf_env : evar_map -> env -> env
 
+
+val ids_of_named_context_avoiding :     Names.Idset.t ->
+    Sign.named_context -> Names.Idset.elt list * Names.Idset.t
+
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index b0e7cb147..306ef3a19 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -209,11 +209,9 @@ let instances r =
 let solve_instanciation_problem = ref (fun _ _ _ _ -> assert false)
 
 let resolve_typeclass env ev evi (evd, defined as acc) =
-  if evi.evar_body = Evar_empty then
-    try
-      !solve_instanciation_problem env evd ev evi
-    with Exit -> acc
-  else acc
+  try
+    !solve_instanciation_problem env evd ev evi
+  with Exit -> acc
 
 let resolve_one_typeclass env types =
   try
@@ -280,7 +278,9 @@ let resolve_typeclasses ?(check=true) env sigma evd =
     let (evars', progress) = 
       Evd.fold 
 	(fun ev evi acc -> 
-	  if Evd.mem tc_evars ev then resolve_typeclass env ev evi acc else acc) 
+	  if (Evd.mem tc_evars ev || not (Evd.mem evm ev)) && evi.evar_body = Evar_empty then
+	    resolve_typeclass env ev evi acc 
+	  else acc) 
 	(Evd.evars_of evars) (evars, false) 
     in
       if not progress then evars'
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index 851579e12..7963a307b 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 4832f1d72..7be514169 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 b7b62f394..c3870e6bd 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. *)