The Coq mailing list

[Enrico Tassi <enrico.tassi AT inria.fr>]

On Fri, Aug 01, 2014 at 03:28:01PM +0200, Matthieu Sozeau wrote:
> As an experiment, I tried to implement a strategy closer to ssreflect’s
> (without the canonical structure hints) which applies conversion in all
> cases as soon as the head symbol of the subterm matches (syntactically here)
> the head symbol of the left hand side. It turns out, most of the standard
> library of Coq already abides with this heuristic and the performance cost
> seems minimal.

That looks good!  I was indeed feeling a disturbance in the force ;-)

> > I don't have strong opinions on how to define the classes (by hints for
> > the unification algorithm or by another mean) but I believe the whole
> > system should take them into account, consistently.
> 
> Agreed, a set of hints would greatly help here and be used in the indexes 
> for auto, autorewrite etc… You’re saying simply doing indexing modulo the 
> equality of head symbols like sf and list would suffice? That sounds easy
> enough to implement.

I'm saying that even if "unification" would succeed, sometimes you don't
even try because you index terms in a very simplistic way.  E.g. the
head symbol of the coercion source and target type.

In Matita coercion (and auto) lookups are up to these classes.  Then,
when you find a candidate (coercion or lemma) you insert/apply it using
the regular unification algorithm, that does do some conversion.

This is clearly faster than trying to typecheck any coercion
application, and it is smarter that trying only the coercions
that trivially work (even with conversion turned off).

IIRC we had a standard "imperfect discrimination tree", where the lookup
term is preprocessed by replacing its symbols with the corresponding (up
to date) eq class.  Then the search works the same, but istead of symbol
comparison you use set membership.  No idea is this works fine with the
discrimination nets I've seen in the sources of Coq.

Ciao
-- 
Enrico Tassi