Require Import chan.
Require Import chanlist.

(** syntax *)

Set Implicit Arguments.
Unset Strict Implicit.

Inductive proc : Type :=
  | zeroP : proc
  | inP : forall A b, chan A b -> (A -> proc) -> proc
  | rinP : forall A b, chan A b -> (A -> proc) -> proc
  | outP : forall A b, chan A b -> A -> proc -> proc
  | parP : proc -> proc -> proc
  | nuP : forall A, (chan A false -> proc) -> proc
  | nuPl : forall A, (chan A true -> proc) -> proc.

(*Parameter c : (chan nat true).
Check (inP c (fun m => match m with O => zeroP | S _ => parP zeroP zeroP end)).*)

Notation "c << v >> P" := (outP c v P) (at level 40).
Notation "c ?? P" := (inP c P) (at level 40).
Notation "c ??* P" := (rinP c P) (at level 40).

Definition OutAtom (A : Set) (b : bool) (x : chan A b) (v : A) := 
  x << v >> zeroP.
Definition InAtom (A : Set) (b : bool) (x : chan A b) :=
  x ?? (fun y => zeroP).

Definition Cheq (A : Set) (a' : bool) (a : chan A a') 
  (B : Set) (b' : bool) (b : chan B b') : bool :=
  match chan_dec a b with
  | left yes => true
  | right no => false
  end.

(** transition semantics *)

Inductive TrLabel : Type :=
  | OutL : forall (A : Set) (b : bool), chan A b -> A -> TrLabel
  | InL : forall (A : Set) (b : bool), chan A b -> A -> TrLabel
  | NewL : forall (A : Set) (b : bool), chan A b -> TrLabel
  | TauL : forall (A : Set) (b : bool), chan A b -> TrLabel.

Inductive Trans : proc -> TrLabel -> proc -> Prop :=
  | tr_out : forall A b (x : chan A b) v P,
      Trans (x << v >> P) (OutL x v) P
  | tr_in : forall A b (x : chan A b) v (C : A -> proc),
      Trans (x ?? C) (InL x v) (C v)
  | tr_rin : forall A b (x : chan A b) v (C : A -> proc),
      Trans (x ??* C) (InL x v) (parP (x ??* C) (C v))
  | tr_newl : forall A (C : chan A true -> proc) (x : chan A true),
      Trans (nuPl C) (NewL x) (C x)
  | tr_new : forall A (C : chan A false -> proc) (x : chan A false),
      Trans (nuP C) (NewL x) (C x)
  | tr_comOI : forall P P' Q Q' A b (x : chan A b) v,
      Trans P (OutL x v) P' ->
      Trans Q (InL x v) Q' -> Trans (parP P Q) (TauL x) (parP P' Q')
  | tr_comIO : forall P P' Q Q' A b (x : chan A b) v,
      Trans P (InL x v) P' ->
      Trans Q (OutL x v) Q' -> Trans (parP P Q) (TauL x) (parP P' Q')
  | tr_parL : forall P P' Q L,
      Trans P L P' -> Trans (parP P Q) L (parP P' Q)
  | tr_parR : forall P P' Q L,
      Trans P L P' -> Trans (parP Q P) L (parP Q P').

(** freshness *)

Definition fresh (A : Set) (b : bool) (c : chan A b) (L : ChanList) :=
  forall (B : Set) (b' : bool) (d : chan B b'), 
    in_ChanList d L -> ~ c && d.

(** there are infinitely many non-linearized and linearized channels,
note that a process cannot use the axiom to create new channels because
Coq does not allow case analysis on type Prop:
fun x:proc => match (my_choose_fresh A x) with (exist y _) => y 
 *)
Axiom choose_fresh : forall (A : Set) (L : ChanList), 
  exists x : chan A false, fresh x L.
Axiom choose_freshl : forall (A : Set) (L : ChanList), 
  exists x : chan A true, fresh x L.

(** reduction semantics *)

Inductive RedLabel : Type :=
  | New : forall A b, chan A b -> RedLabel
  | epsilon : forall A b, chan A b -> RedLabel.

Notation "l # P" := (pairT l P) (at level 70).

Definition state := prodT ChanList proc.

Inductive Redwith : state -> RedLabel -> state -> Prop :=
  | red_com : forall L P Q A b (x : chan A b),
      Trans P (TauL x) Q -> Redwith (L # P) (epsilon x) (L # Q)
  | red_new : forall L P Q A b (x : chan A b),
      Trans P (NewL x) Q -> fresh x L -> Redwith (L # P) (New x) (x & L # Q).

Notation "P -- L --> Q" := (Redwith P L Q) (at level 50).

Set Strict Implicit.
Unset Implicit Arguments.

Definition Red (P Q : state) : Prop := exists lbl : RedLabel, Redwith P lbl Q.

(** reflexive, transitive closure *)
Inductive Reds : state -> state -> Prop :=
  | reds_b : forall P : state, Reds P P
  | reds_i : forall P Q R : state, Red P Q -> Reds Q R -> Reds P R.

Lemma reds_trans : forall P Q R, Reds P Q -> Reds Q R -> Reds P R.
  induction 1; auto.
  intro.
  apply reds_i with Q; auto.
Qed.

Inductive Reds' : state -> state -> Prop :=
  | reds_b' : forall P, Reds' P P
  | reds_i' : forall P Q R, Reds' P Q -> Red Q R -> Reds' P R.

Lemma reds'_trans : forall P Q R : state, Reds' P Q -> Reds' Q R -> Reds' P R.
intros P Q R PQ.
intro PQ'.
generalize PQ; clear PQ.
elim PQ'.
auto.
intros.
apply (reds_i' _ _ _ (H0 PQ) H1).
Qed.

Lemma reds_reds' : forall P Q : state, Reds' P Q <-> Reds P Q.
intros.
split.
intros.
induction H.
apply reds_b.
apply reds_trans with Q.
auto.
apply reds_i with R.
auto.
apply reds_b.
intros.
induction H.
apply reds_b'.
apply reds'_trans with Q.
apply reds_i' with P.
apply reds_b'.
auto.
auto.
Qed.

Lemma reds_i2 : forall P Q R : state, Reds P Q -> Red Q R -> Reds P R.
intros.
generalize (reds_reds' P R); intro.
inversion_clear H1.
apply H2.
apply reds_i' with Q.
generalize (reds_reds' P Q); intro.
inversion_clear H1.
auto.
generalize (reds_reds' Q R); intro.
tauto.
Qed.

Lemma invariant_by_red :
 forall P : state -> Prop,
 (forall Q0 Q1 : state, Red Q0 Q1 -> P Q0 -> P Q1) ->
 forall p0 pn : state, P p0 -> Reds p0 pn -> P pn.
intros.
inversion H1.
rewrite <- H3; auto.
clear H4 P0 H5 R.
cut (P Q).
(* our goal can be expressed as a property of two universally
quantified processes, we can do elimination using the induction
principle generated by Coq *)
elim H3.
intros; auto.
intros.
apply H6.
apply H with (Q0 := P0).
auto.
auto.
apply H with (Q0 := p0).
auto.
auto.
Qed.