Exercise 8.2 page 213 On palindromes

Exercise 8.3 page 213 Reflexive and transitive closures

Exercise 8.4 page 214 On permutations

Exercise 8.8 page 224 About JM equality

Exercises 8.9 and 8.10 page 229 About even numbers

Exercise 8.11 page 230 Simulating

Exercises 8.12 and 8.13 page 230 An impredicative définition of <= on

Exercise 8.14 page 230 Another definition of <=

Exercise 8.15 page 230 Yet another definition of <=

Exercise 8.16 page 230 Non inductive definition of sorted lists

Exercise 8.17 page 231 Impredicative approach to inductive predicates

Exercise 8.18 page 231 A weird induction principle

Exercise 8.25 page 244 An alternative proof for the Hoare logic rule for while loops

Exercise 8.26 page 244 Infinite loop in an imperative language

Exercise 8.27 page 244 Hoare Logic rule for sequences

Exercise 8.29 page 250 On Frobenius stamp problem

Two Solutions are given : using JM equality and defining an ad hoc identity function (Solution proposed by Laurent Théry, see also Section 13.4.1 of the Coq'Art)

"binary_word (n+p)" and "binary_word (p+n)"

Going home

Pierre Castéran