The following is an example of the structure you should use when proving
something by structural induction (rule induction for abstract syntax). This
will be the case for most proofs in this class.
Theorem:
If X then A.
Proof by induction on the structure of the derivation J.
Foo-1
(p1)premise 1
...(pn)premise n
conclusion
Foo-1
(1)...
[by (p1) and Lemma 1]
(2)X[by assumption]
(3)...
[by (1)
and (2)]
......
(n)A
[by (n-3) and
(n-1)]
Foo-2
(p1)premise 1
...(pn)premise n
conclusion
Foo-2
Similar to case Foo-1.
Bar
(p1)premise 1
...(pn)premise n
conclusion
Bar
(1)...
[by (p1) and Lemma 3]
(2)...
[by (p2) and
I.H. on (p3)]
(3)
...
[by (1)
and (2)]
......
(n)A
[by (n-3)
and (n-1)]
Rules to Prove By
Clearly state the induction hypothesis.
Clearly state the proof methodology (what you are doing induction on).
There should be one case for each rule in the inductive definition.
Use a two-column format where the left side contains the logical steps and the
right side contains the reasoning for each step. In general, do not attempt to
write your proof in English sentences. While some written explanations can be
useful, normally they (attempt to) hide the fact that the proof is imprecise
and has holes in it.
Number your steps for easy reference.
Always state where you use the induction hypothesis.
If two cases are very similar, you can prove the first and then say that the
second follows similarly. Just be certain that the cases are really, truly
similar. (For example, the case for projecting the first element of an pair and
the case for projecting the second element of a pair are similar.)
If for some reason you can't prove something in the middle of a proof (because
you don't have time, you don't know how, etc), please don't try to hide that
fact. Use the fact you need and in the reasoning next to it, say something like
"I can't figure out how to conclude this, but it should be true".
Always break down a proof into appropriate lemmas. The result of not
introducing new lemmas where appropriate is usually that you try to proceed
with your proof using the wrong induction hypothesis.
If you define new judgements, make sure you clearly define the judgement before
you begin using it.
Induction Hypothesis Structure
Depending on the structure of your induction hypothesis, you may make different
assumptions and must prove different things.
Induction Hypothesis
Can Assume
Must Prove
If X and Y
then A.
X and Y
A
If X or Y
then A.
(1)
X
A
AND(2)
Y
A
If X then A
and B.
X
A and B
If
X then A
or B.
X
A or B
Most of these are pretty straightforward, but notice the second case where the
condition is X or Y. In this
case, there are two things to prove. You must show that if you are given just
X or just Y, you will always
be able to prove A.
Suggestions on proof writing blatantly stolen from Dave Walker. Page maintained
by frances@cs. Last updated 8/30/2004.