Organizing Large Proofs

Pierre Letouzey edited this page Oct 12, 2017 · 7 revisions
Clone this wiki locally

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.