diff options
Diffstat (limited to 'theories/Classes')
| -rw-r--r-- | theories/Classes/Equivalence.v | 123 | ||||
| -rw-r--r-- | theories/Classes/Morphisms.v | 288 | ||||
| -rw-r--r-- | theories/Classes/Morphisms_Prop.v | 131 | ||||
| -rw-r--r-- | theories/Classes/Morphisms_Relations.v | 47 | ||||
| -rw-r--r-- | theories/Classes/RelationClasses.v | 226 | ||||
| -rw-r--r-- | theories/Classes/SetoidTactics.v | 2 |
6 files changed, 474 insertions, 343 deletions
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v index 0ec6c11f9..d7774a2d7 100644 --- a/theories/Classes/Equivalence.v +++ b/theories/Classes/Equivalence.v @@ -35,23 +35,25 @@ Instance [ Equivalence A R ] => Definition equiv [ Equivalence A R ] : relation A := R. -(** Shortcuts to make proof search possible (unification won't unfold equiv). *) +Typeclasses unfold @equiv. -Program Instance [ sa : Equivalence A ] => equiv_refl : Reflexive equiv. +(* (** Shortcuts to make proof search possible (unification won't unfold equiv). *) *) -Program Instance [ sa : Equivalence A ] => equiv_sym : Symmetric equiv. +(* Program Instance [ sa : Equivalence A ] => equiv_refl : Reflexive equiv. *) - Next Obligation. - Proof. - symmetry ; auto. - Qed. +(* Program Instance [ sa : Equivalence A ] => equiv_sym : Symmetric equiv. *) -Program Instance [ sa : Equivalence A ] => equiv_trans : Transitive equiv. +(* Next Obligation. *) +(* Proof. *) +(* symmetry ; auto. *) +(* Qed. *) - Next Obligation. - Proof. - transitivity y ; auto. - Qed. +(* Program Instance [ sa : Equivalence A ] => equiv_trans : Transitive equiv. *) + +(* Next Obligation. *) +(* Proof. *) +(* transitivity y ; auto. *) +(* Qed. *) (** Overloaded notations for setoid equivalence and inequivalence. Not to be confused with [eq] and [=]. *) @@ -64,23 +66,6 @@ Notation " x =/= y " := (complement equiv x y) (at level 70, no associativity) : Open Local Scope equiv_scope. -(** Use the [clsubstitute] command which substitutes an equality in every hypothesis. *) - -Ltac setoid_subst H := - match type of H with - ?x === ?y => substitute H ; clear H x - end. - -Ltac setoid_subst_nofail := - match goal with - | [ 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. - Lemma nequiv_equiv_trans : forall [ Equivalence A ] (x y z : A), x =/= y -> y === z -> x =/= z. Proof with auto. intros; intro. @@ -97,6 +82,23 @@ Proof. contradiction. Qed. +(** Use the [substitute] command which substitutes an applied relation in every hypothesis. *) + +Ltac setoid_subst H := + match type of H with + ?x === ?y => substitute H ; clear H x + end. + +Ltac setoid_subst_nofail := + match goal with + | [ 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. + Ltac equiv_simplify_one := match goal with | [ H : ?x === ?x |- _ ] => clear H @@ -117,34 +119,28 @@ Ltac equivify := repeat equivify_tac. (** Every equivalence relation gives rise to a morphism, as it is Transitive and Symmetric. *) -Instance [ sa : Equivalence ] => equiv_morphism : Morphism (equiv ++> equiv ++> iff) equiv := - respect := respect. - -(** The partial application too as it is Reflexive. *) +(* Instance [ sa : Equivalence ] => equiv_morphism : Morphism (equiv ++> equiv ++> iff) equiv := *) +(* respect := respect. *) -Instance [ sa : Equivalence A ] (x : A) => - equiv_partial_app_morphism : Morphism (equiv ++> iff) (equiv x) := - respect := respect. +(* (** The partial application too as it is Reflexive. *) *) -Definition type_eq : relation Type := - fun x y => x = y. +(* Instance [ sa : Equivalence A ] (x : A) => *) +(* equiv_partial_app_morphism : Morphism (equiv ++> iff) (equiv x) := *) +(* respect := respect. *) -Program Instance type_equivalence : Equivalence Type type_eq. +(** Instance not exported by default, as comparing types for equivalence may be unintentional. *) - Solve Obligations using constructor ; unfold type_eq ; program_simpl. +Section Type_Equivalence. -Ltac morphism_tac := try red ; unfold arrow ; intros ; program_simpl ; try tauto. - -Ltac obligations_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 iff_impl_id_morphism : - Morphism (iff ++> impl) id. + Definition type_eq : relation Type := + fun x y => x = y. + + Program Instance type_equivalence : Equivalence Type type_eq. + + Next Obligation. + Proof. unfold type_eq in *. subst. reflexivity. Qed. -(* Program Instance eq_arrow_id_morphism : ? Morphism (eq +++> arrow) id. *) +End Type_Equivalence. (** Partial equivs don't require reflexivity so we can build a partial equiv on the function space. *) @@ -152,11 +148,32 @@ Class PartialEquivalence (carrier : Type) (pequiv : relation carrier) := pequiv_prf :> PER carrier pequiv. Definition pequiv [ PartialEquivalence A R ] : relation A := R. +Typeclasses unfold @pequiv. (** Overloaded notation for partial equiv equivalence. *) Notation " x =~= y " := (pequiv x y) (at level 70, no associativity) : type_scope. -(** Reset the default Program tactic. *) +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 := + { morph : A -> B | respectful R R' morph morph }. + + Program Instance [ Equivalence A R, Equivalence B R' ] => + respecting_equiv : Equivalence respecting + (fun (f g : respecting) => forall (x y : A), R x y -> R' (proj1_sig f x) (proj1_sig g y)). + + Solve Obligations using unfold respecting in * ; simpl_relation ; program_simpl. + + Next Obligation. + Proof. + unfold respecting in *. program_simpl. red in H2,H3,H4. + transitivity (y x0) ; auto. + transitivity (y y0) ; auto. + symmetry. auto. + Qed. -Ltac obligations_tactic ::= program_simpl. +End Respecting.
\ No newline at end of file diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v index d10cb9724..7cabc836d 100644 --- a/theories/Classes/Morphisms.v +++ b/theories/Classes/Morphisms.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-emacs-U" "-top" "Coq.Classes.Morphisms") -*- *) +(* -*- coq-prog-args: ("-emacs-U" "-top" "Coq.Classes.Morphisms"); compile-command: "make -C ../.. TIME='time'" -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* Typeclass-based morphisms with standard instances for equivalence relations. +(* Typeclass-based morphism definition and standard, minimal instances. Author: Matthieu Sozeau Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud @@ -26,7 +26,7 @@ Unset Strict Implicit. (** * Morphisms. We now turn to the definition of [Morphism] and declare standard instances. - These will be used by the [clrewrite] tactic later. *) + These will be used by the [setoid_rewrite] tactic later. *) (** Respectful morphisms. *) @@ -71,49 +71,6 @@ Class Morphism A (R : relation A) (m : A) : Prop := Arguments Scope Morphism [type_scope signature_scope]. -(** Here we build an equivalence instance for functions which relates respectful ones only. *) - -Definition respecting [ Equivalence A (R : relation A), Equivalence B (R' : relation B) ] : Type := - { morph : A -> B | respectful R R' morph morph }. - -Ltac obligations_tactic ::= program_simpl. - -Program Instance [ Equivalence A R, Equivalence B R' ] => - respecting_equiv : Equivalence respecting - (fun (f g : respecting) => forall (x y : A), R x y -> R' (proj1_sig f x) (proj1_sig g y)). - - Next Obligation. - Proof. - red ; intros. - destruct x ; simpl. - apply r ; auto. - Qed. - - Next Obligation. - Proof. - red ; intros. - symmetry ; apply H. - symmetry ; auto. - Qed. - - Next Obligation. - Proof. - red ; intros. - transitivity (proj1_sig y y0). - apply H ; auto. - apply H0. reflexivity. - Qed. - -(** Can't use the definition [notT] as it gives a universe inconsistency. *) - -Ltac obligations_tactic ::= program_simpl ; simpl_relation. - -Program Instance not_impl_morphism : - Morphism (Prop -> Prop) (impl --> impl) not. - -Program Instance not_iff_morphism : - Morphism (Prop -> Prop) (iff ++> iff) not. - (** We make the type implicit, it can be infered from the relations. *) Implicit Arguments Morphism [A]. @@ -139,41 +96,41 @@ Proof. firstorder. Qed. (** [Morphism] is itself a covariant morphism for [subrelation]. *) -Lemma subrelation_morphism [ subrelation A R₁ R₂, ! Morphism R₁ m ] : Morphism R₂ m. +Lemma subrelation_morphism [ sub : subrelation A R₁ R₂, mor : Morphism A R₁ m ] : Morphism R₂ m. Proof. - intros. apply* H. apply H0. + intros. apply sub. apply mor. Qed. Instance morphism_subrelation_morphism : Morphism (subrelation ++> @eq _ ==> impl) (@Morphism A). Proof. reduce. subst. firstorder. Qed. -Inductive done : nat -> Type := - did : forall n : nat, done n. +(** 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. Ltac subrelation_tac := match goal with - | [ H : done 1 |- @Morphism _ _ _ ] => fail + | [ H : subrelation_done |- _ ] => fail | [ |- @Morphism _ _ _ ] => let H := fresh "H" in - set(H:=did 1) ; eapply @subrelation_morphism + set(H:=did_subrelation) ; eapply @subrelation_morphism end. -(* Hint Resolve @subrelation_morphism 4 : typeclass_instances. *) - Hint Extern 4 (@Morphism _ _ _) => subrelation_tac : typeclass_instances. -(** Logical implication [impl] is a morphism for logical equivalence. *) +(** Essential subrelation instances for [iff], [impl] and [pointwise_relation]. *) -Program Instance iff_iff_iff_impl_morphism : Morphism (iff ==> iff ==> iff) impl. +Instance iff_impl_subrelation : subrelation iff impl. +Proof. firstorder. Qed. -(* Typeclasses eauto := debug. *) +Instance iff_inverse_impl_subrelation : subrelation iff (inverse impl). +Proof. firstorder. Qed. -Program Instance [ Symmetric A R, Morphism _ (R ==> impl) m ] => Reflexive_impl_iff : Morphism (R ==> iff) m. - - Next Obligation. - Proof. - split ; apply respect ; [ auto | symmetry ] ; auto. - Qed. +Instance [ subrelation A R R' ] => pointwise_subrelation : + subrelation (pointwise_relation (A:=B) R) (pointwise_relation R') | 4. +Proof. reduce. unfold pointwise_relation in *. apply subrelation0. apply H. Qed. (** The complement of a relation conserves its morphisms. *) @@ -183,28 +140,26 @@ Program Instance [ mR : Morphism (A -> A -> Prop) (RA ==> RA ==> iff) R ] => Next Obligation. Proof. unfold complement. - pose (respect). - pose (r x y H). - pose (r0 x0 y0 H0). + pose (mR x y H x0 y0 H0). intuition. Qed. (** The inverse too. *) -Program Instance [ Morphism (A -> _) (RA ==> RA ==> iff) R ] => +Program Instance [ mor : Morphism (A -> _) (RA ==> RA ==> iff) R ] => inverse_morphism : Morphism (RA ==> RA ==> iff) (inverse R). Next Obligation. Proof. - apply respect ; auto. + apply mor ; auto. Qed. -Program Instance [ Morphism (A -> B -> C) (RA ==> RB ==> RC) f ] => +Program Instance [ mor : Morphism (A -> B -> C) (RA ==> RB ==> RC) f ] => flip_morphism : Morphism (RB ==> RA ==> RC) (flip f). Next Obligation. Proof. - apply respect ; auto. + apply mor ; auto. Qed. (** Every Transitive relation gives rise to a binary morphism on [impl], @@ -229,18 +184,6 @@ Program Instance [ Transitive A R ] => apply* trans_contra_co_morphism ; eauto. eauto. Qed. -(* Program Instance [ Transitive A (R : relation A), Symmetric A R ] => *) -(* trans_sym_contra_co_inv_impl_morphism : ? Morphism (R --> R ++> inverse impl) R. *) - -(* Next Obligation. *) -(* Proof with auto. *) -(* trans y... *) -(* sym... *) -(* trans y0... *) -(* sym... *) -(* Qed. *) - - (** Morphism declarations for partial applications. *) Program Instance [ Transitive A R ] (x : A) => @@ -286,18 +229,6 @@ Program Instance [ Equivalence A R ] (x : A) => symmetry... Qed. -(** With Symmetric relations, variance is no issue ! *) - -(* Program Instance (A B : Type) (R : relation A) (R' : relation B) *) -(* [ Morphism _ (R ==> R') m ] [ Symmetric A R ] => *) -(* sym_contra_morphism : Morphism (R --> R') m. *) - -(* Next Obligation. *) -(* Proof with auto. *) -(* repeat (red ; intros). apply respect. *) -(* sym... *) -(* Qed. *) - (** [R] is Reflexive, hence we can build the needed proof. *) Program Instance [ Morphism (A -> B) (R ==> R') m, Reflexive _ R ] (x : A) => @@ -360,57 +291,9 @@ Program Instance iff_impl_id : Program Instance inverse_iff_impl_id : Morphism (iff --> impl) id. -(** Standard instances for [iff] and [impl]. *) - -(** Logical conjunction. *) - -Program Instance and_impl_iff_morphism : - Morphism (impl ==> iff ==> impl) and. - -Program Instance and_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. - -(** Logical disjunction. *) - -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. - (** Coq functions are morphisms for leibniz equality, applied only if really needed. *) -(* Instance {A B : Type} (m : A -> B) => *) -(* any_eq_eq_morphism : Morphism (@Logic.eq A ==> @Logic.eq B) m | 4. *) -(* Proof. *) -(* red ; intros. subst ; reflexivity. *) -(* Qed. *) - -(* Instance {A : Type} (m : A -> Prop) => *) -(* any_eq_iff_morphism : Morphism (@Logic.eq A ==> iff) m | 4. *) -(* Proof. *) -(* red ; intros. subst ; split; trivial. *) -(* Qed. *) - Instance (A : Type) [ Reflexive B R ] (m : A -> B) => eq_reflexive_morphism : Morphism (@Logic.eq A ==> R) m | 3. Proof. simpl_relation. Qed. @@ -419,18 +302,13 @@ Instance (A : Type) [ Reflexive B R' ] => Reflexive (@Logic.eq A ==> R'). Proof. simpl_relation. Qed. -Instance [ Morphism (A -> B) (inverse R ==> R') m ] => - Morphism (R ==> inverse R') m | 10. -Proof. firstorder. Qed. - (** [respectful] is a morphism for relation equivalence. *) Instance respectful_morphism : Morphism (relation_equivalence ++> relation_equivalence ++> relation_equivalence) (@respectful A B). Proof. - do 2 red ; intros. - unfold respectful, relation_equivalence in *. - red ; intros. + reduce. + unfold respectful, relation_equivalence, predicate_equivalence in * ; simpl in *. split ; intros. rewrite <- H0. @@ -452,21 +330,18 @@ Proof. split ; intros ; intuition. Qed. + Class (A : Type) (R : relation A) => Normalizes (m : A) (m' : A) : Prop := normalizes : R m m'. Instance (A : Type) (R : relation A) (B : Type) (R' : relation B) => - Normalizes relation_equivalence (inverse R ==> inverse R') (inverse (R ==> R')) . -Proof. - reduce. - symmetry ; apply inverse_respectful. -Qed. + Normalizes subrelation (inverse R ==> inverse R') (inverse (R ==> R')) . +Proof. simpl_relation. Qed. Instance [ Normalizes (relation B) relation_equivalence R' (inverse R'') ] => ! Normalizes (relation (A -> B)) relation_equivalence (inverse R ==> R') (inverse (R ==> R'')) . -Proof. - red. - pose normalizes. +Proof. red ; intros. + pose normalizes as r. setoid_rewrite r. setoid_rewrite inverse_respectful. reflexivity. @@ -479,23 +354,23 @@ Program Instance [ Morphism A R m ] => Instance morphism_morphism : Morphism (relation_equivalence ==> @eq _ ==> iff) (@Morphism A). Proof. - simpl_relation. - unfold relation_equivalence in H. + simpl_relation. + reduce in H. split ; red ; intros. setoid_rewrite <- H. - apply respect. + apply H0. setoid_rewrite H. - apply respect. + apply H0. Qed. - + Lemma morphism_releq_morphism [ Normalizes (relation A) relation_equivalence R R', Morphism _ R' m ] : Morphism R m. Proof. intros. - pose respect. - assert(n:=normalizes). - setoid_rewrite n. + pose respect as r. + pose normalizes as norm. + setoid_rewrite norm. assumption. Qed. @@ -510,86 +385,3 @@ Ltac morphism_normalization := Hint Extern 5 (@Morphism _ _ _) => morphism_normalization : typeclass_instances. -(** Morphisms for relations *) - -Instance [ PartialOrder A eqA R ] => - partial_order_morphism : Morphism (eqA ==> eqA ==> iff) R. -Proof with auto. - intros. rewrite partial_order_equivalence. - simpl_relation. firstorder. - transitivity x... transitivity x0... - transitivity y... transitivity y0... -Qed. - -Instance Morphism (relation_equivalence (A:=A) ==> - relation_equivalence ==> relation_equivalence) relation_conjunction. - Proof. firstorder. Qed. - -Instance Morphism (relation_equivalence (A:=A) ==> - relation_equivalence ==> relation_equivalence) relation_disjunction. - Proof. firstorder. Qed. - - -(** Morphisms for quantifiers *) - -Program Instance {A : Type} => ex_iff_morphism : Morphism (pointwise_relation iff ==> iff) (@ex A). - - Next Obligation. - Proof. - 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. - Qed. - -Program Instance {A : Type} => ex_impl_morphism : - Morphism (pointwise_relation impl ==> impl) (@ex A). - - Next Obligation. - Proof. - unfold pointwise_relation in H. - exists H0. apply H. assumption. - Qed. - -Program Instance {A : Type} => ex_inverse_impl_morphism : - Morphism (pointwise_relation (inverse impl) ==> inverse impl) (@ex A). - - Next Obligation. - Proof. - unfold pointwise_relation in H. - exists H0. apply H. assumption. - Qed. - -Program Instance {A : Type} => all_iff_morphism : - Morphism (pointwise_relation iff ==> iff) (@all A). - - Next Obligation. - Proof. - unfold pointwise_relation, all in *. - intuition ; specialize (H x0) ; intuition. - Qed. - -Program Instance {A : Type} => all_impl_morphism : - Morphism (pointwise_relation impl ==> impl) (@all A). - - Next Obligation. - Proof. - unfold pointwise_relation, all in *. - intuition ; specialize (H x0) ; intuition. - Qed. - -Program Instance {A : Type} => all_inverse_impl_morphism : - Morphism (pointwise_relation (inverse impl) ==> inverse impl) (@all A). - - Next Obligation. - Proof. - unfold pointwise_relation, all in *. - intuition ; specialize (H x0) ; intuition. - Qed. - -Lemma inverse_pointwise_relation A (R : relation A) : - relation_equivalence (pointwise_relation (inverse R)) (inverse (pointwise_relation (A:=A) R)). -Proof. reflexivity. Qed. diff --git a/theories/Classes/Morphisms_Prop.v b/theories/Classes/Morphisms_Prop.v new file mode 100644 index 000000000..d22ab06cb --- /dev/null +++ b/theories/Classes/Morphisms_Prop.v @@ -0,0 +1,131 @@ +(* -*- 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 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* Morphism instances for propositional connectives. + + Author: Matthieu Sozeau + Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud + 91405 Orsay, France *) + +Require Import Coq.Classes.Morphisms. +Require Import Coq.Program.Program. + +(** Standard instances for [not], [iff] and [impl]. *) + +(** Logical negation. *) + +Program Instance not_impl_morphism : + Morphism (impl --> impl) not. + +Program Instance not_iff_morphism : + Morphism (iff ++> iff) not. + +(** Logical conjunction. *) + +Program Instance and_impl_iff_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. + +(** Logical disjunction. *) + +Program Instance or_impl_iff_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. + +(** Logical implication [impl] is a morphism for logical equivalence. *) + +Program Instance iff_iff_iff_impl_morphism : Morphism (iff ==> iff ==> iff) impl. + +(** Morphisms for quantifiers *) + +Program Instance {A : Type} => ex_iff_morphism : Morphism (pointwise_relation iff ==> iff) (@ex A). + + Next Obligation. + Proof. + 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. + Qed. + +Program Instance {A : Type} => ex_impl_morphism : + Morphism (pointwise_relation impl ==> impl) (@ex A). + + Next Obligation. + Proof. + unfold pointwise_relation in H. + exists H0. apply H. assumption. + Qed. + +Program Instance {A : Type} => ex_inverse_impl_morphism : + Morphism (pointwise_relation (inverse impl) ==> inverse impl) (@ex A). + + Next Obligation. + Proof. + unfold pointwise_relation in H. + exists H0. apply H. assumption. + Qed. + +Program Instance {A : Type} => all_iff_morphism : + Morphism (pointwise_relation iff ==> iff) (@all A). + + Next Obligation. + Proof. + unfold pointwise_relation, all in *. + intuition ; specialize (H x0) ; intuition. + Qed. + +Program Instance {A : Type} => all_impl_morphism : + Morphism (pointwise_relation impl ==> impl) (@all A). + + Next Obligation. + Proof. + unfold pointwise_relation, all in *. + intuition ; specialize (H x0) ; intuition. + Qed. + +Program Instance {A : Type} => all_inverse_impl_morphism : + Morphism (pointwise_relation (inverse impl) ==> inverse impl) (@all A). + + Next Obligation. + Proof. + unfold pointwise_relation, all in *. + intuition ; specialize (H x0) ; intuition. + Qed. diff --git a/theories/Classes/Morphisms_Relations.v b/theories/Classes/Morphisms_Relations.v new file mode 100644 index 000000000..284810e94 --- /dev/null +++ b/theories/Classes/Morphisms_Relations.v @@ -0,0 +1,47 @@ +(* -*- 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 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* Morphism instances for relations. + + Author: Matthieu Sozeau + Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud + 91405 Orsay, France *) + +(** Morphisms for relations *) + +Instance relation_conjunction_morphism : Morphism (relation_equivalence (A:=A) ==> + relation_equivalence ==> relation_equivalence) relation_conjunction. + Proof. firstorder. Qed. + +Instance relation_disjunction_morphism : Morphism (relation_equivalence (A:=A) ==> + relation_equivalence ==> relation_equivalence) relation_disjunction. + Proof. firstorder. Qed. + +(* Predicate equivalence is exactly the same as the pointwise lifting of [iff]. *) + +Require Import List. + +Lemma predicate_equivalence_pointwise (l : list Type) : + Morphism (@predicate_equivalence l ==> lift_pointwise l iff) id. +Proof. do 2 red. unfold predicate_equivalence. auto. Qed. + +Lemma predicate_implication_pointwise (l : list Type) : + Morphism (@predicate_implication l ==> lift_pointwise l impl) 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]. *) + +Instance relation_equivalence_pointwise : + Morphism (relation_equivalence ==> pointwise_relation (A:=A) (pointwise_relation (A:=A) iff)) id. +Proof. apply (predicate_equivalence_pointwise (l:=(cons A (cons A nil)))). Qed. + +Instance subrelation_pointwise : + Morphism (subrelation ==> pointwise_relation (A:=A) (pointwise_relation (A:=A) impl)) id. +Proof. apply (predicate_implication_pointwise (l:=(cons A (cons A nil)))). Qed. diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index f5d3cc1c4..8dfb662b2 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -21,9 +21,6 @@ Require Import Coq.Program.Basics. Require Import Coq.Program.Tactics. Require Export Coq.Relations.Relation_Definitions. -Set Implicit Arguments. -Unset Strict Implicit. - (** Default relation on a given support. *) Class DefaultRelation A (R : relation A). @@ -50,6 +47,9 @@ Proof. reflexivity. Qed. (** We rebind relations in separate classes to be able to overload each proof. *) +Set Implicit Arguments. +Unset Strict Implicit. + Class Reflexive A (R : relation A) := reflexivity : forall x, R x x. @@ -73,6 +73,8 @@ Implicit Arguments Transitive [A]. Hint Resolve @irreflexivity : ord. +Unset Implicit Arguments. + (** We can already dualize all these properties. *) Program Instance [ Reflexive A R ] => flip_Reflexive : Reflexive (flip R) := @@ -115,12 +117,20 @@ Program Instance [ Symmetric A (R : relation A) ] => complement_Symmetric : Symm (** * Standard instances. *) +Ltac reduce_hyp H := + match type of H with + | context [ _ <-> _ ] => fail 1 + | _ => red in H ; try reduce_hyp H + end. + Ltac reduce_goal := match goal with | [ |- _ <-> _ ] => fail 1 | _ => red ; intros ; try reduce_goal end. +Tactic Notation "reduce" "in" hyp(Hid) := reduce_hyp Hid. + Ltac reduce := reduce_goal. Tactic Notation "apply" "*" constr(t) := @@ -203,52 +213,187 @@ Program Instance eq_equivalence : Equivalence A (@eq A) | 10. Program Instance iff_equivalence : Equivalence Prop iff. -(** The following is not definable. *) -(* -Program Instance [ sa : Equivalence a R, sb : Equivalence b R' ] => equiv_setoid : - Equivalence (a -> b) - (fun f g => forall (x y : a), R x y -> R' (f x) (g y)). -*) +(** 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. -(** We define the various operations which define the algebra on relations. - They are essentially liftings of the logical operations. *) +(* Notation " [ ] " := nil : list_scope. *) +(* Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) (at level 1) : list_scope. *) -Definition relation_equivalence {A : Type} : relation (relation A) := - fun (R R' : relation A) => forall x y, R x y <-> R' x y. +(* Open Local Scope list_scope. *) -Class subrelation {A:Type} (R R' : relation A) := - is_subrelation : forall x y, R x y -> R' x y. +(** A compact representation of non-dependent arities, with the codomain singled-out. *) -Implicit Arguments subrelation [[A]]. +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 relation_conjunction {A} (R : relation A) (R' : relation A) : relation A := - fun x y => R x y /\ R' x y. +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 relation_disjunction {A} (R : relation A) (R' : relation A) : relation A := - fun x y => R x y \/ R' x y. +(** We define n-ary [predicate]s as functions into [Prop]. *) -(* Infix "<R>" := relation_equivalence (at level 95, no associativity) : relation_scope. *) -(* Infix "-R>" := subrelation (at level 70) : relation_scope. *) -(* Infix "/R\" := relation_conjunction (at level 80, right associativity) : relation_scope. *) -(* Infix "\R/" := relation_disjunction (at level 85, right associativity) : relation_scope. *) +Definition predicate (l : list Type) := arrows l Prop. -(* Open Local Scope relation_scope. *) +(** Unary predicates, or sets. *) -(** Relation equivalence is an equivalence, and subrelation defines a partial order. *) +Definition unary_predicate A := predicate (cons A nil). -Program Instance relation_equivalence_equivalence : - Equivalence (relation A) relation_equivalence. +(** Homogenous binary relations, equivalent to [relation A]. *) + +Definition binary_relation A := predicate (cons A (cons A nil)). + +(** We can close a predicate by universal or existential quantification. *) + +Fixpoint predicate_all (l : list Type) : predicate l -> Prop := + match l with + | nil => fun f => f + | A :: tl => fun f => forall x : A, predicate_all tl (f x) + end. + +Fixpoint predicate_exists (l : list Type) : predicate l -> Prop := + match l with + | nil => fun f => f + | 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 + on functions whose codomain is [T]. *) + +Fixpoint pointwise_extension {l : list Type} {T : Type} + (op : binary_operation T) : binary_operation (arrows l T) := + match l with + | nil => fun R R' => op R R' + | A :: tl => fun R R' => + fun x => pointwise_extension op (R x) (R' x) + end. + +(** For an operator on [Prop] this lifts the operator to a binary operation. *) + +Definition pointwise_relation_extension (l : list Type) (op : binary_relation Prop) : + binary_operation (predicate l) := pointwise_extension op. + +(** Pointwise lifting, equivalent to doing [pointwise_extension] and closing using [predicate_all]. *) + +Fixpoint lift_pointwise (l : list Type) (op : binary_relation Prop) : binary_relation (predicate l) := + match l with + | nil => fun R R' => op R R' + | A :: tl => fun R R' => + forall x, lift_pointwise tl op (R x) (R' x) + end. + +(** The n-ary equivalence relation, defined by lifting the 0-ary [iff] relation. *) + +Definition predicate_equivalence {l : list Type} : binary_relation (predicate l) := + lift_pointwise l iff. + +(** The n-ary implication relation, defined by lifting the 0-ary [impl] relation. *) + +Definition predicate_implication {l : list Type} := + lift_pointwise l impl. + +(** 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. + +Open Local Scope predicate_scope. + +(** The pointwise liftings of conjunction and disjunctions. + Note that these are [binary_operation]s, building new relations out of old ones. *) + +Definition predicate_intersection {l : list Type} : binary_operation (predicate l) := + pointwise_relation_extension l and. + +Definition predicate_union {l : list Type} : binary_operation (predicate l) := + pointwise_relation_extension l or. + +Infix "/∙\" := predicate_intersection (at level 80, right associativity) : predicate_scope. +Infix "\∙/" := predicate_union (at level 85, right associativity) : predicate_scope. + +(** The always [True] and always [False] predicates. *) + +Fixpoint true_predicate {l : list Type} : predicate l := + match l with + | nil => True + | A :: tl => fun _ => @true_predicate tl + end. + +Fixpoint false_predicate {l : list Type} : predicate l := + match l with + | nil => False + | A :: tl => fun _ => @false_predicate tl + end. + +Notation "∙⊤∙" := true_predicate : predicate_scope. +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. Next Obligation. - Proof. - unfold relation_equivalence in *. - apply transitivity with (y x0 y0) ; [ apply H | apply H0 ]. + induction l ; firstorder. + Qed. + + Next Obligation. + induction l ; firstorder. + Qed. + + Next Obligation. + fold lift_pointwise. + induction l. firstorder. + intros. simpl in *. intro. pose (IHl (x x0) (y x0) (z x0)). + firstorder. + Qed. + +Program Instance predicate_implication_preorder : + PreOrder (predicate l) predicate_implication. + + Next Obligation. + induction l ; firstorder. Qed. -Program Instance subrelation_preorder : - PreOrder (relation A) subrelation. + Next Obligation. + fold lift_pointwise. + induction l. firstorder. + 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, + from the general ones. *) + +Definition relation_equivalence {A : Type} : relation (relation A) := + @predicate_equivalence (cons _ (cons _ nil)). + +Class subrelation {A:Type} (R R' : relation A) : Prop := + is_subrelation : @predicate_implication (cons A (cons 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'. + +Definition relation_disjunction {A} (R : relation A) (R' : relation A) : relation A := + @predicate_union (cons A (cons A nil)) R R'. + +(** Relation equivalence is an equivalence, and subrelation defines a partial order. *) + +Instance (A : Type) => relation_equivalence_equivalence : + Equivalence (relation A) relation_equivalence. +Proof. intro A. exact (@predicate_equivalence_equivalence (cons A (cons A nil))). Qed. + +Instance relation_implication_preorder : PreOrder (relation A) subrelation. +Proof. intro A. exact (@predicate_implication_preorder (cons A (cons A nil))). Qed. (** *** Partial Order. A partial order is a preorder which is additionally antisymmetric. @@ -256,8 +401,7 @@ Program Instance subrelation_preorder : on the carrier. *) Class [ equ : Equivalence A eqA, PreOrder A R ] => PartialOrder := - partial_order_equivalence : relation_equivalence eqA (relation_conjunction R (flip 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). @@ -265,8 +409,8 @@ Class [ equ : Equivalence A eqA, PreOrder A R ] => PartialOrder := Instance [ PartialOrder A eqA R ] => partial_order_antisym : ! Antisymmetric A eqA R. Proof with auto. - reduce_goal. pose partial_order_equivalence. red in r. - apply <- r. firstorder. + reduce_goal. pose partial_order_equivalence as poe. do 3 red in poe. + apply <- poe. firstorder. Qed. (** The partial order defined by subrelation and relation equivalence. *) @@ -279,8 +423,6 @@ Program Instance subrelation_partial_order : unfold relation_equivalence in *. firstorder. Qed. -Instance iff_impl_subrelation : subrelation iff impl. -Proof. firstorder. Qed. - -Instance iff_inverse_impl_subrelation : subrelation iff (inverse impl). -Proof. firstorder. Qed. +Lemma inverse_pointwise_relation A (R : relation A) : + relation_equivalence (pointwise_relation (inverse R)) (inverse (pointwise_relation (A:=A) R)). +Proof. reflexivity. Qed. diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v index 38bdc0bc9..9d3648fef 100644 --- a/theories/Classes/SetoidTactics.v +++ b/theories/Classes/SetoidTactics.v @@ -17,6 +17,7 @@ Require Export Coq.Classes.RelationClasses. Require Export Coq.Classes.Morphisms. +Require Export Coq.Classes.Morphisms_Prop. Require Export Coq.Classes.Equivalence. Require Export Coq.Relations.Relation_Definitions. @@ -89,6 +90,7 @@ Ltac reverse_arrows x := end. Ltac default_add_morphism_tactic := + intros ; (try destruct_morphism) ; match goal with | [ |- (?x ==> ?y) _ _ ] => red_subst_eq_morphism (x ==> y) ; reverse_arrows (x ==> y) |