This Coq-club thread contains an interesting discussion about how to stay oriented while doing large inductive proofs.

Benjamin Pierce suggests using a Case tactic to mark your progress.

Since Coq version 8.2, the best way of organizing a large proof is probably using C-zar, Coq's DeclarativeProof language []. You can use escape and return commands to include a procedural block in a declarative script, or proof and end proof to nest a declarative proof block inside a procedural proof script.

Cocorico: Organizing Large Proofs (last edited 04-05-2009 16:27:28 by oumix)