Companion.companion_rel

Applying the companion to relations

We abstract some common elements between the formalization of CCS with replication and CCS with general fixed points.

Require Import prelim companion.

Preservation of Equivalence Relations

If a function f preserves reflexivity/symmetry/transitivity, then the companion for f is always reflexive/symmetric/transitive. This is essentially Lemma 15, but for arbitrary functions.

Definition symmetric {X} (R : Rel X) :=
  forall x y, R x y -> R y x.

Definition freflexive {X} (F : Rel X -> Rel X) :=
  forall R, reflexive R -> reflexive (F R).

Definition fsymmetric {X} (F : Rel X -> Rel X) :=
  forall R, symmetric R -> symmetric (F R).

Definition ftransitive {X} (F : Rel X -> Rel X) :=
  forall R, transitive R -> transitive (F R).

Section Equiv.
  Variable (X : Type) (f : Rel X -> Rel X).
  Implicit Types (R S : Rel X).

  Lemma t_refl R :
    freflexive f -> reflexive (t f R).
  Proof.
    move=> h. apply: tower_ind R => //=[T F ih x i|R]. exact: ih. exact: h.
  Qed.

  Lemma t_sym R :
    fsymmetric f -> symmetric (t f R).
  Proof.
    move=> h. apply: tower_ind R => /=[T F ih x y rxy i|R].
    apply: ih. exact: rxy. exact: h.
  Qed.

  Lemma t_trans R :
    ftransitive f -> transitive (t f R).
  Proof.
    move=> h. apply: tower_ind R => /=[T F ih x y z rxy ryz i|R].
    apply: (ih i _ y). exact: rxy. exact: ryz. exact: h.
  Qed.
End Equiv.

Lower symmetrization

sceil constructs the largest symmetric function below a given function.

Definition flip {X} (R : Rel X) : Rel X :=
  fun x y => R y x.

Definition sceil {X} (F : Rel X -> Rel X) (R : Rel X) : Rel X :=
  fun x y => F R x y /\ F (flip R) y x.

Lemma flip_symmetric {X} (R : Rel X) : symmetric R -> flip R = R.
Proof. move=> h. apply: le_eq => x y; exact: h. Qed.

Instance sceil_mono {X} (F : Rel X -> Rel X) {fP : monotone F} :
  monotone (sceil F).
Proof.
  move=> /= R S le_r_s x y [h1 h2]. split. exact: fP h1.
  apply: fP y x {h1} h2 => y x /=. exact: le_r_s.
Qed.

sceil preserves pre-orders and is always symmetric

Lemma freflexive_sceil {X} (F : Rel X -> Rel X) :
  freflexive F -> freflexive (sceil F).
Proof.
  move=> h R rxx. split. exact: h. apply: h. exact: rxx.
Qed.

Lemma fsymmetric_sceil {X} (F : Rel X -> Rel X) :
  fsymmetric (sceil F).
Proof.
  move=> R h x y [h1 h2]. by rewrite -[R]flip_symmetric.
Qed.

Lemma ftransitive_sceil {X} (F : Rel X -> Rel X) :
  ftransitive F -> ftransitive (sceil F).
Proof.
  move=> h R hT x y z [rxy syx] [ryz szy]. split. exact: h rxy ryz.
  apply: h szy syx => {x y z rxy ryz} x y z ryx rzy. exact: hT rzy ryx.
Qed.

Lemma symmetric_t_sceil {X} (F : Rel X -> Rel X) (R : Rel X) :
  symmetric (t (sceil F) R).
Proof. apply: t_sym. exact: fsymmetric_sceil. Qed.

Fact 16

Lemma sceil_pre {X} (f g : Rel X -> Rel X) (R : Rel X) {hR : Symmetric R} :
  fsymmetric g ->
  g (sceil f R) <= f R ->
  g (sceil f R) <= sceil f R.
Proof.
  move=> h1 h2 x y rxy. split. exact: h2. rewrite (flip_symmetric hR).
  apply: h2. apply: h1 => //. apply: fsymmetric_sceil. exact: hR.
Qed.