help with syntax for loop invariant

[AdamBJ]

I'm trying to get Coq to accept a loop invariant: apply hoare_consequence_pre with (P':= m = X + Y). The problem is that Coq requires X and Y to be nats. However, if I introduce st into the context so that I can do something like aeval AId X in place of X the hoare_triple in the goal is unfolded. I remember reading that this is not something we want to do when using Hoare logic. Can someone help me get my loop invariant into Coq? I've checked that it's correct using decoration as described in the book, I just can't get Coq to accept it.

[jeehoonkang]

I am note quite sure what you mean by "I remember reading that this is not something we want to do when using Hoare logic." Would you please elaborate?

[AdamBJ]

For example, for the reduce_to_zero example in the textbook we're told

"From this informal proof, it is easy to read off a formal proof using the Coq versions of the Hoare rules. Note that we do not unfold the definition of hoare_triple anywhere in this proof — the idea is to use the Hoare rules as a "self-contained" logic for reasoning about programs. "

[AdamBJ]

If I introduce st into the context the goal goes from being a hoare triple to using || notation (ie we've unfolded the definition of hoare triple).

[jeehoonkang]

@AdamBJ I understood what you mean. However, I would like to ask if you could specify more detailed information, like:

• the context and the goal you want to prove; and
• the context and the goal you get after applying hoare_consequence_pre with something with aeval AId X.

[AdamBJ]

1 subgoals
m : nat
______________________________________(1/1)
{{fun st : state => st X = m}}
Y ::= ANum 0;;
WHILE BNot (BEq (AId X) (ANum 0))
DO X ::= AMinus (AId X) (ANum 1);; Y ::= APlus (AId Y) (ANum 1) END
{{fun st : state => st Y = m}}

That's prior to apply hoare_conseq_pre, just give me a second to get the second part.

[AdamBJ]

Here is the goal after introducing st and st':

1 subgoals
m : nat
st : state
st' : state
______________________________________(1/1)
(Y ::= ANum 0;;
 WHILE BNot (BEq (AId X) (ANum 0))
 DO X ::= AMinus (AId X) (ANum 1);; Y ::= APlus (AId Y) (ANum 1) END) / st
|| st' -> st X = m -> st' Y = m

I guess I can't use hoare_conseq_pre here because the goal isn't a hoare triplet anymore.

[jeehoonkang]

How would apply hoare_consequence_pre with (P':= fun st => m = st X + st Y) work?

[AdamBJ]

Doing it that way made it go through, thanks a lot! Now to see if I can finish the rest, haha.

[AdamBJ]

It's too bad that in this section of the textbook there aren't many examples of translating decorated informal proofs into Coq.

[AdamBJ]

Can you tell me why hoare_asgn won't solve this: {{fun st : id -> nat => m = st X + st Y + 1}} Y ::= APlus (AId Y) (ANum 1) {{fun st : id -> nat => m = st X + st Y}}?

[jeehoonkang]

To apply hoare_asgn, I guess the precondition should be: {{fun st : id -> nat => m = st X + (st Y + 1)}}. Note the order of plus operations. Since it is too different from the one you gave for poor Coq, you have to use hoare_consequence_pre to massage the precondition.

[AdamBJ]

Just to experiment, I tried getting up to {{fun st : id -> nat => m = st X + st Y + 1}} Y ::= APlus (AId Y) (ANum 1) {{fun st : id -> nat => m = st X + st Y}} in Coq by using the e versions of tactics instead of explicitly tell Coq the steps, and it worked. I thought we need to provide Coq with a loop invariant in order for things to work though. Can I always use e... instead figuring out the loop invariant? I'm having trouble connecting the Coq implementations of decorated proofs in the textbook.

[jeehoonkang]

@AdamBJ

• In this context, I believe e-tactics are invaluable tools for inferring the invariants.
• However, in my experience, the loop invariants are not particularly well discovered by e-tactics (and other tactics as well). In many cases you have to specify loop invariants specifically.

[AdamBJ]

So maybe input the loop invariant myself, but rely on the e tactics to do the backwards steps through the program for me. No need to input everything myself, just the important stuff.

[AdamBJ]

What is the best way to get my loop invariant into a Coq proof? Can I input the loop invariant using hoare_conseq_pre and hoare_conseq_post interchangeably? What situations do each work best in?

[AdamBJ]

Or maybe inserting it with post would be better? Since with Hoare logic the proof seems to work backwards.

[jeehoonkang]

@AdamBJ Hmm.. once more, I am not quite sure what you mean. More details (context/goal examples, particularly) would be greatly helpful for me to help you.

Jeehoon

[AdamBJ]

I mean say we are working on a question like Assignment09_06. To start, the context looks like this:

1 subgoals
______________________________________(1/1)
forall m : nat,
{{fun st : state => st X = m}}
Y ::= ANum 0;;
WHILE BNot (BEq (AId X) (ANum 0))
DO X ::= AMinus (AId X) (ANum 1);; Y ::= APlus (AId Y) (ANum 1) END
{{fun st : state => st Y = m}}

Now, I know that the loop invariant (fun st => m = st X + st Y) works for this proof, because I wrote out the entire decorated program by hand and checked. The question then becomes how can I input my decorated program that uses this invariant into Coq? Do I need to explicitly state each line in the decorated proof (ie all the assertions involving the loop invariant), or can I let e tactics take care of these details for me? Based on what you said about Coq not figuring out loop invariant very well, my thought was that we need to explicitly provide Coq with an invariant rather than relying on e tactics to come up with one for us.

But if that's that case, what is the best way to specify the loop invariant? Taking question 6 above as an example, what is the best way to tell Coq "(fun st => m = st X + st Y) is the loop invariant I want to use to prove this program is correct? My goal is for the Coq proof to mirror the decorated program: ie I start by showing that the invariant combined with the negated loop guard implies the post condition, then work my way backwards through the decorated proof until I show that the precondition implies the loop invariant.

[jaewooklee93]

apply hoare_seq with (loop invariant) may work.

[AdamBJ]

To summarize that question: what is the best way to tell Coq the loop invariant i want to use? And to what degree can I rely on e tactics to do my work for me?

[jaewooklee93]

e-tactics are very convenient, but only if we try to provide loop invariant, ordinary apply is more useful.

[AdamBJ]

so i should figure out how to get the loop invariant into my Coq proof, then it's ok to use e tactics to "fill in the blanks"?

[AdamBJ]

That strategy seems to be working so far, but now I'm stuck here:

3 subgoal
m : nat
st : state
H : m = st X + st Y /\ beval st (BNot (BEq (AId X) (ANum 0))) = true
H0 : m = st X + st Y
H1 : beval st (BNot (BEq (AId X) (ANum 0))) = true
______________________________________(1/3)
st X + st Y = st Y + (st X - 1) + 1

Do you think it's possible to rewrite the goal using plus_assoc, plus_comm, and plus_permute so that I can apply reflexivity?

[AdamBJ]

I get stuck with the exact same pattern on question 7:

3 subgoal
n : nat
m : nat
st : state
H : st Y + st X = n + m /\ beval st (BNot (BEq (AId X) (ANum 0))) = true
H0 : st Y + st X = n + m
H1 : beval st (BNot (BEq (AId X) (ANum 0))) = true
______________________________________(1/3)
st Y + 1 + (st X - 1) = n + m
______________________________________(2/3)
(fun st : state =>
 (fun st0 : id -> nat => st0 Y + st0 X = n + m) st /\
 beval st (BNot (BEq (AId X) (ANum 0))) = false) ->>
(fun st : state => st Y = n + m)
______________________________________(3/3)
(fun st : state => st X = n /\ st Y = m) ->>
(fun st : id -> nat => st Y + st X = n + m)

Omega can't solve it, and neither can I.

[jaewooklee93]

Both of goals are of course solvable. You don't need to think about plus_comm or similar lemmas here, because omega can solve those easy problems. Your goals are almost trivial, but the reason why omega hesistates to clear the goals is just because the minus between nat is not the same as the one we already know; 2-5=0, since there is no notion of negative in nat. So if you don't provide the fact that st X is greater than zero, omega cannot clear the goal for you. But you already have that condition in H1. Therefore, the only thing you should do is to simplify H1 and apply lemmas to H1 to make it st X<>0 .Then omega can properly work.

[AdamBJ]

You've saved me again, thanks a lot! Really great explanation.