In math it is common to state a theorem, then state and prove auxiliary results, and finally prove the theorem using the intermediate results. That way one keeps the less important intermediate results out of the way and they do not pollute the statement of the main result.
Is it possible to set up a Coq development in this way (that is, state a result, but postpone the proof for later) ?
Admitted. a proof (instead of
Abort. the current proof and to declare the lemma as an
Axiom. This is very useful if you want to prove a lemma later, but the
lemmas have to be in the ‘right order’ in the
It once was possible to nest lemmas, but this feature is deprecated now.
By the way, you can use the command
Print Assumptions LEMMA to check
LEMMA still depends on admitted lemmas / axioms. This is
useful to check whether you are done with a proof that might depend on
Inside a proof, there is the
admit. tactic, which lets you switch to
another goal. If you have
admits left, you can not
Qed. the proof
(but have to use
There’s also the
coq-procrastination plugin, which lets you
defer some definitions and provide them later in the proof script
(when you know more constraints on the term).
The results that you prove using the as-yet unproved theorem can be seen as implications
MyTheorem -> MyCorollary. Modules can package it up nicely:
(* State (but don't prove) the main theorem *)
Module Type MYTHEOREM.
Parameter my_theorem : (insert theorem statement here).
(* Prove some corollaries from it *)
Module MakeCorollaries (MyTheorem : MYTHEOREM).
Lemma my_corollary1 : (something).
... apply MyTheorem.my_theorem. ...
(* Now prove the theorem separately. *)
Module MyTheorem : MYTHEOREM.
Theorem my_theorem : (insert theorem statement here).
(* The corollaries follow. *)
Module Corollaries := MakeCorollaries MyTheorem.
Modules are however a bit heavyweight. You can also prove the corollaries as plain implications
MyTheorem -> MyCorollary, and even make
MyTheorem a type class so corollaries can then be specialized implicitly.
@nojb I’d probably rely on the
Lemma/Theorem distinction, and possibly coqdoc comments to highlight the theorem. The alternatives have problems.
IIUC, the auxiliary results @nojb wants to prove are used to prove the theorem.
A possible solution is
Definition thm_stm := ∀ a b c, ... .
Lemma thm_aux1 : ...
Theorem thm: thm_stm.
But you’ll have to explain what you’re doing, since this is not a very common pattern.
However, if you turn a theorem statement into such a definition, some tactics using it might fail. You could also use a
Notation thm_stm := (∀ a b c, ... ) (only parsing).
Check (thm_stm : Prop).
That would avoid the problems with automation, but the Notation RHS is not typechecked when you define the Notation, but only when you use it — hence, you might need to pollute your script with
Check (thm_stm : Prop). as above.
Thanks a lot for the explanations everyone!
For the record, the feature was deprecated for a long time; it is now hidden behind a flag (
Nested Proofs Allowed) because it is confusing to newcomers, but it is no longer deprecated because there is no plan to remove the feature any time soon. It is still discouraged though, except for those users who absolutely need to rely on it because they are doing computational heavy proofs and it would be too costly to abort the current proof to prove an auxiliary lemma.
On this front, I have
Set Nested Proofs Allowed. in my
~/.coqrc file, and usually nowhere else. This means nested proofs are accepted interactively, but not by
coqc, which works well for my workflow.
You can rely on
Set Nested Proofs Allowed. in your proofs, but that breaks asynchronous compilation, which allows proofs to be processed in parallel by most editors (except Emacs+ProofGeneral) and on the command line (see manual). It especially interferes with the new
make vos +
make vok workflow in Coq 8.11, which is really cool (see manual).