如何证明(2^2)%R=4%R。

Question

如何在Coq中证明以下内容？

Require Import Coq.Reals.Reals.

Definition f (x:R) :R := pow x 2.

Lemma f_2: f 2 = 4%R.
Proof.
Admitted.

Answer 1

方法1：使用强大的策略。

该 ring 手段强大到可以轻易统一 2^2 和 4. 你要展开 f 因为它不是环形操作，不过。

Lemma f_2: f 2 = 4%R.
Proof.
  unfold f.
  ring.
Qed.

---

方法2：硬道理。要看清简单语句中隐含的所有内容 f 2 = 4，暂时关闭记号会有帮助。我还打开了范围 R_scope 所以，我不需要 %R 后缀无处不在。

我们得到这样的东西 eq (f (IZR (Zpos (xO xH)))) (IZR (Zpos (xO (xO xH))))

IZR 是将整数转化为实数的函数。让我们来展开一下，还有就是 f.

现在我们可以把记号打开，然后我们就可以得到 IPR 2 ^ 2 = IPR 4 为目标。所以继续通过展开 IPR. (IPR 转换 积极的 整数到实数）。)

其目标是 IPR_2 1 ^ 2 = IPR_2 2. IPR_2 也是将正整数转换为实数，但引入了一个2的因子。 它基本上是一个方便的函数，用于 IPR. 把它也展开。

最后我们就到了基本常数。我们的目标是 (R1 + R1) ^ 2 = (R1 + R1) * (R1 + R1). 让我们简化权力。简化策略之一，如 cbn 会工作。目标变成了 (R1 + R1) * ((R1 + R1) * 1) = (R1 + R1) * (R1 + R1). 所以最后，我们可以使用 x * 1 = x. 寻找 "*" (最好是： Search (?x * 1 = ?x).)，我发现 Rmult_1_r 是我们想要的。使用 rewrite Rmulti_1_r 然后 reflexivity.

Lemma f_2: f 2 = 4.
Proof.
  unfold f, IZR.
  unfold IPR.
  unfold IPR_2.
  cbn.
  (* Search (?x * 1 = ?x). *)
  rewrite Rmult_1_r.
  reflexivity.
Qed.

当然，所有这些展开步骤都是纯粹的计算，所以我们可以跳到最后，说一些类似于 change 4 with (2 * 2).但这绝对不是很明显 4 被定义为 2 * 2 除非你已经熟悉整数是如何转移到实数的。

Lemma f_2: f 2 = 4.
Proof.
  unfold f; cbn.
  change 4 with (2 * 2).
  rewrite Rmult_1_r.
  reflexivity.
Qed.

Answer 2

你首先需要公开函数的定义。f 通过 "展开 "它。

Require Import Coq.Reals.Reals.  (* "Require Import Reals." would be OK as well. *)
Definition f (x : R) : R := pow x 2.

Lemma f_2 : f 2 = 4%R.
Proof.
unfold f.

那么你就会得到。

1 subgoal

  ============================
  (2 ^ 2)%R = 4%R

而一个成语的方式是将这一目标排出 公理化实数 是依靠 ring 战术。

ring.
Qed.

关于这一战术的更多细节，请参见： 官方Coq文档.