How to prove that ⊂ list mapping results in ⊂ btwn lists

Stream: new members

[aron]

I can't figure out how to prove this. That if you have list and newList where newList = list.map f and you know that f removes some specific item uv from the gather-projection of each item, and you know that there is at least one item whose projection contains uv, you know that the collected projection of newList will be a strict subset of that of list.

just can't figure out how to prove this. I end up tying myself into knots every time I try.

import Mathlib

theorem mapped_list_is_ssubset
  {list newList : List α} {gather : α → Finset β}
  [Union (Finset β)]

  (h : newList = list.map f)

  {uv : β}
  (hin : uv ∈ gather item → gather (f item) ⊂ gather item)
  (hnin : uv ∉ gather item → gather (f item) = gather item)

  (f_removes_uv : uv ∉ gather (f item)) -- this is probably inferrable from the above two but just listing it for clarity

  (hexists : ∃ a ∈ list, uv ∈ gather a)

  : newList.foldr (fun a s ↦ gather a ∪ s) ∅ ⊂ list.foldr (fun a s ↦ gather a ∪ s) ∅ := by sorry

[aron]

I feel like there is probably also a far more elegant statement of this theorem but any attempts at such that I've tried have gotten me even further away from being able to prove it :frown:

[Anthony Wang]

Your theorem as stated right now is false. If list is the empty list, then you don't get a strict subset.

[aron]

That's why I've got (hexists : ∃ a ∈ list, uv ∈ gather a) so the list can't be empty

[Anthony Wang]

Oh sorry, I missed that line.

[aron]

No worries, there's a lot going on here :sweat_smile: it's not a very elegant theorem statement atm

[Matt Diamond]

seems like you're using .foldr to do a flat-map kind of operation... maybe it would be simpler to express it that way?

[aron]

yeah the foldr has been a pain to work with, but how do I go from a list of items to a single combined set of βs in one go with a flat-map? wouldn't a flat-map still just give you a list?

[Matt Diamond]

what if you converted to a finset first?

[Matt Diamond]

is there a reason you need to use a list to begin with?

[Matt Diamond]

perhaps the list / finset conversion is adding to the complexity

[aron]

hmm. well the original data is in a list. but no, there's no reason to map in the list and then gather the βs in a set as opposed to convert to a set of αs first and then flatmap directly to βs if that's what you're saying

[Matt Diamond]

yeah, like maybe it would be easier to convert first and then flat map

docs#Finset.sup_map might be useful

[Anthony Wang]

@aron How about something like this for the theorem statement, using Finset.biUnion instead of a foldr?

import Mathlib

theorem mapped_list_is_ssubset [DecidableEq β] {A B : Finset α} {gather : α → Finset β}
    [Union (Finset β)]
    (h : B = A.map f)
    {uv : β}
    (hin : ∀ item, uv ∈ gather item → gather (f item) ⊂ gather item)
    (hnin : ∀ item, uv ∉ gather item → gather (f item) = gather item)
    (hexists : ∃ a ∈ A, uv ∈ gather a)
    : B.biUnion gather ⊂ A.biUnion gather := by

[Matt Diamond]

also I would get rid of [Union (Finset β)] (I know that was in the original post) and replace it with [DecidableEq β]

[Matt Diamond]

in fact I wonder if that was half the trouble... you're using an arbitrary definition of Union!

[aron]

Is biUnion the Finset version of a flatmap? I was looking for Finset.flatMap or Finset.bind but couldn't find anything – but the biUnion docs say it used to be called bind so that might be it?

[aron]

Matt Diamond said:

in fact I wonder if that was half the trouble... you're using an arbitrary definition of Union!

oh... I hope that wasn't it :melting_face:

[Matt Diamond]

Finset.bind exists since Finset has a Monad instance

[aron]

but I get this:

Invalid field `bind`: The environment does not contain `Finset.bind`
  newList
has type
  Finset α

[aron]

the biUnion doc comment says:

`Finset.biUnion s t` is the union of `t a` over `a ∈ s`.

(This was formerly `bind` due to the monad structure on types with `DecidableEq`.)

[Matt Diamond]

sorry, I misspoke... I meant that you can call bind on a Finset

[Matt Diamond]

and you can use >>=

[Matt Diamond]

though the implementation is just Finset.sup as docs#Finset.bind_def shows

[Matt Diamond]

that's why I was suggesting docs#Finset.sup_map ... the goal being to prove that newList >>= gather is really just list >>= gather ∘ f

[Anthony Wang]

Here's a concise proof of the theorem statement with biUnion:

theorem mapped_list_is_ssubset [DecidableEq β] {list newlist : Finset α} {gather : α → Finset β}
    (h : newlist = list.map f)
    {uv : β}
    (hin : ∀ item, uv ∈ gather item → gather (f item) ⊂ gather item)
    (hnin : ∀ item, uv ∉ gather item → gather (f item) = gather item)
    (f_removes_uv : ∀ item, uv ∉ gather (f item))
    (hexists : ∃ a ∈ list, uv ∈ gather a)
    : newlist.biUnion gather ⊂ list.biUnion gather :=
  Finset.ssubset_iff_of_subset (by grind) |>.mpr (by use uv; grind)

[aron]

oh wow what. thanks @Anthony Wang!

I doubt I'd have thought of that myself in a million years :sweat_smile: I'm very unfamiliar with the Finset library and I've found apply? and grind both pretty useless at pushing me forward

[aron]

ah but one problem – f seems to have type α ↪ α. It's not a regular function α → α

[aron]

looks like the difference is that f also needs to be injective

/-- `α ↪ β` is a bundled injective function. -/
structure Embedding (α : Sort*) (β : Sort*) where
  /-- An embedding as a function. Use coercion instead. -/
  toFun : α → β
  /-- An embedding is an injective function. Use `Function.Embedding.injective` instead. -/
  inj' : Injective toFun

From the definition of Finset.map:

/-- When `f` is an embedding of `α` in `β` and `s` is a finset in `α`, then `s.map f` is the image
finset in `β`. The embedding condition guarantees that there are no duplicates in the image. -/
def map (f : α ↪ β) (s : Finset α) : Finset β :=
  ⟨s.1.map f, s.2.map f.2⟩

[Anthony Wang]

Oh, you need Finset.image instead of Finset.map. The same proof works.

import Mathlib

theorem mapped_list_is_ssubset [DecidableEq α] [DecidableEq β] {list newlist : Finset α} {gather : α → Finset β}
    (h : newlist = list.image f)
    {uv : β}
    (hin : ∀ item, uv ∈ gather item → gather (f item) ⊂ gather item)
    (hnin : ∀ item, uv ∉ gather item → gather (f item) = gather item)
    (f_removes_uv : ∀ item, uv ∉ gather (f item))
    (hexists : ∃ a ∈ list, uv ∈ gather a)
    : newlist.biUnion gather ⊂ list.biUnion gather :=
  Finset.ssubset_iff_of_subset (by grind) |>.mpr (by use uv; grind)

[aron]

ah ok nice! I was gonna say that I understand why Finset.map wants it to be injective, but for my use case I don't care if f a = f b even if a ≠ b. I'd just have multiple αs resulting in the same β, which is fine for me

[aron]

Follow-up question: how do I make this work with prop versions of the gather function? I.e. instead of it having type α → Finset β it has type α → Finset β → Prop representing a relation of input to output instead of an actual function?

For reference I initially had an inductive representing the operation of "gather all βs from a list of αs like:

inductive ListGathering {α β} [DecidableEq β] (gather : α → Finset β → Prop) : (list : List α) → (combined : Finset β) → Prop where
  | nil :
    ListGathering gather [] ∅

  | cons :
    gather head headItems →
    ListGathering gather tail tailItems →
    combined = headItems ∪ tailItems →
    ListGathering gather (head :: tail) combined

but after the above conversation I think it has to be something more like:

def ListGathering' {α β} [DecidableEq α] [DecidableEq β] (gather : α → Finset β) : (list : List α) → (combined : Finset β) → Prop :=
  fun list combined ↦
    let finset := Finset.mk (Multiset.ofList list).dedup (List.nodup_dedup list)
    combined = finset.biUnion gather

which in addition to me not knowing how to adapt it to a prop-valued version of gather is also just far less elegant

[aron]

Ok I managed to figure it out!

The version of ListGathering that uses the function version of gather : α → Finset β is:

def ListGathering' {α β} [DecidableEq α] [DecidableEq β] (gather : α → Finset β)
  : (list : List α) → (combined : Finset β) → Prop :=
  fun list combined ↦
    combined = list.toFinset.biUnion gather

For the relation version of gather : α → Finset β → Prop I first need to introduce a helper prop ListMappingRel:

/-- Relation that maps between an input and output list given a relation prop -/
inductive ListMappingRel (p : α → β → Prop) : (list : List α) → (newList : List β) → Prop where
  | nil : ListMappingRel p [] []
  | cons :
    p head newHead →
    ListMappingRel p tail newTail →
    ListMappingRel p (head :: tail) (newHead :: newTail)

We can then define ListGathering'Rel like:

def ListGathering'Rel {α β} [DecidableEq α] [DecidableEq β]
  (gather_rel : α → Finset β → Prop)
  : (list : List α) → (combined : Finset β) → Prop :=
  fun list combined ↦
    ∀ listOfIds,
      ListMappingRel gather_rel list listOfIds →
      combined = ((listOfIds : Multiset (Finset β)) |>.map Finset.val |>.join |>.toFinset)

[aron]

Here's the combined #mwe containing 4 theorems for each version of the prop relating the presence or absence of a certain β in the original list with the presence or absence of that β in the combined Finset:

Full #mwe

import Mathlib

/-- Relation that maps between an input and output list given a relation prop -/
inductive ListMappingRel (p : α → β → Prop) : (list : List α) → (newList : List β) → Prop where
  | nil : ListMappingRel p [] []
  | cons :
    p head newHead →
    ListMappingRel p tail newTail →
    ListMappingRel p (head :: tail) (newHead :: newTail)





@[simp] def ListGathering' {α β} [DecidableEq α] [DecidableEq β] (gather : α → Finset β)
  : (list : List α) → (combined : Finset β) → Prop :=
  fun list combined ↦
    combined = list.toFinset.biUnion gather



@[grind] theorem ListGathering'.if_in_list_then_in_combined {gather : α → Finset β}
  [DecidableEq α] [DecidableEq β]
  (h : ListGathering' gather list combined)
  : ∀ item ∈ list, ∀ i ∈ gather item, i ∈ combined := by
  intro item inlist i initem
  simp at h
  subst_eqs
  simp
  exists item

@[grind] theorem ListGathering'.if_nin_list_then_nin_combined {gather : α → Finset β}
  [DecidableEq α] [DecidableEq β]
  (h : ListGathering' gather list combined)
  : ∀ i, (∀ item ∈ list, i ∉ gather item) → i ∉ combined := by
  intro i prem
  simp at h
  subst_eqs
  simp
  exact prem



@[grind] theorem ListGathering'.if_in_combined_then_in_list {gather : α → Finset β}
  [DecidableEq α] [DecidableEq β]
  (h : ListGathering' gather list combined)
  : ∀ i ∈ combined, ∃ item ∈ list, i ∈ gather item := by
  intro i incomb
  simp at h
  subst_eqs
  simp at incomb
  have ⟨item,prf⟩ := incomb
  exists item

@[grind] theorem ListGathering'.if_nin_combined_then_nin_list {gather : α → Finset β}
  [DecidableEq α] [DecidableEq β]
  (h : ListGathering' gather list combined)
  : ∀ i ∉ combined, ∀ item ∈ list, i ∉ gather item := by
  intro i incomb
  simp at h
  subst_eqs
  simp at incomb
  exact incomb






@[simp] def ListGathering'Rel {α β} [DecidableEq α] [DecidableEq β]
  (gather_rel : α → Finset β → Prop)
  : (list : List α) → (combined : Finset β) → Prop :=
  fun list combined ↦
    ∀ listOfIds,
      ListMappingRel gather_rel list listOfIds →
      combined = ((listOfIds : Multiset (Finset β)) |>.map Finset.val |>.join |>.toFinset)



@[grind] theorem ListGathering'Rel.if_in_list_then_in_combined {gather : α → Finset β → Prop}
  [DecidableEq α] [DecidableEq β]
  (h : ListGathering'Rel gather list combined)
  : ListMappingRel gather list listOfSets →
    ∀ itemSet ∈ listOfSets, ∀ i ∈ itemSet, i ∈ combined := by
  intro listrel itemSet inlist i initem
  simp at h
  replace h := h _ listrel
  subst_eqs
  simp
  exists itemSet

@[grind] theorem ListGathering'Rel.if_nin_list_then_nin_combined {gather : α → Finset β → Prop}
  [DecidableEq α] [DecidableEq β]
  (h : ListGathering'Rel gather list combined)
  : ListMappingRel gather list listOfSets →
    ∀ i, (∀ itemSet ∈ listOfSets, i ∉ itemSet) → i ∉ combined := by
  intro listrel i prem
  simp at h
  replace h := h _ listrel
  subst_eqs
  simp
  exact prem



@[grind] theorem ListGathering'Rel.if_in_combined_then_in_list {gather : α → Finset β → Prop}
  [DecidableEq α] [DecidableEq β]
  (h : ListGathering'Rel gather list combined)
  : ListMappingRel gather list listOfSets →
    ∀ i ∈ combined, ∃ itemSet ∈ listOfSets, i ∈ itemSet := by
  intro listrel i incomb
  simp at h
  replace h := h _ listrel
  subst_eqs
  simp at incomb
  have ⟨item,prf⟩ := incomb
  exists item

@[grind] theorem ListGathering'Rel.if_nin_combined_then_nin_list {gather : α → Finset β → Prop}
  [DecidableEq α] [DecidableEq β]
  (h : ListGathering'Rel gather list combined)
  : ListMappingRel gather list listOfSets →
    ∀ i ∉ combined, ∀ itemSet ∈ listOfSets, i ∉ itemSet := by
  intro listrel i incomb
  simp at h
  replace h := h _ listrel
  subst_eqs
  simp at incomb
  exact incomb

[aron]

My next step is to adapt this mapped_list_is_ssubset theorem for use with my ListGathering'Rel prop :sparkles:

#new members > How to prove that ⊂ list mapping results in ⊂ btwn lists @ 💬