Ssreflect Users Discussion List

[Enrico Tassi <>]

On Tue, Nov 05, 2013 at 05:13:06PM +0100, Pierre-Yves Strub wrote:
> Any hint on that ? I'm using the v8.4 plugin found in the repository
> with Coq 8.4pl2 and the trunk standard library.

We are investigating (I really mean 2 eyes are not enough here).

The issue has probably something to do with the first matching phase,
the one with no conversion, that used to fail for both rules in 8.3 but
now works for the second one (under some unclear circumstances)
resulting in the second rule being preferred to the first one.

Just for the records, when the goal is matched against a pattern (or a
set of patterns in the case of a multi rule) this happens in two phases:
1) head symbol driven but turning off conversion, hence addnA will not
   match "a + 2 * b" (that can reduce to "a + (b + ...)" and thus expose
   the LHS of addnA).  If this phase fails, the next one is tried.
2) head symbol driven with conversion, that is usually what you see in
   action, and that would rewrite "a + 2 * b" with addnA.  If this phase
   fails, an error message is given.

The implementation of 1) is shaky because it is based on the file
unification.ml that takes an option ~no_conversion but has been revised
many times from 8.1 to 8.4 changing its behavior.
I'd say that the majority of bugs that were recently reported by ssreflect
users were tracked down to phase 1).  At some point I've even started
rewriting 1) from scratch.  I found my old code, but is not finished :-/

Once we figure out exactly what goes wrong, two options are viable.

The first one is to replace once and for all 1) with a well specified
matching procedure.  This very fast matching procedure could also be
exposed to the user directly and may come handy when one deals with very
huge expressions containing latent heavy computations (I've encountered
this many times with Frederic and Assia while working with Maple-sized
polynomials coded using rat.  "Yes, we should use Q or QCanon, but if I
could just rewrite that term down here now...").

The second option is to say that for multi rules we do not use phase 1) to
select the rule that is used but only the term that is affected.  That
would solve the problem we see here, and give to multi rules a more
intuitive and robust semantics.

I'm also quite curious to see how often phase 1) succeeds and if its
justification (normalising associativity) is still very relevant.  I've
the impression that as soon as one does some algebra, phase 1) never
succeeds.
If we remove it, how many scripts would fail?  How many scripts would
need to pre process the goal with lock or bound a ! or use a
contextual pattern to work around the absence of phase 1)?
I don't know, but if we could get rid of it things would get much
simpler (to explain)...

Good night,
-- 
Enrico Tassi