Theory Sunflower
section ‹Sunflowers›
text ‹Sunflowers are sets of sets, such that whenever an element
is contained in at least two of the sets,
then it is contained in all of the sets.›
theory Sunflower
imports Main
"HOL-Library.FuncSet"
begin
definition sunflower :: "'a set set ⇒ bool" where
"sunflower S = (∀ x. (∃ A B. A ∈ S ∧ B ∈ S ∧ A ≠ B ∧
x ∈ A ∧ x ∈ B)
⟶ (∀ A. A ∈ S ⟶ x ∈ A))"
lemma sunflower_subset: "F ⊆ G ⟹ sunflower G ⟹ sunflower F"
unfolding sunflower_def by blast
lemma pairwise_disjnt_imp_sunflower:
"pairwise disjnt F ⟹ sunflower F"
unfolding sunflower_def
by (metis disjnt_insert1 mk_disjoint_insert pairwiseD)
lemma card2_sunflower: assumes "finite S" and "card S ≤ 2"
shows "sunflower S"
proof -
from assms have "card S = 0 ∨ card S = Suc 0 ∨ card S = 2" by linarith
with ‹finite S› obtain A B where "S = {} ∨ S = {A} ∨ S = {A,B}"
using card_2_iff[of S] card_1_singleton_iff[of S] by auto
thus ?thesis unfolding sunflower_def by auto
qed
lemma empty_sunflower: "sunflower {}"
by (rule card2_sunflower, auto)
lemma singleton_sunflower: "sunflower {A}"
by (rule card2_sunflower, auto)
lemma doubleton_sunflower: "sunflower {A,B}"
by (rule card2_sunflower, auto, cases "A = B", auto)
lemma sunflower_imp_union_intersect_unique:
assumes "sunflower S"
and "x ∈ (⋃ S) - (⋂ S)"
shows "∃! A. A ∈ S ∧ x ∈ A"
proof -
from assms obtain A where A: "A ∈ S" "x ∈ A" by auto
show ?thesis
proof
show "A ∈ S ∧ x ∈ A" using A by auto
fix B
assume B: "B ∈ S ∧ x ∈ B"
show "B = A"
proof (rule ccontr)
assume "B ≠ A"
with A B have "∃A B. A ∈ S ∧ B ∈ S ∧ A ≠ B ∧ x ∈ A ∧ x ∈ B" by auto
from ‹sunflower S›[unfolded sunflower_def, rule_format, OF this]
have "x ∈ ⋂ S" by auto
with assms show False by auto
qed
qed
qed
lemma union_intersect_unique_imp_sunflower:
assumes "⋀ x. x ∈ (⋃ S) - (⋂ S) ⟹ ∃⇩≤⇩1 A. A ∈ S ∧ x ∈ A"
shows "sunflower S"
unfolding sunflower_def
proof (intro allI impI, elim exE conjE, goal_cases)
case (1 x C A B)
hence x: "x ∈ ⋃ S" by auto
show ?case
proof (cases "x ∈ ⋂ S")
case False
with assms[of x] x have "∃⇩≤⇩1 A. A ∈ S ∧ x ∈ A" by blast
with 1 have False unfolding Uniq_def by blast
thus ?thesis ..
next
case True
with 1 show ?thesis by blast
qed
qed
lemma sunflower_iff_union_intersect_unique:
"sunflower S ⟷ (∀ x ∈ ⋃ S - ⋂ S. ∃! A. A ∈ S ∧ x ∈ A)"
(is "?l = ?r")
proof
assume ?l
from sunflower_imp_union_intersect_unique[OF this]
show ?r by auto
next
assume ?r
hence *: "∀x∈⋃ S - ⋂ S. ∃⇩≤⇩1 A. A ∈ S ∧ x ∈ A"
unfolding ex1_iff_ex_Uniq by auto
show ?l
by (rule union_intersect_unique_imp_sunflower, insert *, auto)
qed
lemma sunflower_iff_intersect_Uniq:
"sunflower S ⟷ (∀ x. x ∈ ⋂ S ∨ (∃⇩≤⇩1 A. A ∈ S ∧ x ∈ A))"
(is "?l = ?r")
proof
assume ?l
from sunflower_imp_union_intersect_unique[OF this]
show ?r unfolding ex1_iff_ex_Uniq
by (metis (no_types, lifting) DiffI UnionI Uniq_I)
next
assume ?r
show ?l
by (rule union_intersect_unique_imp_sunflower, insert ‹?r›, auto)
qed
text ‹If there exists sunflowers whenever all elements are sets of
the same cardinality @{term r}, then there also exists sunflowers
whenever all elements are sets with cardinality at most @{term r}.›
lemma sunflower_card_subset_lift: fixes F :: "'a set set"
assumes sunflower: "⋀ G :: ('a + nat) set set.
(∀ A ∈ G. finite A ∧ card A = k) ⟹ card G > c
⟹ ∃ S. S ⊆ G ∧ sunflower S ∧ card S = r"
and kF: "∀ A ∈ F. finite A ∧ card A ≤ k"
and cardF: "card F > c"
shows "∃ S. S ⊆ F ∧ sunflower S ∧ card S = r"
proof -
let ?n = "Suc c"
from cardF have "card F ≥ ?n" by auto
then obtain FF where sub: "FF ⊆ F" and cardF: "card FF = ?n"
by (rule obtain_subset_with_card_n)
let ?N = "{0 ..< ?n}"
from cardF have "finite FF"
by (simp add: card_ge_0_finite)
from ex_bij_betw_nat_finite[OF this, unfolded cardF]
obtain f where f: "bij_betw f ?N FF" by auto
hence injf: "inj_on f ?N" by (rule bij_betw_imp_inj_on)
have Ff: "FF = f ` ?N"
by (metis bij_betw_imp_surj_on f)
define g where "g = (λ i. (Inl ` f i) ∪ (Inr ` {0 ..< (k - card (f i))}))"
have injg: "inj_on g ?N" unfolding g_def using f
proof (intro inj_onI, goal_cases)
case (1 x y)
hence "f x = f y" by auto
with injf 1 show "x = y"
by (meson inj_onD)
qed
hence cardgN: "card (g ` ?N) > c"
by (simp add: card_image)
{
fix i
assume "i ∈ ?N"
hence "f i ∈ FF" unfolding Ff by auto
with sub have "f i ∈ F" by auto
hence "card (f i) ≤ k" "finite (f i)" using kF by auto
hence "card (g i) = k ∧ finite (g i)" unfolding g_def
by (subst card_Un_disjoint, auto, subst (1 2) card_image, auto intro: inj_onI)
}
hence "∀ A ∈ g ` ?N. finite A ∧ card A = k" by auto
from sunflower[OF this cardgN]
obtain S where SgN: "S ⊆ g ` ?N" and sf: "sunflower S" and card: "card S = r" by auto
from SgN obtain N where NN: "N ⊆ ?N" and SgN: "S = g ` N"
by (meson subset_image_iff)
from injg NN have inj_g: "inj_on g N"
by (rule inj_on_subset)
from injf NN have inj_f: "inj_on f N"
by (rule inj_on_subset)
from card_image[OF inj_g] SgN card
have cardN: "card N = r" by auto
let ?S = "f ` N"
show ?thesis
proof (intro exI[of _ ?S] conjI)
from NN show "?S ⊆ F" using Ff sub by auto
from card_image[OF inj_f] cardN show "card ?S = r" by auto
show "sunflower ?S" unfolding sunflower_def
proof (intro allI impI, elim exE conjE, goal_cases)
case (1 x C A B)
from ‹A ∈ f ` N› obtain i where i: "i ∈ N" and A: "A = f i" by auto
from ‹B ∈ f ` N› obtain j where j: "j ∈ N" and B: "B = f j" by auto
from ‹C ∈ f ` N› obtain k where k: "k ∈ N" and C: "C = f k" by auto
hence gk: "g k ∈ g ` N" by auto
from ‹A ≠ B› A B have ij: "i ≠ j" by auto
from inj_g ij i j have gij: "g i ≠ g j" by (metis inj_on_contraD)
from ‹x ∈ A› have memi: "Inl x ∈ g i" unfolding A g_def by auto
from ‹x ∈ B› have memj: "Inl x ∈ g j" unfolding B g_def by auto
have "∃A B. A ∈ g ` N ∧ B ∈ g ` N ∧ A ≠ B ∧ Inl x ∈ A ∧ Inl x ∈ B"
using memi memj gij i j by auto
from sf[unfolded sunflower_def SgN, rule_format, OF this gk] have "Inl x ∈ g k" .
thus "x ∈ C" unfolding C g_def by auto
qed
qed
qed
text ‹We provide another sunflower lifting lemma that ensures
non-empty cores. Here, all elements must be taken
from a finite set, and the bound is multiplied the cardinality.›
lemma sunflower_card_core_lift:
assumes finE: "finite (E :: 'a set)"
and sunflower: "⋀ G :: 'a set set.
(∀ A ∈ G. finite A ∧ card A ≤ k) ⟹ card G > c
⟹ ∃ S. S ⊆ G ∧ sunflower S ∧ card S = r"
and F: "∀ A ∈ F. A ⊆ E ∧ s ≤ card A ∧ card A ≤ k"
and cardF: "card F > (card E choose s) * c"
and s: "s ≠ 0"
and r: "r ≠ 0"
shows "∃ S. S ⊆ F ∧ sunflower S ∧ card S = r ∧ card (⋂ S) ≥ s"
proof -
let ?g = "λ (A :: 'a set) x. card x = s ∧ x ⊆ A"
let ?E = "{X. X ⊆ E ∧ card X = s}"
from cardF have finF: "finite F"
by (metis card.infinite le_0_eq less_le)
from cardF have FnE: "F ≠ {}" by force
{
from FnE obtain B where B: "B ∈ F" by auto
with F[rule_format, OF B] obtain A where "A ⊆ E" "card A = s"
by (meson obtain_subset_with_card_n order_trans)
hence "?E ≠ {}" using B by auto
} note EnE = this
define f where "f = (λ A. SOME x. ?g A x)"
from finE have finiteE: "finite ?E" by simp
have "f ∈ F → ?E"
proof
fix B
assume B: "B ∈ F"
with F[rule_format, OF B] have "∃ x. ?g B x" by (meson obtain_subset_with_card_n)
from someI_ex[OF this] B F show "f B ∈ ?E" unfolding f_def by auto
qed
from pigeonhole_card[OF this finF finiteE EnE]
obtain a where a: "a ∈ ?E"
and le: "card F ≤ card (f -` {a} ∩ F) * card ?E" by auto
have precond: "∀A∈f -` {a} ∩ F. finite A ∧ card A ≤ k"
using F finite_subset[OF _ finE] by auto
have "c * (card E choose s) = (card E choose s) * c" by simp
also have "… < card F" by fact
also have "… ≤ (card (f -` {a} ∩ F)) * card ?E" by fact
also have "card ?E = card E choose s" by (rule n_subsets[OF finE])
finally have "c < card (f -` {a} ∩ F)" by auto
from sunflower[OF precond this]
obtain S where *: "S ⊆ f -` {a} ∩ F" "sunflower S" "card S = r"
by auto
from finite_subset[OF _ finF, of S]
have finS: "finite S" using * by auto
from * r have SnE: "S ≠ {}" by auto
have finIS: "finite (⋂ S)"
proof (rule finite_Inter)
from SnE obtain A where A: "A ∈ S" by auto
with F s have "finite A"
using * precond by blast
thus "∃A∈S. finite A" using A by auto
qed
show ?thesis
proof (intro exI[of _ S] conjI *)
show "S ⊆ F" using * by auto
{
fix A
assume "A ∈ S"
with *(1) have "A ∈ f -` {a}" and A: "A ∈ F" using * by auto
from this have **: "f A = a" "A ∈ F" by auto
from F[rule_format, OF A] have "∃x. card x = s ∧ x ⊆ A"
by (meson obtain_subset_with_card_n order_trans)
from someI_ex[of "?g A", OF this] **
have "a ⊆ A" unfolding f_def by auto
}
hence "a ⊆ ⋂ S" by auto
from card_mono[OF finIS this]
have "card a ≤ card (⋂ S)" .
with a show "s ≤ card (⋂ S)" by auto
qed
qed
lemma sunflower_nonempty_core_lift:
assumes finE: "finite (E :: 'a set)"
and sunflower: "⋀ G :: 'a set set.
(∀ A ∈ G. finite A ∧ card A ≤ k) ⟹ card G > c
⟹ ∃ S. S ⊆ G ∧ sunflower S ∧ card S = r"
and F: "∀ A ∈ F. A ⊆ E ∧ card A ≤ k"
and empty: "{} ∉ F"
and cardF: "card F > card E * c"
shows "∃ S. S ⊆ F ∧ sunflower S ∧ card S = r ∧ (⋂ S) ≠ {}"
proof (cases "r = 0")
case False
from F empty have F': "∀A∈F. A ⊆ E ∧ 1 ≤ card A ∧ card A ≤ k " using finE
by (metis One_nat_def Suc_leI card_gt_0_iff finite_subset)
from cardF have cardF': "(card E choose 1) * c < card F" by auto
from sunflower_card_core_lift[OF finE sunflower, of k c F 1, OF _ _ F' cardF' _ False]
obtain S where "S ⊆ F" and main: "sunflower S" "card S = r" "1 ≤ card (⋂ S)" by auto
thus ?thesis by (intro exI[of _ S], auto)
next
case True
thus ?thesis by (intro exI[of _ "{}"], auto simp: empty_sunflower)
qed
end