diff options
Diffstat (limited to 'theories/Classes')
| -rw-r--r-- | theories/Classes/EquivDec.v | 80 | ||||
| -rw-r--r-- | theories/Classes/Equivalence.v | 32 | ||||
| -rw-r--r-- | theories/Classes/Functions.v | 41 | ||||
| -rw-r--r-- | theories/Classes/Init.v | 16 | ||||
| -rw-r--r-- | theories/Classes/Morphisms.v | 391 | ||||
| -rw-r--r-- | theories/Classes/Morphisms_Prop.v | 72 | ||||
| -rw-r--r-- | theories/Classes/Morphisms_Relations.v | 28 | ||||
| -rw-r--r-- | theories/Classes/RelationClasses.v | 193 | ||||
| -rw-r--r-- | theories/Classes/RelationPairs.v | 153 | ||||
| -rw-r--r-- | theories/Classes/SetoidAxioms.v | 34 | ||||
| -rw-r--r-- | theories/Classes/SetoidClass.v | 43 | ||||
| -rw-r--r-- | theories/Classes/SetoidDec.v | 43 | ||||
| -rw-r--r-- | theories/Classes/SetoidTactics.v | 108 | ||||
| -rw-r--r-- | theories/Classes/vo.itarget | 11 |
14 files changed, 760 insertions, 485 deletions
diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v index 15cabf81..0a35ef45 100644 --- a/theories/Classes/EquivDec.v +++ b/theories/Classes/EquivDec.v @@ -6,46 +6,51 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* Decidable equivalences. - * - * Author: Matthieu Sozeau - * Institution: LRI, CNRS UMR 8623 - Universit脙copyright Paris Sud - * 91405 Orsay, France *) +(** * Decidable equivalences. -(* $Id: EquivDec.v 12187 2009-06-13 19:36:59Z msozeau $ *) + Author: Matthieu Sozeau + Institution: LRI, CNRS UMR 8623 - University Paris Sud +*) + +(* $Id$ *) (** Export notations. *) Require Export Coq.Classes.Equivalence. -(** The [DecidableSetoid] class asserts decidability of a [Setoid]. It can be useful in proofs to reason more - classically. *) +(** The [DecidableSetoid] class asserts decidability of a [Setoid]. + It can be useful in proofs to reason more classically. *) Require Import Coq.Logic.Decidable. +Require Import Coq.Bool.Bool. +Require Import Coq.Arith.Peano_dec. +Require Import Coq.Program.Program. + +Generalizable Variables A B R. Open Scope equiv_scope. 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. *) +(** The [EqDec] class gives a decision procedure for a particular + setoid equality. *) 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 - of [==] defined in the type scope, hence we can have both at the same time. *) +(** We define the [==] overloaded notation for deciding equality. It does not + take precedence of [==] defined in the type scope, hence we can have both + at the same time. *) Notation " x == y " := (equiv_dec (x :>) (y :>)) (no associativity, at level 70) : equiv_scope. Definition swap_sumbool {A B} (x : { A } + { B }) : { B } + { A } := match x with - | left H => @right _ _ H - | right H => @left _ _ H + | left H => @right _ _ H + | right H => @left _ _ H end. -Require Import Coq.Program.Program. - Open Local Scope program_scope. (** Invert the branches. *) @@ -69,17 +74,14 @@ Infix "<>b" := nequiv_decb (no associativity, at level 70). (** Decidable leibniz equality instances. *) -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. *) +(** 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 := eq_nat_dec. -Require Import Coq.Bool.Bool. - Program Instance bool_eqdec : EqDec bool eq := bool_dec. -Program Instance unit_eqdec : EqDec unit eq := 位 x y, in_left. +Program Instance unit_eqdec : EqDec unit eq := fun x y => in_left. Next Obligation. Proof. @@ -87,41 +89,37 @@ Program Instance unit_eqdec : EqDec unit eq := 位 x y, in_left. reflexivity. Qed. +Obligation Tactic := unfold complement, equiv ; program_simpl. + 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 - if x1 == y1 then + 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 }. - Solve Obligations using unfold complement, equiv ; program_simpl. - Program Instance sum_eqdec `(EqDec A eq, EqDec B eq) : EqDec (sum A B) eq := { - equiv_dec x y := + 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 }. - Solve Obligations using unfold complement, equiv ; program_simpl. - -(** Objects of function spaces with countable domains like bool have decidable equality. - Proving the reflection requires functional extensionality though. *) +(** 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 := + { equiv_dec f g := if f true == g true then if f false == g false then in_left else in_right else in_right }. - Solve Obligations using try red ; unfold equiv, complement ; program_simpl. - Next Obligation. Proof. extensionality x. @@ -131,21 +129,19 @@ 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 := - fix aux (x : list A) y { struct x } := + { equiv_dec := + fix aux (x y : list A) := match x, y with | nil, nil => in_left - | cons hd tl, cons hd' tl' => + | cons hd tl, cons hd' tl' => if hd == hd' then if aux tl tl' then in_left else in_right else in_right | _, _ => in_right end }. - Solve Obligations using unfold equiv, complement in *; program_simpl; - intuition (discriminate || eauto). + Solve Obligations using unfold equiv, complement in * ; program_simpl ; intuition (discriminate || eauto). - Next Obligation. destruct x ; destruct y ; intuition eauto. Defined. + Next Obligation. destruct y ; intuition eauto. Defined. - Solve Obligations using unfold equiv, complement in *; program_simpl; - intuition (discriminate || eauto). + 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 7068bc6b..d0f24347 100644 --- a/theories/Classes/Equivalence.v +++ b/theories/Classes/Equivalence.v @@ -6,13 +6,13 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* Typeclass-based setoids. Definitions on [Equivalence]. - +(** * Typeclass-based setoids. Definitions on [Equivalence]. + Author: Matthieu Sozeau - Institution: LRI, CNRS UMR 8623 - Universit胏opyright Paris Sud - 91405 Orsay, France *) + Institution: LRI, CNRS UMR 8623 - University Paris Sud +*) -(* $Id: Equivalence.v 12187 2009-06-13 19:36:59Z msozeau $ *) +(* $Id$ *) Require Import Coq.Program.Basics. Require Import Coq.Program.Tactics. @@ -25,16 +25,20 @@ Require Import Coq.Classes.Morphisms. Set Implicit Arguments. Unset Strict Implicit. +Generalizable Variables A R eqA B S eqB. +Local Obligation Tactic := simpl_relation. + Open Local Scope signature_scope. Definition equiv `{Equivalence A R} : relation A := R. -(** Overloaded notations for setoid equivalence and inequivalence. Not to be confused with [eq] and [=]. *) +(** Overloaded notations for setoid equivalence and inequivalence. + Not to be confused with [eq] and [=]. *) 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. - + Open Local Scope equiv_scope. (** Overloading for [PER]. *) @@ -60,7 +64,7 @@ Program Instance equiv_transitive `(sa : Equivalence A) : Transitive equiv. (** Use the [substitute] command which substitutes an equivalence in every hypothesis. *) -Ltac setoid_subst H := +Ltac setoid_subst H := match type of H with ?x === ?y => substitute H ; clear H x end. @@ -70,7 +74,7 @@ Ltac setoid_subst_nofail := | [ H : ?x === ?y |- _ ] => setoid_subst H ; setoid_subst_nofail | _ => idtac end. - + (** [subst*] will try its best at substituting every equality in the goal. *) Tactic Notation "subst" "*" := subst_no_fail ; setoid_subst_nofail. @@ -100,19 +104,19 @@ Ltac equivify := repeat equivify_tac. Section Respecting. - (** Here we build an equivalence instance for functions which relates respectful ones only, + (** Here we build an equivalence instance for functions which relates respectful ones only, we do not export it. *) - Definition respecting `(eqa : Equivalence A (R : relation A), eqb : 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 (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. - Proof. + Proof. unfold respecting in *. program_simpl. transitivity (y y0); auto. apply H0. reflexivity. Qed. diff --git a/theories/Classes/Functions.v b/theories/Classes/Functions.v deleted file mode 100644 index 998f8cb7..00000000 --- a/theories/Classes/Functions.v +++ /dev/null @@ -1,41 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(* Functional morphisms. - - Author: Matthieu Sozeau - Institution: LRI, CNRS UMR 8623 - Universit脙copyright Paris Sud - 91405 Orsay, France *) - -(* $Id: Functions.v 11709 2008-12-20 11:42:15Z msozeau $ *) - -Require Import Coq.Classes.RelationClasses. -Require Import Coq.Classes.Morphisms. - -Set Implicit Arguments. -Unset Strict Implicit. - -Class Injective `(m : Morphism (A -> B) (RA ++> RB) f) : Prop := - injective : forall x y : A, RB (f x) (f y) -> RA x y. - -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)) := - Injective m /\ Surjective m. - -Class MonoMorphism `(m : Morphism (A -> B) (eqA ++> eqB)) := - monic :> Injective m. - -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 AutoMorphism `(m : Morphism (A -> A) (eqA ++> eqA)) {I : IsoMorphism m}. diff --git a/theories/Classes/Init.v b/theories/Classes/Init.v index 762cc5c1..f6e51018 100644 --- a/theories/Classes/Init.v +++ b/theories/Classes/Init.v @@ -6,22 +6,26 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* Initialization code for typeclasses, setting up the default tactic +(** * Initialization code for typeclasses, setting up the default tactic for instance search. Author: Matthieu Sozeau - Institution: LRI, CNRS UMR 8623 - Universit脙copyright Paris Sud - 91405 Orsay, France *) + Institution: LRI, CNRS UMR 8623 - University Paris Sud +*) -(* $Id: Init.v 12187 2009-06-13 19:36:59Z msozeau $ *) +(* $Id$ *) (** 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. +Typeclasses Opaque id const flip compose arrow impl iff not all. -(** The unconvertible typeclass, to test that two objects of the same type are +(** Apply using the same opacity information as typeclass proof search. *) + +Ltac class_apply c := autoapply c using typeclass_instances. + +(** The unconvertible typeclass, to test that two objects of the same type are actually different. *) Class Unconvertible (A : Type) (a b : A) := unconvertible : unit. diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v index 2b653e27..370321c0 100644 --- a/theories/Classes/Morphisms.v +++ b/theories/Classes/Morphisms.v @@ -1,3 +1,4 @@ +(* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -6,41 +7,44 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* Typeclass-based morphism definition and standard, minimal instances. - +(** * Typeclass-based morphism definition and standard, minimal instances + Author: Matthieu Sozeau - Institution: LRI, CNRS UMR 8623 - Universit脙copyright Paris Sud - 91405 Orsay, France *) + Institution: LRI, CNRS UMR 8623 - University Paris Sud +*) -(* $Id: Morphisms.v 12189 2009-06-15 05:08:44Z msozeau $ *) +(* $Id$ *) Require Import Coq.Program.Basics. Require Import Coq.Program.Tactics. Require Import Coq.Relations.Relation_Definitions. Require Export Coq.Classes.RelationClasses. +Generalizable All Variables. +Local Obligation Tactic := simpl_relation. + (** * Morphisms. - We now turn to the definition of [Morphism] and declare standard instances. + We now turn to the definition of [Proper] and declare standard instances. These will be used by the [setoid_rewrite] tactic later. *) -(** A morphism on a relation [R] is an object respecting the relation (in its kernel). - The relation [R] will be instantiated by [respectful] and [A] by an arrow type - for usual morphisms. *) +(** A morphism for a relation [R] is a proper element of the relation. + 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 := - respect : R m m. +Class Proper {A} (R : relation A) (m : A) : Prop := + proper_prf : R m m. (** Respectful morphisms. *) (** The fully dependent version, not used yet. *) -Definition respectful_hetero - (A B : Type) - (C : A -> Type) (D : B -> Type) - (R : A -> B -> Prop) - (R' : forall (x : A) (y : B), C x -> D y -> Prop) : - (forall x : A, C x) -> (forall x : B, D x) -> Prop := +Definition respectful_hetero + (A B : Type) + (C : A -> Type) (D : B -> Type) + (R : A -> B -> Prop) + (R' : forall (x : A) (y : B), C x -> D y -> Prop) : + (forall x : A, C x) -> (forall x : B, D x) -> Prop := fun f g => forall x y, R x y -> R' x y (f x) (g y). (** The non-dependent version is an instance where we forget dependencies. *) @@ -53,27 +57,27 @@ Definition respectful {A B : Type} Delimit Scope signature_scope with signature. -Arguments Scope Morphism [type_scope signature_scope]. +Arguments Scope Proper [type_scope signature_scope]. Arguments Scope respectful [type_scope type_scope signature_scope signature_scope]. -Module MorphismNotations. +Module ProperNotations. - Notation " R ++> R' " := (@respectful _ _ (R%signature) (R'%signature)) + Notation " R ++> R' " := (@respectful _ _ (R%signature) (R'%signature)) (right associativity, at level 55) : signature_scope. - + Notation " R ==> R' " := (@respectful _ _ (R%signature) (R'%signature)) (right associativity, at level 55) : signature_scope. - + Notation " R --> R' " := (@respectful _ _ (inverse (R%signature)) (R'%signature)) (right associativity, at level 55) : signature_scope. -End MorphismNotations. +End ProperNotations. -Export MorphismNotations. +Export ProperNotations. Open Local Scope signature_scope. -(** Dependent pointwise lifting of a relation on the range. *) +(** 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). @@ -82,10 +86,10 @@ Arguments Scope forall_relation [type_scope type_scope signature_scope]. (** Non-dependent pointwise lifting *) -Definition pointwise_relation (A : Type) {B : Type} (R : relation B) : relation (A -> B) := +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) : +Lemma pointwise_pointwise A B (R : relation B) : relation_equivalence (pointwise_relation A R) (@eq A ==> R). Proof. intros. split. simpl_relation. firstorder. Qed. @@ -98,8 +102,7 @@ Hint Unfold Transitive : core. Typeclasses Opaque respectful pointwise_relation forall_relation. -Program Instance respectful_per `(PER A (R : relation A), PER B (R' : relation B)) : - PER (R ==> R'). +Program Instance respectful_per `(PER A R, PER B R') : PER (R ==> R'). Next Obligation. Proof with auto. @@ -110,47 +113,46 @@ Program Instance respectful_per `(PER A (R : relation A), PER B (R' : relation B (** Subrelations induce a morphism on the identity. *) -Instance subrelation_id_morphism `(subrelation A R鈧 R鈧) : Morphism (R鈧 ==> R鈧) id. +Instance subrelation_id_proper `(subrelation A R鈧 R鈧) : Proper (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鈧) : +Lemma 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. (** And of course it is reflexive. *) -Instance morphisms_subrelation_refl : ! subrelation A R R. +Lemma subrelation_refl A R : @subrelation A R R. Proof. simpl_relation. Qed. -(** [Morphism] is itself a covariant morphism for [subrelation]. *) +Ltac subrelation_tac T U := + (is_ground T ; is_ground U ; class_apply @subrelation_refl) || + class_apply @subrelation_respectful || class_apply @subrelation_refl. + +Hint Extern 3 (@subrelation _ ?T ?U) => subrelation_tac T U : typeclass_instances. -Lemma subrelation_morphism `(mor : Morphism A R鈧 m, unc : Unconvertible (relation A) R鈧 R鈧, - sub : subrelation A R鈧 R鈧) : Morphism R鈧 m. +(** [Proper] is itself a covariant morphism for [subrelation]. *) + +Lemma subrelation_proper `(mor : Proper A R鈧 m, unc : Unconvertible (relation A) R鈧 R鈧, + sub : subrelation A R鈧 R鈧) : Proper R鈧 m. Proof. intros. apply sub. apply mor. Qed. -Instance morphism_subrelation_morphism : - Morphism (subrelation ++> @eq _ ==> impl) (@Morphism A). -Proof. reduce. subst. firstorder. Qed. - -(** We use an external tactic to manage the application of subrelation, which is otherwise - always applicable. We allow its use only once per branch. *) - -Inductive subrelation_done : Prop := did_subrelation : subrelation_done. +CoInductive apply_subrelation : Prop := do_subrelation. -Inductive normalization_done : Prop := did_normalization. - -Ltac subrelation_tac := +Ltac proper_subrelation := match goal with - | [ _ : subrelation_done |- _ ] => fail 1 - | [ |- @Morphism _ _ _ ] => let H := fresh "H" in - set(H:=did_subrelation) ; eapply @subrelation_morphism + [ H : apply_subrelation |- _ ] => clear H ; class_apply @subrelation_proper end. -Hint Extern 5 (@Morphism _ _ _) => subrelation_tac : typeclass_instances. +Hint Extern 5 (@Proper _ ?H _) => proper_subrelation : typeclass_instances. + +Instance proper_subrelation_proper : + Proper (subrelation ++> eq ==> impl) (@Proper A). +Proof. reduce. subst. firstorder. Qed. (** Essential subrelation instances for [iff], [impl] and [pointwise_relation]. *) @@ -164,11 +166,29 @@ 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. *) +(** For dependent function types. *) +Lemma forall_subrelation A (B : A -> Type) (R S : forall x : A, relation (B x)) : + (forall a, subrelation (R a) (S a)) -> subrelation (forall_relation R) (forall_relation S). +Proof. reduce. apply H. apply H0. Qed. + +(** We use an extern hint to help unification. *) + +Hint Extern 4 (subrelation (@forall_relation ?A ?B ?R) (@forall_relation _ _ ?S)) => + apply (@forall_subrelation A B R S) ; intro : typeclass_instances. + +(** Any symmetric relation is equal to its inverse. *) + +Lemma subrelation_symmetric A R `(Symmetric A R) : subrelation (inverse R) R. +Proof. reduce. red in H0. symmetry. assumption. Qed. + +Hint Extern 4 (subrelation (inverse _) _) => + class_apply @subrelation_symmetric : typeclass_instances. -Program Instance complement_morphism - `(mR : Morphism (A -> A -> Prop) (RA ==> RA ==> iff) R) : - Morphism (RA ==> RA ==> iff) (complement R). +(** The complement of a relation conserves its proper elements. *) + +Program Instance complement_proper + `(mR : Proper (A -> A -> Prop) (RA ==> RA ==> iff) R) : + Proper (RA ==> RA ==> iff) (complement R). Next Obligation. Proof. @@ -177,22 +197,22 @@ Program Instance complement_morphism intuition. Qed. -(** The [inverse] too, actually the [flip] instance is a bit more general. *) +(** 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) : - Morphism (RB ==> RA ==> RC) (flip f). +Program Instance flip_proper + `(mor : Proper (A -> B -> C) (RA ==> RB ==> RC) f) : + Proper (RB ==> RA ==> RC) (flip f). Next Obligation. Proof. apply mor ; auto. Qed. -(** Every Transitive relation gives rise to a binary morphism on [impl], +(** Every Transitive relation gives rise to a binary morphism on [impl], 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) : Proper (R --> R ++> impl) R. Next Obligation. Proof with auto. @@ -200,10 +220,10 @@ Program Instance trans_contra_co_morphism transitivity x0... Qed. -(** Morphism declarations for partial applications. *) +(** Proper declarations for partial applications. *) Program Instance trans_contra_inv_impl_morphism - `(Transitive A R) : Morphism (R --> inverse impl) (R x) | 3. + `(Transitive A R) : Proper (R --> inverse impl) (R x) | 3. Next Obligation. Proof with auto. @@ -211,7 +231,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) : Proper (R ++> impl) (R x) | 3. Next Obligation. Proof with auto. @@ -219,7 +239,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) : Proper (R ++> inverse impl) (R x) | 3. Next Obligation. Proof with auto. @@ -227,7 +247,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) : Proper (R --> impl) (R x) | 3. Next Obligation. Proof with auto. @@ -235,7 +255,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) : Proper (R ==> iff) (R x) | 2. Next Obligation. Proof with auto. @@ -249,7 +269,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) : Proper (R ==> (@eq A) ==> inverse impl) R | 2. Next Obligation. Proof with auto. @@ -258,21 +278,21 @@ 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) : Proper (R ==> R ==> iff) R | 1. Next Obligation. Proof with auto. split ; intros. transitivity x0... transitivity x... symmetry... - + transitivity y... transitivity y0... symmetry... Qed. 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鈧 : - Morphism ((R鈧 ==> R鈧) ==> (R鈧 ==> R鈧) ==> (R鈧 ==> R鈧)) (@compose A B C). + +Program Instance compose_proper A B C R鈧 R鈧 R鈧 : + Proper ((R鈧 ==> R鈧) ==> (R鈧 ==> R鈧) ==> (R鈧 ==> R鈧)) (@compose A B C). Next Obligation. Proof. @@ -280,7 +300,7 @@ Program Instance compose_morphism A B C R鈧 R鈧 R鈧 : unfold compose. apply H. apply H0. apply H1. Qed. -(** Coq functions are morphisms for leibniz equality, +(** Coq functions are morphisms for Leibniz equality, applied only if really needed. *) Instance reflexive_eq_dom_reflexive (A : Type) `(Reflexive B R') : @@ -289,13 +309,13 @@ Proof. simpl_relation. Qed. (** [respectful] is a morphism for relation equivalence. *) -Instance respectful_morphism : - Morphism (relation_equivalence ++> relation_equivalence ++> relation_equivalence) (@respectful A B). +Instance respectful_morphism : + Proper (relation_equivalence ++> relation_equivalence ++> relation_equivalence) (@respectful A B). Proof. reduce. unfold respectful, relation_equivalence, predicate_equivalence in * ; simpl in *. split ; intros. - + rewrite <- H0. apply H1. rewrite H. @@ -309,43 +329,50 @@ Qed. (** Every element in the carrier of a reflexive relation is a morphism for this relation. We use a proxy class for this case which is used internally to discharge reflexivity constraints. - The [Reflexive] instance will almost always be used, but it won't apply in general to any kind of - [Morphism (A -> B) _ _] goal, making proof-search much slower. A cleaner solution would be to be able + The [Reflexive] instance will almost always be used, but it won't apply in general to any kind of + [Proper (A -> B) _ _] goal, making proof-search much slower. A cleaner solution would be to be able to set different priorities in different hint bases and select a particular hint database for - resolution of a type class constraint.*) + resolution of a type class constraint.*) -Class MorphismProxy {A} (R : relation A) (m : A) : Prop := - respect_proxy : R m m. +Class ProperProxy {A} (R : relation A) (m : A) : Prop := + proper_proxy : R m m. -Instance reflexive_morphism_proxy - `(Reflexive A R) (x : A) : MorphismProxy R x | 1. +Lemma eq_proper_proxy A (x : A) : ProperProxy (@eq A) x. Proof. firstorder. Qed. -Instance morphism_morphism_proxy - `(Morphism A R x) : MorphismProxy R x | 2. +Lemma reflexive_proper_proxy `(Reflexive A R) (x : A) : ProperProxy R x. Proof. firstorder. Qed. +Lemma proper_proper_proxy `(Proper A R x) : ProperProxy R x. +Proof. firstorder. Qed. + +Hint Extern 1 (ProperProxy _ _) => + class_apply @eq_proper_proxy || class_apply @reflexive_proper_proxy : typeclass_instances. +Hint Extern 2 (ProperProxy ?R _) => not_evar R; class_apply @proper_proper_proxy : typeclass_instances. + (** [R] is Reflexive, hence we can build the needed proof. *) -Lemma Reflexive_partial_app_morphism `(Morphism (A -> B) (R ==> R') m, MorphismProxy A R x) : - Morphism R' (m x). +Lemma Reflexive_partial_app_morphism `(Proper (A -> B) (R ==> R') m, ProperProxy A R x) : + Proper R' (m x). Proof. simpl_relation. Qed. Class Params {A : Type} (of : A) (arity : nat). Class PartialApplication. -Ltac partial_application_tactic := +CoInductive normalization_done : Prop := did_normalization. + +Ltac partial_application_tactic := let rec do_partial_apps H m := match m with - | ?m' ?x => eapply @Reflexive_partial_app_morphism ; [do_partial_apps H m'|clear H] + | ?m' ?x => class_apply @Reflexive_partial_app_morphism ; [do_partial_apps H m'|clear H] | _ => idtac end in let rec do_partial H ar m := match ar with | 0 => do_partial_apps H m - | S ?n' => + | S ?n' => match m with ?m' ?x => do_partial H n' m' end @@ -357,25 +384,24 @@ Ltac partial_application_tactic := let v := eval compute in n in clear n ; let H := fresh in assert(H:Params m' v) by typeclasses eauto ; - let v' := eval compute in v in + let v' := eval compute in v in subst m'; do_partial H v' m in match goal with - | [ _ : subrelation_done |- _ ] => fail 1 | [ _ : normalization_done |- _ ] => fail 1 | [ _ : @Params _ _ _ |- _ ] => fail 1 - | [ |- @Morphism ?T _ (?m ?x) ] => - match goal with - | [ _ : PartialApplication |- _ ] => - eapply @Reflexive_partial_app_morphism - | _ => - on_morphism (m x) || - (eapply @Reflexive_partial_app_morphism ; + | [ |- @Proper ?T _ (?m ?x) ] => + match goal with + | [ _ : PartialApplication |- _ ] => + class_apply @Reflexive_partial_app_morphism + | _ => + on_morphism (m x) || + (class_apply @Reflexive_partial_app_morphism ; [ pose Build_PartialApplication | idtac ]) end end. -Hint Extern 4 (@Morphism _ _ _) => partial_application_tactic : typeclass_instances. +Hint Extern 4 (@Proper _ _ _) => partial_application_tactic : typeclass_instances. Lemma inverse_respectful : forall (A : Type) (R : relation A) (B : Type) (R' : relation B), relation_equivalence (inverse (R ==> R')) (inverse R ==> inverse R'). @@ -387,7 +413,7 @@ Qed. (** Special-purpose class to do normalization of signatures w.r.t. inverse. *) -Class Normalizes (A : Type) (m : relation A) (m' : relation A) : Prop := +Class Normalizes (A : Type) (m : relation A) (m' : relation A) : Prop := normalizes : relation_equivalence m m'. (** Current strategy: add [inverse] everywhere and reduce using [subrelation] @@ -400,19 +426,19 @@ Qed. 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. +Proof. unfold Normalizes in *. intros. rewrite NA, NB. firstorder. Qed. -Ltac inverse := +Ltac inverse := match goal with - | [ |- Normalizes _ (respectful _ _) _ ] => eapply @inverse_arrow - | _ => eapply @inverse_atom + | [ |- Normalizes _ (respectful _ _) _ ] => class_apply @inverse_arrow + | _ => class_apply @inverse_atom end. Hint Extern 1 (Normalizes _ _ _) => inverse : typeclass_instances. -(** Treating inverse: can't make them direct instances as we +(** Treating inverse: can't make them direct instances as we need at least a [flip] present in the goal. *) Lemma inverse1 `(subrelation A R' R) : subrelation (inverse (inverse R')) R. @@ -421,18 +447,25 @@ Proof. firstorder. Qed. Lemma inverse2 `(subrelation A R R') : subrelation R (inverse (inverse R')). Proof. firstorder. Qed. -Hint Extern 1 (subrelation (flip _) _) => eapply @inverse1 : typeclass_instances. -Hint Extern 1 (subrelation _ (flip _)) => eapply @inverse2 : typeclass_instances. +Hint Extern 1 (subrelation (flip _) _) => class_apply @inverse1 : typeclass_instances. +Hint Extern 1 (subrelation _ (flip _)) => class_apply @inverse2 : typeclass_instances. + +(** That's if and only if *) + +Lemma eq_subrelation `(Reflexive A R) : subrelation (@eq A) R. +Proof. simpl_relation. Qed. + +(* Hint Extern 3 (subrelation eq ?R) => not_evar R ; class_apply eq_subrelation : typeclass_instances. *) (** Once we have normalized, we will apply this instance to simplify the problem. *) -Definition morphism_inverse_morphism `(mor : Morphism A R m) : Morphism (inverse R) m := mor. +Definition proper_inverse_proper `(mor : Proper A R m) : Proper (inverse R) m := mor. -Hint Extern 2 (@Morphism _ (flip _) _) => eapply @morphism_inverse_morphism : typeclass_instances. +Hint Extern 2 (@Proper _ (flip _) _) => class_apply @proper_inverse_proper : typeclass_instances. (** Bootstrap !!! *) -Instance morphism_morphism : Morphism (relation_equivalence ==> @eq _ ==> iff) (@Morphism A). +Instance proper_proper : Proper (relation_equivalence ==> eq ==> iff) (@Proper A). Proof. simpl_relation. reduce in H. @@ -443,37 +476,139 @@ Proof. apply H0. Qed. -Lemma morphism_releq_morphism `(Normalizes A R R', Morphism _ R' m) : Morphism R m. +Lemma proper_normalizes_proper `(Normalizes A R0 R1, Proper A R1 m) : Proper R0 m. Proof. - intros. - - pose respect as r. - pose normalizes as norm. - setoid_rewrite norm. + red in H, H0. + setoid_rewrite H. assumption. Qed. -Ltac morphism_normalization := +Ltac proper_normalization := match goal with - | [ _ : subrelation_done |- _ ] => fail 1 | [ _ : normalization_done |- _ ] => fail 1 - | [ |- @Morphism _ _ _ ] => let H := fresh "H" in - set(H:=did_normalization) ; eapply @morphism_releq_morphism + | [ _ : apply_subrelation |- @Proper _ ?R _ ] => let H := fresh "H" in + set(H:=did_normalization) ; class_apply @proper_normalizes_proper end. -Hint Extern 6 (@Morphism _ _ _) => morphism_normalization : typeclass_instances. +Hint Extern 6 (@Proper _ _ _) => proper_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) - : Morphism R x. +Lemma reflexive_proper `{Reflexive A R} (x : A) + : Proper R x. Proof. firstorder. Qed. -Ltac morphism_reflexive := +Lemma proper_eq A (x : A) : Proper (@eq A) x. +Proof. intros. apply reflexive_proper. Qed. + +Ltac proper_reflexive := match goal with | [ _ : normalization_done |- _ ] => fail 1 - | [ _ : subrelation_done |- _ ] => fail 1 - | [ |- @Morphism _ _ _ ] => eapply @reflexive_morphism + | _ => class_apply proper_eq || class_apply @reflexive_proper end. -Hint Extern 7 (@Morphism _ _ _) => morphism_reflexive : typeclass_instances. +Hint Extern 7 (@Proper _ _ _) => proper_reflexive : typeclass_instances. + + +(** When the relation on the domain is symmetric, we can + inverse the relation on the codomain. Same for binary functions. *) + +Lemma proper_sym_flip : + forall `(Symmetric A R1)`(Proper (A->B) (R1==>R2) f), + Proper (R1==>inverse R2) f. +Proof. +intros A R1 Sym B R2 f Hf. +intros x x' Hxx'. apply Hf, Sym, Hxx'. +Qed. + +Lemma proper_sym_flip_2 : + forall `(Symmetric A R1)`(Symmetric B R2)`(Proper (A->B->C) (R1==>R2==>R3) f), + Proper (R1==>R2==>inverse R3) f. +Proof. +intros A R1 Sym1 B R2 Sym2 C R3 f Hf. +intros x x' Hxx' y y' Hyy'. apply Hf; auto. +Qed. + +(** When the relation on the domain is symmetric, a predicate is + compatible with [iff] as soon as it is compatible with [impl]. + Same with a binary relation. *) + +Lemma proper_sym_impl_iff : forall `(Symmetric A R)`(Proper _ (R==>impl) f), + Proper (R==>iff) f. +Proof. +intros A R Sym f Hf x x' Hxx'. repeat red in Hf. split; eauto. +Qed. + +Lemma proper_sym_impl_iff_2 : + forall `(Symmetric A R)`(Symmetric B R')`(Proper _ (R==>R'==>impl) f), + Proper (R==>R'==>iff) f. +Proof. +intros A R Sym B R' Sym' f Hf x x' Hxx' y y' Hyy'. +repeat red in Hf. split; eauto. +Qed. + +(** A [PartialOrder] is compatible with its underlying equivalence. *) + +Instance PartialOrder_proper `(PartialOrder A eqA R) : + Proper (eqA==>eqA==>iff) R. +Proof. +intros. +apply proper_sym_impl_iff_2; auto with *. +intros x x' Hx y y' Hy Hr. +transitivity x. +generalize (partial_order_equivalence x x'); compute; intuition. +transitivity y; auto. +generalize (partial_order_equivalence y y'); compute; intuition. +Qed. + +(** From a [PartialOrder] to the corresponding [StrictOrder]: + [lt = le /\ ~eq]. + If the order is total, we could also say [gt = ~le]. *) + +Lemma PartialOrder_StrictOrder `(PartialOrder A eqA R) : + StrictOrder (relation_conjunction R (complement eqA)). +Proof. +split; compute. +intros x (_,Hx). apply Hx, Equivalence_Reflexive. +intros x y z (Hxy,Hxy') (Hyz,Hyz'). split. +apply PreOrder_Transitive with y; assumption. +intro Hxz. +apply Hxy'. +apply partial_order_antisym; auto. +rewrite Hxz; auto. +Qed. + +Hint Extern 4 (StrictOrder (relation_conjunction _ _)) => + class_apply PartialOrder_StrictOrder : typeclass_instances. + +(** From a [StrictOrder] to the corresponding [PartialOrder]: + [le = lt \/ eq]. + If the order is total, we could also say [ge = ~lt]. *) + +Lemma StrictOrder_PreOrder + `(Equivalence A eqA, StrictOrder A R, Proper _ (eqA==>eqA==>iff) R) : + PreOrder (relation_disjunction R eqA). +Proof. +split. +intros x. right. reflexivity. +intros x y z [Hxy|Hxy] [Hyz|Hyz]. +left. transitivity y; auto. +left. rewrite <- Hyz; auto. +left. rewrite Hxy; auto. +right. transitivity y; auto. +Qed. + +Hint Extern 4 (PreOrder (relation_disjunction _ _)) => + class_apply StrictOrder_PreOrder : typeclass_instances. + +Lemma StrictOrder_PartialOrder + `(Equivalence A eqA, StrictOrder A R, Proper _ (eqA==>eqA==>iff) R) : + PartialOrder eqA (relation_disjunction R eqA). +Proof. +intros. intros x y. compute. intuition. +elim (StrictOrder_Irreflexive x). +transitivity y; auto. +Qed. + +Hint Extern 4 (PartialOrder _ (relation_disjunction _ _)) => + class_apply StrictOrder_PartialOrder : typeclass_instances. diff --git a/theories/Classes/Morphisms_Prop.v b/theories/Classes/Morphisms_Prop.v index 3bbd56cf..2dc033d2 100644 --- a/theories/Classes/Morphisms_Prop.v +++ b/theories/Classes/Morphisms_Prop.v @@ -6,81 +6,83 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* Morphism instances for propositional connectives. - +(** * [Proper] instances for propositional connectives. + Author: Matthieu Sozeau - Institution: LRI, CNRS UMR 8623 - Universit脙copyright Paris Sud - 91405 Orsay, France *) + Institution: LRI, CNRS UMR 8623 - University Paris Sud +*) Require Import Coq.Classes.Morphisms. Require Import Coq.Program.Basics. Require Import Coq.Program.Tactics. +Local Obligation Tactic := simpl_relation. + (** Standard instances for [not], [iff] and [impl]. *) (** Logical negation. *) Program Instance not_impl_morphism : - Morphism (impl --> impl) not. + Proper (impl --> impl) not | 1. -Program Instance not_iff_morphism : - Morphism (iff ++> iff) not. +Program Instance not_iff_morphism : + Proper (iff ++> iff) not. (** Logical conjunction. *) Program Instance and_impl_morphism : - Morphism (impl ==> impl ==> impl) and. + Proper (impl ==> impl ==> impl) and | 1. -Program Instance and_iff_morphism : - Morphism (iff ==> iff ==> iff) and. +Program Instance and_iff_morphism : + Proper (iff ==> iff ==> iff) and. (** Logical disjunction. *) -Program Instance or_impl_morphism : - Morphism (impl ==> impl ==> impl) or. +Program Instance or_impl_morphism : + Proper (impl ==> impl ==> impl) or | 1. -Program Instance or_iff_morphism : - Morphism (iff ==> iff ==> iff) or. +Program Instance or_iff_morphism : + Proper (iff ==> iff ==> iff) or. (** 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 : Proper (iff ==> iff ==> iff) impl. (** Morphisms for quantifiers *) -Program Instance ex_iff_morphism {A : Type} : Morphism (pointwise_relation A iff ==> iff) (@ex A). +Program Instance ex_iff_morphism {A : Type} : Proper (pointwise_relation A iff ==> iff) (@ex A). Next Obligation. Proof. - unfold pointwise_relation in H. + unfold pointwise_relation in H. split ; intros. - destruct H0 as [x鈧 H鈧乚. - exists x鈧. rewrite H in H鈧. assumption. - - destruct H0 as [x鈧 H鈧乚. - exists x鈧. rewrite H. assumption. + destruct H0 as [x1 H1]. + exists x1. rewrite H in H1. assumption. + + destruct H0 as [x1 H1]. + exists x1. rewrite H. assumption. Qed. Program Instance ex_impl_morphism {A : Type} : - Morphism (pointwise_relation A impl ==> impl) (@ex A). + Proper (pointwise_relation A impl ==> impl) (@ex A) | 1. Next Obligation. Proof. - unfold pointwise_relation in H. + unfold pointwise_relation in H. exists H0. apply H. assumption. Qed. -Program Instance ex_inverse_impl_morphism {A : Type} : - Morphism (pointwise_relation A (inverse impl) ==> inverse impl) (@ex A). +Program Instance ex_inverse_impl_morphism {A : Type} : + Proper (pointwise_relation A (inverse impl) ==> inverse impl) (@ex A) | 1. Next Obligation. Proof. - unfold pointwise_relation in H. + unfold pointwise_relation in H. exists H0. apply H. assumption. Qed. -Program Instance all_iff_morphism {A : Type} : - Morphism (pointwise_relation A iff ==> iff) (@all A). +Program Instance all_iff_morphism {A : Type} : + Proper (pointwise_relation A iff ==> iff) (@all A). Next Obligation. Proof. @@ -88,18 +90,18 @@ Program Instance all_iff_morphism {A : Type} : intuition ; specialize (H x0) ; intuition. Qed. -Program Instance all_impl_morphism {A : Type} : - Morphism (pointwise_relation A impl ==> impl) (@all A). - +Program Instance all_impl_morphism {A : Type} : + Proper (pointwise_relation A impl ==> impl) (@all A) | 1. + Next Obligation. Proof. unfold pointwise_relation, all in *. intuition ; specialize (H x0) ; intuition. Qed. -Program Instance all_inverse_impl_morphism {A : Type} : - Morphism (pointwise_relation A (inverse impl) ==> inverse impl) (@all A). - +Program Instance all_inverse_impl_morphism {A : Type} : + Proper (pointwise_relation A (inverse impl) ==> inverse impl) (@all A) | 1. + Next Obligation. Proof. unfold pointwise_relation, all in *. diff --git a/theories/Classes/Morphisms_Relations.v b/theories/Classes/Morphisms_Relations.v index 4654e654..d8365abc 100644 --- a/theories/Classes/Morphisms_Relations.v +++ b/theories/Classes/Morphisms_Relations.v @@ -6,23 +6,25 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* Morphism instances for relations. - +(** * Morphism instances for relations. + Author: Matthieu Sozeau - Institution: LRI, CNRS UMR 8623 - Universit脙copyright Paris Sud - 91405 Orsay, France *) + Institution: LRI, CNRS UMR 8623 - University Paris Sud +*) Require Import Relation_Definitions. Require Import Coq.Classes.Morphisms. Require Import Coq.Program.Program. +Generalizable Variables A l. + (** Morphisms for relations *) -Instance relation_conjunction_morphism : Morphism (relation_equivalence (A:=A) ==> +Instance relation_conjunction_morphism : Proper (relation_equivalence (A:=A) ==> relation_equivalence ==> relation_equivalence) relation_conjunction. Proof. firstorder. Qed. -Instance relation_disjunction_morphism : Morphism (relation_equivalence (A:=A) ==> +Instance relation_disjunction_morphism : Proper (relation_equivalence (A:=A) ==> relation_equivalence ==> relation_equivalence) relation_disjunction. Proof. firstorder. Qed. @@ -31,25 +33,25 @@ Instance relation_disjunction_morphism : Morphism (relation_equivalence (A:=A) = Require Import List. Lemma predicate_equivalence_pointwise (l : list Type) : - Morphism (@predicate_equivalence l ==> pointwise_lifting iff l) id. + Proper (@predicate_equivalence l ==> pointwise_lifting iff l) id. Proof. do 2 red. unfold predicate_equivalence. auto. Qed. Lemma predicate_implication_pointwise (l : list Type) : - Morphism (@predicate_implication l ==> pointwise_lifting impl l) id. + Proper (@predicate_implication l ==> pointwise_lifting impl l) id. Proof. do 2 red. unfold predicate_implication. auto. Qed. -(** The instanciation at relation allows to rewrite applications of relations [R x y] to [R' x y] *) -(* when [R] and [R'] are in [relation_equivalence]. *) +(** The instanciation at relation allows to rewrite applications of relations + [R x y] to [R' x y] when [R] and [R'] are in [relation_equivalence]. *) Instance relation_equivalence_pointwise : - Morphism (relation_equivalence ==> pointwise_relation A (pointwise_relation A iff)) id. + Proper (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 (pointwise_relation A impl)) id. + Proper (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) : +Lemma inverse_pointwise_relation A (R : relation A) : 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 e1de9ee9..9b848551 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -1,3 +1,4 @@ +(* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -6,14 +7,15 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* Typeclass-based relations, tactics and standard instances. +(** * Typeclass-based relations, tactics and standard instances + This is the basic theory needed to formalize morphisms and setoids. - + Author: Matthieu Sozeau - Institution: LRI, CNRS UMR 8623 - Universit脙copyright Paris Sud - 91405 Orsay, France *) + Institution: LRI, CNRS UMR 8623 - University Paris Sud +*) -(* $Id: RelationClasses.v 12187 2009-06-13 19:36:59Z msozeau $ *) +(* $Id$ *) Require Export Coq.Classes.Init. Require Import Coq.Program.Basics. @@ -42,16 +44,18 @@ Unset Strict Implicit. Class Reflexive {A} (R : relation A) := reflexivity : forall x, R x x. -Class Irreflexive {A} (R : relation A) := - irreflexivity :> Reflexive (complement R). +Class Irreflexive {A} (R : relation A) := + irreflexivity : Reflexive (complement R). -Class Symmetric {A} (R : relation A) := +Hint Extern 1 (Reflexive (complement _)) => class_apply @irreflexivity : typeclass_instances. + +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. @@ -61,7 +65,7 @@ Unset Implicit Arguments. (** A HintDb for relations. *) Ltac solve_relation := - match goal with + match goal with | [ |- ?R ?x ?x ] => reflexivity | [ H : ?R ?x ?y |- ?R ?y ?x ] => symmetry ; exact H end. @@ -70,34 +74,39 @@ Hint Extern 4 => solve_relation : relations. (** We can already dualize all these properties. *) -Program Instance flip_Reflexive `(Reflexive A R) : Reflexive (flip R) := - reflexivity (R:=R). +Generalizable Variables A B C D R S T U l eqA eqB eqC eqD. -Program Instance flip_Irreflexive `(Irreflexive A R) : Irreflexive (flip R) := - irreflexivity (R:=R). +Program Lemma flip_Reflexive `(Reflexive A R) : Reflexive (flip R). +Proof. tauto. Qed. + +Hint Extern 3 (Reflexive (flip _)) => apply flip_Reflexive : typeclass_instances. -Program Instance flip_Symmetric `(Symmetric A R) : Symmetric (flip R). +Program Definition flip_Irreflexive `(Irreflexive A R) : Irreflexive (flip R) := + irreflexivity (R:=R). - Solve Obligations using unfold flip ; intros ; tcapp symmetry ; assumption. +Program Definition flip_Symmetric `(Symmetric A R) : Symmetric (flip R) := + fun x y H => symmetry (R:=R) H. -Program Instance flip_Asymmetric `(Asymmetric A R) : Asymmetric (flip R). - - Solve Obligations using program_simpl ; unfold flip in * ; intros ; typeclass_app asymmetry ; eauto. +Program Definition flip_Asymmetric `(Asymmetric A R) : Asymmetric (flip R) := + fun x y H H' => asymmetry (R:=R) H H'. -Program Instance flip_Transitive `(Transitive A R) : Transitive (flip R). +Program Definition flip_Transitive `(Transitive A R) : Transitive (flip R) := + fun x y z H H' => transitivity (R:=R) H' H. - Solve Obligations using unfold flip ; program_simpl ; typeclass_app transitivity ; eauto. +Hint Extern 3 (Irreflexive (flip _)) => class_apply flip_Irreflexive : typeclass_instances. +Hint Extern 3 (Symmetric (flip _)) => class_apply flip_Symmetric : typeclass_instances. +Hint Extern 3 (Asymmetric (flip _)) => class_apply flip_Asymmetric : typeclass_instances. +Hint Extern 3 (Transitive (flip _)) => class_apply flip_Transitive : typeclass_instances. -Program Instance Reflexive_complement_Irreflexive `(Reflexive A (R : relation A)) +Definition Reflexive_complement_Irreflexive `(Reflexive A (R : relation A)) : Irreflexive (complement R). +Proof. firstorder. Qed. - Next Obligation. - Proof. firstorder. Qed. - -Program Instance complement_Symmetric `(Symmetric A (R : relation A)) : Symmetric (complement R). +Definition complement_Symmetric `(Symmetric A (R : relation A)) : Symmetric (complement R). +Proof. firstorder. Qed. - Next Obligation. - Proof. firstorder. Qed. +Hint Extern 3 (Symmetric (complement _)) => class_apply complement_Symmetric : typeclass_instances. +Hint Extern 3 (Irreflexive (complement _)) => class_apply Reflexive_complement_Irreflexive : typeclass_instances. (** * Standard instances. *) @@ -117,7 +126,7 @@ Tactic Notation "reduce" "in" hyp(Hid) := reduce_hyp Hid. Ltac reduce := reduce_goal. -Tactic Notation "apply" "*" constr(t) := +Tactic Notation "apply" "*" constr(t) := first [ refine t | refine (t _) | refine (t _ _) | refine (t _ _ _) | refine (t _ _ _ _) | refine (t _ _ _ _ _) | refine (t _ _ _ _ _ _) | refine (t _ _ _ _ _ _ _) ]. @@ -125,7 +134,7 @@ Ltac simpl_relation := unfold flip, impl, arrow ; try reduce ; program_simpl ; try ( solve [ intuition ]). -Ltac obligation_tactic ::= simpl_relation. +Local Obligation Tactic := simpl_relation. (** Logical implication. *) @@ -174,13 +183,14 @@ Instance Equivalence_PER `(Equivalence A R) : PER R | 10 := (** We can now define antisymmetry w.r.t. an equivalence relation on the carrier. *) Class Antisymmetric A eqA `{equ : Equivalence A eqA} (R : relation A) := - antisymmetry : forall x y, R x y -> R y x -> eqA x y. + antisymmetry : forall {x y}, R x y -> R y x -> eqA x y. -Program Instance flip_antiSymmetric `(Antisymmetric A eqA R) : - ! Antisymmetric A eqA (flip R). +Program Definition flip_antiSymmetric `(Antisymmetric A eqA R) : + Antisymmetric A eqA (flip R). +Proof. firstorder. Qed. (** Leibinz equality [eq] is an equivalence relation. - The instance has low priority as it is always applicable + The instance has low priority as it is always applicable if only the type is constrained. *) Program Instance eq_equivalence : Equivalence (@eq A) | 10. @@ -193,26 +203,24 @@ Program Instance iff_equivalence : Equivalence iff. The resulting theory can be applied to homogeneous binary relations but also to arbitrary n-ary predicates. *) -Require Import Coq.Lists.List. +Local Open Scope list_scope. (* Notation " [ ] " := nil : list_scope. *) (* Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) (at level 1) : list_scope. *) -(* Open Local Scope list_scope. *) - (** A compact representation of non-dependent arities, with the codomain singled-out. *) -Fixpoint arrows (l : list Type) (r : Type) : Type := - match l with +Fixpoint arrows (l : list Type) (r : Type) : Type := + match l with | nil => r | A :: l' => A -> arrows l' r end. (** We can define abbreviations for operation and relation types based on [arrows]. *) -Definition unary_operation A := arrows (cons A nil) A. -Definition binary_operation A := arrows (cons A (cons A nil)) A. -Definition ternary_operation A := arrows (cons A (cons A (cons A nil))) A. +Definition unary_operation A := arrows (A::nil) A. +Definition binary_operation A := arrows (A::A::nil) A. +Definition ternary_operation A := arrows (A::A::A::nil) A. (** We define n-ary [predicate]s as functions into [Prop]. *) @@ -220,13 +228,13 @@ Notation predicate l := (arrows l Prop). (** Unary predicates, or sets. *) -Definition unary_predicate A := predicate (cons A nil). +Definition unary_predicate A := predicate (A::nil). (** Homogeneous binary relations, equivalent to [relation A]. *) -Definition binary_relation A := predicate (cons A (cons A nil)). +Definition binary_relation A := predicate (A::A::nil). -(** We can close a predicate by universal or existential quantification. *) +(** We can close a predicate by universal or existential quantification. *) Fixpoint predicate_all (l : list Type) : predicate l -> Prop := match l with @@ -240,7 +248,7 @@ Fixpoint predicate_exists (l : list Type) : predicate l -> Prop := | A :: tl => fun f => exists x : A, predicate_exists tl (f x) end. -(** Pointwise extension of a binary operation on [T] to a binary operation +(** Pointwise extension of a binary operation on [T] to a binary operation on functions whose codomain is [T]. For an operator on [Prop] this lifts the operator to a binary operation. *) @@ -248,7 +256,7 @@ Fixpoint pointwise_extension {T : Type} (op : binary_operation T) (l : list Type) : binary_operation (arrows l T) := match l with | nil => fun R R' => op R R' - | A :: tl => fun R R' => + | A :: tl => fun R R' => fun x => pointwise_extension op tl (R x) (R' x) end. @@ -257,7 +265,7 @@ Fixpoint pointwise_extension {T : Type} (op : binary_operation T) Fixpoint pointwise_lifting (op : binary_relation Prop) (l : list Type) : binary_relation (predicate l) := match l with | nil => fun R R' => op R R' - | A :: tl => fun R R' => + | A :: tl => fun R R' => forall x, pointwise_lifting op tl (R x) (R' x) end. @@ -289,7 +297,7 @@ Infix "\鈭/" := predicate_union (at level 85, right associativity) : predicate_ (** The always [True] and always [False] predicates. *) -Fixpoint true_predicate {l : list Type} : predicate l := +Fixpoint true_predicate {l : list Type} : predicate l := match l with | nil => True | A :: tl => fun _ => @true_predicate tl @@ -306,17 +314,13 @@ Notation "鈭欌姤鈭" := false_predicate : predicate_scope. (** Predicate equivalence is an equivalence, and predicate implication defines a preorder. *) -Program Instance predicate_equivalence_equivalence : - Equivalence (@predicate_equivalence l). - +Program Instance predicate_equivalence_equivalence : Equivalence (@predicate_equivalence l). Next Obligation. induction l ; firstorder. Qed. - Next Obligation. induction l ; firstorder. Qed. - Next Obligation. fold pointwise_lifting. induction l. firstorder. @@ -326,59 +330,59 @@ Program Instance predicate_equivalence_equivalence : Program Instance predicate_implication_preorder : PreOrder (@predicate_implication l). - Next Obligation. induction l ; firstorder. Qed. - Next Obligation. induction l. firstorder. - unfold predicate_implication in *. simpl in *. + unfold predicate_implication in *. simpl in *. intro. pose (IHl (x x0) (y x0) (z x0)). firstorder. Qed. -(** We define the various operations which define the algebra on binary relations, +(** We define the various operations which define the algebra on binary relations, from the general ones. *) Definition relation_equivalence {A : Type} : relation (relation A) := - @predicate_equivalence (cons _ (cons _ nil)). + @predicate_equivalence (_::_::nil). Class subrelation {A:Type} (R R' : relation A) : Prop := - is_subrelation : @predicate_implication (cons A (cons A nil)) R R'. + is_subrelation : @predicate_implication (A::A::nil) R R'. Implicit Arguments subrelation [[A]]. Definition relation_conjunction {A} (R : relation A) (R' : relation A) : relation A := - @predicate_intersection (cons A (cons A nil)) R R'. + @predicate_intersection (A::A::nil) R R'. Definition relation_disjunction {A} (R : relation A) (R' : relation A) : relation A := - @predicate_union (cons A (cons A nil)) R R'. + @predicate_union (A::A::nil) R R'. (** Relation equivalence is an equivalence, and subrelation defines a partial order. *) +Set Automatic Introduction. + Instance relation_equivalence_equivalence (A : Type) : Equivalence (@relation_equivalence A). -Proof. intro A. exact (@predicate_equivalence_equivalence (cons A (cons A nil))). Qed. +Proof. exact (@predicate_equivalence_equivalence (A::A::nil)). Qed. -Instance relation_implication_preorder : PreOrder (@subrelation A). -Proof. intro A. exact (@predicate_implication_preorder (cons A (cons A nil))). Qed. +Instance relation_implication_preorder A : PreOrder (@subrelation A). +Proof. exact (@predicate_implication_preorder (A::A::nil)). Qed. (** *** Partial Order. A partial order is a preorder which is additionally antisymmetric. - We give an equivalent definition, up-to an equivalence relation + We give an equivalent definition, up-to an equivalence relation on the carrier. *) 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 +(** 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. Proof with auto. - reduce_goal. - pose proof partial_order_equivalence as poe. do 3 red in poe. + reduce_goal. + pose proof partial_order_equivalence as poe. do 3 red in poe. apply <- poe. firstorder. Qed. @@ -392,5 +396,52 @@ Program Instance subrelation_partial_order : unfold relation_equivalence in *. firstorder. Qed. -Typeclasses Opaque arrows predicate_implication predicate_equivalence +Typeclasses Opaque arrows predicate_implication predicate_equivalence relation_equivalence pointwise_lifting. + +(** Rewrite relation on a given support: declares a relation as a rewrite + relation for use by the generalized rewriting tactic. + It helps choosing if a rewrite should be handled + by the generalized or the regular rewriting tactic using leibniz equality. + Users can declare an [RewriteRelation A RA] anywhere to declare default + relations. This is also done automatically by the [Declare Relation A RA] + commands. *) + +Class RewriteRelation {A : Type} (RA : relation A). + +Instance: RewriteRelation impl. +Instance: RewriteRelation iff. +Instance: RewriteRelation (@relation_equivalence A). + +(** Any [Equivalence] declared in the context is automatically considered + a rewrite relation. *) + +Instance equivalence_rewrite_relation `(Equivalence A eqA) : RewriteRelation eqA. + +(** Strict Order *) + +Class StrictOrder {A : Type} (R : relation A) := { + StrictOrder_Irreflexive :> Irreflexive R ; + StrictOrder_Transitive :> Transitive R +}. + +Instance StrictOrder_Asymmetric `(StrictOrder A R) : Asymmetric R. +Proof. firstorder. Qed. + +(** Inversing a [StrictOrder] gives another [StrictOrder] *) + +Lemma StrictOrder_inverse `(StrictOrder A R) : StrictOrder (inverse R). +Proof. firstorder. Qed. + +(** Same for [PartialOrder]. *) + +Lemma PreOrder_inverse `(PreOrder A R) : PreOrder (inverse R). +Proof. firstorder. Qed. + +Hint Extern 3 (StrictOrder (inverse _)) => class_apply StrictOrder_inverse : typeclass_instances. +Hint Extern 3 (PreOrder (inverse _)) => class_apply PreOrder_inverse : typeclass_instances. + +Lemma PartialOrder_inverse `(PartialOrder A eqA R) : PartialOrder eqA (inverse R). +Proof. firstorder. Qed. + +Hint Extern 3 (PartialOrder (inverse _)) => class_apply PartialOrder_inverse : typeclass_instances. diff --git a/theories/Classes/RelationPairs.v b/theories/Classes/RelationPairs.v new file mode 100644 index 00000000..7972c96c --- /dev/null +++ b/theories/Classes/RelationPairs.v @@ -0,0 +1,153 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(** * Relations over pairs *) + + +Require Import Relations Morphisms. + +(* NB: This should be system-wide someday, but for that we need to + fix the simpl tactic, since "simpl fst" would be refused for + the moment. + +Implicit Arguments fst [[A] [B]]. +Implicit Arguments snd [[A] [B]]. +Implicit Arguments pair [[A] [B]]. + +/NB *) + +Local Notation Fst := (@fst _ _). +Local Notation Snd := (@snd _ _). + +Arguments Scope relation_conjunction + [type_scope signature_scope signature_scope]. +Arguments Scope relation_equivalence + [type_scope signature_scope signature_scope]. +Arguments Scope subrelation [type_scope signature_scope signature_scope]. +Arguments Scope Reflexive [type_scope signature_scope]. +Arguments Scope Irreflexive [type_scope signature_scope]. +Arguments Scope Symmetric [type_scope signature_scope]. +Arguments Scope Transitive [type_scope signature_scope]. +Arguments Scope PER [type_scope signature_scope]. +Arguments Scope Equivalence [type_scope signature_scope]. +Arguments Scope StrictOrder [type_scope signature_scope]. + +Generalizable Variables A B RA RB Ri Ro f. + +(** Any function from [A] to [B] allow to obtain a relation over [A] + out of a relation over [B]. *) + +Definition RelCompFun {A B}(R:relation B)(f:A->B) : relation A := + fun a a' => R (f a) (f a'). + +Infix "@@" := RelCompFun (at level 30, right associativity) : signature_scope. + +Notation "R @@1" := (R @@ Fst)%signature (at level 30) : signature_scope. +Notation "R @@2" := (R @@ Snd)%signature (at level 30) : signature_scope. + +(** We declare measures to the system using the [Measure] class. + Otherwise the instances would easily introduce loops, + never instantiating the [f] function. *) + +Class Measure {A B} (f : A -> B). + +(** Standard measures. *) + +Instance fst_measure : @Measure (A * B) A Fst. +Instance snd_measure : @Measure (A * B) B Snd. + +(** We define a product relation over [A*B]: each components should + satisfy the corresponding initial relation. *) + +Definition RelProd {A B}(RA:relation A)(RB:relation B) : relation (A*B) := + relation_conjunction (RA @@1) (RB @@2). + +Infix "*" := RelProd : signature_scope. + +Section RelCompFun_Instances. + Context {A B : Type} (R : relation B). + + Global Instance RelCompFun_Reflexive + `(Measure A B f, Reflexive _ R) : Reflexive (R@@f). + Proof. firstorder. Qed. + + Global Instance RelCompFun_Symmetric + `(Measure A B f, Symmetric _ R) : Symmetric (R@@f). + Proof. firstorder. Qed. + + Global Instance RelCompFun_Transitive + `(Measure A B f, Transitive _ R) : Transitive (R@@f). + Proof. firstorder. Qed. + + Global Instance RelCompFun_Irreflexive + `(Measure A B f, Irreflexive _ R) : Irreflexive (R@@f). + Proof. firstorder. Qed. + + Global Instance RelCompFun_Equivalence + `(Measure A B f, Equivalence _ R) : Equivalence (R@@f). + + Global Instance RelCompFun_StrictOrder + `(Measure A B f, StrictOrder _ R) : StrictOrder (R@@f). + +End RelCompFun_Instances. + +Instance RelProd_Reflexive {A B}(RA:relation A)(RB:relation B) + `(Reflexive _ RA, Reflexive _ RB) : Reflexive (RA*RB). +Proof. firstorder. Qed. + +Instance RelProd_Symmetric {A B}(RA:relation A)(RB:relation B) + `(Symmetric _ RA, Symmetric _ RB) : Symmetric (RA*RB). +Proof. firstorder. Qed. + +Instance RelProd_Transitive {A B}(RA:relation A)(RB:relation B) + `(Transitive _ RA, Transitive _ RB) : Transitive (RA*RB). +Proof. firstorder. Qed. + +Instance RelProd_Equivalence {A B}(RA:relation A)(RB:relation B) + `(Equivalence _ RA, Equivalence _ RB) : Equivalence (RA*RB). + +Lemma FstRel_ProdRel {A B}(RA:relation A) : + relation_equivalence (RA @@1) (RA*(fun _ _ : B => True)). +Proof. firstorder. Qed. + +Lemma SndRel_ProdRel {A B}(RB:relation B) : + relation_equivalence (RB @@2) ((fun _ _ : A =>True) * RB). +Proof. firstorder. Qed. + +Instance FstRel_sub {A B} (RA:relation A)(RB:relation B): + subrelation (RA*RB) (RA @@1). +Proof. firstorder. Qed. + +Instance SndRel_sub {A B} (RA:relation A)(RB:relation B): + subrelation (RA*RB) (RB @@2). +Proof. firstorder. Qed. + +Instance pair_compat { A B } (RA:relation A)(RB:relation B) : + Proper (RA==>RB==> RA*RB) (@pair _ _). +Proof. firstorder. Qed. + +Instance fst_compat { A B } (RA:relation A)(RB:relation B) : + Proper (RA*RB ==> RA) Fst. +Proof. +intros (x,y) (x',y') (Hx,Hy); compute in *; auto. +Qed. + +Instance snd_compat { A B } (RA:relation A)(RB:relation B) : + Proper (RA*RB ==> RB) Snd. +Proof. +intros (x,y) (x',y') (Hx,Hy); compute in *; auto. +Qed. + +Instance RelCompFun_compat {A B}(f:A->B)(R : relation B) + `(Proper _ (Ri==>Ri==>Ro) R) : + Proper (Ri@@f==>Ri@@f==>Ro) (R@@f)%signature. +Proof. unfold RelCompFun; firstorder. Qed. + +Hint Unfold RelProd RelCompFun. +Hint Extern 2 (RelProd _ _ _ _) => split. + diff --git a/theories/Classes/SetoidAxioms.v b/theories/Classes/SetoidAxioms.v deleted file mode 100644 index 03bb9a80..00000000 --- a/theories/Classes/SetoidAxioms.v +++ /dev/null @@ -1,34 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(* Extensionality axioms that can be used when reasoning with setoids. - * - * Author: Matthieu Sozeau - * Institution: LRI, CNRS UMR 8623 - Universit脙copyright Paris Sud - * 91405 Orsay, France *) - -(* $Id: SetoidAxioms.v 12083 2009-04-14 07:22:18Z herbelin $ *) - -Require Import Coq.Program.Program. - -Set Implicit Arguments. -Unset Strict Implicit. - -Require Export Coq.Classes.SetoidClass. - -(* Application of the extensionality axiom to turn a goal on - Leibniz equality to a setoid equivalence (use with care!). *) - -Axiom setoideq_eq : forall `{sa : Setoid a} (x y : a), x == y -> x = y. - -(** Application of the extensionality principle for setoids. *) - -Ltac setoid_extensionality := - match goal with - [ |- @eq ?A ?X ?Y ] => apply (setoideq_eq (a:=A) (x:=X) (y:=Y)) - end. diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v index d3da7d5a..c41c5769 100644 --- a/theories/Classes/SetoidClass.v +++ b/theories/Classes/SetoidClass.v @@ -6,23 +6,24 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* Typeclass-based setoids, tactics and standard instances. - +(** * Typeclass-based setoids, tactics and standard instances. + Author: Matthieu Sozeau - Institution: LRI, CNRS UMR 8623 - Universit胏opyright Paris Sud - 91405 Orsay, France *) + Institution: LRI, CNRS UMR 8623 - University Paris Sud +*) -(* $Id: SetoidClass.v 12187 2009-06-13 19:36:59Z msozeau $ *) +(* $Id$ *) Set Implicit Arguments. Unset Strict Implicit. +Generalizable Variables A. + Require Import Coq.Program.Program. Require Import Relation_Definitions. Require Export Coq.Classes.RelationClasses. Require Export Coq.Classes.Morphisms. -Require Import Coq.Classes.Functions. (** A setoid wraps an equivalence. *) @@ -55,7 +56,7 @@ Existing Instance setoid_trans. (* Program Instance eq_setoid : Setoid A := *) (* equiv := eq ; setoid_equiv := eq_equivalence. *) -Program Instance iff_setoid : Setoid Prop := +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 [=]. *) @@ -69,7 +70,7 @@ Notation " x =/= y " := (complement equiv x y) (at level 70, no associativity) : (** Use the [clsubstitute] command which substitutes an equality in every hypothesis. *) -Ltac clsubst H := +Ltac clsubst H := match type of H with ?x == ?y => substitute H ; clear H x end. @@ -79,7 +80,7 @@ Ltac clsubst_nofail := | [ H : ?x == ?y |- _ ] => clsubst H ; clsubst_nofail | _ => idtac end. - + (** [subst*] will try its best at substituting every equality in the goal. *) Tactic Notation "clsubst" "*" := clsubst_nofail. @@ -94,7 +95,7 @@ Qed. Lemma equiv_nequiv_trans : forall `{Setoid A} (x y z : A), x == y -> y =/= z -> x =/= z. Proof. - intros; intro. + intros; intro. assert(y == x) by (symmetry ; auto). assert(y == z) by (transitivity x ; eauto). contradiction. @@ -119,25 +120,15 @@ Ltac setoidify := repeat setoidify_tac. (** Every setoid relation gives rise to a morphism, in fact every partial setoid does. *) -Program Instance setoid_morphism `(sa : Setoid A) : Morphism (equiv ++> equiv ++> iff) equiv := - respect. - -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. - -Ltac obligation_tactic ::= morphism_tac. - -(** These are morphisms used to rewrite at the top level of a proof, - using [iff_impl_id_morphism] if the proof is in [Prop] and - [eq_arrow_id_morphism] if it is in Type. *) +Program Instance setoid_morphism `(sa : Setoid A) : Proper (equiv ++> equiv ++> iff) equiv := + proper_prf. -Program Instance iff_impl_id_morphism : Morphism (iff ++> impl) id. +Program Instance setoid_partial_app_morphism `(sa : Setoid A) (x : A) : Proper (equiv ++> iff) (equiv x) := + proper_prf. (** Partial setoids don't require reflexivity so we can build a partial setoid on the function space. *) -Class PartialSetoid (A : Type) := +Class PartialSetoid (A : Type) := { pequiv : relation A ; pequiv_prf :> PER pequiv }. (** Overloaded notation for partial setoid equivalence. *) @@ -146,4 +137,4 @@ Infix "=~=" := pequiv (at level 70, no associativity) : type_scope. (** Reset the default Program tactic. *) -Ltac obligation_tactic ::= program_simpl. +Obligation Tactic := program_simpl. diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v index bac64724..33b4350f 100644 --- a/theories/Classes/SetoidDec.v +++ b/theories/Classes/SetoidDec.v @@ -1,3 +1,4 @@ +(* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -6,43 +7,47 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* Decidable setoid equality theory. - * - * Author: Matthieu Sozeau - * Institution: LRI, CNRS UMR 8623 - Universit脙copyright Paris Sud - * 91405 Orsay, France *) +(** * Decidable setoid equality theory. -(* $Id: SetoidDec.v 11800 2009-01-18 18:34:15Z msozeau $ *) + Author: Matthieu Sozeau + Institution: LRI, CNRS UMR 8623 - University Paris Sud +*) + +(* $Id$ *) Set Implicit Arguments. Unset Strict Implicit. +Generalizable Variables A B . + (** Export notations. *) Require Export Coq.Classes.SetoidClass. -(** The [DecidableSetoid] class asserts decidability of a [Setoid]. It can be useful in proofs to reason more - classically. *) +(** The [DecidableSetoid] class asserts decidability of a [Setoid]. + It can be useful in proofs to reason more classically. *) Require Import Coq.Logic.Decidable. 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. *) +(** The [EqDec] class gives a decision procedure for a particular setoid + equality. *) 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 - of [==] defined in the type scope, hence we can have both at the same time. *) +(** We define the [==] overloaded notation for deciding equality. It does not + take precedence of [==] defined in the type scope, hence we can have both + at the same time. *) Notation " x == y " := (equiv_dec (x :>) (y :>)) (no associativity, at level 70). Definition swap_sumbool {A B} (x : { A } + { B }) : { B } + { A } := match x with - | left H => @right _ _ H - | right H => @left _ _ H + | left H => @right _ _ H + | right H => @left _ _ H end. Require Import Coq.Program.Program. @@ -72,7 +77,8 @@ Infix "<>b" := nequiv_decb (no associativity, at level 70). 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. *) +(** 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 | 10 := { equiv := eq ; setoid_equiv := eq_equivalence }. @@ -96,16 +102,17 @@ Program Instance unit_eqdec : EqDec (eq_setoid unit) := 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 + 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. Solve Obligations using unfold complement ; program_simpl. -(** Objects of function spaces with countable domains like bool have decidable equality. *) +(** Objects of function spaces with countable domains like bool + have decidable equality. *) Program Instance bool_function_eqdec `(! EqDec (eq_setoid A)) : EqDec (eq_setoid (bool -> A)) := 位 f g, diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v index 36f05e31..669be8b0 100644 --- a/theories/Classes/SetoidTactics.v +++ b/theories/Classes/SetoidTactics.v @@ -1,4 +1,3 @@ -(* -*- coq-prog-args: ("-emacs-U" "-top" "Coq.Classes.SetoidTactics") -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -7,38 +6,28 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* Tactics for typeclass-based setoids. - * - * Author: Matthieu Sozeau - * Institution: LRI, CNRS UMR 8623 - Universit胏opyright Paris Sud - * 91405 Orsay, France *) +(** * Tactics for typeclass-based setoids. -(* $Id: SetoidTactics.v 12187 2009-06-13 19:36:59Z msozeau $ *) + Author: Matthieu Sozeau + Institution: LRI, CNRS UMR 8623 - University Paris Sud +*) + +(* $Id$ *) Require Import Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop. Require Export Coq.Classes.RelationClasses Coq.Relations.Relation_Definitions. Require Import Coq.Classes.Equivalence Coq.Program.Basics. -Export MorphismNotations. +Generalizable Variables A R. + +Export ProperNotations. Set Implicit Arguments. Unset Strict Implicit. -(** Setoid relation on a given support: declares a relation as a setoid - for use with rewrite. It helps choosing if a rewrite should be handled - by setoid_rewrite or the regular rewrite using leibniz equality. - Users can declare an [SetoidRelation A RA] anywhere to declare default - relations. This is also done automatically by the [Declare Relation A RA] - commands. *) - -Class SetoidRelation A (R : relation A). - -Instance impl_setoid_relation : SetoidRelation impl. -Instance iff_setoid_relation : SetoidRelation iff. - (** Default relation on a given support. Can be used by tactics - to find a sensible default relation on any carrier. Users can - declare an [Instance def : DefaultRelation A RA] anywhere to + to find a sensible default relation on any carrier. Users can + declare an [Instance def : DefaultRelation A RA] anywhere to declare default relations. *) Class DefaultRelation A (R : relation A). @@ -47,12 +36,13 @@ Class DefaultRelation A (R : relation A). Definition default_relation `{DefaultRelation A R} := R. -(** Every [Equivalence] gives a default relation, if no other is given (lowest priority). *) +(** Every [Equivalence] gives a default relation, if no other is given + (lowest priority). *) 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. *) +(** The setoid_replace tactics in Ltac, defined in terms of default relations + and the setoid_rewrite tactic. *) Ltac setoidreplace H t := let Heq := fresh "Heq" in @@ -73,86 +63,88 @@ Ltac setoidreplaceat H t occs := Tactic Notation "setoid_replace" constr(x) "with" constr(y) := setoidreplace (default_relation x y) idtac. -Tactic Notation "setoid_replace" constr(x) "with" constr(y) +Tactic Notation "setoid_replace" constr(x) "with" constr(y) "at" int_or_var_list(o) := setoidreplaceat (default_relation x y) idtac o. -Tactic Notation "setoid_replace" constr(x) "with" constr(y) +Tactic Notation "setoid_replace" constr(x) "with" constr(y) "in" hyp(id) := setoidreplacein (default_relation x y) id idtac. Tactic Notation "setoid_replace" constr(x) "with" constr(y) - "in" hyp(id) + "in" hyp(id) "at" int_or_var_list(o) := setoidreplaceinat (default_relation x y) id idtac o. -Tactic Notation "setoid_replace" constr(x) "with" constr(y) +Tactic Notation "setoid_replace" constr(x) "with" constr(y) "by" tactic3(t) := setoidreplace (default_relation x y) ltac:t. -Tactic Notation "setoid_replace" constr(x) "with" constr(y) - "at" int_or_var_list(o) +Tactic Notation "setoid_replace" constr(x) "with" constr(y) + "at" int_or_var_list(o) "by" tactic3(t) := setoidreplaceat (default_relation x y) ltac:t o. -Tactic Notation "setoid_replace" constr(x) "with" constr(y) - "in" hyp(id) +Tactic Notation "setoid_replace" constr(x) "with" constr(y) + "in" hyp(id) "by" tactic3(t) := setoidreplacein (default_relation x y) id ltac:t. -Tactic Notation "setoid_replace" constr(x) "with" constr(y) - "in" hyp(id) - "at" int_or_var_list(o) +Tactic Notation "setoid_replace" constr(x) "with" constr(y) + "in" hyp(id) + "at" int_or_var_list(o) "by" tactic3(t) := setoidreplaceinat (default_relation x y) id ltac:t o. -Tactic Notation "setoid_replace" constr(x) "with" constr(y) +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) +Tactic Notation "setoid_replace" constr(x) "with" constr(y) "using" "relation" constr(rel) "at" int_or_var_list(o) := setoidreplaceat (rel x y) idtac o. -Tactic Notation "setoid_replace" constr(x) "with" constr(y) - "using" "relation" constr(rel) +Tactic Notation "setoid_replace" constr(x) "with" constr(y) + "using" "relation" constr(rel) "by" tactic3(t) := setoidreplace (rel x y) ltac:t. -Tactic Notation "setoid_replace" constr(x) "with" constr(y) - "using" "relation" constr(rel) - "at" int_or_var_list(o) +Tactic Notation "setoid_replace" constr(x) "with" constr(y) + "using" "relation" constr(rel) + "at" int_or_var_list(o) "by" tactic3(t) := setoidreplaceat (rel x y) ltac:t o. -Tactic Notation "setoid_replace" constr(x) "with" constr(y) +Tactic Notation "setoid_replace" constr(x) "with" constr(y) "using" "relation" constr(rel) "in" hyp(id) := setoidreplacein (rel x y) id idtac. -Tactic Notation "setoid_replace" constr(x) "with" constr(y) +Tactic Notation "setoid_replace" constr(x) "with" constr(y) "using" "relation" constr(rel) - "in" hyp(id) + "in" hyp(id) "at" int_or_var_list(o) := setoidreplaceinat (rel x y) id idtac o. -Tactic Notation "setoid_replace" constr(x) "with" constr(y) +Tactic Notation "setoid_replace" constr(x) "with" constr(y) "using" "relation" constr(rel) "in" hyp(id) "by" tactic3(t) := setoidreplacein (rel x y) id ltac:t. -Tactic Notation "setoid_replace" constr(x) "with" constr(y) - "using" "relation" constr(rel) +Tactic Notation "setoid_replace" constr(x) "with" constr(y) + "using" "relation" constr(rel) "in" hyp(id) - "at" int_or_var_list(o) + "at" int_or_var_list(o) "by" tactic3(t) := setoidreplaceinat (rel x y) id ltac:t o. -(** The [add_morphism_tactic] tactic is run at each [Add Morphism] command before giving the hand back - to the user to discharge the proof. It essentially amounts to unfold the right amount of [respectful] calls - and substitute leibniz equalities. One can redefine it using [Ltac add_morphism_tactic ::= t]. *) +(** The [add_morphism_tactic] tactic is run at each [Add Morphism] + command before giving the hand back to the user to discharge the + proof. It essentially amounts to unfold the right amount of + [respectful] calls and substitute leibniz equalities. One can + redefine it using [Ltac add_morphism_tactic ::= t]. *) Require Import Coq.Program.Tactics. @@ -165,9 +157,9 @@ Ltac red_subst_eq_morphism concl := | _ => idtac end. -Ltac destruct_morphism := +Ltac destruct_proper := match goal with - | [ |- @Morphism ?A ?R ?m ] => red + | [ |- @Proper ?A ?R ?m ] => red end. Ltac reverse_arrows x := @@ -179,11 +171,13 @@ Ltac reverse_arrows x := Ltac default_add_morphism_tactic := unfold flip ; intros ; - (try destruct_morphism) ; + (try destruct_proper) ; match goal with | [ |- (?x ==> ?y) _ _ ] => red_subst_eq_morphism (x ==> y) ; reverse_arrows (x ==> y) end. Ltac add_morphism_tactic := default_add_morphism_tactic. -Ltac obligation_tactic ::= program_simpl. +Obligation Tactic := program_simpl. + +(* Notation "'Morphism' s t " := (@Proper _ (s%signature) t) (at level 10, s at next level, t at next level). *) diff --git a/theories/Classes/vo.itarget b/theories/Classes/vo.itarget new file mode 100644 index 00000000..9daf133b --- /dev/null +++ b/theories/Classes/vo.itarget @@ -0,0 +1,11 @@ +Equivalence.vo +EquivDec.vo +Init.vo +Morphisms_Prop.vo +Morphisms_Relations.vo +Morphisms.vo +RelationClasses.vo +SetoidClass.vo +SetoidDec.vo +SetoidTactics.vo +RelationPairs.vo |