Zulip Chat Archive

Stream: general

Topic: failed to synthesize type class instance for is_antisymm

FR (Mar 07 2022 at 14:13):

https://paste.debian.net/1233286/ I have an instance of type is_antisymm (list α) is_prefix. But lean want to find an instance of type is_antisymm (list α) (λ {l l' : list α}, l' <+: l). How should I deal with it?

upd: Sorry it looks like I made a reply, not a new topic. I'm new to here and not familiar with zulip. Sorry for that.

Eric Wieser (Mar 07 2022 at 14:21):

exact antisymm hl' hl works fine, you have your arguments backwards

Johan Commelin (Mar 07 2022 at 14:22):

@FR In this case, it's probably fine to reuse the old topic

Johan Commelin (Mar 07 2022 at 14:22):

At some point we run out of topic titles :grinning:

FR (Mar 07 2022 at 14:30):

image.png My lean gives me an error. Does this mean that the version of my lean is too old?

Eric Wieser (Mar 07 2022 at 14:34):

No, it means you didn't read my comment carefully enough! You're not using the replacement code I suggested.

FR (Mar 07 2022 at 14:38):

Oh, I get it. Thanks for your help!

Eric Wieser (Mar 07 2022 at 14:41):

That is_antisymm instance is probably reasonable to PR to mathlib, if you're interested

Eric Wieser (Mar 07 2022 at 14:42):

I would guess you can make a stronger is_partial_order instance

Eric Wieser (Mar 07 2022 at 14:46):

Yep:

instance : is_partial_order (list α) (<+:) :=
{ refl := λ _, prefix_rfl,
  trans := λ _ _ _, is_prefix.trans,
  antisymm := λ l₁ l₂ h₁ h₂,
    eq_of_prefix_of_length_eq h₁ $ (is_prefix.length_le h₁).antisymm (is_prefix.length_le h₂) }

FR (Mar 08 2022 at 01:51):

All right. My GitHub username is negiizhao. I'm ready to make a PR.

Bryan Gin-ge Chen (Mar 08 2022 at 03:50):

FR said:

All right. My GitHub username is negiizhao. I'm ready to make a PR.

Invite sent! https://github.com/leanprover-community/mathlib/invitations

Last updated: Dec 20 2023 at 11:08 UTC