在 Coq 证明语言中,“没有更多的子目标,但存在未实例化的存在变量”?
Posted
技术标签:
【中文标题】在 Coq 证明语言中,“没有更多的子目标,但存在未实例化的存在变量”?【英文标题】:`No more subgoals, but there are non-instantiated existential variables` in Coq proof language? 【发布时间】:2016-06-21 05:39:06 【问题描述】:我在 Coq 8.5p1 的参考手册第 11 章中关注了(不完整的)示例,关于数学/声明性证明语言。在下面的迭代等式示例(~=
和 =~
)中,我收到警告 Insufficient Justification
将 4
重写为 2+2
,并最终收到错误消息:
没有更多的子目标,但有未实例化的存在 变量:
?目标: [x: R H: x = 2 _eq0: 4 = x * x |- 2 + 2 = 4]
您可以使用抓取存在变量。
例子:
Goal forall x, x = 2 -> x + x = x * x.
Proof.
proof. Show.
let x:R.
assume H: (x = 2). Show.
have ( 4 = 4). Show.
~= (2*2). Show.
~= (x*x) by H. Show.
=~ (2+2). Show. (*Problem Here: Insufficient Justification*)
=~ H':(x + x) by H.
thus thesis by H'.
end proof.
Fail Qed.
我不熟悉 Coq 中的数学证明语言,也不明白为什么会发生这种情况。有人可以帮助解释如何修复错误吗?
--编辑-- @Vinz
在示例之前我有这些随机导入:
Require Import Reals.
Require Import Fourier.
【问题讨论】:
你能添加Require
或你使用的库来拥有这样的语法吗?
抱歉,我没有 Coq 8.5 来测试您的脚本 atm。通常,当您设法证明一个目标但某些元变量(想想类型的洞,您通常通过解决子目标来填充)没有实例化时,就会发生这种情况。
【参考方案1】:
您的证明适用于 nat
或 Z
,但对于 R
则无效。
来自 Coq Reference Manual (v8.5):
声明性证明语言的目的是采取相反的方法,中间状态总是由用户给出,但系统的转换尽可能自动化。
4 = 2 + 2
的自动化似乎失败了。我不知道哪种自动化使用声明式证明引擎,但是,例如,auto
策略无法证明几乎所有简单的等式,比如这个:
Open Scope R_scope.
Goal 2 + 2 = 4. auto. Fail Qed.
作为@ejgallego points out,我们只能偶然使用auto
证明2 * 2 = 4
:
Open Scope R_scope.
Goal 2 * 2 = 4. auto. Qed.
(* `reflexivity.` would do here *)
但是,field
策略就像一个魅力。因此,一种方法是建议使用field
策略的声明式证明引擎:
Require Import Coq.Reals.Reals.
Open Scope R_scope.
Unset Printing Notations. (* to better understand what we prove *)
Goal forall x, x = 2 -> x + x = x * x.
Proof.
proof.
let x : R.
assume H: (x = 2).
have (4 = 4).
~= (x*x) by H.
=~ (2+2) using field. (* we're using the `field` tactic here *)
=~ H':(x + x) by H.
thus thesis by H'.
end proof.
Qed.
【讨论】:
【参考方案2】:这里的问题是 Coq 的标准实数是以公理化的方式定义的。
因此,+ : R -> R -> R
和 *
等......是抽象操作,永远不会计算。这是什么意思?这意味着 Coq 没有关于如何处理 +
的规则,例如与 nat 情况相反,Coq 知道:
0 + n ~> 0
S n + m ~> S (n + m)
因此,对+
操作实数的唯一方法是手动应用表征运算符的相应公理,请参阅:
https://coq.inria.fr/library/Coq.Reals.Rdefinitions.html https://coq.inria.fr/library/Coq.Reals.Raxioms.html
这就是field, omega
等...所做的。甚至0 + 1 = 1
也不可能通过计算。
Anton 的示例 2 + 2 = 4
是偶然的。实际上,Coq 必须使用实数公理将数字 4 解析为合适的表示形式,结果 4 被解析为 Rmult (Rplus R1 R1) (Rplus R1 R1)
(更高效),这与前面等式的左侧相同。
【讨论】:
谢谢!这很有帮助!在Require Import Reals
之后应该是Unset Printing Notations.
:)以上是关于在 Coq 证明语言中,“没有更多的子目标,但存在未实例化的存在变量”?的主要内容,如果未能解决你的问题,请参考以下文章