The Coq mailing list

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

Le Thu, 02 May 2013 12:07:47 -0400,
Adam Chlipala 
<adamc AT csail.mit.edu>
 a écrit :

> On 05/02/2013 12:00 PM, 
> mtkhan AT risc.uni-linz.ac.at
>  wrote:
> > I have the following inductive definition of stack.
> >
> > Inductive stack  :=
> >    | Create : stack
> >    | Push : stack ->  Z ->  stack .
> >
> > and how can I proceed if I have the following goal.
> >
> >    r : stack_rep
> >    h1 : invariant_stack r
> >    h2 : concrete_stack Create r
> >    s : stack
> >    z : Z
> >    ============================
> >     Create = Push s z
> >
> > in fact, this cannot be possible.
> >    
> 
> When the conclusion formula is false, you need to find a
> contradiction from the hypotheses.  Are you asking how to prove
> contradictions in general?

If so, you should start with:

exfalso. (*replace current goal with False*)
clear s z. (*s and z are useless, so remove them*)

then depending on the definition of stack_rep, invariant_stack and
concrete_stack, you may be interested in the [inversion] tactic,
or the [induction tactic].

Without more knowledge, we cannot give very useful hints.
Note also that what you want to prove may also be unprovable (or even
worse, you might be able to prove the contrary).