Zulip Chat Archive

Stream: general

Topic: norm_num


view this post on Zulip Sebastien Gouezel (Dec 03 2018 at 20:19):

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.

view this post on Zulip Kevin Buzzard (Dec 03 2018 at 20:27):

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.

view this post on Zulip Mario Carneiro (Dec 03 2018 at 20:28):

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

view this post on Zulip Mario Carneiro (Dec 03 2018 at 20:28):

which is basically what norm_num does

view this post on Zulip Sebastien Gouezel (Dec 03 2018 at 20:33):

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?

view this post on Zulip Patrick Massot (Dec 03 2018 at 20:34):

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

view this post on Zulip Patrick Massot (Dec 03 2018 at 20:34):

and it's in core lib :sad:

view this post on Zulip Mario Carneiro (Dec 03 2018 at 20:43):

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

view this post on Zulip Mario Carneiro (Dec 03 2018 at 20:43):

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

view this post on Zulip Mario Carneiro (Dec 03 2018 at 20:44):

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

view this post on Zulip Mario Carneiro (Dec 03 2018 at 20:45):

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

view this post on Zulip Mario Carneiro (Dec 03 2018 at 20:46):

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)

view this post on Zulip Sebastien Gouezel (Dec 03 2018 at 20:52):

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

view this post on Zulip Rob Lewis (Dec 03 2018 at 21:14):

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.

view this post on Zulip Rob Lewis (Dec 03 2018 at 21:15):

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

view this post on Zulip Luca Gerolla (Dec 03 2018 at 21:36):

20180814_193304.jpg

view this post on Zulip Luca Gerolla (Dec 03 2018 at 21:36):

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

view this post on Zulip Rob Lewis (Dec 03 2018 at 21:42):

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.

view this post on Zulip Rob Lewis (Dec 03 2018 at 21:43):

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

view this post on Zulip Mario Carneiro (Dec 03 2018 at 22:01):

468?

view this post on Zulip Mario Carneiro (Dec 03 2018 at 22:01):

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

view this post on Zulip Mario Carneiro (Dec 03 2018 at 22:02):

you mean before the ext_simplify_core?

view this post on Zulip Patrick Massot (Dec 03 2018 at 22:02):

Booooo! Rob is not running up to date mathlib

view this post on Zulip Mario Carneiro (Dec 03 2018 at 22:03):

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

view this post on Zulip Rob Lewis (Dec 03 2018 at 22:04):

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

view this post on Zulip Rob Lewis (Dec 03 2018 at 22:04):

So make that the first line of the do block.

view this post on Zulip Mario Carneiro (Dec 03 2018 at 22:05):

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

view this post on Zulip Mario Carneiro (Dec 03 2018 at 22:06):

or is the problem uninstantiated metavars in the user input

view this post on Zulip Rob Lewis (Dec 03 2018 at 22:06):

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.

view this post on Zulip Mario Carneiro (Dec 03 2018 at 22:09):

we could just check for unify instead of alpha equivalent

view this post on Zulip Mario Carneiro (Dec 03 2018 at 22:10):

eh, I guess that doesn't make sense here

view this post on Zulip Mario Carneiro (Dec 03 2018 at 22:11):

yeah okay, ship it

view this post on Zulip Kenny Lau (Dec 03 2018 at 22:17):

ship who?

view this post on Zulip Mario Carneiro (Dec 03 2018 at 23:22):

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

view this post on Zulip Yury G. Kudryashov (Mar 24 2020 at 18:53):

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

view this post on Zulip Mario Carneiro (Mar 24 2020 at 18:56):

It is used for the norm_num tactic

view this post on Zulip Yury G. Kudryashov (Mar 24 2020 at 19:02):

The norm_num tactic in mathlib?

view this post on Zulip Yury G. Kudryashov (Mar 24 2020 at 19:02):

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

view this post on Zulip Mario Carneiro (Mar 24 2020 at 19:03):

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

view this post on Zulip Mario Carneiro (Mar 24 2020 at 19:04):

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

view this post on Zulip Yury G. Kudryashov (Mar 24 2020 at 19:06):

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

view this post on Zulip Mario Carneiro (Mar 24 2020 at 19:07):

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

view this post on Zulip Kevin Buzzard (Mar 24 2020 at 19:08):

move the tests to the mathlib repo?

view this post on Zulip Mario Carneiro (Mar 24 2020 at 19:09):

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

view this post on Zulip Kevin Buzzard (Mar 24 2020 at 19:10):

move all of Lean into mathlib?

view this post on Zulip Simon Hudon (Mar 25 2020 at 00:35):

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.

view this post on Zulip Bryan Gin-ge Chen (Mar 25 2020 at 00:40):

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.

view this post on Zulip Yury G. Kudryashov (Jun 28 2020 at 23:02):

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

view this post on Zulip Yury G. Kudryashov (Jun 28 2020 at 23:03):

@Mario Carneiro :up:

view this post on Zulip Mario Carneiro (Jun 29 2020 at 02:38):

I think it is not imported by anything right now

view this post on Zulip Yury G. Kudryashov (Jun 29 2020 at 13:54):

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

view this post on Zulip Johan Commelin (Jun 29 2020 at 13:58):

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.

view this post on Zulip Johan Commelin (Jun 29 2020 at 13:58):

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

view this post on Zulip Johan Commelin (Jun 29 2020 at 13:59):

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

view this post on Zulip Mario Carneiro (Jun 29 2020 at 14:14):

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


Last updated: May 10 2021 at 00:31 UTC