(**
% Exercises on Generalizing the Induction Hypothesis
% James Wilcox
% February 21, 2017
*)
(**
> _This post collects several Coq exercises on generalizing the
> induction hypothesis._
Most proofs in Coq boil down to induction somewhere. But not all true
statements are provable _directly_ by induction. Often, one or more
_generalizations_ need to be performed before the statement will be
provable.
Starting from a desired (true) statement and coming up with the
"right" statement to prove by induction is a skill that is (in my
opinion) underemphasized in introductory books on verification.
This post is the beginning of an attempt to fill that gap. It is a
sequence of eight exercises that set up a desired theorem, which is
not provable directly by induction, and then ask you to prove it by
coming up with suitable more general helper lemmas.
You can find the source code for the post
[here](http://homes.cs.washington.edu/~jrw12/InductionExercises.v).
In a later post, I hope to develop a "theory of proofs by induction",
which will give concrete guidance and rules of thumb for how to come
up with statements provable by induction. But for now, I hope this
post can help you pick up those skills on your own.
[CPDT]: http://adam.chlipala.net/cpdt/html/Cpdt.StackMachine.html
I adapted the arithmetic expression language exercise from Adam
Chlipala's [CPDT][CPDT], but similar examples have been verification fodder since at least 1967 ([McCarthy
and Painter](http://jmc.stanford.edu/articles/mcpain/mcpain.pdf)).
Miranda Edwards also helped develop several of the exercises.
I would appreciate feedback on these exercises via email.
## Summing lists
Here is a straightforward implementation of a function to add up a
list of natual numbers.
*)
Require Import List Arith Omega.
Import ListNotations.
(*begin code*)
Fixpoint sum (l : list nat) : nat :=
match l with
| [] => 0
| x :: xs => x + sum xs
end.
(*end code*)
(**
### Tail-recursive sum
Here's a slightly more sophisticated tail-recursive implementation,
designed to use constant space when extracted to a strict language
like Scheme or OCaml.
*)
(*begin code*)
Fixpoint sum_tail' (l : list nat) (acc : nat) : nat :=
match l with
| [] => acc
| x :: xs => sum_tail' xs (x + acc)
end.
Definition sum_tail (l : list nat) : nat :=
sum_tail' l 0.
(*end code*)
(**
Any time we make an optimization, it's nice to prove that we haven't
messed things up. In this case, we should show that the two ways of
summing a list are equivalent, as stated by the following theorem.
#### Exercise `sum_tail_correct`.
*)
(*begin code*)
Theorem sum_tail_correct :
forall l,
sum_tail l = sum l.
Proof.
(*end code*)
(**
Try to prove this directly by induction. Convince yourself that you
are stuck.
Unstick yourself by stating and proving (by induction) a more general
helper lemma about the helper function `sum_tail'`. Then prove
`sum_tail_correct` in just one or two lines without induction by
directly applying the helper lemma. In the proofs (both of the helper
lemma and the main theorem), you will likely need a few lemmas about
addition from the standard library (or you can use the `omega`
tactic).
*)
(*begin code*)
Admitted.
(*end code*)
(**
### Continuation-passing style sum
Here's yet another way to define a function to sum a list, this time
in continuation-passing style.
*)
(*begin code*)
Fixpoint sum_cont' {A} (l : list nat) (k : nat -> A) : A :=
match l with
| [] => k 0
| x :: xs => sum_cont' xs (fun ans => k (x + ans))
end.
Definition sum_cont (l : list nat) : nat :=
sum_cont' l (fun x => x).
(*end code*)
(**
While this way of implementing it is a little contrived, it makes for
good practice. Let's again prove it equivalent to the original `sum`
function.
#### Exercise `sum_cont_correct`.
*)
(*begin code*)
Theorem sum_cont_correct :
forall l,
sum_cont l = sum l.
Proof.
(*end code*)
(**
Again, try to prove this directly by induction. Convince yourself that
you are stuck.
Again, unstick yourself by stating and proving (by induction) a more
general helper lemma, this time about the helper function
`sum_cont'`. Then prove `sum_cont_correct` in just one or two lines
without induction by directly applying the helper lemma.
*)
(*begin code*)
Admitted.
(*end code*)
(**
## Manipulating lists with tail recursion
### Reverse
Here is a naive implementation of a function to reverse a list. (Also
built-in to the standard library with the same name and
implementation, but we reproduce it here for completeness.)
*)
(*begin code*)
Fixpoint rev {A} (l : list A) : list A :=
match l with
| [] => []
| x :: xs => rev xs ++ [x]
end.
(*end code*)
(**
Here is standard the tail-recursive implementation.
*)
(*begin code*)
Fixpoint rev_tail' {A} (l : list A) (acc : list A) : list A :=
match l with
| [] => acc
| x :: l' => rev_tail' l' (x :: acc)
end.
Definition rev_tail {A} (l : list A) : list A := rev_tail' l [].
(*end code*)
(**
Here is a statement of the correctness theorem for the tail-recursive
version.
#### Exercise `rev_tail_correct`.
*)
(*begin code*)
Theorem rev_tail_correct :
forall A (l : list A),
rev_tail l = rev l.
Proof.
(*end code*)
(**
Again, try to prove this directly by induction. Convince yourself that
you are stuck.
Again, unstick yourself by stating and proving (by induction) a more
general helper lemma, this time about the helper function
`rev_tail'`. Then prove `rev_tail_correct` in just one or two lines
without induction by directly applying the helper lemma. In the
proofs, you will likely need a few lemmas about list append from the
standard library.
*)
(*begin code*)
Admitted.
(*end code*)
(**
### Map
Here is the standard implementation of mapping a function over a list.
(Also built-in to the standard library with the same name, but we
include it here for completeness.)
*)
(*begin code*)
Fixpoint map {A B} (f : A -> B) (l : list A) : list B :=
match l with
| [] => []
| x :: xs => f x :: map f xs
end.
(*end code*)
(**
Here is a tail-recursive implementation.
*)
(*begin code*)
Fixpoint map_tail' {A B}
(f : A -> B) (l : list A) (acc : list B) : list B :=
match l with
| [] => rev_tail acc
| x :: l' => map_tail' f l' (f x :: acc)
end.
Definition map_tail {A B} (f : A -> B) l := map_tail' f l [].
(*end code*)
(**
Here is the correctness theorem for the tail-recursive implementation.
#### Exercise `map_tail_correct`.
*)
(*begin code*)
Theorem map_tail_correct :
forall A B (f : A -> B) l,
map_tail f l = map f l.
Proof.
(*end code*)
(**
By this point, hopefully you realize that this will not be provable
directly by induction.
State and prove (by induction) a more general helper lemma, this time
about the helper function `map_tail'` and use it to prove
`map_tail_correct`. You will likely need a few lemmas about list
append from the standard library, as well as your `rev_tail_correct`
theorem from above.
*)
(*begin code*)
Admitted.
(*end code*)
(**
## Arithmetic expression languages
Here is a (trivial) language of arithmetic expressions consisting of
nested sums of constants.
*)
(*begin code*)
Inductive expr : Type :=
| Const : nat -> expr
| Plus : expr -> expr -> expr.
(*end code*)
(**
Here is a straightforward evaluation function for the expression
language.
*)
(*begin code*)
Fixpoint eval_expr (e : expr) : nat :=
match e with
| Const n => n
| Plus e1 e2 => eval_expr e1 + eval_expr e2
end.
(*end code*)
(**
### Accumulator-based evaluator
Here is a accumulator-based implementation. (Not tail-recursive
despite its name because the recursive call on `e1` is not in tail
position, since the recursive call on `e2` remains to be done.)
*)
(*begin code*)
Fixpoint eval_expr_tail' (e : expr) (acc : nat) : nat :=
match e with
| Const n => n + acc
| Plus e1 e2 => eval_expr_tail' e2 (eval_expr_tail' e1 acc)
end.
Definition eval_expr_tail e := eval_expr_tail' e 0.
(*end code*)
(**
Here is a theorem relating the two evaluators.
#### Exercise `eval_expr_tail_correct`.
*)
(*begin code*)
Theorem eval_expr_tail_correct :
forall e,
eval_expr_tail e = eval_expr e.
Proof.
(*end code*)
(**
Prove this by finding and proving (by induction) a suitable helper
lemma.
*)
(*begin code*)
Admitted.
(*end code*)
(**
### Continuation-passing style evaluator
Here is another evaluator, this one in continuation-passing style.
*)
(*begin code*)
Fixpoint eval_expr_cont' {A} (e : expr) (k : nat -> A) : A :=
match e with
| Const n => k n
| Plus e1 e2 => eval_expr_cont' e2 (fun n2 =>
eval_expr_cont' e1 (fun n1 => k (n1 + n2)))
end.
Definition eval_expr_cont (e : expr) : nat :=
eval_expr_cont' e (fun n => n).
(*end code*)
(**
And its correctness theorem.
#### Exercise `eval_expr_cont_correct`.
*)
(*begin code*)
Theorem eval_expr_cont_correct :
forall e,
eval_expr_cont e = eval_expr e.
Proof.
(*end code*)
(**
Prove this by finding and proving (by induction) a suitable helper
lemma.
*)
(*begin code*)
Admitted.
(*end code*)
(**
### Compiling arithmetic expressions to a stack language
Here is a "low-level" stack language which can serve as the target
language for a compiler from the arithmetic expression language above.
A program in this language is a list of instructions, each of which
manipulates a stack of natural numbers. There are instructions for
pushing constants onto the stack and for adding the top two elements
of the stack, popping them, and pushing the result.
*)
(*begin code*)
Inductive instr := Push (n : nat) | Add.
Definition prog := list instr.
Definition stack := list nat.
(*end code*)
(**
The `run` function is an interpreter for this language. It takes a
program (list of instructions) and the current stack, and processes
the program instruction-by-instruction, returning the final stack.
*)
(*begin code*)
Fixpoint run (p : prog) (s : stack) : stack :=
match p with
| [] => s
| i :: p' => let s' :=
match i with
| Push n => n :: s
| Add => match s with
| a1 :: a2 :: s' => a1 + a2 :: s'
| _ => s
end
end in
run p' s'
end.
(*end code*)
(**
Now here is a compiler from "high-level" expressions to "low-level"
stack programs. Take a minute to understand how it works. (Try it on a
few example expressions, and try passing the results into `run` with
various initial stacks.)
*)
(*begin code*)
Fixpoint compile (e : expr) : prog :=
match e with
| Const n => [Push n]
| Plus e1 e2 => compile e1 ++ compile e2 ++ [Add]
end.
(*end code*)
(**
Here is a correctness theorem for the compiler: it preserves the
meaning of programs. By "meaning", in this case, we just mean final
answer computed by the program. For high-level expression, the answer
is the result of calling `eval_expr`. For stack programs, the answer
is whatever `run` leaves on the top of the stack. The correctness
theorem states that these answers are the same for an expression and
the corresponding compiled program.
#### Exercise `eval_expr_cont_correct`.
*)
(*begin code*)
Theorem compile_correct :
forall e,
run (compile e) [] = [eval_expr e].
Proof.
(*end code*)
(**
Prove this by proving one or more helper lemmas about `compile`,
`run`, `eval_expr`, and the functions they call. The correct helper
lemmas require several steps of generalization.
This one is harder than anything else up to this point in the file.
*)
(*begin code*)
Admitted.
(*end code*)
(**
## Efficient Fibonacci
Here is a naive (exponential time) implementation of a function to
compute the nth Fibonacci number.
*)
(*begin code*)
Fixpoint fib (n : nat) :=
match n with
| 0 => 1
| S n' => match n' with
| 0 => 1
| S n'' => fib n' + fib n''
end
end.
(*end code*)
(**
And here is a tail-recursive (linear time) solution.
*)
(*begin code*)
Fixpoint fib_tail' (n a b : nat) : nat :=
match n with
| 0 => b
| S n' => fib_tail' n' (a + b) a
end.
Definition fib_tail (n : nat) :=
fib_tail' n 1 1.
(*end code*)
(**
Here is a correctness theorem for the optimized version.
#### Exercise `eval_expr_cont_correct`.
*)
(*begin code*)
Theorem fib_tail_correct :
forall n,
fib_tail n = fib n.
Proof.
(*end code*)
(**
Prove this by proving one or more helper lemmas by induction. This one
is harder than the others in the file, and I don't fully understand
the "why" of my own solution. I would be eager to hear about any
particularly elegant solutions or explanations.
*)
(*begin code*)
Admitted.
(*end code*)