diff options
author | Stephane Glondu <steph@glondu.net> | 2008-08-08 13:18:42 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2008-08-08 13:18:42 +0200 |
commit | 870075f34dd9fa5792bfbf413afd3b96f17e76a0 (patch) | |
tree | 0c647056de1832cf1dba5ba58758b9121418e4be /theories/Classes/Equivalence.v | |
parent | a0cfa4f118023d35b767a999d5a2ac4b082857b4 (diff) |
Imported Upstream version 8.2~beta4+dfsgupstream/8.2.beta4+dfsg
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. |