coq - Coq 证明语言中的 `No more subgoals, but there are non-instantiated existential variables`？

Question

我正在遵循 Coq 8.5p1 引用手册第 11 章中有关数学/声明性证明语言的(不完整)示例。在下面的迭代等式示例中( ~= 和 =~ )，我收到警告 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 中的数学证明语言，无法理解为什么会发生这种情况。有人可以帮助解释如何修复该错误吗？

--编辑-- @文兹

在示例之前我有这些随机导入:

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