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?

Help needed with an exercise from Software Foundations. This is the theorem:
I end up with |

If you inspect |

When replaced by the When replaced by the Best, V. |

- Master Theorem with Log n recombination
- Master's theorem with f(n)=log n
- Injective pairing function
- Assert that a data constructor is injective
- Defining injective functions in Z3
- ^[\p{L}\p{N}]{1,50}$ >>> plus one rule
- with exercise in Matlab
- Looking for examples of a UI element that allows to select N elements from a set plus define a default
- Why does GHC think that this type variable is not injective?
- Find all possible injective mappings of 2 vectors
- Error in beginning exercise in SICP (Exercise 1.3)
- Understanding Bayes' Theorem
- Distributed Erlang and the CAP theorem
- Is the CAP theorem a red herring?
- Propositional Theorem Proving [closed]

© Copyright ask.programmershare.com.

Design by ask.programmershare.com

## comments:

`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`n + n = m + m`

and hypothesis`S n + S n = S m + S m`

. Did I do something wrong?