Stream: Coq users

Topic: ✔ Small step semantics in Coq


view this post on Zulip Julin S (Apr 16 2022 at 16:18):

Hi. I was going through the small step semantics illustrated with Coq at https://github.com/coq-community/semantics/blob/master/little.v

There I am having trouble understanding one of the constructors.

It's a type representing a small step evaluation for a loop:

| SOS4 :
     forall r b i, beval r b true ->
       sos_step r (while b i) (sequence i (while b i)) r

With type annotations:

| SOS4 :
     forall (r:env) (b:bexpr) (i:instr), beval r b true ->
       sos_step r (while b i) (sequence i (while b i)) r

(where bexpr denotes a boolean expression.

So this constructor represents the case where the condition for the loop is still true.

How can we be sure that the environment remains same after the execution of the instruction i?

That's what this constructor indicates, right?

Given an environment r, loop condition b and instruction i as the loop body, result would be the _same_ environment.

What am I missing here?

view this post on Zulip Li-yao (Apr 16 2022 at 16:31):

The instruction i has not been executed yet.

view this post on Zulip Julin S (Apr 16 2022 at 16:35):

Maybe a dumb question, but when will i be evaluated?

view this post on Zulip Li-yao (Apr 16 2022 at 16:39):

At the next step.

while b i -> sequence i (while b i) -> sequence i' (while b i) -> ... -> sequence skip (while b i) -> while b i

view this post on Zulip Julin S (Apr 16 2022 at 16:41):

Ah.. I think I get it now. Thanks!

view this post on Zulip Notification Bot (Apr 16 2022 at 16:41):

Julin S has marked this topic as resolved.


Last updated: Jan 28 2023 at 06:30 UTC