CaptureAboidSubst.v

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 σ) σ.