Require Import base data.fintype ccs.syntax.

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 step : lts :=
| step_act a s : step (Act a s) a s
| step_suml a s t u :
    step s a t -> step (Sum s u) a t
| step_sumr a s t u :
    step t a u -> step (Sum s t) a u
| step_parl a s t u :
    step s a t -> step (Par s u) a (Par t u)
| step_parr a s t u :
    step t a u -> step (Par s t) a (Par s u)
| 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)
| step_restrict n a s t :
    guard n a -> step s a t -> step (New n s) a (New n t)
| step_fix s a u :
    step s.[Fix s/] a u ->
    step (Fix s) a u.

Ltac inv H := inversion H; subst; clear H.

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

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

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

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

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