Coq证明助手中依赖类型的问题

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

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.

问题是Forall_dec在标准库中被定义为不透明(即,使用Qed而不是Defined).因此,Coq不知道使用wfdec是有效的.

您问题的直接解决方案是重新定义Forall_dec,使其透明.您可以通过打印Coq生成的证明术语并将其粘贴到源文件中来完成此操作.我在这里添加了一个完整的解决方案.

毋庸置疑,这种方法适用于膨胀,难以阅读和难以维护的代码.正如ejgallego在他的回答中指出的那样,在这种情况下你最好的选择可能是定义一个决定WF的布尔函数,并使用它来代替WFDec.正如他所说,他的方法唯一的问题是你需要将自己的归纳原理写入Exp,以证明布尔版本确实决定了归纳定义. Adam Chlipala的CPDT在感应类型上有chapter,它提供了这种感应原理的一个例子;只是寻找“嵌套的归纳类型”.