# 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.