Library iris.chan_lang.protocol

From iris.chan_lang Require Export lang derived.

CoInductive protocol (T: Type) :=
  | prot_end
  | prot_send: T → protocol T → protocol T
  | prot_recv: T → protocol T → protocol T
  | prot_ext: protocol T → protocol T → protocol T
  | prot_int: protocol T → protocol T → protocol T.

Arguments prot_end {_}.
Arguments prot_send {_} _ _.
Arguments prot_recv {_} _ _.
Arguments prot_ext {_} _ _.
Arguments prot_int {_} _ _.

Lemma unfold_prot {T} (p: protocol T) :
  p = match p with
      | prot_end ⇒ prot_end
      | prot_send t p' ⇒ prot_send t p'
      | prot_recv t p' ⇒ prot_recv t p'
      | prot_int pl pr ⇒ prot_int pl pr
      | prot_ext pl pr ⇒ prot_ext pl pr
      end.
Proof.
  destruct p; auto.
Qed.

CoFixpoint dual {T: Type} (p: protocol T) : protocol T :=
  match p with
    | prot_end ⇒ prot_end
    | prot_send P p ⇒ prot_recv P (dual p)
    | prot_recv P p ⇒ prot_send P (dual p)
    | prot_ext p p' ⇒ prot_int (dual p) (dual p')
    | prot_int p p' ⇒ prot_ext (dual p) (dual p')
  end.

Inductive choice : Set :=
  | choice_left
  | choice_right
  | choice_next.

CoInductive prot_eq {T: Type} : protocol T → protocol T → Prop :=
  | prot_eq_end: prot_eq prot_end prot_end
  | prot_eq_recv Φ p p':
      prot_eq p p' →
      prot_eq (prot_recv Φ p) (prot_recv Φ p')
  | prot_eq_send Φ p p':
      prot_eq p p' →
      prot_eq (prot_send Φ p) (prot_send Φ p')
  | prot_eq_int p1 p1' p2 p2':
      prot_eq p1 p1' →
      prot_eq p2 p2' →
      prot_eq (prot_int p1 p2) (prot_int p1' p2')
  | prot_eq_ext p1 p1' p2 p2':
      prot_eq p1 p1' →
      prot_eq p2 p2' →
      prot_eq (prot_ext p1 p2) (prot_ext p1' p2').

Instance prot_equiv {A} : Equiv (protocol A) := @prot_eq A.

Global Instance prot_equivalence A: Equivalence (@equiv (protocol A) _).
Proof.
  split.
  - now cofix; intros [ | | | | ]; constructor.
  - now cofix; intros ?? [ | | | | ]; constructor.
  - cofix; intros ???. inversion 1; inversion 1; econstructor; etrans; eauto.
Qed.

Inductive prot_modc {T: Type} : protocol T → list choice → protocol T → Prop :=
  | prot_modc_nil S S':
      prot_eq S S' →
      prot_modc S [] S'
  | prot_modc_recv Φ S S' l:
      prot_modc S l S' →
      prot_modc (prot_recv Φ S) (choice_next::l) S'
  | prot_modc_send Φ S S' l:
      prot_modc S l S' →
      prot_modc (prot_send Φ S) (choice_next::l) S'
  | prot_modc_ext_left S1 S2 S' l:
      prot_modc S1 l S' →
      prot_modc (prot_ext S1 S2) (choice_left ::l) S'
  | prot_modc_ext_right S1 S2 S' l:
      prot_modc S2 l S' →
      prot_modc (prot_ext S1 S2) (choice_right::l) S'
  | prot_modc_int_left S1 S2 S' l:
      prot_modc S1 l S' →
      prot_modc (prot_int S1 S2) (choice_left ::l) S'
  | prot_modc_int_right S1 S2 S' l:
      prot_modc S2 l S' →
      prot_modc (prot_int S1 S2) (choice_right::l) S'.

Lemma prot_modc_inj {T} (p: protocol T) cs p1 p2:
  prot_modc p cs p1 →
  prot_modc p cs p2 →
  p1 ≡ p2.
Proof.
  induction 1; try inversion 1; auto.
  subst. transitivity S; eauto.
Qed.

Instance dual_proper T: Proper ((≡) ==> (≡)) (@dual T).
Proof.
  intros p p' Heq.
  revert p p' Heq.
  cofix. intros p p' Heq.
  rewrite (unfold_prot (dual p)).
  rewrite (unfold_prot (dual p')).
  destruct p, p'; simpl; try inversion Heq; subst;
  econstructor; eapply dual_proper; eauto.
Qed.

Instance prot_modc_proper T: Proper ((≡) ==> (=) ==> (≡) ==> iff) (@prot_modc T).
Proof.
  intros p1 p1' Heq1 l1 l2 → p2 p2' Heq2.
  split.
  - intros Hmodc. revert p1' p2' Heq1 Heq2. induction Hmodc; auto.
    × econstructor; setoid_subst; eauto.
    × intros. inversion Heq1. subst. econstructor. eauto.
    × intros. inversion Heq1. subst. econstructor. eauto.
    × intros. inversion Heq1. subst. econstructor. eauto.
    × intros. inversion Heq1. subst. econstructor. eauto.
    × intros. inversion Heq1. subst. econstructor. eauto.
    × intros. inversion Heq1. subst. econstructor. eauto.
  - intros Hmodc. revert p1 p2 Heq1 Heq2. induction Hmodc; auto.
    × econstructor; setoid_subst; eauto.
    × intros. inversion Heq1. subst. econstructor. eauto.
    × intros. inversion Heq1. subst. econstructor. eauto.
    × intros. inversion Heq1. subst. econstructor. eauto.
    × intros. inversion Heq1. subst. econstructor. eauto.
    × intros. inversion Heq1. subst. econstructor. eauto.
    × intros. inversion Heq1. subst. econstructor. eauto.
Qed.

Lemma prot_modc_app {T} (p1: protocol T) la p2 lb p3:
      prot_modc p1 la p2 →
      prot_modc p2 lb p3 →
      prot_modc p1 (la ++ lb) p3.
Proof.
  revert lb p3.
  induction 1; auto; intros;
  try (rewrite -app_comm_cons;
       econstructor; eauto).
  simpl. rewrite H. auto.
Qed.