IMP Semantics

expr : big step

Heaps : To evaluate an expression containing variables, we need some representation of memory to get the value of variables from. We need to model memory as some mapping from variables to ints. Functions can do just that!

The empty memory just maps everything to zero.

We will also need to evaluate our operators over ints. Since there's a bunch, we'll define a helper function for this.

SearchAbout Z. Now we can define a relation to capture the semantics of expressions

"Big Step" holds for the final result. not: eval h (1 + 2 + 3) (1 + 5)

We can also define an interpreter for expressions.

... and prove relational and functional versions agree

simpl goal and context in all subgoals

NOTE: coercions make it look like types are bogus!

replace z with i everywhere

`apply eval_int` would also work here

replace i with (h s) everywhere

`apply eval_var` would also work here

`apply eval_binop` won't work, even though it seems like it should unify. Coq complains:

  Error: Unable to find an instance for the variables i1, i2.

because it needs to know those to apply the constructor. We can use a variant of apply to tell Coq exacly what i1 and i2 should be.

now we have extra subgoals for the hypotheses of the eval_binop constructor

UGH. IHe1 is too weak, for a specific i :( back out and try again REMEMBER: don't intro too many things too soon!!!

OK, now IHe1 and IHe2 look stronger

`interp_expr_ok` only shows that if the interpreter produces `i` as the result of evaluating expr `e` in heap `h`, then eval relates `h`, `e`, and `i` as well. We can prove the other direction: if the eval relates `h`, `e`, and `i`, then the interpreter will produce `i` as the result of evaluation expr `e` in heap `h`.

careful not to intro too much

inversion tells coq to let us do case analysis on all the ways H could have been produced

we get a bunch of equalities in our context, subst will clean them up

we can "fill in" an equality to rewrite with

we actually could have proved the above lemma in an even cooler way: by doing induction on the derivation of eval!

notice how much cleaner that was! we can also write the one of the earlier lemmas in a slightly cleaner way

`constructor.` will not work here because the goal does not unify with the eval_binop case. `econstructor` is a more flexible version of constructor that introduces existentials that will allow things to unify behind the scenes. Check it out!

`assumption.` will not work here because our goal has an existential in it. However `eassumption` knows how to handle it!

OK, so we've shown that our relational semantics for expr agrees with our functional interpreter. One nice consequence of this is that we can easily show that our eval relation is deterministic.

it's a bit more work without interp, but not too bad

set up a strong induction hyp

cut

replace (i1 + 0) with i1 by omega. assumption.

stmt : small step

To define the semantics for statements, we'll need to be able to update the heap.

| step_while: forall h e s, step h (While e s) h (Cond e (Seq s (While e s))) note that there are several other ways we could have done semantics for while We can also define an interpreter to run a single step of a stmt, but we'll have to learn some new types to write it down. Note that, unlike eval, the step relation is partial: not every heap and stmt is related to another heap and stmt!

umpossible!

In general, we say that any stmt that cannot step is "stuck"

Since the step relation is partial, but all functions have to be total, we will use the `option` type to represent the results of step interpreter.

We could define our interpreter this way, but we end up with a case explosion in the Seq nop / non-nop cases... Fixpoint interp_step (h: heap) (s: stmt) : option (heap * stmt) := match s with | Nop => None | Assign v e => Some (update h v (interp_expr h e), Nop) | Seq Nop s => Some (h, s) | Seq s1 s2 => match interp_step h s1 with | Some (h', s1') => Some (h', Seq s1' s2) | None => None end | Cond e s => if Z_eq_dec (interp_expr h e) 0 then Some (h, Nop) else Some (h, s) | While e s => if Z_eq_dec (interp_expr h e) 0 then Some (h, Nop) else Some (h, Seq s (While e s)) end. So instead, we'll define a helper to simplify the match.

a lot of times we don't really need intros

and we can prove that our step interpreter agrees with our relational semantics

use the weird `eqn:?` after a destruct to remember what you destructed!

and you can control the names of parts of constructors using "destruct ... as ..."

Once again `constructor` and even `apply step_cond_false` will not work because the conclusion of the step_cond_false constructor needs to know what `i` should be. We could explicity use the `apply step_cond_false with (i := ...)` flavor of apply to specify `i`, but using `econstructor` is more convenient and flexible.

now that we have these existentials in our context we have to use the `e` versions of all our regular tactics.

existential resolved!

while is pretty similar to cond

nop can' step

So far, `step` only does one "step" of an execution of a stmt. We can build the transitive closure of this relation though to reason about with more than one step.

Defining an interpreter for more than one step is trickier! Since a stmt may not terminate, we can't just naively write a recursive function to run a stmt. Instead, we'll use a notion of "fuel" to guarantee that our function always terminates Fixpoint run (h: heap) (s: stmt) : (heap * stmt) := match interp_step h s with | Some (h', s') => run h' s' | None => (h, s) end.

and we can verify our interpreter too

step is deterministic

NOTE: we would have a much harder time if we had defined step_n to "add on the right":

Try using this definition and doing the above proofs. TAH DAH! We have a verified interpreter!