The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

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.  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?  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.
-- 
Daniel Schepler