aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/typeclasses/unification_delta.v
diff options
context:
space:
mode:
authorGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-03-16 16:14:08 +0000
committerGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-03-16 16:14:08 +0000
commit87017bcc49f0d9d07f8f8c6a8c0137715118ef46 (patch)
treec81453c5ce16a24596dc16f2f2530b32ca02c817 /test-suite/typeclasses/unification_delta.v
parent5f06da20ffc6446ff1929c376f084165a314a354 (diff)
Using the "relation" constant made some unifications fail in the new
setoid rewrite. Refine and use the new unification flags setup by Hugo to do a little bit of delta in clenv_unify/w_unify. Moved from a boolean indicating conversion is wanted to a Cpred representing the constants one wants to get unfolded to have more precise control. Add corresponding test-suite file. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10684 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/typeclasses/unification_delta.v')
-rw-r--r--test-suite/typeclasses/unification_delta.v46
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 000000000..b8789f26e
--- /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.
+ refl.
+Defined.
+
+Lemma bla' : forall [ ! Equivalence A (eqA : relation A) ] x y, eqA x y -> eqA y x.
+Proof.
+ intros.
+ (* Need delta no [relation] to unify with the right lemmas. *)
+ rewrite <- H0.
+ refl.
+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