Simplify - missing elements in a list

Stream: new members

[Mark Fischer]

I'm stuck on a proof where I can think of a laborious way to prove it, but I'm not sure how to do it concisely (if that's even possible)

inductive Foo | a | b | c
  deriving DecidableEq, Fintype

example: ∀a : List Foo, a.length = 2 → ∃ y, y ∉ a := by
  intro l _
  match l with
  | [e₁, e₂] =>
    cases e₁ <;> cases e₂
    repeat ( first
      | use .a; decide
      | use .b; decide
      | use .c; decide )

Looking through Mathlib, it seems like Combinatorics.Pigeonhole might be related, though I can't directly see how.

My feeling is that I should be able to exploit the relationship between (@Finset.univ Foo).card and a.length somehow. Such that I don't need to brute force the proof.

[Matt Diamond]

one strategy you could try: use by_contra! and work from the hypothesis that the list contains every member of the type

[Matt Diamond]

use this false hypothesis to "prove" that the list, when converted to a finset, is equal to Finset.univ, and then show that the cardinality of the finset doesn't match the cardinality of the Fintype

[Matt Diamond]

do you want me to share a proof? not sure if this is something you wanted to figure out yourself

[Kyle Miller]

Here's a bit of a simplification:

example: ∀a : List Foo, a.length = 2 → ∃ y, y ∉ a := by
  intro l _
  match l with
  | [e₁, e₂] =>
    revert e₁ e₂
    decide

[Matt Diamond]

@Kyle Miller that's giving me an error in the Lean web editor... is there a specific import that it requires?

[Kyle Miller]

It seems to work so long as deriving Fintype works.

import Mathlib.Tactic.DeriveFintype

inductive Foo | a | b | c
  deriving DecidableEq, Fintype

def foo : ∀a : List Foo, a.length = 2 → ∃ y, y ∉ a := by
  intro l _
  match l with
  | [e₁, e₂] =>
    revert e₁ e₂
    decide

[Matt Diamond]

here's something I put together using the strategy I described above:

import Mathlib.Data.Fintype.Card

variable {α : Type*} [Fintype α] [DecidableEq α]

example : ∀ a : List α, a.length < Fintype.card α → ∃ y, y ∉ a := by
  intros a ha
  by_contra! h
  have a_eq_univ : a.toFinset = Finset.univ := by simp [Finset.eq_univ_iff_forall, h]
  have a_card_le : a.toFinset.card ≤ a.length := List.toFinset_card_le a
  rw [a_eq_univ, Finset.card_univ] at a_card_le
  exact ha.not_le a_card_le

[Mark Fischer]

@Matt Diamond Ah, that works well! I didn't think of that approach at all because by_contra is classical, though for my purposes I don't think I actually need this to be constructive. I managed a very similar proof to yours based on the strategy you described :)

I'm thinking a constructive approach might be to do something like recursively keep record of the set of elements that are not in the head of the list, proving at each step that the set of elements aren't empty. Which will leave me with exactly the non-empty set not found in the list.

[Mark Fischer]

Pattern matching on Arrays works differently than on Lists, so the following doesn't compile

import Mathlib

inductive Foo | a | b | c
  deriving DecidableEq, Fintype

example: ∀a : Array Foo, a.size = 2 → ∃ y, y ∉ a := by
  intro l _
  match l with
  | #[e₁, e₂] =>
    revert e₁ e₂
    decide

[Kyle Miller]

It looks like you can pattern match deeper into the list that theoretically backs the Array.

example: ∀a : Array Foo, a.size = 2 → ∃ y, y ∉ a := by
  intro l _
  match l with
  | ⟨[e₁, e₂]⟩ =>
    revert e₁ e₂
    decide

(Theoretical because this only is used in proofs -- at runtime there's no such List.)

[Mark Fischer]

So, here's an almost proof that may work constructively once complete:

I need to dig around in mathlib and/or figure how how to prove:

1. setList[0] ∈ setList - elements of a list are in the list
2. b.erase head ⊆ b - erasing an element from a set give you a subset
3. head ∉ b.erase head - elements are not in sets they've been erased from
4. After erasing an element, the new set's cardinality smaller by 0 or 1

I think @Matt Diamond 's idea makes for a much nicer proof, but this one's been informative nonetheless.

import Mathlib

variable {α : Type*}
  [DecidableEq α] [LE α] [@DecidableRel α LE.le]
  [IsTrans α LE.le] [IsAntisymm α LE.le] [IsTotal α LE.le]

def missing (a : List α) (b : Finset α) (h : a.length < b.card): ∃y, y ∈ b ∧ y ∉ a := by
  match a with
  | [] =>
    let setList := b.sort LE.le
    have h₁ : setList.length = b.card := Finset.length_sort LE.le
    have h₂ : 0 < setList.length := Nat.lt_of_lt_of_eq h (id h₁.symm)
    let e := setList[0]
    use e
    constructor
    . have h₃ : e ∈ setList ↔ e ∈ b := Finset.mem_sort LE.le
      apply h₃.mp
      have h₄ : setList[0] ∈ setList := by sorry
      assumption
    . apply List.not_mem_nil
  | head :: tail =>

    have newSet := b.erase head
    have newSubSet : newSet ⊆ b := sorry
    have newHeadless : head ∉ newSet := sorry

    have newCard :
      (newSet.card = b.card) ∨
      (newSet.card + 1 = b.card) := sorry

    have ⟨e, ⟨eis,ent⟩⟩ := missing tail newSet (by
      simp only [List.length_cons] at h
      cases newCard <;> linarith)

    simp only [List.mem_cons]

    use e
    constructor
    . exact newSubSet eis

    . intro ht
      cases ht with
      | inl eh =>
        rw [eh] at eis
        contradiction
      | inr et => contradiction

[Matt Diamond]

1. is List.get_mem _ _ _
2. is Finset.erase_subset _ _ (but you have to change have newSet to let newSet, as have doesn't preserve the value of the variable, only the type)

[Mark Fischer]

Matt Diamond said:

change have newSet to let newSet, as have doesn't preserve the value of the variable, only the type

I've done this to myself more often than I care to admit. Good catch, and thanks for the tips :)

[Matt Diamond]

no problem!

3. is Finset.not_mem_erase _ _, if you're still looking

[Mark Fischer]

So far, the only way I've managed to get an element of a Finset is through sort. Which is fine, but only works on types with a relation that support DecidableRel, IsTrans, IsAntisymm, and IsTotal

My guess is that taking an element of a non empty finset is strange because which element you get isn't well defined. But so long as I don't depend on it being any particular element, shouldn't that be fine?

[Matt Diamond]

if you're only using the element in the service of proving some proposition, then you could just destructure s.Nonempty to get a random element

[Matt Diamond]

btw I noticed you wrote missing as a def even though the return type is a Prop... that seems a bit weird to me

[Mark Fischer]

:), if there's any benefit to this version of the proof, it's that you can have the data, otherwise by_contra! seems like a much cleaner solution

[Matt Diamond]

well that's the thing... if you've returned it as an Exists, then I don't believe you can have the data... I don't think you can computably extract data from an Exists even if you proved it without choice

[Ruben Van de Velde]

That's correct. You could use a sigma type instead

[Mark Fischer]

Ah, right. A dependent pair in Type 0+ can have data, but in Prop it cannot.

[Matt Diamond]

But so long as I don't depend on it being any particular element, shouldn't that be fine?

if your goal is to write a function that returns a random value from the finset that isn't in the list, then unfortunately I don't think you can do that computably even if you don't care which value it is... if you're returning data from a function, its value must be concretely determined

[Matt Diamond]

it's kinda like wavefunction collapse in a way... if you're able to access the value, then it can't be indeterminate

[Mark Fischer]

Couldn't it be concretely determined without it being clear exactly how? Determined, but not in a way the system will let you prove anything about - that's how I'd imagine it. Behind the scenes it's just the first element of a non-empty list, that determined by some previous computation, but the information is lost (on purpose).

Probably that leads to some bad things in the corner cases I'm not considering.

[Mark Fischer]

4.

have newCard :
  (newSet.card = b.card) ∨
  (newSet.card + 1 = b.card) := if h: head ∈ b
    then by right; exact Finset.card_erase_add_one h
    else by left; simp [h]

That's a good feeling, thanks for you help @Matt Diamond :)

[Matt Diamond]

No problem!

[Matt Diamond]

@Treq was thinking about this a little more and just wanted to note that you can have a simple computable solution if you write a function that simply returns all of the missing elements... the only non-computable part is picking a random one out of the finset:

import Mathlib.Tactic.DeriveFintype
import Mathlib.Data.Finset.Sort

inductive Foo | a | b | c | d | e | f | g
  deriving Repr, DecidableEq, Fintype

open Foo

def missing (l : List Foo) (hl : l.length < Fintype.card Foo)
  : Σ' s : Finset Foo, s.Nonempty ∧ ∀ x ∈ s, x ∉ l := ⟨
  Finset.univ \ l.toFinset,
  ⟨
    sorry,
    by simp
  ⟩
⟩

#eval (missing [a, b, b, d, f] (by decide)).1

[Mark Fischer]

That's the way to do it! Man. Of course

[Mark Fischer]

I filled in the missing proof, because why not.

def missing (l : List Foo) (hl : l.length < Fintype.card Foo)
  : Σ' s : Finset Foo, s.Nonempty ∧ ∀ x ∈ s, x ∉ l :=

  let univ : Finset Foo := Finset.univ
  let lSet := l.toFinset
  let dSet := univ \ lSet

  have dSet_ne : dSet.Nonempty := by
    have cd : Fintype.card Foo = univ.card := by decide
    have h₁ : lSet ⊆ univ := Finset.subset_univ lSet
    have h₂ : lSet.card ≤ l.length := List.toFinset_card_le l
    have h₃ : dSet.card = univ.card - lSet.card := Finset.card_sdiff h₁
    have h₄ : lSet.card < univ.card := by linarith
    have h₅ : 1 ≤ univ.card - lSet.card := Nat.le_sub_of_add_le' h₄
    rw [← h₃] at h₅
    exact Finset.card_pos.mp h₅

  ⟨dSet, ⟨dSet_ne, by simp⟩⟩

[Kyle Miller]

One comment: for Type/Prop pairs, usually you see Subtype rather than PSigma, so {s : Finset Foo // s.Nonempty ∧ ∀ x ∈ s, x ∉ l} rather than Σ' s : Finset Foo, s.Nonempty ∧ ∀ x ∈ s, x ∉ l. Ultimately the type is equivalent, but there's more about Subtype than PSigma in the library.

[Mark Fischer]

Can I extract an element from a Singleton?
Seems like it should be possible as which element you get is then fully determined.

def getFromSingleton (s : Finset α) (h : s.card = 1) : {a // a ∈ s} := sorry

[Matt Diamond]

This is a bit weird but in theory it should work:

import Mathlib.Data.Finset.Card

def getFromSingleton (s : Finset α) (h : s.card = 1) : {a // a ∈ s} :=
let exists_unique : ∃! (a : α), a ∈ s ∧ True := by
  rw [Finset.card_eq_one, Finset.singleton_iff_unique_mem] at h
  simp [h]
⟨Finset.choose _ s exists_unique, Finset.choose_mem _ _ _⟩

[Matt Diamond]

would be great if there was a more straightforward way that I'm unaware of

[Kevin Buzzard]

Guessing the name docs#Finset.card_pos

[Kevin Buzzard]

That would make it more low-level

[Mark Fischer]

I made a version that I think expresses that it's always possible to get the data out of a singleton.

def getFromSingleton {s : Finset α} (h : ∃e, s = {e}) : {e // s = {e}} :=
  have unique : ∃! e, e ∈ s :=  (Finset.singleton_iff_unique_mem s).mp h
  have unique' : ∃! e, e ∈ s ∧ True := by simp only [and_true, unique]
  let e₁ := Finset.choose (λ_↦True) s unique'
  have e₁_in : e₁ ∈ s := Finset.choose_mem (λ_↦True) s unique'

  have h : s = {e₁} :=
    Finset.eq_singleton_iff_unique_mem.mpr ⟨e₁_in, λe₂ e₂_in ↦
      let ⟨_, _, f⟩ := unique
      by rw [f e₁ e₁_in, f e₂ e₂_in]
    ⟩
  ⟨e₁, h⟩

Really, though this could be something like (∃e, s = {e}) ↔ {e // s = {e}}, but I'm not sure the type that best carries that idea. A Bijection?

[Matt Diamond]

@Treq The proper way to do this, I think, is to prove that the goal is a Subsingleton type and then use Quotient.recOnSubsingleton to extract the value. Here's my attempt:

import Mathlib.Data.Multiset.Basic
import Mathlib.Data.Finset.Card

open Multiset

variable {α : Type*}

instance subsingleton_of_card_one (m : Multiset α) (hm : card m = 1) : Subsingleton {a // a ∈ m} :=
by
  constructor
  rintro ⟨a, ha⟩ ⟨b, hb⟩
  rw [card_eq_one] at hm
  cases' hm with x hx
  rw [hx, mem_singleton] at ha hb
  simp [ha, hb]

def Multiset.getFromSingleton (m : Multiset α) : card m = 1 → {a // a ∈ m} :=
Quotient.recOnSubsingleton m
  (h := fun l => by infer_instance)
  (fun l card_eq_one =>
    let not_empty : l ≠ [] := by
      apply List.ne_nil_of_length_pos
      rw [quot_mk_to_coe, coe_card] at card_eq_one
      simp [card_eq_one]
    ⟨l.head not_empty, List.head_mem _⟩
  )

def Finset.getFromSingleton (s : Finset α) (hs : s.card = 1) : {a // a ∈ s} :=
Multiset.getFromSingleton s.val hs

#eval Finset.getFromSingleton {123} (by decide)

[Matt Diamond]

re: (∃e, s = {e}) ↔ {e // s = {e}}, that doesn't really work because the left side is a Prop and the right side is a Type

[Matt Diamond]

you could do (∃e, s = {e}) ↔ Nonempty {e // s = {e}} but I have a feeling that doesn't express what you're trying to express

[Mark Fischer]

Maybe (∃e, s = {e}) ↔ Inhabited {e // s = {e}} is closer, as you can get the default value from an inhabited type? But I was thinking something like an isomorphism/bijection seems to act like a biconditional (At least superficially?), but allows for different types.

[Yaël Dillies]

Iff for Sorts is docs#Equiv

[Mark Fischer]

I suspect this proof would have been easier using Subsingleton. I think an equivalence between not empty Subsingleton types is trivial (It kinda like P Q ⊢ P ↔ Q). I'm still working my way through to understanding what Quotient.recOnSubsingleton is doing though.

def singletonEquiv {s : Finset α} : (∃e, s = {e}) ≃ {e // s = {e}} :=
  let toFun : (∃e, s = {e}) → {e // s = {e}} := getFromSingleton
  let invFun : {e // s = {e}} → (∃e, s = {e}) := λe ↦ ⟨e.val, e.property⟩

  let left_inv : Function.LeftInverse invFun toFun := congrFun rfl
  let right_inv : Function.RightInverse invFun toFun := by
    intro ⟨e₁, e₁_sng⟩
    have ep : ∃e, s = {e} := ⟨e₁, e₁_sng⟩
    have ⟨e₂, e₂_sng⟩ := toFun ep
    have e₁_in : e₁ ∈ s := by simp_all
    have e₂_in : e₂ ∈ s := by simp_all
    have ⟨_, _, f⟩ : ∃! e, e ∈ s :=  (Finset.singleton_iff_unique_mem s).mp ep
    have e_eq : e₁ = e₂ := by rw [f e₁ e₁_in, f e₂ e₂_in]
    exact SetCoe.ext (id e_eq.symm)

  ⟨toFun, invFun, left_inv, right_inv⟩