Backtrack changes on eauto, move specialized version of eauto in

class_tactics for further customizations. Add Equivalence.v for
typeclass definitions on equivalences and clrewrite.v test-suite for
clrewrite. Debugging the tactic I found missing morphisms that are now
in Morphisms.v and removed some that made proof search fail or take too
long, not sure it's complete however.


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

1 files changed, 111 insertions, 0 deletions

diff --git a/test-suite/typeclasses/clrewrite.v b/test-suite/typeclasses/clrewrite.v
new file mode 100644
index 000000000..5c56a0daf
--- /dev/null
+++ b/test-suite/typeclasses/clrewrite.v
@@ -0,0 +1,111 @@
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+Require Import Coq.Classes.Equivalence.
+
+Section Equiv.
+  Context [ Equivalence A eqA ].
+
+  Variables x y z w : A.
+
+  Goal eqA x y -> eqA y x.
+    intros H ; clrewrite H.
+    refl.
+  Qed.
+
+  Tactic Notation "simpl" "*" := auto || relation_tac.
+  
+  Goal eqA x y -> eqA y x /\ True.
+    intros H ; clrewrite H.
+    split ; simpl*.
+  Qed.
+
+  Goal eqA x y -> eqA y x /\ eqA x x.
+    intros H ; clrewrite H.
+    split ; simpl*.
+  Qed.
+
+  Goal eqA x y -> eqA y z -> eqA x y.
+    intros H. 
+    clrewrite H.
+    intro. refl.
+  Qed.
+        
+  Goal eqA x y -> eqA z y -> eqA x y.
+    intros H. 
+    clrewrite <- H at 2.
+    clrewrite <- H at 1.
+    intro. refl.
+  Qed.
+
+  Opaque complement.
+
+  Print iff_inverse_impl_binary_morphism.
+
+  Goal eqA x y -> eqA x y -> eqA x y.
+    intros H.
+    clrewrite H.
+    intro. refl.
+  Qed.
+
+  Goal eqA x y -> eqA x y -> eqA x y.
+    intros H.
+    clrewrite <- H.
+    refl.
+  Qed.
+  
+  Goal eqA x y -> True /\ True /\ False /\ eqA x x -> True /\ True /\ False /\ eqA x y.
+  Proof.
+    intros.
+    clrewrite <- H.
+    apply H0.
+  Qed.
+
+End Equiv.
+
+Section Trans.
+  Context [ Transitive A R ].
+
+  Variables x y z w : A.
+
+  Tactic Notation "simpl" "*" := auto || relation_tac.
+  
+(*   Typeclasses eauto := debug. *)
+
+  Goal R x y -> R y x -> R y y -> R x x.
+  Proof with auto.
+    intros H H' H''. 
+
+    clrewrite <- H' at 2.
+    clrewrite H at 1...
+  Qed.
+
+  Goal R x y -> R y z -> R x z.
+    intros H.
+    clrewrite H.
+    refl.
+  Qed.
+        
+  Goal R x y -> R z y -> R x y.
+    intros H. 
+    clrewrite <- H at 2.
+    intro. 
+    clrewrite H at 1.
+  Abort.
+
+  Goal R x y -> True /\ R y z -> True /\ R x z.
+  Proof.
+    intros.
+    clrewrite H.
+    apply H0.
+  Qed.
+
+  Goal R x y -> True /\ True /\ False /\ R y z -> True /\ True /\ False /\ R x z.
+  Proof.
+    intros.
+    clrewrite H.
+    apply H0.
+  Qed.
+
+End Trans.
\ No newline at end of file