The Coq mailing list

[Benjamin Pierce <bcpierce AT cis.upenn.edu>]

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?

Here's one idea I've been wondering about.  I suppose it would not be  
impossible to write a variant of the induction tactic (say,  
induction_with_cases) that would somehow leave a marker at the top of  
each subgoal, containing the name of the case that generated it.   
(I.e., a subgoal "prove P" arising from case C of an inductive  
definition would become a goal of the form "prove something trivial  
involving the string C and then prove P.")  Then one could have a  
tactic "Case C" that would supply the trivial proof involving C and  
uncover the subgoal P to be proved next.  Now a proof by induction  
would look like this:

  Proof.
    intros.
    induction_with_cases H1.
      Case C1. ...
      Case C2. ...
     ...
  Qed.

One problem I can see with this is that notations like  
"induction; ..." would not work so well -- perhaps there would need  
to be a variant of ; (or something to put at the beginning of the  
"...") that would treat the case markers in the subgoals  
transparently.  And perhaps there are other problems that I don't  
see. :-)

Would this be a good idea?  Has it been done?

Thanks,

    - Benjamin

P.S.  I'm sure this general topic must have been discussed before,  
but I'm not sure what keywords to search for...!  Pointers appreciated.