The Coq mailing list

[Adam Chlipala <adamc AT cs.berkeley.edu>]

Benjamin Pierce wrote:
> When writing or reading big inductive proofs in Coq, I find it's quite 
> difficult to keep track of which case of the induction one is in at 
> any given moment: The proof script doesn't signal explicitly when one 
> case is finished and we are moving on to the next.
>
> What do people do about this?

My opinion is that, in any proof complicated enough to make this a 
problem, you should prove each inductive case as its own lemma. Then, 
add each lemma as an 'auto' hint, possibly to a database just for the 
theorem that you want to prove. Now the final proof is just 'induction 
something; eauto with MyDatabase.'. The end result should be more 
readable than anything just using a single proof script, as you have the 
setting of each inductive case spelled out explicitly in your code. (You 
can even make the proof easier to understand by dropping hypotheses that 
aren't needed on a per-case basis.)

If you're just trying to prove a theorem without being concerned about 
leaving an artifact that others can read to "understand" the proof, then 
best yet is if you just automate the whole thing inside a single proof 
script by adding plenty of hints ahead of time and skipping the lemmas!