Correction du bug #1634 + ajout de bugs dans la test-suite

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

5 files changed, 146 insertions, 40 deletions

diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 9452d4f3c..b33e38005 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -1874,47 +1874,49 @@ let general_setoid_replace rewrite_tac try_prove_eq_tac_opt relation c1 c2 ~new_
       | Some tac ->  Tacticals.tclTRY (Tacticals.tclCOMPLETE tac )
   in 
   try
-  let relation =
-   match relation with
-      Some rel ->
-       (try
-         match find_relation_class rel with
-            Relation sa -> sa
-          | Leibniz _ -> raise Optimize
-        with
-         Not_found ->
-          errorlabstrm "Setoid_rewrite"
-           (pr_lconstr rel ++ str " is not a registered relation."))
-    | None ->
-       match default_relation_for_carrier (pf_type_of gl c1) with
-          Relation sa -> sa
-        | Leibniz _ -> raise Optimize
-  in
-   let eq_left_to_right = mkApp (relation.rel_aeq, [| c1 ; c2 |]) in
-   let eq_right_to_left = mkApp (relation.rel_aeq, [| c2 ; c1 |]) in
-   let replace dir eq =
-    tclTHENS (assert_tac false Anonymous eq)
-      [onLastHyp (fun id ->
-        tclTHEN
-          (rewrite_tac dir (mkVar id) ~new_goals)
-          (clear [id]));
-       try_prove_eq_tac]
-   in
-    tclORELSE
-     (replace true eq_left_to_right) (replace false eq_right_to_left) gl
- with
-  Optimize -> (* (!replace tac_opt c1 c2) gl *)
-    let eq =  mkApp (Lazy.force  coq_eq, [| pf_type_of gl c1;c2 ; c1 |]) in 
-    tclTHENS (assert_tac false Anonymous eq)
-      [onLastHyp (fun id ->
-		    tclTHEN
-		      (rewrite_tac false (mkVar id) ~new_goals)
-		      (clear [id]));
-       try_prove_eq_tac] gl
+    let carrier,args = decompose_app (pf_type_of gl c1) in
+    let relation =
+      match relation with
+	  Some rel ->
+	    (try
+		match find_relation_class rel with
+		    Relation sa -> if not (eq_constr carrier sa.rel_a) then 		    
+			errorlabstrm "Setoid_rewrite"
+			  (str "the carrier of " ++ pr_lconstr rel ++ 
+			      str " does not match the type of " ++ pr_lconstr c1);
+		      sa
+		  | Leibniz _ -> raise Optimize
+              with
+		  Not_found ->
+		    errorlabstrm "Setoid_rewrite"
+		      (pr_lconstr rel ++ str " is not a registered relation."))
+	| None ->
+	    match default_relation_for_carrier (pf_type_of gl c1) with
+		Relation sa -> sa
+              | Leibniz _ -> raise Optimize
+    in
+    let eq_left_to_right = mkApp (relation.rel_aeq, Array.of_list (List.append args [ c1 ; c2 ])) in
+    let eq_right_to_left = mkApp (relation.rel_aeq, Array.of_list (List.append args [ c2 ; c1 ])) in
+    let replace dir eq =
+      tclTHENS (assert_tac false Anonymous eq)
+	[onLastHyp (fun id ->
+          tclTHEN
+            (rewrite_tac dir (mkVar id) ~new_goals)
+            (clear [id]));
+	 try_prove_eq_tac]
+    in
+      tclORELSE
+	(replace true eq_left_to_right) (replace false eq_right_to_left) gl
+  with
+      Optimize -> (* (!replace tac_opt c1 c2) gl *)
+	let eq =  mkApp (Lazy.force  coq_eq, [| pf_type_of gl c1;c2 ; c1 |]) in 
+	  tclTHENS (assert_tac false Anonymous eq)
+	    [onLastHyp (fun id ->
+	      tclTHEN
+		(rewrite_tac false (mkVar id) ~new_goals)
+		(clear [id]));
+	     try_prove_eq_tac] gl
       
-
-
-
 let setoid_replace = general_setoid_replace general_s_rewrite
 let setoid_replace_in  tac_opt id relation c1 c2 ~new_goals gl = 
   general_setoid_replace (general_s_rewrite_in id)  tac_opt relation c1 c2 ~new_goals gl
diff --git a/test-suite/bugs/closed/shouldsucceed/1414.v b/test-suite/bugs/closed/shouldsucceed/1414.v
new file mode 100644
index 000000000..9c2686ceb
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1414.v
@@ -0,0 +1,41 @@
+Require Import ZArith Coq.Program.Utils.
+
+Parameter data:Set.
+
+Inductive t : Set :=
+  | Leaf : t
+  | Node : t -> data -> t -> Z -> t.
+
+Parameter avl : t -> Prop.
+Parameter bst : t -> Prop. 
+Parameter In : data -> t -> Prop. 
+Parameter cardinal : t -> nat.
+Definition card2 (s:t*t) := let (s1,s2) := s in cardinal s1 + cardinal s2.
+
+Parameter split : data -> t -> t*(bool*t).
+Parameter join : t -> data -> t -> t.
+Parameter add : data -> t -> t.
+
+Program Fixpoint union 
+  (s:t*t)
+  (hb1: bst (fst s))(ha1: avl (fst s))(hb2: bst (snd s))(hb2: avl (snd s)) 
+  { measure card2 s } : 
+  {s' : t | bst s' /\ avl s' /\ forall x, In x s' <-> In x (fst s) \/ In x (snd
+s)} := 
+  match s with 
+    | (Leaf,t2) => t2
+    | (t1,Leaf) => t1
+    | (Node l1 v1 r1 h1, Node l2 v2 r2 h2) =>        
+        if (Z_ge_lt_dec h1 h2) then
+          if (Z_eq_dec h2 1) 
+          then add v2 (fst s)
+          else
+            let (l2', r2') := split v1 (snd s) in
+            join (union (l1,l2') _ _ _ _) v1 (union (r1,snd r2') _ _ _ _)
+        else
+          if (Z_eq_dec h1 1) 
+          then add v1 (snd s) 
+          else
+            let (l1', r1') := split v2 (fst s) in
+            join (union (l1',l2) _ _ _ _) v2 (union (snd r1',r2) _ _ _ _)
+  end. 
diff --git a/test-suite/bugs/closed/shouldsucceed/1634.v b/test-suite/bugs/closed/shouldsucceed/1634.v
new file mode 100644
index 000000000..9e50f6f25
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1634.v
@@ -0,0 +1,24 @@
+Require Export Relation_Definitions.
+Require Export Setoid.
+
+Variable A : Type.
+Variable S : A -> Type.
+Variable Seq : forall (a:A), relation (S a).
+
+Hypothesis Seq_refl : forall (a:A) (x : S a), Seq a x x.
+Hypothesis Seq_sym : forall (a:A) (x y : S a), Seq a x y -> Seq a y x.
+Hypothesis Seq_trans : forall (a:A) (x y z : S a), Seq a x y -> Seq a y z ->
+Seq
+a x z.
+
+Add Relation S Seq
+ reflexivity proved by Seq_refl
+ symmetry proved by Seq_sym
+ transitivity proved by Seq_trans
+ as S_Setoid.
+
+Goal forall (a : A) (x y : S a), Seq a x y -> Seq a x y.
+  intros a x y H.
+  setoid_replace x with y using relation Seq.
+  apply Seq_refl. trivial.
+Qed.
diff --git a/test-suite/bugs/opened/shouldnotfail/1416.v b/test-suite/bugs/opened/shouldnotfail/1416.v
new file mode 100644
index 000000000..c6f4302d8
--- /dev/null
+++ b/test-suite/bugs/opened/shouldnotfail/1416.v
@@ -0,0 +1,27 @@
+Set Implicit Arguments.
+
+Record Place (Env A: Type) : Type := {
+  read: Env -> A ;
+  write: Env -> A -> Env ;
+  write_read: forall (e:Env), (write e (read e))=e
+}. 
+
+Hint Rewrite -> write_read: placeeq.
+
+Record sumPl (Env A B: Type) (vL:(Place Env A)) (vR:(Place Env B)) : Type :=
+ { 
+   mkEnv: A -> B -> Env ;
+   mkEnv2writeL: forall (e:Env) (x:A), (mkEnv x (read vR e))=(write vL e x)
+ }.
+
+(* when the following line is commented, the bug does not appear *)
+Hint Rewrite -> mkEnv2writeL: placeeq.
+
+Lemma autorewrite_raise_anomaly: forall (Env A:Type) (e: Env) (p:Place Env A),
+  (exists e1:Env, e=(write p e1 (read p e))).
+Proof.
+  intros Env A e p; eapply ex_intro.
+  autorewrite with placeeq. (* Here is the bug *)
+  auto.
+Qed.
+
diff --git a/test-suite/bugs/opened/shouldnotfail/743.v b/test-suite/bugs/opened/shouldnotfail/743.v
new file mode 100644
index 000000000..f1eee6c18
--- /dev/null
+++ b/test-suite/bugs/opened/shouldnotfail/743.v
@@ -0,0 +1,12 @@
+Require Import Omega.
+
+Lemma foo : forall n m : Z, (n >= 0)%Z -> (n * m >= 0)%Z -> (n <= n + n * m)%Z.
+Proof.
+  intros. omega.
+Qed.
+
+Lemma foo' : forall n m : nat, n <=  n + n * m.
+Proof.
+  intros. omega.
+Qed.
+