在Coq中定义证明系统规范性属性的两类实现难题

问题背景 #

已在Coq中实现论文中的证明系统，代码如下：

Require Import Ensembles.

Definition Var := nat.
Definition Name := nat.

Inductive Term: Type :=
| VarTerm (v: Var)
| PrivKeyTerm (k: Name)
| PubKeyTerm (k: Name)
| PairTerm (t1 t2: Term)
| PrivEncTerm  (t: Term) (k: Name)
| PubEncTerm (t: Term) (k: Name).

Definition TermSet: Type := Ensemble Term.


Inductive dy : TermSet -> Term -> Prop:=
| ax {X: TermSet} {t: Term} (inH: In Term X t) : dy X t
| pk {X: TermSet} {k: Name} (kH: dy X (PrivKeyTerm k)) : dy X (PubKeyTerm k)
                                                           
| splitL {X: TermSet} {t1 t2: Term} (splitH: dy X (PairTerm t1 t2)) : dy X t1
| splitR {X: TermSet} {t1 t2: Term} (splitH: dy X (PairTerm t1 t2)) : dy X t2
| pair {X: TermSet} {t1 t2: Term} (tH: dy X t1) (uH: dy X t2) : dy X (PairTerm t1 t2)
                                                               
| sdec {X: TermSet} {t: Term} {k: Name} (encH: dy X (PrivEncTerm t k)) (kH: dy X (PrivKeyTerm k)): dy X t
| senc {X: TermSet} {t: Term} {k: Name} (tH: dy X t) (kH: dy X (PrivKeyTerm k)) : dy X (PrivEncTerm t k)
                                                                                     
| adec {X: TermSet} {t: Term} {k: Name} (encH: dy X (PubEncTerm t k)) (keyH: dy X (PrivKeyTerm k)): dy X t
| aenc {X: TermSet} {t: Term} {k: Name} (tH: dy X t) (kH: dy X (PubKeyTerm k)) : dy X (PubEncTerm t k).

当前目标是证明该系统的规范性属性，尝试两种方法均受阻：

遇到的问题 #

1. 归纳定义Normal关系的类型统一问题 #

尝试定义如下归纳关系时，Coq无法完成类型统一（例如无法将PrivEncTerm t k与dy X t中的t统一）：

Inductive Normal {X: TermSet} {t: Term} : dy X t -> Prop := (* .. *),

2. isNormal计算函数的类型错误问题 #

尝试定义计算函数isNormal时出现类型错误，已知错误原因但不愿修改dy的定义，转而尝试让isNormal返回Prop仍未成功：

Fixpoint isNormal {X: TermSet} {t: Term} (proof: dy X t) : bool := 
  match proof with
  | pair p1 p2 => andb (isNormal p1) (isNormal p2)
  | senc pt pK => andb (isNormal pt) (isNormal pK)
  | aenc pt pK => andb (isNormal pt) (isNormal pK)
  | pk pK => isNormal pK
                       
  | ax _ => true
  | splitL p =>  andb (isNormal p) (match p with | pair _ _ => false
                                           | senc _ _ => false
                                           | aenc _ _ => false
                                           | pk _ => false
                                          
                                           | splitL _ => true
                                           | splitR _ => true
                                           | sdec _ _ => true
                                           | adec _ _ => true
                                                           | ax _ => true
                                   end)
  | splitR p => andb (isNormal p) (match p with | pair _ _ => false
                                           | senc _ _ => false
                                           | aenc _ _ => false
                                           | pk _ => false
                                           | _ => true
                                   end)
  | sdec pe pK => andb (isNormal pe) (andb (isNormal pK) (match pe with | pair _ _ => false
                                                                   | senc _ _ => false
                                                                   | aenc _ _ => false
                                                                   | pk _ => false
                                                                   | _ => true
                                                          end))
  | adec pe pK => andb andb (isNormal pe) (andb (isNormal pK) (match pe with | pair _ _ => false
                                                                        | senc _ _ => false
                                                                        | aenc _ _ => false
                                                                        | pk _ => false
                                                                        | _ => true end))
end.

技术指导 #

针对归纳定义Normal的类型统一问题 #

问题核心在于Normal的参数绑定方式：当前定义中X和t是固定的，但dy的构造子（如sdec）会关联不同的t（比如sdec的前提是dy X (PrivEncTerm t k)，结论是dy X t），导致归纳子句中出现类型不匹配。

解决方法是调整Normal的参数结构，让它不固定X和t，而是对任意X和t的dy X t证明树定义规范性：

Inductive Normal {X: TermSet} : forall t, dy X t -> Prop :=
  | Normal_ax {t} (inH: In Term X t) : Normal t (ax inH)
  | Normal_pk {k} (kH: dy X (PrivKeyTerm k)) (n: Normal (PrivKeyTerm k) kH) : Normal (PubKeyTerm k) (pk kH)
  | Normal_splitL {t1 t2} (splitH: dy X (PairTerm t1 t2)) (n: Normal (PairTerm t1 t2) splitH) : Normal t1 (splitL splitH)
  | Normal_splitR {t1 t2} (splitH: dy X (PairTerm t1 t2)) (n: Normal (PairTerm t1 t2) splitH) : Normal t2 (splitR splitH)
  | Normal_pair {t1 t2} (tH: dy X t1) (uH: dy X t2) (n1: Normal t1 tH) (n2: Normal t2 uH) : Normal (PairTerm t1 t2) (pair tH uH)
  | Normal_sdec {t k} (encH: dy X (PrivEncTerm t k)) (kH: dy X (PrivKeyTerm k)) (n_enc: Normal (PrivEncTerm t k) encH) (n_k: Normal (PrivKeyTerm k) kH) : Normal t (sdec encH kH)
  | Normal_senc {t k} (tH: dy X t) (kH: dy X (PrivKeyTerm k)) (n_t: Normal t tH) (n_k: Normal (PrivKeyTerm k) kH) : Normal (PrivEncTerm t k) (senc tH kH)
  | Normal_adec {t k} (encH: dy X (PubEncTerm t k)) (keyH: dy X (PrivKeyTerm k)) (n_enc: Normal (PubEncTerm t k) encH) (n_key: Normal (PrivKeyTerm k) keyH) : Normal t (adec encH keyH)
  | Normal_aenc {t k} (tH: dy X t) (kH: dy X (PubKeyTerm k)) (n_t: Normal t tH) (n_k: Normal (PubKeyTerm k) kH) : Normal (PubEncTerm t k) (aenc tH kH)
  (* 可补充规范性核心约束：比如禁止splitL的前提是pair构造，需在归纳子句中添加对应条件 *)

关键是让Normal量化t，这样每个构造子可以处理dy中不同t之间的关联，解决类型统一问题。

针对isNormal函数的类型错误问题 #

原代码的类型错误源于：在match p with分支中，p的类型是dy X T（比如splitL p中的p类型是dy X (PairTerm t1 t2)），但模式匹配试图匹配所有dy构造子，而有些构造子的结论t与当前p的t不兼容，导致Coq无法推断类型。

如果不想修改dy，可改用依赖模式匹配，或直接使用上述归纳定义的Prop版本（更适合后续规范性证明）。若坚持用计算函数，可使用Program Fixpoint配合终止度量实现：

Require Import Program.
Require Import Lia.

(* 定义证明树的大小度量 *)
Fixpoint dy_size {X: TermSet} {t: Term} (d: dy X t) : nat :=
  match d with
  | ax _ => 1
  | pk d => 1 + dy_size d
  | splitL d => 1 + dy_size d
  | splitR d => 1 + dy_size d
  | pair d1 d2 => 1 + dy_size d1 + dy_size d2
  | sdec d1 d2 => 1 + dy_size d1 + dy_size d2
  | senc d1 d2 => 1 + dy_size d1 + dy_size d2
  | adec d1 d2 => 1 + dy_size d1 + dy_size d2
  | aenc d1 d2 => 1 + dy_size d1 + dy_size d2
  end.

Program Fixpoint isNormal {X: TermSet} {t: Term} (proof: dy X t) : bool := 
  match proof with
  | pair p1 p2 => andb (isNormal p1) (isNormal p2)
  | senc pt pK => andb (isNormal pt) (isNormal pK)
  | aenc pt pK => andb (isNormal pt) (isNormal pK)
  | pk pK => isNormal pK
  | ax _ => true
  | splitL p => andb (isNormal p) 
                (match p in dy _ T return bool with
                 | pair _ _ => false
                 | _ => true
                 end)
  | splitR p => andb (isNormal p) 
                (match p in dy _ T return bool with
                 | pair _ _ => false
                 | _ => true
                 end)
  | sdec pe pK => andb (isNormal pe) (andb (isNormal pK) 
                   (match pe in dy _ T return bool with
                    | senc _ _ => false
                    | _ => true
                    end))
  | adec pe pK => andb (isNormal pe) (andb (isNormal pK) 
                   (match pe in dy _ T return bool with
                    | aenc _ _ => false
                    | _ => true
                    end))
  end.
Next Obligation.
  lia. (* 证明递归调用的size更小 *)
Qed.

这里用in dy _ T的依赖模式匹配明确约束匹配的T类型，避免类型错误，同时用Program Fixpoint配合dy_size度量保证递归终止。

核心思路总结 #

• 归纳定义规范性时，必须让关系量化dy中的t参数，处理不同构造子之间的类型关联；
• 计算性函数需要用依赖模式匹配处理dy的依赖类型，同时提供终止度量；
• 优先考虑归纳定义的Prop版本（即Normal关系），因为它更适合后续的规范性证明（如证明所有可推导的项都有规范形式）。

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