The Coq mailing list

[Kristopher Micinski <krismicinski AT gmail.com>]

Adam has it right.  When you are faced with a contradiction, you need
to derive false from your hypotheses (and, using that contradiction,
you can of course produce a proof of anything).  Many tactics can do
this, but you also need to give some definitions of the other things
in your environment.

(Unless, of course, your theorem is just plain wrong.  In that case
you go back and start again..!)

Were this in your context rather than goal, you could simply use
inversion to derive the contradiction.

Kris


On Thu, May 2, 2013 at 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.
>
> Any help or hint here.
>
> regards,
> tk
>