diff options
Diffstat (limited to 'theories/Classes/Equivalence.v')
| -rw-r--r-- | theories/Classes/Equivalence.v | 15 |
1 files changed, 7 insertions, 8 deletions
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v index 70bf3483..d52eed47 100644 --- a/theories/Classes/Equivalence.v +++ b/theories/Classes/Equivalence.v @@ -13,7 +13,7 @@ Institution: LRI, CNRS UMR 8623 - UniversitĂcopyright Paris Sud 91405 Orsay, France *) -(* $Id: Equivalence.v 10919 2008-05-11 22:04:26Z msozeau $ *) +(* $Id: Equivalence.v 11282 2008-07-28 11:51:53Z msozeau $ *) Require Export Coq.Program.Basics. Require Import Coq.Program.Tactics. @@ -116,7 +116,7 @@ Section Respecting. Definition respecting [ Equivalence A (R : relation A), Equivalence B (R' : relation B) ] : Type := { morph : A -> B | respectful R R' morph morph }. - Program Instance respecting_equiv [ Equivalence A R, Equivalence B R' ] : + Program Instance respecting_equiv [ eqa : Equivalence A R, eqb : Equivalence B R' ] : Equivalence respecting (fun (f g : respecting) => forall (x y : A), R x y -> R' (proj1_sig f x) (proj1_sig g y)). @@ -124,18 +124,17 @@ Section Respecting. Next Obligation. Proof. - unfold respecting in *. program_simpl. red in H2,H3,H4. - transitivity (y x0) ; auto. - transitivity (y y0) ; auto. - symmetry. auto. + unfold respecting in *. program_simpl. transitivity (y y0); auto. apply H0. reflexivity. Qed. End Respecting. (** The default equivalence on function spaces, with higher-priority than [eq]. *) -Program Instance pointwise_equivalence [ Equivalence A eqA ] : - Equivalence (B -> A) (pointwise_relation eqA) | 9. +Program Instance pointwise_equivalence [ eqb : Equivalence B eqB ] : + Equivalence (A -> B) (pointwise_relation eqB) | 9. + + Solve Obligations using simpl_relation ; first [ reflexivity | (symmetry ; auto) ]. Next Obligation. Proof. |