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: Oct 13 2024 at 01:02 UTC