Require Import Relations Morphisms.


Local Notation Fst := (@fst _ _).
Local Notation Snd := (@snd _ _).

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.

Class Measure {A B} (f : A -> B).

Instance fst_measure : @Measure (A * B) A Fst.
Instance snd_measure : @Measure (A * B) B Snd.

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.