Library Coq.Classes.RelationClasses
Require Export Coq.Classes.Init.
Require Import Coq.Program.Basics.
Require Import Coq.Program.Tactics.
Require Export Coq.Relations.Relation_Definitions.
We allow to unfold the relation definition while doing morphism search.
Notation inverse R := (flip (R:relation _) : relation _).
Definition complement {A} (R : relation A) : relation A := fun x y => R x y -> False.
Opaque for proof-search.
These are convertible.
Lemma complement_inverse : forall A (R : relation A), complement (inverse R) = inverse (complement R).
We rebind relations in separate classes to be able to overload each proof.
Class Reflexive {A} (R : relation A) :=
reflexivity : forall x, R x x.
Class Irreflexive {A} (R : relation A) :=
irreflexivity :> Reflexive (complement R).
Class Symmetric {A} (R : relation A) :=
symmetry : forall x y, R x y -> R y x.
Class Asymmetric {A} (R : relation A) :=
asymmetry : forall x y, R x y -> R y x -> False.
Class Transitive {A} (R : relation A) :=
transitivity : forall x y z, R x y -> R y z -> R x z.
Hint Resolve @irreflexivity : ord.
A HintDb for relations.
Ltac solve_relation :=
match goal with
| [ |- ?R ?x ?x ] => reflexivity
| [ H : ?R ?x ?y |- ?R ?y ?x ] => symmetry ; exact H
end.
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).
Program Instance flip_Irreflexive `(Irreflexive A R) : Irreflexive (flip R) :=
irreflexivity (R:=R).
Program Instance flip_Symmetric `(Symmetric A R) : Symmetric (flip R).
Solve Obligations using unfold flip ; intros ; tcapp symmetry ; assumption.
Program Instance flip_Asymmetric `(Asymmetric A R) : Asymmetric (flip R).
Solve Obligations using program_simpl ; unfold flip in * ; intros ; typeclass_app asymmetry ; eauto.
Program Instance flip_Transitive `(Transitive A R) : Transitive (flip R).
Solve Obligations using unfold flip ; program_simpl ; typeclass_app transitivity ; eauto.
Program Instance Reflexive_complement_Irreflexive `(Reflexive A (R : relation A))
: Irreflexive (complement R).
Next Obligation.
Program Instance complement_Symmetric `(Symmetric A (R : relation A)) : Symmetric (complement R).
Next Obligation.
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) :=
first [ refine t | refine (t _) | refine (t _ _) | refine (t _ _ _) | refine (t _ _ _ _) |
refine (t _ _ _ _ _) | refine (t _ _ _ _ _ _) | refine (t _ _ _ _ _ _ _) ].
Ltac simpl_relation :=
unfold flip, impl, arrow ; try reduce ; program_simpl ;
try ( solve [ intuition ]).
Ltac obligation_tactic ::= simpl_relation.
Logical implication.
Program Instance impl_Reflexive : Reflexive impl.
Program Instance impl_Transitive : Transitive impl.
Logical equivalence.
Program Instance iff_Reflexive : Reflexive iff.
Program Instance iff_Symmetric : Symmetric iff.
Program Instance iff_Transitive : Transitive iff.
Leibniz equality.
Program Instance eq_Reflexive : Reflexive (@eq A).
Program Instance eq_Symmetric : Symmetric (@eq A).
Program Instance eq_Transitive : Transitive (@eq A).
Various combinations of reflexivity, symmetry and transitivity.
A PreOrder is both Reflexive and Transitive.
Class PreOrder {A} (R : relation A) : Prop := {
PreOrder_Reflexive :> Reflexive R ;
PreOrder_Transitive :> Transitive R }.
A partial equivalence relation is Symmetric and Transitive.
Class PER {A} (R : relation A) : Prop := {
PER_Symmetric :> Symmetric R ;
PER_Transitive :> Transitive R }.
Equivalence relations.
Class Equivalence {A} (R : relation A) : Prop := {
Equivalence_Reflexive :> Reflexive R ;
Equivalence_Symmetric :> Symmetric R ;
Equivalence_Transitive :> Transitive R }.
An Equivalence is a PER plus reflexivity.
Instance Equivalence_PER `(Equivalence A R) : PER R | 10 :=
{ PER_Symmetric := Equivalence_Symmetric ;
PER_Transitive := Equivalence_Transitive }.
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.
Program Instance flip_antiSymmetric `(Antisymmetric A eqA R) :
! Antisymmetric A eqA (flip R).
Leibinz equality eq is an equivalence relation.
The instance has low priority as it is always applicable
if only the type is constrained.
Logical equivalence iff is an equivalence relation.
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.
A compact representation of non-dependent arities, with the codomain singled-out.
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.
We define n-ary predicates as functions into Prop.
Unary predicates, or sets.
Homogeneous binary relations, equivalent to relation A.
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.
For an operator on Prop this lifts the operator to a binary operation.
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' =>
fun x => pointwise_extension op tl (R x) (R' x)
end.
Pointwise lifting, equivalent to doing pointwise_extension and closing using predicate_all.
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' =>
forall x, pointwise_lifting op tl (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) :=
pointwise_lifting iff l.
The n-ary implication relation, defined by lifting the 0-ary impl relation.
Notations for pointwise equivalence and implication of predicates.
Infix "<∙>" := predicate_equivalence (at level 95, no associativity) : predicate_scope.
Infix "-∙>" := predicate_implication (at level 70, right associativity) : predicate_scope.
Open Local Scope predicate_scope.
The pointwise liftings of conjunction and disjunctions.
Note that these are binary_operations, building new relations out of old ones.
Definition predicate_intersection := pointwise_extension and.
Definition predicate_union := pointwise_extension 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_equivalence l).
Next Obligation.
Next Obligation.
Next Obligation.
Program Instance predicate_implication_preorder :
PreOrder (@predicate_implication l).
Next Obligation.
Next Obligation.
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 relation_equivalence_equivalence (A : Type) :
Equivalence (@relation_equivalence A).
Instance relation_implication_preorder : PreOrder (@subrelation A).
Partial Order.
A partial order is a preorder which is additionally antisymmetric. 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
for equivalence (see Morphisms).
It is also sufficient to show that R is antisymmetric w.r.t. eqA
The partial order defined by subrelation and relation equivalence.
Program Instance subrelation_partial_order :
! PartialOrder (relation A) relation_equivalence subrelation.
Next Obligation.
Typeclasses Opaque arrows predicate_implication predicate_equivalence
relation_equivalence pointwise_lifting.