## Stream: general

### Topic: repr for finsets

#### Pablo Le Hénaff (Jun 20 2018 at 14:15):

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

#### Pablo Le Hénaff (Jun 20 2018 at 14:15):

I would like to run some algorithms with eval

#### Sean Leather (Jun 20 2018 at 14:17):

One option: use finset.sort.

#### Pablo Le Hénaff (Jun 20 2018 at 14:18):

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

#### Sean Leather (Jun 20 2018 at 14:19):

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

#### 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

#### Pablo Le Hénaff (Jun 20 2018 at 14:22):

yes total order is an assumption. good idea

#### 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.

#### 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?

#### 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]


#### 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.

#### Sean Leather (Jun 20 2018 at 14:31):

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

#### Pablo Le Hénaff (Jun 20 2018 at 14:32):

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

#### 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


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


#### Sean Leather (Jun 20 2018 at 14:38):

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

#### 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

#### Simon Hudon (Jun 20 2018 at 14:39):

Interesting, I didn't think of injectivity

#### Simon Hudon (Jun 20 2018 at 14:39):

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

#### Simon Hudon (Jun 20 2018 at 14:40):

But injectivity might be a good law to have in has_to_repr

#### 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

#### Kevin Buzzard (Jun 20 2018 at 20:30):

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

#### Chris Hughes (Jun 20 2018 at 20:42):

or subtype.has_repr

#### 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).

#### Chris Hughes (Jun 20 2018 at 20:45):

Why were you goofing around with pnat?

#### 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