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.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 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 in the eight chapter of the book 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. This file is a full development which can be considered as a solution to all these exercises.

New !

Prove that the only vector of lengh 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)"


Going home
Pierre Castéran