## Stream: maths

### Topic: list from a finset

#### Sean Leather (Apr 13 2018 at 12:37):

Is there a way to get a list from a finset without using finset.sort or writing my own recursive function on finset?

#### Kenny Lau (Apr 13 2018 at 12:38):

but finset is a subquotient of list

#### Kenny Lau (Apr 13 2018 at 12:38):

and quotients can't be reversed

#### Sean Leather (Apr 13 2018 at 12:39):

That's right, so I couldn't use a recursive function anyway.

#### Sean Leather (Apr 13 2018 at 12:43):

Well, I suppose I could follow the sort example:

def finset.sort (s : finset α) : list α := multiset.sort r s.1

def multiset.sort (s : multiset α) : list α :=
quot.lift_on s (merge_sort r) $λ a b h, eq_of_sorted_of_perm tr.trans an.antisymm ((perm_merge_sort _ _).trans$ h.trans (perm_merge_sort _ _).symm)
(sorted_merge_sort r to.total tr.trans _)
(sorted_merge_sort r to.total tr.trans _)


#### Sean Leather (Apr 13 2018 at 12:48):

Ah, fold?

#### Simon Hudon (Apr 13 2018 at 12:50):

Why do you not want to sort it?

#### Sean Leather (Apr 13 2018 at 12:50):

Because I don't need a particular order.

#### Kenny Lau (Apr 13 2018 at 12:50):

then it's uncomputable

#### Simon Hudon (Apr 13 2018 at 12:52):

Right but them being in a particular order can't be harmful, is it? Is it that you care about the performances?

#### Sean Leather (Apr 13 2018 at 12:53):

It requires adding an ordering constraint to the elements that I don't need or want.

#### Simon Hudon (Apr 13 2018 at 12:53):

What you could do is compute on the list before taking it out of the quotient and proving that the result is independent of order

#### Sean Leather (Apr 13 2018 at 12:55):

def multiset.foldr (f : α → β → β) (H : left_commutative f) (b : β) (s : multiset α) : β :=
quot.lift_on s (λ l, foldr f b l) (λ l₁ l₂ p, foldr_eq_of_perm H p b)


#### Kenny Lau (Apr 13 2018 at 12:56):

It requires adding an ordering constraint to the elements that I don't need or want.

otherwise it won't be a well-defined function

#### Simon Hudon (Apr 13 2018 at 13:01):

def multiset.foldr (f : α → β → β) (H : left_commutative f) (b : β) (s : multiset α) : β :=
quot.lift_on s (λ l, foldr f b l) (λ l₁ l₂ p, foldr_eq_of_perm H p b)


Exactly. What are you trying to compute?

#### Sean Leather (Apr 13 2018 at 13:10):

So, finset.fold doesn't work because it requires the append operator to be commutative, which it is not:

def to_list : finset α → list α :=
fold (++) [] (λ a, [a])

⊢ is_commutative (list α) append


#### Kenny Lau (Apr 13 2018 at 13:10):

right, because the function you're trying to define isn't well-defined

#### Sean Leather (Apr 13 2018 at 13:11):

Since finset is a quotient on list permutations, is it not possible to choose an arbitrary permutation?

#### Kenny Lau (Apr 13 2018 at 13:11):

no, that's what quotient is

#### Kenny Lau (Apr 13 2018 at 13:11):

it needs to work for any permutation

#### Kenny Lau (Apr 13 2018 at 13:12):

your functions need to be well-defined

#### Kenny Lau (Apr 13 2018 at 13:13):

if {2,1,3} gives [2,1,3] and {1,2,3} gives [1,2,3], then it isn't a well-defined function

#### Chris Hughes (Apr 13 2018 at 13:13):

quotient.out works, but that's noncomputable

#### Chris Hughes (Apr 13 2018 at 13:13):

quot.unquot also works, but you can't use that in a proof, because it implies false.

#### Kenny Lau (Apr 13 2018 at 13:14):

in fact, if your function did that, then I can prove false

#### Kenny Lau (Apr 13 2018 at 13:14):

because {2,1,3} and {1,2,3} are equal

#### Sean Leather (Apr 13 2018 at 13:17):

@Kenny Lau Right, so your point is that the function has to produce the same permutation for any set, and that's why sorting is necessary.

#### Simon Hudon (Apr 13 2018 at 13:35):

Right. But the other idea is: what are you going to do with that list? If the function that uses the list works the same for all permutation, you don't need to care about sorting the list. You just need to make sure that when you use the list, you produce the same results regardless of order

#### Sean Leather (Apr 13 2018 at 13:35):

In the end, I want a list with certain properties. I thought using a finset to construct it would be simpler (since that function is easier), but it appears that I should just construct the list directly. I'm going to try using list.to_finset to simplify the property testing during construction in an auxiliary function and then extract the list-specific properties from the finset properties in a wrapper.

#### Simon Hudon (Apr 13 2018 at 13:36):

Instead of going inside the quot to extract a list, go inside to do more of your computations

#### Kevin Buzzard (Apr 13 2018 at 13:48):

Sean -- you want your function to be computable?

#### Sean Leather (Apr 19 2018 at 06:30):

To catch up on this thread, I was trying to figure out how to use

def fresh_finset (s₁ : finset α) : ∀ n, Σ' (s₂ : finset α), card s₂ = n ∧ s₂ ∩ s₁ = ∅


in the definition of

def fresh_list (s : finset α) : ∀ n, Σ' (l : list α), l.length = n ∧ l.nodup ∧ l.to_finset ∩ s = ∅


but, as has been pointed out to me, this is not possible without adding an additional constraint on α. In the end, I wrote fresh_list from scratch. It wasn't as difficult as I thought, and it shares a proof structure with fresh_finset.

See the source for the definitions.

Kevin: Yes, I want a computable definition.

#### Mario Carneiro (Apr 19 2018 at 06:36):

I agree that it is best to write the list definition directly in this case. I think it would be better to have the fresh list separate from the properties though

How so?

#### Mario Carneiro (Apr 19 2018 at 06:37):

It makes the code path a bit more obvious

#### Mario Carneiro (Apr 19 2018 at 06:38):

I always worry that the match and such will add extra overhead

#### Mario Carneiro (Apr 19 2018 at 06:38):

it's not clear to me whether it is in fact optimized away

#### Sean Leather (Apr 19 2018 at 06:38):

What type signature would you want?

#### Mario Carneiro (Apr 19 2018 at 06:42):

class has_fresh (α : Type*) :=
(fresh : finset α → α)
(fresh_not_mem : ∀ s, fresh s ∉ s)

def fresh_list (s : finset α) : nat → list α
| 0 := []
| (n+1) := let l := fresh_list n in fresh (l.to_finset ∪ s) :: l

theorem fresh_list_length (s : finset α) : ∀ n, (fresh_list s n).length = n

theorem fresh_list_nodup_disjoint (s : finset α) :
∀ n, (fresh_list s n).nodup ∧ (fresh_list s n).to_finset ∩ s = ∅


I conjoin the last two only because I think the proof is by mutual recursion

#### Sean Leather (Apr 19 2018 at 06:46):

Ah, I see what you mean. You're talking about splitting the methods of the class. Yeah, that seems fine, assuming it works.

#### Mario Carneiro (Apr 19 2018 at 06:47):

By the way, it is conceivable that fresh in the typeclass will be difficult to define, since it enforces that the fresh element not depend on the order of the input list

#### Sean Leather (Apr 19 2018 at 07:36):

By the way, it is conceivable that fresh in the typeclass will be difficult to define, since it enforces that the fresh element not depend on the order of the input list

@Mario Carneiro I don't follow. I'm guessing you mean it's difficult to define fresh for instances of has_fresh. But what “input list”? has_fresh only depends on the element of the finset.

You could, of course, define different functions to produce a fresh element from a list or a fresh element from a finset with a required ordering to the element. Nonetheless, it is possible to define a has_fresh instance for nat and other infinite types for which it is possible to find an extreme, and has_fresh does not impose an ordering constraint that is not always needed.

#### Mario Carneiro (Apr 19 2018 at 07:39):

I mean that to implement fresh on a type A, you need to define a function list A -> A, and then lift it to a function finset A -> A, meaning that the original function must map [a, b] and [b, a] to the same fresh value c. Depending on A, that may not be convenient to do, for example if you hash the list or something to generate a disambiguator

#### Sean Leather (Apr 19 2018 at 11:31):

I think it would be better to have the fresh list separate from the properties though

@Mario Carneiro This was a good suggestion. The result is much cleaner now.

I mean that to implement fresh on a type A, you need to define a function list A -> A, and then lift it to a function finset A -> A [...]

This is the part I don't follow. Why does one need to define a function list A -> A? For nat, this isn't necessary. I conjecture that the same is true for other types.

#### Mario Carneiro (Apr 19 2018 at 11:32):

every function on finset is ultimately the lift of a function on list

#### Mario Carneiro (Apr 19 2018 at 11:32):

I assume you used finset.fold or something to define the nat function

#### Sean Leather (Apr 19 2018 at 11:33):

True, but that doesn't mean I have to write the list function itself.

Last updated: May 18 2021 at 07:19 UTC