Exercises

[Yves]

To set up your working environment, you need to have coq-8.1 running
on your machine. The development
tool should be either coqide (as provided in the Coq environment) or a
recent Gnu-Emacs extended with
the Proof-General package. For proof general, the "stable" release
does not work, you need to use
the latest pre-release (I use Carbon Emacs on an Intel MacBook, my
version of Proof General is
ProofGeneral-3.7pre070312.tar.gz, but I had to patch a few auxiliary
commands that were not work
properly).

You should create a directory, untar the file got.tgz and run make in
this directory.

Exercises can be done in a context that is obtained by starting
Coq-8.1 and executing the following
three lines.

Require Import little_w_string parser ZArith List String.
Open Scope Z_scope.
Import B A D L S.

----------------
A first exercise you can do is to model the evaluation of "(x+1)+y" in
the environment "(x,1).(y,2).nil".
The Coq statement is as follows:

Example ex1 : a_eval (("x",1)::("y",2)::nil) (aplus (aplus (avar "x")
(anum 1)) (avar "y")).

A second exercise is to prove the associativity of sequences with
respect to execution:

Example ex2 : forall r i1 i2 i3 r', exec r (sequence i1 (sequence i2
i3)) r' ->
exec r (sequence (sequence i1 i2) i3) r'.

A third exercise is to prove a simple property of a loop program:

Example ex3 : forall p p', exec (("x",p)::nil)
(while (blt (avar "x")(anum 10))
(assign "x" (aplus (avar "x") (anum 3))))
(("x",p')::nil) -> exists k, p' -p
= 3*k