diff options
Diffstat (limited to 'theories/Classes/Morphisms.v')
| -rw-r--r-- | theories/Classes/Morphisms.v | 467 |
1 files changed, 467 insertions, 0 deletions
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v new file mode 100644 index 00000000..f21c68a6 --- /dev/null +++ b/theories/Classes/Morphisms.v @@ -0,0 +1,467 @@ +(* -*- 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 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* Typeclass-based morphism definition and standard, minimal instances. + + Author: Matthieu Sozeau + Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud + 91405 Orsay, France *) + +(* $Id: Morphisms.v 11092 2008-06-10 18:28:26Z msozeau $ *) + +Require Import Coq.Program.Basics. +Require Import Coq.Program.Tactics. +Require Import Coq.Relations.Relation_Definitions. +Require Export Coq.Classes.RelationClasses. + +Set Implicit Arguments. +Unset Strict Implicit. + +(** * Morphisms. + + We now turn to the definition of [Morphism] and declare standard instances. + 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. *) + +Class Morphism A (R : relation A) (m : A) : Prop := + respect : R m m. + +(** We make the type implicit, it can be infered from the relations. *) + +Implicit Arguments Morphism [A]. + +(** We allow to unfold the [relation] definition while doing morphism search. *) + +Typeclasses unfold relation. + +(** 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 := + 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. *) + +Definition respectful (A B : Type) + (R : relation A) (R' : relation B) : relation (A -> B) := + Eval compute in @respectful_hetero A A (fun _ => B) (fun _ => B) R (fun _ _ => R'). + +(** Notations reminiscent of the old syntax for declaring morphisms. *) + +Delimit Scope signature_scope with signature. +Arguments Scope Morphism [type_scope signature_scope]. + +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. + +Arguments Scope respectful [type_scope type_scope signature_scope signature_scope]. + +Open Local Scope signature_scope. + +(** We can build a PER on the Coq function space if we have PERs on the domain and + codomain. *) + +Program Instance respectful_per [ PER A (R : relation A), PER B (R' : relation B) ] : + PER (A -> B) (R ==> R'). + + Next Obligation. + Proof with auto. + assert(R x0 x0). + transitivity y0... symmetry... + transitivity (y x0)... + Qed. + +(** Subrelations induce a morphism on the identity, not used for morphism search yet. *) + +Lemma subrelation_id_morphism [ subrelation A R₁ R₂ ] : Morphism (R₁ ==> R₂) id. +Proof. firstorder. Qed. + +(** The subrelation property goes through products as usual. *) + +Instance morphisms_subrelation [ sub : subrelation A R₁ R₂ ] : + ! subrelation (B -> A) (R ==> R₁) (R ==> R₂). +Proof. firstorder. Qed. + +Instance morphisms_subrelation_left [ sub : subrelation A R₂ R₁ ] : + ! subrelation (A -> B) (R₁ ==> R) (R₂ ==> R) | 3. +Proof. firstorder. Qed. + +(** [Morphism] is itself a covariant morphism for [subrelation]. *) + +Lemma subrelation_morphism [ sub : subrelation A R₁ R₂, mor : Morphism A R₁ m ] : Morphism 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. + +Ltac subrelation_tac := + match goal with + | [ _ : subrelation_done |- _ ] => fail 1 + | [ |- @Morphism _ _ _ ] => let H := fresh "H" in + set(H:=did_subrelation) ; eapply @subrelation_morphism + end. + +Hint Extern 4 (@Morphism _ _ _) => subrelation_tac : typeclass_instances. + +(** Essential subrelation instances for [iff], [impl] and [pointwise_relation]. *) + +Instance iff_impl_subrelation : subrelation iff impl. +Proof. firstorder. Qed. + +Instance iff_inverse_impl_subrelation : subrelation iff (inverse impl). +Proof. firstorder. Qed. + +Instance pointwise_subrelation [ sub : subrelation A R R' ] : + subrelation (pointwise_relation (A:=B) R) (pointwise_relation R') | 4. +Proof. reduce. unfold pointwise_relation in *. apply sub. apply H. Qed. + +(** The complement of a relation conserves its morphisms. *) + +Program Instance complement_morphism + [ mR : Morphism (A -> A -> Prop) (RA ==> RA ==> iff) R ] : + Morphism (RA ==> RA ==> iff) (complement R). + + Next Obligation. + Proof. + unfold complement. + pose (mR x y H x0 y0 H0). + intuition. + Qed. + +(** 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). + + Next Obligation. + Proof. + apply mor ; auto. + Qed. + +(** 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. + + Next Obligation. + Proof with auto. + transitivity x... + transitivity x0... + Qed. + +(* (** Dually... *) *) + +(* Program Instance [ Transitive A R ] => *) +(* trans_co_contra_inv_impl_morphism : Morphism (R ++> R --> inverse impl) R. *) + +(* Next Obligation. *) +(* Proof with auto. *) +(* apply* trans_contra_co_morphism ; eauto. eauto. *) +(* Qed. *) + +(** Morphism declarations for partial applications. *) + +Program Instance trans_contra_inv_impl_morphism + [ Transitive A R ] : Morphism (R --> inverse impl) (R x). + + Next Obligation. + Proof with auto. + transitivity y... + Qed. + +Program Instance trans_co_impl_morphism + [ Transitive A R ] : Morphism (R ==> impl) (R x). + + Next Obligation. + Proof with auto. + transitivity x0... + Qed. + +Program Instance trans_sym_co_inv_impl_morphism + [ Transitive A R, Symmetric A R ] : Morphism (R ==> inverse impl) (R x). + + Next Obligation. + Proof with auto. + transitivity y... + Qed. + +Program Instance trans_sym_contra_impl_morphism + [ Transitive A R, Symmetric _ R ] : Morphism (R --> impl) (R x). + + Next Obligation. + Proof with auto. + transitivity x0... + Qed. + +Program Instance equivalence_partial_app_morphism + [ Equivalence A R ] : Morphism (R ==> iff) (R x). + + Next Obligation. + Proof with auto. + split. intros ; transitivity x0... + intros. + transitivity y... + symmetry... + Qed. + +(** Every Transitive relation induces a morphism by "pushing" an [R x y] on the left of an [R x z] proof + to get an [R y z] goal. *) + +Program Instance trans_co_eq_inv_impl_morphism + [ Transitive A R ] : Morphism (R ==> (@eq A) ==> inverse impl) R. + + Next Obligation. + Proof with auto. + transitivity y... + Qed. + +(* Program Instance [ Transitive A R ] => *) +(* trans_contra_eq_impl_morphism : Morphism (R --> (@eq A) ==> impl) R. *) + +(* Next Obligation. *) +(* Proof with auto. *) +(* transitivity x... *) +(* Qed. *) + +(** Every Symmetric and Transitive relation gives rise to an equivariant morphism. *) + +Program Instance trans_sym_morphism + [ Transitive A R, Symmetric _ R ] : Morphism (R ==> R ==> iff) R. + + Next Obligation. + Proof with auto. + split ; intros. + transitivity x0... transitivity x... + + transitivity y... transitivity y0... + Qed. + +Program Instance equiv_morphism [ Equivalence A R ] : + Morphism (R ==> R ==> iff) R. + + Next Obligation. + Proof with auto. + split ; intros. + transitivity x0... transitivity x... symmetry... + + transitivity y... transitivity y0... symmetry... + Qed. + +(** In case the rewrite happens at top level. *) + +Program Instance iff_inverse_impl_id : + Morphism (iff ==> inverse impl) id. + +Program Instance inverse_iff_inverse_impl_id : + Morphism (iff --> inverse impl) id. + +Program Instance iff_impl_id : + Morphism (iff ==> impl) id. + +Program Instance inverse_iff_impl_id : + Morphism (iff --> impl) id. + +(** Coq functions are morphisms for leibniz equality, + applied only if really needed. *) + +(* Instance (A : Type) [ Reflexive B R ] => *) +(* eq_reflexive_morphism : Morphism (@Logic.eq A ==> R) m | 3. *) +(* Proof. simpl_relation. Qed. *) + +Instance reflexive_eq_dom_reflexive (A : Type) [ Reflexive B R' ] : + Reflexive (@Logic.eq A ==> R'). +Proof. simpl_relation. Qed. + +(** [respectful] is a morphism for relation equivalence. *) + +Instance respectful_morphism : + Morphism (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. + assumption. + + rewrite H0. + apply H1. + rewrite <- H. + assumption. +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 + to set different priorities in different hint bases and select a particular hint database for + resolution of a type class constraint.*) + +Class MorphismProxy A (R : relation A) (m : A) : Prop := + respect_proxy : R m m. + +Instance reflexive_morphism_proxy + [ Reflexive A R ] (x : A) : MorphismProxy A R x | 1. +Proof. firstorder. Qed. + +Instance morphism_morphism_proxy + [ Morphism A R x ] : MorphismProxy A R x | 2. +Proof. firstorder. Qed. + +(* Instance (A : Type) [ Reflexive B R ] => *) +(* eq_reflexive_morphism : Morphism (@Logic.eq A ==> R) m | 3. *) +(* Proof. simpl_relation. Qed. *) + +(** [R] is Reflexive, hence we can build the needed proof. *) + +Lemma Reflexive_partial_app_morphism [ Morphism (A -> B) (R ==> R') m, MorphismProxy A R x ] : + Morphism R' (m x). +Proof. simpl_relation. Qed. + +Ltac partial_application_tactic := + let tac x := + match type of x with + | Type => fail 1 + | _ => eapply @Reflexive_partial_app_morphism + end + in + let on_morphism m := + match m with + | ?m' ?x => tac x + | ?m' _ ?x => tac x + | ?m' _ _ ?x => tac x + | ?m' _ _ _ ?x => tac x + | ?m' _ _ _ _ ?x => tac x + | ?m' _ _ _ _ _ ?x => tac x + | ?m' _ _ _ _ _ _ ?x => tac x + | ?m' _ _ _ _ _ _ _ ?x => tac x + | ?m' _ _ _ _ _ _ _ _ ?x => tac x + end + in + match goal with + | [ |- @Morphism _ _ ?m ] => on_morphism m + end. + +(* Program Instance [ Morphism (A -> B) (R ==> R') m, Reflexive A R ] (x : A) => *) +(* reflexive_partial_app_morphism : Morphism R' (m x). *) + +Hint Extern 4 (@Morphism _ _ _) => 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'). +Proof. + intros. + unfold flip, respectful. + split ; intros ; intuition. +Qed. + +(** Special-purpose class to do normalization of signatures w.r.t. inverse. *) + +Class (A : Type) => Normalizes (m : relation A) (m' : relation A) : Prop := + normalizes : relation_equivalence m m'. + +Instance inverse_respectful_norm : + Normalizes (A -> B) (inverse R ==> inverse R') (inverse (R ==> R')) . +Proof. firstorder. Qed. + +(* If not an inverse on the left, do a double inverse. *) + +Instance not_inverse_respectful_norm : + Normalizes (A -> B) (R ==> inverse R') (inverse (inverse R ==> R')) | 4. +Proof. firstorder. Qed. + +Instance inverse_respectful_rec_norm [ Normalizes B R' (inverse R'') ] : + Normalizes (A -> B) (inverse R ==> R') (inverse (R ==> R'')). +Proof. red ; intros. + pose normalizes as r. + setoid_rewrite r. + setoid_rewrite inverse_respectful. + reflexivity. +Qed. + +(** Once we have normalized, we will apply this instance to simplify the problem. *) + +Program Instance morphism_inverse_morphism + [ Morphism A R m ] : Morphism (inverse R) m | 2. + +(** Bootstrap !!! *) + +Instance morphism_morphism : Morphism (relation_equivalence ==> @eq _ ==> iff) (@Morphism A). +Proof. + simpl_relation. + reduce in H. + split ; red ; intros. + setoid_rewrite <- H. + apply H0. + setoid_rewrite H. + apply H0. +Qed. + +Lemma morphism_releq_morphism [ Normalizes A R R', Morphism _ R' m ] : Morphism R m. +Proof. + intros. + pose respect as r. + pose normalizes as norm. + setoid_rewrite norm. + assumption. +Qed. + +Inductive normalization_done : Prop := did_normalization. + +Ltac morphism_normalization := + match goal with + | [ _ : normalization_done |- _ ] => fail 1 + | [ |- @Morphism _ _ _ ] => let H := fresh "H" in + set(H:=did_normalization) ; eapply @morphism_releq_morphism + end. + +Hint Extern 6 (@Morphism _ _ _) => morphism_normalization : typeclass_instances. + +(** Every reflexive relation gives rise to a morphism, only for immediately solving goals without variables. *) + +Lemma reflexive_morphism [ Reflexive A R ] (x : A) + : Morphism R x. +Proof. firstorder. Qed. + +Ltac morphism_reflexive := + match goal with + | [ _ : normalization_done |- _ ] => fail 1 + | [ _ : subrelation_done |- _ ] => fail 1 + | [ |- @Morphism _ _ _ ] => eapply @reflexive_morphism + end. + +Hint Extern 4 (@Morphism _ _ _) => morphism_reflexive : typeclass_instances.
\ No newline at end of file |