How to Structure Proofs
General Structure
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.