The Coq mailing list

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

Hi All,

I have the following original Coq goal.

1 subgoal
______________________________________(1/1)
forall (r : Z) (rho : map Z Z) (rho1 : Z),
~
match to_abstract_stack (mk_stack_rep rho1 (mk_array r rho)) with
| Create => True
| Push _ _ => False
end /\ invariant_stack (mk_stack_rep rho1 (mk_array r rho)) ->
-2147483648 <= rho1 - 1 <= 2147483647

which translates to the following after the command

intros r rho rho1 r1 (h1,h2).

1 subgoal
r : Z
rho : map Z Z
rho1 : Z
r1 := mk_stack_rep rho1 (mk_array r rho) : stack_rep
h1 : ~
     match to_abstract_stack r1 with
     | Create => True
     | Push _ _ => False
     end
h2 : invariant_stack r1
______________________________________(1/1)
- (2147483648) <= rho1 - 1 <= 2147483647

rho1 is the index bound for the array and invariant_stack
is defined as.

Definition invariant_stack(r:stack_rep): Prop := (0%Z <= (size r))%Z /\
  ((size r) <= (length (data r)))%Z.

which gives the bound on the size of the array.

Do someone have any clue, how to carry the proof regarding
the array index bound in Coq?

Thanks.

regards,
tk