与相关类型的勒柯克证明助理

Question

考虑下面这个简单的表达式语言问题：

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 CASE表达式的列表。我明显的猜测是：

 ... 

    match Forall_dec (WF env) wfdec es with 

    ... 

但勒柯克拒绝这一提议，认为递归调用wfdec是形成不良。我的问题是：是否可以在不改变表达式表示的情况下定义这种良好形式谓词的可判定性？

完整的工作代码位于以下gist。

Answer 1

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

您的问题的直接解决方案是重新定义Forall_dec，以便它是透明的。您可以通过打印Coq生成的证明术语并将其粘贴到源文件中来完成此操作。我在这里添加了一个gist并提供了一个完整的解决方案。不用说，这种方法使其本身变得臃肿，难以阅读并且难以维护代码。正如ejgallego在他的回答中指出的那样，在这种情况下，您最好的选择可能是定义一个布尔函数，该函数决定WF，并使用该函数代替WFDec。正如他所说的，他的方法唯一的问题是你需要编写自己的归纳原理到Exp以证明布尔版本确实决定了归纳定义。 Adam Chlipala的CPDT在归纳类型上有一个chapter，它给出了这种归纳原理的一个例子;只要寻找“嵌套归纳类型”。

Answer 2

随着时间的解决方法，你可以定义为wf：

Definition wf (env : Env) := fix wf (e : Exp) : bool := 
    match e with 
    | EConst _ => true 
    | EVar v => v \in env 
    | EFun v l => [&& v \in env & all wf l] 
    end. 

通常是这样使用起来更加方便。然而，由于Coq产生了exp的错误归纳原则，因此这个定义将毫无用处，因为它没有检测到列表。我通常做的是手动修复感应原理，但这是昂贵的。例如：

From Coq Require Import List. 
From mathcomp Require Import all_ssreflect. 

Set Implicit Arguments. 
Unset Printing Implicit Defensive. 
Import Prenex Implicits. 

Section ReflectMorph. 

Lemma and_MR P Q b c : reflect P b -> reflect Q c -> reflect (P /\ Q) (b && c). 
Proof. by move=> h1 h2; apply: (iffP andP) => -[/h1 ? /h2 ?]. Qed. 

Lemma or_MR P Q b c : reflect P b -> reflect Q c -> reflect (P \/ Q) (b || c). 
Proof. by move=> h1 h2; apply: (iffP orP) => -[/h1|/h2]; auto. Qed. 

End ReflectMorph. 

Section IN. 
Variables (X : eqType). 

Lemma InP (x : X) l : reflect (In x l) (x \in l). 
Proof. 
elim: l => [|y l ihl]; first by constructor 2. 
by apply: or_MR; rewrite // eq_sym; exact: eqP. 
Qed. 

End IN. 

Section FORALL. 

Variables (X : Type) (P : X -> Prop). 
Variables (p : X -> bool). 

Lemma Forall_inv x l : Forall P (x :: l) -> P x /\ Forall P l. 
Proof. by move=> U; inversion U. Qed. 

Lemma ForallP l : (forall x, In x l -> reflect (P x) (p x)) -> reflect (Forall P l) (all p l). 
Proof. 
elim: l => [|x l hp ihl /= ]; first by constructor. 
have/hp {hp}hp : forall x : X, In x l -> reflect (P x) (p x). 
    by move=> y y_in; apply: ihl; right. 
have {ihl} ihl := ihl _ (or_introl erefl). 
by apply: (iffP andP) => [|/Forall_inv] [] /ihl hx /hp hall; constructor. 
Qed. 

End FORALL. 

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

Lemma Exp_rect_list (P : Exp -> Type) : 
    (forall n : nat, P (EConst n)) -> 
    (forall n : nat, P (EVar n)) -> 
    (forall (n : nat) (l : seq Exp), (forall x, In x l -> P x) -> P (EFun n l)) -> 
    forall e : Exp, P e. 
Admitted. 

Definition Env := list nat. 

Definition wf (env : Env) := fix wf (e : Exp) : bool := 
    match e with 
    | EConst _ => true 
    | EVar v => v \in env 
    | EFun v l => [&& v \in env & all wf l] 
    end. 

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

Lemma WF_inv env e (wf : WF env e) : 
    match e with 
    | EConst n => True 
    | EVar n => In n env 
    | EFun n es => In n env /\ Forall (WF env) es 
    end. 
Proof. by case: e wf => // [n|n l] H; inversion H. Qed. 

Lemma wfP env e : reflect (WF env e) (wf env e). 
Proof. 
elim/Exp_rect_list: e => [n|n|n l ihe] /=; try repeat constructor. 
    by apply: (iffP idP) => [/InP|/WF_inv/InP //]; constructor. 
apply: (iffP andP) => [[/InP ? /ForallP H]|/WF_inv[/InP ? /ForallP]]. 
    by constructor => //; exact: H. 
by auto. 
Qed.