Inductive Predicates

Scripts taken from the book

Exercises

Exercise 8.1 page 213 The last element of a list
Exercise 8.2 page 213 On palindromes
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 elim with apply
Exercises 8.12 and 8.13 page 230 An impredicative définition of <= on nat
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

About parsing

A thread of 9 exercises is devoted to parsing well balanced sequences of parentheses. This thread ends with the proof of correctness (i.e. soundness and completeness) of a parsing function.

New !

Prove that the only vector of length 0 is Vnil.
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)

Errata

Page 220, section 8.2.7, read : 
 "binary_word (n+p)" and "binary_word (p+n)"


Page 227, last paragraph. Erase the proposition "and to the fact ... auto"
Pagge 229, last paragraph. Read "(page 134)" instead of "(Sect. 134)"