我在 Coq 中定义属性时遇到困难，不知道如何处理

Question

我在 Coq 中实现了一篇论文的证明系统，如下所示。 期限证明系统

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

现在，我正在尝试证明其归一化属性，如此处所定义。 （忽略酒吧）。 归一化属性

在尝试做到这一点时，我试图实现一种证明证明是正常的方法。然而，我在这方面失败了。

我一直在尝试两种方法。一种是在称为 Normal 的证明上构建关系，并尝试在该关系上定义构造函数。我一直在尝试构建类似的东西

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

但是，我在这方面遇到了麻烦，特别是当我尝试实现任何构造函数规则时，因为 Coq 无法统一，例如 (PrivEncTerm t k) 与参数中特定的 {t: Term} （在 dy 中使用） Xt）。

我一直在尝试的另一种方法是定义一个计算来计算证明是否正常，但是，当我这样做时，我遇到了一些奇怪的类型错误。

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.

奇怪的类型错误

所讨论的“bool 类型的 true”位于 splitL 情况下匹配的最后一个分支（ax 分支）中。

当我觉得功能本身没问题时，我不知道如何解决这个问题。任何有关这两种方法中任何一种的建议将不胜感激，

Answer 1

（请始终给出编译的内容，直到出现您想要指出的错误）。

两点备注：

首先，你不能定义一个函数来计算（dy，在）Prop 中，以产生（bool，在）Type 中的东西。因此，即使您修复了看到的错误消息，您的定义也会失败。见下文。

其次，您正在定义依赖模式匹配，并且类型检查器需要一些帮助来确定分支的类型。这里一个简单的

return bool

似乎就可以解决问题。但正如您所看到的，由于“消除不正确”，您的定义失败了。因此，要么将

ty

转换为

Type

而不是

Prop

，要么将 isNormal 定义为归纳法。让我提一下第三个选项：你返回

True

和

False

而不是

true

和

false

（这样你就可以从 Ptop 消除到 Prop），但这对于初学者来说相当混乱（与感应）。

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 := (* change to Type here to solve the error below*)
| 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).




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 return bool 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.