There are some stunningly simple examples where `nia`

fails such as

```
Goal forall n m, (S (S m)) * n <> 1.
Proof. Fail nia. intros; destruct n; nia. Qed.
```

Of course here, a destruct suffices to help `nia`

.

I would like to understand why `nia`

itself cannot solve such simple looking goals.

It doesn't look that simple to me. Without the destruct, you need a parity argument to conclude (whereas, after the destruct the case n = 0 is tirivial and n >= 1 implies ((m+2)*n >= 2 which is much simpler).

Pierre Roux said:

Without the destruct, you need a parity argument to conclude.

Since `1`

is a constant, I would disagree that a parity argument is necessary; rather, a simple case analysis of `n`

.

`intros. cut (n = 0 \/ n > 0); nia.`

also works.

That is, I'm not convinced that any goal that is solvable by a simple case analysis is "difficult".

Sometimes it's hard to tell how many cases are going to be needed :smile:

Last updated: Jan 28 2023 at 05:02 UTC