bug in norm_num handling of ge?

Stream: general

[Heather Macbeth]

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]

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]

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]

Grateful for any help here ...

[Heather Macbeth]

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]

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

[Heather Macbeth]

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

[Eric Wieser]

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

[Heather Macbeth]

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

Yes, I guess I must mean that

[Eric Wieser]

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]

Good question! Yup, these both time out:

import data.rat.order

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

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

[Eric Wieser]

Ouch

[Heather Macbeth]

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]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

or abstract the numerals first

[Heather Macbeth]

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]

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]

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

[Mario Carneiro]

#14425

[Heather Macbeth]

Thanks Mario!