diff options
Diffstat (limited to 'theories/Classes')
| -rw-r--r-- | theories/Classes/EquivDec.v | 56 | ||||
| -rw-r--r-- | theories/Classes/Equivalence.v | 40 | ||||
| -rw-r--r-- | theories/Classes/Functions.v | 19 | ||||
| -rw-r--r-- | theories/Classes/Init.v | 14 | ||||
| -rw-r--r-- | theories/Classes/Morphisms.v | 140 | ||||
| -rw-r--r-- | theories/Classes/Morphisms_Prop.v | 37 | ||||
| -rw-r--r-- | theories/Classes/Morphisms_Relations.v | 10 | ||||
| -rw-r--r-- | theories/Classes/RelationClasses.v | 116 | ||||
| -rw-r--r-- | theories/Classes/SetoidAxioms.v | 9 | ||||
| -rw-r--r-- | theories/Classes/SetoidClass.v | 66 | ||||
| -rw-r--r-- | theories/Classes/SetoidDec.v | 35 | ||||
| -rw-r--r-- | theories/Classes/SetoidTactics.v | 8 |
12 files changed, 244 insertions, 306 deletions
diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v index 1e58d05d..157217ae 100644 --- a/theories/Classes/EquivDec.v +++ b/theories/Classes/EquivDec.v @@ -1,4 +1,3 @@ -(* -*- coq-prog-args: ("-emacs-U" "-nois") -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -10,13 +9,12 @@ (* Decidable equivalences. * * 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: EquivDec.v 11282 2008-07-28 11:51:53Z msozeau $ *) +(* $Id: EquivDec.v 11800 2009-01-18 18:34:15Z msozeau $ *) -Set Implicit Arguments. -Unset Strict Implicit. +Set Manual Implicit Arguments. (** Export notations. *) @@ -29,12 +27,12 @@ Require Import Coq.Logic.Decidable. Open Scope equiv_scope. -Class [ equiv : Equivalence A ] => DecidableEquivalence := +Class DecidableEquivalence `(equiv : Equivalence A) := setoid_decidable : forall x y : A, decidable (x === y). (** The [EqDec] class gives a decision procedure for a particular setoid equality. *) -Class [ equiv : Equivalence A ] => EqDec := +Class EqDec A R {equiv : Equivalence R} := equiv_dec : forall x y : A, { x === y } + { x =/= y }. (** We define the [==] overloaded notation for deciding equality. It does not take precedence @@ -54,7 +52,7 @@ Open Local Scope program_scope. (** 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. *) @@ -62,10 +60,10 @@ Infix "<>" := nequiv_dec (no associativity, at level 70) : equiv_scope. (** 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). @@ -77,16 +75,13 @@ Require Import Coq.Arith.Peano_dec. (** The equiv is burried inside the setoid, but we can recover it by specifying which setoid we're talking about. *) -Program Instance nat_eq_eqdec : ! EqDec nat eq := - equiv_dec := eq_nat_dec. +Program Instance nat_eq_eqdec : EqDec nat eq := eq_nat_dec. Require Import Coq.Bool.Bool. -Program Instance bool_eqdec : ! EqDec bool eq := - equiv_dec := bool_dec. +Program Instance bool_eqdec : EqDec bool eq := bool_dec. -Program Instance unit_eqdec : ! EqDec unit eq := - equiv_dec x y := in_left. +Program Instance unit_eqdec : EqDec unit eq := λ x y, in_left. Next Obligation. Proof. @@ -94,39 +89,38 @@ Program Instance unit_eqdec : ! EqDec unit eq := reflexivity. Qed. -Program Instance prod_eqdec [ EqDec A eq, EqDec B eq ] : +Program Instance prod_eqdec `(EqDec A eq, EqDec B eq) : ! EqDec (prod A B) eq := - equiv_dec x y := + { equiv_dec x y := let '(x1, x2) := x in let '(y1, y2) := y in if x1 == y1 then if x2 == y2 then in_left else in_right - else in_right. + else in_right }. Solve Obligations using unfold complement, equiv ; program_simpl. -Program Instance sum_eqdec [ EqDec A eq, EqDec B eq ] : - ! 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 | inr a, inr b => if a == b then in_left else in_right | inl _, inr _ | inr _, inl _ => in_right - end. + end }. Solve Obligations using unfold complement, equiv ; program_simpl. -(** Objects of function spaces with countable domains like bool have decidable equality. *) - -Require Import Coq.Program.FunctionalExtensionality. +(** Objects of function spaces with countable domains like bool have decidable equality. + Proving the reflection requires functional extensionality though. *) -Program Instance bool_function_eqdec [ EqDec A eq ] : ! EqDec (bool -> A) eq := - equiv_dec f g := +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 else in_right - else in_right. + else in_right }. Solve Obligations using try red ; unfold equiv, complement ; program_simpl. @@ -138,8 +132,8 @@ Program Instance bool_function_eqdec [ EqDec A eq ] : ! EqDec (bool -> A) eq := Require Import List. -Program Instance list_eqdec [ eqa : EqDec A eq ] : ! EqDec (list A) eq := - equiv_dec := +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 | nil, nil => in_left @@ -148,7 +142,7 @@ Program Instance list_eqdec [ eqa : EqDec A eq ] : ! EqDec (list A) eq := if aux tl tl' then in_left else in_right else in_right | _, _ => in_right - end. + end }. Solve Obligations using unfold equiv, complement in * ; program_simpl ; intuition (discriminate || eauto). diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v index d52eed47..5e5895ab 100644 --- a/theories/Classes/Equivalence.v +++ b/theories/Classes/Equivalence.v @@ -1,4 +1,3 @@ -(* -*- coq-prog-args: ("-emacs-U" "-nois") -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -13,7 +12,7 @@ Institution: LRI, CNRS UMR 8623 - UniversitĂcopyright Paris Sud 91405 Orsay, France *) -(* $Id: Equivalence.v 11282 2008-07-28 11:51:53Z msozeau $ *) +(* $Id: Equivalence.v 11709 2008-12-20 11:42:15Z msozeau $ *) Require Export Coq.Program.Basics. Require Import Coq.Program.Tactics. @@ -28,9 +27,7 @@ Unset Strict Implicit. Open Local Scope signature_scope. -Definition equiv [ Equivalence A R ] : relation A := R. - -Typeclasses unfold equiv. +Definition equiv `{Equivalence A R} : relation A := R. (** Overloaded notations for setoid equivalence and inequivalence. Not to be confused with [eq] and [=]. *) @@ -42,9 +39,7 @@ Open Local Scope equiv_scope. (** Overloading for [PER]. *) -Definition pequiv [ PER A R ] : relation A := R. - -Typeclasses unfold pequiv. +Definition pequiv `{PER A R} : relation A := R. (** Overloaded notation for partial equivalence. *) @@ -52,16 +47,11 @@ Infix "=~=" := pequiv (at level 70, no associativity) : equiv_scope. (** Shortcuts to make proof search easier. *) -Program Instance equiv_reflexive [ sa : Equivalence A ] : Reflexive equiv. - -Program Instance equiv_symmetric [ sa : Equivalence A ] : Symmetric equiv. +Program Instance equiv_reflexive `(sa : Equivalence A) : Reflexive equiv. - Next Obligation. - Proof. - symmetry ; auto. - Qed. +Program Instance equiv_symmetric `(sa : Equivalence A) : Symmetric equiv. -Program Instance equiv_transitive [ sa : Equivalence A ] : Transitive equiv. +Program Instance equiv_transitive `(sa : Equivalence A) : Transitive equiv. Next Obligation. Proof. @@ -113,13 +103,12 @@ Section Respecting. (** Here we build an equivalence instance for functions which relates respectful ones only, we do not export it. *) - Definition respecting [ Equivalence A (R : relation A), Equivalence B (R' : relation B) ] : Type := + Definition respecting `(eqa : Equivalence A (R : relation A), eqb : Equivalence B (R' : relation B)) : Type := { morph : A -> B | respectful R R' morph morph }. - 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)). - + Program Instance respecting_equiv `(eqa : Equivalence A R, eqb : Equivalence B R') : + Equivalence (fun (f g : respecting eqa eqb) => 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. Next Obligation. @@ -131,13 +120,10 @@ End Respecting. (** The default equivalence on function spaces, with higher-priority than [eq]. *) -Program Instance pointwise_equivalence [ eqb : Equivalence B eqB ] : - Equivalence (A -> B) (pointwise_relation eqB) | 9. - - Solve Obligations using simpl_relation ; first [ reflexivity | (symmetry ; auto) ]. +Program Instance pointwise_equivalence {A} `(eqb : Equivalence B eqB) : + Equivalence (pointwise_relation A eqB) | 9. Next Obligation. Proof. - transitivity (y x0) ; auto. + transitivity (y a) ; auto. Qed. - diff --git a/theories/Classes/Functions.v b/theories/Classes/Functions.v index 4c844911..998f8cb7 100644 --- a/theories/Classes/Functions.v +++ b/theories/Classes/Functions.v @@ -1,4 +1,3 @@ -(* -*- coq-prog-args: ("-emacs-U" "-nois") -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -13,7 +12,7 @@ Institution: LRI, CNRS UMR 8623 - UniversitĂcopyright Paris Sud 91405 Orsay, France *) -(* $Id: Functions.v 11282 2008-07-28 11:51:53Z msozeau $ *) +(* $Id: Functions.v 11709 2008-12-20 11:42:15Z msozeau $ *) Require Import Coq.Classes.RelationClasses. Require Import Coq.Classes.Morphisms. @@ -21,22 +20,22 @@ Require Import Coq.Classes.Morphisms. Set Implicit Arguments. Unset Strict Implicit. -Class Injective ((m : Morphism (A -> B) (RA ++> RB) f)) : 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 Surjective `(m : Morphism (A -> B) (RA ++> RB) f) : 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 MonoMorphism (( m : Morphism (A -> B) (eqA ++> eqB) )) := +Class MonoMorphism `(m : Morphism (A -> B) (eqA ++> eqB)) := monic :> Injective m. -Class EpiMorphism ((m : Morphism (A -> B) (eqA ++> eqB))) := +Class EpiMorphism `(m : Morphism (A -> B) (eqA ++> eqB)) := epic :> Surjective m. -Class IsoMorphism ((m : Morphism (A -> B) (eqA ++> eqB))) := - monomorphism :> MonoMorphism m ; epimorphism :> EpiMorphism m. +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 AutoMorphism `(m : Morphism (A -> A) (eqA ++> eqA)) {I : IsoMorphism m}. diff --git a/theories/Classes/Init.v b/theories/Classes/Init.v index e5f951d0..5df7a4ed 100644 --- a/theories/Classes/Init.v +++ b/theories/Classes/Init.v @@ -13,12 +13,18 @@ Institution: LRI, CNRS UMR 8623 - UniversitĂcopyright Paris Sud 91405 Orsay, France *) -(* $Id: Init.v 11282 2008-07-28 11:51:53Z msozeau $ *) +(* $Id: Init.v 11709 2008-12-20 11:42:15Z msozeau $ *) (* Ltac typeclass_instantiation := typeclasses eauto || eauto. *) Tactic Notation "clapply" ident(c) := - eapply @c ; eauto with typeclass_instances. + eapply @c ; typeclasses eauto. + +(** Hints for the proof search: these combinators should be considered rigid. *) + +Require Import Coq.Program.Basics. + +Typeclasses Opaque id const flip compose arrow impl iff. (** The unconvertible typeclass, to test that two objects of the same type are actually different. *) @@ -27,8 +33,8 @@ Class Unconvertible (A : Type) (a b : A). Ltac unconvertible := match goal with - | |- @Unconvertible _ ?x ?y => conv x y ; fail 1 "Convertible" - | |- _ => apply Build_Unconvertible + | |- @Unconvertible _ ?x ?y => unify x y with typeclass_instances ; fail 1 "Convertible" + | |- _ => eapply 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 c2ae026d..86097a56 100644 --- a/theories/Classes/Morphisms.v +++ b/theories/Classes/Morphisms.v @@ -13,16 +13,15 @@ Institution: LRI, CNRS UMR 8623 - UniversitĂcopyright Paris Sud 91405 Orsay, France *) -(* $Id: Morphisms.v 11282 2008-07-28 11:51:53Z msozeau $ *) +(* $Id: Morphisms.v 11709 2008-12-20 11:42:15Z msozeau $ *) + +Set Manual Implicit Arguments. Require Import Coq.Program.Basics. Require Import Coq.Program.Tactics. Require Import Coq.Relations.Relation_Definitions. Require Export Coq.Classes.RelationClasses. -Set Implicit Arguments. -Unset Strict Implicit. - (** * Morphisms. We now turn to the definition of [Morphism] and declare standard instances. @@ -32,13 +31,9 @@ Unset Strict Implicit. The relation [R] will be instantiated by [respectful] and [A] by an arrow type for usual morphisms. *) -Class Morphism A (R : relation A) (m : A) : Prop := +Class Morphism {A} (R : relation A) (m : A) : Prop := respect : R m m. -(** We make the type implicit, it can be infered from the relations. *) - -Implicit Arguments Morphism [A]. - (** Respectful morphisms. *) (** The fully dependent version, not used yet. *) @@ -53,7 +48,7 @@ Definition respectful_hetero (** The non-dependent version is an instance where we forget dependencies. *) -Definition respectful (A B : Type) +Definition respectful {A B : Type} (R : relation A) (R' : relation B) : relation (A -> B) := Eval compute in @respectful_hetero A A (fun _ => B) (fun _ => B) R (fun _ _ => R'). @@ -75,13 +70,20 @@ Arguments Scope respectful [type_scope type_scope signature_scope signature_scop Open Local Scope signature_scope. -(** Pointwise lifting is just respect with leibniz equality on the left. *) +(** Dependent pointwise lifting of a relation on the range. *) + +Definition forall_relation {A : Type} {B : A -> Type} (sig : Î a : A, relation (B a)) : relation (Î x : A, B x) := + λ f g, Î a : A, sig a (f a) (g a). + +Arguments Scope forall_relation [type_scope type_scope signature_scope]. -Definition pointwise_relation {A B : Type} (R : relation B) : relation (A -> B) := - fun f g => forall x : A, R (f x) (g x). +(** Non-dependent pointwise lifting *) + +Definition pointwise_relation (A : Type) {B : Type} (R : relation B) : relation (A -> B) := + Eval compute in forall_relation (B:=λ _, B) (λ _, R). Lemma pointwise_pointwise A B (R : relation B) : - relation_equivalence (pointwise_relation R) (@eq A ==> R). + relation_equivalence (pointwise_relation A 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 @@ -91,24 +93,26 @@ 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'). +Typeclasses Opaque respectful pointwise_relation forall_relation. + +Program Instance respectful_per `(PER A (R : relation A), PER B (R' : relation B)) : + PER (R ==> R'). Next Obligation. Proof with auto. - assert(R x0 x0). + assert(R x0 x0). transitivity y0... symmetry... transitivity (y x0)... Qed. (** Subrelations induce a morphism on the identity. *) -Instance 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_respectful [ subl : subrelation A Râ Râ, subr : subrelation B Sâ Sâ ] : +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. @@ -119,8 +123,8 @@ Proof. simpl_relation. Qed. (** [Morphism] is itself a covariant morphism for [subrelation]. *) -Lemma subrelation_morphism [ mor : Morphism A Râ m, unc : Unconvertible (relation A) Râ Râ, - sub : subrelation A Râ Râ ] : 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. @@ -153,14 +157,14 @@ Proof. firstorder. Qed. Instance iff_inverse_impl_subrelation : subrelation iff (inverse impl). Proof. firstorder. Qed. -Instance pointwise_subrelation [ sub : subrelation A R R' ] : - subrelation (pointwise_relation (A:=B) R) (pointwise_relation R') | 4. +Instance pointwise_subrelation {A} `(sub : subrelation B R R') : + subrelation (pointwise_relation A R) (pointwise_relation A R') | 4. Proof. reduce. unfold pointwise_relation in *. apply sub. apply H. Qed. (** The complement of a relation conserves its morphisms. *) Program Instance complement_morphism - [ mR : Morphism (A -> A -> Prop) (RA ==> RA ==> iff) R ] : + `(mR : Morphism (A -> A -> Prop) (RA ==> RA ==> iff) R) : Morphism (RA ==> RA ==> iff) (complement R). Next Obligation. @@ -173,7 +177,7 @@ Program Instance complement_morphism (** The [inverse] too, actually the [flip] instance is a bit more general. *) Program Instance flip_morphism - [ mor : Morphism (A -> B -> C) (RA ==> RB ==> RC) f ] : + `(mor : Morphism (A -> B -> C) (RA ==> RB ==> RC) f) : Morphism (RB ==> RA ==> RC) (flip f). Next Obligation. @@ -185,7 +189,7 @@ Program Instance flip_morphism contravariant in the first argument, covariant in the second. *) Program Instance trans_contra_co_morphism - [ Transitive A R ] : Morphism (R --> R ++> impl) R. + `(Transitive A R) : Morphism (R --> R ++> impl) R. Next Obligation. Proof with auto. @@ -196,7 +200,7 @@ Program Instance trans_contra_co_morphism (** Morphism declarations for partial applications. *) Program Instance trans_contra_inv_impl_morphism - [ Transitive A R ] : Morphism (R --> inverse impl) (R x) | 3. + `(Transitive A R) : Morphism (R --> inverse impl) (R x) | 3. Next Obligation. Proof with auto. @@ -204,7 +208,7 @@ Program Instance trans_contra_inv_impl_morphism Qed. Program Instance trans_co_impl_morphism - [ Transitive A R ] : Morphism (R ==> impl) (R x) | 3. + `(Transitive A R) : Morphism (R ==> impl) (R x) | 3. Next Obligation. Proof with auto. @@ -212,7 +216,7 @@ Program Instance trans_co_impl_morphism Qed. Program Instance trans_sym_co_inv_impl_morphism - [ PER A R ] : Morphism (R ==> inverse impl) (R x) | 2. + `(PER A R) : Morphism (R ==> inverse impl) (R x) | 2. Next Obligation. Proof with auto. @@ -220,7 +224,7 @@ Program Instance trans_sym_co_inv_impl_morphism Qed. Program Instance trans_sym_contra_impl_morphism - [ PER A R ] : Morphism (R --> impl) (R x) | 2. + `(PER A R) : Morphism (R --> impl) (R x) | 2. Next Obligation. Proof with auto. @@ -228,7 +232,7 @@ Program Instance trans_sym_contra_impl_morphism Qed. Program Instance per_partial_app_morphism - [ PER A R ] : Morphism (R ==> iff) (R x) | 1. + `(PER A R) : Morphism (R ==> iff) (R x) | 1. Next Obligation. Proof with auto. @@ -242,7 +246,7 @@ Program Instance per_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 | 2. + `(Transitive A R) : Morphism (R ==> (@eq A) ==> inverse impl) R | 2. Next Obligation. Proof with auto. @@ -251,7 +255,7 @@ Program Instance trans_co_eq_inv_impl_morphism (** Every Symmetric and Transitive relation gives rise to an equivariant morphism. *) -Program Instance PER_morphism [ PER A R ] : Morphism (R ==> R ==> iff) R | 1. +Program Instance PER_morphism `(PER A R) : Morphism (R ==> R ==> iff) R | 1. Next Obligation. Proof with auto. @@ -261,7 +265,7 @@ Program Instance PER_morphism [ PER A R ] : Morphism (R ==> R ==> iff) R | 1. transitivity y... transitivity y0... symmetry... Qed. -Lemma symmetric_equiv_inverse [ Symmetric A R ] : relation_equivalence R (flip R). +Lemma symmetric_equiv_inverse `(Symmetric A R) : relation_equivalence R (flip R). Proof. firstorder. Qed. Program Instance compose_morphism A B C Râ Râ Râ : @@ -276,7 +280,7 @@ Program Instance compose_morphism A B C Râ Râ Râ : (** Coq functions are morphisms for leibniz equality, applied only if really needed. *) -Instance reflexive_eq_dom_reflexive (A : Type) [ Reflexive B R' ] : +Instance reflexive_eq_dom_reflexive (A : Type) `(Reflexive B R') : Reflexive (@Logic.eq A ==> R'). Proof. simpl_relation. Qed. @@ -307,20 +311,20 @@ Qed. to set different priorities in different hint bases and select a particular hint database for resolution of a type class constraint.*) -Class MorphismProxy A (R : relation A) (m : A) : Prop := +Class MorphismProxy {A} (R : relation A) (m : A) : Prop := respect_proxy : R m m. Instance reflexive_morphism_proxy - [ Reflexive A R ] (x : A) : MorphismProxy R x | 1. + `(Reflexive A R) (x : A) : MorphismProxy R x | 1. Proof. firstorder. Qed. Instance morphism_morphism_proxy - [ Morphism A R x ] : MorphismProxy R x | 2. + `(Morphism A R x) : MorphismProxy R x | 2. Proof. firstorder. 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 ] : +Lemma Reflexive_partial_app_morphism `(Morphism (A -> B) (R ==> R') m, MorphismProxy A R x) : Morphism R' (m x). Proof. simpl_relation. Qed. @@ -399,38 +403,48 @@ Qed. (** Special-purpose class to do normalization of signatures w.r.t. inverse. *) -Class (A : Type) => Normalizes (m : relation A) (m' : relation A) : Prop := +Class Normalizes (A : Type) (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')) . -Proof. firstorder. Qed. +(** Current strategy: add [inverse] everywhere and reduce using [subrelation] + afterwards. *) + +Lemma inverse_atom A R : Normalizes A R (inverse (inverse R)). +Proof. + firstorder. +Qed. -(* If not an inverse on the left, do a double inverse. *) +Lemma inverse_arrow `(NA : Normalizes A R (inverse R'''), NB : Normalizes B R' (inverse R'')) : + Normalizes (A -> B) (R ==> R') (inverse (R''' ==> R'')%signature). +Proof. unfold Normalizes. intros. + rewrite NA, NB. firstorder. +Qed. + +Ltac inverse := + match goal with + | [ |- Normalizes _ (respectful _ _) _ ] => eapply @inverse_arrow + | _ => eapply @inverse_atom + end. + +Hint Extern 1 (Normalizes _ _ _) => inverse : typeclass_instances. + +(** Treating inverse: can't make them direct instances as we + need at least a [flip] present in the goal. *) -Instance not_inverse_respectful_norm : - ! Normalizes (A -> B) (R ==> inverse R') (inverse (inverse R ==> R')) | 4. +Lemma inverse1 `(subrelation A R' R) : subrelation (inverse (inverse R')) R. 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. - assert(r:=normalizes). - setoid_rewrite r. - setoid_rewrite inverse_respectful. - reflexivity. -Qed. +Lemma inverse2 `(subrelation A R R') : subrelation R (inverse (inverse R')). +Proof. firstorder. Qed. -(** Once we have normalized, we will apply this instance to simplify the problem. *) +Hint Extern 1 (subrelation (flip _) _) => eapply @inverse1 : typeclass_instances. +Hint Extern 1 (subrelation _ (flip _)) => eapply @inverse2 : typeclass_instances. -Definition morphism_inverse_morphism [ mor : Morphism A R m ] : Morphism (inverse R) m := mor. +(** Once we have normalized, we will apply this instance to simplify the problem. *) -Ltac morphism_inverse := - match goal with - [ |- @Morphism _ (flip _) _ ] => eapply @morphism_inverse_morphism - end. +Definition morphism_inverse_morphism `(mor : Morphism A R m) : Morphism (inverse R) m := mor. -Hint Extern 2 (@Morphism _ _ _) => morphism_inverse : typeclass_instances. +Hint Extern 2 (@Morphism _ (flip _) _) => eapply @morphism_inverse_morphism : typeclass_instances. (** Bootstrap !!! *) @@ -445,7 +459,7 @@ Proof. apply H0. Qed. -Lemma morphism_releq_morphism [ Normalizes A R R', Morphism _ R' m ] : Morphism R m. +Lemma morphism_releq_morphism `(Normalizes A R R', Morphism _ R' m) : Morphism R m. Proof. intros. @@ -467,7 +481,7 @@ Hint Extern 6 (@Morphism _ _ _) => morphism_normalization : typeclass_instances. (** Every reflexive relation gives rise to a morphism, only for immediately solving goals without variables. *) -Lemma reflexive_morphism [ Reflexive A R ] (x : A) +Lemma reflexive_morphism `{Reflexive A R} (x : A) : Morphism R x. Proof. firstorder. Qed. diff --git a/theories/Classes/Morphisms_Prop.v b/theories/Classes/Morphisms_Prop.v index ec62e12e..3bbd56cf 100644 --- a/theories/Classes/Morphisms_Prop.v +++ b/theories/Classes/Morphisms_Prop.v @@ -1,4 +1,3 @@ -(* -*- coq-prog-args: ("-emacs-U" "-top" "Coq.Classes.Morphisms") -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -32,18 +31,6 @@ Program Instance not_iff_morphism : Program Instance and_impl_morphism : Morphism (impl ==> impl ==> 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_inverse_impl_iff_morphism : *) -(* Morphism (inverse impl ==> iff ==> inverse impl) and. *) - -(* Program Instance and_iff_inverse_impl_morphism : *) -(* Morphism (iff ==> inverse impl ==> inverse impl) and. *) - Program Instance and_iff_morphism : Morphism (iff ==> iff ==> iff) and. @@ -52,18 +39,6 @@ Program Instance and_iff_morphism : Program Instance or_impl_morphism : Morphism (impl ==> impl ==> 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_inverse_impl_iff_morphism : *) -(* Morphism (inverse impl ==> iff ==> inverse impl) or. *) - -(* Program Instance or_iff_inverse_impl_morphism : *) -(* Morphism (iff ==> inverse impl ==> inverse impl) or. *) - Program Instance or_iff_morphism : Morphism (iff ==> iff ==> iff) or. @@ -73,7 +48,7 @@ Program Instance iff_iff_iff_impl_morphism : Morphism (iff ==> iff ==> iff) impl (** Morphisms for quantifiers *) -Program Instance ex_iff_morphism {A : Type} : Morphism (pointwise_relation iff ==> iff) (@ex A). +Program Instance ex_iff_morphism {A : Type} : Morphism (pointwise_relation A iff ==> iff) (@ex A). Next Obligation. Proof. @@ -87,7 +62,7 @@ Program Instance ex_iff_morphism {A : Type} : Morphism (pointwise_relation iff = Qed. Program Instance ex_impl_morphism {A : Type} : - Morphism (pointwise_relation impl ==> impl) (@ex A). + Morphism (pointwise_relation A impl ==> impl) (@ex A). Next Obligation. Proof. @@ -96,7 +71,7 @@ Program Instance ex_impl_morphism {A : Type} : Qed. Program Instance ex_inverse_impl_morphism {A : Type} : - Morphism (pointwise_relation (inverse impl) ==> inverse impl) (@ex A). + Morphism (pointwise_relation A (inverse impl) ==> inverse impl) (@ex A). Next Obligation. Proof. @@ -105,7 +80,7 @@ Program Instance ex_inverse_impl_morphism {A : Type} : Qed. Program Instance all_iff_morphism {A : Type} : - Morphism (pointwise_relation iff ==> iff) (@all A). + Morphism (pointwise_relation A iff ==> iff) (@all A). Next Obligation. Proof. @@ -114,7 +89,7 @@ Program Instance all_iff_morphism {A : Type} : Qed. Program Instance all_impl_morphism {A : Type} : - Morphism (pointwise_relation impl ==> impl) (@all A). + Morphism (pointwise_relation A impl ==> impl) (@all A). Next Obligation. Proof. @@ -123,7 +98,7 @@ Program Instance all_impl_morphism {A : Type} : Qed. Program Instance all_inverse_impl_morphism {A : Type} : - Morphism (pointwise_relation (inverse impl) ==> inverse impl) (@all A). + Morphism (pointwise_relation A (inverse impl) ==> inverse impl) (@all A). Next Obligation. Proof. diff --git a/theories/Classes/Morphisms_Relations.v b/theories/Classes/Morphisms_Relations.v index 1b389667..24b8d636 100644 --- a/theories/Classes/Morphisms_Relations.v +++ b/theories/Classes/Morphisms_Relations.v @@ -1,4 +1,3 @@ -(* -*- coq-prog-args: ("-emacs-U" "-top" "Coq.Classes.Morphisms") -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -42,17 +41,14 @@ Proof. do 2 red. unfold predicate_implication. auto. Qed. (* when [R] and [R'] are in [relation_equivalence]. *) Instance relation_equivalence_pointwise : - Morphism (relation_equivalence ==> pointwise_relation (A:=A) (pointwise_relation (A:=A) iff)) id. + Morphism (relation_equivalence ==> pointwise_relation A (pointwise_relation A iff)) id. 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. + Morphism (subrelation ==> pointwise_relation A (pointwise_relation 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)). + relation_equivalence (pointwise_relation A (inverse R)) (inverse (pointwise_relation A R)). Proof. intros. split; firstorder. Qed. - - - diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index 9a43a1ba..f95894be 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -1,4 +1,3 @@ -(* -*- coq-prog-name: "coqtop.byte"; coq-prog-args: ("-emacs-U" "-top" "Coq.Classes.RelationClasses") -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -14,7 +13,7 @@ Institution: LRI, CNRS UMR 8623 - UniversitĂcopyright Paris Sud 91405 Orsay, France *) -(* $Id: RelationClasses.v 11282 2008-07-28 11:51:53Z msozeau $ *) +(* $Id: RelationClasses.v 11800 2009-01-18 18:34:15Z msozeau $ *) Require Export Coq.Classes.Init. Require Import Coq.Program.Basics. @@ -23,12 +22,13 @@ Require Export Coq.Relations.Relation_Definitions. (** We allow to unfold the [relation] definition while doing morphism search. *) -Typeclasses unfold relation. - Notation inverse R := (flip (R:relation _) : relation _). Definition complement {A} (R : relation A) : relation A := fun x y => R x y -> False. +(** Opaque for proof-search. *) +Typeclasses Opaque complement. + (** These are convertible. *) Lemma complement_inverse : forall A (R : relation A), complement (inverse R) = inverse (complement R). @@ -39,64 +39,65 @@ Proof. reflexivity. Qed. Set Implicit Arguments. Unset Strict Implicit. -Class Reflexive A (R : relation A) := +Class Reflexive {A} (R : relation A) := reflexivity : forall x, R x x. -Class Irreflexive A (R : relation A) := +Class Irreflexive {A} (R : relation A) := irreflexivity :> Reflexive (complement R). -Class Symmetric A (R : relation A) := +Class Symmetric {A} (R : relation A) := symmetry : forall x y, R x y -> R y x. -Class Asymmetric A (R : relation A) := +Class Asymmetric {A} (R : relation A) := asymmetry : forall x y, R x y -> R y x -> False. -Class Transitive A (R : relation A) := +Class Transitive {A} (R : relation A) := transitivity : forall x y z, R x y -> R y z -> R x z. Hint Resolve @irreflexivity : ord. Unset Implicit Arguments. +(** A HintDb for relations. *) + +Ltac solve_relation := + match goal with + | [ |- ?R ?x ?x ] => reflexivity + | [ H : ?R ?x ?y |- ?R ?y ?x ] => symmetry ; exact H + end. + +Hint Extern 4 => solve_relation : relations. + (** We can already dualize all these properties. *) -Program Instance flip_Reflexive [ Reflexive A R ] : Reflexive (flip R) := - reflexivity := reflexivity (R:=R). +Program Instance flip_Reflexive `(Reflexive A R) : Reflexive (flip R) := + reflexivity (R:=R). -Program Instance flip_Irreflexive [ Irreflexive A R ] : Irreflexive (flip R) := - irreflexivity := irreflexivity (R:=R). +Program Instance flip_Irreflexive `(Irreflexive A R) : Irreflexive (flip R) := + irreflexivity (R:=R). -Program Instance flip_Symmetric [ Symmetric A R ] : Symmetric (flip R). +Program Instance flip_Symmetric `(Symmetric A R) : Symmetric (flip R). - Solve Obligations using unfold flip ; program_simpl ; clapply Symmetric. + Solve Obligations using unfold flip ; intros ; tcapp symmetry ; assumption. -Program Instance flip_Asymmetric [ Asymmetric A R ] : Asymmetric (flip R). +Program Instance flip_Asymmetric `(Asymmetric A R) : Asymmetric (flip R). - Solve Obligations using program_simpl ; unfold flip in * ; intros ; clapply asymmetry. + Solve Obligations using program_simpl ; unfold flip in * ; intros ; typeclass_app asymmetry ; eauto. -Program Instance flip_Transitive [ Transitive A R ] : Transitive (flip R). +Program Instance flip_Transitive `(Transitive A R) : Transitive (flip R). - Solve Obligations using unfold flip ; program_simpl ; clapply transitivity. + Solve Obligations using unfold flip ; program_simpl ; typeclass_app transitivity ; eauto. -Program Instance Reflexive_complement_Irreflexive [ Reflexive A (R : relation A) ] +Program Instance Reflexive_complement_Irreflexive `(Reflexive A (R : relation A)) : Irreflexive (complement R). Next Obligation. - Proof. - unfold complement. - red. intros H. - intros H' ; apply H'. - apply reflexivity. - Qed. - + Proof. firstorder. Qed. -Program Instance complement_Symmetric [ Symmetric A (R : relation A) ] : Symmetric (complement R). +Program Instance complement_Symmetric `(Symmetric A (R : relation A)) : Symmetric (complement R). Next Obligation. - Proof. - red ; intros H'. - apply (H (symmetry H')). - Qed. + Proof. firstorder. Qed. (** * Standard instances. *) @@ -147,52 +148,52 @@ Program Instance eq_Transitive : Transitive (@eq A). (** A [PreOrder] is both Reflexive and Transitive. *) -Class PreOrder A (R : relation A) : Prop := +Class PreOrder {A} (R : relation A) : Prop := { PreOrder_Reflexive :> Reflexive R ; - PreOrder_Transitive :> Transitive R. + PreOrder_Transitive :> Transitive R }. (** A partial equivalence relation is Symmetric and Transitive. *) -Class PER (carrier : Type) (pequiv : relation carrier) : Prop := - PER_Symmetric :> Symmetric pequiv ; - PER_Transitive :> Transitive pequiv. +Class PER {A} (R : relation A) : Prop := { + PER_Symmetric :> Symmetric R ; + PER_Transitive :> Transitive R }. (** Equivalence relations. *) -Class Equivalence (carrier : Type) (equiv : relation carrier) : Prop := - Equivalence_Reflexive :> Reflexive equiv ; - Equivalence_Symmetric :> Symmetric equiv ; - Equivalence_Transitive :> Transitive equiv. +Class Equivalence {A} (R : relation A) : Prop := { + Equivalence_Reflexive :> Reflexive R ; + Equivalence_Symmetric :> Symmetric R ; + Equivalence_Transitive :> Transitive R }. (** An Equivalence is a PER plus reflexivity. *) -Instance Equivalence_PER [ Equivalence A R ] : PER A R | 10 := - PER_Symmetric := Equivalence_Symmetric ; - PER_Transitive := Equivalence_Transitive. +Instance Equivalence_PER `(Equivalence A R) : PER 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 Antisymmetric ((equ : Equivalence A eqA)) (R : relation A) := +Class Antisymmetric A eqA `{equ : Equivalence A eqA} (R : relation A) := antisymmetry : forall x y, R x y -> R y x -> eqA x y. -Program Instance flip_antiSymmetric {{Antisymmetric A eqA 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 if only the type is constrained. *) -Program Instance eq_equivalence : Equivalence A (@eq A) | 10. +Program Instance eq_equivalence : Equivalence (@eq A) | 10. (** Logical equivalence [iff] is an equivalence relation. *) -Program Instance iff_equivalence : Equivalence Prop iff. +Program Instance iff_equivalence : Equivalence iff. (** We now develop a generalization of results on relations for arbitrary predicates. The resulting theory can be applied to homogeneous binary relations but also to arbitrary n-ary predicates. *) -Require Import List. +Require Import Coq.Lists.List. (* Notation " [ ] " := nil : list_scope. *) (* Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) (at level 1) : list_scope. *) @@ -273,7 +274,7 @@ Definition predicate_implication {l : list Type} := (** Notations for pointwise equivalence and implication of predicates. *) Infix "<â>" := predicate_equivalence (at level 95, no associativity) : predicate_scope. -Infix "-â>" := predicate_implication (at level 70) : predicate_scope. +Infix "-â>" := predicate_implication (at level 70, right associativity) : predicate_scope. Open Local Scope predicate_scope. @@ -306,7 +307,7 @@ Notation "ââ„â" := false_predicate : predicate_scope. (** Predicate equivalence is an equivalence, and predicate implication defines a preorder. *) Program Instance predicate_equivalence_equivalence : - Equivalence (predicate l) predicate_equivalence. + Equivalence (@predicate_equivalence l). Next Obligation. induction l ; firstorder. @@ -324,7 +325,7 @@ Program Instance predicate_equivalence_equivalence : Qed. Program Instance predicate_implication_preorder : - PreOrder (predicate l) predicate_implication. + PreOrder (@predicate_implication l). Next Obligation. induction l ; firstorder. @@ -356,10 +357,10 @@ Definition relation_disjunction {A} (R : relation A) (R' : relation A) : relatio (** Relation equivalence is an equivalence, and subrelation defines a partial order. *) Instance relation_equivalence_equivalence (A : Type) : - Equivalence (relation A) relation_equivalence. + Equivalence (@relation_equivalence A). Proof. intro A. exact (@predicate_equivalence_equivalence (cons A (cons A nil))). Qed. -Instance relation_implication_preorder : PreOrder (relation A) subrelation. +Instance relation_implication_preorder : PreOrder (@subrelation A). Proof. intro A. exact (@predicate_implication_preorder (cons A (cons A nil))). Qed. (** *** Partial Order. @@ -367,14 +368,14 @@ 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, preo : PreOrder A R ] => PartialOrder := +Class PartialOrder A eqA `{equ : Equivalence A eqA} R `{preo : PreOrder A R} := partial_order_equivalence : relation_equivalence eqA (relation_conjunction R (inverse R)). (** The equivalence proof is sufficient for proving that [R] must be a morphism for equivalence (see Morphisms). It is also sufficient to show that [R] is antisymmetric w.r.t. [eqA] *) -Instance partial_order_antisym [ PartialOrder A eqA R ] : ! Antisymmetric A eqA R. +Instance partial_order_antisym `(PartialOrder A eqA R) : ! Antisymmetric A eqA R. Proof with auto. reduce_goal. pose proof partial_order_equivalence as poe. do 3 red in poe. apply <- poe. firstorder. @@ -389,3 +390,6 @@ Program Instance subrelation_partial_order : Proof. unfold relation_equivalence in *. firstorder. Qed. + +Typeclasses Opaque arrows predicate_implication predicate_equivalence + relation_equivalence pointwise_lifting. diff --git a/theories/Classes/SetoidAxioms.v b/theories/Classes/SetoidAxioms.v index 9264b6d2..305168ec 100644 --- a/theories/Classes/SetoidAxioms.v +++ b/theories/Classes/SetoidAxioms.v @@ -1,4 +1,3 @@ -(* -*- coq-prog-args: ("-emacs-U" "-nois") -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -13,7 +12,7 @@ * Institution: LRI, CNRS UMR 8623 - UniversitĂcopyright Paris Sud * 91405 Orsay, France *) -(* $Id: SetoidAxioms.v 10739 2008-04-01 14:45:20Z herbelin $ *) +(* $Id: SetoidAxioms.v 11709 2008-12-20 11:42:15Z msozeau $ *) Require Import Coq.Program.Program. @@ -22,10 +21,10 @@ Unset Strict Implicit. Require Export Coq.Classes.SetoidClass. -(* Application of the extensionality axiom to turn a goal on leibinz equality to - a setoid equivalence. *) +(* Application of the extensionality axiom to turn a goal on + Leibinz equality to a setoid equivalence (use with care!). *) -Axiom setoideq_eq : forall [ sa : Setoid a ] (x y : a), x == y -> x = y. +Axiom setoideq_eq : forall `{sa : Setoid a} (x y : a), x == y -> x = y. (** Application of the extensionality principle for setoids. *) diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v index 178d5333..47f92ada 100644 --- a/theories/Classes/SetoidClass.v +++ b/theories/Classes/SetoidClass.v @@ -1,4 +1,3 @@ -(* -*- coq-prog-args: ("-emacs-U" "-nois") -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -13,7 +12,7 @@ Institution: LRI, CNRS UMR 8623 - UniversitĂcopyright Paris Sud 91405 Orsay, France *) -(* $Id: SetoidClass.v 11282 2008-07-28 11:51:53Z msozeau $ *) +(* $Id: SetoidClass.v 11800 2009-01-18 18:34:15Z msozeau $ *) Set Implicit Arguments. Unset Strict Implicit. @@ -27,11 +26,9 @@ Require Import Coq.Classes.Functions. (** A setoid wraps an equivalence. *) -Class Setoid A := +Class Setoid A := { equiv : relation A ; - setoid_equiv :> Equivalence A equiv. - -Typeclasses unfold equiv. + setoid_equiv :> Equivalence equiv }. (* Too dangerous instance *) (* Program Instance [ eqa : Equivalence A eqA ] => *) @@ -40,13 +37,13 @@ Typeclasses unfold equiv. (** Shortcuts to make proof search easier. *) -Definition setoid_refl [ sa : Setoid A ] : Reflexive equiv. +Definition setoid_refl `(sa : Setoid A) : Reflexive equiv. Proof. typeclasses eauto. Qed. -Definition setoid_sym [ sa : Setoid A ] : Symmetric equiv. +Definition setoid_sym `(sa : Setoid A) : Symmetric equiv. Proof. typeclasses eauto. Qed. -Definition setoid_trans [ sa : Setoid A ] : Transitive equiv. +Definition setoid_trans `(sa : Setoid A) : Transitive equiv. Proof. typeclasses eauto. Qed. Existing Instance setoid_refl. @@ -58,8 +55,8 @@ Existing Instance setoid_trans. (* Program Instance eq_setoid : Setoid A := *) (* equiv := eq ; setoid_equiv := eq_equivalence. *) -Program Instance iff_setoid : Setoid Prop := - equiv := iff ; setoid_equiv := iff_equivalence. +Program Instance iff_setoid : Setoid Prop := + { equiv := iff ; setoid_equiv := iff_equivalence }. (** Overloaded notations for setoid equivalence and inequivalence. Not to be confused with [eq] and [=]. *) @@ -87,7 +84,7 @@ Ltac clsubst_nofail := Tactic Notation "clsubst" "*" := clsubst_nofail. -Lemma nequiv_equiv_trans : forall [ Setoid A ] (x y z : A), x =/= y -> y == z -> x =/= z. +Lemma nequiv_equiv_trans : forall `{Setoid A} (x y z : A), x =/= y -> y == z -> x =/= z. Proof with auto. intros; intro. assert(z == y) by (symmetry ; auto). @@ -95,7 +92,7 @@ Proof with auto. contradiction. Qed. -Lemma equiv_nequiv_trans : forall [ Setoid A ] (x y z : A), x == y -> y =/= z -> x =/= z. +Lemma equiv_nequiv_trans : forall `{Setoid A} (x y z : A), x == y -> y =/= z -> x =/= z. Proof. intros; intro. assert(y == x) by (symmetry ; auto). @@ -122,23 +119,11 @@ 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 := - PER_morphism. - -(** Add this very useful instance in the database. *) - -Implicit Arguments setoid_morphism [[!sa]]. -Existing Instance setoid_morphism. - -Program Definition setoid_partial_app_morphism [ sa : Setoid A ] (x : A) : Morphism (equiv ++> iff) (equiv x) := - Reflexive_partial_app_morphism. - -Existing Instance setoid_partial_app_morphism. +Program Instance setoid_morphism `(sa : Setoid A) : Morphism (equiv ++> equiv ++> iff) equiv := + respect. -Definition type_eq : relation Type := - fun x y => x = y. - -Program Instance type_equivalence : Equivalence Type type_eq. +Program Instance setoid_partial_app_morphism `(sa : Setoid A) (x : A) : Morphism (equiv ++> iff) (equiv x) := + respect. Ltac morphism_tac := try red ; unfold arrow ; intros ; program_simpl ; try tauto. @@ -148,29 +133,12 @@ Ltac obligation_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) Basics.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. *) +Program Instance iff_impl_id_morphism : Morphism (iff ++> impl) id. (** Partial setoids don't require reflexivity so we can build a partial setoid on the function space. *) -Class PartialSetoid (carrier : Type) := - pequiv : relation carrier ; - pequiv_prf :> PER carrier pequiv. +Class PartialSetoid (A : Type) := + { pequiv : relation A ; pequiv_prf :> PER pequiv }. (** Overloaded notation for partial setoid equivalence. *) diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v index 8a069343..bac64724 100644 --- a/theories/Classes/SetoidDec.v +++ b/theories/Classes/SetoidDec.v @@ -1,4 +1,3 @@ -(* -*- coq-prog-args: ("-emacs-U" "-nois") -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -10,10 +9,10 @@ (* Decidable setoid equality theory. * * 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: SetoidDec.v 11282 2008-07-28 11:51:53Z msozeau $ *) +(* $Id: SetoidDec.v 11800 2009-01-18 18:34:15Z msozeau $ *) Set Implicit Arguments. Unset Strict Implicit. @@ -27,12 +26,12 @@ Require Export Coq.Classes.SetoidClass. Require Import Coq.Logic.Decidable. -Class DecidableSetoid A [ Setoid A ] := +Class DecidableSetoid `(S : Setoid A) := setoid_decidable : forall x y : A, decidable (x == y). (** The [EqDec] class gives a decision procedure for a particular setoid equality. *) -Class (( s : Setoid A )) => EqDec := +Class EqDec `(S : Setoid A) := equiv_dec : forall x y : A, { x == y } + { x =/= y }. (** We define the [==] overloaded notation for deciding equality. It does not take precedence @@ -52,7 +51,7 @@ Open Local Scope program_scope. (** 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 +59,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). @@ -75,19 +74,19 @@ 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 A : Setoid A := - equiv := eq ; setoid_equiv := eq_equivalence. +Program Instance eq_setoid A : Setoid A | 10 := + { equiv := eq ; setoid_equiv := eq_equivalence }. Program Instance nat_eq_eqdec : EqDec (eq_setoid nat) := - equiv_dec := eq_nat_dec. + eq_nat_dec. Require Import Coq.Bool.Bool. Program Instance bool_eqdec : EqDec (eq_setoid bool) := - equiv_dec := bool_dec. + bool_dec. Program Instance unit_eqdec : EqDec (eq_setoid unit) := - equiv_dec x y := in_left. + λ x y, in_left. Next Obligation. Proof. @@ -95,8 +94,8 @@ 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)) := - equiv_dec x y := +Program Instance prod_eqdec `(! EqDec (eq_setoid A), ! EqDec (eq_setoid B)) : EqDec (eq_setoid (prod A B)) := + λ x y, let '(x1, x2) := x in let '(y1, y2) := y in if x1 == y1 then @@ -108,10 +107,8 @@ Program Instance prod_eqdec [ ! EqDec (eq_setoid A), ! EqDec (eq_setoid B) ] : E (** Objects of function spaces with countable domains like bool have decidable equality. *) -Require Import Coq.Program.FunctionalExtensionality. - -Program Instance bool_function_eqdec [ ! EqDec (eq_setoid A) ] : EqDec (eq_setoid (bool -> A)) := - equiv_dec f g := +Program Instance bool_function_eqdec `(! EqDec (eq_setoid A)) : EqDec (eq_setoid (bool -> A)) := + λ f g, if f true == g true then if f false == g false then in_left else in_right diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v index 6398b125..caacc9ec 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 11282 2008-07-28 11:51:53Z msozeau $ *) +(* $Id: SetoidTactics.v 11709 2008-12-20 11:42:15Z msozeau $ *) Require Export Coq.Classes.RelationClasses. Require Export Coq.Classes.Morphisms. @@ -45,11 +45,11 @@ Class DefaultRelation A (R : relation A). (** To search for the default relation, just call [default_relation]. *) -Definition default_relation [ DefaultRelation A R ] := R. +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 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. *) @@ -178,7 +178,7 @@ Ltac reverse_arrows x := end. Ltac default_add_morphism_tactic := - intros ; + unfold flip ; intros ; (try destruct_morphism) ; match goal with | [ |- (?x ==> ?y) _ _ ] => red_subst_eq_morphism (x ==> y) ; reverse_arrows (x ==> y) |