Theorem plus_n_n_injective, exercise

Question

Help needed with an exercise from Software Foundations. This is the theorem:

Theorem plus_n_n_injective : ∀n m,
 n + n = m + m →
 n = m.
Proof.

I end up with n = 0 as goal and n + n = 0 as hypothesis. How to move on?

Answer 1

If you inspect n (destruct it), it's either going to be 0 in which case the goal is provable by reflexivity, or S n' in which case the hypothesis is contradictory by congruence/inversion.

Answer 2

n + n cannot be simplified further because n is a variable, not a type constructor. You can expose all the construction cases of n by destructing it as Ptival said. However using inversion in this context seems to me a bit extreme and not what this Sf exercise is about.

When replaced by the O constructor, O + O will reduce (using simpl for example) to O and reflexivity should do the trick.

When replaced by the S constructor, S foo + bar will always reduce to the shape S something, which can't be equal to O (the easiest way to assert that is by using discriminate) because they are two constructors of the same type.

Best, V.

Answer 3

The trick to solving this problem can be garnered from the Theorem for length_snoc' previously shown in the same chapter.

As this was the first time so far in the book that introducing some of the variable/hypothesis after doing an induction on n, this may come off as unusual to newcomers (like me). This allows you to get a more general hypotheses in your context after proving for the base case.

As mentioned before, you will be able to prove some goals simply by reflexivity. Some of them can be proven by inversion on a false hypotheses in your context(those should become straightforward once you spot them, the idea that 2 + 2 = 5 -> anything is true can go a long way).

Finally, you will have to rework one of your hypotheses using the previously defined lemmas plus_n_Sm and eq_add_S as well as symmetry to be able to apply the more general hypotheses we discussed earlier.