diff options
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Classes/Equivalence.v | 112 | ||||
| -rw-r--r-- | theories/Classes/Functions.v | 14 | ||||
| -rw-r--r-- | theories/Classes/Morphisms.v | 242 | ||||
| -rw-r--r-- | theories/Classes/Relations.v | 58 | ||||
| -rw-r--r-- | theories/Classes/SetoidClass.v | 2 | ||||
| -rw-r--r-- | theories/Classes/SetoidDec.v | 20 | ||||
| -rw-r--r-- | theories/Classes/SetoidTactics.v | 3 | ||||
| -rw-r--r-- | theories/Program/Basics.v | 29 | ||||
| -rw-r--r-- | theories/Program/FunctionalExtensionality.v | 1 |
9 files changed, 269 insertions, 212 deletions
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v index bd525e0356..bf26021800 100644 --- a/theories/Classes/Equivalence.v +++ b/theories/Classes/Equivalence.v @@ -16,26 +16,27 @@ (* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *) +Require Export Coq.Program.Basics. Require Import Coq.Program.Program. + Require Import Coq.Classes.Init. +Require Export Coq.Classes.Relations. +Require Export Coq.Classes.Morphisms. Set Implicit Arguments. Unset Strict Implicit. -Require Export Coq.Classes.Relations. -Require Export Coq.Classes.Morphisms. - Definition equiv [ Equivalence A R ] : relation A := R. (** Shortcuts to make proof search possible (unification won't unfold equiv). *) -Definition equivalence_refl [ sa : Equivalence A ] : Reflexive equiv. +Definition equivalence_refl [ sa : ! Equivalence A ] : Reflexive equiv. Proof. eauto with typeclass_instances. Qed. -Definition equivalence_sym [ sa : Equivalence A ] : Symmetric equiv. +Definition equivalence_sym [ sa : ! Equivalence A ] : Symmetric equiv. Proof. eauto with typeclass_instances. Qed. -Definition equivalence_trans [ sa : Equivalence A ] : Transitive equiv. +Definition equivalence_trans [ sa : ! Equivalence A ] : Transitive equiv. Proof. eauto with typeclass_instances. Qed. (** Overloaded notations for setoid equivalence and inequivalence. Not to be confused with [eq] and [=]. *) @@ -43,20 +44,22 @@ Proof. eauto with typeclass_instances. Qed. (** Subset objects should be first coerced to their underlying type, but that notation doesn't work in the standard case then. *) (* Notation " x == y " := (equiv (x :>) (y :>)) (at level 70, no associativity) : type_scope. *) -Notation " x == y " := (equiv x y) (at level 70, no associativity) : type_scope. +Notation " x === y " := (equiv x y) (at level 70, no associativity) : equiv_scope. + +Notation " x =/= y " := (complement equiv x y) (at level 70, no associativity) : equiv_scope. -Notation " x =/= y " := (complement equiv x y) (at level 70, no associativity) : type_scope. +Open Local Scope equiv_scope. (** Use the [clsubstitute] command which substitutes an equality in every hypothesis. *) Ltac clsubst H := match type of H with - ?x == ?y => clsubstitute H ; clear H x + ?x === ?y => clsubstitute H ; clear H x end. Ltac clsubst_nofail := match goal with - | [ H : ?x == ?y |- _ ] => clsubst H ; clsubst_nofail + | [ H : ?x === ?y |- _ ] => clsubst H ; clsubst_nofail | _ => idtac end. @@ -64,29 +67,62 @@ Ltac clsubst_nofail := Tactic Notation "clsubst" "*" := clsubst_nofail. -Lemma nequiv_equiv_trans : forall [ Equivalence A ] (x y z : A), x =/= y -> y == z -> x =/= z. +Ltac setoidreplace H t := + let Heq := fresh "Heq" in + cut(H) ; [ intro Heq ; setoid_rewrite Heq ; clear Heq | unfold equiv ; t ]. + +Ltac setoidreplacein H H' t := + let Heq := fresh "Heq" in + cut(H) ; [ intro Heq ; setoid_rewrite Heq in H' ; clear Heq | unfold equiv ; t ]. + +Tactic Notation "setoid_replace" constr(x) "with" constr(y) := + setoidreplace (x === y) idtac. + +Tactic Notation "setoid_replace" constr(x) "with" constr(y) "in" hyp(id) := + setoidreplacein (x === y) id idtac. + +Tactic Notation "setoid_replace" constr(x) "with" constr(y) "by" tactic(t) := + setoidreplace (x === y) ltac:t. + +Tactic Notation "setoid_replace" constr(x) "with" constr(y) "in" hyp(id) "by" tactic(t) := + setoidreplacein (x === y) id ltac:t. + +Tactic Notation "setoid_replace" constr(x) "with" constr(y) "using" "relation" constr(rel) := + setoidreplace (rel x y) idtac. + +Tactic Notation "setoid_replace" constr(x) "with" constr(y) + "using" "relation" constr(rel) "by" tactic(t) := + setoidreplace (rel x y) ltac:t. + +Tactic Notation "setoid_replace" constr(x) "with" constr(y) "in" hyp(id) + "using" "relation" constr(rel) := + setoidreplacein (rel x y) id idtac. + +Tactic Notation "setoid_replace" constr(x) "with" constr(y) "in" hyp(id) + "using" "relation" constr(rel) "by" tactic(t) := + setoidreplacein (rel x y) id ltac:t. + +Lemma nequiv_equiv_trans : forall [ ! Equivalence A ] (x y z : A), x =/= y -> y === z -> x =/= z. Proof with auto. intros; intro. - assert(z == y) by relation_sym. - assert(x == y) by relation_trans. + assert(z === y) by relation_sym. + assert(x === y) by relation_trans. contradiction. Qed. -Lemma equiv_nequiv_trans : forall [ Equivalence A ] (x y z : A), x == y -> y =/= z -> x =/= z. +Lemma equiv_nequiv_trans : forall [ ! Equivalence A ] (x y z : A), x === y -> y =/= z -> x =/= z. Proof. intros; intro. - assert(y == x) by relation_sym. - assert(y == z) by relation_trans. + assert(y === x) by relation_sym. + assert(y === z) by relation_trans. contradiction. Qed. -Open Scope type_scope. - Ltac equiv_simplify_one := match goal with - | [ H : ?x == ?x |- _ ] => clear H - | [ H : ?x == ?y |- _ ] => clsubst H - | [ |- ?x =/= ?y ] => let name:=fresh "Hneq" in intro name + | [ H : (?x === ?x)%type |- _ ] => clear H + | [ H : (?x === ?y)%type |- _ ] => clsubst H + | [ |- (?x =/= ?y)%type ] => let name:=fresh "Hneq" in intro name end. Ltac equiv_simplify := repeat equiv_simplify_one. @@ -101,13 +137,13 @@ Ltac equivify := repeat equivify_tac. (** Every equivalence relation gives rise to a morphism, as it is transitive and symmetric. *) -Instance [ sa : Equivalence A ] => equiv_morphism : ? Morphism (equiv ++> equiv ++> iff) equiv := +Instance [ sa : ! Equivalence ] => equiv_morphism : Morphism (equiv ++> equiv ++> iff) equiv := respect := respect. (** The partial application too as it is reflexive. *) -Instance [ sa : Equivalence A ] (x : A) => - equiv_partial_app_morphism : ? Morphism (equiv ++> iff) (equiv x) := +Instance [ sa : ! Equivalence A ] (x : A) => + equiv_partial_app_morphism : Morphism (equiv ++> iff) (equiv x) := respect := respect. Definition type_eq : relation Type := @@ -125,24 +161,11 @@ Ltac obligations_tactic ::= morphism_tac. using [iff_impl_id_morphism] if the proof is in [Prop] and [eq_arrow_id_morphism] if it is in Type. *) -Program Instance iff_impl_id_morphism : ? Morphism (iff ++> impl) id. +Program Instance iff_impl_id_morphism : + Morphism (iff ++> impl) id. (* Program Instance eq_arrow_id_morphism : ? Morphism (eq +++> arrow) id. *) -(* Definition compose_respect (A B C : Type) (R : relation (A -> B)) (R' : relation (B -> C)) *) -(* (x y : A -> C) : Prop := forall (f : A -> B) (g : B -> C), R f f -> R' g g. *) - -(* Program Instance (A B C : Type) (R : relation (A -> B)) (R' : relation (B -> C)) *) -(* [ mg : ? Morphism R' g ] [ mf : ? Morphism R f ] => *) -(* compose_morphism : ? Morphism (compose_respect R R') (g o f). *) - -(* Next Obligation. *) -(* Proof. *) -(* apply (respect (m0:=mg)). *) -(* apply (respect (m0:=mf)). *) -(* assumption. *) -(* Qed. *) - (** Partial equivs don't require reflexivity so we can build a partial equiv on the function space. *) Class PartialEquivalence (carrier : Type) (pequiv : relation carrier) := @@ -155,3 +178,14 @@ Class PartialEquivalence (carrier : Type) (pequiv : relation carrier) := (** Reset the default Program tactic. *) Ltac obligations_tactic ::= program_simpl. + +(** Default relation on a given support. *) + +Class DefaultRelation A := default_relation : relation A. + +(** Every [Equivalence] gives a default relation, if no other is given (lowest priority). *) + +Instance [ ! Equivalence A R ] => + equivalence_default : DefaultRelation A | 4 := + default_relation := R. + diff --git a/theories/Classes/Functions.v b/theories/Classes/Functions.v index 7942d36427..c08dee76f3 100644 --- a/theories/Classes/Functions.v +++ b/theories/Classes/Functions.v @@ -22,22 +22,22 @@ Require Export Coq.Classes.Morphisms. Set Implicit Arguments. Unset Strict Implicit. -Class [ m : Morphism (A -> B) (RA ++> RB) f ] => Injective := +Class [ m : ! Morphism (A -> B) (RA ++> RB) f ] => Injective := injective : forall x y : A, RB (f x) (f y) -> RA x y. -Class [ m : Morphism (A -> B) (RA ++> RB) f ] => Surjective := +Class [ m : ! Morphism (A -> B) (RA ++> RB) f ] => Surjective := 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 [ m : ! Morphism (A -> B) (eqA ++> eqB) ] => MonoMorphism := monic :> Injective m. -Class [ m : Morphism (A -> B) (eqA ++> eqB) ] => EpiMorphism := +Class [ m : ! Morphism (A -> B) (eqA ++> eqB) ] => EpiMorphism := epic :> Surjective m. -Class [ m : Morphism (A -> B) (eqA ++> eqB) ] => IsoMorphism := +Class [ m : ! Morphism (A -> B) (eqA ++> eqB) ] => IsoMorphism := 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/Morphisms.v b/theories/Classes/Morphisms.v index 5d679d2c9a..fb0acb39ca 100644 --- a/theories/Classes/Morphisms.v +++ b/theories/Classes/Morphisms.v @@ -10,7 +10,7 @@ (* Typeclass-based morphisms with standard instances for equivalence relations. Author: Matthieu Sozeau - Institution: LRI, CNRS UMR 8623 - UniversitĂcopyright Paris Sud + Institution: LRI, CNRS UMR 8623 - UniversitĂcopyright Paris Sud 91405 Orsay, France *) (* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *) @@ -37,8 +37,8 @@ Definition respectful A (R : relation A) B (R' : relation B) : relation (A -> B) (** Notations reminiscent of the old syntax for declaring morphisms. *) -Notation " R ==> R' " := (@respectful _ R _ R') (right associativity, at level 20). Notation " R ++> R' " := (@respectful _ R _ R') (right associativity, at level 20). +Notation " R ==> R' " := (@respectful _ R _ R') (right associativity, at level 20). Notation " R --> R' " := (@respectful _ (inverse R) _ R') (right associativity, at level 20). (** A morphism on a relation [R] is an object respecting the relation (in its kernel). @@ -106,34 +106,87 @@ Qed. (* Program Definition arrow_morphism `A B` (m : A -> B) : Morphism (eq ++> eq) m. *) -(** Any binary morphism respecting some relations up to [iff] respects +(** Any morphism respecting some relations up to [iff] respects them up to [impl] in each way. Very important instances as we need [impl] morphisms at the top level when we rewrite. *) -Program Instance `A` (R : relation A) `B` (R' : relation B) - [ ? Morphism (R ++> R' ++> iff) m ] => +Class SubRelation A (R S : relation A) := + subrelation :> Morphism (S ==> R) (fun x => x). - iff_impl_binary_morphism : ? Morphism (R ++> R' ++> impl) m. +Instance iff_impl_subrelation : SubRelation Prop impl iff. +Proof. + constructor ; red ; intros. + tauto. +Qed. - Next Obligation. - Proof. - destruct respect with x y x0 y0 ; auto. - Qed. +Instance iff_inverse_impl_subrelation : SubRelation Prop (inverse impl) iff. +Proof. + constructor ; red ; intros. + tauto. +Qed. -Program Instance (A : Type) (R : relation A) `B` (R' : relation B) - [ ? Morphism (R ++> R' ++> iff) m ] => - iff_inverse_impl_binary_morphism : ? Morphism (R ++> R' ++> inverse impl) m. +Instance [ SubRelation A Râ Râ ] => + morphisms_subrelation : SubRelation (B -> A) (R ==> Râ) (R ==> Râ). +Proof. + constructor ; repeat red ; intros. + destruct subrelation. + red in respect0, H ; unfold id in *. + apply respect0. + apply H. + apply H0. +Qed. - Next Obligation. - Proof. - destruct respect with x y x0 y0 ; auto. - Qed. +(** High priority because it is always applicable and loops. *) + +Instance [ SubRelation A Râ Râ, Morphism Râ m ] => + subrelation_morphism : Morphism Râ m | 4. +Proof. + destruct subrelation. + red in respect0. + unfold id in * ; apply respect0. + apply respect. +Qed. + +(* Program Instance `A` (R : relation A) `B` (R' : relation B) *) +(* [ ? Morphism (R ==> R' ==> iff) m ] => *) +(* iff_impl_binary_morphism : ? Morphism (R ==> R' ==> impl) m. *) + +(* Next Obligation. *) +(* Proof. *) +(* destruct respect with x y x0 y0 ; auto. *) +(* Qed. *) + +(* Program Instance `A` (R : relation A) `B` (R' : relation B) *) +(* [ ? Morphism (R ==> R' ==> iff) m ] => *) +(* iff_inverse_impl_binary_morphism : ? Morphism (R ==> R' ==> inverse impl) m. *) + +(* Next Obligation. *) +(* Proof. *) +(* destruct respect with x y x0 y0 ; auto. *) +(* Qed. *) + + +(* Program Instance [ Morphism (A -> Prop) (R ==> iff) m ] => *) +(* iff_impl_morphism : ? Morphism (R ==> impl) m. *) + +(* Next Obligation. *) +(* Proof. *) +(* destruct respect with x y ; auto. *) +(* Qed. *) + +(* Program Instance [ Morphism (A -> Prop) (R ==> iff) m ] => *) +(* iff_inverse_impl_morphism : ? Morphism (R ==> inverse impl) m. *) + +(* Next Obligation. *) +(* Proof. *) +(* destruct respect with x y ; auto. *) +(* Qed. *) (** Logical implication [impl] is a morphism for logical equivalence. *) -Program Instance iff_iff_iff_impl_morphism : ? Morphism (iff ++> iff ++> iff) impl. +Program Instance iff_iff_iff_impl_morphism : Morphism (iff ==> iff ==> iff) impl. -Lemma reflexive_impl_iff [ Symmetric A R, ? Morphism (R ++> impl) m ] : Morphism (R ==> iff) m. +Lemma reflexive_impl_iff [ ! Symmetric A R, Morphism (R ==> impl) m ] : Morphism (R ==> iff) m. Proof. intros. constructor. red ; intros. @@ -142,8 +195,8 @@ Qed. (** The complement of a relation conserves its morphisms. *) -Program Instance `A` (RA : relation A) [ ? Morphism (RA ++> RA ++> iff) R ] => - complement_morphism : ? Morphism (RA ++> RA ++> iff) (complement R). +Program Instance {A} (RA : relation A) [ Morphism (RA ==> RA ==> iff) R ] => + complement_morphism : Morphism (RA ==> RA ==> iff) (complement R). Next Obligation. Proof. @@ -156,8 +209,8 @@ Program Instance `A` (RA : relation A) [ ? Morphism (RA ++> RA ++> iff) R ] => (** The inverse too. *) -Program Instance `A` (RA : relation A) [ ? Morphism (RA ++> RA ++> iff) R ] => - inverse_morphism : ? Morphism (RA ++> RA ++> iff) (inverse R). +Program Instance {A} (RA : relation A) [ Morphism (RA ==> RA ==> iff) R ] => + inverse_morphism : Morphism (RA ==> RA ==> iff) (inverse R). Next Obligation. Proof. @@ -165,8 +218,8 @@ Program Instance `A` (RA : relation A) [ ? Morphism (RA ++> RA ++> iff) R ] => apply respect ; auto. Qed. -Program Instance (A B C : Type) [ ? Morphism (RA ++> RB ++> RC) (f : A -> B -> C) ] => - flip_morphism : ? Morphism (RB ++> RA ++> RC) (flip f). +Program Instance {A B C : Type} [ Morphism (RA ==> RB ==> RC) (f : A -> B -> C) ] => + flip_morphism : Morphism (RB ==> RA ==> RC) (flip f). Next Obligation. Proof. @@ -174,51 +227,13 @@ Program Instance (A B C : Type) [ ? Morphism (RA ++> RB ++> RC) (f : A -> B -> C apply respect ; auto. Qed. -(* Definition respectful' A (R : relation A) B (R' : relation B) (f : A -> B) : relation A := *) -(* fun x y => R x y -> R' (f x) (f y). *) - -(* Definition morphism_respectful' A R B (R' : relation B) (f : A -> B) *) -(* [ ? Morphism (R ++> R') f ] (x y : A) : respectful' R R' f x y. *) -(* intros. *) -(* destruct H. *) -(* red in respect0. *) -(* red. *) -(* apply respect0. *) -(* Qed. *) - -(* Existing Instance morphism_respectful'. *) - -(* Goal forall A [ Equivalence A (eqA : relation A) ] R [ ? Morphism (eqA ++> iff) m ] (x y : A) *) -(* [ ? Morphism (eqA ++> eqA) m' ] (m' : A -> A), eqA x y -> True. *) -(* intros. *) -(* cut (relation A) ; intros R'. *) -(* cut ((eqA ++> R') m' m') ; intros. *) -(* assert({ R' : relation A & Reflexive R' }). *) -(* econstructor. *) -(* typeclass_instantiation. *) - - -(* assert (exists R' : relation A, Morphism ((fun x y => eqA x y -> R' (m' x) (m' y)) ++> iff) m). *) -(* eapply ex_intro. *) -(* unfold respectful. *) -(* typeclass_instantiation. *) - - -(* assert (exists R', Morphism (R' ++> iff) m /\ Morphism (eqA ++> R') m'). *) -(* typeclass_instantiation. *) -(* Set Printing All. *) -(* Show Proof. *) - - -(* apply respect. *) - (** Partial applications are ok when a proof of refl is available. *) (** A proof of [R x x] is available. *) (* Program Instance (A : Type) R B (R' : relation B) *) -(* [ ? Morphism (R ++> R') m ] [ ? Morphism R x ] => *) -(* morphism_partial_app_morphism : ? Morphism R' (m x). *) +(* [ Morphism (R ==> R') m ] [ Morphism R x ] => *) +(* morphism_partial_app_morphism : Morphism R' (m x). *) (* Next Obligation. *) (* Proof with auto. *) @@ -229,24 +244,24 @@ Program Instance (A B C : Type) [ ? Morphism (RA ++> RB ++> RC) (f : A -> B -> C (** Morpshism declarations for partial applications. *) -Program Instance [ Transitive A R ] (x : A) => - trans_contra_inv_impl_morphism : ? Morphism (R --> inverse impl) (R x). +Program Instance [ ! Transitive A R ] (x : A) => + trans_contra_inv_impl_morphism : Morphism (R --> inverse impl) (R x). Next Obligation. Proof with auto. trans y... Qed. -Program Instance [ Transitive A R ] (x : A) => - trans_co_impl_morphism : ? Morphism (R ++> impl) (R x). +Program Instance [ ! Transitive A R ] (x : A) => + trans_co_impl_morphism : Morphism (R ==> impl) (R x). Next Obligation. Proof with auto. trans x0... Qed. -Program Instance [ Transitive A R, Symmetric A R ] (x : A) => - trans_sym_co_inv_impl_morphism : ? Morphism (R ++> inverse impl) (R x). +Program Instance [ ! Transitive A R, Symmetric R ] (x : A) => + trans_sym_co_inv_impl_morphism : Morphism (R ==> inverse impl) (R x). Next Obligation. Proof with auto. @@ -254,8 +269,8 @@ Program Instance [ Transitive A R, Symmetric A R ] (x : A) => sym... Qed. -Program Instance [ Transitive A R, Symmetric A R ] (x : A) => - trans_sym_contra_impl_morphism : ? Morphism (R --> impl) (R x). +Program Instance [ ! Transitive A R, Symmetric R ] (x : A) => + trans_sym_contra_impl_morphism : Morphism (R --> impl) (R x). Next Obligation. Proof with auto. @@ -264,7 +279,7 @@ Program Instance [ Transitive A R, Symmetric A R ] (x : A) => Qed. Program Instance [ Equivalence A R ] (x : A) => - equivalence_partial_app_morphism : ? Morphism (R ++> iff) (R x). + equivalence_partial_app_morphism : Morphism (R ==> iff) (R x). Next Obligation. Proof with auto. @@ -277,8 +292,8 @@ Program Instance [ Equivalence A R ] (x : A) => (** With symmetric relations, variance is no issue ! *) (* Program Instance (A B : Type) (R : relation A) (R' : relation B) *) -(* [ Morphism _ (R ++> R') m ] [ Symmetric A R ] => *) -(* sym_contra_morphism : ? Morphism (R --> R') m. *) +(* [ Morphism _ (R ==> R') m ] [ Symmetric A R ] => *) +(* sym_contra_morphism : Morphism (R --> R') m. *) (* Next Obligation. *) (* Proof with auto. *) @@ -289,8 +304,8 @@ Program Instance [ Equivalence A R ] (x : A) => (** [R] is reflexive, hence we can build the needed proof. *) Program Instance (A B : Type) (R : relation A) (R' : relation B) - [ ? Morphism (R ++> R') m ] [ Reflexive A R ] (x : A) => - reflexive_partial_app_morphism : ? Morphism R' (m x). + [ Morphism (R ==> R') m ] [ Reflexive R ] (x : A) => + reflexive_partial_app_morphism : Morphism R' (m x) | 3. Next Obligation. Proof with auto. @@ -302,8 +317,8 @@ Program Instance (A B : Type) (R : relation A) (R' : relation B) (** Every transitive relation induces a morphism by "pushing" an [R x y] on the left of an [R x z] proof to get an [R y z] goal. *) -Program Instance [ Transitive A R ] => - trans_co_eq_inv_impl_morphism : ? Morphism (R ++> eq ++> inverse impl) R. +Program Instance [ ! Transitive A R ] => + trans_co_eq_inv_impl_morphism : Morphism (R ==> eq ==> inverse impl) R. Next Obligation. Proof with auto. @@ -311,8 +326,8 @@ Program Instance [ Transitive A R ] => subst x0... Qed. -Program Instance [ Transitive A R ] => - trans_contra_eq_inv_impl_morphism : ? Morphism (R --> eq ++> impl) R. +Program Instance [ ! Transitive A R ] => + trans_contra_eq_impl_morphism : Morphism (R --> eq ==> impl) R. Next Obligation. Proof with auto. @@ -322,8 +337,8 @@ Program Instance [ Transitive A R ] => (** Every symmetric and transitive relation gives rise to an equivariant morphism. *) -Program Instance [ Transitive A R, Symmetric A R ] => - trans_sym_morphism : ? Morphism (R ++> R ++> iff) R. +Program Instance [ ! Transitive A R, Symmetric R ] => + trans_sym_morphism : Morphism (R ==> R ==> iff) R. Next Obligation. Proof with auto. @@ -334,7 +349,7 @@ Program Instance [ Transitive A R, Symmetric A R ] => Qed. Program Instance [ Equivalence A R ] => - equiv_morphism : ? Morphism (R ++> R ++> iff) R. + equiv_morphism : Morphism (R ==> R ==> iff) R. Next Obligation. Proof with auto. @@ -346,44 +361,65 @@ Program Instance [ Equivalence A R ] => (** In case the rewrite happens at top level. *) -Program Instance iff_inverse_impl_id : - ? Morphism (iff ++> inverse impl) id. +Program Instance iff_inverse_impl_id : + Morphism (iff ==> inverse impl) id. -Program Instance inverse_iff_inverse_impl_id : - ? Morphism (iff --> inverse impl) id. +Program Instance inverse_iff_inverse_impl_id : + Morphism (iff --> inverse impl) id. -Program Instance iff_impl_id : - ? Morphism (iff ++> impl) id. +Program Instance iff_impl_id : + Morphism (iff ==> impl) id. -Program Instance inverse_iff_impl_id : - ? Morphism (iff --> impl) id. +Program Instance inverse_iff_impl_id : + Morphism (iff --> impl) id. (** Standard instances for [iff] and [impl]. *) (** Logical conjunction. *) -Program Instance and_impl_iff_morphism : ? Morphism (impl ++> iff ++> impl) and. +Program Instance and_impl_iff_morphism : + Morphism (impl ==> iff ==> impl) and. -Program Instance and_iff_impl_morphism : ? Morphism (iff ++> impl ++> impl) and. +Program Instance and_iff_impl_morphism : + Morphism (iff ==> impl ==> impl) and. Program Instance and_inverse_impl_iff_morphism : - ? Morphism (inverse impl ++> iff ++> inverse impl) and. + Morphism (inverse impl ==> iff ==> inverse impl) and. Program Instance and_iff_inverse_impl_morphism : - ? Morphism (iff ++> inverse impl ++> inverse impl) and. + Morphism (iff ==> inverse impl ==> inverse impl) and. -Program Instance and_iff_morphism : ? Morphism (iff ++> iff ++> iff) and. +Program Instance and_iff_morphism : + Morphism (iff ==> iff ==> iff) and. (** Logical disjunction. *) -Program Instance or_impl_iff_morphism : ? Morphism (impl ++> iff ++> impl) or. +Program Instance or_impl_iff_morphism : + Morphism (impl ==> iff ==> impl) or. -Program Instance or_iff_impl_morphism : ? Morphism (iff ++> impl ++> impl) or. +Program Instance or_iff_impl_morphism : + Morphism (iff ==> impl ==> impl) or. Program Instance or_inverse_impl_iff_morphism : - ? Morphism (inverse impl ++> iff ++> inverse impl) or. + Morphism (inverse impl ==> iff ==> inverse impl) or. Program Instance or_iff_inverse_impl_morphism : - ? Morphism (iff ++> inverse impl ++> inverse impl) or. + Morphism (iff ==> inverse impl ==> inverse impl) or. + +Program Instance or_iff_morphism : + Morphism (iff ==> iff ==> iff) or. -Program Instance or_iff_morphism : ? Morphism (iff ++> iff ++> iff) or. +(** Coq functions are morphisms for leibniz equality, + applied only if really needed. *) + +Instance {A B : Type} (m : A -> B) => + any_eq_eq_morphism : Morphism (@Logic.eq A ==> @Logic.eq B) m | 4. +Proof. + red ; intros. subst ; reflexivity. +Qed. + +Instance {A : Type} (m : A -> Prop) => + any_eq_iff_morphism : Morphism (@Logic.eq A ==> iff) m | 4. +Proof. + red ; intros. subst ; reflexivity. +Qed. diff --git a/theories/Classes/Relations.v b/theories/Classes/Relations.v index 28f582c3d7..b14647d065 100644 --- a/theories/Classes/Relations.v +++ b/theories/Classes/Relations.v @@ -63,46 +63,46 @@ Hint Resolve @irreflexive : ord. (** We can already dualize all these properties. *) -Program Instance [ Reflexive A R ] => flip_reflexive : Reflexive A (flip R) := +Program Instance [ bla : ! Reflexive A R ] => flip_reflexive : Reflexive (flip R) := reflexive := reflexive (R:=R). -Program Instance [ Irreflexive A R ] => flip_irreflexive : Irreflexive A (flip R) := +Program Instance [ ! Irreflexive A R ] => flip_irreflexive : Irreflexive (flip R) := irreflexive := irreflexive (R:=R). -Program Instance [ Symmetric A R ] => flip_symmetric : Symmetric A (flip R). +Program Instance [ ! Symmetric A R ] => flip_symmetric : Symmetric (flip R). Solve Obligations using unfold flip ; program_simpl ; clapply symmetric. -Program Instance [ Asymmetric A R ] => flip_asymmetric : Asymmetric A (flip R). +Program Instance [ ! Asymmetric A R ] => flip_asymmetric : Asymmetric (flip R). Solve Obligations using program_simpl ; unfold flip in * ; intros ; clapply asymmetric. -Program Instance [ Transitive A R ] => flip_transitive : Transitive A (flip R). +Program Instance [ ! Transitive A R ] => flip_transitive : Transitive (flip R). Solve Obligations using unfold flip ; program_simpl ; clapply transitive. (** Have to do it again for Prop. *) -Program Instance [ Reflexive A (R : relation A) ] => inverse_reflexive : Reflexive A (inverse R) := +Program Instance [ ! Reflexive A (R : relation A) ] => inverse_reflexive : Reflexive (inverse R) := reflexive := reflexive (R:=R). -Program Instance [ Irreflexive A (R : relation A) ] => inverse_irreflexive : Irreflexive A (inverse R) := +Program Instance [ ! Irreflexive A (R : relation A) ] => inverse_irreflexive : Irreflexive (inverse R) := irreflexive := irreflexive (R:=R). -Program Instance [ Symmetric A (R : relation A) ] => inverse_symmetric : Symmetric A (inverse R). +Program Instance [ ! Symmetric A (R : relation A) ] => inverse_symmetric : Symmetric (inverse R). Solve Obligations using unfold inverse, flip ; program_simpl ; clapply symmetric. -Program Instance [ Asymmetric A (R : relation A) ] => inverse_asymmetric : Asymmetric A (inverse R). +Program Instance [ ! Asymmetric A (R : relation A) ] => inverse_asymmetric : Asymmetric (inverse R). Solve Obligations using program_simpl ; unfold inverse, flip in * ; intros ; clapply asymmetric. -Program Instance [ Transitive A (R : relation A) ] => inverse_transitive : Transitive A (inverse R). +Program Instance [ ! Transitive A (R : relation A) ] => inverse_transitive : Transitive (inverse R). Solve Obligations using unfold inverse, flip ; program_simpl ; clapply transitive. -Program Instance [ Reflexive A (R : relation A) ] => - reflexive_complement_irreflexive : Irreflexive A (complement R). +Program Instance [ ! Reflexive A (R : relation A) ] => + reflexive_complement_irreflexive : Irreflexive (complement R). Next Obligation. Proof. @@ -110,8 +110,8 @@ Program Instance [ Reflexive A (R : relation A) ] => apply reflexive. Qed. -Program Instance [ Irreflexive A (R : relation A) ] => - irreflexive_complement_reflexive : Reflexive A (complement R). +Program Instance [ ! Irreflexive A (R : relation A) ] => + irreflexive_complement_reflexive : Reflexive (complement R). Next Obligation. Proof. @@ -119,7 +119,7 @@ Program Instance [ Irreflexive A (R : relation A) ] => apply (irreflexive H). Qed. -Program Instance [ Symmetric A (R : relation A) ] => complement_symmetric : Symmetric A (complement R). +Program Instance [ ! Symmetric A (R : relation A) ] => complement_symmetric : Symmetric (complement R). Next Obligation. Proof. @@ -137,20 +137,20 @@ Ltac obligations_tactic ::= simpl_relation. (** Logical implication. *) -Program Instance impl_refl : ? Reflexive impl. -Program Instance impl_trans : ? Transitive impl. +Program Instance impl_refl : Reflexive impl. +Program Instance impl_trans : Transitive impl. (** Logical equivalence. *) -Program Instance iff_refl : ? Reflexive iff. -Program Instance iff_sym : ? Symmetric iff. -Program Instance iff_trans : ? Transitive iff. +Program Instance iff_refl : Reflexive iff. +Program Instance iff_sym : Symmetric iff. +Program Instance iff_trans : Transitive iff. (** Leibniz equality. *) -Program Instance eq_refl : ? Reflexive (@eq A). -Program Instance eq_sym : ? Symmetric (@eq A). -Program Instance eq_trans : ? Transitive (@eq A). +Program Instance eq_refl : Reflexive (@eq A). +Program Instance eq_sym : Symmetric (@eq A). +Program Instance eq_trans : Transitive (@eq A). (** ** General tactics to solve goals on relations. Each tactic comes in two flavors: @@ -298,9 +298,7 @@ Class PreOrder A (R : relation A) := preorder_refl :> Reflexive R ; preorder_trans :> Transitive R. -(** A [PreOrder] is both reflexive and transitive. *) - -(** The [PER] typeclass. *) +(** A partial equivalence relation is symmetric and transitive. *) Class PER (carrier : Type) (pequiv : relation carrier) := per_sym :> Symmetric pequiv ; @@ -332,13 +330,13 @@ Class Equivalence (carrier : Type) (equiv : relation carrier) := Class [ Equivalence A eqA ] => Antisymmetric (R : relation A) := antisymmetric : forall x y, R x y -> R y x -> eqA x y. -Program Instance [ eq : Equivalence A eqA, ? Antisymmetric eq R ] => - flip_antisymmetric : ? Antisymmetric eq (flip R). +Program Instance [ eq : Equivalence A eqA, Antisymmetric eq R ] => + flip_antisymmetric : Antisymmetric eq (flip R). Solve Obligations using unfold inverse, flip ; program_simpl ; eapply @antisymmetric ; eauto. -Program Instance [ eq : Equivalence A eqA, ? Antisymmetric eq (R : relation A) ] => - inverse_antisymmetric : ? Antisymmetric eq (inverse R). +Program Instance [ eq : Equivalence A eqA, Antisymmetric eq (R : relation A) ] => + inverse_antisymmetric : Antisymmetric eq (inverse R). Solve Obligations using unfold inverse, flip ; program_simpl ; eapply @antisymmetric ; eauto. diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v index 571f65b627..9dd4f61812 100644 --- a/theories/Classes/SetoidClass.v +++ b/theories/Classes/SetoidClass.v @@ -149,7 +149,7 @@ Ltac obligations_tactic ::= morphism_tac. using [iff_impl_id_morphism] if the proof is in [Prop] and [eq_arrow_id_morphism] if it is in Type. *) -Program Instance iff_impl_id_morphism : ? Morphism (iff ++> impl) id. +Program Instance iff_impl_id_morphism : Morphism (iff ++> impl) id. (* Program Instance eq_arrow_id_morphism : ? Morphism (eq +++> arrow) id. *) diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v index c385fc5b5c..8a435b4493 100644 --- a/theories/Classes/SetoidDec.v +++ b/theories/Classes/SetoidDec.v @@ -42,7 +42,7 @@ Notation " x == y " := (equiv_dec (x :>) (y :>)) (no associativity, at level 70) (** Use program to solve some obligations. *) -Definition swap_sumbool `A B` (x : { A } + { B }) : { B } + { A } := +Definition swap_sumbool {A B} (x : { A } + { B }) : { B } + { A } := match x with | left H => @right _ _ H | right H => @left _ _ H @@ -52,7 +52,7 @@ Require Import Coq.Program.Program. (** Invert the branches. *) -Program Definition nequiv_dec [ EqDec A ] (x y : A) : { x =/= y } + { x == y } := swap_sumbool (x == y). +Program Definition nequiv_dec [ ! EqDec A ] (x y : A) : { x =/= y } + { x == y } := swap_sumbool (x == y). (** Overloaded notation for inequality. *) @@ -60,10 +60,10 @@ Infix "=/=" := nequiv_dec (no associativity, at level 70). (** Define boolean versions, losing the logical information. *) -Definition equiv_decb [ EqDec A ] (x y : A) : bool := +Definition equiv_decb [ ! EqDec A ] (x y : A) : bool := if x == y then true else false. -Definition nequiv_decb [ EqDec A ] (x y : A) : bool := +Definition nequiv_decb [ ! EqDec A ] (x y : A) : bool := negb (equiv_decb x y). Infix "==b" := equiv_decb (no associativity, at level 70). @@ -78,15 +78,15 @@ Require Import Coq.Arith.Arith. Program Instance eq_setoid : 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 := left. Next Obligation. @@ -95,8 +95,8 @@ Program Instance unit_eqdec : ? EqDec (@eq_setoid unit) := reflexivity. Qed. -Program Instance [ ? EqDec (@eq_setoid A), ? EqDec (@eq_setoid B) ] => - prod_eqdec : ? EqDec (@eq_setoid (prod A B)) := +Program Instance [ EqDec (@eq_setoid A), EqDec (@eq_setoid B) ] => + prod_eqdec : EqDec (@eq_setoid (prod A B)) := equiv_dec x y := dest x as (x1, x2) in dest y as (y1, y2) in @@ -111,7 +111,7 @@ Program Instance [ ? EqDec (@eq_setoid A), ? EqDec (@eq_setoid B) ] => Require Import Coq.Program.FunctionalExtensionality. -Program Instance [ ? EqDec (@eq_setoid A) ] => bool_function_eqdec : ? EqDec (@eq_setoid (bool -> A)) := +Program Instance [ EqDec (@eq_setoid A) ] => bool_function_eqdec : EqDec (@eq_setoid (bool -> A)) := equiv_dec f g := if f true == g true then if f false == g false then left diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v index 953296c28c..1277dcda9a 100644 --- a/theories/Classes/SetoidTactics.v +++ b/theories/Classes/SetoidTactics.v @@ -32,5 +32,4 @@ Axiom setoideq_eq : forall [ sa : Setoid a ] (x y : a), x == y -> x = y. Ltac setoid_extensionality := match goal with [ |- @eq ?A ?X ?Y ] => apply (setoideq_eq (a:=A) (x:=X) (y:=Y)) - end. - + end.
\ No newline at end of file diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v index 8a3e5dccd9..ddc61a2dc0 100644 --- a/theories/Program/Basics.v +++ b/theories/Program/Basics.v @@ -21,11 +21,11 @@ Require Export Coq.Program.FunctionalExtensionality. Notation " 'λ' x : T , y " := (fun x:T => y) (at level 100, x,T,y at level 10, no associativity) : program_scope. -Open Scope program_scope. +Open Local Scope program_scope. -Definition id `A` := λ x : A, x. +Definition id {A} := λ x : A, x. -Definition compose `A B C` (g : B -> C) (f : A -> B) := λ x : A , g (f x). +Definition compose {A B C} (g : B -> C) (f : A -> B) := λ x : A , g (f x). Hint Unfold compose. @@ -58,11 +58,11 @@ Definition arrow (A B : Type) := A -> B. Definition impl (A B : Prop) : Prop := A -> B. -Notation " f '#' x " := (f x) (at level 100, x at level 200, only parsing). +(* Notation " f x " := (f x) (at level 100, x at level 200, only parsing) : program_scope. *) -Definition const `A B` (a : A) := fun x : B => a. +Definition const {A B} (a : A) := fun x : B => a. -Definition flip `A B C` (f : A -> B -> C) x y := f y x. +Definition flip {A B C} (f : A -> B -> C) x y := f y x. Lemma flip_flip : forall A B C (f : A -> B -> C), flip (flip f) = f. Proof. @@ -72,7 +72,7 @@ Proof. reflexivity. Qed. -Definition apply `A B` (f : A -> B) (x : A) := f x. +Definition apply {A B} (f : A -> B) (x : A) := f x. (** Notations for the unit type and value. *) @@ -94,10 +94,10 @@ Implicit Arguments right [[A] [B]]. (** Curryfication. *) -Definition curry `a b c` (f : a -> b -> c) (p : prod a b) : c := +Definition curry {a b c} (f : a -> b -> c) (p : prod a b) : c := let (x, y) := p in f x y. -Definition uncurry `a b c` (f : prod a b -> c) (x : a) (y : b) : c := +Definition uncurry {a b c} (f : prod a b -> c) (x : a) (y : b) : c := f (x, y). Lemma uncurry_curry : forall a b c (f : a -> b -> c), uncurry (curry f) = f. @@ -116,17 +116,6 @@ Proof. destruct x ; simpl ; reflexivity. Qed. -(** Useful implicits and notations for lists. *) - -Require Import Coq.Lists.List. - -Implicit Arguments nil [[A]]. -Implicit Arguments cons [[A]]. - -Notation " [] " := nil. -Notation " [ x ] " := (cons x nil). -Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..). - (** n-ary exists ! *) Notation " 'exists' x y , p" := (ex (fun x => (ex (fun y => p)))) diff --git a/theories/Program/FunctionalExtensionality.v b/theories/Program/FunctionalExtensionality.v index e890261e12..c2a6f3df6c 100644 --- a/theories/Program/FunctionalExtensionality.v +++ b/theories/Program/FunctionalExtensionality.v @@ -17,6 +17,7 @@ Require Import Coq.Program.Utils. Require Import Coq.Program.Wf. +Require Import Coq.Program.Equality. Set Implicit Arguments. Unset Strict Implicit. |