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 [http://www.lix.polytechnique.fr/coq/distrib/current/refman/Reference-Manual014.html]. 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.

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

Cocorico!WikiLicense