The Coq mailing list

[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.
>