Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg

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 00000000..2978fda2
--- /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.