Require Import prelim companion companion_param ccs_rep_lang ccs_rep_bisim.

Section Soundndess.
  Variables (A : clat) (f : A -> A).
  Hypothesis (fP : monotone f).

  Definition sound g := forall x, x <= f (g x) -> x <= nu f.

  Lemma sound_t :
    sound (t f).
  Proof.
    move=> x. by rewrite nu_coind_t.
  Qed.

  Lemma upto_sound g :
    g <= t f -> sound g.
  Proof.
    move=> h1 x h2. apply: sound_t. by rewrite {1}h2 h1.
  Qed.
End Soundndess.

Inductive C (R : Rel exp) : Rel exp :=
| C_R : R <= C R
| C_bisim : bisim <= C R
| C_sym : symmetric _ (C R)
| C_trans : transitive (C R)
| C_ctx (c : ctx) (s t : exp) : C R s t -> C R (fill c s) (fill c t).

Lemma C_sound :
  sound Fbisim C.
Proof.
  apply: upto_sound => R s t. elim=> {s t}.
  - move=> s t rst. exact: (t_inc Fbisim).
  - move=> s t. exact: bisim_bisim.
  - move=> s t _ rst. by symmetry.
  - move=> s t u _ h1 _ h2. by transitivity t.
  - move=> c s t _. exact: fill_proper.
Qed.