The Coq mailing list

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

On Thu, Jul 31, 2014 at 06:48:25PM +0200, Xavier Leroy wrote:
> Why just a stop-gap and not a proper fix?

I think the issue you raised is more general that what one may think.
I agree one should look for a proper fix, that IMO must be system-wide,
not just for a tactic.

In Matita we had the luck to see this issue on a young system we could
hack on easily.  What follows is what we did.  A similar solution may
apply to Coq as well.

The problem arises when one starts to play with any form of term indexing.
Term indexing is inherently weaker than conversion, usually one indexes
up to syntactic equality.  Term indexes are used everywhere.  Coercions
from A to B are indexes over (A,B), or better the head symbols of A and
B; databases of lemmas for automatic tactics are index on the symbols
as well (you don't want eauto to blindly try to apply any theorem
right?); decision procedures have to recognize the domain they master
(like Omega); etc...

In Matita the problem popped up as soon as we started doing algebra.
In that setting "Z" and the carrier of the additive group over the integers
"carr ZGrp" are synonims (ZGrp being a record packaging Z with + etc...). 
Both denotations for the type of integers ended up in the same goals
(that is very hard to avoid).
Immediately the system became stupid.  Eg. the coercion from Z to Q was
not applied, because the term had a type convertible to Z but denoted
using a different head constant; automation was pruning lemmas because
they were on Z and the goal on ZGrp, or viceversa.

The only thing that was working was unification thanks to a set of hints
that are declared by the user (that would be a Canonical Structure in
Coq's terminology).  In the syntax of Matita a hint would like the
following one.

     ?X := ZGrp
   -------------
    carr ?X = Z

That reads "whenever you face an unification problem like carr ?X = Z,
use this solution: ?X := ZGrp".  If you ignore the solution given by the
user, and take into account only the head constants in the conclusion of
"the rule", you can read the hint as "carr and Z are in the same class".

Now, if are looking for a coercion from "carr ZGrp" to Q, you actually
look for a coercion from any symbol in the same class of "carr" (that
includes Z) to Q (actually, any symbol in the class of Q), and you do
find Z_to_Q.

Hopefully the size of these classes is smaller than of size of classes
given by the conversion relation: you have more candidates to test with
the real conversion/unification algorithm than you had with the
simplistic syntactic filtering, but you don't have to blindly try all
possibilities, you try only the ones hinted by the user.

In Matita this worked rather decently: we have just 1 indexing data
structure (IIRC a discrimination tree) that works up to equivalence
classes of symbols (given by the user) and it was used everywhere, for
coercions, eauto, eauto+rewrite...

Hints like

  --------------------------------------
    sf = list (terminal + non_terminal)

or 

  -----------
    Z = word

would be of no help to the unification algorithm, since both sides
are closed and conversion is complete on closed terms.  But could play
a role in term indexing, and make omega, lia and company less shaky (if
they all use the same indexing data structure of course).

Curiously enough I discovered that the approach we used in Matita was
also part of the code Goerges  wrote for his original implementation of
rewrite for ssreflect. In ssr equations are indexed using only the head
symbol of their (say) LHS.  So one may have the LHS look like "op
SomeGrp a b" and hence "op" as the key of the commutativity law of an
abelian group, but have + (Zplus) in his goal.  Once again these two
constants ("op" and "+") are different, but a hint like

       ?X := ZGrp
  --------------------
    op ?X a b = a + b

could help the system behaving in a smart way.  In ssr this is what the
code does by hand: if the head symbol is a canonical projection we
consider it equal to any canonical value associated to it.

I don't know how Coq's rewrite tactic indexes the terms for fast matching,
but if it were using an indexing data structure that takes hints into
account then it would behave in a smarter way: it would find matches
that do not match syntactically, but that the user hinted as matches
that work up to conversion (or unification).

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.

My 2 cents,
-- 
Enrico Tassi