Why 'intuition' works in the example of Coq?

Question

My question is: why 'intuition' works in my example?

I'm trying to prove

Lemma eqb_false : forall n m : nat, eqb n m = false -> n <> m.

At the last step, I can see

n : nat
IHn : forall m : nat, (n =? m) = false -> n <> m
m : nat
IHm : (S n =? m) = false -> S n <> m
============================
 (n =? m) = false -> S n <> S m

Then 'intuition'/'firstorder'/'auto' all work on the current goal.

But why do they work? The Coq manual says they will some search work. Does it mean it can be rewritten with some other simple tactics?

Thank you!

EDIT: It can be seen that I applied induction on n and m in the proof above. According to @Vinz's answer, it has no necessity to conduct such an induction process. intros at the first step and intro at the goal of n <> m, it will generate a contradictory hypothesis to H.

Vinz Vinz · Accepted Answer · 2015-05-19T14:04:13

Tactics like intuition, firstorder or auto try to solve your goal with some automatic reasoning, but you can always replace one of their proofs by one you crafted by hand.

In previous version of Coq, you could do info intuition to get the proof script, but I heard it doesn't work anymore. Maybe you could try it. You can always Show Proof after intuition to get the proof term, but it won't give you the tactics used.

In your particular case, the proof is quite easy by introducing the S n = S m from the end of your goal, using injection on it to get n = m in the context, and then derive a contradiction with (n =? m) = false.

EDIT for xywang: any statement of the shape A <> B is just syntactic sugar for A = B -> False. Therefore, the intros tactic can be applied to any goal P1 -> ... Pn -> A <> B, with n+1 (note the +1) names. For example consider:

=============================
 P -> Q -> A <> B

by applying the tactic intros p q eqAB., the goal becomes

p : P
q : Q
eqAB : A = B
=============================
False

Why 'intuition' works in the example of Coq?

1 Answers