element of list of lists that is minimal subset

Stream: Is there code for X?

[Paige Thomas]

I'm wondering if there is an existing proof of this, or a more generic lemma that would specialize to this?

example
  {α : Type}
  (xss : List (List α))
  (xs : List α)
  (h1 : xs ∈ xss) :
  ∃ (ys : List α), ys ∈ xss ∧ ys ⊆ xs ∧ ∀ (zs : List α), (zs ∈ xss ∧ zs ⊆ ys) → zs = ys :=
  sorry

[Kim Morrison]

Isn't it false because of reordering? e.g. take xss := [[0,1], [1,0]].

[Kim Morrison]

(Nerd-snipe: now make by plausible show you this counterexample.)

[Paige Thomas]

Sorry, I'm not familiar with plausible.

[Paige Thomas]

Hmm, I think your right though.

[Paige Thomas]

Maybe

example
  {α : Type}
  (xss : List (List α))
  (xs : List α)
  (h1 : xs ∈ xss) :
  ∃ (ys : List α), ys ∈ xss ∧ ys ⊆ xs ∧ ∀ (zs : List α), (zs ∈ xss ∧ zs ⊆ ys) → ys ⊆ zs :=
  sorry

?

[Kevin Buzzard]

Did you try plausible?

[Paige Thomas]

I got an error message with

import Mathlib

example
  {α : Type}
  (xss : List (List α))
  (xs : List α)
  (h1 : xs ∈ xss) :
  ∃ (ys : List α), ys ∈ xss ∧ ys ⊆ xs ∧ ∀ (zs : List α), (zs ∈ xss ∧ zs ⊆ ys) → zs = ys :=
  by plausible

[Paige Thomas]

Failed to create a `testable` instance for `∀ {α : Type} (xss : List (List α)),
  ∀ xs ∈ xss, ∃ ys ∈ xss, ys ⊆ xs ∧ ∀ (zs : List α), zs ∈ xss ∧ zs ⊆ ys → zs = ys`.

[Kevin Buzzard]

What happens if you change alpha to Nat? Or maybe it's beyond the scope of the tactic

[Paige Thomas]

I seem to get the same error.

[Paige Thomas]

I'm basically trying to show that if there is some element xs of xss, then there is also an element ys of xss that is the minimal subset of xs.

[Paige Thomas]

Even if ys is xs itself.

[Kim Morrison]

It's not beyond the scope of the tactic, someone just needs to write some Decidable instances, probably for "for all elements of some list such that" type quantifiers.

[Bhavik Mehta]

That decidable instance exists in core, it's docs#List.decidableBAll, but it's not firing because of the ∧ near the end. Uncurrying that, or just calling simp first, plausible still fails, but it tries this time:

import Mathlib

example
    {α : Type}
    (xss : List (List α))
    (xs : List α)
    (h1 : xs ∈ xss) :
    ∃ (ys : List α), ys ∈ xss ∧ ys ⊆ xs ∧ ∀ (zs : List α), (zs ∈ xss ∧ zs ⊆ ys) → zs = ys := by
  simp
  plausible -- Gave up after failing to generate values that fulfill the preconditions 87 times.

example
    {α : Type}
    (xss : List (List α))
    (xs : List α)
    (h1 : xs ∈ xss) :
    ∃ (ys : List α), ys ∈ xss ∧ ys ⊆ xs ∧ ∀ (zs : List α), zs ∈ xss → zs ⊆ ys → zs = ys := by
  plausible -- Gave up after failing to generate values that fulfill the preconditions 86 times.

[Bhavik Mehta]

Kim Morrison said:

(Nerd-snipe: now make by plausible show you this counterexample.)

Try as I might, I can't make it find a counterexample:

example (xss : List (List Nat)) :
    ∀ xs ∈ xss, ∃ (ys : List Nat), ys ∈ xss ∧ ys ⊆ xs ∧ ∀ (zs : List Nat), zs ∈ xss → zs ⊆ ys → zs = ys := by
  plausible

and turning on the trace options

import Mathlib

set_option trace.plausible.discarded true

example (xss : List (List Nat)) :
    ∀ xs ∈ xss, ∃ (ys : List Nat), ys ∈ xss ∧ ys ⊆ xs ∧ ∀ (zs : List Nat), zs ∈ xss → zs ⊆ ys → zs = ys := by
  plausible (config := {numInst := 4})

shows the things it tried. (I had to decrease the number of attempts otherwise it takes too long to show anything, and the live editor disconnects itself because of the time). This looks like the Sampleable instance for lists is doing something suboptimal, at least for this problem.

[Paige Thomas]

I think maybe this is a formalization of the idea I am trying to prove:

  {α : Type}
  (xss : List (List α))
  (xs : List α)
  (h1 : xs ∈ xss) :
  ∃ (ys : List α), ys ∈ xss ∧ ys ⊆ xs ∧
    ∀ (zs : List α), (zs ∈ xss ∧ zs ⊆ xs) → ys ⊆ zs :=
  by
  sorry

[Aaron Liu]

That particular version is false:

import Mathlib

example : ¬∀
  {α : Type}
  (xss : List (List α))
  (xs : List α)
  (h1 : xs ∈ xss),
  ∃ (ys : List α), ys ∈ xss ∧ ys ⊆ xs ∧
    ∀ (zs : List α), (zs ∈ xss ∧ zs ⊆ xs) → ys ⊆ zs :=
  by
  intro h
  simp_rw [and_imp] at h
  specialize @h (Fin 3) [[1, 2, 3], [0, 1], [0, 2]] [1, 2, 3] List.mem_cons_self
  revert h
  decide

[Paige Thomas]

argh

[Paige Thomas]

example
  {α : Type}
  (xss : List (List α))
  (xs : List α)
  (h1 : xs ∈ xss) :
  ∃ (ys : List α), ys ∈ xss ∧ ys ⊆ xs ∧
    ∀ (zs : List α), (zs ∈ xss ∧ zs ⊆ ys) → ys ⊆ zs :=
  by
  sorry

?

[Aaron Liu]

import Mathlib

example
  {α : Type}
  (xss : List (List α))
  (xs : List α)
  (h1 : xs ∈ xss) :
  ∃ (ys : List α), ys ∈ xss ∧ ys ⊆ xs ∧
    ∀ (zs : List α), (zs ∈ xss ∧ zs ⊆ ys) → ys ⊆ zs :=
  by
  classical
  obtain ⟨ys, hys, hall⟩ := (xss.finite_toSet.inter_of_left {ys | ys ⊆ xs}).exists_minimal_wrt List.toFinset _  ⟨xs, h1, fun _ => id⟩
  use ys, hys.left, hys.right
  intro zs hzs x hx
  specialize hall zs ⟨hzs.left, hzs.right.trans hys.right⟩ fun x hx => List.mem_toFinset.mpr (hzs.right (List.mem_toFinset.mp hx))
  rwa [← List.mem_toFinset, ← hall, List.mem_toFinset]

[Paige Thomas]

Thank you!