# Is it possible to postpone a proof?

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) ?

Thanks!
Nicolás

You can `Admitted.` a proof (instead of `Qed.` or `Defined.`). This
means to `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 `.v` file.

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
whether `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 `admit`s left, you can not `Qed.` the proof
(but have to use `Admitted.` instead).

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).

3 Likes

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).
End MYTHEOREM.

(* Prove some corollaries from it *)
Module MakeCorollaries (MyTheorem : MYTHEOREM).
Lemma my_corollary1 : (something).
Proof.
... apply MyTheorem.my_theorem. ...
Qed.
End MakeCorollaries.

(* Now prove the theorem separately. *)
Module MyTheorem : MYTHEOREM.
Theorem my_theorem : (insert theorem statement here).
Proof.
...
Qed.
End MyTheorem.

(* 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`:

``````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.

1 Like

Thanks a lot for the explanations everyone!

Cheers,
Nicolás

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.

2 Likes

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).

1 Like