與相關類型的勒柯克證明助理

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.