All lists with a maximum length and elements of a finset

Stream: Is there code for X?

[Johannes Tantow]

Hi,
I am looking for a function of the form def generateAll (X : Finset A) (n : ℕ) : Finset (List A) that fulfills the following property

theorem generateAll_def (X: Finset A) (l': List A) (n : ℕ):
    l' ∈ generateAllX n ↔ l'.length ≤ n ∧ ∀ x ∈ l', x ∈ X :=  sorry

It would also be fine if X is a list instead of a finite set. Do we have anything like that?

[Eric Wieser]

is this almost docs#Finset.powersetCard ?

[Johannes Tantow]

Kind of. The powerset can be larger, which I can filter out,but the lists are allowed to contain duplicates in my case.

[Eric Wieser]

How's this, via docs#Vector.fintype ?

import Mathlib

def generateAll (X : Finset A) (n : ℕ) : Finset (List A) :=
  (Finset.univ : Finset (List.Vector X n)).map <|
    .trans (.subtype _) ⟨_, List.map_injective_iff.2 Subtype.val_injective⟩

[Eric Wieser]

Ah, I guess that's only the ones of fixed length

[Eric Wieser]

But you could take the disjiUnion over all i <= n

[Johannes Tantow]

The normal union should suffice as well for this as A is decidable. I'll build Mathlib and test that. Thanks

[Eric Wieser]

disjiUnion will be much faster to execute and kernel reduce

[Eric Wieser]

But also it might be easier to implement this from scratch rather than via my suggestion above!

[Johannes Tantow]

I don't really want to execute this and only need this to show decidability. disjUnion wants me to prove disjointness

[Johannes Tantow]

I tried this before from scratch by recursion, but didn't find a good way to combine the elements of the lists with the finset of lists with length le m-1.

[Eric Wieser]

Either you prove the disjointness now, or you'll find you probably need it later

[Eric Wieser]

Johannes Tantow said:

I tried this before from scratch by recursion, but didn't find a good way to combine the elements of the lists with the finset of lists with length le m-1.

Probably you should start with lists:

import Mathlib

def generateAll (l : List A) (n : ℕ) : List (List A) :=
  match n with
  | 0 => [[]]
  | n + 1 =>
    let last := generateAll l n
    [] :: l.flatMap fun x => last.map fun ls => x :: ls

#eval generateAll [1, 2, 3] 2```
and then show that:
* permuting the input permutes the output (to get to multisets)
* if the input has no duplicate, then nor does the output (to get to finsets)

[Johannes Tantow]

I can also work with lists directly, but I thought the other form might be more general

[Johannes Tantow]

so that it would exist already somewhere

[Eric Wieser]

Unfortunately my code above doesn't actually work, it creates duplicates! fixed

[Eric Wieser]

But usually the pattern with these combinatorial constructions is to build them for Lists, then Multiset, then Finset

[Eric Wieser]

Since often it actually is useful to have the "less general" version

[Eric Wieser]

eg docs#List.sublists, docs#Multiset.powerset, docs#Finset.powerset

[Eric Wieser]

For instance, with my definition above, you could prove that if l is sorted then generateAll l 2 is sorted lexicographically

[Johannes Tantow]

Thanks, I managed to prove my result now.

[Kevin Buzzard]

Johannes Tantow said:

The normal union should suffice as well for this as A is decidable. I'll build Mathlib and test that. Thanks

Just to check -- you didn't mean "I'll spend at least an hour building mathlib on my computer because I don't know about lake exe cache get which downloads compiled binaries" do you?

[Johannes Tantow]

I theoretically know that, but didn't think of that in the moment and just pressed reload files and started the process