diff options
author | Samuel Mimram <smimram@debian.org> | 2008-07-25 15:12:53 +0200 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2008-07-25 15:12:53 +0200 |
commit | a0cfa4f118023d35b767a999d5a2ac4b082857b4 (patch) | |
tree | dabcac548e299fee1da464c93b3dba98484f45b1 /test-suite/typeclasses/unification_delta.v | |
parent | 2281410e38ef99d025ea77194585a9bc019fdaa9 (diff) |
Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg
Diffstat (limited to 'test-suite/typeclasses/unification_delta.v')
-rw-r--r-- | test-suite/typeclasses/unification_delta.v | 46 |
1 files changed, 46 insertions, 0 deletions
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 |