Require Import prelim companion companion_rel companion_mu fin ccs_mu_syn ccs_mu_sem.

Implicit Types (R S : Rel cexp).

Definition Fsim (R : Rel cexp) (s t : cexp) : 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).

Definition OBisim {n} (R : Rel cexp) : Rel (exp n) :=
  fun s t => forall f : 'I_n -> cexp, Bisim R s.[f] t.[f].

Notation obisim := (@OBisim _ bot).

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 obisim_coind n (s t : exp n) :
  (forall R, OBisim R s t -> OBisim (○R) s t) ->
  obisim s t.
Proof.
  move=> st. rewrite/OBisim. apply tower_ind. move=> T F ch f i. exact: ch.
  move=> /= R ch f. rewrite t_f. apply: st. exact: ch.
Qed.

Lemma bisim_fold (R : Rel cexp) 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 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 cexp) : RewriteRelation (Bisim R).

Instance bisim_refl (R : Rel cexp) : 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 cexp) : Symmetric (Bisim R).
Proof. exact: symmetric_t_sceil. Qed.

Instance bisim_trans (R : Rel cexp) : 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 obisim_refl n (R : Rel cexp) : Reflexive (@OBisim n R).
Proof. move=> s f /=. reflexivity. Qed.

Instance obisim_sym n (R : Rel cexp) : Symmetric (@OBisim n R).
Proof. move=> s t h f /=. symmetry. exact: h. Qed.

Instance obisim_trans n (R : Rel cexp) : Transitive (@OBisim n R).
Proof.
  move=> s t u h1 h2 f /=. transitivity (t.[f]).
  exact: h1. exact: h2.
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 cexp :=
| 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 cexp :=
| 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 cexp :=
| 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 cexp :=
| 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 cFix (R : Rel cexp) : Rel cexp :=
| CFix (s1 s2 : exp 1) :
    (forall u : cexp, R s1.[u/] s2.[u/]) ->
    cFix R (Fix s1) (Fix s2).

Inductive cSubst (R : Rel cexp) : Rel cexp :=
| CSubst n (f g : 'I_n -> cexp) (s : exp n) :
    (forall x, R (f x) (g x)) -> cSubst R s.[f] s.[g].

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

Lemma cFix_symmetric : fsymmetric cFix.
Proof. move=>????[]; eauto using cFix. Qed.

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

Lemma cSubst_symmetric : fsymmetric cSubst.
Proof. move=>????[]; eauto using cSubst. Qed.

Lemma step_subst_sim R n (f g : 'I_n -> cexp) :
  (forall s, Bisim R s.[f] s.[g]) ->
  (forall S : lts,
      (forall s a t, Step S s.[f] a t -> exists2 t', step s.[g] a t' & Bisim R t t') ->
      forall x a t, Fstep (Step S) (f x) a t -> exists2 t', step (g x) a t' & Bisim R t t') ->
  forall s a t, step s.[f] a t -> exists2 t', step s.[g] a t' & Bisim R t t'.
Proof.
  move=> ch H. pattern step at 1. apply: ind => /=.
  move=> T F ih s a s' [i st]. exact: (ih i).
  move=> S ih [b s|s1 s2|s1 s2|b s|s|x] a s' st.
  - inv st. eexists; [apply: step_act|exact: ch].
  - inv st.
    + move: H4 => /ih[s1' st bs]. eexists; [exact: step_suml st|exact: bs].
    + move: H4 => /ih[s2' st bs]. eexists; [exact: step_sumr st|exact: bs].
  - inv st.
    + move: H4 => /ih[t'' p q]. eexists. apply: step_parl. exact: p. exact: upto_par.
    + move: H4 => /ih[t'' p q]. eexists. apply: step_parr. exact: p. exact: upto_par.
    + move: H3 => /ih[t1' p1 q1]. move: H6 => /ih[t2' p2 q2].
      exists (Par t1' t2'). exact: step_comm p1 p2. exact: upto_par.
  - inv st. move: H5 => /ih[s' st bs]. eexists. apply: step_new => //. exact: st.
    apply: upto_new. exact: bs.
  - inv st. move: H1. rewrite (@subst_up _ _ _ (Fix s)) => /ih[t' st bs].
    eexists; [|exact: bs]. apply: step_fix. rewrite (@subst_up _ _ _ (Fix s)). exact: st.
  - move: st => /=. apply: H. exact: ih.
Qed.

Lemma upto_inst' R :
  cSubst (Bisim R) <= Bisim R.
Proof.
  apply: bisim_upto R => [|R ch]. exact: cSubst_symmetric.
  move=> s t [{s t}n f g s h_subst] a s' st.
  (* Coinductive hypothesis *)
  have {ch}ch: forall s : exp n, Bisim R s.[f] s.[g].
    move=> t. apply: ch. constructor=> x. apply: bisim_fold. exact: h_subst.
  (* Induction on the step relation *)
  apply: step_subst_sim ch _ s a s' st. move=> S _ x a t.
  move=> /ffstep_step/(bisim_left (h_subst x)). exact.
Qed.

Lemma upto_inst_w R n (s : exp n) (f g : 'I_n -> cexp) :
  (forall x, Bisim R (f x) (g x)) -> Bisim R s.[f] s.[g].
Proof.
  move=> h. apply: upto_inst'. by constructor.
Qed.

Lemma upto_beta R (s t : cexp) u :
  Bisim R s t -> Bisim R u.[s/] u.[t/].
Proof.
  move=> bs. apply: upto_inst_w.
  apply: ord_inv => [|x]; rewrite ?asimpl //. reflexivity.
Qed.

Lemma upto_fix' R :
  cFix (Bisim R) <= Bisim R.
Proof.
  apply: bisim_upto R => [|R ch]. exact: cFix_symmetric.
  move=> s t [{s t}s t h] a s' /step_fix_inv st.
  case: (step_subst_sim (R := R) (g := Fix t .: ids) _ _ st).
  - move=> {a s' st} u. apply: upto_beta. apply: ch. constructor => v. apply: bisim_fold. exact: h.
  - move=> {a s' st} S ih. apply: ord_inv => [|[]//] a s'.
    rewrite !scons0 => st. inv st. move: H0 => /ih[t' st bs].
    move: st => /(bisim_left (h (Fix t)))[t'' st' bs'].
    exists t''. exact: step_fix. by transitivity t'.
  - move=> s'' st' bs. move: st' => /(bisim_left (h (Fix t)))[t'' st'' bs''].
    exists t''. exact: step_fix. by transitivity s''.
Qed.

Lemma upto_fix R (s t : exp 1) :
  (forall u, Bisim R s.[u/] t.[u/]) -> Bisim R (Fix s) (Fix t).
Proof.
  move=> h. apply: upto_fix'. by constructor.
Qed.

Instance bisim_equiv n R : Equivalence (@OBisim n R).
Proof. constructor; exact _. Qed.

Instance act_proper n R : Proper (eq ==> OBisim R ==> OBisim (○R)) (@Act n).
Proof. move=> a b -> s t rst f /=. exact: upto_act_s. Qed.

Instance act_proper_l n R : Proper (eq ==> OBisim R ==> OBisim R) (@Act n).
Proof. move=> a b -> s1 s2 rs f /=. exact: upto_act. Qed.

Instance sum_proper n R : Proper (OBisim R ==> OBisim R ==> OBisim R) (@Sum n).
Proof. move=> s1 s2 rs t1 t2 rt f /=. exact: upto_sum. Qed.

Instance par_proper n R : Proper (OBisim R ==> OBisim R ==> OBisim R) (@Par n).
Proof. move=> s1 s2 rs t1 t2 rt f /=. exact: upto_par. Qed.

Instance new_proper n R : Proper (eq ==> OBisim R ==> OBisim R) (@New n).
Proof. move=> a b -> s t rst f /=. exact: upto_new. Qed.

Instance fix_proper n R : Proper (OBisim R ==> OBisim R) (@Fix n).
Proof.
  move=> s t rst f /=. apply: upto_fix => u. rewrite !asimpl. exact: rst.
Qed.

Theorem upto_inst m n R (f g : 'I_m -> exp n) (s t : exp m) :
  (forall x, OBisim R (f x) (g x)) -> OBisim R s t -> OBisim R s.[f] t.[g].
Proof.
  move=> h1 h2 k /=. rewrite !asimpl. etransitivity. apply: h2.
  apply: upto_inst'. constructor => /= x. exact: h1.
Qed.