如何证明Coq中Pi演算的Nil进程无法执行迁移？

进程与动作定义 #

Inductive proc : Type :=
| In (n : nat) (p : proc)
| Out (n m : nat) (p : proc)
| Res (p : proc)
| Rep (p : proc)
| Par (p q : proc)
| Nil.


Inductive act : Set :=
  | a_tau : act
  | a_out: nat -> nat -> act
  | a_in: nat -> nat -> act
  | a_bout: nat -> act.

迁移系统定义 #

Reserved Notation "P -( a )> Q" (at level 70).
Inductive trans: proc -> act -> proc -> Prop := 
  | OUT   (n m : nat) (P : proc): 
    trans (Out n m P) (a_out n m) P
  | IN    (n m : nat) (P: proc): 
    trans (In n P) (a_in n m) (P[[m |> id]])
  | PAR1 (a : act) (n m : nat) (P Q R: proc):
    a = a_in n m \/ a = a_tau \/ a = a_out n m ->
    trans P a R -> trans (Par P Q) a (Par R Q)
  | PAR2  (a : act) (n : nat) (P Q R : proc):
    trans P (a_bout n) R -> trans (Par P Q) (a_bout n) (Par R (Q[[shift]]))
  | RES1  (n : nat) (P R : proc):
    trans P (a_out (n + 1) 0 ) R -> trans (Res P) (a_bout n) R
  | RES21 (a : nat -> nat -> act) (n m : nat) (P Q : proc) :
    a = a_out \/ a = a_in ->
    trans P (a (n + 1) (m + 1)) Q -> 
    trans (Res P) (a_out n m) (Res Q)
  | RES22 (P Q : proc) :
    trans P (a_tau) Q -> 
    trans (Res P) (a_tau) (Res Q)
  | RESBOUT (n : nat) (P Q : proc) :
    trans P (a_bout (n+1)) Q -> trans (Res P) (a_bout n) (Res (Q[[swap]]))
  | COM11  (n m : nat) (P Q R S : proc) :
    trans P (a_in n m) R ->
    trans Q (a_out n m) S ->
    trans (Par P Q) a_tau (Par (R) S)
  | COM12  (n m : nat) (P Q R S : proc) :
    trans P (a_out n m) R ->
    trans Q (a_in n m) S ->
    trans (Par P Q) a_tau (Par R (S))
  | COM21  (n : nat) (P Q R S : proc) :
    trans P (a_in n 0) R ->
    trans Q (a_bout n) S 
  | COM22  (n : nat) (P Q R S : proc) :
    trans P (a_bout n) R ->
    trans Q (a_in n 0) S ->
    trans (Par P Q) a_tau (Res (Par R S))
  | REP   (a : act) (P Q: proc) : 
    trans (Par P (Rep P)) a Q -> trans (Rep P) a Q
 
  where "P -( a )> Q" := (trans P a Q).

待证引理与当前困境 #

尝试证明Nil进程无法执行任何迁移：

Lemma Nil_transition_less : forall P a, ~(Nil -(a)> P).

使用inversion策略后：

Lemma Nil_transition_less : forall P a, ~(Nil -(a)> P).
Proof. intros. intro H. inversion H.

得到目标状态：

1 goal
P : proc
a : act
H : Nil -( a )> P
n : nat
P0, Q, R, S : proc
H0 : P0 -( a_in n 0 )> R
H1 : Q = Nil
H2 : a_bout n = a
H3 : S = P
______________________________________(1/1)
False

问题分析与解决方案 #

1. 迁移系统的语法错误 #

首先注意到COM21构造子存在语法错误：它仅给出了前提条件，未定义对应的迁移结论（缺少trans (Par P Q) ...部分）。这会导致Coq的归纳类型定义不完整，进而在inversion时产生异常目标。需要修正COM21的定义，补充结论部分，参考COM22的结构：

| COM21  (n : nat) (P Q R S : proc) :
    trans P (a_in n 0) R ->
    trans Q (a_bout n) S ->
    trans (Par P Q) a_tau (Res (Par R S))

2. 完成引理证明 #

修正迁移系统后，重新执行证明。对于inversion H生成的所有子目标，只需使用discriminate策略即可完成证明——每个子目标都会包含与Nil构造子矛盾的进程结构假设，discriminate可直接利用归纳类型构造子的互斥性导出False。

完整证明代码：

Lemma Nil_transition_less : forall P a, ~(Nil -(a)> P).
Proof.
  intros P a H.
  inversion H; discriminate.
Qed.

若不修正COM21，即使继续处理当前目标，也会因规则本身的不完整性导致后续证明出现更多问题，因此优先修正迁移系统定义是关键。

内容的提问来源于stack exchange，提问作者Nikolaj Kristensen