The Coq mailing list

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

Thanks to everyone for all the responses!  It's nice to see a range  
solutions to this issue, from Georges's (predictably :-)  
sophisticated approach and Arnaud's interesting-sounding refinement  
of the proof engine to Benjamin's useful low-tech hack and Adam's  
proof-structuring alternative.  I'll do some experimenting and see  
which is most comfortable for the proofs I'm doing now (in the  
context of preparing my graduate course on operational semantics and  
type systems, as I signaled a few weeks ago).

A priori, I find Adam's philosophy -- that proofs should be rather  
automatic and opaque *after* all their important ideas have been  
broken out as lemmas -- rather persuasive (and indeed not necessarily  
incompatible with Gerard's remarks)...

    - Benjamin


On Sep 5, 2007, at 9:23 AM, Georges Gonthier wrote:

>   Well, since, as I understand it, the solution Arnaud mention is  
> inspired
> by the one I've been using in the soon-to-be-released ssreflect  
> extension
> package, perhaps I should chime in and explain how we've been doing  
> things,
> especially since this addresses both of Benjamin's concerns.
>   There are really two issues here:
>    - preventing silent fall-through from one branch of the proof to  
> another;
>    - putting checkable labels on case or induction branches.
> These are orthogonal but not quite independent features (think of the
> infamous C switch statement).
>    The first issue, which addressed by the mechanism below, is more  
> general:
> it occurs with any tactic that produces multiple subgoals.
> Ssreflect proposes a two-pronged approach: it provides
>   - a 'by' tactical for closing a branch,
>   - and a "bullet" comment to mark up the opening of a new branch.
> A typical multi-branch proof is laid out like so:
>   apply some-lemma.
>   - start-proof-of-1st-assumption.
>     by end-proof-of-1st-assumption.
>   - by prove-2nd-assumption.
>   start-proof-of-main-assumption.
>   ...
> Now "by tac1; tac2" just means "tac1; tac2; done" where done is a  
> tactic
> that ends with solve [...], so "by tac1; tac2" tells Coq that it  
> must solve
> all subgoals produced by tac1; tac2, using the recipe provided by done
> (approximately, trivial + symmetry + discriminate + split).
>    Systemetically using "by" to terminate branches, even when it is  
> not
> strictly needed (as in "by auto with arith"), is sufficient to  
> ensure that
> the script and the prover are in sync.
>   Note that "by" doesn't provide a visual cue to the start of  
> branches;
> this is provided by the "-" bullets (and "+" and "*"), but these  
> are not
> checked; the extension mentioned below would add checked bullets.
>   I've found the simple by/- combination quite effective, however.
> You could implement "by" with Tactic Notation, and use (**) for  
> bullets, if
> you don't want to wait for or use an extended Coq. Indeed, I've not  
> yet
> convinced that it's a good idea to enforce bullet checks in the  
> prover,
> as opposed to the IDE, because they are tied to the use of  
> indentation.
> I usually replace the last bullet by negative indent as in the example
> above, to avoid creeping left margins, and omit single bullets  
> altogether,
> which are by far the most common case. And my IDE check is most  
> simple:
> hilighting "by" in red...
>
>   Ssreflect proposes a different mechanism to deal with the second  
> issue:
> elimination equations. You can write
>   elim Ehyp1: hyp1 => [...] in hyp2 hyp3 *.
> which is equivalent to
>   induction hyp1 as [...]
> except that
>   - it is checked that hyp1 only appears in hyp2, hyp3 and the goal
>   - it is guaranteed that the induction hypotheses have the form
>     (hyp2 -> hyp3 -> goal){h_i/hyp1}
>   - each branch gets an additional hypothesis Ehyp1 : hyp1 = Ki ...
>     where Ki ... is the term substituted for hyp1 in that branch
>     (the ... come from the => [...]).
> If you omit Ehyp1, then you don't get the latter equation.
>   Equation generation works is a generally useful feature, and  
> works for all
> elimination tactics; indeed, case Dx: x => ... is the most common  
> form, and
> corresponds the case_eq tactical that was added Coq 8.1.
>   The equation obviously tells you directly which branch you're in,  
> even
> after you've done some processing (as in elim Ehyp: ...; some-post- 
> tactic),
> and I've often used them in this way to debug a proof that had gone  
> astray.
>   Check (Ehyp1 : hyp1 = Ki ...).
> will verify that you're in the right branch statically; you can add a
> clear Ehyp1 if you don't really care about the equation, as this  
> will cause
> any fall-through Check to fail; you can also do this in Ltac, if  
> you prefer.
>
>   Georges
>
> -----Original Message-----
> From: coq-club-admin AT pauillac.inria.fr [mailto:coq-club- 
> admin AT pauillac.inria.fr] On Behalf Of Arnaud Spiwack
> Sent: 05 September 2007 09:58
> Cc: 
> coq-club AT pauillac.inria.fr
> Subject: Re: [Coq-Club] Basic question on navigating inductive proofs
>
> 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
>
>
> --------------------------------------------------------
> 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
>
> --------------------------------------------------------
> 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