Library Stdlib.Classes.CRelationClasses
Typeclass-based relations, tactics and standard instances
Require Export Stdlib.Classes.Init.
Require Import Stdlib.Program.Basics.
Require Import Stdlib.Program.Tactics.
Generalizable Variables A B C D R S T U l eqA eqB eqC eqD.
Definition crelation (A : Type) := A -> A -> Type.
Definition arrow (A B : Type) := A -> B.
Definition flip {A B C : Type} (f : A -> B -> C) := fun x y => f y x.
Definition iffT (A B : Type) := ((A -> B) * (B -> A))%type.
Global Typeclasses Opaque flip arrow iffT.
We allow to unfold the crelation definition while doing morphism search.
We rebind crelational properties in separate classes to be able to overload each proof.
Class Reflexive (R : crelation A) :=
reflexivity : forall x : A, R x x.
Definition complement (R : crelation A) : crelation A :=
fun x y => R x y -> False.
Opaque for proof-search.
Typeclasses Opaque complement iffT.
These are convertible.
Lemma complement_inverse R : complement (flip R) = flip (complement R).
Class Irreflexive (R : crelation A) :=
irreflexivity : Reflexive (complement R).
Class Symmetric (R : crelation A) :=
symmetry : forall {x y}, R x y -> R y x.
Class Asymmetric (R : crelation A) :=
asymmetry : forall {x y}, R x y -> (complement R y x : Type).
Class Transitive (R : crelation A) :=
transitivity : forall {x y z}, R x y -> R y z -> R x z.
Class Irreflexive (R : crelation A) :=
irreflexivity : Reflexive (complement R).
Class Symmetric (R : crelation A) :=
symmetry : forall {x y}, R x y -> R y x.
Class Asymmetric (R : crelation A) :=
asymmetry : forall {x y}, R x y -> (complement R y x : Type).
Class Transitive (R : crelation A) :=
transitivity : forall {x y z}, R x y -> R y z -> R x z.
Various combinations of reflexivity, symmetry and transitivity.
A PreOrder is both Reflexive and Transitive.
Class PreOrder (R : crelation A) := {
#[global] PreOrder_Reflexive :: Reflexive R | 2 ;
#[global] PreOrder_Transitive :: Transitive R | 2 }.
A StrictOrder is both Irreflexive and Transitive.
Class StrictOrder (R : crelation A) := {
#[global] StrictOrder_Irreflexive :: Irreflexive R ;
#[global] StrictOrder_Transitive :: Transitive R }.
By definition, a strict order is also asymmetric
A partial equivalence crelation is Symmetric and Transitive.
Class PER (R : crelation A) := {
#[global] PER_Symmetric :: Symmetric R | 3 ;
#[global] PER_Transitive :: Transitive R | 3 }.
Equivalence crelations.
Class Equivalence (R : crelation A) := {
#[global] Equivalence_Reflexive :: Reflexive R ;
#[global] Equivalence_Symmetric :: Symmetric R ;
#[global] Equivalence_Transitive :: Transitive R }.
An Equivalence is a PER plus reflexivity.
Global Instance Equivalence_PER {R} `(Equivalence R) : PER R | 10 :=
{ PER_Symmetric := Equivalence_Symmetric ;
PER_Transitive := Equivalence_Transitive }.
We can now define antisymmetry w.r.t. an equivalence crelation on the carrier.
Class Antisymmetric eqA `{equ : Equivalence eqA} (R : crelation A) :=
antisymmetry : forall {x y}, R x y -> R y x -> eqA x y.
Class subrelation (R R' : crelation A) :=
is_subrelation : forall {x y}, R x y -> R' x y.
Any symmetric crelation is equal to its inverse.
Lemma subrelation_symmetric R `(Symmetric R) : subrelation (flip R) R.
Section flip.
Lemma flip_Reflexive `{Reflexive R} : Reflexive (flip R).
Program Definition flip_Irreflexive `(Irreflexive R) : Irreflexive (flip R) :=
irreflexivity (R:=R).
Program Definition flip_Symmetric `(Symmetric R) : Symmetric (flip R) :=
fun x y H => symmetry (R:=R) H.
Program Definition flip_Asymmetric `(Asymmetric R) : Asymmetric (flip R) :=
fun x y H H' => asymmetry (R:=R) H H'.
Program Definition flip_Transitive `(Transitive R) : Transitive (flip R) :=
fun x y z H H' => transitivity (R:=R) H' H.
Program Lemma flip_Antisymmetric `(Antisymmetric eqA R) :
Antisymmetric eqA (flip R).
Inversing the larger structures
Lemma flip_PreOrder `(PreOrder R) : PreOrder (flip R).
Lemma flip_StrictOrder `(StrictOrder R) : StrictOrder (flip R).
Lemma flip_PER `(PER R) : PER (flip R).
Lemma flip_Equivalence `(Equivalence R) : Equivalence (flip R).
End flip.
Section complement.
Lemma complement_Irreflexive `(Reflexive R)
: Irreflexive (complement R).
Lemma complement_Symmetric `(Symmetric R) : Symmetric (complement R).
End complement.
Rewrite crelation on a given support: declares a crelation as a rewrite
crelation for use by the generalized rewriting tactic.
It helps choosing if a rewrite should be handled
by the generalized or the regular rewriting tactic using leibniz equality.
Users can declare an RewriteRelation A RA anywhere to declare default
crelations. This is also done automatically by the Declare Relation A RA
commands.
Any Equivalence declared in the context is automatically considered
a rewrite crelation.
Leibniz equality.
Section Leibniz.
Global Instance eq_Reflexive : Reflexive (@eq A) := @eq_refl A.
Global Instance eq_Symmetric : Symmetric (@eq A) := @eq_sym A.
Global Instance eq_Transitive : Transitive (@eq A) := @eq_trans A.
Global Instance eq_Reflexive : Reflexive (@eq A) := @eq_refl A.
Global Instance eq_Symmetric : Symmetric (@eq A) := @eq_sym A.
Global Instance eq_Transitive : Transitive (@eq A) := @eq_trans A.
Leibinz equality eq is an equivalence crelation.
The instance has low priority as it is always applicable
if only the type is constrained.
Default rewrite crelations handled by setoid_rewrite.
#[global]
Instance: RewriteRelation impl.
Defined.
#[global]
Instance: RewriteRelation iff.
Defined.
Instance: RewriteRelation impl.
Defined.
#[global]
Instance: RewriteRelation iff.
Defined.
Hints to drive the typeclass resolution avoiding loops
due to the use of full unification.
#[global]
Hint Extern 1 (Reflexive (complement _)) => class_apply @irreflexivity : typeclass_instances.
#[global]
Hint Extern 3 (Symmetric (complement _)) => class_apply complement_Symmetric : typeclass_instances.
#[global]
Hint Extern 3 (Irreflexive (complement _)) => class_apply complement_Irreflexive : typeclass_instances.
#[global]
Hint Extern 3 (Reflexive (flip _)) => apply flip_Reflexive : typeclass_instances.
#[global]
Hint Extern 3 (Irreflexive (flip _)) => class_apply flip_Irreflexive : typeclass_instances.
#[global]
Hint Extern 3 (Symmetric (flip _)) => class_apply flip_Symmetric : typeclass_instances.
#[global]
Hint Extern 3 (Asymmetric (flip _)) => class_apply flip_Asymmetric : typeclass_instances.
#[global]
Hint Extern 3 (Antisymmetric (flip _)) => class_apply flip_Antisymmetric : typeclass_instances.
#[global]
Hint Extern 3 (Transitive (flip _)) => class_apply flip_Transitive : typeclass_instances.
#[global]
Hint Extern 3 (StrictOrder (flip _)) => class_apply flip_StrictOrder : typeclass_instances.
#[global]
Hint Extern 3 (PreOrder (flip _)) => class_apply flip_PreOrder : typeclass_instances.
#[global]
Hint Extern 4 (subrelation (flip _) _) =>
class_apply @subrelation_symmetric : typeclass_instances.
#[global]
Hint Resolve irreflexivity : ord.
Unset Implicit Arguments.
Ltac solve_crelation :=
match goal with
| [ |- ?R ?x ?x ] => reflexivity
| [ H : ?R ?x ?y |- ?R ?y ?x ] => symmetry ; exact H
end.
#[global]
Hint Extern 4 => solve_crelation : crelations.
Hint Extern 1 (Reflexive (complement _)) => class_apply @irreflexivity : typeclass_instances.
#[global]
Hint Extern 3 (Symmetric (complement _)) => class_apply complement_Symmetric : typeclass_instances.
#[global]
Hint Extern 3 (Irreflexive (complement _)) => class_apply complement_Irreflexive : typeclass_instances.
#[global]
Hint Extern 3 (Reflexive (flip _)) => apply flip_Reflexive : typeclass_instances.
#[global]
Hint Extern 3 (Irreflexive (flip _)) => class_apply flip_Irreflexive : typeclass_instances.
#[global]
Hint Extern 3 (Symmetric (flip _)) => class_apply flip_Symmetric : typeclass_instances.
#[global]
Hint Extern 3 (Asymmetric (flip _)) => class_apply flip_Asymmetric : typeclass_instances.
#[global]
Hint Extern 3 (Antisymmetric (flip _)) => class_apply flip_Antisymmetric : typeclass_instances.
#[global]
Hint Extern 3 (Transitive (flip _)) => class_apply flip_Transitive : typeclass_instances.
#[global]
Hint Extern 3 (StrictOrder (flip _)) => class_apply flip_StrictOrder : typeclass_instances.
#[global]
Hint Extern 3 (PreOrder (flip _)) => class_apply flip_PreOrder : typeclass_instances.
#[global]
Hint Extern 4 (subrelation (flip _) _) =>
class_apply @subrelation_symmetric : typeclass_instances.
#[global]
Hint Resolve irreflexivity : ord.
Unset Implicit Arguments.
Ltac solve_crelation :=
match goal with
| [ |- ?R ?x ?x ] => reflexivity
| [ H : ?R ?x ?y |- ?R ?y ?x ] => symmetry ; exact H
end.
#[global]
Hint Extern 4 => solve_crelation : crelations.
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_crelation :=
unfold flip, impl, arrow ; try reduce ; program_simpl ;
try ( solve [ dintuition auto with crelations ]).
Local Obligation Tactic := simpl_crelation.
Logical implication.
#[global]
Program Instance impl_Reflexive : Reflexive impl.
#[global]
Program Instance impl_Transitive : Transitive impl.
Logical equivalence.
#[global]
Instance iff_Reflexive : Reflexive iff := iff_refl.
#[global]
Instance iff_Symmetric : Symmetric iff := iff_sym.
#[global]
Instance iff_Transitive : Transitive iff := iff_trans.
Logical equivalence iff is an equivalence crelation.
#[global]
Program Instance iff_equivalence : Equivalence iff.
#[global]
Program Instance arrow_Reflexive : Reflexive arrow.
#[global]
Program Instance arrow_Transitive : Transitive arrow.
#[global]
Instance iffT_Reflexive : Reflexive iffT.
#[global]
Instance iffT_Symmetric : Symmetric iffT.
#[global]
Instance iffT_Transitive : Transitive iffT.
We now develop a generalization of results on crelations for arbitrary predicates.
The resulting theory can be applied to homogeneous binary crelations but also to
arbitrary n-ary predicates.
Local Open Scope list_scope.
A compact representation of non-dependent arities, with the codomain singled-out.
We define the various operations which define the algebra on binary crelations
Section Binary.
Context {A : Type}.
Definition relation_equivalence : crelation (crelation A) :=
fun R R' => forall x y, iffT (R x y) (R' x y).
Global Instance: RewriteRelation relation_equivalence.
Defined.
Definition relation_conjunction (R : crelation A) (R' : crelation A) : crelation A :=
fun x y => prod (R x y) (R' x y).
Definition relation_disjunction (R : crelation A) (R' : crelation A) : crelation A :=
fun x y => sum (R x y) (R' x y).
Context {A : Type}.
Definition relation_equivalence : crelation (crelation A) :=
fun R R' => forall x y, iffT (R x y) (R' x y).
Global Instance: RewriteRelation relation_equivalence.
Defined.
Definition relation_conjunction (R : crelation A) (R' : crelation A) : crelation A :=
fun x y => prod (R x y) (R' x y).
Definition relation_disjunction (R : crelation A) (R' : crelation A) : crelation A :=
fun x y => sum (R x y) (R' x y).
Relation equivalence is an equivalence, and subrelation defines a partial order.
Global Instance relation_equivalence_equivalence :
Equivalence relation_equivalence.
Global 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 crelation on the carrier.Class PartialOrder eqA `{equ : Equivalence A eqA} R `{preo : PreOrder A R} :=
partial_order_equivalence : relation_equivalence eqA (relation_conjunction R (flip 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
Global Instance partial_order_antisym `(PartialOrder eqA R) : Antisymmetric eqA R.
Lemma PartialOrder_inverse `(PartialOrder eqA R) : PartialOrder eqA (flip R).
End Binary.
#[global]
Hint Extern 3 (PartialOrder (flip _)) => class_apply PartialOrder_inverse : typeclass_instances.
The partial order defined by subrelation and crelation equivalence.
Global Typeclasses Opaque relation_equivalence.
Register arrow as rewrite.type.arrow.
Register flip as rewrite.type.flip.
Register crelation as rewrite.type.relation.
Register subrelation as rewrite.type.subrelation.
Register Reflexive as rewrite.type.Reflexive.
Register reflexivity as rewrite.type.reflexivity.
Register Symmetric as rewrite.type.Symmetric.
Register symmetry as rewrite.type.symmetry.
Register Transitive as rewrite.type.Transitive.
Register transitivity as rewrite.type.transitivity.
Register RewriteRelation as rewrite.type.RewriteRelation.