From 30443ddaba7a0cc996216b3d692b97e0b05907fe Mon Sep 17 00:00:00 2001 From: msozeau Date: Sun, 11 May 2008 22:04:26 +0000 Subject: - Cleanup parsing of binders, reducing to a single production for all binders. - Change syntax of type class instances to better match the usual syntax of lemmas/definitions with name first, then arguments ":" instance. Update theories/Classes accordingly. - Correct globalization of tactic references when doing Ltac :=/::=, update documentation. - Remove the not so useful "(x &)" and "{{x}}" syntaxes from Program.Utils, and subset_scope as well. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10919 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Classes/EquivDec.v | 12 +++--- theories/Classes/Equivalence.v | 14 +++---- theories/Classes/Morphisms.v | 76 +++++++++++++++++++------------------- theories/Classes/Morphisms_Prop.v | 12 +++--- theories/Classes/RelationClasses.v | 27 +++++++------- theories/Classes/SetoidDec.v | 5 +-- theories/Classes/SetoidTactics.v | 3 +- 7 files changed, 73 insertions(+), 76 deletions(-) (limited to 'theories/Classes') diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v index 62744b1d1..d96a532c3 100644 --- a/theories/Classes/EquivDec.v +++ b/theories/Classes/EquivDec.v @@ -94,8 +94,8 @@ Program Instance unit_eqdec : ! EqDec unit eq := reflexivity. Qed. -Program Instance [ EqDec A eq, EqDec B eq ] => - prod_eqdec : ! EqDec (prod A B) eq := +Program Instance prod_eqdec [ EqDec A eq, EqDec B eq ] : + ! EqDec (prod A B) eq := equiv_dec x y := let '(x1, x2) := x in let '(y1, y2) := y in @@ -106,8 +106,8 @@ Program Instance [ EqDec A eq, EqDec B eq ] => Solve Obligations using unfold complement, equiv ; program_simpl. -Program Instance [ EqDec A eq, EqDec B eq ] => - sum_eqdec : ! EqDec (sum A B) eq := +Program Instance sum_eqdec [ EqDec A eq, EqDec B eq ] : + ! EqDec (sum A B) eq := equiv_dec x y := match x, y with | inl a, inl b => if a == b then in_left else in_right @@ -121,7 +121,7 @@ Program Instance [ EqDec A eq, EqDec B eq ] => Require Import Coq.Program.FunctionalExtensionality. -Program Instance [ EqDec A eq ] => bool_function_eqdec : ! EqDec (bool -> A) eq := +Program Instance bool_function_eqdec [ EqDec A eq ] : ! EqDec (bool -> A) eq := equiv_dec f g := if f true == g true then if f false == g false then in_left @@ -138,7 +138,7 @@ Program Instance [ EqDec A eq ] => bool_function_eqdec : ! EqDec (bool -> A) eq Require Import List. -Program Instance [ eqa : EqDec A eq ] => list_eqdec : ! EqDec (list A) eq := +Program Instance list_eqdec [ eqa : EqDec A eq ] : ! EqDec (list A) eq := equiv_dec := fix aux (x : list A) y { struct x } := match x, y with diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v index 23af8a744..42961baea 100644 --- a/theories/Classes/Equivalence.v +++ b/theories/Classes/Equivalence.v @@ -52,16 +52,16 @@ Infix "=~=" := pequiv (at level 70, no associativity) : equiv_scope. (** Shortcuts to make proof search easier. *) -Program Instance [ sa : Equivalence A ] => equiv_reflexive : Reflexive equiv. +Program Instance equiv_reflexive [ sa : Equivalence A ] : Reflexive equiv. -Program Instance [ sa : Equivalence A ] => equiv_symmetric : Symmetric equiv. +Program Instance equiv_symmetric [ sa : Equivalence A ] : Symmetric equiv. Next Obligation. Proof. symmetry ; auto. Qed. -Program Instance [ sa : Equivalence A ] => equiv_transitive : Transitive equiv. +Program Instance equiv_transitive [ sa : Equivalence A ] : Transitive equiv. Next Obligation. Proof. @@ -116,8 +116,8 @@ 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 [ Equivalence A R, Equivalence B R' ] => - respecting_equiv : Equivalence respecting + Program Instance respecting_equiv [ Equivalence A R, 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)). Solve Obligations using unfold respecting in * ; simpl_relation ; program_simpl. @@ -134,8 +134,8 @@ End Respecting. (** The default equivalence on function spaces, with higher-priority than [eq]. *) -Program Instance [ Equivalence A eqA ] => - pointwise_equivalence : Equivalence (B -> A) (pointwise_relation eqA) | 9. +Program Instance pointwise_equivalence [ Equivalence A eqA ] : + Equivalence (B -> A) (pointwise_relation eqA) | 9. Next Obligation. Proof. diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v index 5ac6d8ee5..cd38f318c 100644 --- a/theories/Classes/Morphisms.v +++ b/theories/Classes/Morphisms.v @@ -87,12 +87,12 @@ Proof. firstorder. Qed. (** The subrelation property goes through products as usual. *) -Instance [ sub : subrelation A R₁ R₂ ] => - morphisms_subrelation : ! subrelation (B -> A) (R ==> R₁) (R ==> R₂). +Instance morphisms_subrelation [ sub : subrelation A R₁ R₂ ] : + ! subrelation (B -> A) (R ==> R₁) (R ==> R₂). Proof. firstorder. Qed. -Instance [ sub : subrelation A R₂ R₁ ] => - morphisms_subrelation_left : ! subrelation (A -> B) (R₁ ==> R) (R₂ ==> R) | 3. +Instance morphisms_subrelation_left [ sub : subrelation A R₂ R₁ ] : + ! subrelation (A -> B) (R₁ ==> R) (R₂ ==> R) | 3. Proof. firstorder. Qed. (** [Morphism] is itself a covariant morphism for [subrelation]. *) @@ -129,16 +129,15 @@ Proof. firstorder. Qed. Instance iff_inverse_impl_subrelation : subrelation iff (inverse impl). Proof. firstorder. Qed. -Instance [ sub : subrelation A R R' ] => pointwise_subrelation : +Instance pointwise_subrelation [ sub : subrelation A R R' ] : subrelation (pointwise_relation (A:=B) R) (pointwise_relation R') | 4. Proof. reduce. unfold pointwise_relation in *. apply sub. apply H. Qed. (** The complement of a relation conserves its morphisms. *) -Program Instance [ mR : Morphism (A -> A -> Prop) - (RA ==> RA ==> iff) R ] => - complement_morphism : Morphism (RA ==> RA ==> iff) - (complement R). +Program Instance complement_morphism + [ mR : Morphism (A -> A -> Prop) (RA ==> RA ==> iff) R ] : + Morphism (RA ==> RA ==> iff) (complement R). Next Obligation. Proof. @@ -149,8 +148,9 @@ Program Instance [ mR : Morphism (A -> A -> Prop) (** The [inverse] too, actually the [flip] instance is a bit more general. *) -Program Instance [ mor : Morphism (A -> B -> C) (RA ==> RB ==> RC) f ] => - flip_morphism : Morphism (RB ==> RA ==> RC) (flip f). +Program Instance flip_morphism + [ mor : Morphism (A -> B -> C) (RA ==> RB ==> RC) f ] : + Morphism (RB ==> RA ==> RC) (flip f). Next Obligation. Proof. @@ -160,8 +160,8 @@ Program Instance [ mor : Morphism (A -> B -> C) (RA ==> RB ==> RC) f ] => (** Every Transitive relation gives rise to a binary morphism on [impl], contravariant in the first argument, covariant in the second. *) -Program Instance [ Transitive A R ] => - trans_contra_co_morphism : Morphism (R --> R ++> impl) R. +Program Instance trans_contra_co_morphism + [ Transitive A R ] : Morphism (R --> R ++> impl) R. Next Obligation. Proof with auto. @@ -181,40 +181,40 @@ Program Instance [ Transitive A R ] => (** Morphism declarations for partial applications. *) -Program Instance [ Transitive A R ] => - trans_contra_inv_impl_morphism : Morphism (R --> inverse impl) (R x). +Program Instance trans_contra_inv_impl_morphism + [ Transitive A R ] : Morphism (R --> inverse impl) (R x). Next Obligation. Proof with auto. transitivity y... Qed. -Program Instance [ Transitive A R ] => - trans_co_impl_morphism : Morphism (R ==> impl) (R x). +Program Instance trans_co_impl_morphism + [ Transitive A R ] : Morphism (R ==> impl) (R x). Next Obligation. Proof with auto. transitivity x0... Qed. -Program Instance [ Transitive A R, Symmetric A R ] => - trans_sym_co_inv_impl_morphism : Morphism (R ==> inverse impl) (R x). +Program Instance trans_sym_co_inv_impl_morphism + [ Transitive A R, Symmetric A R ] : Morphism (R ==> inverse impl) (R x). Next Obligation. Proof with auto. transitivity y... Qed. -Program Instance [ Transitive A R, Symmetric _ R ] => - trans_sym_contra_impl_morphism : Morphism (R --> impl) (R x). +Program Instance trans_sym_contra_impl_morphism + [ Transitive A R, Symmetric _ R ] : Morphism (R --> impl) (R x). Next Obligation. Proof with auto. transitivity x0... Qed. -Program Instance [ Equivalence A R ] => - equivalence_partial_app_morphism : Morphism (R ==> iff) (R x). +Program Instance equivalence_partial_app_morphism + [ Equivalence A R ] : Morphism (R ==> iff) (R x). Next Obligation. Proof with auto. @@ -227,8 +227,8 @@ Program Instance [ Equivalence A R ] => (** 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 A) ==> inverse impl) R. +Program Instance trans_co_eq_inv_impl_morphism + [ Transitive A R ] : Morphism (R ==> (@eq A) ==> inverse impl) R. Next Obligation. Proof with auto. @@ -245,8 +245,8 @@ Program Instance [ Transitive A R ] => (** Every Symmetric and Transitive relation gives rise to an equivariant morphism. *) -Program Instance [ Transitive A R, Symmetric _ R ] => - trans_sym_morphism : Morphism (R ==> R ==> iff) R. +Program Instance trans_sym_morphism + [ Transitive A R, Symmetric _ R ] : Morphism (R ==> R ==> iff) R. Next Obligation. Proof with auto. @@ -256,8 +256,8 @@ Program Instance [ Transitive A R, Symmetric _ R ] => transitivity y... transitivity y0... Qed. -Program Instance [ Equivalence A R ] => - equiv_morphism : Morphism (R ==> R ==> iff) R. +Program Instance equiv_morphism [ Equivalence A R ] : + Morphism (R ==> R ==> iff) R. Next Obligation. Proof with auto. @@ -288,7 +288,7 @@ Program Instance inverse_iff_impl_id : (* eq_reflexive_morphism : Morphism (@Logic.eq A ==> R) m | 3. *) (* Proof. simpl_relation. Qed. *) -Instance (A : Type) [ Reflexive B R' ] => +Instance reflexive_eq_dom_reflexive (A : Type) [ Reflexive B R' ] : Reflexive (@Logic.eq A ==> R'). Proof. simpl_relation. Qed. @@ -322,12 +322,12 @@ Qed. Class MorphismProxy A (R : relation A) (m : A) : Prop := respect_proxy : R m m. -Instance [ Reflexive A R ] (x : A) => - reflexive_morphism_proxy : MorphismProxy A R x | 1. +Instance reflexive_morphism_proxy + [ Reflexive A R ] (x : A) : MorphismProxy A R x | 1. Proof. firstorder. Qed. -Instance [ Morphism A R x ] => - morphism_morphism_proxy : MorphismProxy A R x | 2. +Instance morphism_morphism_proxy + [ Morphism A R x ] : MorphismProxy A R x | 2. Proof. firstorder. Qed. (* Instance (A : Type) [ Reflexive B R ] => *) @@ -392,8 +392,8 @@ Instance not_inverse_respectful_norm : Normalizes (A -> B) (R ==> inverse R') (inverse (inverse R ==> R')) | 4. Proof. firstorder. Qed. -Instance [ Normalizes B R' (inverse R'') ] => - inverse_respectful_rec_norm : Normalizes (A -> B) (inverse R ==> R') (inverse (R ==> R'')). +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. setoid_rewrite r. @@ -403,8 +403,8 @@ Qed. (** Once we have normalized, we will apply this instance to simplify the problem. *) -Program Instance [ Morphism A R m ] => - morphism_inverse_morphism : Morphism (inverse R) m | 2. +Program Instance morphism_inverse_morphism + [ Morphism A R m ] : Morphism (inverse R) m | 2. (** Bootstrap !!! *) diff --git a/theories/Classes/Morphisms_Prop.v b/theories/Classes/Morphisms_Prop.v index 301fba534..7dc1f95ef 100644 --- a/theories/Classes/Morphisms_Prop.v +++ b/theories/Classes/Morphisms_Prop.v @@ -73,7 +73,7 @@ Program Instance iff_iff_iff_impl_morphism : Morphism (iff ==> iff ==> iff) impl (** Morphisms for quantifiers *) -Program Instance {A : Type} => ex_iff_morphism : Morphism (pointwise_relation iff ==> iff) (@ex A). +Program Instance ex_iff_morphism {A : Type} : Morphism (pointwise_relation iff ==> iff) (@ex A). Next Obligation. Proof. @@ -86,7 +86,7 @@ Program Instance {A : Type} => ex_iff_morphism : Morphism (pointwise_relation if exists x₁. rewrite H. assumption. Qed. -Program Instance {A : Type} => ex_impl_morphism : +Program Instance ex_impl_morphism {A : Type} : Morphism (pointwise_relation impl ==> impl) (@ex A). Next Obligation. @@ -95,7 +95,7 @@ Program Instance {A : Type} => ex_impl_morphism : exists H0. apply H. assumption. Qed. -Program Instance {A : Type} => ex_inverse_impl_morphism : +Program Instance ex_inverse_impl_morphism {A : Type} : Morphism (pointwise_relation (inverse impl) ==> inverse impl) (@ex A). Next Obligation. @@ -104,7 +104,7 @@ Program Instance {A : Type} => ex_inverse_impl_morphism : exists H0. apply H. assumption. Qed. -Program Instance {A : Type} => all_iff_morphism : +Program Instance all_iff_morphism {A : Type} : Morphism (pointwise_relation iff ==> iff) (@all A). Next Obligation. @@ -113,7 +113,7 @@ Program Instance {A : Type} => all_iff_morphism : intuition ; specialize (H x0) ; intuition. Qed. -Program Instance {A : Type} => all_impl_morphism : +Program Instance all_impl_morphism {A : Type} : Morphism (pointwise_relation impl ==> impl) (@all A). Next Obligation. @@ -122,7 +122,7 @@ Program Instance {A : Type} => all_impl_morphism : intuition ; specialize (H x0) ; intuition. Qed. -Program Instance {A : Type} => all_inverse_impl_morphism : +Program Instance all_inverse_impl_morphism {A : Type} : Morphism (pointwise_relation (inverse impl) ==> inverse impl) (@all A). Next Obligation. diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index 015eb7323..25316c278 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -65,26 +65,26 @@ Unset Implicit Arguments. (** We can already dualize all these properties. *) -Program Instance [ Reflexive A R ] => flip_Reflexive : Reflexive (flip R) := +Program Instance flip_Reflexive [ Reflexive A R ] : Reflexive (flip R) := reflexivity := reflexivity (R:=R). -Program Instance [ Irreflexive A R ] => flip_Irreflexive : Irreflexive (flip R) := +Program Instance flip_Irreflexive [ Irreflexive A R ] : Irreflexive (flip R) := irreflexivity := irreflexivity (R:=R). -Program Instance [ Symmetric A R ] => flip_Symmetric : Symmetric (flip R). +Program Instance flip_Symmetric [ Symmetric A R ] : Symmetric (flip R). Solve Obligations using unfold flip ; program_simpl ; clapply Symmetric. -Program Instance [ Asymmetric A R ] => flip_Asymmetric : Asymmetric (flip R). +Program Instance flip_Asymmetric [ Asymmetric A R ] : Asymmetric (flip R). Solve Obligations using program_simpl ; unfold flip in * ; intros ; clapply asymmetry. -Program Instance [ Transitive A R ] => flip_Transitive : Transitive (flip R). +Program Instance flip_Transitive [ Transitive A R ] : Transitive (flip R). Solve Obligations using unfold flip ; program_simpl ; clapply transitivity. -Program Instance [ Reflexive A (R : relation A) ] => - Reflexive_complement_Irreflexive : Irreflexive (complement R). +Program Instance Reflexive_complement_Irreflexive [ Reflexive A (R : relation A) ] + : Irreflexive (complement R). Next Obligation. Proof. @@ -95,7 +95,7 @@ Program Instance [ Reflexive A (R : relation A) ] => Qed. -Program Instance [ Symmetric A (R : relation A) ] => complement_Symmetric : Symmetric (complement R). +Program Instance complement_Symmetric [ Symmetric A (R : relation A) ] : Symmetric (complement R). Next Obligation. Proof. @@ -165,8 +165,7 @@ Class PER (carrier : Type) (pequiv : relation carrier) : Prop := (** We can build a PER on the Coq function space if we have PERs on the domain and codomain. *) -Program Instance [ PER A (R : relation A), PER B (R' : relation B) ] => - arrow_per : PER (A -> B) +Program Instance arrow_per [ PER A (R : relation A), PER B (R' : relation B) ] : PER (A -> B) (fun f g => forall (x y : A), R x y -> R' (f x) (g y)). Next Obligation. @@ -188,8 +187,8 @@ Class Equivalence (carrier : Type) (equiv : relation carrier) : Prop := Class [ Equivalence A eqA ] => Antisymmetric (R : relation A) := antisymmetry : 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 flip_antiSymmetric [ eq : Equivalence A eqA, ! Antisymmetric eq R ] : + Antisymmetric eq (flip R). (** Leibinz equality [eq] is an equivalence relation. The instance has low priority as it is always applicable @@ -368,7 +367,7 @@ Definition relation_disjunction {A} (R : relation A) (R' : relation A) : relatio (** Relation equivalence is an equivalence, and subrelation defines a partial order. *) -Instance (A : Type) => relation_equivalence_equivalence : +Instance relation_equivalence_equivalence (A : Type) : Equivalence (relation A) relation_equivalence. Proof. intro A. exact (@predicate_equivalence_equivalence (cons A (cons A nil))). Qed. @@ -387,7 +386,7 @@ Class [ equ : Equivalence A eqA, PreOrder A R ] => PartialOrder := for equivalence (see Morphisms). It is also sufficient to show that [R] is antisymmetric w.r.t. [eqA] *) -Instance [ PartialOrder A eqA R ] => partial_order_antisym : ! Antisymmetric A eqA R. +Instance partial_order_antisym [ PartialOrder A eqA R ] : ! Antisymmetric A eqA R. Proof with auto. reduce_goal. pose partial_order_equivalence as poe. do 3 red in poe. apply <- poe. firstorder. diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v index 639b15f50..4d6601a6e 100644 --- a/theories/Classes/SetoidDec.v +++ b/theories/Classes/SetoidDec.v @@ -95,8 +95,7 @@ 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 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 @@ -111,7 +110,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 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 8412cc102..aeaa197e8 100644 --- a/theories/Classes/SetoidTactics.v +++ b/theories/Classes/SetoidTactics.v @@ -38,8 +38,7 @@ Definition default_relation [ DefaultRelation A R ] := R. (** Every [Equivalence] gives a default relation, if no other is given (lowest priority). *) -Instance [ Equivalence A R ] => - equivalence_default : DefaultRelation A R | 4. +Instance equivalence_default [ Equivalence A R ] : DefaultRelation A R | 4. (** The setoid_replace tactics in Ltac, defined in terms of default relations and the setoid_rewrite tactic. *) -- cgit v1.2.3