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

Question

我正在关注 Coq 8.5p1 参考手册第 11 章中关于 mathematical/declarative 证明语言的（不完整）示例。在下面的迭代等式（~= 和 =~）的示例中，我收到警告 Insufficient Justification 将 4 重写为 2+2，并最终收到错误提示:

No more subgoals, but there are non-instantiated existential variables:

?Goal : [x : R H : x = 2 _eq0 : 4 = x * x |- 2 + 2 = 4]

You can use Grab Existential Variables.

示例：

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

The purpose of a declarative proof language is to take the opposite approach where intermediate states are always given by the user, but the transitions of the system are automated as much as possible.

4 = 2 + 2 的自动化似乎失败了。我不知道什么样的自动化使用声明性证明引擎，但是，例如，auto 策略无法证明几乎所有简单的等式，就像这个：

Open Scope R_scope.
Goal 2 + 2 = 4. auto. Fail Qed.

和@ejgallego 一样，我们只能偶然使用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 也不是通过计算可能的。

安东的例子 2 + 2 = 4 是偶然的。实际上，Coq 必须使用实数公理将数字 4 解析为合适的表示形式，结果 4 被解析为 Rmult (Rplus R1 R1) (Rplus R1 R1)（为了更高效），这与前面的左侧相同平等。

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

`No more subgoals, but there are non-instantiated existential variables` in Coq proof language?

coq