repr for finsets

Stream: general

[Pablo Le Hénaff]

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

[Pablo Le Hénaff]

I would like to run some algorithms with eval

[Sean Leather]

One option: use finset.sort.

[Pablo Le Hénaff]

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

[Sean Leather]

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

[Simon Hudon]

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]

yes total order is an assumption. good idea

[Sean Leather]

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]

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]

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]

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

[Sean Leather]

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

[Pablo Le Hénaff]

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

[Simon Hudon]

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

[Sean Leather]

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

[Pablo Le Hénaff]

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]

Interesting, I didn't think of injectivity

[Simon Hudon]

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

[Simon Hudon]

But injectivity might be a good law to have in has_to_repr

[Mario Carneiro]

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]

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

[Chris Hughes]

or subtype.has_repr

[Kevin Buzzard]

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

[Chris Hughes]

Why were you goofing around with pnat?

[Kevin Buzzard]

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.