From 870075f34dd9fa5792bfbf413afd3b96f17e76a0 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Fri, 8 Aug 2008 13:18:42 +0200 Subject: Imported Upstream version 8.2~beta4+dfsg --- theories/Classes/EquivDec.v | 8 +- theories/Classes/Equivalence.v | 15 +-- theories/Classes/Functions.v | 16 +-- theories/Classes/Init.v | 15 ++- theories/Classes/Morphisms.v | 230 +++++++++++++++++---------------- theories/Classes/Morphisms_Prop.v | 4 +- theories/Classes/Morphisms_Relations.v | 8 ++ theories/Classes/RelationClasses.v | 37 ++---- theories/Classes/SetoidClass.v | 14 +- theories/Classes/SetoidDec.v | 18 +-- theories/Classes/SetoidTactics.v | 23 +++- 11 files changed, 213 insertions(+), 175 deletions(-) (limited to 'theories/Classes') diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v index debe953a..1e58d05d 100644 --- a/theories/Classes/EquivDec.v +++ b/theories/Classes/EquivDec.v @@ -13,7 +13,7 @@ * Institution: LRI, CNRS UMR 8623 - UniversitĂcopyright Paris Sud * 91405 Orsay, France *) -(* $Id: EquivDec.v 10919 2008-05-11 22:04:26Z msozeau $ *) +(* $Id: EquivDec.v 11282 2008-07-28 11:51:53Z msozeau $ *) Set Implicit Arguments. Unset Strict Implicit. @@ -40,7 +40,7 @@ Class [ equiv : Equivalence A ] => EqDec := (** We define the [==] overloaded notation for deciding equality. It does not take precedence of [==] defined in the type scope, hence we can have both at the same time. *) -Notation " x == y " := (equiv_dec (x :>) (y :>)) (no associativity, at level 70). +Notation " x == y " := (equiv_dec (x :>) (y :>)) (no associativity, at level 70) : equiv_scope. Definition swap_sumbool {A B} (x : { A } + { B }) : { B } + { A } := match x with @@ -58,7 +58,7 @@ Program Definition nequiv_dec [ EqDec A ] (x y : A) : { x =/= y } + { x === y } (** Overloaded notation for inequality. *) -Infix "=/=" := nequiv_dec (no associativity, at level 70). +Infix "<>" := nequiv_dec (no associativity, at level 70) : equiv_scope. (** Define boolean versions, losing the logical information. *) @@ -155,4 +155,4 @@ Program Instance list_eqdec [ eqa : EqDec A eq ] : ! EqDec (list A) eq := Next Obligation. Proof. clear aux. red in H0. subst. destruct y; intuition (discriminate || eauto). - Defined. \ No newline at end of file + Defined. 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. diff --git a/theories/Classes/Functions.v b/theories/Classes/Functions.v index 49fc4f89..4c844911 100644 --- a/theories/Classes/Functions.v +++ b/theories/Classes/Functions.v @@ -13,7 +13,7 @@ Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud 91405 Orsay, France *) -(* $Id: Functions.v 10739 2008-04-01 14:45:20Z herbelin $ *) +(* $Id: Functions.v 11282 2008-07-28 11:51:53Z msozeau $ *) Require Import Coq.Classes.RelationClasses. Require Import Coq.Classes.Morphisms. @@ -21,22 +21,22 @@ Require Import Coq.Classes.Morphisms. Set Implicit Arguments. Unset Strict Implicit. -Class [ m : Morphism (A -> B) (RA ++> RB) f ] => Injective : Prop := +Class Injective ((m : Morphism (A -> B) (RA ++> RB) f)) : Prop := injective : forall x y : A, RB (f x) (f y) -> RA x y. -Class [ m : Morphism (A -> B) (RA ++> RB) f ] => Surjective : Prop := +Class ((m : Morphism (A -> B) (RA ++> RB) f)) => Surjective : Prop := surjective : forall y, exists x : A, RB y (f x). -Definition Bijective [ m : Morphism (A -> B) (RA ++> RB) (f : A -> B) ] := +Definition Bijective ((m : Morphism (A -> B) (RA ++> RB) (f : A -> B))) := Injective m /\ Surjective m. -Class [ m : Morphism (A -> B) (eqA ++> eqB) ] => MonoMorphism := +Class MonoMorphism (( m : Morphism (A -> B) (eqA ++> eqB) )) := monic :> Injective m. -Class [ m : Morphism (A -> B) (eqA ++> eqB) ] => EpiMorphism := +Class EpiMorphism ((m : Morphism (A -> B) (eqA ++> eqB))) := epic :> Surjective m. -Class [ m : Morphism (A -> B) (eqA ++> eqB) ] => IsoMorphism := +Class IsoMorphism ((m : Morphism (A -> B) (eqA ++> eqB))) := monomorphism :> MonoMorphism m ; epimorphism :> EpiMorphism m. -Class [ m : Morphism (A -> A) (eqA ++> eqA), ! IsoMorphism m ] => AutoMorphism. +Class ((m : Morphism (A -> A) (eqA ++> eqA))) [ ! IsoMorphism m ] => AutoMorphism. diff --git a/theories/Classes/Init.v b/theories/Classes/Init.v index 6ba0c61e..e5f951d0 100644 --- a/theories/Classes/Init.v +++ b/theories/Classes/Init.v @@ -13,9 +13,22 @@ Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud 91405 Orsay, France *) -(* $Id: Init.v 10739 2008-04-01 14:45:20Z herbelin $ *) +(* $Id: Init.v 11282 2008-07-28 11:51:53Z msozeau $ *) (* Ltac typeclass_instantiation := typeclasses eauto || eauto. *) Tactic Notation "clapply" ident(c) := eapply @c ; eauto with typeclass_instances. + +(** The unconvertible typeclass, to test that two objects of the same type are + actually different. *) + +Class Unconvertible (A : Type) (a b : A). + +Ltac unconvertible := + match goal with + | |- @Unconvertible _ ?x ?y => conv x y ; fail 1 "Convertible" + | |- _ => apply Build_Unconvertible + end. + +Hint Extern 0 (@Unconvertible _ _ _) => unconvertible : typeclass_instances. \ No newline at end of file diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v index f21c68a6..c2ae026d 100644 --- a/theories/Classes/Morphisms.v +++ b/theories/Classes/Morphisms.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-emacs-U" "-top" "Coq.Classes.Morphisms"); compile-command: "make -C ../.. TIME='time'" -*- *) +(* -*- coq-prog-name: "~/research/coq/trunk/bin/coqtop.byte"; coq-prog-args: ("-emacs-U" "-top" "Coq.Classes.Morphisms"); compile-command: "make -C ../.. TIME='time'" -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* B) := + fun f g => forall x : A, R (f x) (g x). + +Lemma pointwise_pointwise A B (R : relation B) : + relation_equivalence (pointwise_relation R) (@eq A ==> R). +Proof. intros. split. simpl_relation. firstorder. Qed. + (** We can build a PER on the Coq function space if we have PERs on the domain and codomain. *) +Hint Unfold Reflexive : core. +Hint Unfold Symmetric : core. +Hint Unfold Transitive : core. + Program Instance respectful_per [ PER A (R : relation A), PER B (R' : relation B) ] : PER (A -> B) (R ==> R'). @@ -92,24 +101,26 @@ Program Instance respectful_per [ PER A (R : relation A), PER B (R' : relation B transitivity (y x0)... Qed. -(** Subrelations induce a morphism on the identity, not used for morphism search yet. *) +(** Subrelations induce a morphism on the identity. *) -Lemma subrelation_id_morphism [ subrelation A R₁ R₂ ] : Morphism (R₁ ==> R₂) id. +Instance subrelation_id_morphism [ subrelation A R₁ R₂ ] : Morphism (R₁ ==> R₂) id. Proof. firstorder. Qed. (** The subrelation property goes through products as usual. *) -Instance morphisms_subrelation [ sub : subrelation A R₁ R₂ ] : - ! subrelation (B -> A) (R ==> R₁) (R ==> R₂). -Proof. firstorder. Qed. +Instance morphisms_subrelation_respectful [ subl : subrelation A R₂ R₁, subr : subrelation B S₁ S₂ ] : + subrelation (R₁ ==> S₁) (R₂ ==> S₂). +Proof. simpl_relation. apply subr. apply H. apply subl. apply H0. Qed. -Instance morphisms_subrelation_left [ sub : subrelation A R₂ R₁ ] : - ! subrelation (A -> B) (R₁ ==> R) (R₂ ==> R) | 3. -Proof. firstorder. Qed. +(** And of course it is reflexive. *) + +Instance morphisms_subrelation_refl : ! subrelation A R R | 10. +Proof. simpl_relation. Qed. (** [Morphism] is itself a covariant morphism for [subrelation]. *) -Lemma subrelation_morphism [ sub : subrelation A R₁ R₂, mor : Morphism A R₁ m ] : Morphism R₂ m. +Lemma subrelation_morphism [ mor : Morphism A R₁ m, unc : Unconvertible (relation A) R₁ R₂, + sub : subrelation A R₁ R₂ ] : Morphism R₂ m. Proof. intros. apply sub. apply mor. Qed. @@ -121,8 +132,9 @@ Proof. reduce. subst. firstorder. Qed. (** We use an external tactic to manage the application of subrelation, which is otherwise always applicable. We allow its use only once per branch. *) -Inductive subrelation_done : Prop := - did_subrelation : subrelation_done. +Inductive subrelation_done : Prop := did_subrelation : subrelation_done. + +Inductive normalization_done : Prop := did_normalization. Ltac subrelation_tac := match goal with @@ -131,7 +143,7 @@ Ltac subrelation_tac := set(H:=did_subrelation) ; eapply @subrelation_morphism end. -Hint Extern 4 (@Morphism _ _ _) => subrelation_tac : typeclass_instances. +Hint Extern 5 (@Morphism _ _ _) => subrelation_tac : typeclass_instances. (** Essential subrelation instances for [iff], [impl] and [pointwise_relation]. *) @@ -181,20 +193,10 @@ Program Instance trans_contra_co_morphism transitivity x0... Qed. -(* (** Dually... *) *) - -(* Program Instance [ Transitive A R ] => *) -(* trans_co_contra_inv_impl_morphism : Morphism (R ++> R --> inverse impl) R. *) - -(* Next Obligation. *) -(* Proof with auto. *) -(* apply* trans_contra_co_morphism ; eauto. eauto. *) -(* Qed. *) - (** Morphism declarations for partial applications. *) Program Instance trans_contra_inv_impl_morphism - [ Transitive A R ] : Morphism (R --> inverse impl) (R x). + [ Transitive A R ] : Morphism (R --> inverse impl) (R x) | 3. Next Obligation. Proof with auto. @@ -202,7 +204,7 @@ Program Instance trans_contra_inv_impl_morphism Qed. Program Instance trans_co_impl_morphism - [ Transitive A R ] : Morphism (R ==> impl) (R x). + [ Transitive A R ] : Morphism (R ==> impl) (R x) | 3. Next Obligation. Proof with auto. @@ -210,23 +212,23 @@ Program Instance trans_co_impl_morphism Qed. Program Instance trans_sym_co_inv_impl_morphism - [ Transitive A R, Symmetric A R ] : Morphism (R ==> inverse impl) (R x). + [ PER A R ] : Morphism (R ==> inverse impl) (R x) | 2. Next Obligation. Proof with auto. - transitivity y... + transitivity y... symmetry... Qed. Program Instance trans_sym_contra_impl_morphism - [ Transitive A R, Symmetric _ R ] : Morphism (R --> impl) (R x). + [ PER A R ] : Morphism (R --> impl) (R x) | 2. Next Obligation. Proof with auto. - transitivity x0... + transitivity x0... symmetry... Qed. -Program Instance equivalence_partial_app_morphism - [ Equivalence A R ] : Morphism (R ==> iff) (R x). +Program Instance per_partial_app_morphism + [ PER A R ] : Morphism (R ==> iff) (R x) | 1. Next Obligation. Proof with auto. @@ -240,36 +242,16 @@ Program Instance equivalence_partial_app_morphism to get an [R y z] goal. *) Program Instance trans_co_eq_inv_impl_morphism - [ Transitive A R ] : Morphism (R ==> (@eq A) ==> inverse impl) R. + [ Transitive A R ] : Morphism (R ==> (@eq A) ==> inverse impl) R | 2. Next Obligation. Proof with auto. transitivity y... Qed. -(* Program Instance [ Transitive A R ] => *) -(* trans_contra_eq_impl_morphism : Morphism (R --> (@eq A) ==> impl) R. *) - -(* Next Obligation. *) -(* Proof with auto. *) -(* transitivity x... *) -(* Qed. *) - (** Every Symmetric and Transitive relation gives rise to an equivariant morphism. *) -Program Instance trans_sym_morphism - [ Transitive A R, Symmetric _ R ] : Morphism (R ==> R ==> iff) R. - - Next Obligation. - Proof with auto. - split ; intros. - transitivity x0... transitivity x... - - transitivity y... transitivity y0... - Qed. - -Program Instance equiv_morphism [ Equivalence A R ] : - Morphism (R ==> R ==> iff) R. +Program Instance PER_morphism [ PER A R ] : Morphism (R ==> R ==> iff) R | 1. Next Obligation. Proof with auto. @@ -279,27 +261,21 @@ Program Instance equiv_morphism [ Equivalence A R ] : transitivity y... transitivity y0... symmetry... Qed. -(** In case the rewrite happens at top level. *) - -Program Instance iff_inverse_impl_id : - Morphism (iff ==> inverse impl) id. - -Program Instance inverse_iff_inverse_impl_id : - Morphism (iff --> inverse impl) id. +Lemma symmetric_equiv_inverse [ Symmetric A R ] : relation_equivalence R (flip R). +Proof. firstorder. Qed. -Program Instance iff_impl_id : - Morphism (iff ==> impl) id. +Program Instance compose_morphism A B C R₀ R₁ R₂ : + Morphism ((R₁ ==> R₂) ==> (R₀ ==> R₁) ==> (R₀ ==> R₂)) (@compose A B C). + + Next Obligation. + Proof. + simpl_relation. + unfold compose. apply H. apply H0. apply H1. + Qed. -Program Instance inverse_iff_impl_id : - Morphism (iff --> impl) id. - (** Coq functions are morphisms for leibniz equality, applied only if really needed. *) -(* Instance (A : Type) [ Reflexive B R ] => *) -(* eq_reflexive_morphism : Morphism (@Logic.eq A ==> R) m | 3. *) -(* Proof. simpl_relation. Qed. *) - Instance reflexive_eq_dom_reflexive (A : Type) [ Reflexive B R' ] : Reflexive (@Logic.eq A ==> R'). Proof. simpl_relation. Qed. @@ -335,49 +311,81 @@ Class MorphismProxy A (R : relation A) (m : A) : Prop := respect_proxy : R m m. Instance reflexive_morphism_proxy - [ Reflexive A R ] (x : A) : MorphismProxy A R x | 1. + [ Reflexive A R ] (x : A) : MorphismProxy R x | 1. Proof. firstorder. Qed. Instance morphism_morphism_proxy - [ Morphism A R x ] : MorphismProxy A R x | 2. + [ Morphism A R x ] : MorphismProxy R x | 2. Proof. firstorder. Qed. -(* Instance (A : Type) [ Reflexive B R ] => *) -(* eq_reflexive_morphism : Morphism (@Logic.eq A ==> R) m | 3. *) -(* Proof. simpl_relation. Qed. *) - (** [R] is Reflexive, hence we can build the needed proof. *) Lemma Reflexive_partial_app_morphism [ Morphism (A -> B) (R ==> R') m, MorphismProxy A R x ] : Morphism R' (m x). Proof. simpl_relation. Qed. +Class Params {A : Type} (of : A) (arity : nat). + +Class PartialApplication. + Ltac partial_application_tactic := - let tac x := - match type of x with - | Type => fail 1 - | _ => eapply @Reflexive_partial_app_morphism + let rec do_partial_apps H m := + match m with + | ?m' ?x => eapply @Reflexive_partial_app_morphism ; [do_partial_apps H m'|clear H] + | _ => idtac end in - let on_morphism m := - match m with - | ?m' ?x => tac x - | ?m' _ ?x => tac x - | ?m' _ _ ?x => tac x - | ?m' _ _ _ ?x => tac x - | ?m' _ _ _ _ ?x => tac x - | ?m' _ _ _ _ _ ?x => tac x - | ?m' _ _ _ _ _ _ ?x => tac x - | ?m' _ _ _ _ _ _ _ ?x => tac x - | ?m' _ _ _ _ _ _ _ _ ?x => tac x + let rec do_partial H ar m := + match ar with + | 0 => do_partial_apps H m + | S ?n' => + match m with + ?m' ?x => do_partial H n' m' + end end in + let on_morphism m := + let m' := fresh in head_of_constr m' m ; + let n := fresh in evar (n:nat) ; + let v := eval compute in n in clear n ; + let H := fresh in + assert(H:Params m' v) by typeclasses eauto ; + let v' := eval compute in v in + do_partial H v' m + in match goal with - | [ |- @Morphism _ _ ?m ] => on_morphism m + | [ _ : subrelation_done |- _ ] => fail 1 + | [ _ : normalization_done |- _ ] => fail 1 + | [ _ : @Params _ _ _ |- _ ] => fail 1 + | [ |- @Morphism ?T _ (?m ?x) ] => + match goal with + | [ _ : PartialApplication |- _ ] => + eapply @Reflexive_partial_app_morphism + | _ => + on_morphism (m x) || + (eapply @Reflexive_partial_app_morphism ; + [ pose Build_PartialApplication | idtac ]) + end end. -(* Program Instance [ Morphism (A -> B) (R ==> R') m, Reflexive A R ] (x : A) => *) -(* reflexive_partial_app_morphism : Morphism R' (m x). *) +Section PartialAppTest. + Instance and_ar : Params and 0. + + Goal Morphism (iff) (and True True). + partial_application_tactic. + Admitted. + + Goal Morphism (iff) (or True True). + partial_application_tactic. + partial_application_tactic. + Admitted. + + Goal Morphism (iff ==> iff) (iff True). + partial_application_tactic. + (*partial_application_tactic. *) + Admitted. + +End PartialAppTest. Hint Extern 4 (@Morphism _ _ _) => partial_application_tactic : typeclass_instances. @@ -395,19 +403,19 @@ Class (A : Type) => Normalizes (m : relation A) (m' : relation A) : Prop := normalizes : relation_equivalence m m'. Instance inverse_respectful_norm : - Normalizes (A -> B) (inverse R ==> inverse R') (inverse (R ==> R')) . + ! Normalizes (A -> B) (inverse R ==> inverse R') (inverse (R ==> R')) . Proof. firstorder. Qed. (* If not an inverse on the left, do a double inverse. *) Instance not_inverse_respectful_norm : - Normalizes (A -> B) (R ==> inverse R') (inverse (inverse R ==> R')) | 4. + ! Normalizes (A -> B) (R ==> inverse R') (inverse (inverse R ==> R')) | 4. Proof. firstorder. Qed. Instance inverse_respectful_rec_norm [ Normalizes B R' (inverse R'') ] : - Normalizes (A -> B) (inverse R ==> R') (inverse (R ==> R'')). -Proof. red ; intros. - pose normalizes as r. + ! Normalizes (A -> B) (inverse R ==> R') (inverse (R ==> R'')). +Proof. red ; intros. + assert(r:=normalizes). setoid_rewrite r. setoid_rewrite inverse_respectful. reflexivity. @@ -415,8 +423,14 @@ Qed. (** Once we have normalized, we will apply this instance to simplify the problem. *) -Program Instance morphism_inverse_morphism - [ Morphism A R m ] : Morphism (inverse R) m | 2. +Definition morphism_inverse_morphism [ mor : Morphism A R m ] : Morphism (inverse R) m := mor. + +Ltac morphism_inverse := + match goal with + [ |- @Morphism _ (flip _) _ ] => eapply @morphism_inverse_morphism + end. + +Hint Extern 2 (@Morphism _ _ _) => morphism_inverse : typeclass_instances. (** Bootstrap !!! *) @@ -434,16 +448,16 @@ Qed. Lemma morphism_releq_morphism [ Normalizes A R R', Morphism _ R' m ] : Morphism R m. Proof. intros. + pose respect as r. pose normalizes as norm. setoid_rewrite norm. assumption. Qed. -Inductive normalization_done : Prop := did_normalization. - Ltac morphism_normalization := match goal with + | [ _ : subrelation_done |- _ ] => fail 1 | [ _ : normalization_done |- _ ] => fail 1 | [ |- @Morphism _ _ _ ] => let H := fresh "H" in set(H:=did_normalization) ; eapply @morphism_releq_morphism @@ -464,4 +478,4 @@ Ltac morphism_reflexive := | [ |- @Morphism _ _ _ ] => eapply @reflexive_morphism end. -Hint Extern 4 (@Morphism _ _ _) => morphism_reflexive : typeclass_instances. \ No newline at end of file +Hint Extern 7 (@Morphism _ _ _) => morphism_reflexive : typeclass_instances. diff --git a/theories/Classes/Morphisms_Prop.v b/theories/Classes/Morphisms_Prop.v index 7dc1f95e..ec62e12e 100644 --- a/theories/Classes/Morphisms_Prop.v +++ b/theories/Classes/Morphisms_Prop.v @@ -29,7 +29,7 @@ Program Instance not_iff_morphism : (** Logical conjunction. *) -Program Instance and_impl_iff_morphism : +Program Instance and_impl_morphism : Morphism (impl ==> impl ==> impl) and. (* Program Instance and_impl_iff_morphism : *) @@ -49,7 +49,7 @@ Program Instance and_iff_morphism : (** Logical disjunction. *) -Program Instance or_impl_iff_morphism : +Program Instance or_impl_morphism : Morphism (impl ==> impl ==> impl) or. (* Program Instance or_impl_iff_morphism : *) diff --git a/theories/Classes/Morphisms_Relations.v b/theories/Classes/Morphisms_Relations.v index 5018fa01..1b389667 100644 --- a/theories/Classes/Morphisms_Relations.v +++ b/theories/Classes/Morphisms_Relations.v @@ -48,3 +48,11 @@ Proof. intro. apply (predicate_equivalence_pointwise (cons A (cons A nil))). Qed Instance subrelation_pointwise : Morphism (subrelation ==> pointwise_relation (A:=A) (pointwise_relation (A:=A) impl)) id. Proof. intro. apply (predicate_implication_pointwise (cons A (cons A nil))). Qed. + + +Lemma inverse_pointwise_relation A (R : relation A) : + relation_equivalence (pointwise_relation (inverse R)) (inverse (pointwise_relation (A:=A) R)). +Proof. intros. split; firstorder. Qed. + + + diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index a9a53068..9a43a1ba 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-emacs-U" "-top" "Coq.Classes.RelationClasses") -*- *) +(* -*- coq-prog-name: "coqtop.byte"; coq-prog-args: ("-emacs-U" "-top" "Coq.Classes.RelationClasses") -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* R x y -> False. -Definition pointwise_relation {A B : Type} (R : relation B) : relation (A -> B) := - fun f g => forall x : A, R (f x) (g x). - (** These are convertible. *) Lemma complement_inverse : forall A (R : relation A), complement (inverse R) = inverse (complement R). @@ -42,7 +43,7 @@ Class Reflexive A (R : relation A) := reflexivity : forall x, R x x. Class Irreflexive A (R : relation A) := - irreflexivity :> Reflexive A (complement R). + irreflexivity :> Reflexive (complement R). Class Symmetric A (R : relation A) := symmetry : forall x y, R x y -> R y x. @@ -53,12 +54,6 @@ Class Asymmetric A (R : relation A) := Class Transitive A (R : relation A) := transitivity : forall x y z, R x y -> R y z -> R x z. -Implicit Arguments Reflexive [A]. -Implicit Arguments Irreflexive [A]. -Implicit Arguments Symmetric [A]. -Implicit Arguments Asymmetric [A]. -Implicit Arguments Transitive [A]. - Hint Resolve @irreflexivity : ord. Unset Implicit Arguments. @@ -91,7 +86,7 @@ Program Instance Reflexive_complement_Irreflexive [ Reflexive A (R : relation A) unfold complement. red. intros H. intros H' ; apply H'. - apply (reflexivity H). + apply reflexivity. Qed. @@ -129,7 +124,7 @@ Ltac simpl_relation := unfold flip, impl, arrow ; try reduce ; program_simpl ; try ( solve [ intuition ]). -Ltac obligations_tactic ::= simpl_relation. +Ltac obligation_tactic ::= simpl_relation. (** Logical implication. *) @@ -171,17 +166,17 @@ Class Equivalence (carrier : Type) (equiv : relation carrier) : Prop := (** An Equivalence is a PER plus reflexivity. *) -Instance Equivalence_PER [ Equivalence A R ] : PER A R := +Instance Equivalence_PER [ Equivalence A R ] : PER A R | 10 := PER_Symmetric := Equivalence_Symmetric ; PER_Transitive := Equivalence_Transitive. (** We can now define antisymmetry w.r.t. an equivalence relation on the carrier. *) -Class [ Equivalence A eqA ] => Antisymmetric (R : relation A) := +Class Antisymmetric ((equ : Equivalence A eqA)) (R : relation A) := antisymmetry : forall x y, R x y -> R y x -> eqA x y. -Program Instance flip_antiSymmetric [ eq : Equivalence A eqA, ! Antisymmetric eq R ] : - Antisymmetric eq (flip R). +Program Instance flip_antiSymmetric {{Antisymmetric A eqA R}} : + ! Antisymmetric A eqA (flip R). (** Leibinz equality [eq] is an equivalence relation. The instance has low priority as it is always applicable @@ -372,7 +367,7 @@ Proof. intro A. exact (@predicate_implication_preorder (cons A (cons A nil))). Q We give an equivalent definition, up-to an equivalence relation on the carrier. *) -Class [ equ : Equivalence A eqA, PreOrder A R ] => PartialOrder := +Class [ equ : Equivalence A eqA, preo : PreOrder A R ] => PartialOrder := partial_order_equivalence : relation_equivalence eqA (relation_conjunction R (inverse R)). (** The equivalence proof is sufficient for proving that [R] must be a morphism @@ -394,7 +389,3 @@ Program Instance subrelation_partial_order : Proof. unfold relation_equivalence in *. firstorder. Qed. - -Lemma inverse_pointwise_relation A (R : relation A) : - relation_equivalence (pointwise_relation (inverse R)) (inverse (pointwise_relation (A:=A) R)). -Proof. reflexivity. Qed. diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v index a9bdaa8f..178d5333 100644 --- a/theories/Classes/SetoidClass.v +++ b/theories/Classes/SetoidClass.v @@ -13,7 +13,7 @@ Institution: LRI, CNRS UMR 8623 - UniversitĂcopyright Paris Sud 91405 Orsay, France *) -(* $Id: SetoidClass.v 11065 2008-06-06 22:39:43Z msozeau $ *) +(* $Id: SetoidClass.v 11282 2008-07-28 11:51:53Z msozeau $ *) Set Implicit Arguments. Unset Strict Implicit. @@ -41,13 +41,13 @@ Typeclasses unfold equiv. (** Shortcuts to make proof search easier. *) Definition setoid_refl [ sa : Setoid A ] : Reflexive equiv. -Proof. eauto with typeclass_instances. Qed. +Proof. typeclasses eauto. Qed. Definition setoid_sym [ sa : Setoid A ] : Symmetric equiv. -Proof. eauto with typeclass_instances. Qed. +Proof. typeclasses eauto. Qed. Definition setoid_trans [ sa : Setoid A ] : Transitive equiv. -Proof. eauto with typeclass_instances. Qed. +Proof. typeclasses eauto. Qed. Existing Instance setoid_refl. Existing Instance setoid_sym. @@ -123,7 +123,7 @@ Ltac setoidify := repeat setoidify_tac. (** Every setoid relation gives rise to a morphism, in fact every partial setoid does. *) Program Definition setoid_morphism [ sa : Setoid A ] : Morphism (equiv ++> equiv ++> iff) equiv := - trans_sym_morphism. + PER_morphism. (** Add this very useful instance in the database. *) @@ -142,7 +142,7 @@ Program Instance type_equivalence : Equivalence Type type_eq. Ltac morphism_tac := try red ; unfold arrow ; intros ; program_simpl ; try tauto. -Ltac obligations_tactic ::= morphism_tac. +Ltac obligation_tactic ::= morphism_tac. (** These are morphisms used to rewrite at the top level of a proof, using [iff_impl_id_morphism] if the proof is in [Prop] and @@ -178,4 +178,4 @@ Infix "=~=" := pequiv (at level 70, no associativity) : type_scope. (** Reset the default Program tactic. *) -Ltac obligations_tactic ::= program_simpl. +Ltac obligation_tactic ::= program_simpl. diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v index cf3d202d..8a069343 100644 --- a/theories/Classes/SetoidDec.v +++ b/theories/Classes/SetoidDec.v @@ -13,7 +13,7 @@ * Institution: LRI, CNRS UMR 8623 - UniversitĂcopyright Paris Sud * 91405 Orsay, France *) -(* $Id: SetoidDec.v 10919 2008-05-11 22:04:26Z msozeau $ *) +(* $Id: SetoidDec.v 11282 2008-07-28 11:51:53Z msozeau $ *) Set Implicit Arguments. Unset Strict Implicit. @@ -27,12 +27,12 @@ Require Export Coq.Classes.SetoidClass. Require Import Coq.Logic.Decidable. -Class [ Setoid A ] => DecidableSetoid := +Class DecidableSetoid A [ Setoid A ] := setoid_decidable : forall x y : A, decidable (x == y). (** The [EqDec] class gives a decision procedure for a particular setoid equality. *) -Class [ Setoid A ] => EqDec := +Class (( s : Setoid A )) => EqDec := equiv_dec : forall x y : A, { x == y } + { x =/= y }. (** We define the [==] overloaded notation for deciding equality. It does not take precedence @@ -75,18 +75,18 @@ Require Import Coq.Arith.Arith. (** The equiv is burried inside the setoid, but we can recover it by specifying which setoid we're talking about. *) -Program Instance eq_setoid : Setoid A := +Program Instance eq_setoid A : Setoid A := equiv := eq ; setoid_equiv := eq_equivalence. -Program Instance nat_eq_eqdec : EqDec (@eq_setoid nat) := +Program Instance nat_eq_eqdec : EqDec (eq_setoid nat) := equiv_dec := eq_nat_dec. Require Import Coq.Bool.Bool. -Program Instance bool_eqdec : EqDec (@eq_setoid bool) := +Program Instance bool_eqdec : EqDec (eq_setoid bool) := equiv_dec := bool_dec. -Program Instance unit_eqdec : EqDec (@eq_setoid unit) := +Program Instance unit_eqdec : EqDec (eq_setoid unit) := equiv_dec x y := in_left. Next Obligation. @@ -95,7 +95,7 @@ Program Instance unit_eqdec : EqDec (@eq_setoid unit) := reflexivity. Qed. -Program Instance prod_eqdec [ ! EqDec (@eq_setoid A), ! EqDec (@eq_setoid B) ] : EqDec (@eq_setoid (prod A B)) := +Program Instance prod_eqdec [ ! EqDec (eq_setoid A), ! EqDec (eq_setoid B) ] : EqDec (eq_setoid (prod A B)) := equiv_dec x y := let '(x1, x2) := x in let '(y1, y2) := y in @@ -110,7 +110,7 @@ Program Instance prod_eqdec [ ! EqDec (@eq_setoid A), ! EqDec (@eq_setoid B) ] : Require Import Coq.Program.FunctionalExtensionality. -Program Instance bool_function_eqdec [ ! EqDec (@eq_setoid A) ] : EqDec (@eq_setoid (bool -> A)) := +Program Instance bool_function_eqdec [ ! EqDec (eq_setoid A) ] : EqDec (eq_setoid (bool -> A)) := equiv_dec f g := if f true == g true then if f false == g false then in_left diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v index b29a52cc..6398b125 100644 --- a/theories/Classes/SetoidTactics.v +++ b/theories/Classes/SetoidTactics.v @@ -13,7 +13,7 @@ * Institution: LRI, CNRS UMR 8623 - UniversitĂcopyright Paris Sud * 91405 Orsay, France *) -(* $Id: SetoidTactics.v 10921 2008-05-12 12:27:25Z msozeau $ *) +(* $Id: SetoidTactics.v 11282 2008-07-28 11:51:53Z msozeau $ *) Require Export Coq.Classes.RelationClasses. Require Export Coq.Classes.Morphisms. @@ -24,11 +24,22 @@ Require Export Coq.Relations.Relation_Definitions. Set Implicit Arguments. Unset Strict Implicit. +(** Setoid relation on a given support: declares a relation as a setoid + for use with rewrite. It helps choosing if a rewrite should be handled + by setoid_rewrite or the regular rewrite using leibniz equality. + Users can declare an [SetoidRelation A RA] anywhere to declare default + relations. This is also done automatically by the [Declare Relation A RA] + commands. *) + +Class SetoidRelation A (R : relation A). + +Instance impl_setoid_relation : SetoidRelation impl. +Instance iff_setoid_relation : SetoidRelation iff. + (** Default relation on a given support. Can be used by tactics to find a sensible default relation on any carrier. Users can - declare an [Instance A RA] anywhere to declare default relations. - This is also done by the [Declare Relation A RA] command with no - parameters for backward compatibility. *) + declare an [Instance def : DefaultRelation A RA] anywhere to + declare default relations. *) Class DefaultRelation A (R : relation A). @@ -38,7 +49,7 @@ Definition default_relation [ DefaultRelation A R ] := R. (** Every [Equivalence] gives a default relation, if no other is given (lowest priority). *) -Instance equivalence_default [ Equivalence A R ] : DefaultRelation A R | 4. +Instance equivalence_default [ Equivalence A R ] : DefaultRelation R | 4. (** The setoid_replace tactics in Ltac, defined in terms of default relations and the setoid_rewrite tactic. *) @@ -174,3 +185,5 @@ Ltac default_add_morphism_tactic := end. Ltac add_morphism_tactic := default_add_morphism_tactic. + +Ltac obligation_tactic ::= program_simpl. -- cgit v1.2.3