2

I have a pretty basic expression involving real number literals and +, namely the fact that 4 = 1 + 1 + 1 + 1.

I'm trying to figure out how to prove this fact using as little cleverness as possible.

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.

I attempted to prove it by using strategically chosen assertions and spamming intuition, but I can't seem to build integral reals above 3 using that technique.

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.

leaves me in the proof state

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
Greg Nisbet
  • 6,710
  • 3
  • 25
  • 65

1 Answers1

2

Based on this answer, it looks like the field tactic will work. I'm not sure if that's too much cleverness.

Require Export RIneq.

Open Scope R_scope.

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

(Tested in Coq 8.9+beta1)

SCappella
  • 9,534
  • 1
  • 26
  • 35
  • Why not use the more generic `Require Import Reals.` This gives all the general tools to result about numeric expressions. For an equality between expression (not necessarily linear), the right answer should be `ring` which is slightly simpler than `field`. It is worthwhile learning about this tactic, because it is very predictable: *it solves any equality that is true modulo associativity, commutativity, cancellation, of addition, multiplication, subtraction*. – Yves Jan 15 '19 at 07:11
  • The tactic `field` proposed here is slightly more powerful than `ring` as it also deals with *division*, but this is trickier because it needs to check that denominators are not zero. – Yves Jan 15 '19 at 07:20