Ssreflect Users Discussion List

[Maxime Dénès <>]

Hello Georges and Enrico,

Is the flag you mention "default_no_delta_unify_flags" in 
unification.ml, which sets "modulo_betaiota" to false but leaves the 
default "modulo_eta" (true)?

I can relay the problem on coqdev if you wish, so that we know if this 
was intended for some reason or if a record field update was simply 
forgotten (and get it fixed, in this case).

As for the change of behavior of the cooking, did you trace it?

Maxime.

On 11/07/2013 10:05 AM, Georges Gonthier wrote:
> Well we finally did work it, and here's the somewhat long story.
> The quick summary is that this is the consequence of a small regression in 
> Coq 8.4, that also masked a second v8.4 regression.
> The problem may also cause us to revisit a somewhat arbitrary design decision 
> in the ssr matching algorithm, though we are still evaluating that.
>
>     As per Enrico's answer, you are getting this behaviour because the "literal 
> match" clause of the ssr matching algorithm gets triggered; this overrides the 
> usual left-to-right order to give precedence to patterns that match exactly, without 
> conversion.
>    Specifically, here "no conversion" means no expansion of constants 
> (delta), lets (zeta), and no beta-reduction. These restrictions entail that
> in 8.3 the clause is never triggered in your example, because the left-hand 
> side of rules declared with the {morph ...} notation always consist of 
> explicit beta redexes, e.g. ,
>     the lhs of fB is f ((fun x y => x - y) ?x ?y)
>     the lhs of fD is f ((fun x y => x + y) ?x ?y)
> and since your goal does not contain beta redexes (which Coq reduces quite 
> eagerly), these never match literally (of course, they do so up to 
> conversion).
>    Now it just happens that beta-redex in the lhs of fD is also an eta-redex. 
> Unfortunately, the Coq developers forgot to turn off the newly added eta-expansion in 
> the standard "no_conversion" flags in unify.ml -- and we didn't recheck 
> behind them when we ported. Hence, in 8.4, fD matches (up to eta),
> while fB only matches up to beta.
>    Matching of the generic raddfB and raddfD lhs actually fail earlier, for a 
> different reason, which holds in both 8.4 and 8.3. Because f is not really a CiC 
> function, but an {additive rT -> rT}, the application f ... actually stands 
> for the coercion
>     @GRing.Additive.apply zT zT (Phant (T -> T)) f ...
> where zT stands for (GRing.Ring.zmodType rT) (the Z-module substructure for 
> rT) and T for (GRing.Ring.sort rT) (the carrier Type for rT).
> Note that both zT and T are normally displayed as rT. Now raddfD expects a 
> lhs of the form
>     @GRing.Additive.apply ?U ?U (Phant (GRing.Zmodule.sort ?U -> 
> GRing.Zmodule.sort ?U)) ?f ...
> which requires the conversion from GRing.Zmodule.sort zT to T in order to 
> match the above, so raddfD could never match without conversion.
> (This is a bit silly, because the dummy Phant term is only used to implement the 
> {additive ...} notation, but has to be an argument of the Additive.apply coercion to 
> comply with the infamous "uniform inheritance" restriction.)
>     As a first fix we have explicitly turned off eta-expansion during literal 
> matches; this exposed another undocumented 8.4 regression, namely that 
> Sections no longer beta-normalize lemma statements. This normalization 
> removed the beta redexes in the statement of the group morphism lemma
>    morphM : {in D &, {morph f: x y / x * y}}
> allowing the use of the literal matching clause for morphM to avoid spurious 
> expansion of group conjugation expressions x ^ y (the {in ...} notation
> exposes the predicate hidden in the {morph ...} notation). There was one use 
> of this in gproduct.v, which therefore was broken in 8.4, but this was masked 
> by the eta-expansion loophole.
>    There is another reasonable fix for this issue, which would be to allow 
> both beta, iota, and eta in literal matching (blocking only delta and zeta). 
> We're experimenting with that, for now.
>
>     Cheers,
> Georges
>
> -----Original Message-----
> From: Enrico Tassi []
> Sent: 05 November 2013 21:54
> To:
> Subject: Re: [ssreflect] Inconsistant behaviour of rewrite (...,...)
>
> 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