## Stream: maths

### Topic: norm_num weirdness

#### Kevin Buzzard (Jan 17 2019 at 23:09):

What's going on here?

import tactic.norm_num
import data.real.basic

lemma floor_iff_bounds (r : ℝ) (z : ℤ) :
↑z ≤ r ∧ r < (z + 1) ↔ ⌊ r ⌋ = z :=
by rw [←le_floor, ←int.cast_one, ←int.cast_add, ←floor_lt,

-- set_option pp.all true
theorem floor_example : floor (71/10 : ℝ) = 7 :=
begin
rw ←floor_iff_bounds,
split,
{ norm_num},
-- ⊢ 71 / 10 < ↑7 + 1
-- norm_num, -- seems to hang
suffices : (71 : ℝ) / 10 < 7 + 1,
simpa using this,
-- ⊢ 71 / 10 < 7 + 1
-- norm_num -- deterministic timeout
sorry
end

example : (71 : ℝ) / 10 < 7 + 1 :=
begin
-- ⊢ 71 / 10 < 7 + 1
-- exactly the same term as the sorry above
-- even with pp.all true
norm_num -- works fine?!
end


Inside the bigger proof, I can't get norm_num to work, even though with pp.all on the goal seems to be exactly the same as the simpler example, where norm_num works fine. I checked the types with diff and there was no difference (unless I did something stupid)

#### Bryan Gin-ge Chen (Jan 17 2019 at 23:27):

And lean is happy with this:

import tactic.norm_num
import data.real.basic

lemma floor_iff_bounds (r : ℝ) (z : ℤ) :
↑z ≤ r ∧ r < (z + 1) ↔ ⌊ r ⌋ = z :=
by rw [←le_floor, ←int.cast_one, ←int.cast_add, ←floor_lt,

set_option pp.all true
lemma aux : (71 : ℝ) / 10 < 7 + 1 :=
begin
-- ⊢ 71 / 10 < 7 + 1
-- exactly the same term as the sorry above
-- even with pp.all true
norm_num -- works fine?!
end

theorem floor_example : floor (71/10 : ℝ) = 7 :=
begin
rw ←floor_iff_bounds,
split,
{ norm_num},
-- ⊢ 71 / 10 < ↑7 + 1
-- norm_num, -- seems to hang
suffices : (71 : ℝ) / 10 < 7 + 1,
simpa using this,
exact aux,
-- ⊢ 71 / 10 < 7 + 1
-- norm_num -- deterministic timeout
-- sorry
end


Weird.

#### Bryan Gin-ge Chen (Jan 17 2019 at 23:30):

And this works too:

import tactic.norm_num
import data.real.basic

lemma floor_iff_bounds (r : ℝ) (z : ℤ) :
↑z ≤ r ∧ r < (z + 1) ↔ ⌊ r ⌋ = z :=
by rw [←le_floor, ←int.cast_one, ←int.cast_add, ←floor_lt,

set_option pp.all true
theorem floor_example : floor (71/10 : ℝ) = 7 :=
begin
rw ←floor_iff_bounds,
split,
{ norm_num},
-- ⊢ 71 / 10 < ↑7 + 1
-- norm_num, -- seems to hang
suffices : (71 : ℝ) / 10 < 7 + 1,
simpa using this,
have  : (71 : ℝ) / 10 < 7 + 1 := by norm_num,
exact this,
-- ⊢ 71 / 10 < 7 + 1
-- norm_num -- deterministic timeout
-- sorry
end


#### Rob Lewis (Jan 17 2019 at 23:32):

This is really weird. The second norm_num works if you sorry the first. But then, bizarrely, if you change the first one to {suffices : (7 : ℝ) ≤ 71/10, simpa, sorry} the second norm_num fails.

#### Bryan Gin-ge Chen (Jan 17 2019 at 23:34):

Last one, I promise! This works too (probably should have tried this first):

import tactic.norm_num
import data.real.basic

lemma floor_iff_bounds (r : ℝ) (z : ℤ) :
↑z ≤ r ∧ r < (z + 1) ↔ ⌊ r ⌋ = z :=
by rw [←le_floor, ←int.cast_one, ←int.cast_add, ←floor_lt,

--set_option pp.all true

theorem floor_example : floor (71/10 : ℝ) = 7 :=
begin
rw ←floor_iff_bounds,
split,
{ norm_num},
-- ⊢ 71 / 10 < ↑7 + 1
-- norm_num, -- seems to hang
suffices : (71 : ℝ) / 10 < 7 + 1,
simpa using this,
-- have  : (71 : ℝ) / 10 < 7 + 1 := by norm_num1,
exact by norm_num,
-- ⊢ 71 / 10 < 7 + 1
-- norm_num -- deterministic timeout
-- sorry
end


#### Rob Lewis (Jan 17 2019 at 23:38):

My best guess is that it has something to do with the type class instance cache. But it's bedtime now.

#### Rob Lewis (Jan 18 2019 at 10:19):

This localizes to the same place as https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/norm_num . If you add some tracing around norm_num.lean:162 you see what's going on: the guard is failing because e2 and e2' have different has_one instances. I'm still not 100% sure why norm_num creates different instances in different circumstances, but I guess it's some kind of a cache issue.

#### Rob Lewis (Jan 18 2019 at 10:21):

One solution: guarding for structural equality is maybe too strong there, but checking that they unify is too weak. We really want to check that the numeral structures match exactly, and the type class instances unify.

#### Rob Lewis (Jan 18 2019 at 10:22):

@Mario Carneiro what do you think?

#### Mario Carneiro (Jan 18 2019 at 10:30):

I see that norm_num is replacing one instance with another, but I don't see how that makes the later stage fail

#### Mario Carneiro (Jan 18 2019 at 10:31):

even if the bottom up simp decides to replace the instance, normalizing the lt should still work

#### Rob Lewis (Jan 18 2019 at 10:39):

norm_num1 should kill the second goal. But it fails at that guard call, because the output of C++ norm_num uses a different has_one instance than the one that (I think) came from the elaborator. It made some progress though, which simp then reverts, so it loops.

#### Mario Carneiro (Jan 18 2019 at 10:40):

doesn't the guard just make sure that something has changed before changing it? It should be harmless

#### Mario Carneiro (Jan 18 2019 at 10:41):

oh, different guard

#### Mario Carneiro (Jan 18 2019 at 10:41):

that guard is just an assert, it can be removed if it's causing trouble

#### Rob Lewis (Jan 18 2019 at 10:41):

The guard makes sure that the output of C++ norm_num is what Lean norm_num was expecting.

#### Mario Carneiro (Jan 18 2019 at 10:42):

I guess it could be defeq instead

#### Rob Lewis (Jan 18 2019 at 10:43):

defeq doesn't really make sense here. The point of the guard is to catch mistakes, I guess. If you check for defeq and there is a mistake, you could force the kernel to normalize numerals.

#### Rob Lewis (Jan 18 2019 at 10:43):

Removing the guard completely seems better than that.

#### Mario Carneiro (Jan 18 2019 at 10:44):

is there an option in is_def_eq for don't try too hard?

#### Rob Lewis (Jan 18 2019 at 10:44):

But then "bugs" like this one are harder to notice. I could imagine this slowing down norm_num noticeably in some cases, instead of failing, but that's harder for Kevin to notice/point out here.

#### Mario Carneiro (Jan 18 2019 at 10:44):

I'm not sure what approx does, but md := reducible should help

#### Kevin Buzzard (Jan 18 2019 at 10:45):

By the way -- thanks @Bryan Gin-ge Chen for the exact by workaround! I've heard of by exact but never this way round. This works great in my use case.

#### Rob Lewis (Jan 18 2019 at 10:46):

approx has something to do with the higher order unification strategy, I think? Not sure. Are the relevant type class defs reducible?

eh, I guess not

#### Mario Carneiro (Jan 18 2019 at 10:47):

I think is_def_eq should be okay as long as they are actually defeq

#### Mario Carneiro (Jan 18 2019 at 10:47):

if they aren't it will start unfolding numerals but that's still impossible to my knowledge

#### Rob Lewis (Jan 18 2019 at 10:47):

Heh. If they're actually defeq we don't need the check at all.

#### Mario Carneiro (Jan 18 2019 at 10:48):

maybe you are right - failing would be great if it made norm_num fail, but this is deep in an inner function and failure has a particular meaning

#### Mario Carneiro (Jan 18 2019 at 10:49):

it just causes these funny loops instead

#### Rob Lewis (Jan 18 2019 at 10:55):

Yeah. A "structurally equal numeral, up to type classes" test would work here, and could maybe be useful elsewhere. The instances will be unified somewhere regardless (if we want this example to succeed).

#### Rob Lewis (Jan 18 2019 at 10:56):

Again, the alternative is just removing the guard, which also doesn't seem so bad.

#### Mario Carneiro (Jan 18 2019 at 10:56):

I think n1.to_nat = n2.to_nat should work for that

#### Rob Lewis (Jan 18 2019 at 10:57):

The two "bugs" that it's identified are only kind of bugs.

Last updated: May 12 2021 at 08:14 UTC