Theorem plus_n_n_injective, exercise

Tag: coq Author: liujaingtao Date: 2014-03-31

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?

Best Answer

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.

comments:

Could you please elaborate on the destruct and inversion tactic?
destruct n. does case analysis on n, exposing one case for each constructor of n's type. inversion does case analysis while preserving facts about n's indices. You should be able to learn about them in any decent Coq introduction. For instance, this chapter of CPDT covers inversion: adam.chlipala.net/cpdt/html/Predicates.html
OK, thanks. Now I'm stuck at another place, with goal n + n = m + m and hypothesis S n + S n = S m + S m. Did I do something wrong?

Other Answer1

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.