Stream: general

Topic: bug in norm_num handling of ge?

Heather Macbeth (May 26 2022 at 22:26):

I discovered some odd behaviour of norm_num on numeric inequalities, seemingly related to the ge/le defeq since it works for the le phrasing but not the ge phrasing:

import tactic.norm_num

-- (deterministic) timeout
example : (63:ℚ) ≥ 5 := by norm_num1

-- works
example : (5:ℚ) ≤ 63 := by norm_num1


Heather Macbeth (May 26 2022 at 22:27):

Drilling down a bit more, it seems like this already arises in the bit1_le_bit1 lemma which gets used in the norm_num proof:

import tactic.norm_num

-- (deterministic) timeout
example : bit1 (31:ℚ) ≥ bit1 2 := norm_num.le_bit1_bit1 2 31 sorry

-- (deterministic) timeout
example : bit1 (31:ℚ) ≥ bit1 2 := (@bit1_le_bit1 _ _ 2 31).mpr sorry


Heather Macbeth (May 26 2022 at 22:29):

And the issue only seems to arise for fairly large numbers! This works:

example : bit1 (11:ℚ) ≥ bit1 2 := (@bit1_le_bit1 _ _ 2 11).mpr sorry


Heather Macbeth (May 26 2022 at 22:29):

Grateful for any help here ...

Heather Macbeth (May 26 2022 at 23:09):

One further observation: annoyingly, I can't even trick Lean here by telling it the le fact I want norm_num to find. This still fails:

import tactic.norm_num

-- (deterministic) timeout
example : (63:ℚ) ≥ 5 :=
begin
have : (5:ℚ) ≤ 63 := by norm_num1,
exact this,
end


Yaël Dillies (May 26 2022 at 23:10):

Let me ask the obvious question: How did you get a ≥ in your goal in the first place?

Heather Macbeth (May 26 2022 at 23:11):

I'm writing a tactic for undergraduate use (and not just Yaël-level undergraduates!).

Eric Wieser (May 26 2022 at 23:19):

My guess would be that it starts unfolding the rats before the ge

Heather Macbeth (May 26 2022 at 23:22):

@Eric Wieser By "it" do you mean the typechecker? Because in the example

import tactic.norm_num

-- (deterministic) timeout
example : bit1 (31:ℚ) ≥ bit1 2 := (@bit1_le_bit1 _ _ 2 31).mpr sorry


what's happening is that it's checking (@bit1_le_bit1 _ _ 2 31).mpr sorry is a term of type bit1 (31:ℚ) ≥ bit1 2, right?

Eric Wieser (May 26 2022 at 23:23):

Yes, I guess I must mean that

Eric Wieser (May 26 2022 at 23:25):

Do you get the same timeout if you prove the two statements (le vs ge) are the same (as either an iff or eq) with refl?

Heather Macbeth (May 26 2022 at 23:30):

Good question! Yup, these both time out:

import data.rat.order

example : ((63:ℚ) ≥ 5) = ((5:ℚ) ≤ 63) := rfl

example (h : (5:ℚ) ≤ 63) : (63:ℚ) ≥ 5 := h


Ouch

Heather Macbeth (May 27 2022 at 21:20):

I'll ping @Mario Carneiro here, any idea why

import data.rat.order

example : ((63:ℚ) ≥ 5) = ((5:ℚ) ≤ 63) := rfl

example (h : (5:ℚ) ≤ 63) : (63:ℚ) ≥ 5 := h


would time out?

Mario Carneiro (May 27 2022 at 21:21):

I think Eric explained it already: lean sometimes thinks it would be better to unfold the numerals than the relation. I remember having similar issues with (12:int) <= 100 kind of things

Mario Carneiro (May 27 2022 at 21:22):

norm_num has to be super careful with these kinds of hypotheses to avoid doing anything that could trigger a definitional reduction

Mario Carneiro (May 27 2022 at 21:22):

in this case the solution would be to rw ge instead of using rfl

Mario Carneiro (May 27 2022 at 21:23):

or abstract the numerals first

Heather Macbeth (May 27 2022 at 21:24):

If norm_num is hitting this timeout (see top of thread), does that mean that there's a bug in norm_num, because it is triggering a definitional reduction that it ought not to trigger?

Mario Carneiro (May 27 2022 at 23:27):

Ah, yes. I swear, I wrote a few things like this thinking "surely, unfolding this definition should be fine without applying a lemma...?" and every time I was wrong

Mario Carneiro (May 27 2022 at 23:29):

the moral of the story is: never trust defeq, it will choose an adversarial reduction strategy when possible

#14425

Heather Macbeth (May 27 2022 at 23:48):

Thanks Mario!

Last updated: Dec 20 2023 at 11:08 UTC