How to use tactic forward_if Q?

Using Coq
1

I am doing exercise 2 of Verfi_stack. I got stuck because of the tactic forward_if.
The subgoal is illustrated as follows:

1 subgoal
Espec : OracleKind
p : val
i : Z
il : list Z
gv : globals
Delta_specs := abbreviate : Maps.PTree.t funspec
Delta := abbreviate : tycontext
H : Int.min_signed <= i <= Int.max_signed
POSTCONDITION := abbreviate : ret_assert
MORE_COMMANDS := abbreviate : statement
H0 : eq_dec nullval nullval = left eq_refl

semax Delta
  (PROP ( )
   LOCAL (temp _q nullval; gvars gv; 
   temp _p p; temp _i (Vint (Int.repr i)))
   SEP (mem_mgr gv; emp; stack il p))
  (if (!_q) {
     _exit((1));
   }
   MORE_COMMANDS) POSTCONDITION

The hint shows: Hint: try 'forward_if', which may inform you that you need to supply a postcondition.
So, I was trying to use forward_if to forward if block, that is, (if(!_q)) {_exit((1))}. But it didn’t work, showing No matching clauses for match.
I did check how to use this tactic in Verifiable C, but I am still not having a clue about how to use it to solve this subgoal.
Thank you!

.

2

forward_if must be applied to a postcondition. Here, depending on whether q is nullval (which is the case in your current goal), the if clause either exits (postcondition False) or does nothing (postcondition True). Try forward_if False.

3

I tried forward_if False. It turned one subgoal into False. I got stuck again. Then, I tried forward_if True, it generated three subgoals. And I finally solved all the goals. It seems to me that forward_if True or forward_if False give similar subgoals except that the latter gives also an additional subgoal of the statement that is just after the if block. In my case, forward_if False leaves the goals ... (_exit((1));)... and ... (/*skip*/;) ... but forward_if True leaves also this goal ... ((_q->_value) = _i; MORE_COMMANDS) ....
Hence, I didn’t really understand the difference between them. Could you please explain a little bit more? Thank you!

4

Given a Hoare triple

{{ pre }}
  if (cond) { f() }
  etc()
{{ post }}

forward_if Q first breaks it into the following, isolating the if statement:

{{ pre }}
if (cond) { f() }
{{ Q * pre }}

{{ Q * pre }}
etc()
{{ post }}

(Note this is the simplified variant, where Q is just a Prop; there is a more general version of forward_if.)

Moreover, the single if clause desugars into if/else: if (cond) { f() } else { /*skip*/; }. And the triple for if above splits into one for each branch.

{{ cond * pre }}
  f()
{{ Q * pre }}

{{ ~cond * pre }}
  /*skip*/;
{{ Q * pre }}

So there are three subgoals, one for f(), one for /*skip*/; and one for etc() (after the if branches). If Q = False. then the etc() triple is trivially solved. That is why forward_if False leaves you with only two goals.

Which of forward_if True or forward_if False to use here depends on the branch of the case split on q you’re in.

5

It is very clear to me! Thank you so much! I would also like to ask another question, if I may. I would like to know how I can use Verifiable C to prove theorems without the help of hint tactic. The goal is rather complicated to read. Sometimes, when I unfold a definition, it makes the goal much more complicated. It is very hard to know exactly what to do next. I am now trying to read Verifiable C and read volume Verifiable C of software foundation. So, do you have any specific suggestions? Thanks a lot.