Coq证明了涉及实数文字的算术表达式是相等的。

Question

我有一个非常基本的表达式，涉及实数文本和+，即4 = 1 + 1 + 1 + 1。

我想弄清楚如何用尽可能少的聪明来证明这个事实。

Require Export RIneq. (* probably overkill, but it pulls in
                         enough real number stuff to be useful *)

Open Scope R_scope.

Lemma test_sum2 : 4 = 1 + 1 + 1 + 1.

我试图通过使用战略性选择的断言和垃圾邮件intuition来证明这一点，但我似乎无法使用该技术在3之上构建整体reals。

Require Export RIneq.

Open Scope R_scope.

Lemma test_sum2 : 4 = 1 + 1 + 1 + 1.
Proof.
assert (1 + 1 = 2).
intuition.
rewrite H.
assert (1 + 2 = 3).
intuition.
assert (1 + 2 = 2 + 1).
intuition.
rewrite H1 in H0.
rewrite H0.
assert (1 + 3 = 3 + 1).
intuition.

让我处于证据状态

1 subgoal
H : 1 + 1 = 2
H0 : 2 + 1 = 3
H1 : 1 + 2 = 2 + 1
H2 : 1 + 3 = 3 + 1
______________________________________(1/1)
4 = 3 + 1

Answer 1

根据this的回答，field的策略看起来是可行的。我不确定这是不是太聪明了。

Require Export RIneq.

Open Scope R_scope.

Lemma test_sum2 : 4 = 1 + 1 + 1 + 1.
Proof.
  field.
Qed.

(用Coq 8.9+beta1测试)