pi_calc.v

From mathcomp Require Import ssreflect.
From Autosubst Require Import Autosubst.
Require Import Nat.

Inductive proc_ :=
  | Var (x : var)
  | Nil
  | Para (P Q : proc_)
  | Repl (P : proc_)
  | Send (M : proc_) (N : proc_) (P : proc_)
  | Recv (M : proc_)  (P : {bind proc_})  
  | Nu  (P : {bind proc_})
  .

Instance Ids_proc_ : Ids proc_. derive. Defined.
Instance Rename_proc_ : Rename proc_. derive. Defined.
Instance Subst_proc_ : Subst proc_. derive. Defined.
Instance SubstLemmas_proc_ : SubstLemmas proc_. derive. Qed.

Definition valid (P : proc_) : Prop :=
  match P with
  | Var _ => False
  | Send M N P => 
    match M with
    | Var _ => 
      match N with 
      | Var _ => True
      | _ => False
      end
    | _ => False
    end
  | Recv M P =>
    match M with
    | Var _ => True 
    | _ => False
    end
  | _ => True
  end.

Definition proc := {p : proc_ | valid p}.
Definition proc2proc_ : proc -> proc_ := fun P => proj1_sig P.
Coercion proc2proc_ : proc >-> proc_.

(* Instance Ids_proc : Ids proc. derive. Defined. *)
Instance Rename_proc : Rename proc. derive. Defined.
Instance Subst_proc : Subst proc. derive. Defined.
(* Instance SubstLemmas_proc : SubstLemmas proc. derive. Qed. *)

Definition Para_ (P Q : proc) : proc.
  exists (Para P Q); simpl; auto.
Defined.  

Definition Repl_ (P : proc) : proc.
  exists (Repl P); simpl; auto.
Defined.

Definition Send_ (M : var) (N : var) (P :  proc) : proc.
  exists (Send (Var M) (Var N) P); simpl; auto.
Defined.

Definition Recv_ (M : var) (P :  proc) : proc.
  exists (Recv (Var M) P); simpl; auto.
Defined.

Definition Nu_ (P : proc) : proc.
  exists (Nu P); simpl; auto.
Defined.

Definition Nil_ : proc.
  exists Nil; simpl; auto.
Defined.

Definition subst_ (σ : var -> proc) (P : proc) : proc.
Proof.
  exact (P.[σ]).
Defined.



Notation "P ‖ Q" := (Para_ P Q) (at level 30).
Notation "! P" := (Repl_ P) (at level 30).
Notation "M _[ N ]_ P" := (Send_ M N P) (at level 30).
Notation "< n >_ P" := (Recv_ n P) (at level 30).
Notation "0" := Nil_.
Notation ν_ := Nu_. 


Definition rename (σ : var -> var) (P : proc) : proc.
Proof.
  move: P => [p Hp].
  eapply exist with (p.[ren σ]).
  induction p; simpl; auto; simpl in Hp.
  - destruct p1, p2; simpl; auto.
  - destruct p; inversion Hp; simpl; auto.
Defined.  

Definition swap_ : var -> var :=
  fun x => match x with
  | O => 1
  | 1 => O
  | _ => x
  end.

Definition swap : proc -> proc := rename swap_.

Fixpoint isFree (n : var) (P : proc_) : Prop :=
  match P with 
  | Send M N' Q => 
    match M, N' with 
    | Var m, Var n' => m = n \/ n'= n \/ isFree n Q
    | _, _ => False
    end
  | Recv M Q => 
     match M with 
    | Var m => m = n \/ isFree n Q
    | _ => False
    end
  | Para P Q => isFree n P \/ isFree n Q
  | Repl P => isFree n P
  | Nu P => isFree n P  
  | _ => False
  end.

Definition isFree' (n : var) (P : proc) : Prop :=
  isFree n (proj1_sig P).

Inductive congr : proc -> proc -> Prop :=
  | para_nil P : congr (P ‖ 0) P
  | para_comm P Q : congr (P ‖ Q) (Para_ P Q)
  | para_assoc P Q R : congr (P ‖ (Q ‖ R)) ((P ‖ Q) ‖ R)
  | nu_nil : congr (ν_ 0) 0
  | nu_swap P : congr (ν_ (ν_ P)) (swap (ν_ (ν_ P)))
  | nu_free P Q : ~ isFree' O P -> congr (ν_ (P ‖ Q)) (P ‖ (ν_ Q))
  | repl_fix P : congr (! P) ((! P) ‖ P)
  | repl_nil : congr (! 0) 0
  | repl_elim P : congr (! ! P) (! P)
  | repl_para P Q : congr (! (P ‖ Q)) ((! P) ‖ (! Q)).

Notation "P ≡ Q" := (congr P Q)(at level 30).


Inductive reduct : proc -> proc -> Prop :=
  | reduct_communicate n a P Q : reduct (n _[ a ]_ P ‖ < n >_ Q) (P ‖ rename (fun x => if eqb x O then a else x) Q)
  | reduct_nu P P' : reduct P P' -> reduct (ν_ P) (ν_ P')
  | reduct_para P P' Q : reduct P P' -> reduct (P ‖ Q) (P' ‖ Q)
  | reduct_congr P P' Q Q' : P ≡ P' -> Q ≡ Q' -> reduct P P' -> reduct Q Q'.

Notation "P ⇒ Q" := (reduct P Q) (at level 30).