The Coq mailing list

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

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

> On Fri, Aug 31, 2012 at 12:27 PM, AUGER Cédric 
> <sedrikov AT gmail.com>
> wrote:
> > 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.
> 
> In fact, the only thing I use omega for is in the obligations
> expressing that the measure (5 * length l + i) decreases on each
> recursive call -- which is why I was proving length > 0 for maximum
> convenience in this proof.  And the completeness proof, which is the
> one running slowly, isn't using omega at all.

I know it, but the aim was just to make proof terms (a little) smaller.

> So I doubt that using
> an intermediate AST would change anything in terms of performance --
> what difference would it make whether the term is Z.plus n m or
> plus_node t1 t2?

What do you mean by performance? Code extracted performance? Time spent
to prove things in Coq? Time spent for Coq to check/generate the proof?

For code extracted performance, I guess that the AST would degrade
them, but it would be neglictable.

For time spent to prove stuff in Coq, it is not clear.
You have to do two times the job: list token → AST and AST → Z.
But the first step does not involve computation at all (by computation
I mean inspecting the contents of the intermediate results to provide a
new one, like "z1 + z2" when z1 and z2 have been computed recursively,
but not "Plus z1 z2", where Plus is just a constructor).
And the second part would not have to deal with the "++" operator and
all its associated lemmas.

So both parts would be (a little) easier to write and also to read.
I guess, it would also be easier to specify.

For time spent by Coq to check/generate the proof, I did not examine
enough your code to see if it has some back-tracking. If so, splitting
the proof into two easier parts may result on an earlier backtrack in
case of a failure, and so be faster.

I do not pretend it would be better to use an AST, but for some
external people like me, it would have been simpler to read the code,
as each step would be slightly simpler.

> I guess the monster obligation tactic could
> definitely use some more documentation on what each part of it is
> trying to accomplish (or splitting into separate tactics with more
> self-explanatory names).
> 
> My thinking on making it evaluate the expression as it goes was to
> illustrate how easy it is to incorporate "semantic actions" into the
> parser and the proof of correctness.  And in reality, even a parser
> into an AST will involve some (shallow) semantic actions, unless you
> want the AST to include useless conversion nodes from factor ->
> summand -> expr, parenthesis nodes, etc.