norm_num

Stream: general

[Sebastien Gouezel]

I was under the impression that norm_num was always successful in its range of expertise. Here is a real-life counterexample:

lemma crazy (k l : ℕ) (h : l ≤ k): ((2:real)⁻¹)^k ≤ (2⁻¹)^l :=
begin
  apply pow_le_pow_of_le_one _ _ h,
  norm_num,
  -- goal is 2⁻¹ ≤ 1
  norm_num
end

The last norm_num call gives rise to a deterministic timeout. Replacing it with show 2⁻¹ ≤ (1 : real), by norm_num works fine, so this is not really a problem for me, but still surprising.

[Kevin Buzzard]

import data.real.basic tactic.norm_num

lemma crazy (k l : ℕ) (h : l ≤ k): ((2:real)⁻¹)^k ≤ (2⁻¹)^l :=
begin
  apply pow_le_pow_of_le_one _ _ h,
    norm_num,
  -- goal is 2⁻¹ ≤ 1
  show (2⁻¹ : ℝ) ≤ 1,
  norm_num,
end

I've seen this before, but don't remember why it's happening.

[Mario Carneiro]

norm_num is fighting with simp. Compare with norm_num1, simp, norm_num1, simp,

[Mario Carneiro]

which is basically what norm_num does

[Sebastien Gouezel]

Does it mean that it would be more safe for norm_num to call simp [-one_div_eq_inv]? By the way, I am not convinced that one_div_eq_inv is a good simp rule, what do you think?

[Patrick Massot]

It's the same family that turns every a-b into a+-b that I hate

[Patrick Massot]

and it's in core lib :sad:

[Mario Carneiro]

a better question is why norm_num1 isn't solving the goal

[Mario Carneiro]

since it does solve the goal if you canonize the instances by restating the goal as you did

[Mario Carneiro]

I think this one is a result of my relying on the C++ norm_num implementation, which lags behind the mathlib implementation quite a bit

[Mario Carneiro]

I use it for doing + - * / on rings and fields, and do everything else in lean

[Mario Carneiro]

but I have seen it get confused with weird instances before (i.e. simp wants to prove that (0 : int) != (1 : multiplicative int) even though it's false)

[Sebastien Gouezel]

It is definitely confused by the instances. With pp.all, the goal it can not solve is

@has_le.le.{0} real
    (@preorder.to_has_le.{0} real
       (@partial_order.to_preorder.{0} real
          (@ordered_comm_monoid.to_partial_order.{0} real
             (@ordered_cancel_comm_monoid.to_ordered_comm_monoid.{0} real
                (@ordered_semiring.to_ordered_cancel_comm_monoid.{0} real
                   (@linear_ordered_semiring.to_ordered_semiring.{0} real real.linear_ordered_semiring))))))
    (@has_inv.inv.{0} real (@division_ring.to_has_inv.{0} real real.division_ring)
       (@bit0.{0} real
          (@distrib.to_has_add.{0} real
             (@ring.to_distrib.{0} real
                (@normed_ring.to_ring.{0} real (@normed_field.to_normed_ring.{0} real real.normed_field))))
          (@has_one.one.{0} real
             (@zero_ne_one_class.to_has_one.{0} real (@domain.to_zero_ne_one_class.{0} real real.domain)))))
    (@has_one.one.{0} real
       (@monoid.to_has_one.{0} real
          (@semiring.to_monoid.{0} real
             (@ordered_semiring.to_semiring.{0} real
                (@linear_ordered_semiring.to_ordered_semiring.{0} real real.linear_ordered_semiring)))))

while the "right" instance is the much nicer

@has_le.le.{0} real real.has_le
    (@has_inv.inv.{0} real (@division_ring.to_has_inv.{0} real real.division_ring)
       (@bit0.{0} real
          (@distrib.to_has_add.{0} real
             (@ring.to_distrib.{0} real
                (@normed_ring.to_ring.{0} real (@normed_field.to_normed_ring.{0} real real.normed_field))))
          (@has_one.one.{0} real
             (@zero_ne_one_class.to_has_one.{0} real (@domain.to_zero_ne_one_class.{0} real real.domain)))))
    (@has_one.one.{0} real (@zero_ne_one_class.to_has_one.{0} real (@domain.to_zero_ne_one_class.{0} real real.domain)))

[Rob Lewis]

Something in norm_num, either in C++ or in mathlib, is creating some metavars and leaving them uninstantiated. Adding e₂ ← instantiate_mvars e₂, before the guard at https://github.com/leanprover/mathlib/blob/master/tactic/norm_num.lean#L162 allows norm_num1 to kill the goal.

[Rob Lewis]

I haven't tracked down where the uninstantiated metavar is coming from yet.

[Luca Gerolla]

20180814_193304.jpg

[Luca Gerolla]

I also bumped into deterministic timeout few times when solving various inequality; the common situation was that I had goals involving some "variable" real number (i.e. not explicit - like the 'k' and 'l' in the example) and norm_num got in a loop (often involving 'one_div_eq_inv')

[Rob Lewis]

Hmm. I think the C++ norm_num instantiates mvars as a side effect, but only sometimes. It doesn't do it when it when the term is already in normal form.

[Rob Lewis]

Simple fix: e ← instantiate_mvars e, at norm_num.lean:468

[Mario Carneiro]

468?

[Mario Carneiro]

https://github.com/leanprover/mathlib/blob/master/tactic/norm_num.lean#L468

[Mario Carneiro]

you mean before the ext_simplify_core?

[Patrick Massot]

Booooo! Rob is not running up to date mathlib

[Mario Carneiro]

lol, you don't want to know what I'm running

[Rob Lewis]

Nope, the argument to derive should be instantiated before you do anything with it.

[Rob Lewis]

So make that the first line of the do block.

[Mario Carneiro]

why not 471/472? that's the first place after calling C norm_num

[Mario Carneiro]

or is the problem uninstantiated metavars in the user input

[Rob Lewis]

Yeah, exactly. At some point you compare the input with something that went through the C++ norm_num. The former has mvars, the latter doesn't.

[Mario Carneiro]

we could just check for unify instead of alpha equivalent

[Mario Carneiro]

eh, I guess that doesn't make sense here

[Mario Carneiro]

yeah okay, ship it

[Kenny Lau]

ship who?

[Mario Carneiro]

Not sure if this is a serious question, but this is an international forum, so... ship it

[Yury G. Kudryashov]

What is the purpose of algebra/norm_num in the Lean core library? Is it used for some tactic?

[Mario Carneiro]

It is used for the norm_num tactic

[Yury G. Kudryashov]

The norm_num tactic in mathlib?

[Yury G. Kudryashov]

I mean, can we move all these lemmas to mathlib?

[Mario Carneiro]

tactic.norm_num is in core, and norm_num in mathlib uses it

[Mario Carneiro]

we recently discussed having mathlib norm_num be implemented as standalone so that tactic.norm_num can be deleted

[Yury G. Kudryashov]

tactic.norm_num is a meta constant. Will it work if supporting lemmas will be in mathlib instead of stdlib?

[Mario Carneiro]

no, there are tests in the lean repo that would fail if you did that

[Kevin Buzzard]

move the tests to the mathlib repo?

[Mario Carneiro]

that's just breaking lean and pretending we didn't

[Kevin Buzzard]

move all of Lean into mathlib?

[Simon Hudon]

It's not really practical to move constants backed by C++ code outside of core. For now. In Lean 4 we could do something like that but not in Lean 3.

[Bryan Gin-ge Chen]

Out of curiosity, was the issue discussed at the start of this thread in Dec 2018 ever fixed? Yep, the example works in 3.7.2c and a recent mathlib.

[Yury G. Kudryashov]

Do we need init_/algebra/norm_num for some reason?

[Yury G. Kudryashov]

@Mario Carneiro :up:

[Mario Carneiro]

I think it is not imported by anything right now

[Yury G. Kudryashov]

I meant "it is not imported, may I remove it"?

[Johan Commelin]

Yup, I think it can go. I didn't pay close attention to what stuff was dead code when I ripped algebra out of core.

[Johan Commelin]

But since Mario rewrote norm_num, I think this is now a leaf and can be safely deleted.

[Johan Commelin]

(Unless you think there is something in there that is worth merging into the main tree.)

[Mario Carneiro]

When I did my second pass on Johan's import I specifically attended to making sure that everything in init_.algebra.norm_num that is needed by the new norm_num got moved where it needs to be, without importing it, exactly so that it could be deleted

[Yaël Dillies]

@Mario Carneiro, I broke norm_num in #14683. It does not infer the 0 < b argument to docs#norm_num.zpow_neg anymore. Do you think you could investigate?

[Mario Carneiro]

@Yaël Dillies fixed in #14852. The bug was there all along but it was causing a non-fatal error and simp used to find an alternative proof if you use norm_num instead of norm_num1.

[Mario Carneiro]

It appears the way this interacted with your PR is that simp would previously rewrite

  (@has_div.div real
     (@div_inv_monoid.to_has_div real
        (@division_ring.to_div_inv_monoid real
           (@field.to_division_ring real (@linear_ordered_field.to_field real real.linear_ordered_ring))))
     1
     9)
==>
  (@has_div.div real
     (@div_inv_monoid.to_has_div real
        (@field.to_div_inv_monoid real (@linear_ordered_field.to_field real real.linear_ordered_ring)))
     1
     9)

which would cause a failure in simp when applying transitivity with the bad proof in a place that would get ignored, and on your branch the term is

       (@has_div.div real
           (@div_inv_monoid.to_has_div real
              (@division_ring.to_div_inv_monoid real
                 (@field.to_division_ring real (@linear_ordered_field.to_field real real.linear_ordered_ring))))
           1
           9)

and simp is no longer interested in rewriting it, so the bad proof makes it to the top level and causes the failure. I guess you changed the instance search around division rings in some way?

[Yaël Dillies]

I added semifield and division_semiring under field and division_ring, so I had to change the inheritance around those parts.