Skip to content

Instantly share code, notes, and snippets.

@gaxiiiiiiiiiiii
Created February 9, 2024 09:43
Show Gist options
  • Save gaxiiiiiiiiiiii/5cd39405ca22746060b49c163d4c0182 to your computer and use it in GitHub Desktop.
Save gaxiiiiiiiiiiii/5cd39405ca22746060b49c163d4c0182 to your computer and use it in GitHub Desktop.
From mathcomp Require Import ssreflect.
Require Import Nat.
Definition name := nat.
Inductive proc :=
| Nil
| Tau (P : proc)
| Para (P Q : proc)
| Sum (P Q : proc)
| Repl (P : proc)
| Send (M N : name) (P : proc)
| Recv (M: name) (N : name) (P : proc)
| Nu (M : name) (P : proc)
| Match (x y : name)(P : proc)
.
Definition Subst := name -> name.
Definition isSupp (σ : Subst) x := (σ x <> x).
Definition isCosupp (σ : Subst) y := exists x, y = σ x /\ isSupp σ x.
Axiom MaxSubst : Subst -> name.
Axiom MaxSubst_Supp : forall σ, isSupp σ (MaxSubst σ).
Axiom MaxSubst_Max : forall σ x, isCosupp σ x -> x < MaxSubst σ.
Axiom namesOf : Subst -> name -> bool.
Axiom namesOfT : forall σ x, namesOf σ x = true <-> isSupp σ x \/ isCosupp σ x.
Axiom namesOfF : forall σ x, namesOf σ x = false <-> ~ (isSupp σ x \/ isCosupp σ x).
Fixpoint isFree (P: proc) (n : name) : bool :=
match P with
| Nil => false
| Tau P => isFree P n
| Para P Q => isFree P n || isFree Q n
| Sum P Q => isFree P n || isFree Q n
| Repl P => isFree P n
| Send M N P => isFree P n || (n =? M) || ( n =? N)
| Recv M N P => isFree P n || (n =? M)
| Nu M P => isFree P n
| Match x y P => isFree P n || (n =? x) || (n =? y)
end.
Fixpoint isBound (P: proc) (n : name) : bool :=
match P with
| Nil => false
| Tau P => isBound P n
| Para P Q => isBound P n || isBound Q n
| Sum P Q => isBound P n || isBound Q n
| Repl P => isBound P n
| Send M N P => isBound P n
| Recv M N P => isBound P n || (n =? N)
| Nu M P => isBound P n || (n =? M)
| Match x y P => isBound P n
end.
Definition rename (x n m : name) : name :=
if x =? n then m else x.
Definition maxBound (P : proc) (n : name) : name :=
match P with
| Recv _ N P => max n N
| Nu N _ => max n N
| _ => n
end.
Fixpoint maxName (P : proc) (n : name) : name :=
match P with
| Nil => n
| Tau P => maxName P n
| Para P Q => maxName Q (maxName P n)
| Sum P Q => maxName Q (maxName P n)
| Repl P => maxName P n
| Send M N P => max M (max N (maxName P n))
| Recv M N P => max M (max N (maxName P n))
| Nu M P => max M (maxName P n)
| Match x y P => max x (max y (maxName P n))
end.
Fixpoint renameBound (P : proc) (n m : name) : proc :=
match P with
| Nil => Nil
| Tau P => Tau (renameBound P n m)
| Para P Q => Para (renameBound P n m) (renameBound Q n m)
| Sum P Q => Sum (renameBound P n m) (renameBound Q n m)
| Repl P => Repl (renameBound P n m)
| Send M N P => Send M N (renameBound P n m)
| Recv M N P => Recv M (rename N n m) (renameBound P n m)
| Nu N P => Nu (rename N n m) (renameBound P n m)
| Match x y P => Match x y (renameBound P n m)
end.
Definition fresh (P : proc) (σ : Subst) : name :=
S (max (maxName P 0) (MaxSubst σ)).
Fixpoint convert_aux (P : proc) (σ : Subst) (n : name) : proc :=
match n with
| O => P
| S n' =>
if isFree P n && namesOf σ n
then convert_aux (renameBound P n (fresh P σ)) σ n'
else P
end.
Definition convert P σ := convert_aux P σ (maxBound P 0).
Fixpoint subst_aux (P : proc) (σ : Subst) : proc :=
match P with
| Nil => Nil
| Tau P => Tau (subst_aux P σ)
| Para P Q => Para (subst_aux P σ) (subst_aux Q σ)
| Sum P Q => Sum (subst_aux P σ) (subst_aux Q σ)
| Repl P => Repl (subst_aux P σ)
| Send M N P => Send (σ M) (σ N) (subst_aux P σ)
| Recv M N P => Recv (σ M) (σ N) (subst_aux P σ)
| Nu N P => Nu (σ N) (subst_aux P σ)
| Match x y P => Match (σ x) (σ y) (subst_aux P σ)
end.
Definition subst P σ := subst_aux (convert P σ) σ.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment