The Coq mailing list

[mtkhan AT risc.uni-linz.ac.at]

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

> 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?
>