The Coq mailing list

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

Hi,

Thanks for the reply. However, I am interested in the general
proof strategy of Coq regarding the proofs which involve
structural equality, e.g. some builtin mechanism (automatic)
for proving the equality of two integers.

However, I have attached my Coq file, where I need to
prove the equivalence of two integers and the corresponding
stacks, which are represented as arrays and size.

Thanks for your valuable feedback and remarks.

regards,
taimoor

> We lack information on many things to give a clear answer.
> But I guess that you should start with:
>
> clear h1 h3 h4 h7 h9 h12; subst; simpl in *.
>
> That should clean a lot of useless stuff.
>
> 2013/5/7 
> <mtkhan AT risc.uni-linz.ac.at>
>
>> Hi,
>>
>> Thanks Adam again; yes, the later tactics worked. I am still wondering
>> what is the general proof strategy in Coq for such structural
>> equality?
>>
>> For example now, in the following
>>
>> 1 subgoal
>> e : int
>> rho : int
>> rho1 : Map.map int int
>> rho2 : int
>> r := mk_stack_rep rho2 (mk_array rho rho1) : stack_rep
>> h1 : 0 <= rho
>> h2 : invariant_stack r
>> h3 : rho2 = rho -> 2 * rho + 1 < 2147483647
>> h4 : rho2 <> rho
>> h5 : 0 <= rho2
>> h6 : rho2 < rho
>> o : Map.map int int
>> h7 : 0 <= rho
>> h8 : o = Map.set rho1 rho2 e
>> h9 : - (2147483648) <= rho2 + 1
>> h10 : rho2 + 1 <= 2147483647
>> rho3 : int
>> h11 : rho3 = rho2 + 1
>> h12 : 0 <= rho
>> s : stack
>> z : int
>> H : to_abstract_stack (mk_stack_rep rho3 (mk_array rho o)) = Push s z
>> ______________________________________(1/1)
>> s = to_abstract_stack r /\ z = e
>>
>> I want to prove
>> 1) s = to_abstract_stack r
>> 2) z = e
>>
>> How can I really proceed without induction on z or e in the
>> second case. Also any clue or help regarding case 1, where
>> stack is inductively defined as
>>
>> Inductive stack :=
>>   | Create : stack
>>   | Push : stack -> Z -> stack.
>>
>> Thanks.
>>
>> regards,
>> taimoor
>>
>> > On 05/06/2013 11:26 AM, 
>> > mtkhan AT risc.uni-linz.ac.at
>> >  wrote:
>> >> ...
>> >> H0 : s = to_abstract_stack r /\ z = e
>> >> ______________________________________(1/1)
>> >> Push s z = Push (to_abstract_stack r) e
>> >>
>> >> my question here, how to prove structural induction reasonably
>> >> in a well-manner in Coq.
>> >>
>> >
>> > Perhaps there is some aspect of your problem that isn't expressed
>> > adequately by the above goal, but it looks to me like the goal can be
>> > proved with
>> >      congruence
>> > or maybe
>> >      intuition congruence
>> > if the former isn't smart enough.  It follows by basic properties of
>> > equality, with no induction required.
>> >
>>
>>
>>
>
>
> --
> .../Sedrikov\...
>

Attachment: binz9bOQide1U.bin
Description: application/trash