Zulip Chat Archive

Stream: general

Topic: norm_num can't solve 1 ≤ 2


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Yakov Pechersky (Feb 11 2021 at 15:50):

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

view this post on Zulip Gabriel Ebner (Feb 11 2021 at 15:50):

1 ≤ 3 is a completely benign statement about natural numbers

view this post on Zulip Yakov Pechersky (Feb 11 2021 at 15:51):

Oh I see what you mean

view this post on Zulip 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

view this post on Zulip Gabriel Ebner (Feb 11 2021 at 15:54):

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

view this post on Zulip 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?

view this post on Zulip Gabriel Ebner (Feb 11 2021 at 15:55):

src#pgame.le_trans

view this post on Zulip Gabriel Ebner (Feb 11 2021 at 15:56):

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

view this post on Zulip Bryan Gin-ge Chen (Feb 11 2021 at 16:11):

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

view this post on Zulip 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?

view this post on Zulip Yury G. Kudryashov (Feb 11 2021 at 16:12):

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

view this post on Zulip Yury G. Kudryashov (Feb 11 2021 at 16:13):

I saw it with subset on set vs finset.

view this post on Zulip Gabriel Ebner (Feb 11 2021 at 16:26):

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

view this post on Zulip 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

view this post on Zulip Bryan Gin-ge Chen (Feb 11 2021 at 16:36):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 11 2021 at 16:39):

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

view this post on Zulip 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