From bb3560885d943baef87b7f99a5d646942f0fb288 Mon Sep 17 00:00:00 2001
From: msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Thu, 14 Feb 2008 12:56:21 +0000
Subject: 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
---
 test-suite/typeclasses/clrewrite.v | 111 +++++++++++++++++++++++++++++++++++++
 1 file changed, 111 insertions(+)
 create mode 100644 test-suite/typeclasses/clrewrite.v

(limited to 'test-suite/typeclasses')

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
-- 
cgit v1.2.3