norm_num weirdness

Stream: maths

[Kevin Buzzard]

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)

[Bryan Gin-ge Chen]

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.

[Bryan Gin-ge Chen]

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

[Rob Lewis]

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]

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

[Rob Lewis]

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

[Rob Lewis]

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]

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]

@Mario Carneiro what do you think?

[Mario Carneiro]

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]

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

[Rob Lewis]

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]

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

[Mario Carneiro]

oh, different guard

[Mario Carneiro]

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

[Rob Lewis]

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

[Mario Carneiro]

I guess it could be defeq instead

[Rob Lewis]

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]

Removing the guard completely seems better than that.

[Mario Carneiro]

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

[Rob Lewis]

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]

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

[Kevin Buzzard]

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]

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

[Mario Carneiro]

eh, I guess not

[Mario Carneiro]

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

[Mario Carneiro]

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

[Rob Lewis]

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

[Mario Carneiro]

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]

it just causes these funny loops instead

[Rob Lewis]

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]

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

[Mario Carneiro]

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

[Rob Lewis]

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