The Coq mailing list

[e AT x80.org (Emilio Jesús Gallego Arias)]

Hi Kenneth,

a couple of comments:

Kenneth Roe 
<kendroe AT hotmail.com>
 writes:

> 1) Use a bignum format for natural numbers rather than the current
> "successor" format.  Right now, using Talia Ringer's printAST library,
> I get the following representation for "100":
>
> printAST 100.

Umm, I think that "printAST" of 100 may not be the best name, as the AST
of 100 is:

(CPrim (Numeral 100 true))

Such primitives are then interpreted by the notation system to various
numerical formats that include binary and bignum representations,
depending on what options / packages you have enabled.

> 2) Intern symbols.
> 3) Intern subexpressions.

Coq uses hash-consing extensively, so indeed in many cases equality is
cheap; YMMV in the tactic layer thou, but I am not expert.

> 4) Maintain special handling for operators with associative and
> communitive properties.  In my system operators with these properties
> have there terms sorted before interning the expression.  Hence,
> "x+y+z" and "x+z+y" will be the same node in the sub term intern DAG.

Indeed better support for this in Coq would be great; the acc tactics
package provides some support for that, and IMHO it would be great if at
some point it would be distributed with Coq.

E.