diff options
Diffstat (limited to 'theories/Classes/Relations.v')
| -rw-r--r-- | theories/Classes/Relations.v | 569 |
1 files changed, 569 insertions, 0 deletions
diff --git a/theories/Classes/Relations.v b/theories/Classes/Relations.v new file mode 100644 index 0000000000..6ecd4ac3c7 --- /dev/null +++ b/theories/Classes/Relations.v @@ -0,0 +1,569 @@ +(* -*- coq-prog-args: ("-emacs-U" "-nois") -*- *) +(************************************************************************) +(* 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 setoids, tactics and standard instances. + TODO: explain clrewrite, clsubstitute and so on. + + Author: Matthieu Sozeau + Institution: LRI, CNRS UMR 8623 - UniversitĂcopyright Paris Sud + 91405 Orsay, France *) + +(* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *) + +Require Import Coq.Program.Program. +Require Import Coq.Classes.Init. + +Set Implicit Arguments. +Unset Strict Implicit. + +Definition relationT A := A -> A -> Type. +Definition relation A := A -> A -> Prop. + +Definition inverse A (R : relation A) : relation A := flip R. + +Lemma inverse_inverse : forall A (R : relation A), inverse (inverse R) = R. +Proof. intros ; unfold inverse. apply (flip_flip R). Qed. + +Definition complementT A (R : relationT A) := fun x y => ! R x y. + +Definition complement A (R : relation A) := fun x y => ~ R x y. + +(** These are convertible. *) + +Lemma complementT_flip : forall A (R : relationT A), complementT (flip R) = flip (complementT R). +Proof. reflexivity. Qed. + +Lemma complement_inverse : forall A (R : relation A), complement (inverse R) = inverse (complement R). +Proof. reflexivity. Qed. + +(** We rebind relations in separate classes to be able to overload each proof. *) + +Class Reflexive A (R : relationT A) := + reflexive : forall x, R x x. + +Class Irreflexive A (R : relationT A) := + irreflexive : forall x, R x x -> False. + +Class Symmetric A (R : relationT A) := + symmetric : forall x y, R x y -> R y x. + +Class Asymmetric A (R : relationT A) := + asymmetric : forall x y, R x y -> R y x -> False. + +Class Transitive A (R : relationT A) := + transitive : forall x y z, R x y -> R y z -> R x z. + +Implicit Arguments Reflexive [A]. +Implicit Arguments Irreflexive [A]. +Implicit Arguments Symmetric [A]. +Implicit Arguments Asymmetric [A]. +Implicit Arguments Transitive [A]. + +Hint Resolve @irreflexive : ord. + +(** We can already dualize all these properties. *) + +Program Instance [ Reflexive A R ] => flip_reflexive : Reflexive A (flip R) := + reflexive := reflexive (R:=R). + +Program Instance [ Irreflexive A R ] => flip_irreflexive : Irreflexive A (flip R) := + irreflexive := irreflexive (R:=R). + +Program Instance [ Symmetric A R ] => flip_symmetric : Symmetric A (flip R). + + Solve Obligations using unfold flip ; program_simpl ; eapply symmetric ; eauto. + +Program Instance [ Asymmetric A R ] => flip_asymmetric : Asymmetric A (flip R). + + Solve Obligations using program_simpl ; unfold flip in * ; intros ; eapply asymmetric ; eauto. + +Program Instance [ Transitive A R ] => flip_transitive : Transitive A (flip R). + + Solve Obligations using unfold flip ; program_simpl ; eapply transitive ; eauto. + +(** Have to do it again for Prop. *) + +Program Instance [ Reflexive A (R : relation A) ] => inverse_reflexive : Reflexive A (inverse R) := + reflexive := reflexive (R:=R). + +Program Instance [ Irreflexive A (R : relation A) ] => inverse_irreflexive : Irreflexive A (inverse R) := + irreflexive := irreflexive (R:=R). + +Program Instance [ Symmetric A (R : relation A) ] => inverse_symmetric : Symmetric A (inverse R). + + Solve Obligations using unfold inverse, flip ; program_simpl ; eapply symmetric ; eauto. + +Program Instance [ Asymmetric A (R : relation A) ] => inverse_asymmetric : Asymmetric A (inverse R). + + Solve Obligations using program_simpl ; unfold inverse, flip in * ; intros ; eapply asymmetric ; eauto. + +Program Instance [ Transitive A (R : relation A) ] => inverse_transitive : Transitive A (inverse R). + + Solve Obligations using unfold inverse, flip ; program_simpl ; eapply transitive ; eauto. + +Program Instance [ Reflexive A (R : relation A) ] => + reflexive_complement_irreflexive : Irreflexive A (complement R). + + Next Obligation. + Proof. + unfold complement in * ; intros. + apply H. + apply reflexive. + Qed. + +Program Instance [ Irreflexive A (R : relation A) ] => + irreflexive_complement_reflexive : Reflexive A (complement R). + + Next Obligation. + Proof. + unfold complement in * ; intros. + red ; intros. + apply (irreflexive H). + Qed. + +Program Instance [ Symmetric A (R : relation A) ] => complement_symmetric : Symmetric A (complement R). + + Next Obligation. + Proof. + unfold complement in *. + red ; intros H'. + apply (H (symmetric H')). + Qed. + +(** Tactics to solve goals. Each tactic comes in two flavors: + - a tactic to immediately solve a goal without user intervention + - a tactic taking input from the user to make progress on a goal *) + +Definition relate A (R : relationT A) : relationT A := R. + +Ltac relationify_relation R R' := + match goal with + | [ H : context [ R ?x ?y ] |- _ ] => change (R x y) with (R' x y) in H + | [ |- context [ R ?x ?y ] ] => change (R x y) with (R' x y) + end. + +Ltac relationify R := + set (R' := relate R) ; progress (repeat (relationify_relation R R')). + +Ltac relation_refl := + match goal with + | [ |- ?R ?X ?X ] => apply (reflexive (R:=R) X) + | [ H : ?R ?X ?X |- _ ] => apply (irreflexive (R:=R) H) + + | [ |- ?R ?A ?X ?X ] => apply (reflexive (R:=R A) X) + | [ H : ?R ?A ?X ?X |- _ ] => apply (irreflexive (R:=R A) H) + + | [ |- ?R ?A ?B ?X ?X ] => apply (reflexive (R:=R A B) X) + | [ H : ?R ?A ?B ?X ?X |- _ ] => apply (irreflexive (R:=R A B) H) + + | [ |- ?R ?A ?B ?C ?X ?X ] => apply (reflexive (R:=R A B C) X) + | [ H : ?R ?A ?B ?C ?X ?X |- _ ] => apply (irreflexive (R:=R A B C) H) + + | [ |- ?R ?A ?B ?C ?D ?X ?X ] => apply (reflexive (R:=R A B C D) X) + | [ H : ?R ?A ?B ?C ?D ?X ?X |- _ ] => apply (irreflexive (R:=R A B C D) H) + end. + +Ltac refl := relation_refl. + +Ltac relation_sym := + match goal with + | [ H : ?R ?X ?Y |- ?R ?Y ?X ] => apply (symmetric (R:=R) (x:=X) (y:=Y) H) + + | [ H : ?R ?A ?X ?Y |- ?R ?A ?Y ?X ] => apply (symmetric (R:=R A) (x:=X) (y:=Y) H) + + | [ H : ?R ?A ?B ?X ?Y |- ?R ?A ?B ?Y ?X ] => apply (symmetric (R:=R A B) (x:=X) (y:=Y) H) + + | [ H : ?R ?A ?B ?C ?X ?Y |- ?R ?A ?B ?C ?Y ?X ] => apply (symmetric (R:=R A B C) (x:=X) (y:=Y) H) + + | [ H : ?R ?A ?B ?C ?D ?X ?Y |- ?R ?A ?B ?C ?D ?Y ?X ] => apply (symmetric (R:=R A B C D) (x:=X) (y:=Y) H) + + end. + +Ltac relation_symmetric := + match goal with + | [ |- ?R ?Y ?X ] => apply (symmetric (R:=R) (x:=X) (y:=Y)) + + | [ |- ?R ?A ?Y ?X ] => apply (symmetric (R:=R A) (x:=X) (y:=Y)) + + | [ |- ?R ?A ?B ?Y ?X ] => apply (symmetric (R:=R A B) (x:=X) (y:=Y)) + + | [ |- ?R ?A ?B ?C ?Y ?X ] => apply (symmetric (R:=R A B C) (x:=X) (y:=Y)) + + | [ |- ?R ?A ?B ?C ?D ?Y ?X ] => apply (symmetric (R:=R A B C D) (x:=X) (y:=Y)) + end. + +Ltac sym := relation_symmetric. + +Ltac relation_trans := + match goal with + | [ H : ?R ?X ?Y, H' : ?R ?Y ?Z |- ?R ?X ?Z ] => + apply (transitive (R:=R) (x:=X) (y:=Y) (z:=Z) H H') + + | [ H : ?R ?A ?X ?Y, H' : ?R ?A ?Y ?Z |- ?R ?A ?X ?Z ] => + apply (transitive (R:=R A) (x:=X) (y:=Y) (z:=Z) H H') + + | [ H : ?R ?A ?B ?X ?Y, H' : ?R ?A ?B ?Y ?Z |- ?R ?A ?B ?X ?Z ] => + apply (transitive (R:=R A B) (x:=X) (y:=Y) (z:=Z) H H') + + | [ H : ?R ?A ?B ?C ?X ?Y, H' : ?R ?A ?B ?C ?Y ?Z |- ?R ?A ?B ?C ?X ?Z ] => + apply (transitive (R:=R A B C) (x:=X) (y:=Y) (z:=Z) H H') + + | [ H : ?R ?A ?B ?C ?D ?X ?Y, H' : ?R ?A ?B ?C ?D ?Y ?Z |- ?R ?A ?B ?C ?D ?X ?Z ] => + apply (transitive (R:=R A B C D) (x:=X) (y:=Y) (z:=Z) H H') + end. + +Ltac relation_transitive Y := + match goal with + | [ |- ?R ?X ?Z ] => + apply (transitive (R:=R) (x:=X) (y:=Y) (z:=Z)) + + | [ |- ?R ?A ?X ?Z ] => + apply (transitive (R:=R A) (x:=X) (y:=Y) (z:=Z)) + + | [ |- ?R ?A ?B ?X ?Z ] => + apply (transitive (R:=R A B) (x:=X) (y:=Y) (z:=Z)) + + | [ |- ?R ?A ?B ?C ?X ?Z ] => + apply (transitive (R:=R A B C) (x:=X) (y:=Y) (z:=Z)) + + | [ |- ?R ?A ?B ?C ?D ?X ?Z ] => + apply (transitive (R:=R A B C D) (x:=X) (y:=Y) (z:=Z)) + end. + +Ltac trans Y := relation_transitive Y. + +(** To immediatly solve a goal on setoid equality. *) + +Ltac relation_tac := relation_refl || relation_sym || relation_trans. + +(** * Morphisms. + + We now turn to the definition of [Morphism] and declare standard instances. + These will be used by the [clrewrite] tactic later. *) + +(** Respectful morphisms. *) + +Definition respectful_depT (A : Type) (R : relationT A) + (B : A -> Type) (R' : forall x y, B x -> B y -> Type) : relationT (forall x : A, B x) := + fun f g => forall x y : A, R x y -> R' x y (f x) (g y). + +Definition respectfulT A (eqa : relationT A) B (eqb : relationT B) : relationT (A -> B) := + Eval compute in (respectful_depT eqa (fun _ _ => eqb)). + +Definition respectful A (R : relation A) B (R' : relation B) : relation (A -> B) := + fun f g => forall x y : A, R x y -> R' (f x) (g y). + +(** Notations reminiscent of the old syntax for declaring morphisms. + We use three + or - for type morphisms, and two for [Prop] ones. + *) + +Notation " R +++> R' " := (@respectfulT _ R _ R') (right associativity, at level 20). +Notation " R ---> R' " := (@respectfulT _ (flip R) _ R') (right associativity, at level 20). + +Notation " R ++> R' " := (@respectful _ R _ R') (right associativity, at level 20). +Notation " R --> R' " := (@respectful _ (inverse R) _ R') (right associativity, at level 20). + +(** 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 : relationT A) (m : A) := + respect : R m m. + +Ltac simpl_morphism := + try red ; unfold inverse, flip, impl, arrow ; program_simpl ; try tauto ; + try (red ; intros) ; try ( solve [ intuition ]). + +Ltac obligations_tactic ::= simpl_morphism. + +(** The arrow is a reflexive and transitive relation on types. *) + +Program Instance arrow_refl : ? Reflexive arrow := + reflexive X := id. + +Program Instance arrow_trans : ? Transitive arrow := + transitive X Y Z f g := g o f. + +(** Can't use the definition [notT] as it gives a to universe inconsistency. *) + +Program Instance notT_arrow_morphism : + Morphism (Type -> Type) (arrow ---> arrow) (fun X : Type => X -> False). + +(** Isomorphism. *) + +Definition iso (A B : Type) := + A -> B * B -> A. + +Program Instance iso_refl : ? Reflexive iso. +Program Instance iso_sym : ? Symmetric iso. +Program Instance iso_trans : ? Transitive iso. + +Program Instance not_iso_morphism : + Morphism (Type -> Type) (iso +++> iso) (fun X : Type => X -> False). + +(** Logical implication. *) + +Program Instance impl_refl : ? Reflexive impl. +Program Instance impl_trans : ? Transitive impl. + +Program Instance not_impl_morphism : + Morphism (Prop -> Prop) (impl --> impl) not. + +(** Logical equivalence. *) + +Program Instance iff_refl : ? Reflexive iff. +Program Instance iff_sym : ? Symmetric iff. +Program Instance iff_trans : ? Transitive iff. + +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]. + +(** If you have a morphism from [RA] to [RB] you have a contravariant morphism + from [RA] to [inverse RB]. *) + +Program Instance `A` (RA : relation A) `B` (RB : relation B) [ ? Morphism (RA ++> RB) m ] => + morph_impl_co_contra_inverse : + ? Morphism (RA --> inverse RB) m. + + Next Obligation. + Proof. + apply respect. + apply H. + Qed. + +(** Every transitive relation gives rise to a binary morphism on [impl], + contravariant in the first argument, covariant in the second. *) + +Program Instance [ Transitive A (R : relation A) ] => + trans_contra_co_morphism : ? Morphism (R --> R ++> impl) R. + + Next Obligation. + Proof with auto. + trans x... + trans x0... + Qed. + +(** Dually... *) + +Program Instance [ Transitive A (R : relation A) ] => + trans_co_contra_inv_impl_morphism : ? Morphism (R ++> R --> inverse impl) R. + + Obligations Tactic := idtac. + + Next Obligation. + Proof with auto. + intros. + destruct (trans_contra_co_morphism (R:=inverse R)). + revert respect0. + unfold respectful, inverse, flip in * ; intros. + apply respect0 ; auto. + Qed. + +Obligations Tactic := simpl_morphism. + +(** With symmetric relations, variance is no issue ! *) + +Program Instance [ Symmetric A (R : relation A) ] B (R' : relation B) + [ Morphism _ (R ++> R') m ] => + sym_contra_morphism : ? Morphism (R --> R') m. + + Next Obligation. + Proof with auto. + apply respect. + sym... + Qed. + +(** Every symmetric and transitive relation gives rise to an equivariant morphism. *) + +Program Instance [ Transitive A (R : relation A), Symmetric A R ] => + trans_sym_morphism : ? Morphism (R ++> R ++> iff) R. + + Next Obligation. + Proof with auto. + split ; intros. + trans x0... trans x... sym... + + trans y... trans y0... sym... + Qed. + +(** The complement of a relation conserves its morphisms. *) + +Program Instance `A` (RA : relation A) [ ? Morphism (RA ++> RA ++> iff) R ] => + complement_morphism : ? Morphism (RA ++> RA ++> iff) (complement R). + + Next Obligation. + Proof. + red ; unfold complement ; intros. + pose (respect). + pose (r x y H). + pose (r0 x0 y0 H0). + intuition. + Qed. + +(** The inverse too. *) + +Program Instance `A` (RA : relation A) [ ? Morphism (RA ++> RA ++> iff) R ] => + inverse_morphism : ? Morphism (RA ++> RA ++> iff) (inverse R). + + Next Obligation. + Proof. + unfold inverse ; unfold flip. + apply respect ; auto. + 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. + +(** Any binary morphism respecting some relations up to [iff] respects + them up to [impl] in each way. Very important instances as we need [impl] + morphisms at the top level when we rewrite. *) + +Program Instance `A` (R : relation A) `B` (R' : relation B) + [ ? Morphism (R ++> R' ++> iff) m ] => + iff_impl_binary_morphism : ? Morphism (R ++> R' ++> impl) m. + + Next Obligation. + Proof. + destruct respect with x y x0 y0 ; auto. + Qed. + +Program Instance `A` (R : relation A) `B` (R' : relation B) + [ ? Morphism (R ++> R' ++> iff) m ] => + iff_inverse_impl_binary_morphism : ? Morphism (R ++> R' ++> inverse impl) m. + + Next Obligation. + Proof. + destruct respect with x y x0 y0 ; auto. + Qed. + +(** 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_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_iff_morphism : ? Morphism (iff ++> iff ++> iff) or. + +(** Leibniz equality. *) + +Program Instance eq_refl : ? Reflexive (@eq A). +Program Instance eq_sym : ? Symmetric (@eq A). +Program Instance eq_trans : ? Transitive (@eq A). + +Program Definition eq_morphism A : Morphism (eq ++> eq ++> iff) (eq (A:=A)) := + trans_sym_morphism. + +Program Instance `A B` (m : A -> B) => arrow_morphism : ? Morphism (eq ++> eq) m. + +(** The [PER] typeclass. *) + +Class PER (carrier : Type) (pequiv : relationT carrier) := + per_sym :> Symmetric pequiv ; + per_trans :> Transitive pequiv. + +(** We can build a PER on the coq function space if we have PERs on the domain and + codomain. *) + +Program Instance [ PER A (R : relation A), PER B (R' : relation B) ] => + arrow_per : PER (A -> B) + (fun f g => forall (x y : A), R x y -> R' (f x) (g y)). + + Next Obligation. + Proof with auto. + constructor ; intros... + assert(R x0 x0) by (trans y0 ; [ auto | sym ; auto ]). + trans (y x0)... + Qed. + +(** The [Equivalence] typeclass. *) + +Class Equivalence (carrier : Type) (equiv : relationT carrier) := + equiv_refl :> Reflexive equiv ; + equiv_sym :> Symmetric equiv ; + equiv_trans :> Transitive equiv. + +(** We can now define antisymmetry w.r.t. an equivalence relation on the carrier. *) + +Class [ Equivalence A eqA ] => Antisymmetric (R : relationT A) := + antisymmetric : forall x y, R x y -> R y x -> eqA x y. + +Program Instance [ eq : Equivalence A eqA, ? Antisymmetric eq R ] => + flip_antisymmetric : ? Antisymmetric eq (flip R). + + Solve Obligations using unfold flip ; program_simpl ; eapply antisymmetric ; eauto. + +(** 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 : relation A), Equivalence B (R' : relation B) ] => + respecting_equiv : Equivalence respecting + (fun (f g : respecting) => forall (x y : A), R x y -> R' (`f x) (`g y)). + + Next Obligation. + Proof. + constructor ; intros. + destruct x ; simpl. + apply r ; auto. + Qed. + + Next Obligation. + Proof. + constructor ; intros. + sym ; apply H. + sym ; auto. + Qed. + + Next Obligation. + Proof. + constructor ; intros. + trans ((`y) y0). + apply H ; auto. + apply H0. refl. + Qed. + +(** Leibinz equality [eq] is an equivalence relation. *) + +Program Instance eq_equivalence : Equivalence A eq. + +(** Logical equivalence [iff] is an equivalence relation. *) + +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)). +*) |