# How to define the SEP(R) clauses?

**URL:** <https://discourse.rocq-prover.org/t/how-to-define-the-sep-r-clauses/1442>\
**Category:** Using Rocq\
**Created:** [September 20, 2021, 6:52am UTC](https://discourse.rocq-prover.org/t/how-to-define-the-sep-r-clauses/1442 "2021-09-20T06:52:16Z")\
**Posts on this page:** 2\
**Page:** 1

<div class="post-metadata">

**Author:** ![lyl](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/lyl/32/575_2.png) [@lyl](https://discourse.rocq-prover.org/u/lyl)\
**Post date:** [September 20, 2021, 6:52am UTC](https://discourse.rocq-prover.org/t/how-to-define-the-sep-r-clauses/1442/1 "2021-09-20T06:52:16Z")

</div>

I am now working on proving one lemma of Verif\_triang of VC:

Lemma [body\_push\_increasing](#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!

---

<div class="post-metadata">

**Author:** ![liuxingpeng520521](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/liuxingpeng520521/32/865_2.png) [@liuxingpeng520521](https://discourse.rocq-prover.org/u/liuxingpeng520521)\
**Post date:** [November 8, 2023, 8:33am UTC](https://discourse.rocq-prover.org/t/how-to-define-the-sep-r-clauses/1442/2 "2023-11-08T08:33:38Z")

</div>

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.