Zulip Chat Archive

Stream: maths

Topic: norm_num weirdness


view this post on Zulip 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,
  int.lt_add_one_iff, le_antisymm_iff, and.comm]

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

view this post on Zulip 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,
  int.lt_add_one_iff, le_antisymm_iff, and.comm]

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.

view this post on Zulip 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,
  int.lt_add_one_iff, le_antisymm_iff, and.comm]

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

view this post on Zulip 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.

view this post on Zulip 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,
  int.lt_add_one_iff, le_antisymm_iff, and.comm]

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Rob Lewis (Jan 18 2019 at 10:22):

@Mario Carneiro what do you think?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jan 18 2019 at 10:41):

oh, different guard

view this post on Zulip Mario Carneiro (Jan 18 2019 at 10:41):

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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Jan 18 2019 at 10:42):

I guess it could be defeq instead

view this post on Zulip 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.

view this post on Zulip Rob Lewis (Jan 18 2019 at 10:43):

Removing the guard completely seems better than that.

view this post on Zulip Mario Carneiro (Jan 18 2019 at 10:44):

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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Jan 18 2019 at 10:44):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Jan 18 2019 at 10:46):

eh, I guess not

view this post on Zulip Mario Carneiro (Jan 18 2019 at 10:47):

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

view this post on Zulip 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

view this post on Zulip Rob Lewis (Jan 18 2019 at 10:47):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jan 18 2019 at 10:49):

it just causes these funny loops instead

view this post on Zulip 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).

view this post on Zulip Rob Lewis (Jan 18 2019 at 10:56):

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

view this post on Zulip Mario Carneiro (Jan 18 2019 at 10:56):

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

view this post on Zulip 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