I am now working on proving one lemma of Verif_triang of VC:

Lemma body_push_increasing: semax_body Vprog Gprog

f_push_increasing push_increasing_spec.

Here are my current proofs:

Proof.

start_function.

forward.

forward_loop

(EX i:Z,

PROP(0 <= i <= n)

LOCAL(temp _i (Vint(Int.repr i));

temp _n (Vint(Int.repr n));

temp _st st)

SEP(stack nil st; mem_mgr gv)).

+

Set Nested Proofs Allowed.

Goal forall (f: Z->Z) (x: Z), f(x)=0 → exists i:Z, f(x)=i.

intros.

(** To prove such a goal, one uses Coq’s “exists” tactic to

demonstrate a value for [i]: *)

exists 0.

auto.

Qed.

Exists 0.

entailer!.

- Intros i.

forward_if True.

- forward. entailer!.
- forward. entailer!.

cannot continue…

In fact, I have a few questions to ask:

- Why here Coq prefer to use
`forward_loop`

instead of`forward_while`

? - How to define the SEP() clause of the loop invariant? I took the SEP() from the precondition of the function specification. I tried also the one from the postcondition (It didn’t work for me).
- Tactics
`forward_if True`

are`forward_if False`

are suitable to be applied in which situations, respectively? For me, I tried them both every time, if one doesn’t work, I will try the other.

Thank you for much for your help!