The Coq mailing list

[Stefan Monnier <monnier AT iro.umontreal.ca>]

>> When writing or reading big inductive proofs in Coq, I find it's quite
>> difficult to keep track of which case of the induction one is in at any
>> given moment: The proof script doesn't signal explicitly when one case is
>> finished and we are moving on to the next.
>> What do people do about this?

> My opinion is that, in any proof complicated enough to make this a problem,
> you should prove each inductive case as its own lemma. Then, add each lemma
> as an 'auto' hint, possibly to a database just for the theorem that you want
> to prove. Now the final proof is just 'induction something; eauto with
> MyDatabase.'. The end result should be more readable than anything just
> using a single proof script, as you have the setting of each inductive case
> spelled out explicitly in your code. (You can even make the proof easier to
> understand by dropping hypotheses that aren't needed on a per-case basis.)

The problem I have with separate lemmas is that it forces you to write the
whole statement (i.e. type) of the lemma, which may be large and is
otherwise automatically computed/inferred by Coq.

I'd like my Lemmas to be kept within the scope of the larger proof.  I guess
what it could look like within the tactics language is a tactic "postpone_to
<name>" which just accepts the current goal and generates a lemma <name>
that you need to prove later (but whose type is already given, so you can
just do "Lemma <name>. <proof>".


        Stefan