Coq Proof Assistant 中依赖类型的问题

考虑以下简单的表达语言：

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谓词：

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案件。我的明显猜测是：

     ...  

     match Forall_dec (WF env) wfdec es with

     ...

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

完整的工作代码如下gist https://gist.github.com/rodrigogribeiro/132e4feca910f40198242d3da3eca040.

问题是Forall_dec在标准库中被定义为不透明（即，Qed代替Defined）。因此，Coq 不知道使用wfdec已验证。

解决您的问题的直接方法是重新定义Forall_dec使其透明。您可以通过打印 Coq 生成的证明项并将其粘贴到源文件中来完成此操作。我添加了一个gist https://gist.github.com/anonymous/5b3fdc11871e42b3e9cfe006f6d8cc76这里有一个完整的解决方案。

不用说，这种方法会使代码变得臃肿、难以阅读和难以维护。正如 ejgallego 在他的回答中指出的那样，在这种情况下，最好的选择可能是定义一个布尔函数来决定WF，并用它代替WFDec。正如他所说，他的方法的唯一问题是你需要编写自己的归纳原理Exp为了证明布尔版本确实决定了归纳定义。 Adam Chlipala 的 CPDT 有一个chapter http://adam.chlipala.net/cpdt/html/InductiveTypes.html关于归纳类型，给出了这种归纳原理的例子；只需寻找“嵌套归纳类型”。