From a0cfa4f118023d35b767a999d5a2ac4b082857b4 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 25 Jul 2008 15:12:53 +0200 Subject: Imported Upstream version 8.2~beta3+dfsg --- test-suite/typeclasses/unification_delta.v | 46 ++++++++++++++++++++++++++++++ 1 file changed, 46 insertions(+) create mode 100644 test-suite/typeclasses/unification_delta.v (limited to 'test-suite/typeclasses/unification_delta.v') 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 -- cgit v1.2.3