# Library Coq.Classes.RelationPairs

# Relations over pairs

Require Import Relations Morphisms.
Local Notation Fst := (@fst _ _).
Local Notation Snd := (@snd _ _).
Any function from A to B allow to obtain a relation over A out of a relation over B.
Definition RelCompFun {A B}(R:relation B)(f:A->B) : relation A :=
fun a a' => R (f a) (f a').
Infix "@@" := RelCompFun (at level 30, right associativity) : signature_scope.
Notation "R @@1" := (R @@ Fst)%signature (at level 30) : signature_scope.
Notation "R @@2" := (R @@ Snd)%signature (at level 30) : signature_scope.
We declare measures to the system using the Measure class. Otherwise the instances would easily introduce loops, never instantiating the f function.
Class Measure {A B} (f : A -> B).
Standard measures.
Instance fst_measure : @Measure (A * B) A Fst.
Instance snd_measure : @Measure (A * B) B Snd.
We define a product relation over A*B: each components should satisfy the corresponding initial relation.
Definition RelProd {A B}(RA:relation A)(RB:relation B) : relation (A * B) :=
relation_conjunction (RA @@1) (RB @@2).
Infix "*" := RelProd : signature_scope.
Section RelCompFun_Instances.
Context {A B : Type} (R : relation B).
Global Instance RelCompFun_Reflexive
`(Measure A B f, Reflexive _ R) : Reflexive (R@@f).
Global Instance RelCompFun_Symmetric
`(Measure A B f, Symmetric _ R) : Symmetric (R@@f).
Global Instance RelCompFun_Transitive
`(Measure A B f, Transitive _ R) : Transitive (R@@f).
Global Instance RelCompFun_Irreflexive
`(Measure A B f, Irreflexive _ R) : Irreflexive (R@@f).
Global Program Instance RelCompFun_Equivalence
`(Measure A B f, Equivalence _ R) : Equivalence (R@@f).
Global Program Instance RelCompFun_StrictOrder
`(Measure A B f, StrictOrder _ R) : StrictOrder (R@@f).
End RelCompFun_Instances.
Instance RelProd_Reflexive {A B}(RA:relation A)(RB:relation B)
`(Reflexive _ RA, Reflexive _ RB) : Reflexive (RA * RB).
Instance RelProd_Symmetric {A B}(RA:relation A)(RB:relation B)
`(Symmetric _ RA, Symmetric _ RB) : Symmetric (RA * RB).
Instance RelProd_Transitive {A B}(RA:relation A)(RB:relation B)
`(Transitive _ RA, Transitive _ RB) : Transitive (RA * RB).
Program Instance RelProd_Equivalence {A B}(RA:relation A)(RB:relation B)
`(Equivalence _ RA, Equivalence _ RB) : Equivalence (RA * RB).
Lemma FstRel_ProdRel {A B}(RA:relation A) :
relation_equivalence (RA @@1) (RA *( fun _ _ : B => True )).
Lemma SndRel_ProdRel {A B}(RB:relation B) :
relation_equivalence (RB @@2) (( fun _ _ : A =>True ) * RB).
Instance FstRel_sub {A B} (RA:relation A)(RB:relation B):
subrelation (RA * RB) (RA @@1).
Instance SndRel_sub {A B} (RA:relation A)(RB:relation B):
subrelation (RA * RB) (RB @@2).
Instance pair_compat { A B } (RA:relation A)(RB:relation B) :
Proper (RA ==> RB ==> RA * RB) (@pair _ _).
Instance fst_compat { A B } (RA:relation A)(RB:relation B) :
Proper (RA * RB ==> RA) Fst.
Instance snd_compat { A B } (RA:relation A)(RB:relation B) :
Proper (RA * RB ==> RB) Snd.
Instance RelCompFun_compat {A B}(f:A->B)(R : relation B)
`(Proper _ (Ri ==> Ri ==> Ro) R) :
Proper (Ri@@f ==> Ri@@f ==> Ro) (R@@f)%signature.
Hint Unfold RelProd RelCompFun.
Hint Extern 2 (RelProd _ _ _ _) => split.