Coq证明助理中依赖类型的问题 [英] Problems with dependent types in Coq proof assistant

问题描述

考虑以下简单表达语言：

Consider the following simple expression language:

Inductive Exp : Set :=
| EConst : nat -> Exp
| EVar   : nat -> Exp
| EFun   : nat -> list Exp -> Exp.

及其格式正确的谓词：

Definition Env := list nat.

Inductive WF (env : Env) : Exp -> Prop :=
| WFConst : forall n, WF env (EConst n)
| WFVar   : forall n, In n env -> WF env (EVar n)
| WFFun   : forall n es, In n env ->
                         Forall (WF env) es ->
                         WF env (EFun n es).

基本上说明必须在环境中定义每个变量和函数符号。现在，我想定义一个表示 WF 谓词可判定性的函数：

which basically states that every variable and function symbols must be defined in the environment. Now, I want to define a function that states the decidability of WF predicate:

Definition WFDec (env : Env) : forall e, {WF env e} + {~ WF env e}.
   refine (fix wfdec e : {WF env e} + {~ WF env e} :=
             match e as e' return e = e' -> {WF env e'} + {~ WF env e'} with
             | EConst n => fun _ => left _ _
             | EVar n => fun _ =>
                      match in_dec eq_nat_dec n env with
                      | left _ _ => left _ _ 
                      | right _ _ => right _ _                    
                      end
             | EFun n es => fun _ =>
                      match in_dec eq_nat_dec n env with
                      | left _ _ => _
                      | right _ _ => right _ _                    
                      end  
             end (eq_refl e)) ; clear wfdec ; subst ; eauto.

问题在于如何声明 WF 谓词是否适用于 EFun 情况下的表达式列表。我显而易见的猜测是：

The trouble is how to state that WF predicate holds or not for a list of expressions in the EFun case. My obvious guess was:

     ...  

     match Forall_dec (WF env) wfdec es with

     ...

但是Coq拒绝了，认为递归调用 wfdec 格式错误。我的问题是：是否可以在不更改表达式表示形式的情况下定义这种格式正确的谓词的可判定性？

But Coq refuses it, arguing that the recursive call wfdec is ill-formed. My question is: Is it possible to define decidability of such wellformedness predicate without changing the expression representation?

完整的工作代码如下： 。

The complete working code is at the following gist.

推荐答案

问题是定义了 Forall_dec 在标准库中显示为不透明（即使用 Qed 而不是 Defined ）。因此，Coq不知道使用 wfdec 是有效的。

The problem is that Forall_dec is defined as opaque in the standard library (that is, with Qed instead of Defined). Because of that, Coq does not know that the use of wfdec is valid.

立即解决问题的方法是重新定义 Forall_dec 以便透明。您可以通过打印Coq生成的证明条款并将其粘贴到源文件中来实现。我在此处添加了要点，并提供了完整的解决方案。

The immediate solution to your problem is to redefine Forall_dec so that it is transparent. You can do this by printing the proof term that Coq generates and pasting it in your source file. I've added a gist here with a complete solution.

不用说，这种方法很容易膨胀，难以阅读，并且难以维护代码。正如ejgallego在他的答案中指出的那样，在这种情况下，您最好的选择是定义一个决定 WF 的布尔函数，并使用该函数代替 WFDec 。正如他所说，他的方法的唯一问题是您需要将自己的归纳原理写到 Exp ，以证明布尔型确实决定了归纳定义。 。 Adam Chlipala的CPDT在归纳类型上有一个第章，提供了这种归纳的示例原理;只是寻找嵌套归纳类型。

Needless to say, this approach lends itself to bloated, hard to read, and hard to maintain code. As ejgallego was pointing out in his answer, your best bet in this case is probably to define a Boolean function that decides WF, and use that instead of WFDec. The only problem with his approach, as he said, is that you will need to write your own induction principle to Exp in order to prove that the Boolean version indeed decides the inductive definition. Adam Chlipala's CPDT has a chapter on inductive types that gives an example of such an induction principle; just look for "nested inductive types".

这篇关于Coq证明助理中依赖类型的问题的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！