Bug squashing day !

- Closed bugs 121, 1696, 1438, 1425, 1696, 1604, 1738, 1760, 1683 related to
setoids. Add corresponding test files.
- Add new modulo_zeta flag to control zeta during unification (e.g. not
allowed for setoid_rewrite unification, but ok for almost everything
else).
- Various fixes in class_tactics with respect to evars and error
messages.
- Correct error message for NoOccurenceFound, distinguishing between a
rewrite in the goal or an hypothesis.
- Move notations for ==>, --> and ++> to level 90 as suggested by
Russell O'Conor.


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

8 files changed, 376 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/shouldsucceed/121.v b/test-suite/bugs/closed/shouldsucceed/121.v
new file mode 100644
index 000000000..d193aa73f
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/121.v
@@ -0,0 +1,17 @@
+Require Import Setoid.
+
+Section Setoid_Bug.
+
+Variable X:Type -> Type.
+Variable Xeq : forall A, (X A) -> (X A) -> Prop.
+Hypothesis Xst : forall A, Equivalence (X A) (Xeq A).
+
+Variable map : forall A B, (A -> B) -> X A -> X B.
+
+Implicit Arguments map [A B].
+
+Goal forall A B (a b:X (B -> A)) (c:X A) (f:A -> B -> A), Xeq _ a b -> Xeq _ b (map f c) -> Xeq _ a (map f c).
+intros A B a b c f Hab Hbc.
+rewrite Hab.
+assumption.
+Qed.
diff --git a/test-suite/bugs/closed/shouldsucceed/1425.v b/test-suite/bugs/closed/shouldsucceed/1425.v
new file mode 100644
index 000000000..f5fbb8a2a
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1425.v
@@ -0,0 +1,13 @@
+Require Import Setoid. 
+
+Parameter recursion : forall A : Set, A -> (nat -> A -> A) -> nat -> A.
+
+Axiom recursion_S :
+  forall (A : Set) (EA : relation A) (a : A) (f : nat -> A -> A) (n : nat),
+    EA (recursion A a f (S n)) (f n (recursion A a f n)).
+
+Goal forall n : nat, recursion nat 0 (fun _ _ => 1) (S n) = 1.
+intro n.
+setoid_rewrite recursion_S.
+reflexivity.
+Qed.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/shouldsucceed/1604.v b/test-suite/bugs/closed/shouldsucceed/1604.v
new file mode 100644
index 000000000..2d0991cb1
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1604.v
@@ -0,0 +1,7 @@
+Require Import Setoid.
+
+Parameter F : nat -> nat.
+Axiom F_id : forall n : nat, n = F n.
+Goal forall n : nat, F n = n.
+intro n. setoid_rewrite F_id at 2. reflexivity.
+Qed.
diff --git a/test-suite/bugs/closed/shouldsucceed/1683.v b/test-suite/bugs/closed/shouldsucceed/1683.v
new file mode 100644
index 000000000..1571ee20e
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1683.v
@@ -0,0 +1,42 @@
+Require Import Setoid.
+
+Section SetoidBug.
+
+Variable ms : Type.
+Variable ms_type : ms -> Type.
+Variable ms_eq : forall (A:ms), relation (ms_type A).
+
+Variable CR : ms.
+
+Record Ring : Type :=
+{Ring_type : Type}.
+
+Variable foo : forall (A:Ring), nat -> Ring_type A.
+Variable IR : Ring.
+Variable IRasCR : Ring_type IR -> ms_type CR.
+
+Definition CRasCRing : Ring := Build_Ring (ms_type CR).
+
+Hypothesis ms_refl : forall A x, ms_eq A x x.
+Hypothesis ms_sym : forall A x y, ms_eq A x y -> ms_eq A y x.
+Hypothesis ms_trans : forall A x y z, ms_eq A x y -> ms_eq A y z -> ms_eq A x z.
+
+Add Parametric Relation A : (ms_type A) (ms_eq A)
+  reflexivity proved by (ms_refl A)
+  symmetry proved by (ms_sym A)
+  transitivity proved by (ms_trans A)
+  as ms_Setoid.
+
+Hypothesis foobar : forall n, ms_eq CR (IRasCR (foo IR n)) (foo CRasCRing n).
+
+Goal forall (b:ms_type CR),
+ ms_eq CR (IRasCR (foo IR O)) b -> 
+ ms_eq CR (IRasCR (foo IR O)) b.
+intros b H.
+rewrite foobar.
+rewrite foobar in H.
+assumption.
+Qed.
+
+
+
diff --git a/test-suite/bugs/closed/shouldsucceed/1696.v b/test-suite/bugs/closed/shouldsucceed/1696.v
new file mode 100644
index 000000000..0826428a3
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1696.v
@@ -0,0 +1,16 @@
+Require Import Setoid.
+
+Inductive mynat := z : mynat | s : mynat -> mynat.
+
+Parameter E : mynat -> mynat -> Prop.
+Axiom E_equiv : equiv mynat E.
+
+Add Relation mynat E
+ reflexivity proved by (proj1 E_equiv)
+ symmetry proved by (proj2 (proj2 E_equiv))
+ transitivity proved by (proj1 (proj2 E_equiv))
+as E_rel.
+
+Notation "x == y" := (E x y) (at level 70).
+
+Goal z == s z -> s z == z. intros H. setoid_rewrite H at 2. reflexivity. Qed.
diff --git a/test-suite/bugs/closed/shouldsucceed/1738.v b/test-suite/bugs/closed/shouldsucceed/1738.v
new file mode 100644
index 000000000..0deed3663
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1738.v
@@ -0,0 +1,30 @@
+Require Import FSets.
+
+Module SomeSetoids (Import M:FSetInterface.S).
+
+Lemma Equal_refl : forall s, s[=]s.
+Proof. red; split; auto. Qed.
+
+Add Relation t Equal 
+ reflexivity proved by Equal_refl 
+ symmetry proved by eq_sym
+ transitivity proved by eq_trans 
+ as EqualSetoid.
+
+Add Morphism Empty with signature Equal ==> iff as Empty_m.
+Proof.
+unfold Equal, Empty; firstorder.
+Qed.
+
+End SomeSetoids.
+
+Module Test (Import M:FSetInterface.S).
+ Module A:=SomeSetoids M.
+ Module B:=SomeSetoids M. (* lots of warning *)
+
+ Lemma Test : forall s s', s[=]s' -> Empty s -> Empty s'.
+ intros.
+ rewrite H in H0.
+ assumption.
+Qed.
+End Test.
\ No newline at end of file
diff --git a/test-suite/bugs/opened/shouldnotfail/1596.v b/test-suite/bugs/opened/shouldnotfail/1596.v
new file mode 100644
index 000000000..766bf524c
--- /dev/null
+++ b/test-suite/bugs/opened/shouldnotfail/1596.v
@@ -0,0 +1,242 @@
+
+Require Import Relations.
+Require Import FSets.
+Require Import Arith.
+
+Lemma Bool_elim_bool : forall (b:bool),b=true \/ b=false.
+  destruct b;try tauto.
+Qed.
+
+Module OrderedPair (X:OrderedType) (Y:OrderedType) <: OrderedType with
+Definition t := (X.t * Y.t)%type.
+  Definition t := (X.t * Y.t)%type.
+
+  Definition eq (xy1:t) (xy2:t) := 
+    let (x1,y1) := xy1 in
+      let (x2,y2) := xy2 in
+        (X.eq x1 x2) /\ (Y.eq y1 y2).
+
+  Definition lt (xy1:t) (xy2:t) := 
+    let (x1,y1) := xy1 in
+      let (x2,y2) := xy2 in
+        (X.lt x1 x2) \/ ((X.eq x1 x2) /\ (Y.lt y1 y2)).
+
+  Lemma eq_refl : forall (x:t),(eq x x).
+    destruct x.
+    unfold eq.
+    split;[apply X.eq_refl | apply Y.eq_refl].
+  Qed.
+
+  Lemma eq_sym : forall (x y:t),(eq x y)->(eq y x).
+    destruct x;destruct y;unfold eq;intro.
+    elim H;clear H;intros.
+    split;[apply X.eq_sym | apply Y.eq_sym];trivial.
+  Qed.
+
+  Lemma eq_trans : forall (x y z:t),(eq x y)->(eq y z)->(eq x z).
+    unfold eq;destruct x;destruct y;destruct z;intros.
+    elim H;clear H;intros.
+    elim H0;clear H0;intros.
+    split;[eapply X.eq_trans | eapply Y.eq_trans];eauto.
+  Qed.
+
+  Lemma lt_trans : forall (x y z:t),(lt x y)->(lt y z)->(lt x z).
+    unfold lt;destruct x;destruct y;destruct z;intros.
+    case H;clear H;intro.
+    case H0;clear H0;intro.
+    left.
+    eapply X.lt_trans;eauto.
+    elim H0;clear H0;intros.
+    left.
+    case (X.compare t0 t4);trivial;intros.
+    generalize (X.eq_sym H0);intro.
+    generalize (X.eq_trans e H2);intro.
+    elim (X.lt_not_eq H H3).
+    generalize (X.lt_trans l H);intro.
+    generalize (X.eq_sym H0);intro.
+    elim (X.lt_not_eq H2 H3).
+    elim H;clear H;intros.
+    case H0;clear H0;intro.
+    left.
+    case (X.compare t0 t4);trivial;intros.
+    generalize (X.eq_sym H);intro.
+    generalize (X.eq_trans H2 e);intro.
+    elim (X.lt_not_eq H0 H3).
+    generalize (X.lt_trans H0 l);intro.
+    generalize (X.eq_sym H);intro.
+    elim (X.lt_not_eq H2 H3).
+    elim H0;clear H0;intros.
+    right.
+    split.
+    eauto.
+    eauto.
+  Qed.
+
+  Lemma lt_not_eq : forall (x y:t),(lt x y)->~(eq x y).
+    unfold lt, eq;destruct x;destruct y;intro;intro.
+    elim H0;clear H0;intros.
+    case H.
+    intro.
+    apply (X.lt_not_eq H2 H0).
+    intro.
+    elim H2;clear H2;intros.
+    apply (Y.lt_not_eq H3 H1).
+  Qed.
+
+  Definition compare : forall (x y:t),(Compare lt eq x y).
+    destruct x;destruct y.
+    case (X.compare t0 t2);intro.
+    apply LT.
+    left;trivial.
+    case (Y.compare t1 t3);intro.
+    apply LT.
+    right.
+    tauto.
+    apply EQ.
+    split;trivial.
+    apply GT.
+    right;auto.
+    apply GT.
+    left;trivial.
+  Defined.
+
+  Hint Immediate eq_sym.
+  Hint Resolve eq_refl eq_trans lt_not_eq lt_trans. 
+End OrderedPair.
+
+Module MessageSpi.
+  Inductive message : Set :=
+  | MNam : nat -> message.
+
+  Definition t := message.
+
+  Fixpoint message_lt (m n:message) {struct m} : Prop :=
+    match (m,n) with
+      | (MNam n1,MNam n2) => n1 < n2
+    end.
+
+  Module Ord <: OrderedType with Definition t := message with Definition eq :=
+@eq message.
+    Definition t := message.
+    Definition eq := @eq message.
+    Definition lt := message_lt.
+
+    Lemma eq_refl : forall (x:t),eq x x.
+      unfold eq;auto.
+    Qed.
+
+    Lemma eq_sym : forall (x y:t),(eq x y )->(eq y x).
+      unfold eq;auto.
+    Qed.
+
+    Lemma eq_trans : forall (x y z:t),(eq x y)->(eq y z)->(eq x z).
+      unfold eq;auto;intros;congruence.
+    Qed.
+
+    Lemma lt_trans : forall (x y z:t),(lt x y)->(lt y z)->(lt x z).
+      unfold lt.
+      induction x;destruct y;simpl;try tauto;destruct z;try tauto;intros.
+      omega.
+    Qed.
+
+    Lemma lt_not_eq : forall (x y:t),(lt x y)->~(eq x y).
+      unfold eq;unfold lt.
+      induction x;destruct y;simpl;try tauto;intro;red;intro;try (discriminate
+H0);injection H0;intros.
+      elim (lt_irrefl n);try omega.
+    Qed.
+
+    Definition compare : forall (x y:t),(Compare lt eq x y).
+      unfold lt, eq.
+      induction x;destruct y;intros;try (apply LT;simpl;trivial;fail);try
+(apply
+GT;simpl;trivial;fail).
+      case (lt_eq_lt_dec n n0);intros;try (case s;clear s;intros).
+      apply LT;trivial.
+      apply EQ;trivial.
+      rewrite e;trivial.
+      apply GT;trivial.
+    Defined.
+
+    Hint Immediate eq_sym.
+    Hint Resolve eq_refl eq_trans lt_not_eq lt_trans.
+  End Ord.
+
+  Theorem eq_dec : forall (m n:message),{m=n}+{~(m=n)}.
+    intros.
+    case (Ord.compare m n);intro;[right | left | right];try (red;intro).
+    elim (Ord.lt_not_eq m n);auto.
+    rewrite e;auto.
+    elim (Ord.lt_not_eq n m);auto.
+  Defined.
+End MessageSpi.
+
+Module MessagePair := OrderedPair MessageSpi.Ord MessageSpi.Ord.
+
+Module Type Hedge := FSetInterface.S with Module E := MessagePair.
+
+Module A (H:Hedge).
+  Definition hedge := H.t.
+
+  Definition message_relation := relation MessageSpi.message.
+
+  Definition relation_of_hedge (h:hedge) (m n:MessageSpi.message) := H.In (m,n)
+h.
+
+  Inductive hedge_synthesis_relation (h:message_relation) : message_relation :=
+    | SynInc : forall (m n:MessageSpi.message),(h m
+n)->(hedge_synthesis_relation h m n).
+
+  Fixpoint hedge_in_synthesis (h:hedge) (m:MessageSpi.message)
+(n:MessageSpi.message) {struct m} : bool :=
+    if H.mem (m,n) h 
+      then true 
+      else false.
+
+  Definition hedge_synthesis_spec (h:hedge) := hedge_synthesis_relation
+(relation_of_hedge h).
+
+  Lemma hedge_in_synthesis_impl_hedge_synthesis_spec : forall (h:hedge),forall
+(m n:MessageSpi.message),(hedge_in_synthesis h m n)=true->(hedge_synthesis_spec
+h m n).
+    unfold hedge_synthesis_spec;unfold relation_of_hedge.
+    induction m;simpl;intro.
+    elim (Bool_elim_bool (H.mem (MessageSpi.MNam n,n0) h));intros.
+    apply SynInc;apply H.mem_2;trivial.
+    rewrite H in H0.  (* !! possible here !! *)
+    discriminate H0.
+  Qed.
+End A.
+
+Module B (H:Hedge).
+  Definition hedge := H.t.
+
+  Definition message_relation := relation MessageSpi.t.
+
+  Definition relation_of_hedge (h:hedge) (m n:MessageSpi.t) := H.In (m,n) h.
+
+  Inductive hedge_synthesis_relation (h:message_relation) : message_relation :=
+    | SynInc : forall (m n:MessageSpi.t),(h m n)->(hedge_synthesis_relation h m
+n).
+
+  Fixpoint hedge_in_synthesis (h:hedge) (m:MessageSpi.t) (n:MessageSpi.t)
+{struct m} : bool :=
+    if H.mem (m,n) h 
+      then true 
+      else false.
+
+  Definition hedge_synthesis_spec (h:hedge) := hedge_synthesis_relation
+(relation_of_hedge h).
+
+  Lemma hedge_in_synthesis_impl_hedge_synthesis_spec : forall (h:hedge),forall
+(m n:MessageSpi.t),(hedge_in_synthesis h m n)=true->(hedge_synthesis_spec h m
+n).
+    unfold hedge_synthesis_spec;unfold relation_of_hedge.
+    induction m;simpl;intro.
+    elim (Bool_elim_bool (H.mem (MessageSpi.MNam n,n0) h));intros.
+    apply SynInc;apply H.mem_2;trivial.
+    
+    rewrite H in H0. (* !! impossible here !! *)
+    discriminate H0.
+  Qed.
+End B.
\ No newline at end of file
diff --git a/test-suite/bugs/opened/shouldnotfail/1811.v b/test-suite/bugs/opened/shouldnotfail/1811.v
new file mode 100644
index 000000000..037b7cb2d
--- /dev/null
+++ b/test-suite/bugs/opened/shouldnotfail/1811.v
@@ -0,0 +1,9 @@
+Require Export Bool.
+
+Lemma neg2xor : forall b, xorb true b = negb b.
+Proof. auto. Qed.
+
+Goal forall b1 b2, (negb b1 = b2)  ->  xorb true b1 = b2.
+Proof.
+  intros b1 b2.
+  rewrite neg2xor.
\ No newline at end of file