finset proof

Stream: Is there code for X?

[Patrick Thomas]

I was wondering if anyone might have advice on proving this? I think I might make progress if I can get it to a point where I can use something similar to finset.bUnion_insert?

import data.finset

lemma finset_bUnion_sdiff
  {T : Type} [decidable_eq T]
  (x x' : T)
  (S : finset T)
  (f : T → finset T)
  (h1 : f x = {x'}) :
  (finset.bUnion S f) \ {x'} = (finset.bUnion (S \ {x}) f) \ {x'} :=
begin
  by_cases x ∈ S,
  {
    sorry
  },
  {
    congr, symmetry, exact finset.sdiff_singleton_not_mem_eq_self S h,
  }
end

[Eric Wieser]

Does docs#finset.bUnion_erase exist?

[Stuart Presnell]

Not particularly elegant, but this does the job:

lemma finset_bUnion_sdiff
  {T : Type} [decidable_eq T]
  (x x' : T)
  (S : finset T)
  (f : T → finset T)
  (h1 : f x = {x'}) :
  (finset.bUnion S f) \ {x'} = (finset.bUnion (S \ {x}) f) \ {x'} :=
begin
  by_cases hxS : x ∈ S,
  { ext,
    simp only [finset.mem_sdiff, finset.mem_bUnion, and.congr_left_iff, finset.mem_singleton],
    intros ha,
    split,
  { rintros ⟨i, ⟨hi1, hi2⟩⟩,
    refine ⟨i, ⟨⟨hi1, _⟩, hi2⟩⟩,
    contrapose! ha,
    subst ha,
    exact finset.mem_singleton.1 (h1 ▸ hi2) },
  { rintros ⟨i, ⟨hi1, hi2⟩⟩, exact ⟨i, ⟨hi1.1, hi2⟩⟩ } },
  { congr, symmetry, exact finset.sdiff_singleton_not_mem_eq_self S hxS }
end

[Patrick Thomas]

Thank you!

[Patrick Johnson]

Simpler proof:

import tactic

lemma finset_bUnion_sdiff
  {T : Type} [decidable_eq T]
  (x x' : T)
  (S : finset T)
  (f : T → finset T)
  (h1 : f x = {x'}) :
  (finset.bUnion S f) \ {x'} = (finset.bUnion (S \ {x}) f) \ {x'} :=
begin
  ext y, simp, intro, congr', ext z,
  have : y ∈ f z → z ≠ x := by rintro _ rfl; simp * at *,
  tauto,
end

[Kyle Miller]

Taking care of the nonterminal simp and making it more mathliby:

lemma finset_bUnion_sdiff
  {T : Type} [decidable_eq T]
  (x x' : T)
  (S : finset T)
  (f : T → finset T)
  (h1 : f x = {x'}) :
  (finset.bUnion S f) \ {x'} = (finset.bUnion (S \ {x}) f) \ {x'} :=
begin
  ext y,
  simp only [finset.mem_sdiff, finset.mem_bUnion, exists_prop,
    finset.mem_singleton, and.congr_left_iff],
  intro,
  congr' with z,
  have : y ∈ f z → z ≠ x,
  { rintro h' rfl,
    simpa only [*, finset.mem_singleton] using h', },
  tauto,
end

By the way, congr' takes a with clause for doing ext.

[Kevin Buzzard]

Using a non-terminal simp is supposed to be a code smell, but sometimes it's really handy. I understand how simp only [finset.mem_sdiff, finset.mem_bUnion, exists_prop, finset.mem_singleton, and.congr_left_iff], is easier to maintain, but it's a darn sight uglier :-/ Before squeeze_simp we used to write suffices : [result of simp], by simpa; probably this is often shorter than what we do nowadays, as well as being easier to read.

[Kevin Buzzard]

With that way of doing it, the proof looks like this:

begin
  ext y,
  suffices : y ≠ x' →
    ((∃ (a : T), a ∈ S ∧ y ∈ f a) ↔ ∃ (a : T), (a ∈ S ∧ a ≠ x) ∧ y ∈ f a),
  { simpa },
  intro,
  congr' with z,
  have : y ∈ f z → z ≠ x,
  { rintro h' rfl,
    simpa only [*, finset.mem_singleton] using h', },
  tauto,
end

This way you get a glimpse at what simp actually did, but you have to copy out the goal :-(

[Patrick Johnson]

I think the trade-off between readability and maintainability is unavoidable in this case. If we use simp to modify the goal, we have to specify either what the goal should look like after simplification, or what simplification rules are allowed to be used. Otherwise, adding another @[simp] lemma may break the proof.

[Kyle Miller]

I've been thinking that we should allow this type of nonterminal simp:

begin
  ext y,
  simp,
  match_target ¬y = x' →
    ((∃ (a : T), a ∈ S ∧ y ∈ f a) ↔ ∃ (a : T), (a ∈ S ∧ ¬a = x) ∧ y ∈ f a),
  intro,
  congr' with z,
  have : y ∈ f z → z ≠ x,
  { rintro h' rfl,
    simpa only [*, finset.mem_singleton] using h', },
  tauto,
end

[Kyle Miller]

It's a lot more readable than the suffices/simpa pattern in my opinion

[Patrick Johnson]

simp is not aware of the match_target's argument, while simpa ... using is aware of what the result should be. Adding a new @[simp] lemma may break simp, match_target, but not simp only or suffices ... simpa

[Kyle Miller]

simpa doesn't actually use what the result should be -- the algorithm is more-or-less "simp both the target and the specified hypothesis then use exact"

[Kyle Miller]

A reason non-terminal simp is not allowed is that you get brittle code from not knowing what the intermediate goal is supposed to be. When you have a terminal simp, you at least know what the goal is supposed to be, which makes it much easier to fix things when the proof breaks when the simp set changes.

[Kyle Miller]

If the simp set changes, the suffices/simpa construct can also break (if it's not a simpa only), but having the explicit goal right there in the tactic proof makes fixing it easier.

[Patrick Thomas]

Would the previous and the following be worth adding to mathlib? Did I miss simpler proofs from already existing theorems?

import data.finset

example
  {T : Type}
  [decidable_eq T]
  (x : T)
  (s : finset T)
  (f : T → finset T)
  (h1 : ∀ y : T, y ∈ s → x ∉ (f y)) :
  (finset.bUnion s f) \ {x} = finset.bUnion s f :=
begin
  ext1, finish
end

example
  {T : Type}
  [decidable_eq T]
  (s t : finset T)
  (f : T → finset T) :
  (finset.bUnion s f) ∪ (finset.bUnion t f) = finset.bUnion (s ∪ t) f :=
begin
  ext1, simp only [finset.mem_union, finset.mem_bUnion, exists_prop], split, finish, finish
end

example
  {T : Type}
  [decidable_eq T]
  {n : ℕ}
  (g : T → finset T)
  (f : fin n → finset T) :
  finset.bUnion finset.univ (fun i : fin n, finset.bUnion (f i) g) =
    finset.bUnion (finset.bUnion finset.univ (fun i : fin n, (f i))) g :=
begin
  ext1, simp only [finset.mem_bUnion, finset.mem_univ, exists_prop, exists_true_left], tauto
end

example
  {T : Type}
  [decidable_eq T]
  (x : T)
  (S : finset T)
  (f : T → finset T) :
  finset.bUnion ({x} ∪ S) f = (finset.bUnion S f) ∪ f x :=
begin
  ext, simp only [finset.mem_bUnion, finset.mem_union, finset.mem_singleton, exists_prop],
  split, finish, finish,
end

[Kyle Miller]

@Patrick Thomas I think some versions of these should find their way into mathlib. I had a go at generalizing them and adding some other missing lemmas.

import data.finset

namespace finset
variables {α : Type*} {β : Type*} {γ : Type*}

lemma mem_ite (x : α) (p : Prop) [decidable p] (s s' : finset α) :
  x ∈ (if p then s else s') ↔ (p → x ∈ s) ∧ (¬ p → x ∈ s') :=
by split_ifs with h; simp [h]

lemma bUnion_sdiff [decidable_eq α] [decidable_eq β]
  (s : finset α) (t : α → finset β) (s' : finset β) :
  s.bUnion t \ s' = s.bUnion (λ x, t x \ s') :=
by { ext, simp only [mem_sdiff, mem_bUnion, exists_prop], tauto }

lemma bUnion_filter [decidable_eq α] [decidable_eq β]
  (s : finset α) (t : α → finset β) (p : α → Prop) [decidable_pred p] :
  (s.filter p).bUnion t = s.bUnion (λ x, if p x then t x else ∅) :=
begin
  ext,
  simp only [mem_ite, imp_iff_not_or, or_and_distrib_right, mem_bUnion, mem_filter, exists_prop,
    not_mem_empty, not_not, or_false, not_and_self, false_or],
  tauto,
end

lemma sdiff_singleton_bUnion [decidable_eq α] [decidable_eq β]
  (s : finset α) (t : α → finset β)
  (x : α) (s' : finset β)
  (h : t x = s') :
  (s \ {x}).bUnion t \ s' = s.bUnion t \ s' :=
begin
  rw [← h, bUnion_sdiff, bUnion_sdiff, sdiff_eq_filter s, bUnion_filter],
  congr',
  ext y,
  suffices : (a ∉ t y ∨ a ∈ t x) ∨ ¬y = x,
  { simpa [mem_ite, imp_false, imp_iff_not_or, and_or_distrib_left] },
  rw [or_comm, ← imp_iff_not_or],
  rintro rfl,
  apply em',
end

lemma bUnion_union [decidable_eq α] [decidable_eq β]
  (s s' : finset α) (t : α → finset β) :
  (s ∪ s').bUnion t = s.bUnion t ∪ s'.bUnion t :=
by { ext, simp [or_and_distrib_right, exists_or_distrib] }

lemma bUnion_sdiff_of_forall_disjoint [decidable_eq β]
  (s : finset α) (t : α → finset β) (s' : finset β)
  (h : ∀ y : α, y ∈ s → disjoint (t y) s') :
  (s.bUnion t) \ s' = s.bUnion t :=
by simpa [sdiff_eq_self_iff_disjoint, disjoint_bUnion_left]

-- Maybe this might be somewhat too specialized?
lemma bUnion_sdiff_singleton_of_forall_not_mem [decidable_eq β]
  (s : finset α) (x : β) (t : α → finset β)
  (h : ∀ y : α, y ∈ s → x ∉ t y) :
  (s.bUnion t) \ {x} = s.bUnion t :=
bUnion_sdiff_of_forall_disjoint s t _ (by simpa [disjoint_singleton_right])

end finset

[Kyle Miller]

Here are then your specializations:

-- This one is `finset.bUnion_bUnion`
example
  {T : Type}
  [decidable_eq T]
  {n : ℕ}
  (g : T → finset T)
  (f : fin n → finset T) :
  finset.bUnion finset.univ (fun i : fin n, finset.bUnion (f i) g) =
    finset.bUnion (finset.bUnion finset.univ (fun i : fin n, (f i))) g :=
(finset.bUnion_bUnion _ _ _).symm

-- This one is essentially `finset.bUnion_union`
example
  {T : Type}
  [decidable_eq T]
  (x : T)
  (S : finset T)
  (f : T → finset T) :
  finset.bUnion ({x} ∪ S) f = (finset.bUnion S f) ∪ f x :=
by simp [finset.bUnion_union, finset.union_comm]

example
  {T : Type} [decidable_eq T]
  (x x' : T)
  (S : finset T)
  (f : T → finset T)
  (h1 : f x = {x'}) :
  (finset.bUnion S f) \ {x'} = (finset.bUnion (S \ {x}) f) \ {x'} :=
(finset.sdiff_singleton_bUnion _ _ _ _ h1).symm

[Kyle Miller]

By the way, tactic#finish is no longer used for mathlib since it's not being ported to Lean 4.

[Patrick Thomas]

Thank you!

[Kyle Miller]

Here's a generalization of sdiff_singleton_bUnion:

lemma and_self_imp {p q : Prop} : p ∧ (p → q) ↔ p ∧ q := by tauto

lemma finset.sdiff_bUnion_sdiff [decidable_eq α] [decidable_eq β]
  (s s' : finset α) (t : α → finset β) :
  (s \ s').bUnion t \ s'.bUnion t = s.bUnion t \ s'.bUnion t :=
begin
  simp only [sdiff_eq_filter, bUnion_filter, filter_bUnion, ite_not, mem_bUnion,
    exists_prop, not_exists, not_and],
  congr',
  ext,
  simp only [mem_ite, imp_false, and_self_imp, imp_not_comm, mem_filter, not_mem_empty,
    and.congr_left_iff, and_iff_right_iff_imp],
  intro h,
  exact h x,
end

[Patrick Thomas]

Thank you! What would be the next step to get these into mathlib?