I don't know if it's wanted. But from the download of Volume 1: Logical Foundations, there are exercises at the end of the chapter about Induction which don't appears on the website version.
Definition manual_grade_for_plus_comm_informal : option (nat*string) := None.
(** [] *)
(** **** Exercise: 2 stars, standard, optional (eqb_refl_informal)
Write an informal proof of the following theorem, using the
informal proof of [plus_assoc] as a model. Don't just
paraphrase the Coq tactics into English!
Theorem: [true = n =? n] for any [n].
Proof: (* FILL IN HERE *)
[] *)
(* ################################################################# *)
(** * More Exercises *)
(** **** Exercise: 3 stars, standard, recommended (mult_comm)
Use [assert] to help prove this theorem. You shouldn't need to
use induction on [plus_swap]. *)
Theorem plus_swap : forall n m p : nat,
n + (m + p) = m + (n + p).
Proof.
(* FILL IN HERE *) Admitted.
(** Now prove commutativity of multiplication. (You will probably
need to define and prove a separate subsidiary theorem to be used
in the proof of this one. You may find that [plus_swap] comes in
handy.) *)
Theorem mult_comm : forall m n : nat,
m * n = n * m.
Proof.
(* FILL IN HERE *) Admitted.
(** [] *)
(** **** Exercise: 3 stars, standard, optional (more_exercises)
Take a piece of paper. For each of the following theorems, first
_think_ about whether (a) it can be proved using only
simplification and rewriting, (b) it also requires case
analysis ([destruct]), or (c) it also requires induction. Write
down your prediction. Then fill in the proof. (There is no need
to turn in your piece of paper; this is just to encourage you to
reflect before you hack!) *)
Check leb.
Theorem leb_refl : forall n:nat,
true = (n <=? n).
Proof.
(* FILL IN HERE *) Admitted.
Theorem zero_nbeq_S : forall n:nat,
0 =? (S n) = false.
Proof.
(* FILL IN HERE *) Admitted.
Theorem andb_false_r : forall b : bool,
andb b false = false.
Proof.
(* FILL IN HERE *) Admitted.
Theorem plus_ble_compat_l : forall n m p : nat,
n <=? m = true -> (p + n) <=? (p + m) = true.
Proof.
(* FILL IN HERE *) Admitted.
Theorem S_nbeq_0 : forall n:nat,
(S n) =? 0 = false.
Proof.
(* FILL IN HERE *) Admitted.
Theorem mult_1_l : forall n:nat, 1 * n = n.
Proof.
(* FILL IN HERE *) Admitted.
Theorem all3_spec : forall b c : bool,
orb
(andb b c)
(orb (negb b)
(negb c))
= true.
Proof.
(* FILL IN HERE *) Admitted.
Theorem mult_plus_distr_r : forall n m p : nat,
(n + m) * p = (n * p) + (m * p).
Proof.
(* FILL IN HERE *) Admitted.
Theorem mult_assoc : forall n m p : nat,
n * (m * p) = (n * m) * p.
Proof.
(* FILL IN HERE *) Admitted.
(** [] *)
(** **** Exercise: 2 stars, standard, optional (eqb_refl)
Prove the following theorem. (Putting the [true] on the left-hand
side of the equality may look odd, but this is how the theorem is
stated in the Coq standard library, so we follow suit. Rewriting
works equally well in either direction, so we will have no problem
using the theorem no matter which way we state it.) *)
Theorem eqb_refl : forall n : nat,
true = (n =? n).
Proof.
(* FILL IN HERE *) Admitted.
(** [] *)
(** **** Exercise: 2 stars, standard, optional (plus_swap')
The [replace] tactic allows you to specify a particular subterm to
rewrite and what you want it rewritten to: [replace (t) with (u)]
replaces (all copies of) expression [t] in the goal by expression
[u], and generates [t = u] as an additional subgoal. This is often
useful when a plain [rewrite] acts on the wrong part of the goal.
Use the [replace] tactic to do a proof of [plus_swap'], just like
[plus_swap] but without needing [assert (n + m = m + n)]. *)
(* etc... *)
It is clearer to me to read text on the HTML version so I hope it's a bug.
Thx, for this book anyway.