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.
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.
I adapted the arithmetic expression language exercise from Adam Chlipala's CPDT, but similar examples have been verification fodder since at least 1967 (McCarthy and Painter). Miranda Edwards also helped develop several of the exercises.
I would appreciate feedback on these exercises via email.
Here is a straightforward implementation of a function to add up a list of natual numbers.
Fixpoint sum (l : list nat) : nat :=
match l with
| [] => 0
| x :: xs => x + sum xs
end.
Here's a slightly more sophisticated tail-recursive implementation, designed to use constant space when extracted to a strict language like Scheme or OCaml.
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.
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.
sum_tail_correct.Theorem sum_tail_correct :
forall l,
sum_tail l = sum l.
Proof.
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).
Admitted.
Here's yet another way to define a function to sum a list, this time in continuation-passing style.
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).
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.
sum_cont_correct.Theorem sum_cont_correct :
forall l,
sum_cont l = sum l.
Proof.
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.
Admitted.
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.)
Fixpoint rev {A} (l : list A) : list A :=
match l with
| [] => []
| x :: xs => rev xs ++ [x]
end.
Here is standard the tail-recursive implementation.
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 [].
Here is a statement of the correctness theorem for the tail-recursive version.
rev_tail_correct.Theorem rev_tail_correct :
forall A (l : list A),
rev_tail l = rev l.
Proof.
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.
Admitted.
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.)
Fixpoint map {A B} (f : A -> B) (l : list A) : list B :=
match l with
| [] => []
| x :: xs => f x :: map f xs
end.
Here is a tail-recursive implementation.
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 [].
Here is the correctness theorem for the tail-recursive implementation.
map_tail_correct.Theorem map_tail_correct :
forall A B (f : A -> B) l,
map_tail f l = map f l.
Proof.
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.
Admitted.
Here is a (trivial) language of arithmetic expressions consisting of nested sums of constants.
Inductive expr : Type :=
| Const : nat -> expr
| Plus : expr -> expr -> expr.
Here is a straightforward evaluation function for the expression language.
Fixpoint eval_expr (e : expr) : nat :=
match e with
| Const n => n
| Plus e1 e2 => eval_expr e1 + eval_expr e2
end.
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.)
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.
Here is a theorem relating the two evaluators.
eval_expr_tail_correct.Theorem eval_expr_tail_correct :
forall e,
eval_expr_tail e = eval_expr e.
Proof.
Prove this by finding and proving (by induction) a suitable helper lemma.
Admitted.
Here is another evaluator, this one in continuation-passing style.
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).
And its correctness theorem.
eval_expr_cont_correct.Theorem eval_expr_cont_correct :
forall e,
eval_expr_cont e = eval_expr e.
Proof.
Prove this by finding and proving (by induction) a suitable helper lemma.
Admitted.
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.
Inductive instr := Push (n : nat) | Add.
Definition prog := list instr.
Definition stack := list nat.
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.
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.
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.)
Fixpoint compile (e : expr) : prog :=
match e with
| Const n => [Push n]
| Plus e1 e2 => compile e1 ++ compile e2 ++ [Add]
end.
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.
eval_expr_cont_correct.Theorem compile_correct :
forall e,
run (compile e) [] = [eval_expr e].
Proof.
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.
Admitted.
Here is a naive (exponential time) implementation of a function to compute the nth Fibonacci number.
Fixpoint fib (n : nat) :=
match n with
| 0 => 1
| S n' => match n' with
| 0 => 1
| S n'' => fib n' + fib n''
end
end.
And here is a tail-recursive (linear time) solution.
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.
Here is a correctness theorem for the optimized version.
eval_expr_cont_correct.Theorem fib_tail_correct :
forall n,
fib_tail n = fib n.
Proof.
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.
Admitted.