# Intuitive understanding of limits of intuition tactic in Coq

On an intuitive level, why does intuition get stuck in cases where the proof can be unblocked with a destruct?

What options are there for using a standard library tactic or defining a fairly simple custom tactic that wouldn't get stuck in this situation?

I am working my way through Software Foundations Volume 1. I meant to do it years ago, but I suppose better late than never.

Here is one theorem from the text (which is not an exercise, so posting it on a public forum like this one doesn't go against the wishes of the authors), that's given as an example in Basics.v with an aborted proof.

Theorem plus_1_neq_0_firsttry : forall n : nat,
(n + 1) =? 0 = false.


=? is defined as follows:

Notation "x =? y" := (eqb x y) (at level 70) : nat_scope.


With eqb being an equality function that takes two natural numbers and returns a bool.

The purpose of this example is to show that you can't spam simpl and call it a day.

Interestingly, you can't spam intuition either.

If we try to just use intuition, it will not complete the proof.

Theorem plus_1_neq_0_firsttry : forall n : nat,
(n + 1) =? 0 = false.
Proof.
intuition.


Here is our proof state:

1 goal (ID 91)

n : nat
============================
(n + 1 =? 0) = false


However, if I destruct once, then we can use reflexivity in each branch (as is noted later down the page).

Intuitively this makes sense. Both zero and any non-zero natural number are headed by S. It also makes sense why destructing + was necessary. Once we know that n is of the form S n', we can evaluate + one step and determine what we have a natural number headed by S on the LHS of =?.

Theorem plus_1_neq_0_firsttry : forall n : nat,
(n + 1) =? 0 = false.
Proof.
intros.
destruct n.
- reflexivity.
- reflexivity.
Qed.


In my past experience, which is admittedly very limited, intuition was pretty good at clearing simple roadblocks. I'm trying to understand what happened here.

1. Intuitively, why is intuition getting stuck before we destruct n?
2. Is there a way to automate trying a few destructs or inductions and trying intuition or another medium-to-high-powered tactic in each branch?
3. Which standard library tactics can prove this theorem by themselves?
• For 2: destruct n; intuition. Or in some cases try destruct n; intuition. For the reverse order, intuition now destruct n. They all work here but each works slightly differently from the others.
– djao
Commented Jun 12 at 4:07