We saw in the Imp chapter how a naive approach to defining a function representing evaluation for Imp runs into difficulties. There, we adopted the solution of changing from a functional to a relational definition of evaluation. In this optional chapter, we consider strategies for getting the functional approach to work.
Here was our first try at an evaluation function for commands, omitting WHILE.
As we remarked in chapter Imp, in a traditional functional programming language like ML or Haskell we could write the WHILE case as follows:
| WHILE b1 DO c1 END => if (beval st b1) then ceval_step1 st (c1;; WHILE b1 DO c1 END) else st
Coq doesn't accept such a definition (Error: Cannot guess decreasing argument of fix) because the function we want to define is not guaranteed to terminate. Indeed, the changed ceval_step1 function applied to the loop program from Imp.v would never terminate. Since Coq is not just a functional programming language, but also a consistent logic, any potentially non-terminating function needs to be rejected. Here is an invalid(!) Coq program showing what would go wrong if Coq allowed non-terminating recursive functions:
Fixpoint loop_false (n : nat) : False := loop_false n.
That is, propositions like False would become provable (e.g., loop_false 0 would be a proof of False), which would be a disaster for Coq's logical consistency.
Thus, because it doesn't terminate on all inputs, the full version of ceval_step1 cannot be written in Coq -- at least not without one additional trick...
The trick we need is to pass an additional parameter to the
evaluation function that tells it how long to run. Informally, we
start the evaluator with a certain amount of gas
in its tank,
and we allow it to run until either it terminates in the usual way
or it runs out of gas, at which point we simply stop evaluating
and say that the final result is the empty memory. (We could also
say that the result is the current state at the point where the
evaluator runs out of gas -- it doesn't really matter because the
result is going to be wrong in either case!)
Note: It is tempting to think that the index i here is
counting the number of steps of evaluation.
But if you look
closely you'll see that this is not the case: for example, in the
rule for sequencing, the same i is passed to both recursive
calls. Understanding the exact way that i is treated will be
important in the proof of ceval__ceval_step, which is given as
an exercise below.
One thing that is not so nice about this evaluator is that we can't tell, from its result, whether it stopped because the program terminated normally or because it ran out of gas. Our next version returns an option state instead of just a state, so that we can distinguish between normal and abnormal termination.
We can improve the readability of this version by introducing a bit of auxiliary notation to hide the plumbing involved in repeatedly matching against optional states.
Write an Imp program that sums the numbers from 1 to X (inclusive: 1 + 2 + ... + X) in the variable Y. Make sure your solution satisfies the test that follows.
Write an Imp program that sets Z to 0 if X is even and sets Z to 1 otherwise. Use test_ceval to test your program.
As for arithmetic and boolean expressions, we'd hope that the two alternative definitions of evaluation would actually amount to the same thing in the end. This section shows that this is the case.
Write an informal proof of ceval_step__ceval, following the usual template. (The template for case analysis on an inductively defined value should look the same as for induction, except that there is no induction hypothesis.) Make your proof communicate the main ideas to a human reader; do not simply transcribe the steps of the formal proof.
Finish the following proof. You'll need ceval_step_more in a few places, as well as some basic facts about <= and plus.
Using the fact that the relational and step-indexed definition of evaluation are the same, we can give a slicker proof that the evaluation relation is deterministic.