如何证明（2 ^ 2）％R = Coq中的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

您首先需要通过“展开”功能来公开功能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.

有关此策略的更多详细信息，请参见official Coq doc。

Answer 2

方法1：使用强大的战术。