nlinarith: if at first you don't succeed...

Stream: general

[Eric Wieser]

There are no unicode tricks here, the examples contain exactly the same text

import tactic.linarith
import data.rat.basic

variables (x y : ℚ)

example
  (hx : x * x + x * x + y = 0) (hy : y * y + x * y + y = 0) :
  (y - x) * 2 = (x - y) * y :=
begin
  nlinarith, -- fails
end
example
  (hx : x * x + x * x + y = 0) (hy : y * y + x * y + y = 0) :
  (y - x) * 2 = (x - y) * y :=
begin
  nlinarith, -- works
end

What's going on?

[Scott Morrison]

Haha, I get the opposite failures. :-)

[Mario Carneiro]

I also replicated Eric's result

[Scott Morrison]

It works with my fix.

[Scott Morrison]

#17307

[Scott Morrison]

So you discovered the same bug in linarith I discovered while porting.

[Eric Wieser]

Isn't your bug at least deterministic?

[Scott Morrison]

The appearance of the bug is sensitive to ordering of variables used.

[Scott Morrison]

And apparently that is not deterministic??

[Eric Wieser]

Is this "ordering" in the sense of "some random hash of some garbage-named metavariables"?

[Mario Carneiro]

It might be due to the names of fvars?

[Mario Carneiro]

this is weird, I agree

[Eric Wieser]

I think it's deterministic with lean --make within a single process

[Eric Wieser]

And just not with the lean server

[Mario Carneiro]

variable ordering should not be nondeterministic

[Eric Wieser]

If your variables are named _mfresh.123 or whatever, are they guaranteed to be the same every time you run the tactic?

[Eric Wieser]

Or are those counters global within a module?

[Mario Carneiro]

they are a global counter

[Eric Wieser]

Then I bet if you put your variables in a name_set and iterate them, the iteration order is non-deterministic (as a function of human-visible state)

[Mario Carneiro]

but I would have expected linarith to name its variables in the order they occur in the hypothesis list

[Mario Carneiro]

Note that the one-liner test case I made for bug #17307 depends on the traversal order to get variables numbered in the right way

[Mario Carneiro]

Found it:

do s ← ls.mfoldr (λ h s', infer_type h >>= find_squares s') mk_rb_set,
   new_es ← s.mfold ([] : list expr) $ λ ⟨e, is_sq⟩ new_es,
     ((do p ← mk_app (if is_sq then ``sq_nonneg else ``mul_self_nonneg) [e],
       return $ p::new_es) <|> return new_es),

that's a monadic fold over an rb_set (expr ×ₗ bool)

[Mario Carneiro]

and expr.lt of course depends on the ordering of those unique names

[Eric Wieser]

Damn, beat me to it

[Eric Wieser]

I guess using list.dedup instead of mk_rb_set would solve the problem?

[Mario Carneiro]

yes

[Mario Carneiro]

what's more, that is usually better because we want to use defeq up to reducible or something like that

[Eric Wieser]

Surely list.dedup won't do that either?

[Mario Carneiro]

well I mean the algorithm

[Eric Wieser]

RIght, so just manually iterate and insert if none of the existing items match; which is unfortunately O(n^2), but I guess n is small

[Mario Carneiro]

the dedup is usually done manually, using logic like this

[Mario Carneiro]

yeah, nothing that can be done about that

[Eric Wieser]

find_squares looks like it needs a similar fix

[Eric Wieser]

Either that, or we should canonize the order after doing all the initial deduplicating

[Mario Carneiro]

the comment says something about the inputs having been canonized, not sure when that happens but it seems like it should have also numbered the atoms

[Mario Carneiro]

assuming we aren't doing any big changes to this code, I guess find_squares should accumulate two list exprs (or I guess list (expr * unit) to pass to find_defeq)

[Eric Wieser]

Do you plan to make the patch, @Mario Carneiro?

[Mario Carneiro]

no, unless you are having trouble

[Eric Wieser]

Do you think it's worth making at all, or is there little point with Scott's patch on the horizon?

[Mario Carneiro]

I think it is best not to have nondeterministic tactics. Scott's fix is an independent issue

[Eric Wieser]

In theory it ought to be externally deterministic irrespective of the order, right? I suppose we can't use a quot.lift in meta code to prove that...