Zulip Chat Archive

Stream: general

Topic: repr for finsets


view this post on Zulip Pablo Le Hénaff (Jun 20 2018 at 14:15):

Is there a way to define a has_repr instance for finsets ?

view this post on Zulip Pablo Le Hénaff (Jun 20 2018 at 14:15):

I would like to run some algorithms with eval

view this post on Zulip Sean Leather (Jun 20 2018 at 14:17):

One option: use finset.sort.

view this post on Zulip Pablo Le Hénaff (Jun 20 2018 at 14:18):

oh ! that's cool, i never noticed it. Thanks

view this post on Zulip Sean Leather (Jun 20 2018 at 14:19):

No problem. If you come up with something useful, please share it with us.

view this post on Zulip Simon Hudon (Jun 20 2018 at 14:21):

do you need a total order to use it? You could probably get rid of that constraint if you convert each element to string and then sorting the result

view this post on Zulip Pablo Le Hénaff (Jun 20 2018 at 14:22):

yes total order is an assumption. good idea

view this post on Zulip Sean Leather (Jun 20 2018 at 14:22):

By “get rid of,” you mean push the total order off onto the string, right? That's not a bad idea for all of the constraints.

view this post on Zulip Simon Hudon (Jun 20 2018 at 14:24):

Yes, we need a total order on strings but this is readily available. Basically, what I meant was "weaken the assumptions to make it more generally usable". What are the other constraints?

view this post on Zulip Sean Leather (Jun 20 2018 at 14:25):

Right, that's what I thought. So finset.image to string and finset.sort the result.

variables (r : α → α → Prop) [decidable_rel r] [is_trans α r] [is_antisymm α r] [is_total α r]

view this post on Zulip Simon Hudon (Jun 20 2018 at 14:27):

Not quite. In this situation, α is now string so r is now the linear order on strings.

view this post on Zulip Sean Leather (Jun 20 2018 at 14:31):

I don't understand. Something like finset.sort (<) ∘ finset.image to_string doesn't work?

view this post on Zulip Pablo Le Hénaff (Jun 20 2018 at 14:32):

there are missing instances for string, they shouldn't be too hard to write

view this post on Zulip Simon Hudon (Jun 20 2018 at 14:34):

Yes it does. But because we're using (<) on string, we have weaker assumptions about α and we can discharge the assumptions about string once and for all. That means that to_repr has type:

def to_repr {α} [has_to_repr α] : finset α -> string

instead of

def to_repr {α} [has_to_repr α] [decidable_linear_order α] : finset α -> string

view this post on Zulip Sean Leather (Jun 20 2018 at 14:38):

That of course depends on how to_string : α → string is defined for your α.

view this post on Zulip Pablo Le Hénaff (Jun 20 2018 at 14:38):

You also need to make sure that has_repr.to_repr for \alpha is injective (and maybe use map instead of image)
but that's not so interesting

view this post on Zulip Simon Hudon (Jun 20 2018 at 14:39):

Interesting, I didn't think of injectivity

view this post on Zulip Simon Hudon (Jun 20 2018 at 14:39):

You could get around it by first converting to a multiset I think

view this post on Zulip Simon Hudon (Jun 20 2018 at 14:40):

But injectivity might be a good law to have in has_to_repr

view this post on Zulip Mario Carneiro (Jun 20 2018 at 20:01):

It's a good point that we can sort strings here, I hadn't thought of that. I'll add a has_repr instance for multiset and finset then

view this post on Zulip Kevin Buzzard (Jun 20 2018 at 20:30):

While you're at it, you could add one for pnat (nat.repr \circ subtype.val)

view this post on Zulip Chris Hughes (Jun 20 2018 at 20:42):

or subtype.has_repr

view this post on Zulip Kevin Buzzard (Jun 20 2018 at 20:44):

I also made an instance of has_to_string pnat (when I was goofing around with pnat a few weeks ago).

view this post on Zulip Chris Hughes (Jun 20 2018 at 20:45):

Why were you goofing around with pnat?

view this post on Zulip Kevin Buzzard (Jun 20 2018 at 20:51):

I was trying to get on top of exactly what one should do when defining a new structure in Lean. If I had to define pnat I would start by writing down the definition as a subtype, and then I realised that I would not really know what to do next. So I read pnat.lean quite carefully to try and get a feeling for it. I then read real.lean for the same sort of reason.


Last updated: May 13 2021 at 04:21 UTC