The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

Hi thread,

I'm kinda sorry, I was a bit abroad, didn't read all the mails, let the 
mailling lists bombing me with thousands of new technical stuff every day.

However, I guess I had to mention that some work around the proof engine 
is currently being done. One of the feature that is meant to be 
implemented is related to that. Even though its final form is not 
currently known, the goal is to give a native tool (not only manual 
indentation and commenting) to structure a proof. Unfortunately, we will 
not be able at this point to provide some stuff like "Case 0", "Case S", 
though this was seen as an interesting long term option. But we want to 
introduce keywords to ensure that a certain goal is being solved 
entirely before we move to the next one, which resembles the feature you 
are asking for.


PS : in any case, the old dirty way is still possible, thus tacticals 
won't be affected. This is an optional mechanism.


Arnaud Spiwack


Benjamin Pierce a écrit :
> 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.
>
>
> --------------------------------------------------------
> Bug reports: http://logical.futurs.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>          http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club