## 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: Aug 03 2023 at 10:10 UTC