The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Mon, 6 May 2013 10:00:07 +0200 (CEST),
mtkhan AT risc.uni-linz.ac.at
 a écrit :

> Hi,
> 
> Thanks Adam and others for the suggestions. I will be
> grateful, if you can also provide the guidelines for
> the proving strategy of contradictions in general in
> Coq?
> 
> Thanks.
> 
> regards,
> taimoor

You just have to prove "False".

For that you can use lemmas implying "False" under some hypothesis.
For instance, if you have in your lemmas a "H : forall x, P x ->
False", then you can do "apply (H <the x you need>)." then you have to
prove "P <the x you need>". Note that in Coq some people tend to define
such lemmas with "not" rather than "-> False". That is your lemma will
have the "H : forall x, not (P x)" ['not' is defined as "fun P => P ->
False"], and knowing that there is a special notation for 'not', you
should look at "H : forall x, ~ P x" ("~ P x" being the notation for
"not (P x)").

I see no other way beside the more complex one (and in fact used in the
lemmas implying False if you inspect the proofs) where you have to
burrow False under a pattern matching.

For instance consider the following context:

s : stack
z : Z
Habs : Create = Push s z
========================
False

Here people will tell you "use 'inversion Habs.'" or "use
'discriminate.'". They are not wrong, but I consider that using stuff
without knowing the trick behind is not always the right thing to do.
So let us do what is behind the hood.
Obviously, you have no lemmas implying False, so you need to work by
yourself. The only one hypothesis which seems useful is Habs, so as it
is an equation, you will involve one of its members into a pattern
matching.

To do that, try the following tactic:

⇒change False
⇒with (match Push s z with Push _ _ => False | _ => True end).

You should get something like:

s : stack
z : Z
Habs : Create = Push s z
========================
match Push s z with Push _ _ => False | _ => True end

This works due to subject reduction (well I am not sure it is the right
name here…), that is when you reduce your goal, you get "False" which
was your previous goal.

From here the proof should be obvious. Just use your Habs hypothesis.

⇒rewrite <- Habs. (* or "case Habs." if you want to be low-level *)

Now your goal should look like:

s : stack
z : Z
Habs : Create = Push s z
========================
match Create with Push _ _ => False | _ => True end

But I think that Coq is too hasty to show you this intermediate goal
and will immediately reduce it to:

s : stack
z : Z
Habs : Create = Push s z
========================
True

Then from here, the proof should be obvious (even for Coq !)

⇒trivial. (* or "split." or "exact I." or "easy." or … *)

Proof done.


In practice, using the "change" tactic is rather unconvenient, and once
you well understand the mechanics, you may want to use "inversion" or
"discriminate" in this kind of case. Nonetheless, being able to do what
I show can be very useful as it can be tuned to perfectly fit your
needs. Note also that "inversion" is very powerful, but leads to
unecessary big proofs (not in the size of the script, but in the size
of the term generated by Coq) and can have an impact on the
performances (using too much this tactic can lead to having a Coq
session _very_ slow), and will pollute your context with too many
hypothesis (inversion_clear is a tactic which cleans them, but lack of
smartness and may clear equalities which may still be useful, so you
may get stuck) [that is why I prefer to do "inversion H; clear H;
subst."].