Require Import base ord tower.tarski tower.tower data.fintype ccs.syntax ccs.semantics.

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 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; hnf=> x; hnf=> 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.

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

Lemma bisim_coind (s t : cexp) :
  (forall R, Bisim R s t -> Bisim (○R) s t) ->
  bisim s t.
Proof.
  move=> st. apply tower_induction. move=> T F ih. exact: ih.
  move=> /= R ch. rewrite t_f. apply: st. exact: ch.
Qed.

Definition OBisim {n} (R : Rel cexp) : Rel (exp n) :=
  fun s t => forall f : fin 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 bisim_fold (R : Rel cexp) s t : Bisim (○R) s t -> Bisim R s t.
Proof. rewrite -t_f. exact: (@t_fdec _ Fbisim). Qed.

Lemma bisim_unfold s t : bisim s t -> Fbisim bisim s t.
Proof. by rewrite t_gfp gfpE. Qed.

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

Lemma bisim_left R s t : Bisim (○R) s t -> Fsim (Bisim R) s t.
Proof. by rewrite -t_f => -[]. 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_induction. move=> T F ch f i. exact: ch.
  move=> /= R ch f. rewrite t_f. apply: st. exact: ch.
Qed.

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

Global Instance bisim_equiv R : Equivalence (Bisim R).
Proof.
  apply tower_induction.
  - move=> I/= F ih. constructor. move=> s i. reflexivity.
    move=> s t h i. symmetry. exact: h. move=> s t u h1 h2 i.
      by transitivity t.
  - move=> /= {R}R equiv_R. constructor.
    + move=> s. suff: Fsim (Bisim R) s s. split=> //. by rewrite flip_symmetric.
      move=> a t st. exists t => //. reflexivity.
    + move=> s t [h1 h2]. split=> a u st. case: (h2 a u) => // v st' h.
      exists v => //. symmetry. exact: h. case: (h1 a u) => // v st' h.
      exists v => //. unfold flip. symmetry. exact: h.
    + move=> s t u [hst hts] [htu hut]. split=> a v st.
      case: (hst a v st) => v' /htu[v'' st' /=h1] h2. exists v'' => //. by etransitivity.
      case: (hut a v st) => v' /hts[v'' st' /=h1] h2. exists v'' => //.
      unfold flip in *. by etransitivity.
Qed.

Global Instance obisim_equiv n R : Equivalence (@OBisim n R).
Proof.
  constructor. move=> s f. reflexivity. move=> s t h f. symmetry. exact: h.
  move=> s t u h1 h2 f. by transitivity t.[f].
Qed.

Lemma obisim_unfold_mu n (P : exp n.+1) :
  obisim (Fix P) P.[Fix P/].
Proof.
  move=> f /=. rewrite !asimpl. apply: bisim_fold. rewrite -t_f. split.
  - move=> a s st. inv st. move: H0. rewrite !asimpl/=upE => st.
    exists s => //. reflexivity.
  - move=> a s /=. rewrite upE => st. exists s; last first. unfold flip. reflexivity.
    constructor. by rewrite !asimpl/=.
Qed.

Class CcsCongruence (R : Rel cexp) :=
  { ccs_congruence_sum :> Proper (R ==> R ==> R) (@Sum 0)
  ; ccs_congruence_par :> Proper (R ==> R ==> R) (@Par 0)
  ; ccs_congruence_new :> forall a, Proper (R ==> R) (@New 0 a)
  ; ccs_congruence_fix : forall (P Q : exp 1), (forall u : cexp, R P.[u/] Q.[u/]) -> R (Fix P) (Fix Q)
  }.

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. wlog suff: s t h / Fsim (Bisim R) (Act a s) (Act a t).
  move=> h'. split; [|rewrite flip_symmetric]; apply: h' => //. by symmetry.

  apply: step_act_inv. exists t => //. by constructor.
Qed.

Lemma upto_act_s_open n R a s t :
  @OBisim n R s t -> OBisim (○R) (Act a s) (Act a t).
Proof.
  move=> rst f /=. apply: upto_act_s. exact: rst.
Qed.

Global Instance upto_act R a : Proper (Bisim R ==> Bisim R) (Act a).
Proof.
  move=> s t rst. apply: bisim_fold. exact: upto_act_s.
Qed.

Global Instance upto_act_open n R a : Proper (@OBisim n R ==> OBisim R) (Act a).
Proof.
  move=> s t rst f /=. apply: upto_act. exact: rst.
Qed.

Global Instance upto_sum_o R :
  Proper (Bisim (○R) ==> Bisim (○R) ==> Bisim (○R)) (@Sum 0).
Proof.
  move=> s1 s2 rs t1 t2 rt. rewrite -t_f.
  wlog suff h: s1 s2 t1 t2 rs rt / Fsim (Bisim R) (Sum s1 t1) (Sum s2 t2).
  split; [|rewrite flip_symmetric]; apply: h=> //; by symmetry.

  apply bisim_left in rs. apply bisim_left in rt.
  move=> a. apply: step_sum_inv => [u/rs[v st]|u/rt[v st]] h; exists v=> //.
  by constructor. by constructor 3.
Qed.

Section CongruenceProofs.

Variable (R : Rel cexp).
Variable (congruence_properties : CcsCongruence (Bisim R)).

Lemma upto_par_o :
  Proper (Bisim (○R) ==> Bisim (○R) ==> Bisim (○R)) (@Par 0).
Proof with eauto using @step.
  move=> s1 s2 rs t1 t2 rt. rewrite -t_f.
  wlog suff h: s1 s2 t1 t2 rs rt / Fsim (Bisim R) (Par s1 t1) (Par s2 t2).
  split; [|rewrite flip_symmetric]; apply: h => //; by symmetry.

  apply: step_par_inv.
  - move=> a u /(bisim_left rs)[s2' st ru]. eexists... f_equiv=> //. exact: bisim_fold.
  - move=> a u /(bisim_left rt)[t2' st ru]. eexists... f_equiv=> //. exact: bisim_fold.
  - move=> a u v oa /(bisim_left rs)[s2' st ru] /(bisim_left rt)[t2' st' rv].
    exists (Par s2' t2'). exact: step_comm st'. by f_equiv.
Qed.

Lemma upto_new_o a :
  Proper (Bisim (○R) ==> Bisim (○R)) (@New 0 a).
Proof.
  move=> s t rst. rewrite -t_f. wlog suff h: s t rst / Fsim (Bisim R) (New a s) (New a t).
  split; [|rewrite flip_symmetric]; apply: h => //; by symmetry.

  apply: step_new_inv => b s' guarded /(bisim_left rst)[t' st rst'].
  exists (New a t'). by constructor. rewrite rst'. reflexivity.
Qed.

Lemma upto_inst' n (f g : fin n -> cexp) (s : exp n) :
  (forall i, Bisim R (f i) (g i)) -> Bisim R s.[f] s.[g].
Proof.
  elim: s f g => {n}[n a s ih|n s ihs t iht|n s ihs t iht|n a s ih|n s ih|n x] f g h/=.
  apply: upto_act. exact: ih. f_equiv. exact: ihs. exact: iht.
  f_equiv. exact: ihs. exact: iht. apply ccs_congruence_new. exact: ih.
  apply ccs_congruence_fix => u. rewrite !asimpl/=. apply: ih.
  move=>/=-[a|]//=. reflexivity. exact: h.
Qed.

Lemma upto_inst_beta' (s t : cexp) (u : exp 1) :
  Bisim R s t -> Bisim R u.[s/] u.[t/].
Proof.
  move=> h. by apply: upto_inst' => /=-[].
Qed.

Lemma upto_fix_gen (s t u : exp 1) :
  (forall v : cexp, Bisim (○R) s.[v/] t.[v/]) ->
  Bisim (○R) u.[Fix s/] u.[Fix t/].
Proof.
  move=> rst. wlog suff h: s t rst / Fsim (Bisim R) u.[Fix s/] u.[Fix t/].
  rewrite -t_f; split; [|rewrite flip_symmetric]; apply: h => v //; by symmetry.
  move=> a v. move eqn:u.[Fix s/] => e st. elim: st u s t eqn rst => {e a v}.
  - move=> a e -[]//=; last by case=> //. move=> a' s t u [e1 e2]; subst=> h.
    eexists; eauto using @step. apply: upto_inst_beta'.
    apply ccs_congruence_fix => u'. exact: bisim_fold.
  - move=> a s t u st ih -[]//=; last by case. move=> s' t' s'' t'' [e1 e2] h; subst.
    case: (ih s' s'' _ erefl h) => u' st' h'. eexists; by eauto using @step.
  - move=> a s t u st ih -[]//=; last by case. move=> s' t' s'' t'' [e1 e2] h; subst.
    case: (ih _ _ _ erefl h) => u' st' h'. eexists; by eauto using @step.
  - move=> a s t u st ih -[]//=; last by case. move=> s' t' s'' t'' [e1 e2] h; subst.
    case: (ih _ _ _ erefl h) => u' st' h'. eexists; eauto using @step.
    f_equiv=> //. apply: upto_inst_beta'. apply ccs_congruence_fix => u. exact: bisim_fold.
  - move=> a s t u st ih -[]//=; last by case. move=> s' t' s'' t'' [e1 e2] h; subst.
    case: (ih _ _ _ erefl h) => u' st' h'. eexists; eauto using @step.
    f_equiv=> //. apply: upto_inst_beta'. apply ccs_congruence_fix => v. exact: bisim_fold.
  - move=> a s t u v oa st1 ih1 st2 ih2 -[]//=; last by case.
    move=> s' t' s'' t'' [e1 e2] h; subst.
    case: (ih1 _ _ _ erefl h) => u1 st1' h1'.
    case: (ih2 _ _ _ erefl h) => u2 st2' h2'.
    exists (Par u1 u2). by eauto using @step. by f_equiv.
  - move=> n a s t ga st ih -[]//=; last by case.
    move=> b s' t' u' [e1 e2] h; subst.
    case: (ih _ _ _ erefl h) => u st' h'. eexists; eauto using @step.
      by apply ccs_congruence_new.
  - move=> s a u st ih -[]//=.
    + move=> s' t' u' [e] h; subst.
      case/(_ _)/Wrap: (ih s'.[Fix s'/] t' _ _ h). by rewrite -subst_up.
      case=> v' st' h'. eexists. econstructor. rewrite (subst_up s' (Fix s')). eassumption.
      exact: h'.
    + case=> //= s' t' [e] h; subst.
      case: (ih _ _ _ erefl h) => u' st' h'.
      case: (bisim_left (h (Fix t')) st') => u'' st'' h''.
      exists u''. by constructor. by transitivity u'.
Qed.

Lemma upto_fix_o s t :
  (forall u, Bisim (○R) s.[u/] t.[u/]) -> Bisim (○R) (Fix s) (Fix t).
Proof.
  move=> /upto_fix_gen h. exact: (h (Var bound)).
Qed.

Lemma congruence_step : CcsCongruence (Bisim (○R)).
Proof.
  constructor. exact: upto_sum_o. exact: upto_par_o.
  exact: upto_new_o. exact: upto_fix_o.
Qed.

End CongruenceProofs.

Global Instance ccs_congruence_bisim R : CcsCongruence (Bisim R).
Proof.
  apply tower_induction => {R} /=.
  - move=> I F ih. constructor.
    + move=> s1 s2 rs t1 t2 rt i. f_equiv. exact: rs. exact: rt.
    + move=> s1 s2 rs t1 t2 rt i. f_equiv. exact: rs. exact: rt.
    + move=> a s1 s2 rs i. apply ccs_congruence_new. exact: rs.
    + move=> s1 s2 rs i. apply ccs_congruence_fix => u. exact: rs.
  - move=> R cR. rewrite t_f. exact: congruence_step.
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 /=. f_equiv. exact: rs. exact: rt. Qed.

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

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

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

Theorem upto_inst m n R (f g : fin 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' => /= x. exact: h1.
Qed.