norm_num can't solve 1 ≤ 2

Stream: general

[Gabriel Ebner]

Just found out something interesting:

import set_theory.game
import tactic.norm_num

example : 1 ≤ 3 := -- both norm_num fail
calc 1 ≤ 2 : by norm_num
   ... ≤ 3 : by norm_num

[Eric Wieser]

Even sorry fails:

import set_theory.pgame

-- ok
example : 1 ≤ 3 :=
calc 1 ≤ 2 : sorry
   ... ≤ 3 : sorry

-- fails
example : 1 ≤ 3 :=
calc 1 ≤ 2 : by sorry
   ... ≤ 3 : sorry

-- fails
example : 1 ≤ 3 :=
calc 1 ≤ 2 : sorry
   ... ≤ 3 : by sorry

[Yakov Pechersky]

Because lt on it is some weird data that doesn't have [trans] afair

[Gabriel Ebner]

1 ≤ 3 is a completely benign statement about natural numbers

[Yakov Pechersky]

Oh I see what you mean

[Eric Wieser]

Unfortunately local attribute [-trans] isn't legal, otherwise we could use it to track down which trans lemma is firing

[Gabriel Ebner]

I'll spare you the effort of searching: src#game.le_trans

[Eric Wieser]

The problem persists with just pgame imported though, so I guess src#pgame.le_trans is also a culprit?

[Gabriel Ebner]

src#pgame.le_trans

[Gabriel Ebner]

Also: src#pgame.lt_of_le_of_lt and src#pgame.lt_of_lt_of_le

[Bryan Gin-ge Chen]

I might be being dense: is the issue with those lemmas or in calc?

[Rob Lewis]

I'm guessing calc chooses lemmas keyed to the head symbol? So those lemmas overwrite the generic trans lemma for has_le.le?

[Yury G. Kudryashov]

The issue is that calc can't handle multiple @[trans] lemmas per binrel

[Yury G. Kudryashov]

I saw it with subset on set vs finset.

[Gabriel Ebner]

It's not just calc either, also the transitivity tactic fails after importing pgame.

[Mario Carneiro]

Is pgame not a preorder? This @[trans] lemma should not exist, it should be using the lemma on preorders

[Bryan Gin-ge Chen]

Sadly, no: https://github.com/leanprover-community/mathlib/blob/d405c5e9099b4b2e23a475dd76e418918d08b666/src/set_theory/pgame.lean#L40

[Mario Carneiro]

It looks like lt is quite badly behaved too. I wonder if it would work to have a preorder instance and a has_lt instance of higher priority

[Mario Carneiro]

Or a local notation `<` := weird_lt so that lt_of_lt_of_le and such work

[Yury G. Kudryashov]

Can we have lt_game and notation instead of has_lt?

[Eric Wieser]

This has come up again here: https://github.com/leanprover-community/mathlib/pull/7440/files#r627673550