Zulip Chat Archive

Stream: Is there code for X?

Topic: remove lists that have subsets in list of lists

Paige Thomas (Jun 22 2025 at 01:51):

I'm trying to find or define a function that does the following:
Given a list of lists ll, for every pair of lists l1 and l2 at distinct indexes in ll, if l1 is a subset of l2 then remove l2.
Some examples:

[[1], [1]] -> [[1]]
[[1], [2]] -> [[1], [2]]
[[2], [1]] -> [[2], [1]]
[[1], [1, 2]] -> [[1]]
[[1, 2], [1]] -> [[1]]
[[1], [1, 2], [1, 2, 3]] -> [[1]]
[[1], [2], [1, 2], [1, 2, 3], [2, 3, 4]] -> [[1], [2]]

I tried List.pwFilter (fun (l1 l2 : List Nat) => ¬ (l1 ⊆ l2)) as an example, but it doesn't seem to match the output I am looking for.
I'm only using Nat as an example type, it should be arbitrary.

Aaron Liu (Jun 22 2025 at 02:01):

I wonder if there's a faster way to do this

import Mathlib

def filterMin {α : Type*} [DecidableEq α] (l : List (List α)) : List (List α) :=
  l.filter fun x => ∀ y ∈ l, y ⊆ x → x ⊆ y

Aaron Liu (Jun 22 2025 at 02:01):

I don't think this one accounts for duplicates though

Paige Thomas (Jun 22 2025 at 02:05):

Yeah, it appears to keep duplicates.

Paige Thomas (Jun 22 2025 at 02:31):

Hmm, well, this appears to work:

def filterMinAux
  {α : Type}
  [DecidableEq α]
  (acc : List (List α)) :
  List (List α) → List (List α)
  | [] => acc
  | hd :: tl =>
    if ∃ (l : List α), l ∈ (acc ++ tl) ∧ l ⊆ hd
    then filterMinAux acc tl
    else filterMinAux (acc ++ [hd]) tl

def filterMin
  {α : Type}
  [DecidableEq α]
  (ll : List (List α)) :=
  filterMinAux [] ll

I'd be interested in if there is if a more elegant or efficient way though.

Paige Thomas (Jun 22 2025 at 02:38):

I guess you could also add a dedup to the one you have.

Aaron Liu (Jun 22 2025 at 02:39):

import Mathlib

def filterMin {α : Type*} [DecidableEq α] (l : List (List α)) : List (List α) :=
  (l.filter fun x => ∀ y ∈ l, y ⊆ x → x ⊆ y).pwFilter fun x y => ¬(x ⊆ y ∧ y ⊆ x)

Paige Thomas (Jun 22 2025 at 02:48):

Thank you!

Kenny Lau (Jun 22 2025 at 11:13):

@Paige Thomas I'm not convinced your function is even well-defined

Kenny Lau (Jun 22 2025 at 11:13):

for example, if I follow the literal interpretation of your specification, then [[1], [1]] should return []!

Kenny Lau (Jun 22 2025 at 11:20):

import Mathlib

def foo (ll : List (List ℕ)) : List (List ℕ) :=
  let indices := (List.finRange ll.length).filter fun i ↦
    ¬∃ j : Fin ll.length, j ≠ i ∧ ll.get j ⊆ ll.get i
  indices.map ll.get

#eval foo [[1], [1]] -- [[1]]
#eval foo [[1], [2]] -- [[1], [2]]
#eval foo [[2], [1]] -- [[2], [1]]
#eval foo [[1], [1, 2]] -- [[1]]
#eval foo [[1, 2], [1]] -- [[1]]
#eval foo [[1], [1, 2], [1, 2, 3]] -- [[1]]
#eval foo [[1], [2], [1, 2], [1, 2, 3], [2, 3, 4]] -- [[1], [2]]