## Stream: Coq users

### Topic: Tricky nia goals

#### Andrej Dudenhefner (Apr 13 2021 at 09:35):

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.

#### Pierre Roux (Apr 13 2021 at 11:12):

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).

#### Andrej Dudenhefner (Apr 13 2021 at 11:19):

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.

#### Andrej Dudenhefner (Apr 13 2021 at 11:20):

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

#### Cody Roux (Apr 13 2021 at 15:07):

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

Last updated: Jun 18 2024 at 07:01 UTC