## Stream: general

### Topic: norm_num can't solve 1 ≤ 2

#### Gabriel Ebner (Feb 11 2021 at 15:26):

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 (Feb 11 2021 at 15:43):

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 (Feb 11 2021 at 15:50):

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

#### Gabriel Ebner (Feb 11 2021 at 15:50):

1 ≤ 3 is a completely benign statement about natural numbers

#### Yakov Pechersky (Feb 11 2021 at 15:51):

Oh I see what you mean

#### Eric Wieser (Feb 11 2021 at 15:52):

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

#### Gabriel Ebner (Feb 11 2021 at 15:54):

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

#### Eric Wieser (Feb 11 2021 at 15:54):

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

#### Gabriel Ebner (Feb 11 2021 at 15:55):

src#pgame.le_trans

#### Bryan Gin-ge Chen (Feb 11 2021 at 16:11):

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

#### Rob Lewis (Feb 11 2021 at 16:12):

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 (Feb 11 2021 at 16:12):

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

#### Yury G. Kudryashov (Feb 11 2021 at 16:13):

I saw it with subset on set vs finset.

#### Gabriel Ebner (Feb 11 2021 at 16:26):

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

#### Mario Carneiro (Feb 11 2021 at 16:35):

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

#### Mario Carneiro (Feb 11 2021 at 16:38):

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 (Feb 11 2021 at 16:39):

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

#### Yury G. Kudryashov (Feb 11 2021 at 16:39):

Can we have lt_game and notation instead of has_lt?

Last updated: May 10 2021 at 00:31 UTC