Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Why 'intuition' works in the example of Coq?

Tags:

coq

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.

like image 345
xywang Avatar asked May 19 '15 11:05

xywang


People also ask

What does Simpl do in Coq?

simpl: Simplifies the goal or hypotheses in the context. unfold: Unfolds the definitions of terms. apply: Uses implications to transform goals and hypotheses. rewrite: Replaces a term with an equivalent term if the equivalence of the terms has already been proven.

What are Coq tactics?

Tactics specify how to transform the proof state of an incomplete proof to eventually generate a complete proof. Proofs can be developed in two basic ways: In forward reasoning, the proof begins by proving simple statements that are then combined to prove the theorem statement as the last step of the proof.


1 Answers

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
like image 88
Vinz Avatar answered Sep 22 '22 11:09

Vinz