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, используя эту технику.

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

Исходя из этого ответа, похоже, что тактика field сработает. Я не уверен, что это слишком умно.

Require Export RIneq.

Open Scope R_scope.

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

(протестировано в Coq 8,9 + бета1)