# Zulip Chat Archive

## 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 (@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 (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):

#### 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`

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

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

#### Kenny Lau (Dec 03 2018 at 22:17):

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