Library Coq.Classes.RelationPairs

Relations over pairs

Require Import SetoidList.
Require Import Relations Morphisms.

Arguments relation_conjunction A%type (R R')%signature _ _.
Arguments relation_equivalence A%type (_ _)%signature.
Arguments subrelation A%type (R R')%signature.
Arguments Reflexive A%type R%signature.
Arguments Irreflexive A%type R%signature.
Arguments Symmetric A%type R%signature.
Arguments Transitive A%type R%signature.
Arguments PER A%type R%signature.
Arguments Equivalence A%type R%signature.
Arguments StrictOrder A%type R%signature.

Generalizable Variables A B RA RB Ri Ro f.

Any function from A to B allow to obtain a relation over A out of a relation over B.

Definition RelCompFun {A} {B : Type}(R:relation B)(f:A ->B) : relation A :=
fun a a' => R (f a) (f a').

Instances on RelCompFun must match syntactically

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.

#[global]
Instance fst_measure {A B} : @Measure (A * B) A Fst := {}.

#[global]
Instance snd_measure {A B} : @Measure (A * B) B Snd := {}.

We define a product relation over A*B: each components should satisfy the corresponding initial relation.

Definition RelProd {A : Type} {B : Type} (RA:relation A)(RB:relation B) : relation (A *B) :=
relation_conjunction (@RelCompFun (A * B) A RA fst) (RB @@2).

Infix "*" := RelProd : signature_scope.

Section RelCompFun_Instances.
  Context {A : Type} {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 Instance RelCompFun_Equivalence
    `(Measure A B f, Equivalence _ R) : Equivalence (R@@f) := {}.

  Global Instance RelCompFun_StrictOrder
    `(Measure A B f, StrictOrder _ R) : StrictOrder (R@@f) := {}.

End RelCompFun_Instances.

Section RelProd_Instances.

  Context {A : Type} {B : Type} (RA : relation A) (RB : relation B).

  Global Instance RelProd_Reflexive `(Reflexive _ RA, Reflexive _ RB) : Reflexive (RA *RB).

  Global Instance RelProd_Symmetric `(Symmetric _ RA, Symmetric _ RB)
  : Symmetric (RA *RB).

  Global Instance RelProd_Transitive
           `(Transitive _ RA, Transitive _ RB) : Transitive (RA *RB).

  Lemma FstRel_ProdRel :
    relation_equivalence (RA @@1) (RA *(fun _ _ : B => True )).

  Lemma SndRel_ProdRel :
    relation_equivalence (RB @@2) ((fun _ _ : A =>True ) * RB).

  Global Instance FstRel_sub :
    subrelation (RA *RB) (RA @@1).

  Global Instance SndRel_sub :
    subrelation (RA *RB) (RB @@2).

  Global Instance pair_compat :
    Proper (RA ==>RB ==> RA *RB) (@pair _ _).

  Global Instance fst_compat :
    Proper (RA *RB ==> RA) Fst.

  Global Instance snd_compat :
    Proper (RA *RB ==> RB) Snd.

  Global Instance RelCompFun_compat (f:A ->B)
           `(Proper _ (Ri ==>Ri ==>Ro ) RB) :
    Proper (Ri@@f ==>Ri@@f ==>Ro) (RB@@f)%signature.
End RelProd_Instances.

#[global]
Hint Unfold RelProd RelCompFun : core.
#[global]
Hint Extern 2 (RelProd _ _ _ _) => split : core.

Library Coq.Classes.RelationPairs

Relations over pairs

Navigation