Is it possible to postpone a proof?

Using Coq
1

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

2

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
admitted lemmas.

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 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
3

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.

4

@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
5

Thanks a lot for the explanations everyone!

Cheers,
Nicolás

6

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
7

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