list from a finset

Stream: maths

[Sean Leather]

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]

but finset is a subquotient of list

[Kenny Lau]

and quotients can't be reversed

[Sean Leather]

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

[Sean Leather]

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]

Ah, fold?

[Simon Hudon]

Why do you not want to sort it?

[Sean Leather]

Because I don't need a particular order.

[Kenny Lau]

then it's uncomputable

[Simon Hudon]

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

[Sean Leather]

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

[Simon Hudon]

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]

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]

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]

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]

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]

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

[Sean Leather]

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

[Kenny Lau]

no, that's what quotient is

[Kenny Lau]

it needs to work for any permutation

[Kenny Lau]

your functions need to be well-defined

[Kenny Lau]

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]

quotient.out works, but that's noncomputable

[Chris Hughes]

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

[Kenny Lau]

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

[Kenny Lau]

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

[Sean Leather]

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

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]

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]

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

[Kevin Buzzard]

Sean -- you want your function to be computable?

[Sean Leather]

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]

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

[Sean Leather]

How so?

[Mario Carneiro]

It makes the code path a bit more obvious

[Mario Carneiro]

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

[Mario Carneiro]

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

[Sean Leather]

What type signature would you want?

[Mario Carneiro]

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]

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]

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]

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]

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]

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]

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

[Mario Carneiro]

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

[Sean Leather]

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