Zulip Chat Archive

Stream: maths

Topic: list from a finset


view this post on Zulip 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?

view this post on Zulip Kenny Lau (Apr 13 2018 at 12:38):

but finset is a subquotient of list

view this post on Zulip Kenny Lau (Apr 13 2018 at 12:38):

and quotients can't be reversed

view this post on Zulip Sean Leather (Apr 13 2018 at 12:39):

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

view this post on Zulip 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 _)

view this post on Zulip Sean Leather (Apr 13 2018 at 12:48):

Ah, fold?

view this post on Zulip Simon Hudon (Apr 13 2018 at 12:50):

Why do you not want to sort it?

view this post on Zulip Sean Leather (Apr 13 2018 at 12:50):

Because I don't need a particular order.

view this post on Zulip Kenny Lau (Apr 13 2018 at 12:50):

then it's uncomputable

view this post on Zulip 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?

view this post on Zulip Sean Leather (Apr 13 2018 at 12:53):

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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Kenny Lau (Apr 13 2018 at 13:10):

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

view this post on Zulip 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?

view this post on Zulip Kenny Lau (Apr 13 2018 at 13:11):

no, that's what quotient is

view this post on Zulip Kenny Lau (Apr 13 2018 at 13:11):

it needs to work for any permutation

view this post on Zulip Kenny Lau (Apr 13 2018 at 13:12):

your functions need to be well-defined

view this post on Zulip 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

view this post on Zulip Chris Hughes (Apr 13 2018 at 13:13):

quotient.out works, but that's noncomputable

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Apr 13 2018 at 13:14):

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

view this post on Zulip Kenny Lau (Apr 13 2018 at 13:14):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 13 2018 at 13:48):

Sean -- you want your function to be computable?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Sean Leather (Apr 19 2018 at 06:37):

How so?

view this post on Zulip Mario Carneiro (Apr 19 2018 at 06:37):

It makes the code path a bit more obvious

view this post on Zulip Mario Carneiro (Apr 19 2018 at 06:38):

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

view this post on Zulip Mario Carneiro (Apr 19 2018 at 06:38):

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

view this post on Zulip Sean Leather (Apr 19 2018 at 06:38):

What type signature would you want?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Apr 19 2018 at 11:32):

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

view this post on Zulip Mario Carneiro (Apr 19 2018 at 11:32):

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

view this post on Zulip 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