The Coq mailing list

[Brandon Moore <brandon_m_moore AT yahoo.com>]

> please excuse my  dumbness:

> 
> is normal behavior invoking a lemma to break the future proof  of the true 
>fact:
> "True -> True" (implication).

Which lemm? False_ind?
 
> the lemma magically  changes the coq subgoal from True to False after 
> invoking
> the lemma. (if i  can change it the other way, i will have a fake proof).
> 
> is there some  theoretical justification the subgoal to be changed to False 
>  
at
> will?

Yes. Given false, you can prove anything. It's a plausible strategy for
proving a goal to say "I will first prove False (show that the hypotheses
are inconsistent), and then use that to trivially prove the current goal."
Depending on the lemma or tactic you use, the second step might be handled
automatically, leaving you with just the subgoal of proving the first
part.

It's not surprising that there are some strategies you just can't use to
finish certain proofs. In particular, using "clear" to throw away hypotheses
will quickly make most goals impossible.

Coq can't always warn you that making a step you request leads
into such a dead end. A common case is trying to prove something
by induction, and eventually realizing that you actually needed to generalize
the original goal before the inductive proof can go through.

Brandon