Coq 证明助手中依赖类型的问题
Problems with dependent types in 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.
作为临时解决方法，您可以将 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.
问题是 Forall_dec 在标准库中被定义为不透明的（即 Qed 而不是 Defined）。因此，Coq 不知道 wfdec 的使用是有效的。
您的问题的直接解决方案是重新定义 Forall_dec 以使其透明。您可以通过打印 Coq 生成的证明项并将其粘贴到您的源文件中来完成此操作。我在这里添加了一个完整的解决方案 gist。
不用说，这种方法会使代码变得臃肿、难以阅读和维护。正如 ejgallego 在他的回答中指出的那样，在这种情况下，您最好的选择可能是定义一个决定 WF 的布尔函数，并使用它而不是 WFDec。正如他所说，他的方法的唯一问题是您需要将自己的归纳原理写入 Exp 以证明布尔版本确实决定了归纳定义。 Adam Chlipala 的 CPDT 有一个关于归纳类型的 chapter，它给出了这种归纳原理的一个例子；只需查找 "nested inductive types"。
考虑以下简单的表达式语言：
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.
作为临时解决方法，您可以将 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.
问题是 Forall_dec 在标准库中被定义为不透明的（即 Qed 而不是 Defined）。因此，Coq 不知道 wfdec 的使用是有效的。
您的问题的直接解决方案是重新定义 Forall_dec 以使其透明。您可以通过打印 Coq 生成的证明项并将其粘贴到您的源文件中来完成此操作。我在这里添加了一个完整的解决方案 gist。
不用说，这种方法会使代码变得臃肿、难以阅读和维护。正如 ejgallego 在他的回答中指出的那样，在这种情况下，您最好的选择可能是定义一个决定 WF 的布尔函数，并使用它而不是 WFDec。正如他所说，他的方法的唯一问题是您需要将自己的归纳原理写入 Exp 以证明布尔版本确实决定了归纳定义。 Adam Chlipala 的 CPDT 有一个关于归纳类型的 chapter，它给出了这种归纳原理的一个例子；只需查找 "nested inductive types"。