Require Import prelim companion_mu ccs_mu_syn.

Definition cexp := exp 0.
Definition lts := cexp -> act -> cexp -> Prop.

Definition observable (a : act) : bool :=
  if a isn't ActTau then true else false.

Definition dual (a : act) : act :=
  match a with
  | ActSend n => ActRecv n
  | ActRecv n => ActSend n
  | ActTau => ActTau
  end.

Definition guard (n : nat) (a : act) : bool :=
  match a with
  | ActSend m | ActRecv m => n != m
  | ActTau => true
  end.

Inductive Fstep (R : lts) : lts :=
| Fstep_act a s : Fstep R (Act a s) a s
| Fstep_suml a s t u :
    R s a t -> Fstep R (Sum s u) a t
| Fstep_sumr a s t u :
    R t a u -> Fstep R (Sum s t) a u
| Fstep_parl a s t u :
    R s a t -> Fstep R (Par s u) a (Par t u)
| Fstep_parr a s t u :
    R t a u -> Fstep R (Par s t) a (Par s u)
| Fstep_comm a s t u v :
    observable a -> R s a t -> R u (dual a) v -> Fstep R (Par s u) ActTau (Par t v)
| Fstep_restrict n a s t :
    guard n a -> R s a t -> Fstep R (New n s) a (New n t)
| Fstep_fix s a u :
    R s.[Fix s/] a u ->
    Fstep R (Fix s) a u.

Notation Step := (l Fstep).
Notation step := (Step top).

Instance Fstep_mono : monotone Fstep.
Proof.
  move=> R S /(_ _ _ _ _)le_r_s s a t h.
  inversion_clear h; eauto using Fstep.
Qed.

Lemma step_unfold (R : lts) s a t : Step R s a t -> Fstep (Step R) s a t.
Proof. exact: (@l_unfold _ Fstep). Qed.

Lemma step_fold s a t : Fstep step s a t -> step s a t.
Proof. by rewrite -mu_l mu_fp. Qed.

Lemma fstep_step R a s t : Step R s a t -> step s a t.
Proof. apply: (l_monotone Fstep). exact: topI. Qed.

Lemma ffstep_step R a s t : Fstep (Step R) s a t -> step s a t.
Proof. rewrite l_f. exact: fstep_step. Qed.

Lemma step_act a s : step (Act a s) a s.
Proof. eauto using step_fold, Fstep. Qed.

Lemma step_suml a s t u : step s a t -> step (Sum s u) a t.
Proof. eauto using step_fold, Fstep. Qed.

Lemma step_sumr a s t u : step t a u -> step (Sum s t) a u.
Proof. eauto using step_fold, Fstep. Qed.

Lemma step_parl a s t u : step s a t -> step (Par s u) a (Par t u).
Proof. eauto using step_fold, Fstep. Qed.

Lemma step_parr a s t u : step t a u -> step (Par s t) a (Par s u).
Proof. eauto using step_fold, Fstep. Qed.

Lemma step_comm a s t u v :
  observable a ->
  step s a t -> step u (dual a) v -> step (Par s u) ActTau (Par t v).
Proof. eauto using step_fold, Fstep. Qed.

Lemma step_new n a s t :
  guard n a -> step s a t -> step (New n s) a (New n t).
Proof. eauto using step_fold, Fstep. Qed.

Lemma step_fix a s u :
  step s.[Fix s/] a u -> step (Fix s) a u.
Proof. eauto using step_fold, Fstep. Qed.

Lemma step_act_inv (R : lts) (P : act -> cexp -> Prop) a s :
  P a s -> forall b t, Step R (Act a s) b t -> P b t.
Proof. move=> p b t /step_unfold st. by inv st. Qed.

Lemma step_sum_inv (R : lts) (P : cexp -> Prop) a s t :
  (forall u, Step R s a u -> P u) ->
  (forall u, Step R t a u -> P u) ->
  forall u, Step R (Sum s t) a u -> P u.
Proof.
  move=> p1 p2 u /step_unfold st. inv st; by [exact: p1|exact: p2].
Qed.

Lemma step_par_inv (R : lts) (P : act -> cexp -> Prop) s t :
  (forall a u, Step R s a u -> P a (Par u t)) ->
  (forall a u, Step R t a u -> P a (Par s u)) ->
  (forall a u v, observable a -> Step R s a u -> Step R t (dual a) v -> P ActTau (Par u v)) ->
  (forall a u, Step R (Par s t) a u -> P a u).
Proof.
  move=> p1 p2 p3 a u /step_unfold st. inv st; eauto.
Qed.

Lemma step_new_inv (R : lts) (P : act -> cexp -> Prop) n s :
  (forall a t, guard n a -> Step R s a t -> P a (New n t)) ->
  forall a t, Step R (New n s) a t -> P a t.
Proof.
  move=> p a t /step_unfold st. inv st; eauto.
Qed.

Lemma step_fix_inv (R : lts) a s u :
  Step R (Fix s) a u -> Step R s.[Fix s/] a u.
Proof. move=> /step_unfold st. by inv st. Qed.