Zulip Chat Archive

Stream: general

Topic: equality of multisets


view this post on Zulip Johan Commelin (Jun 19 2019 at 10:13):

How is one supposed to prove

lemma test {σ : Type*} (s t : σ) : ([s, s, t] : multiset σ) = [t, s, s] := _

view this post on Zulip Mario Carneiro (Jun 19 2019 at 10:14):

by simp [insert_comm]?

view this post on Zulip Mario Carneiro (Jun 19 2019 at 10:16):

alternatively, apply quotient.sound and then use perm.swap and friends

view this post on Zulip Johan Commelin (Jun 19 2019 at 10:19):

Aha... ok.

view this post on Zulip Johan Commelin (Jun 19 2019 at 10:19):

I didn't know about insert_comm.

view this post on Zulip Mario Carneiro (Jun 19 2019 at 10:19):

I actually just guessed it existed

view this post on Zulip Mario Carneiro (Jun 19 2019 at 10:20):

thanks yesterday mario

view this post on Zulip Kevin Buzzard (Jun 19 2019 at 10:26):

When I look at files like multiset.lean I honestly think "golly, I'm glad I didn't take up Lean about 18 months earlier than I did"

view this post on Zulip Kevin Buzzard (Jun 19 2019 at 10:27):

Those files are so huge, and so complete, and because everything is a quotient the proofs are often extremely cryptic and would be very hard indeed for a beginner to generate.

view this post on Zulip Kenny Lau (Jun 19 2019 at 10:28):

maybe we should write a tactic that will sort the elements

view this post on Zulip Mario Carneiro (Jun 19 2019 at 10:34):

there is a function for that, multiset.sort

view this post on Zulip Mario Carneiro (Jun 19 2019 at 10:35):

as for sorting it syntactically, that's what simp does


Last updated: May 09 2021 at 18:17 UTC