Stream: general

Topic: norm_num

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.

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.

Mario Carneiro (Dec 03 2018 at 20:28):

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

Mario Carneiro (Dec 03 2018 at 20:28):

which is basically what norm_num does

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?

Patrick Massot (Dec 03 2018 at 20:34):

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

Patrick Massot (Dec 03 2018 at 20:34):

and it's in core lib :sad:

Mario Carneiro (Dec 03 2018 at 20:43):

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

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

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

Mario Carneiro (Dec 03 2018 at 20:45):

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

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)

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
(@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
(@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 (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.

Rob Lewis (Dec 03 2018 at 21:15):

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

Luca Gerolla (Dec 03 2018 at 21:36):

20180814_193304.jpg

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

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.

Rob Lewis (Dec 03 2018 at 21:43):

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

468?

Mario Carneiro (Dec 03 2018 at 22:01):

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

Mario Carneiro (Dec 03 2018 at 22:02):

you mean before the ext_simplify_core?

Patrick Massot (Dec 03 2018 at 22:02):

Booooo! Rob is not running up to date mathlib

Mario Carneiro (Dec 03 2018 at 22:03):

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

Rob Lewis (Dec 03 2018 at 22:04):

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

Rob Lewis (Dec 03 2018 at 22:04):

So make that the first line of the do block.

Mario Carneiro (Dec 03 2018 at 22:05):

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

Mario Carneiro (Dec 03 2018 at 22:06):

or is the problem uninstantiated metavars in the user input

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.

Mario Carneiro (Dec 03 2018 at 22:09):

we could just check for unify instead of alpha equivalent

Mario Carneiro (Dec 03 2018 at 22:10):

eh, I guess that doesn't make sense here

Mario Carneiro (Dec 03 2018 at 22:11):

yeah okay, ship it

ship who?

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

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?

Mario Carneiro (Mar 24 2020 at 18:56):

It is used for the norm_num tactic

Yury G. Kudryashov (Mar 24 2020 at 19:02):

The norm_num tactic in mathlib?

Yury G. Kudryashov (Mar 24 2020 at 19:02):

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

Mario Carneiro (Mar 24 2020 at 19:03):

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

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

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?

Mario Carneiro (Mar 24 2020 at 19:07):

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

Kevin Buzzard (Mar 24 2020 at 19:08):

move the tests to the mathlib repo?

Mario Carneiro (Mar 24 2020 at 19:09):

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

Kevin Buzzard (Mar 24 2020 at 19:10):

move all of Lean into mathlib?

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.

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.

Yury G. Kudryashov (Jun 28 2020 at 23:02):

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

Yury G. Kudryashov (Jun 28 2020 at 23:03):

@Mario Carneiro :up:

Mario Carneiro (Jun 29 2020 at 02:38):

I think it is not imported by anything right now

Yury G. Kudryashov (Jun 29 2020 at 13:54):

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

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.

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.

Johan Commelin (Jun 29 2020 at 13:59):

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

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