Skip to content

Instantly share code, notes, and snippets.

@gaxiiiiiiiiiiii
Created February 3, 2024 08:39
Show Gist options
  • Save gaxiiiiiiiiiiii/4276d6849a508c19740e91ba504f593c to your computer and use it in GitHub Desktop.
Save gaxiiiiiiiiiiii/4276d6849a508c19740e91ba504f593c to your computer and use it in GitHub Desktop.
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).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment