diff options
Diffstat (limited to 'test-suite/typeclasses')
| -rw-r--r-- | test-suite/typeclasses/NewSetoid.v | 74 | ||||
| -rw-r--r-- | test-suite/typeclasses/clrewrite.v | 111 | ||||
| -rw-r--r-- | test-suite/typeclasses/unification_delta.v | 46 |
3 files changed, 231 insertions, 0 deletions
diff --git a/test-suite/typeclasses/NewSetoid.v b/test-suite/typeclasses/NewSetoid.v new file mode 100644 index 00000000..8ad03880 --- /dev/null +++ b/test-suite/typeclasses/NewSetoid.v @@ -0,0 +1,74 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* Certified Haskell Prelude. + * Author: Matthieu Sozeau + * Institution: LRI, CNRS UMR 8623 - UniversitĂcopyright Paris Sud + * 91405 Orsay, France *) + +(* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *) + +Require Import Coq.Program.Program. + +Set Implicit Arguments. +Unset Strict Implicit. + +Require Import Coq.Classes.SetoidTactics. + +Goal not True == not (not False) -> ((not True -> True)) \/ True. + intros. + clrewrite H. + clrewrite <- H. + right ; auto. +Defined. + +Definition reduced_thm := Eval compute in Unnamed_thm. + +(* Print reduced_thm. *) + +Lemma foo [ Setoid a R ] : True. (* forall x y, R x y -> x -> y. *) +Proof. + intros. + Print respect2. + pose setoid_morphism. + pose (respect2 (b0:=b)). + simpl in b0. + unfold binary_respectful in b0. + pose (arrow_morphism R). + pose (respect2 (b0:=b1)). + unfold binary_respectful in b2. + + pose (eq_morphism (A:=a)). + pose (respect2 (b0:=b3)). + unfold binary_respectful in b4. + exact I. +Qed. + +Goal forall A B C (H : A <-> B) (H' : B <-> C), A /\ B <-> B /\ C. + intros. + Set Printing All. + Print iff_morphism. + clrewrite H. + clrewrite H'. + reflexivity. +Defined. + +Goal forall A B C (H : A <-> B) (H' : B <-> C), A /\ B <-> B /\ C. + intros. + rewrite H. + rewrite H'. + reflexivity. +Defined. + +Require Import Setoid_tac. +Require Import Setoid_Prop. + +(* Print Unnamed_thm0. *) +(* Print Unnamed_thm1. *) + + 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. diff --git a/test-suite/typeclasses/unification_delta.v b/test-suite/typeclasses/unification_delta.v new file mode 100644 index 00000000..663a837f --- /dev/null +++ b/test-suite/typeclasses/unification_delta.v @@ -0,0 +1,46 @@ +Require Import Coq.Classes.Equivalence. +Require Import Coq.Program.Program. + +Ltac obligations_tactic ::= program_simpl ; simpl_relation. + +Lemma bla : forall [ ! Equivalence A (eqA : relation A) ] x y, eqA x y -> eqA y x. +Proof. + intros. + rewrite H0. + reflexivity. +Defined. + +Lemma bla' : forall [ ! Equivalence A (eqA : relation A) ] x y, eqA x y -> eqA y x. +Proof. + intros. + (* Need delta on [relation] to unify with the right lemmas. *) + rewrite <- H0. + reflexivity. +Qed. + +Axiom euclid : nat -> { x : nat | x > 0 } -> nat. + +Definition eq_proj {A} {s : A -> Prop} : relation (sig s) := + fun x y => `x = `y. + +Program Instance {A : Type} {s : A -> Prop} => Equivalence (sig s) eq_proj. + + Next Obligation. + Proof. + constructor ; red ; intros. + reflexivity. + Qed. + + Admit Obligations. + +Instance Morphism (eq ==> eq_proj ==> eq) euclid. +Proof. +Admitted. + +Goal forall (x : nat) (y : nat | y > 0) (z : nat | z > 0), eq_proj y z -> euclid x y = euclid x z. +Proof. + intros. + (* Breaks if too much delta in unification *) + rewrite H. + reflexivity. +Qed.
\ No newline at end of file |