The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT gmail.com>]

Hi,

On 1 août 2014, at 11:16, Enrico Tassi 
<enrico.tassi AT inria.fr>
 wrote:

> 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).

Coq’s rewrite does not use indexing, but restricts the subterm matching
procedure.

Basically, rewrite (in goal) starts by solving a higher-order unification 
problem 
?P LHS ~ goal. and allowing full conversion of the LHS with every subterm
of the goal could make it perform very badly.

So, it does not do unfolding of constants in general but allows full 
conversion 
on evar-free subterms in case the LHS _does_ contain an existential variable 
(evar)
initially. If it _doesn’t_ contain any, then it uses pure syntactic equality. 
This 
results in a rather frustrating situation indeed. For example:

Definition obj := nat.
Axiom op : forall {A} (l : list A), list A.
Axiom foo : forall l, @op nat l = l.

  l : list obj
  H : forall l' : list nat, @eq (list nat) (@op nat l') l'
  ============================
   @eq (list obj) (@op obj l) l

[rewrite H] will succeed, whereas [rewrite (H l)] won’t, as [nat] and [obj]
are syntactically different (!).

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.

> 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.

Thanks for your 2 cents,
— Matthieu