在 Coq 证明语言中，“没有更多的子目标，但存在未实例化的存在变量”？

Question

我在 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.

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

Answer 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)（更高效），这与前面等式的左侧相同。