diff options
Diffstat (limited to 'test-suite/typeclasses/clrewrite.v')
-rw-r--r-- | test-suite/typeclasses/clrewrite.v | 111 |
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. |