First lab session 1) get the files Tools.v and Semantics1.v from the course page 2) generate a makefile by the command coq_makefile Tools.v Semantics1.v -o Makefile 3) execute "make all" 4) edit Semantics1.v in order to accept conditional statements 5) In order to test your new version of f_sos, write a small program (e.g. Euclid's algorithm) and test it It would be nice if you define a function test_euclid (i j : Z) (fuel : nat) that returns - Some (gcd i j) if this value could be computed in at most fuel small steps - None otherwise. 6) Define in Coq the following tests - "the variable v may be assigned in the execution of the instruction i" - "the variable v is used in the execution of i" 7) Define in Coq the following predicates : - the environments r and r' define the same set of variables - the environments r and r' give the same value (defined or not) for the variable v 8) Define the predicate "the instruction i loops forever in the environment r". 9) (difficult) Prove that the program (while btrue skip) loops forever in any environment 10) (lovely) Prove that the program : (while (0 <= "x") ("x" <-- "x" + 1))%toy loops in the environment ("x",p)::nil) where p is a non null integer.