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
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.
1 is a constant, I would disagree that a parity argument is necessary; rather, a simple case analysis of
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