How to define the SEP(R) clauses?

Using Coq
1

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:

  1. Why here Coq prefer to use forward_loop instead of forward_while?
  2. 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).
  3. 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!

2

Hi, I am learning Verif_stack of VC and now I am stuck by the lemma [body_push]. Can you share your answer? Million thanks.