(* -*- coq-prog-args: ("-emacs-U" "-nois") -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* A -> Prop) (at level 0). Definition inverse A (R : relation A) : relation A := fun x y => R y x. Lemma inverse_inverse : forall A (R : relation A), inverse (inverse R) = R. Proof. intros ; unfold inverse. apply (flip_flip R). Qed. Definition complement A (R : relation A) := fun x y => R x y -> False. (** These are convertible. *) 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 : relation A) := reflexive : forall x, R x x. Class Irreflexive A (R : relation A) := irreflexive : forall x, R x x -> False. Class Symmetric A (R : relation A) := symmetric : forall x y, R x y -> R y x. Class Asymmetric A (R : relation A) := asymmetric : forall x y, R x y -> R y x -> False. Class Transitive A (R : relation 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 ; apply 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. apply H. apply reflexive. Qed. Program Instance [ Irreflexive A (R : relation A) ] => irreflexive_complement_reflexive : Reflexive A (complement R). Next Obligation. Proof. red ; intros. apply (irreflexive H). Qed. Program Instance [ Symmetric A (R : relation A) ] => complement_symmetric : Symmetric A (complement R). Next Obligation. Proof. red ; intros H'. apply (H (symmetric H')). Qed. (** * Standard instances. *) Ltac simpl_relation := try red ; unfold inverse, flip, impl, arrow ; program_simpl ; try tauto ; repeat (red ; intros) ; try ( solve [ intuition ]). Ltac obligations_tactic ::= simpl_relation. (** Logical implication. *) Program Instance impl_refl : ? Reflexive impl. Program Instance impl_trans : ? Transitive impl. (** Logical equivalence. *) Program Instance iff_refl : ? Reflexive iff. Program Instance iff_sym : ? Symmetric iff. Program Instance iff_trans : ? Transitive iff. (** Leibniz equality. *) Program Instance eq_refl : ? Reflexive (@eq A). Program Instance eq_sym : ? Symmetric (@eq A). Program Instance eq_trans : ? Transitive (@eq A). (** ** General tactics to solve goals on relations. 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 : relation A) : relation 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') | [ H : ?R ?A ?B ?C ?D ?E ?X ?Y, H' : ?R ?A ?B ?C ?D ?E ?Y ?Z |- ?R ?A ?B ?C ?D ?E ?X ?Z ] => apply (transitive (R:=R A B C D E) (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. (** The [PER] typeclass. *) Class PER (carrier : Type) (pequiv : relation 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 : relation 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 : relation 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 inverse, flip ; program_simpl ; eapply @antisymmetric ; eauto. Program Instance [ eq : Equivalence A eqA, ? Antisymmetric eq (R : relation A) ] => inverse_antisymmetric : ? Antisymmetric eq (inverse R). Solve Obligations using unfold inverse, flip ; program_simpl ; eapply @antisymmetric ; eauto. (** 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)). *)