Require Import prelim companion companion_rel ccs_rep_lang.

Implicit Types (R S : Rel exp) (s t : exp).

Definition Fsim (R : Rel exp) (s t : exp) : Prop :=
  forall a s', step s a s' -> exists2 t', step t a t' & R s' t'.

Definition Fbisim := sceil Fsim.

Notation Bisim := (t Fbisim).
Notation bisim := (Bisim bot).
Notation "'○' R" := (Fbisim (Bisim R))
  (at level 100, format "○ R") : type_scope.

Notation "R '|-' s '~' t" := (Bisim R s t) (at level 60).
Notation "s ~~ t" := (bisim s t) (at level 60).

Instance Fsim_mono : monotone Fsim.
Proof.
  move=> R S le_r_s s t h a s' /h[t' st rst].
  exists t' => //. exact: le_r_s.
Qed.

Instance Fbisim_mono : monotone Fbisim.
Proof. exact _. Qed.

Instance Bisim_mono : monotone Bisim.
Proof. exact _. Qed.

Lemma bisim_coind (s t : exp) :
  (forall R : Rel exp, Bisim R s t -> Bisim (○R) s t) ->
  bisim s t.
Proof.
  move=> st. apply tower_ind => [T F h i//|/=R /st]. by rewrite -t_f.
Qed.

Lemma bisim_fold (R : Rel exp) s t : Bisim (○R) s t -> Bisim R s t.
Proof. rewrite -t_f. exact: (@t_fold _ Fbisim). Qed.

Lemma bisim_unfold s t : bisim s t -> Fbisim bisim s t.
Proof. by rewrite -nu_t nu_fp. Qed.

Lemma bisim_bisim R s t : bisim s t -> Bisim R s t.
Proof. apply: (t_monotone Fbisim). exact: botE. Qed.

Lemma r_bisim (R : Rel exp) s t : R s t -> Bisim R s t.
Proof. exact: (t_inc Fbisim). Qed.

Lemma bisim_left R s t : Bisim (○R) s t -> Fsim (Bisim R) s t.
Proof. by rewrite -t_f => -[]. Qed.

Instance bisim_rewrite (R : Rel exp) : RewriteRelation (Bisim R).

Instance bisim_refl (R : Rel exp) : Reflexive (Bisim R).
Proof.
  apply: t_refl. apply: freflexive_sceil => {R} R rxx s a t st. by exists t.
Qed.

Instance bisim_sym (R : Rel exp) : Symmetric (Bisim R).
Proof. exact: symmetric_t_sceil. Qed.

Instance bisim_trans (R : Rel exp) : Transitive (Bisim R).
Proof.
  apply: t_trans. apply: ftransitive_sceil => {R} R tR s t u rst rtu.
  move=> a s' /rst[t'/rtu[u' st rtu'] rst']. exists u' => //.
  exact: tR rst' rtu'.
Qed.

Instance rbisim_subrel R : subrelation bisim (Bisim R).
Proof. exact: bisim_bisim. Qed.

Instance rbisim_fold_subrel R : subrelation (Bisim (○R)) (Bisim R).
Proof. exact: bisim_fold. Qed.

Lemma bisim_upto g :
  monotone g -> fsymmetric g ->
  (forall R, g (Bisim R) <= Bisim R -> g (Bisim (○R)) <= Fsim (Bisim R)) ->
  forall R, g (Bisim R) <= Bisim R.
Proof.
  move=> h1 h2 h3. apply: upto => /= R /h3 h4.
  apply: sceil_pre h2 _. by rewrite t_f.
Qed.

Inductive cAct (R : Rel exp) : Rel exp :=
| CAct a s t : R s t -> cAct R (Act a s) (Act a t).

Lemma cAct_step R :
  cAct R <= Fbisim R.
Proof.
  move=> s t [{s t}a s t rst]. split; rewrite/Fsim; apply step_act_inv;
    eexists; by [exact: step_act|exact: rst].
Qed.

Lemma upto_act_s R a s t :
  Bisim R s t -> Bisim (○R) (Act a s) (Act a t).
Proof.
  move=> h. rewrite -t_f. apply: cAct_step. by constructor.
Qed.

Lemma upto_act R a s t :
  Bisim R s t -> Bisim R (Act a s) (Act a t).
Proof.
  move=> h. apply: bisim_fold. exact: upto_act_s.
Qed.

Inductive cSum (R : Rel exp) : Rel exp :=
| CSum s1 s2 t1 t2 : R s1 t1 -> R s2 t2 -> cSum R (Sum s1 s2) (Sum t1 t2).

Instance cSum_mono : monotone cSum.
Proof. move=> R S le_r_s s t h. inv h. apply: CSum; exact: le_r_s. Qed.

Lemma cSum_symmetric : fsymmetric cSum.
Proof. move=> R Rh ??[]; eauto using cSum. Qed.

Lemma upto_sum' R :
  cSum (Bisim R) <= Bisim R.
Proof.
  apply: bisim_upto R => [|R ch]. exact: cSum_symmetric.
  move=> s t [{s t}s1 s2 t1 t2 /bisim_left h1 /bisim_left h2] a.
  apply step_sum_inv => [u/h1|u/h2] [t' st r];
    exists t'; eauto using step_suml, step_sumr.
Qed.

Lemma upto_sum R s1 s2 t1 t2 :
  Bisim R s1 s2 -> Bisim R t1 t2 -> Bisim R (Sum s1 t1) (Sum s2 t2).
Proof. move=> h1 h2. apply: upto_sum'. by constructor. Qed.

Inductive cPar (R : Rel exp) : Rel exp :=
| CPar s1 s2 t1 t2 : R s1 t1 -> R s2 t2 -> cPar R (Par s1 s2) (Par t1 t2).

Instance cPar_mono : monotone cPar.
Proof. move=> R S le_r_s s t h. inv h. apply: CPar; exact: le_r_s. Qed.

Lemma cPar_symmetric : fsymmetric cPar.
Proof. move=> R Rh ??[]; eauto using cPar. Qed.

Lemma upto_par' R :
  cPar (Bisim R) <= Bisim R.
Proof.
  apply: bisim_upto R => [|R h]. exact: cPar_symmetric.
  move=> s t [{s t}s1 s2 t1 t2 h1 h2].
  apply: step_par_inv => [a u st|a u st|a u v ob].
  - move: (st) => /(bisim_left h1)[u' st' ru]. exists (Par u' t2).
    exact: step_parl. apply: h. constructor. exact: ru. exact: bisim_fold.
  - move: (st) => /(bisim_left h2)[u' st' ru]. exists (Par t1 u').
    exact: step_parr. apply: h. constructor. exact: bisim_fold. exact: ru.
  - move=> /(bisim_left h1)[u1 st1 r1] /(bisim_left h2)[u2 st2 r2].
    exists (Par u1 u2). exact: step_comm st1 st2. apply: h. by constructor.
Qed.

Lemma upto_par R s1 s2 t1 t2 :
  Bisim R s1 s2 -> Bisim R t1 t2 -> Bisim R (Par s1 t1) (Par s2 t2).
Proof.
  move=> h1 h2. apply: upto_par'. by constructor.
Qed.

Inductive cNew (R : Rel exp) : Rel exp :=
| CNew n s t : R s t -> cNew R (New n s) (New n t).

Instance cNew_mono : monotone cNew.
Proof. move=> R S/(_ _ _)???[]; firstorder using cNew. Qed.

Lemma cNew_symmetric : fsymmetric cNew.
Proof. move=>????[]; eauto using cNew. Qed.

Lemma upto_new' R :
  cNew (Bisim R) <= Bisim R.
Proof.
  apply: bisim_upto R => [|R ch]. exact: cNew_symmetric.
  move=> s t [{s t}n s1 s2 /bisim_left h].
  apply: step_new_inv => b t1 g /h[t2 st rst].
  exists (New n t2). exact: step_new. exact: ch.
Qed.

Lemma upto_new R n s t :
  Bisim R s t -> Bisim R (New n s) (New n t).
Proof.
  move=> h. apply: upto_new'. by constructor.
Qed.

Inductive cRep (R : Rel exp) : Rel exp :=
| CRep s t : R s t -> cRep R (Rep s) (Rep t).

Instance cRep_mono : monotone cRep.
Proof. move=> R S le_r_s s t h. inv h. apply: CRep. exact: le_r_s. Qed.

Lemma cRep_symmetric : fsymmetric cRep.
Proof. move=>????[]; eauto using cRep. Qed.

Lemma upto_rep' R :
  cRep (Bisim R) <= Bisim R.
Proof.
  apply: bisim_upto R => [|R ch]. exact: cRep_symmetric.
  move=> s t [{s t}s t rst]. apply: step_rep_ind.
  - move=> a s' st1 [t' st2 rst']. exists (Par t' t).
    apply: step_rep. exact: step_parl.
    apply: upto_par. exact: rst'. exact: bisim_fold.
  - move=> a s' /(bisim_left rst)[t' st rst']. exists (Par (Rep t) t').
    apply: step_rep. exact: step_parr. apply: upto_par.
    apply: ch. constructor. exact: bisim_fold. exact: rst'.
  - move=> a u1 u2 ob st1 [v1 st2 ruv1] /(bisim_left rst)[v2 st3 ruv2].
    exists (Par v1 v2). apply: step_rep. exact: step_comm ob st2 st3.
    exact: upto_par.
Qed.

Lemma upto_rep R s t :
  Bisim R s t -> Bisim R (Rep s) (Rep t).
Proof.
  move=> h. apply: upto_rep'. by constructor.
Qed.

Instance bisim_equiv R : Equivalence (Bisim R).
Proof. constructor; exact _. Qed.

Instance act_proper R : Proper (eq ==> Bisim R ==> Bisim (○R)) Act.
Proof. move=> a b ->. exact: upto_act_s. Qed.

Instance act_proper_l R : Proper (eq ==> Bisim R ==> Bisim R) Act.
Proof. move=> a b -> s1 s2 rs. rewrite rs. reflexivity. Qed.

Instance sum_proper R : Proper (Bisim R ==> Bisim R ==> Bisim R) Sum.
Proof. move=> s1 s2 rs t1 t2 rt. exact: upto_sum. Qed.

Instance par_proper R : Proper (Bisim R ==> Bisim R ==> Bisim R) Par.
Proof. move=> s1 s2 rs t1 t2 rt. exact: upto_par. Qed.

Instance new_proper R : Proper (eq ==> Bisim R ==> Bisim R) New.
Proof. move=> m n ->. exact: upto_new. Qed.

Instance rep_proper R : Proper (Bisim R ==> Bisim R) Rep.
Proof. exact: upto_rep. Qed.

Inductive ctx :=
| THole
| TExp (s : exp)
| TAct (a : act) (c : ctx)
| TSum (c1 c2 : ctx)
| TPar (c1 c2 : ctx)
| TRep (c : ctx)
| TNew (n : nat) (c : ctx).

Inductive gctx :=
| GExp (s : exp)
| GAct (a : act) (c : ctx)
| GSum (c1 c2 : gctx)
| GPar (c1 c2 : gctx)
| GRep (c : gctx)
| GNew (n : nat) (c : gctx).

Fixpoint fill (c : ctx) (s : exp) : exp :=
  match c with
  | THole => s
  | TExp t => t
  | TAct a c => Act a (fill c s)
  | TSum c1 c2 => Sum (fill c1 s) (fill c2 s)
  | TPar c1 c2 => Par (fill c1 s) (fill c2 s)
  | TRep c => Rep (fill c s)
  | TNew n c => New n (fill c s)
  end.

Fixpoint gfill (c : gctx) (s : exp) : exp :=
  match c with
  | GExp t => t
  | GAct a c => Act a (fill c s)
  | GSum c1 c2 => Sum (gfill c1 s) (gfill c2 s)
  | GPar c1 c2 => Par (gfill c1 s) (gfill c2 s)
  | GRep c => Rep (gfill c s)
  | GNew n c => New n (gfill c s)
  end.

Lemma fill_proper R c s t :
  Bisim R s t -> Bisim R (fill c s) (fill c t).
Proof.
  move=> rst. elim: c => //=[u|a c->|c1 ch c2->|c1 ch c2->|c->|n c->];
    rewrite ?ch; reflexivity.
Qed.

Lemma gfill_proper R c s t :
  Bisim R s t -> Bisim (○R) (gfill c s) (gfill c t).
Proof.
  move=> rst. elim: c => //=[u|a c|c1 ch c2->|c1 ch c2->|c->|n c->];
    rewrite ?ch; try reflexivity. apply: upto_act_s. exact: fill_proper.
Qed.

Theorem unique_solutions c s t :
  bisim s (gfill c s) ->
  bisim t (gfill c t) ->
  bisim s t.
Proof.
  move=> h1 h2. apply: bisim_coind => R ch. etransitivity.
  apply: bisim_bisim. exact: h1. etransitivity. exact: gfill_proper.
  apply: bisim_bisim. by symmetry.
Qed.

Lemma parC R s t :
  Bisim R (Par s t) (Par t s).
Proof.
  move: s t. apply tower_ind => {R} /= [T F ch s t i|R ch]; first by exact: ch.
  wlog suff: / forall s t, Fsim (Bisim R) (Par s t) (Par t s).
  move=> h. split. exact: h. rewrite flip_symmetric. exact: h. exact: bisim_sym.
  move=> s t. apply: step_par_inv.
  - move=> a u st. exists (Par t u). exact: step_parr. exact: ch.
  - move=> a u st. exists (Par u s). exact: step_parl. exact: ch.
  - move=> a u v ob st1 st2. exists (Par v u). case: a ob st1 st2 => //=a ob st1 st2;
    exact: step_comm st2 st1. exact: ch.
Qed.

Section Example.
  Variable A B : exp.
  Let ai : act := ActRecv 0.
  Let ao : act := dual (ai).
  Hypothesis A_def : bisim A (Par (Act ao (Rep A)) (Act ai B)).
  Hypothesis B_def : bisim B (Par (Act ao (Rep B)) (Act ai A)).

  Lemma AB :
    bisim A B.
  Proof.
    apply: bisim_coind => R ch.
    etransitivity. apply: bisim_bisim. exact: A_def.
    etransitivity; last first. apply: bisim_bisim. symmetry. exact: B_def.
    apply: upto_par; apply: upto_act_s. exact: upto_rep. by symmetry.
  Qed.
End Example.