The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Tue, Aug 28, 2012 at 1:45 PM, Daniel Schepler 
<dschepler AT gmail.com>
 wrote:
> I've just spent some time writing a certified parser, as I couldn't
> find any examples in Coq of such a thing with a quick Google search,
> and I was curious how the proofs might look.  (I did see a parser for
> something called IMP, I think; but it wasn't certified as to
> correctness or completeness with respect to any formal grammar, and
> furthermore it didn't bother to prove termination, just passed in a
> bound on recursion depth.)  It's not very short (but also not
> extremely long), so I posted it at
> http://coq.inria.fr/cocorico/ArithmeticExpressionParser .  There are
> still a couple points that I'd like to improve, but I can't quite
> figure out how:

OK, I've figured out some solutions and updated the Wiki page.  Along
the way, I discovered a nice way to autogenerate "proof context" from
monad invocations.  (Or more likely, rediscovered it, given how common
the problem must be when using monads in Coq or other interactive
theorem provers...)

But now several of the subcases in the completeness proof are taking a
lot longer than before (on the order of a minute, where before each
case took a few seconds at most).  I'm wondering if anybody has
suggestions for how to make them perform better.
-- 
Daniel Schepler