The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Fri, 31 Aug 2012 09:13:29 -0700,
Daniel Schepler 
<dschepler AT gmail.com>
 a écrit :

> 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.

It was too long for me to check all, but I was wondering if using some
AST wouldn't simplify things.

I mean having some "list token -> expression_tree" which does not
involve arithmetic at all on one side and a "expression_tree -> Z" on
the other side which does involve arithmetic, but no list managing.

I guess it would improve the readability of the developpement, though
extracting to Ocaml may give some less efficient code as the full AST
should be built before proceeding (as Haskell is lazy, it wouldn't be
that less efficient to do so).

I also see that you defined "non_empty (l:list token)" as "length l >
0", where I would have defined "Inductive netokens : list token -> Prop
:= NEtok_intro : forall t l, netokens (t::l)." which avoids using
arithmetic and the omega tactic.