diff --git a/TheBook/Combinatorics/LYM.lean b/TheBook/Combinatorics/LYM.lean new file mode 100644 index 0000000..7a6d4ee --- /dev/null +++ b/TheBook/Combinatorics/LYM.lean @@ -0,0 +1,98 @@ +import Mathlib.Tactic +import Mathlib.Combinatorics.Enumerative.DoubleCounting +import Mathlib.Combinatorics.Derangements.Finite +import Mathlib.Logic.Equiv.Defs +import Mathlib.Data.Set.Basic +import Mathlib.Data.Finset.Slice +import Mathlib.Order.Antichain +import Mathlib.Order.Chain +import Mathlib.Data.List.Perm.Basic +import TheBook.ToMathlib.Chain +import TheBook.ToMathlib.Antichain +import TheBook.ToMathlib.List +import TheBook.Combinatorics.SpernerHelpingDataStructures + +/-! +# LYM + +In this file we give the proof of the **Lubell-Yamamoto-Meshalkin inequality** as it is given in the book of the proofs. +Sperner's Theorem follows from this as a corollary (compare with Mathlib.Combinatorics.SetFamily.LYM). + +## Main results +- `lym_inequality`: The sum of the proportional cardinalities of all slices of an antichain is at most '1'. +-/ + +open Function Finset Nat Set BigOperators List + +variable {α : Type*} {n m : ℕ} [DecidableEq α] [Fintype α] {𝒜 : Set (Finset α)} [DecidablePred (· ∈ 𝒜)] [DecidableEq (Set (Finset α))] +instance : Fintype 𝒜 := setFintype 𝒜 + +namespace Finset + +/-- The sum of the proportional cardinalities of all slices of an antichain is at most '1'. -/ +theorem lym_inequality (antichain𝒜 : IsAntichain (· ⊂ ·) 𝒜) (hn : Fintype.card α = n): + ∑ k ∈ Iic n, #(𝒜.toFinset # k) / (n.choose k : ℚ) ≤ (1 : ℚ) := by + have : ∑ k ∈ Iic n, #(𝒜.toFinset # k) / (n.choose k : ℚ) ≤ (∑ k ∈ Iic n, #(𝒜.toFinset # k) * (k)! * (n - k)!) * (1 / (n)! : ℚ) := by + calc + ∑ k ∈ Iic n, #(𝒜.toFinset # k) / (n.choose k : ℚ) = ∑ k ∈ Iic n, #(𝒜.toFinset # k) * (k)! * (n - k)! * (1 / (n)! : ℚ) := by + apply Finset.sum_congr (by simp) + intro j jmem + simp at jmem + rw [div_eq_mul_inv, mul_assoc, mul_assoc, Nat.choose_eq_factorial_div_factorial] + congr + field_simp + + have choose_divisibility (a b : ℕ) (h : a ≤ b) : ((a)! * (b - a)!) ∣ (b)! := by + use b.choose a + rw [Nat.mul_comm, ←Nat.mul_assoc] + exact (Nat.choose_mul_factorial_mul_factorial h).symm + + rw [Nat.cast_div (choose_divisibility j n jmem), Nat.cast_mul] + · field_simp + · norm_num + constructor <;> apply Nat.factorial_ne_zero + · exact jmem + _ = (∑ k ∈ Iic n, #(𝒜.toFinset # k) * (k)! * (n - k)!) * (1 / (n)! : ℚ) := by simp [←Finset.sum_mul] + rfl + + refine' le_trans this _ + rw [mul_one_div] + apply (div_le_one (by simp [Nat.factorial_pos n])).mpr + + norm_cast + + have slice_partition : Finset.disjiUnion (Iic n) 𝒜.toFinset.slice (Finset.pairwiseDisjoint_slice.subset (Set.subset_univ _)) = 𝒜.toFinset := by + rw [Finset.disjiUnion_eq_biUnion (Iic n) 𝒜.toFinset.slice (Finset.pairwiseDisjoint_slice.subset (Set.subset_univ _))] + rw [←hn] + have := biUnion_slice 𝒜.toFinset + exact this + + calc + ∑ k ∈ Iic n, #(𝒜.toFinset # k) * (k)! * (n - k)! = ∑ k ∈ Iic n, ∑ e ∈ (𝒜.toFinset # k), (#e)! * (n - #e)! := by + apply Finset.sum_congr (by simp) + intro k _ + have hq : ∀ e ∈ (𝒜.toFinset # k), (#e)! * (n - #e)! = (k)! * (n - k)! := by + intro e he + simp [slice] at he + rw [he.2] + rw [Finset.sum_congr rfl hq, Finset.sum_const] + ring + _ = ∑ e ∈ 𝒜, (#e)! * (n - #e)! := by + conv => + rhs + rw [←slice_partition] + apply Eq.symm + apply sum_disjiUnion + _ = ∑ e ∈ 𝒜, Fintype.card (MaxChainThrough {e}) := by + apply Finset.sum_congr (by simp) + intro e _ + apply Eq.symm + exact count_maxChains_through_singleton e hn + _ = ∑ e ∈ 𝒜, #((Finset.univ : Finset (MaxChainThrough {e})).image (emb_MaxChainThrough {e})) := by + apply Finset.sum_congr (by simp) + intro e e_mem + rw [Finset.card_image_of_injective (Finset.univ : Finset (MaxChainThrough {e})) inj_emb_MaxChainThrough, Finset.card_univ] + _ = #(𝒜.toFinset.disjiUnion (fun e : Finset α ↦ (Finset.univ : Finset (MaxChainThrough {e})).image (emb_MaxChainThrough {e})) (by simp [AntiChain.disj_union_chain_through antichain𝒜])) := by + + sorry + _ ≤ (n)! := by sorry diff --git a/TheBook/Combinatorics/SpernerHelpingDataStructures.lean b/TheBook/Combinatorics/SpernerHelpingDataStructures.lean new file mode 100644 index 0000000..bb25fa9 --- /dev/null +++ b/TheBook/Combinatorics/SpernerHelpingDataStructures.lean @@ -0,0 +1,548 @@ +import TheBook.ToMathlib.Chain +import TheBook.ToMathlib.List + +open Function Finset Nat Set BigOperators List + +variable {α : Type*} {n m : ℕ} {𝒜 ℬ : Set (Finset α)} + +set_option maxHeartbeats 500000 + +namespace Finset + +section MaxChainThrough + +/-! +# Sperner Helping Data Structures + +## Main results +- `incident_indices_monotone_cards`: Two sets in a chain with no intermediate sets are incident in the list of chain elements that is sorted by cardinality. +- `chain_through_extension_candidates_pairwiseDisjoint`: The maximal chains through 'Insert x e' and 'ℬ' for extension candidates of 'e' in 'ℬ' are pairwise disjoint. +- `central_identity`: The set of maximal chains through 'ℬ' equals the disjoint union all chains through 'ℬ' and 'Insert x e' for all extension candidates 'x' of 'e' in 'ℬ' in case that these extension candidates are nonempty. +- `count_maxChainsThrough`: An exact formula for the number of maximal chains through any given chain. +- `count_maxChains_through_singleton_insert_empty`: Inserting the empty set into a chain does not change the maximal chains running through. +- `count_maxChains_through_singleton_insert_univ`: Inserting the universal set into a chain does not change the maximal chains running through. +- `count_maxChains_through_empty`: The count of maximal chains through the empty set is 'n!'. +- `count_maxChains_through_univ`: The count of maximal chains through the universal set is 'n!'. +- `count_maxChains_through_singleton`: The count of maximal chains through a set 'e' is '(n - #e)! * (#e)!'. +-/ + + +structure MaxChainThrough (ℬ : Set (Finset α)) where + /- The set of elements in the chain. -/ + 𝒜 : Set (Finset α) + /- '𝒜' is a maximal chain. -/ + isMaxChain : IsMaxChain (· ⊂ ·) 𝒜 + /- '𝒜' is a subset of 'ℬ'. -/ + subChain : ℬ ⊆ 𝒜 + +/- Projection of 'MaxChainThrough' on the set of elements. -/ +def emb_MaxChainThrough (ℬ : Set (Finset α)) (X : MaxChainThrough ℬ) : Set (Finset α) := X.𝒜 + +/- Definition of equality of two variables of type 'MaxChainThrough'-/ +@[ext] lemma MaxChainThrough_eq (𝒞₁ 𝒞₂ : MaxChainThrough ℬ) (hA : 𝒞₁.𝒜 = 𝒞₂.𝒜) : 𝒞₁ = 𝒞₂ := by + cases 𝒞₁ + cases 𝒞₂ + congr + +/- 'emb_MaxChainThrough' is injective. -/ +lemma inj_emb_MaxChainThrough : Injective (emb_MaxChainThrough ℬ) := by + intro 𝒞₁ 𝒞₂ h + unfold emb_MaxChainThrough at h + ext + rw [h] + +instance instFintypeMaxChainThrough : Fintype (MaxChainThrough ℬ) := by sorry + +variable [Fintype α] [DecidableEq α] [DecidableEq (Set (Finset α))] + +instance {C : MaxChainThrough ℬ} : DecidablePred (· ∈ C.𝒜) := by sorry +instance : DecidablePred (· ∈ ℬ) := by sorry +instance : DecidablePred (· ∈ 𝒜) := by sorry + +instance {C : MaxChainThrough ℬ} : Fintype C.𝒜 := setFintype C.𝒜 + +instance : Fintype ℬ := setFintype ℬ +instance : Fintype 𝒜 := setFintype 𝒜 + +/- The first entry in a list of Finsets containing the empty set that is ordered by cardinality is the empty set. -/ +lemma first_entry (list : List (Finset α)) + (monotone_cards: List.Sorted (fun (e₁ e₂) ↦ #e₁ < #e₂) list) (h_list: ℬ.toFinset.toList ~ list) + (empty_in_chain : ∅ ∈ ℬ) : list[0]'(by rw [←Perm.length_eq h_list]; exact length_pos_of_mem (mem_toList.mpr (mem_toFinset.mpr empty_in_chain))) = ∅ := by sorry + +/- The first entry in a list of Finsets containing the universal set that is ordered by cardinality is the universal set. -/ +lemma last_entry {list : List (Finset α)} + (monotone_cards: List.Sorted (fun (e₁ e₂) ↦ #e₁ < #e₂) list) (h_list: ℬ.toFinset.toList ~ list) + (univ_in_chain : univ ∈ ℬ) : list[list.length - 1]'(by sorry) = univ := by sorry + +/- Two sets in a chain with no intermediate sets are incident in the list of chain elements that is sorted by cardinality. -/ +lemma incident_indices_monotone_cards {s t : Fin (n + 1)} {ℬ : Finset (Finset α)} (s_lt_t : s < t) (list : List (Finset α)) + (monotone_cards: List.Sorted (fun (e₁ e₂) ↦ #e₁ < #e₂) list) (h_list: ℬ.toList ~ list) + (hs : (ℬ # s) = {layer_s}) (ht : (ℬ # t) = {layer_t}) + (empty_layer : ∀ j : Fin (n + 1), s < j → j < t → #(ℬ # ↑j) = 0) : + ∃ i_s : Fin (list.length - 1), list[i_s.val] = layer_s ∧ list[i_s.val + 1] = layer_t := by + + let i_s := list.indexOf layer_s + have i_s_in_range : i_s < list.length := List.indexOf_lt_length.mpr (h_list.subset (mem_toList.mpr (Slice.singleton_explicit.mp hs).left)) + have h_i_s : list[i_s] = layer_s := list.indexOf_get i_s_in_range + + let i_t := list.indexOf layer_t + have i_t_in_range : i_t < list.length := List.indexOf_lt_length.mpr (h_list.subset (mem_toList.mpr (Slice.singleton_explicit.mp ht).left)) + have h_i_t : list[i_t] = layer_t := list.indexOf_get i_t_in_range + + simp at i_t_in_range + simp at i_s_in_range + + have i_s_eq_i_t_succ : i_t = i_s + 1 := by + by_contra ass₁ + have : i_t > i_s := by + by_contra! ass₂ + unfold List.Sorted at monotone_cards + have : list[i_t] ≤ list[i_s] := by + cases le_iff_eq_or_lt.mp ass₂ with + | inl h => + simp [h] + | inr h => + have : i_t < list.length := by + simpa + have := ((List.pairwise_iff_get.mp monotone_cards) ⟨i_t, by simpa⟩ ⟨i_s, by simpa⟩ h) + simp at this + exact le_of_lt this + simp [h_i_s, h_i_t] at this + have : t.val ≤ s.val := by + simp [←(Slice.singleton_explicit.mp hs).right.left, ←(Slice.singleton_explicit.mp ht).right.left] + exact this + simp at this + omega + have i_s_succ_lt : i_s + 1 < i_t := Nat.lt_of_le_of_ne this fun a => ass₁ (id (Eq.symm a)) + + let e := list[i_s + 1] + + have e_card_gt' : #e > s := by + have := (List.pairwise_iff_get.mp monotone_cards) ⟨i_s, by simpa⟩ ⟨i_s + 1, by apply Nat.lt_trans i_s_succ_lt; simpa ⟩ (by simp : i_s < i_s + 1) + simp [h_i_s, (Slice.singleton_explicit.mp hs).right.left] at this + unfold e + exact this + + have e_card_lt' : #e < t := by + have := (List.pairwise_iff_get.mp monotone_cards) ⟨i_s + 1, by apply Nat.lt_trans i_s_succ_lt; simpa⟩ ⟨i_t, by simpa⟩ i_s_succ_lt + simp [h_i_t, (Slice.singleton_explicit.mp ht).right.left] at this + exact this + + have card_e_mod : #e % (n + 1) = #e := mod_eq_of_lt (Nat.lt_trans e_card_lt' t.is_lt) + + have e_card_gt : Fin.ofNat #e > s := by simp [Fin.ofNat, card_e_mod]; exact e_card_gt' + have e_card_lt : Fin.ofNat #e < t := by simp [Fin.ofNat, card_e_mod]; exact e_card_lt' + + have layer_empty := empty_layer (Fin.ofNat #e) e_card_gt e_card_lt + + have layer_nonempty : e ∈ (ℬ # ↑(Fin.ofNat #e : Fin (n + 1))) := by + simp [mem_slice] + constructor + · apply mem_toList.mp + exact (List.Perm.symm h_list).subset ((List.get_mem list (i_s + 1)) (Nat.lt_trans i_s_succ_lt i_t_in_range)) + · simp [Fin.ofNat, card_e_mod] + + simp at layer_empty + + simp [layer_empty] at layer_nonempty + + have i_s_upperbound : i_s < list.length - 1 := + have : i_s + 1 < list.length := by rw [←i_s_eq_i_t_succ]; exact i_t_in_range + lt_sub_of_add_lt this + + use ⟨i_s, i_s_upperbound⟩ + + simp only [i_s_eq_i_t_succ] at h_i_t + exact ⟨h_i_s, h_i_t⟩ + +/- The projections of all maximal chains through '(Insert.insert x e)' and 'ℬ'. -/ +def extensions_wrt [DecidableEq (Set (Finset α))] [DecidableEq (Finset α)] (ℬ : Set (Finset α)) (e : Finset α) (x : α) : Finset (Set (Finset α)) := by + let ℬ' := Insert.insert (Insert.insert x e) ℬ + exact (univ : Finset (MaxChainThrough ℬ')).image (emb_MaxChainThrough ℬ') + +variable [DecidableEq (Set (Finset α))] [DecidableEq (Finset α)] + +/- The maximal chains through 'Insert x e' and 'ℬ' for extension candidates 'e' are pairwise disjoint. -/ +lemma chain_through_extension_candidates_pairwiseDisjoint {e : Finset α} (e_mem : e ∈ ℬ) : PairwiseDisjoint (extension_candidates ℬ e) (extensions_wrt ℬ e) := by + intro x hx y hy xneqy + simp [_root_.Disjoint] + simp [extensions_wrt] + intro A hA_x hA_y + intro 𝒜 h𝒜 + simp + + simp [extension_candidates,insert_extends_chain] at hx hy + + have a_extension_e_x := hA_x h𝒜 + have a_extension_e_y := hA_y h𝒜 + simp at a_extension_e_x a_extension_e_y + + obtain ⟨𝒜_x, image_𝒜_x⟩ := a_extension_e_x + obtain ⟨𝒜_y, image_𝒜_y⟩ := a_extension_e_y + + unfold emb_MaxChainThrough at image_𝒜_x image_𝒜_y + + have x_e_mem_𝒜_y : (insert x e) ∈ 𝒜_y.𝒜 := by + rw [image_𝒜_y, ←image_𝒜_x] + apply 𝒜_x.subChain + simp + + have y_e_mem_𝒜_y : (insert y e) ∈ 𝒜_y.𝒜 := by apply 𝒜_y.subChain; simp + + have x_nmem : x ∉ e := by + by_contra! ass + rw [insert_eq_of_mem ass] at hx + exact hx.right e_mem + + have y_nmem : y ∉ e := by + by_contra! ass + rw [insert_eq_of_mem ass] at hy + exact hy.right e_mem + + have eq_card : #(insert x e) = #(insert y e) := by + rw [Finset.card_insert_of_not_mem x_nmem, Finset.card_insert_of_not_mem y_nmem] + + have : y = x ∨ y ∈ e := by + apply mem_insert.mp + rw [IsChain.unique_of_cardinality_chain 𝒜_y.isMaxChain.left x_e_mem_𝒜_y y_e_mem_𝒜_y eq_card] + exact mem_insert_self y e + + cases this with + | inl h => exact xneqy h.symm + | inr h => exact y_nmem h + +/- The set of maximal chains through 'ℬ' equals the disjoint union all chains through 'ℬ' and 'Insert x e' for all extension candidates 'x' of 'e' in 'ℬ' in case that these extension candidates are nonempty. -/ +lemma central_identity (e : Finset α) (e_mem : e ∈ ℬ) (h : extension_candidates ℬ e ≠ ∅): + (univ : Finset (MaxChainThrough ℬ)).image (emb_MaxChainThrough ℬ) = (extension_candidates ℬ e).disjiUnion (extensions_wrt ℬ e) + (chain_through_extension_candidates_pairwiseDisjoint e_mem) := by + ext + constructor + · intro 𝒜_mem_image + simp at 𝒜_mem_image + + simp [extension_candidates, insert_extends_chain, extensions_wrt] + + have e_card_lt := (extension_candidates_nonempty rfl h).left + + obtain ⟨C,C_emb⟩ := 𝒜_mem_image + simp [emb_MaxChainThrough] at C_emb + + have card_next := IsMaxChain.one_elt_max_chain_layer rfl C.isMaxChain ⟨#e + 1, mem_range.mpr ((add_lt_add_iff_right 1).mpr e_card_lt)⟩ + obtain ⟨u, hu⟩ := card_eq_one.mp card_next + + have u_slice := mem_singleton_self u + rw [←hu] at u_slice + simp [slice] at u_slice + + have card_e_lt_u : #e < #u := by sorry + + have e_ssub_u := IsChain.ssubset_of_lt_cardinality C.isMaxChain.left (C.subChain e_mem) u_slice.left card_e_lt_u + + obtain ⟨a, ha⟩ := sdiff_nonempty.mpr (not_subset_of_ssubset e_ssub_u) + + use a + + constructor + · sorry + · sorry + · sorry + +/- In a non-maximal chain containing the empty and universal set there are two non-neighbouring slices with no intermediate chain elements. -/ +lemma range_empty_layer (hn : Fintype.card α = n) (chain𝒜 : IsChain (· ⊂ ·) 𝒜) (empty_layer : ∃ i : Fin (n + 1), #(𝒜.toFinset # i) = 0) (empty_elt : ∅ ∈ 𝒜) (univ_elt : univ ∈ 𝒜) : + ∃ s : Fin (n + 1), ∃ t : Fin (n + 1), s.val + 2 ≤ t.val ∧ #(𝒜.toFinset # s) = 1 ∧ #(𝒜.toFinset # t) = 1 ∧ ∀ j : Fin (n + 1), s < j ∧ j < t → #(𝒜.toFinset # j) = 0 := by sorry + +/- An exact formula for the number of maximal chains through any given chain. -/ +theorem count_maxChainsThrough (h_mn : m ≤ n + 1) (hn : Fintype.card α = n) + (cardℬ : #ℬ.toFinset = m) (chainℬ : IsChain (· ⊂ ·) ℬ) (empty_in_chain : ∅ ∈ ℬ) (univ_in_chain : univ ∈ ℬ) + (list : List (Finset α)) (list_per : ℬ.toFinset.toList ~ list) (list_sorted : list.Sorted (#· < #·)): + Fintype.card (MaxChainThrough ℬ) = ∏ j : Fin (list.length - 1), (#list[j.val + 1] - #list[j.val])! := by + revert ℬ list + induction' h_mn using decreasingInduction with n_ q ih + · intro ℬ cardℬ chainℬ empty_in_chain univ_in_chain list list_per list_sorted + + let sorted_list := ((univ : Finset ℬ).toList.insertionSort (fun (e₁ e₂ : ℬ) ↦ #e₁.val ≤ #e₂.val)) + + obtain ⟨s', t', empty_range : s'.val + 2 ≤ t'.val ∧ #(ℬ.toFinset # s') = 1 ∧ #(ℬ.toFinset # t') = 1 ∧ ∀ (j : Fin (n + 1)), s' < j ∧ j < t' → #(ℬ.toFinset # ↑j) = 0⟩ := + range_empty_layer hn chainℬ (by sorry) empty_in_chain univ_in_chain + + let s : range (n + 1) := ⟨s'.val, mem_range.mpr s'.is_lt⟩ + let t : range (n + 1) := ⟨t'.val, mem_range.mpr t'.is_lt⟩ + + have ilej_succ_succ : (s : ℕ) + 2 ≤ (t : ℕ) := by simp [empty_range.left] + + obtain ⟨layer_t, ht : (ℬ.toFinset # t) = {layer_t}⟩ := card_eq_one.mp empty_range.right.right.left + obtain ⟨layer_s, hs : (ℬ.toFinset # s) = {layer_s}⟩ := card_eq_one.mp empty_range.right.left + + have empty_layer' : ∀ j ∈ range (n + 1), s < j → j < t → #(ℬ.toFinset # ↑j) = 0 := by + simp + intro j jinrange jgt jlt + + have nsuccnezero : n + 1 ≠ 0 := by simp + have jmod : j % (n + 1) = j := (mod_eq_iff_lt nsuccnezero).mpr jinrange + have s'ltj : s' < Fin.ofNat j := by simp [Fin.ofNat, jmod]; exact jgt + have jltt' : Fin.ofNat j < t' := by simp [Fin.ofNat, jmod]; exact jlt + have := empty_range.right.right.right j ⟨s'ltj, jltt'⟩ + simp [jmod] at this + exact this + + have empty_layer : ∀ j : Fin (n + 1), s' < j → j < t' → #(ℬ.toFinset # ↑j) = 0 := by + simp + intro j jgt jlt + + have nsuccnezero : n + 1 ≠ 0 := by simp + have := empty_range.right.right.right j ⟨jgt, jlt⟩ + simp at this + exact this + + let extension_candidates := extension_candidates ℬ layer_s + + have extension_candidates_eq : extension_candidates = layer_t \ layer_s := by + refine' extension_candidates_characterisation hn ilej_succ_succ chainℬ hs ht empty_layer' + + have layer_s_mem_card := Slice.singleton_explicit.mp hs + have layer_t_mem_card := Slice.singleton_explicit.mp ht + + have := list_per + + obtain ⟨i_s, ⟨entry_i_s, entry_i_s_succ⟩⟩ := incident_indices_monotone_cards (by sorry) list list_sorted list_per hs ht empty_layer + + have i_s_in_range : i_s < list.length := Nat.lt_of_lt_of_le i_s.is_lt (Nat.pred_le list.length) + have i_s_succ_in_range : i_s.val + 1 < list.length := add_lt_of_lt_sub i_s.is_lt + + let multiplicant' (j : Fin (list.length - 1)) : ℕ := (#list[j.val + 1] - #list[j.val] - 1)! + let multiplicant (j : Fin (list.length - 1)) : ℕ := (#list[j.val + 1] - #list[j.val])! + + have extension_candidates_card : #extension_candidates = #list[i_s.val + 1] - #list[i_s.val] := by + rw [entry_i_s, entry_i_s_succ, layer_s_mem_card.right.left, layer_t_mem_card.right.left] + rw [extension_candidates_eq] + have card_bottom_lt_card_top : #layer_s < #layer_t := by + rw [layer_s_mem_card.right.left, layer_t_mem_card.right.left] + linarith + have bottom_subset_top : layer_s ⊂ layer_t := + IsChain.ssubset_of_lt_cardinality chainℬ (mem_toFinset.mp layer_s_mem_card.left) (mem_toFinset.mp layer_t_mem_card.left) card_bottom_lt_card_top + have := card_sdiff_add_card_eq_card bottom_subset_top.left + rw [←layer_s_mem_card.right.left, ←layer_t_mem_card.right.left] + exact Nat.eq_sub_of_add_eq this + + let 𝒬 := (univ : Finset (Fin (list.length - 1))) + let 𝒬' := 𝒬 \ {i_s} + + let extensions_wrt (x : α) : Finset (Set (Finset α)) := by + let ℬ' : Set (Finset α) := Insert.insert (Insert.insert x layer_s) ℬ + exact (univ : Finset (MaxChainThrough ℬ')).image (emb_MaxChainThrough ℬ') + + /- Here the induction hypothesis ih is applied-/ + have card_extensions_wrt (a : extension_candidates) : #(extensions_wrt a) = (multiplicant' i_s) * ∏ j ∈ 𝒬', (multiplicant j) := by + let e_new := Insert.insert (↑a) layer_s + let ℬ' := (Insert.insert e_new ℬ) + + have a_property₁ := a.prop + simp only [extension_candidates, Finset.extension_candidates, mem_filter, insert_extends_chain] at a_property₁ + + have a_property₂ := a.prop + simp [extension_candidates_eq] at a_property₂ + + have card_e_new : #e_new = s + 1 := by + have := layer_s_mem_card.right.left + simp [s] at this + simp [e_new, ←this] + apply card_insert_of_not_mem + · exact a_property₂.right + + have ℬ'card : #ℬ'.toFinset = n_ + 1 := by + simp only [ℬ', ←cardℬ, e_new] + sorry + -- have := card_insert_of_not_mem a_property₁.right.right + -- · exact a_property₁.right.right + + obtain ⟨list', ⟨list_per' : list' ~ (insert e_new ℬ).toFinset.toList, list_sorted' ⟩⟩ := Chain.card_strict_mono a_property₁.right.left + have embedding_card := card_image_of_injective (univ : Finset (MaxChainThrough ℬ')) inj_emb_MaxChainThrough + simp [extensions_wrt, embedding_card] + + have empty_in_chain' : ∅ ∈ ℬ' := by simp [ℬ']; exact mem_insert_iff.mpr (Or.inr empty_in_chain) + have univ_in_chain' : univ ∈ ℬ' := by simp [ℬ']; exact mem_insert_iff.mpr (Or.inr univ_in_chain) + + let i_new := list'.indexOf e_new + have := list_per'.symm.subset (mem_toList.mpr (mem_toFinset.mpr (Set.mem_insert e_new ℬ))) + + have := (mem_toList.mpr (mem_insert_self e_new ℬ.toFinset)) + have i_new_in_range : i_new < list'.length := (List.indexOf_lt_length.mpr (list_per'.symm.subset (mem_toList.mpr (mem_toFinset.mpr (Set.mem_insert e_new ℬ))))) + have h_i_new : list'[i_new] = e_new := list'.indexOf_get i_new_in_range + + let i_univ := list'.indexOf univ + have i_univ_in_range : i_univ < list'.length := List.indexOf_lt_length.mpr (list_per'.symm.subset (mem_toList.mpr (mem_toFinset.mpr univ_in_chain'))) + have h_i_univ : list'[i_univ] = univ := list'.indexOf_get i_univ_in_range + + have i_new_lt_i_univ' : (⟨i_new, i_new_in_range⟩ : Fin list'.length) < (⟨i_univ, i_univ_in_range⟩ : Fin list'.length) := by + by_contra! ass + + have : s'.val + 2 < n + 1 := lt_of_le_of_lt empty_range.left t'.is_lt + have : s'.val < n + 1 := s'.isLt + + cases lt_or_eq_of_le ass with + | inl h => + have := List.pairwise_iff_get.mp list_sorted' ⟨i_univ, i_univ_in_range⟩ ⟨i_new, i_new_in_range⟩ h + simp at this + simp [h_i_new, h_i_univ, card_e_new, hn] at this + + linarith + | inr h => + have : e_new = univ := by + calc + e_new = list'[i_new] := h_i_new.symm + _ = list'[i_univ] := by simp [Fin.mk.inj_iff.mp h] + _ = univ := h_i_univ + have : s.val + 1 = n := by + rw [←card_e_new, ←hn, this] + rfl + linarith + + have i_new_lt_i_univ_pred : i_new < list'.length - 1 := Nat.lt_of_lt_of_le i_new_lt_i_univ' (Nat.le_pred_of_lt i_univ_in_range) + + let i_new' : Fin (list'.length - 1) := ⟨i_new, i_new_lt_i_univ_pred⟩ + let i_new'_pred : Fin (list'.length - 1) := ⟨i_new - 1, Nat.lt_of_le_of_lt (Nat.pred_le i_new) i_new_lt_i_univ_pred⟩ + + have ind_present : Fintype.card (MaxChainThrough ℬ') = ∏ j : Fin (list'.length - 1), (#list'[j.val + 1] - #list'[j.val])! := + ih ℬ'card a_property₁.right.left empty_in_chain' univ_in_chain' list' list_per'.symm list_sorted' + + have product_split : ∏ j : Fin (list'.length - 1), (#list'[j.val + 1] - #list'[j.val])! = + (#list'[i_new'.val + 1] - #list'[i_new'.val])! * ∏ j ∈ univ \ {i_new'}, (#list'[j.val + 1] - #list'[j.val])! := + prod_eq_mul_prod_diff_singleton (by simp) (fun (i : Fin (list'.length - 1)) ↦ (#list'[i.val + 1] - #list'[i.val])!) + + rw [ind_present, product_split] + + have prod_identity : ∏ j ∈ (univ : Finset (Fin (list'.length - 1))) \ {i_new'}, (#list'[j.val + 1] - #list'[j.val])! = ∏ j ∈ 𝒬', multiplicant j := by + calc + ∏ j ∈ (univ : Finset (Fin (list'.length - 1))) \ {i_new'}, (#list'[j.val + 1] - #list'[j.val])! + = (#list'[i_new'_pred.val + 1] - #list'[i_new'_pred.val])! * ∏ j ∈ ((univ : Finset (Fin (list'.length - 1))) \ {i_new'}) \ {i_new'_pred}, (#list'[j.val + 1] - #list'[j.val])! := by + refine' prod_eq_mul_prod_diff_singleton _ (fun (i : Fin (list'.length - 1)) ↦ (#list'[i.val + 1] - #list'[i.val])!) + apply mem_sdiff.mpr + constructor + · simp + · unfold i_new'_pred i_new' + simp + apply sub_one_ne_self + + have list_first_entry : list'[0] = ∅ := first_entry list' list_sorted' list_per'.symm empty_in_chain' + + by_contra ass + + simp [←ass, h_i_new] at list_first_entry + unfold e_new at list_first_entry + + have := nonempty_iff_ne_empty.mp (insert_nonempty a.val layer_s) + + exact this list_first_entry + + _ = 1 * ∏ j ∈ ((univ : Finset (Fin (list'.length - 1))) \ {i_new'}) \ {i_new'_pred}, (#list'[j.val + 1] - #list'[j.val])! := by + congr + sorry + sorry + sorry + --have mul_identity : multiplicant' i_s = (#list'[↑i_new' + 1] - #list'[↑i_new'])! := by sorry + + have : extension_candidates ≠ ∅ := by + by_contra! ass + have equality : #extension_candidates = 0 := by simp [ass] + rw [extension_candidates_card] at equality + + have : #list[i_s.val + 1] = #list[i_s.val] := by sorry + have inequality := (pairwise_iff_getElem.mp list_sorted) i_s.val (i_s.val + 1) i_s_in_range i_s_succ_in_range (Nat.lt_succ_self i_s.val) + linarith + + have central_identity := central_identity layer_s (mem_toFinset.mp layer_s_mem_card.left) (by sorry) + + have := card_image_of_injective (univ : Finset (MaxChainThrough ℬ)) inj_emb_MaxChainThrough + + rw [Fintype.card, ←this, central_identity, card_disjiUnion] + + calc + ∑ a ∈ extension_candidates, #(extensions_wrt a) = + ∑ a ∈ extension_candidates, (multiplicant' i_s) * ∏ j ∈ 𝒬', (multiplicant j) := by + apply sum_congr (by simp) + intro x hx + exact card_extensions_wrt ⟨x, hx⟩ + _ = (multiplicant i_s) * ∏ j ∈ 𝒬', (multiplicant j) := by + simp [sum_const, extension_candidates_card, multiplicant'] + rw [←mul_assoc] + congr + simp [multiplicant] + apply mul_factorial_pred _ + · simp [entry_i_s, entry_i_s_succ, layer_s_mem_card.right.left, layer_t_mem_card.right.left] + have : s'.val < t'.val := by linarith [empty_range.left] + exact this + _ = (multiplicant i_s) * ∏ j ∈ 𝒬', (multiplicant j) := by simp + _ = ∏ j ∈ 𝒬, (multiplicant j) := by + simp [𝒬'] + have : i_s ∈ 𝒬 := by simp [𝒬] + exact (prod_eq_mul_prod_diff_singleton this multiplicant).symm + _ = ∏ j ∈ 𝒬, (#list[j.val + 1] - #list[j.val])! := by + apply prod_congr (by simp) + intro x hx + rfl + + · intro ℬ cardℬ chainℬ empty_in_chain univ_in_chain list list_perm list_sorted + have entry_cards : ∀ j : Fin (list.length - 1), #list[j.val] = j.val := by sorry + have rhs_one := by calc + ∏ j : Fin (list.length - 1), (#list[j.val + 1] - #list[j.val])! = ∏ j : Fin (list.length - 1), 1 := by + apply prod_congr (by simp) + intro j _ + rw [entry_cards, entry_cards ⟨j + 1, by sorry⟩] + simp + _ = 1 := Fintype.prod_eq_one (fun a => 1) (congrFun rfl) + rw [rhs_one, Fintype.card_eq_one_iff] + have ℬmaxChain := (IsMaxChain.iff_card hn chainℬ).mpr cardℬ + use { + 𝒜 := ℬ, + isMaxChain := ℬmaxChain, + subChain := by simp + } + intro X + have same_elements : X.𝒜 = ℬ := (ℬmaxChain.right X.isMaxChain.left X.subChain).symm + rcases X with ⟨X.𝒜, b, c⟩ + simpa + +/- Inserting the empty set into a chain does not change the maximal chains running through. -/ +lemma count_maxChains_through_singleton_insert_empty : Fintype.card (MaxChainThrough ℬ) = Fintype.card (MaxChainThrough (insert ∅ ℬ)) := by sorry + +/- Inserting the universal set into a chain does not change the maximal chains running through. -/ +lemma count_maxChains_through_singleton_insert_univ : Fintype.card (MaxChainThrough ℬ) = Fintype.card (MaxChainThrough (insert univ ℬ)) := by sorry + +/- The count of maximal chains through the empty set is 'n!'. -/ +lemma count_maxChains_through_empty (hn : Fintype.card α = n): Fintype.card (MaxChainThrough {(∅ : Finset α)}) = n! := by sorry + +/- The count of maximal chains through the universal set is 'n!'. -/ +lemma count_maxChains_through_univ (hn : Fintype.card α = n): Fintype.card (MaxChainThrough {(Finset.univ : Finset α)}) = n! := by sorry + +/- The count of maximal chains through a set 'e' is '(n - #e)! * (#e)!'. -/ +lemma count_maxChains_through_singleton (e : Finset α) (hn : Fintype.card α = n): Fintype.card (MaxChainThrough {e}) = (#e)! * (n - #e)! := by + by_cases e_empty : ∅ ≠ e + · by_cases e_univ : univ ≠ e + · let 𝒞 : Set (Finset α) := {∅, univ, e} + have req : #𝒞.toFinset ≤ n + 1 := by sorry + have empty_in_chain : ∅ ∈ 𝒞 := Set.mem_insert ∅ {univ, e} + have univ_in_chain : univ ∈ 𝒞 := by sorry + have chain_singleton : IsChain (· ⊂ ·) 𝒞 := by sorry + + obtain ⟨list, ⟨list_per, list_sorted⟩⟩ := Chain.card_strict_mono chain_singleton + + have := count_maxChainsThrough req hn rfl chain_singleton empty_in_chain univ_in_chain list list_per.symm list_sorted + + rw [count_maxChains_through_singleton_insert_univ, count_maxChains_through_singleton_insert_empty, this] + + have list_length : list.length = 3 := by + calc + list.length = 𝒞.toFinset.toList.length := Perm.length_eq list_per + _ = #𝒞.toFinset := length_toList 𝒞.toFinset + _ = 𝒞.ncard := Eq.symm (ncard_eq_toFinset_card' 𝒞) + _ = 3 := by + refine' ncard_eq_three.mpr _ + use ∅, univ, e + have : ∅ ≠ (univ : Finset α) := by sorry + exact ⟨this, e_empty, e_univ, by simp⟩ + + sorry + · sorry + · sorry + +end MaxChainThrough diff --git a/TheBook/ToMathlib/Antichain.lean b/TheBook/ToMathlib/Antichain.lean new file mode 100644 index 0000000..2ea2c18 --- /dev/null +++ b/TheBook/ToMathlib/Antichain.lean @@ -0,0 +1,37 @@ +import TheBook.Combinatorics.SpernerHelpingDataStructures + +open Function Finset Nat Set BigOperators List + +variable {α : Type*} [Fintype α] {𝒜 : Set (Finset α)} [DecidablePred (· ∈ 𝒜)] [DecidableEq (Set (Finset α))] +instance : Fintype 𝒜 := setFintype 𝒜 + +namespace Finset + +/- The maximal chains through different elements of an antichain are pairwise disjoint. -/ +lemma AntiChain.disj_union_chain_through (anti_chain : IsAntichain (· ⊂ ·) 𝒜) : + 𝒜.PairwiseDisjoint (fun e ↦ ((Finset.univ : Finset (MaxChainThrough {e})).image (emb_MaxChainThrough {e}))) := by + intro e₁ e₁_mem_𝒜 e₂ e₂_mem_𝒜 e₁neqe₂ + simp [onFun] + + refine' disjoint_left.mpr _ + intro C C_mem₁ C_mem₂ + + obtain ⟨C₁, ⟨_, C₁_image⟩⟩ := mem_image.mp C_mem₁ + obtain ⟨C₂, ⟨_, C₂_image⟩⟩ := mem_image.mp C_mem₂ + + have e₁_mem_C₁ := Set.singleton_subset_iff.mp C₁.subChain + have e₂_mem_C₂ := Set.singleton_subset_iff.mp C₂.subChain + unfold emb_MaxChainThrough at C₁_image C₂_image + rw [C₂_image, ←C₁_image] at e₂_mem_C₂ + + have comparable := C₁.isMaxChain.left e₁_mem_C₁ e₂_mem_C₂ e₁neqe₂ + simp at comparable + + have noncomparable₁ := anti_chain e₁_mem_𝒜 e₂_mem_𝒜 e₁neqe₂ + have noncomparable₂ := anti_chain e₂_mem_𝒜 e₁_mem_𝒜 e₁neqe₂.symm + simp at noncomparable₁ + simp at noncomparable₂ + + cases comparable with + | inl h => exact noncomparable₁ h + | inr h => exact noncomparable₂ h diff --git a/TheBook/ToMathlib/Chain.lean b/TheBook/ToMathlib/Chain.lean new file mode 100644 index 0000000..67841b2 --- /dev/null +++ b/TheBook/ToMathlib/Chain.lean @@ -0,0 +1,721 @@ +import TheBook.ToMathlib.List +import TheBook.ToMathlib.Slice +import Mathlib.Data.Finset.Slice +import Mathlib.Data.Fintype.Basic +import Init.Core + +/-! +# Chain + +In this file we introduce introduce Lemmata for chains with respect to the subset relation. +First we consider finite chains of sets in general. Then we consider chains of sets containing elements of some 'Fintype α'. + +This module is organized into the sections 'ChainCoercions', 'ChainSubset', 'ChainExtension', 'ChainSubsetFintype' and 'ChainCardinalityOrder'. + +## Main results + +- `IsChain.equivalence_subset_relations`: A set of sets is a chain with respect to the proper subset relation if and only if it is a chain with respect to the subset relation. +- `IsChain.max_one_elt_chain_layer`: In a finite chain each slice (layer) contains at most one element. +- `IsChain.ssubset_of_lt_cardinality`: A strong inequality of the cardinality of two chain elements implies a proper subset relation. +- `IsChain.subset_of_le_cardinality`: A weak inequality of the cardinality of two chain elements implies a subset relation. +- `extension_candidates_characterisation`: Given two sets 'layer_i' and 'layer_j' in a chain such that there is no set of intermediate cardinality and '#layer_j ≥ #layer_i + 2', the extension candidates for 'layer_i' are given by 'layer_j \ layer_i'. +- `Chain.empty_layer_by_card`: Any chain of sets of 'Fintype α' that contains less than 'Fintype.card α' sets, contains an empty slice. +- `Chain.empty_layer_by_card`: In a maximal chain every slice contains exactly one element. +- `IsMaxChain.card`: The cardinality of a maximal chain of sets of some 'Fintpype α' is 'Fintype.card α + 1'. +- `IsChain.card_le`: The cardinality of a chain of sets of some 'Fintpype α' is at most 'Fintype.card α + 1'. +- `IsMaxChain.iff_card`: A chain of sets of some 'Fintpype α' is maximal if and only if it contains 'Fintype.card α + 1' sets. +- `Chain.card_strict_mono`: Given a chain of sets of some 'Fintype α' there exists a permutation of the list of its elements, such that its elements cardinalities are sorted by strict inequalities. +-/ + +namespace Finset + +open Function Finset Nat Set BigOperators List + +section ChainCoercions + +/-! +# ChainCoercions + +In this section we introduce coercions such that we can use the 'IsChain' relation together with the coercions 'toSet' and 'toFinset' in a natural way +and use the subset and the proper subset relation interchangably. + +## Main results + +- `IsChain.equivalence_subset_relations`: A set of sets is a chain with respect to the proper subset relation if and only if it is a chain with respect to the subset relation. +-/ + +variable {α : Type*} {𝒜 : Finset (Finset α)} {ℬ : Finset (Set α)} {𝒞 : Set (Finset α)} {𝒟 : Set (Set α)} + +/- A set of sets is a chain with respect to the proper subset relation if and only if it is a chain with respect to the subset relation. -/ +lemma IsChain.equivalence_subset_relations : (IsChain (· ⊆ .) 𝒟) ↔ (IsChain (· ⊂ .) 𝒟) := by + constructor + · intro h e₁ e₁mem e₂ e₂mem e₁neqe₂ + cases h e₁mem e₂mem e₁neqe₂ with + | inl e₁sube₂ => left; exact Set.ssubset_iff_subset_ne.mpr ⟨e₁sube₂, e₁neqe₂⟩ + | inr e₂sube₁ => right; exact Set.ssubset_iff_subset_ne.mpr ⟨e₂sube₁, e₁neqe₂.symm⟩ + · intro h e₁ e₁mem e₂ e₂mem e₁neqe₂ + cases h e₁mem e₂mem e₁neqe₂ with + | inl e₁sube₂ => left; exact e₁sube₂.left + | inr e₂sube₁ => right; exact e₂sube₁.left + +/- A set of sets is a maximal chain with respect to the proper subset relation if and only if it is a chain with respect to the subset relation. -/ +lemma IsMaxChain.equivalence_subset_relations : (IsMaxChain (· ⊆ .) 𝒟) ↔ (IsMaxChain (· ⊂ .) 𝒟) := by + constructor + · intro h + exact ⟨IsChain.equivalence_subset_relations.mp h.left, fun t chain => h.right (IsChain.equivalence_subset_relations.mpr chain)⟩ + · intro h + exact ⟨IsChain.equivalence_subset_relations.mpr h.left, fun t chain => h.right (IsChain.equivalence_subset_relations.mp chain)⟩ + +instance : Coe (IsChain (· ⊆ ·) 𝒟) (IsChain (· ⊂ ·) 𝒟) := ⟨fun h => IsChain.equivalence_subset_relations.mp h⟩ +instance : Coe (IsChain (· ⊂ ·) 𝒟) (IsChain (· ⊆ ·) 𝒟) := ⟨fun h => IsChain.equivalence_subset_relations.mpr h⟩ + +/- A set of sets is a chain if the set of the corresponding finite sets is a chain (with respect to the proper subset relation). -/ +instance : Coe (IsChain (· ⊂ ·) 𝒞) (IsChain (· ⊂ ·) (toSet '' 𝒞)) := ⟨ by + intro h + intro x hx y hy x_neg_y + obtain ⟨x', hx'⟩ := hx + obtain ⟨y', hy'⟩ := hy + have x'_neg_y' : x' ≠ y' := by + by_contra ass + rw [ass] at hx' + rw [←hx'.right, hy'.right] at x_neg_y + simp at x_neg_y + + simp [←hx'.right, ←hy'.right] + exact h hx'.left hy'.left x'_neg_y' +⟩ + +/- A set of sets is a chain if the set of the corresponding finite sets is a chain (with respect to the subset relation). -/ +instance : Coe (IsChain (· ⊆ ·) 𝒞) (IsChain (· ⊆ ·) (toSet '' 𝒞)) := ⟨ by + intro h + intro x hx y hy x_neg_y + obtain ⟨x', hx'⟩ := hx + obtain ⟨y', hy'⟩ := hy + have x'_neg_y' : x' ≠ y' := by + by_contra ass + rw [ass] at hx' + rw [←hx'.right, hy'.right] at x_neg_y + simp at x_neg_y + + simp [←hx'.right, ←hy'.right] + exact h hx'.left hy'.left x'_neg_y' +⟩ + +/- A set of finite sets is a chain if the set of the corresponding sets is a chain (with respect to the proper subset relation). -/ +instance : Coe (IsChain (· ⊂ ·) (toSet '' 𝒞)) (IsChain (· ⊂ ·) 𝒞) := + ⟨fun h _ hx _ hy x_neg_y ↦ h (Set.mem_image_of_mem toSet hx) (Set.mem_image_of_mem toSet hy) (fun ass ↦ x_neg_y (coe_inj.mp ass))⟩ + +/- A set of finite sets is a chain if the set of the corresponding sets is a chain (with respect to the subset relation). -/ +instance : Coe (IsChain (· ⊆ ·) (toSet '' 𝒞)) (IsChain (· ⊆ ·) 𝒞) := + ⟨fun h _ hx _ hy x_neg_y ↦ h (Set.mem_image_of_mem toSet hx) (Set.mem_image_of_mem toSet hy) (fun ass ↦ x_neg_y (coe_inj.mp ass))⟩ + +/- Now we can write the following examples without coercion errors. -/ +example (h : IsChain (· ⊂ ·) 𝒞) : (IsChain (· ⊆ ·) (toSet '' 𝒞)) := h +example (h : IsChain (· ⊂ ·) (toSet '' 𝒞)) : (IsChain (· ⊆ ·) 𝒞) := h + +/- Considering the next two examples we might want to have also a coercion from 'IsChain (· ⊂ ·) 𝒞' to 'IsChain (· ⊂ ·) 𝒞.toFinset.toSet', but we do not need it. -/ +example [Fintype 𝒞] (h : IsChain (· ⊂ ·) 𝒞) : (IsChain (· ⊆ ·) 𝒞.toFinset.toSet) := by simp; exact (h : IsChain (· ⊆ ·) 𝒞) +example [Fintype 𝒟] (h : IsChain (· ⊆ ·) 𝒟) : (IsChain (· ⊂ ·) 𝒟.toFinset.toSet) := by simp; exact (h : IsChain (· ⊂ ·) 𝒟) + +/- For completion consider also the following examples. -/ +example (h : IsChain (· ⊂ ·) 𝒜.toSet) : (IsChain (· ⊆ ·) 𝒜.toSet) := h +example (h : IsChain (· ⊂ ·) ℬ.toSet) : (IsChain (· ⊆ ·) ℬ.toSet) := h +example (h : IsChain (· ⊆ ·) 𝒜.toSet) : (IsChain (· ⊂ ·) 𝒜.toSet) := h +example (h : IsChain (· ⊆ ·) ℬ.toSet) : (IsChain (· ⊂ ·) ℬ.toSet) := h +example (h : IsChain (· ⊂ ·) 𝒜.toSet) : (IsChain (· ⊆ ·) (toSet '' 𝒜.toSet)) := h + +/- A general observation. -/ +example : IsTrans 𝒟 (fun (e₁ e₂ : 𝒟) ↦ e₁.val ⊆ e₂.val) := by apply IsTrans.swap + +end ChainCoercions + + +section ChainSubset + +/-! +# ChainSubset + +In this section we consider Lemmata on general chains with respect to the subset relation + +## Main results + +- `IsChain.max_one_elt_chain_layer`: In a finite chain each slice (layer) contains at most one element. +- `IsChain.ssubset_of_lt_cardinality`: A strong inequality of the cardinality of two chain elements implies a proper subset relation. +- `IsChain.subset_of_le_cardinality`: A weak inequality of the cardinality of two chain elements implies a subset relation. +-/ + +variable {α : Type*} {𝒞 : Set (Finset α)} {𝒟 : Set (Set α)} + +/- Two elements in a chain of equal cardinality must be equal. -/ +lemma IsChain.unique_of_cardinality_chain (chain𝒞 : IsChain (· ⊂ ·) 𝒞) {a b : Finset α} + (amem : a ∈ 𝒞) (bmem : b ∈ 𝒞) (hcard : #a = #b) : a = b := by + by_contra aneb + cases chain𝒞 amem bmem aneb with + | inl h => + have := Finset.card_strictMono h + linarith + | inr h => + have := Finset.card_strictMono h + linarith + +/- In a finite chain each slice (layer) contains at most one element. -/ +lemma IsChain.max_one_elt_chain_layer [Fintype 𝒞] (chain𝒞 : IsChain (· ⊂ ·) 𝒞) (j : ℕ) : #(𝒞.toFinset # j) ≤ 1 := by + by_contra! ass + have : (𝒞.toFinset # j) ≠ (∅ : Finset (Finset α)) := by + intro assempty + have := Finset.card_eq_zero.mpr assempty + linarith + obtain ⟨a, amem⟩ := Finset.nonempty_iff_ne_empty.mpr this + obtain ⟨b, ⟨bmem, aneb⟩⟩ := Finset.exists_mem_ne ass a + have cardeqab : #a = #b := by rw [(Finset.mem_slice.mp amem).right, (Finset.mem_slice.mp bmem).right] + have := Finset.slice_subset (bmem) + exact aneb (IsChain.unique_of_cardinality_chain chain𝒞 (mem_toFinset.mp (Finset.slice_subset bmem)) (mem_toFinset.mp (Finset.slice_subset amem)) cardeqab.symm) + +/- In a finite chain a non-empty layer is a singleton. -/ +lemma Chain.layer_singleton_of_nonempty [Fintype 𝒞] (chain𝒞 : IsChain (· ⊂ ·) 𝒞) (j : Finset.range (n + 1)) (layer_nonempty : (𝒞.toFinset # j) ≠ ∅): + ∃! e : Finset α, 𝒞.toFinset # j = {e} := by + have : # (𝒞.toFinset # j) = 1 := by + cases Nat.le_one_iff_eq_zero_or_eq_one.mp (IsChain.max_one_elt_chain_layer chain𝒞 j) with + | inl card_zero => + simp at card_zero + exact False.elim (layer_nonempty card_zero) + | inr card_one => exact card_one + obtain ⟨e, he⟩ := Finset.card_eq_one.mp this + have unique : ∀ a : Finset α, 𝒞.toFinset # j = {a} → a = e := by + intro a ha + rw [he] at ha + simp at ha + exact ha.symm + + exact ⟨e, he, unique⟩ + +/- A strong inequality of the cardinality of two chain elements implies a proper subset relation. -/ +lemma IsChain.ssubset_of_lt_cardinality (chain𝒞 : IsChain (· ⊂ ·) 𝒞) {e₁ e₂ : Finset α} (e₁mem : e₁ ∈ 𝒞) (e₂mem : e₂ ∈ 𝒞) + (hcard : #e₁ < #e₂) : e₁ ⊂ e₂ := by + have e₁nee₂ : e₁ ≠ e₂ := by + intro ass + have : #e₁ = #e₂ := by rw [ass] + linarith + cases chain𝒞 e₁mem e₂mem e₁nee₂ with + | inl h => exact Finset.ssubset_iff_subset_ne.mpr ⟨h.left, e₁nee₂⟩ + | inr h => + have : #e₂ < #e₁ := Finset.card_strictMono h + linarith + +/- A weak inequality of the cardinality of two chain elements implies a subset relation. -/ +lemma IsChain.subset_of_le_cardinality (chain𝒞 : IsChain (· ⊂ ·) 𝒞) {e₁ e₂ : Finset α} (e₁mem : e₁ ∈ 𝒞) (e₂mem : e₂ ∈ 𝒞) + (hcard : #e₁ ≤ #e₂) : e₁ ⊆ e₂ := by + cases Nat.eq_or_lt_of_le hcard with + | inr hcard_lt => + exact (IsChain.ssubset_of_lt_cardinality chain𝒞 e₁mem e₂mem hcard_lt).left + | inl hcard_eq => + exact Finset.subset_of_eq (IsChain.unique_of_cardinality_chain chain𝒞 e₁mem e₂mem hcard_eq) + +end ChainSubset + + +section ChainExtension + +/-! +# ChainExtension + +In this section we consider Lemmata on the extension of chains of sets containing a Fintype. + +## Main results + +- `extension_candidates_characterisation`: Given two sets 'layer_i' and 'layer_j' in a chain such that there is no set of intermediate cardinality and '#layer_j ≥ #layer_i + 2', the extension candidates for 'layer_i' are given by 'layer_j \ layer_i'. +-/ + +variable {α : Type*} [DecidableEq α] [Fintype α] {𝒜 : Set (Finset α)} [DecidablePred (· ∈ 𝒜)] +instance : Fintype 𝒜 := setFintype 𝒜 + +def extends_chain (ℬ : Set (Finset α)) : Finset α → Prop := + fun e ↦ (IsChain (· ⊂ ·) (insert e ℬ)) ∧ e ∉ ℬ + +/- In order to count maximal chains through a chain, we are interested in the following way of chain extension-/ +def insert_extends_chain (ℬ : Set (Finset α)) (e : Finset α) : α → Prop := + fun a : α ↦ extends_chain ℬ (insert a e) + --fun a : α ↦ IsChain (· ⊂ ·) (insert (insert a e) ℬ) ∧ insert a e ∉ ℬ + +instance instDecidableIsChain : Decidable (IsChain (· ⊂ ·) 𝒜) := by + sorry --apply Finset.decidableDforallFinset + +instance instDecidablePredChainExtension (e : Finset α) : + DecidablePred (insert_extends_chain 𝒜 e) := + fun a : α => by sorry --inferInstanceAs (Decidable (IsChain (· ⊂ ·) (insert (insert a e) 𝒜).toSet ∧ insert a e ∉ 𝒜)) + +def extension_candidates (ℬ : Set (Finset α)) (e : Finset α) := Finset.filter (insert_extends_chain ℬ e) (Finset.univ : Finset α) + +/- Given two sets 'layer_i' and 'layer_j' in a chain such that there is no set of intermediate cardinality and '#layer_j ≥ #layer_i + 2', the extension candidates for 'layer_i' are given by 'layer_j \ layer_i'. -/ +theorem extension_candidates_characterisation {i j : Finset.range (n + 1)} (hn : Fintype.card α = n) (ilej_succ_succ : (i : ℕ) + 2 ≤ (j : ℕ)) (chain𝒜 : IsChain (· ⊂ ·) 𝒜) + (hi : (𝒜.toFinset # i) = {layer_i}) (hj : (𝒜.toFinset # j) = {layer_j}) (emptylayer : ∀ l ∈ (Finset.range (n + 1)), i < l → l < j → #(𝒜.toFinset # l) = 0): + extension_candidates 𝒜 layer_i = layer_j \ layer_i := by + unfold extension_candidates + + have layer_j_mem_card := Slice.singleton_explicit.mp hj + have layer_i_mem_card := Slice.singleton_explicit.mp hi + + ext x + let e_new := insert x layer_i + have he_new : e_new = insert x layer_i := rfl + + have e_new_card_lt_layer_j_card: #e_new < #layer_j := by + rw [layer_j_mem_card.right.left] + have : #e_new ≤ #layer_i + 1 := by + simp only [e_new] + exact Finset.card_insert_le x layer_i + rw [layer_i_mem_card.right.left] at this + apply Nat.lt_of_le_of_lt this + exact Nat.succ_le_of_lt ilej_succ_succ + + constructor + · intro hx + simp only [mem_filter, insert_extends_chain, ←he_new] at hx + have hx := hx.right + + have e_new_neq_layer_j : e_new ≠ layer_j := by + intro ass + have := mem_toFinset.mp layer_j_mem_card.left + rw [←ass] at this + exact hx.right this + simp + constructor + · have e_new_mem : e_new ∈ insert e_new 𝒜 := by simp + have layer_j_mem_insert : layer_j ∈ insert e_new 𝒜 := by + simp + right + exact Set.mem_toFinset.mp (layer_j_mem_card.left) + have e_new_sub_layer_j := IsChain.subset_of_le_cardinality hx.left e_new_mem (layer_j_mem_insert) (Nat.le_of_lt e_new_card_lt_layer_j_card) + rw [he_new] at e_new_sub_layer_j + exact e_new_sub_layer_j (mem_insert_self x layer_i) + · intro x_mem_layer_i + have := mem_toFinset.mp layer_i_mem_card.left + rw [←(Finset.insert_eq_self.mpr x_mem_layer_i)] at this + exact hx.right this + · intro hx + simp at hx + simp [insert_extends_chain] + + have case_helper {e₁ e₂ : Finset α} (e₁neqe₂ : e₁ ≠ e₂) (e₂_not_new : e₂ ∈ 𝒜) (e₁_new : e₁ = e_new) : e₁ ⊂ e₂ ∨ e₂ ⊂ e₁ := by + have := chain𝒜 (mem_toFinset.mp layer_i_mem_card.left) e₂_not_new + by_cases h : layer_i = e₂ + · right + rw [←h, e₁_new, he_new] + apply Finset.ssubset_iff_subset_ne.mpr + constructor + · simp + · exact (Finset.insert_ne_self.mpr hx.right).symm + · cases chain𝒜 e₂_not_new (mem_toFinset.mp layer_i_mem_card.left) (fun q => h q.symm) with + | inl e₂_sub_layer_i => + right + simp at e₂_sub_layer_i + rw [e₁_new, he_new] + refine' Finset.ssubset_of_ssubset_of_subset e₂_sub_layer_i _ + apply Finset.subset_insert + | inr layer_i_sub_e₂ => + simp at layer_i_sub_e₂ + left + by_contra e₂_sub_e₁ + + have e₁_sub_e₂ : e₁ ⊆ e₂ := by + rw [e₁_new, he_new] + have layer_j_card_le_e₂_card : #layer_j ≤ #e₂ := by + rw [layer_j_mem_card.right.left] + by_contra! + have e₂_card_gt_i : #e₂ > ↑i := by + rw [←layer_i_mem_card.right.left] + exact Finset.card_strictMono layer_i_sub_e₂ + have e₂_card_lt_n_succ : #e₂ < n + 1 := by + apply Nat.lt_succ_of_le + rw [←hn] + apply Finset.card_le_univ + have e₂_empty_layer := emptylayer #e₂ (by simp; exact e₂_card_lt_n_succ) e₂_card_gt_i this + simp at e₂_empty_layer + have : e₂ ∈ 𝒜.toFinset # #e₂ := by simpa [slice] + simp [e₂_empty_layer] at this + + have layer_j_sub_e₂ := IsChain.subset_of_le_cardinality chain𝒜 (mem_toFinset.mp layer_j_mem_card.left) e₂_not_new layer_j_card_le_e₂_card + + apply Finset.insert_subset + · exact layer_j_sub_e₂ hx.left + · have : #layer_i ≤ #e₂ := by + rw [layer_i_mem_card.right.left] + rw [layer_j_mem_card.right.left] at layer_j_card_le_e₂_card + exact Nat.le_trans (Nat.le_of_lt (Nat.lt_of_succ_lt ilej_succ_succ)) layer_j_card_le_e₂_card + + exact IsChain.subset_of_le_cardinality chain𝒜 (mem_toFinset.mp layer_i_mem_card.left) e₂_not_new this + + have : ¬(e₁ ⊆ e₂ ∧ e₁ ≠ e₂) := fun q => e₂_sub_e₁ (Finset.ssubset_iff_subset_ne.mpr q) + simp at this + exact e₁neqe₂ (this e₁_sub_e₂) + + constructor + · intro e₁ e₁mem e₂ e₂mem e₁neqe₂ + simp [←he_new] at e₁mem e₂mem + simp + cases e₁mem with + | inl e₁_new => + cases e₂mem with + | inl e₂_new => + rw [←e₂_new] at e₁_new + left + exact Finset.ssubset_iff_subset_ne.mpr ⟨Finset.subset_of_eq e₁_new, e₁neqe₂⟩ + | inr e₂_not_new => + exact case_helper e₁neqe₂ e₂_not_new e₁_new + | inr e₁_not_new => + cases e₂mem with + | inl e₂_new => + apply Or.symm + exact case_helper e₁neqe₂.symm e₁_not_new e₂_new + | inr e₂_not_new => + exact chain𝒜 e₁_not_new e₂_not_new e₁neqe₂ + + · intro e_new_mem_𝒜 + have e_new_card_gt_layer_i : #e_new > i := by simp [Finset.card_insert_of_not_mem hx.right, layer_i_mem_card.right.left] + + rw [layer_j_mem_card.right.left] at e_new_card_lt_layer_j_card + have : #(𝒜.toFinset # #e_new) = 0 := by + refine' emptylayer #e_new _ e_new_card_gt_layer_i e_new_card_lt_layer_j_card + · simp + exact Nat.lt_trans e_new_card_lt_layer_j_card (mem_range.mp j.property) + have : (𝒜.toFinset # #e_new).Nonempty := by + have : e_new ∈ 𝒜.toFinset # #e_new := by simpa [slice] + exact nonempty_of_mem this + have : #(𝒜.toFinset # #e_new) > 0 := Finset.card_pos.mpr this + linarith + +/- For any finite set 'e' in a chain with nonempty extension candidates, we know that 'e' is not 'univ' and the slice of the chain above 'e' is empty. -/ +lemma extension_candidates_nonempty {e : Finset α} (hn : Fintype.card α = n) (h : extension_candidates 𝒜 e ≠ ∅) : #e < n ∧ (𝒜.toFinset # (#e + 1)) = ∅ := by + by_contra! ass₀ + apply h + have : (𝒜.toFinset # (#e + 1)) ≠ ∅ ∨ #e ≥ n := by + by_cases h : #e < n + · exact Or.inl (ass₀ h) + · exact Or.inr (Nat.ge_of_not_lt h) + + cases this with + | inl next_ne_empty => + by_contra! ass₁ + obtain ⟨a, ha⟩ := nonempty_of_ne_empty ass₁ + simp [extension_candidates, insert_extends_chain] at ha + + obtain ⟨u, hu⟩ := nonempty_of_ne_empty next_ne_empty + simp [slice] at hu + + have insert_a_mem : (insert a e) ∈ insert (insert a e) 𝒜 := Set.mem_insert (insert a e) 𝒜 + have u_mem : u ∈ insert (insert a e) 𝒜 := Set.mem_insert_of_mem (insert a e) hu.left + + have card_eq : #(insert a e) = #u := by sorry + + have := IsChain.unique_of_cardinality_chain ha.left insert_a_mem u_mem card_eq + rw [this] at ha + exact ha.right hu.left + | inr card_ge => + sorry + +end ChainExtension + +section ChainSubsetFintype + +/-! +# ChainSubsetFintype + +Here we proof Lemmata on the poset of the subset relation on sets containing elements of a 'Fintype'. + +## Main results + +- `Chain.empty_layer_by_card`: Any chain of sets of 'Fintype α' that contains less than 'Fintype.card α' sets, contains an empty slice. +- `Chain.empty_layer_by_card`: In a maximal chain every slice contains exactly one element. +- `IsMaxChain.card`: The cardinality of a maximal chain of sets of some 'Fintpype α' is 'Fintype.card α + 1'. +- `IsChain.card_le`: The cardinality of a chain of sets of some 'Fintpype α' is at most 'Fintype.card α + 1'. +- `IsMaxChain.iff_card`: A chain of sets of some 'Fintpype α' is maximal if and only if it contains 'Fintype.card α + 1' sets. +-/ + +variable {α : Type*} [Fintype α] {𝒜 : Set (Finset α)} [DecidablePred (· ∈ 𝒜)] + +instance : Fintype 𝒜 := setFintype 𝒜 + +/- Any chain of sets of 'Fintype α' that contains less than 'Fintype.card α' sets, contains an empty slice. -/ +lemma Chain.empty_layer_by_card (hn : Fintype.card α = n) (chain𝒜 : IsChain (· ⊂ ·) 𝒜) (card𝒜 : #𝒜.toFinset < n+1) : ∃ i : Fin (n + 1), #(𝒜.toFinset # i) = 0 := by + by_contra! ass + have : ∀ (i : Fin (n + 1)), #(𝒜.toFinset # i) = 1 := by + intro i + have non_zero := ass i + cases Nat.le_one_iff_eq_zero_or_eq_one.mp (IsChain.max_one_elt_chain_layer chain𝒜 i) with + | inl h => exfalso; exact (non_zero h) + | inr h => exact h + rw [←sum_card_slice 𝒜.toFinset] at card𝒜 + have := calc + ∑ r ∈ Iic (Fintype.card α), #(𝒜.toFinset # r) = ∑ r ∈ Iic (Fintype.card α), 1 := by + apply Finset.sum_congr (by rfl) + intro j jmem + simp [hn] at jmem + exact this ⟨j, by simp [Nat.lt_succ_of_le jmem]⟩ + _ = n + 1 := by rw [←(Finset.card_eq_sum_ones (Iic (Fintype.card α)))]; simp [hn] + linarith + +/- In a maximal chain every slice contains exactly one element. -/ +lemma IsMaxChain.one_elt_max_chain_layer [DecidableEq α] (hn : Fintype.card α = n) (maxchain𝒜 : IsMaxChain (· ⊂ ·) 𝒜) + (j : Finset.range (n + 1)) : #(𝒜.toFinset # j) = 1 := by + by_contra! ass + have empty_layer : 𝒜.toFinset # j = ∅ := by + cases Nat.le_one_iff_eq_zero_or_eq_one.mp (IsChain.max_one_elt_chain_layer maxchain𝒜.left j) with + | inl h => simp at h; exact h + | inr h => omega + + if htop : ∀ i : Finset.range (n + 1), i > j → 𝒜.toFinset # i = ∅ then + have univnotin𝒜 : (Finset.univ : Finset α) ∉ 𝒜 := by + intro ass₂ + have nslicemem : (Finset.univ : Finset α) ∈ 𝒜.toFinset # n := by + simp [Finset.slice] + exact ⟨ass₂, hn⟩ + cases Nat.lt_or_ge j n with + | inl jltn => + have nsliceempty : 𝒜.toFinset # n = ∅ := htop ⟨n, Finset.mem_range.mpr (Nat.lt_succ_self n)⟩ jltn + simp [nsliceempty] at nslicemem + | inr jgen => + have jeqn : j = n := Nat.eq_of_le_of_lt_succ jgen (Finset.mem_range.1 (by simp)) + rw [jeqn] at empty_layer + simp [empty_layer] at nslicemem + simp [IsMaxChain] at maxchain𝒜 + + have larger_chain_with_univ' : _root_.IsChain (· ⊂ ·) (Insert.insert (Finset.univ : Finset α) 𝒜) := by + refine' IsChain.insert maxchain𝒜.left _ + intro b bmem bneq + right + exact Finset.ssubset_iff_subset_ne.mpr ⟨by simp, fun h => bneq h.symm⟩ + + have larger_chain_with_univ : IsChain (· ⊂ ·) ((Insert.insert (Finset.univ : Finset α) 𝒜)) := larger_chain_with_univ' + + have univin𝒜 := Set.insert_eq_self.mp (maxchain𝒜.right larger_chain_with_univ (by simp)).symm + exact univnotin𝒜 univin𝒜 + else if hbottom : ∀ i : Finset.range (n + 1), i < j → 𝒜.toFinset # i = ∅ then + have emptynotin𝒜 : (∅ : Finset α) ∉ 𝒜 := by + intro ass₃ + have zeroslicemem : (∅ : Finset α) ∈ 𝒜.toFinset # 0 := by + simp [Finset.slice] + exact ass₃ + cases Nat.eq_zero_or_pos j with + | inl jeqzero => + rw [jeqzero] at empty_layer + simp [empty_layer] at zeroslicemem + | inr jgen => + simp [hbottom ⟨0, by simp⟩ jgen] at zeroslicemem + simp [IsMaxChain] at maxchain𝒜 + have larger_chain_with_empty' : _root_.IsChain (· ⊂ ·) (Insert.insert (∅ : Finset α) 𝒜) := by + have : (Insert.insert (∅ : Finset α) 𝒜) = Insert.insert (∅ : Finset α) 𝒜 := by simp + rw [this] + refine' IsChain.insert maxchain𝒜.left _ + intro b bmem bneq + left + exact Finset.ssubset_iff_subset_ne.mpr ⟨by simp, bneq⟩ + + have larger_chain_with_empty : IsChain (· ⊂ ·) (Insert.insert (∅ : Finset α) 𝒜) := larger_chain_with_empty' + + have emptyin𝒜 := Set.insert_eq_self.mp (maxchain𝒜.right larger_chain_with_empty (by simp)).symm + exact emptynotin𝒜 emptyin𝒜 + + else + simp at htop hbottom + let indices_nonempty_top := Finset.filter (fun i : Finset.range (n + 1) ↦ i > j ∧ 𝒜.toFinset # i ≠ ∅) (Finset.univ : Finset (Finset.range (n + 1))) + let indices_nonempty_bottom := Finset.filter (fun i : Finset.range (n + 1) ↦ i < j ∧ 𝒜.toFinset # i ≠ ∅) (Finset.univ : Finset (Finset.range (n + 1))) + have nonempty_indices_nonempty_top : indices_nonempty_top.Nonempty := by + simp [Finset.Nonempty] + obtain ⟨i, ⟨⟨ilen, jlti⟩, jlayernotempty⟩⟩ := htop + use i + simp [indices_nonempty_top] + constructor + · use ilen + · exact jlayernotempty + + have nonempty_indices_nonempty_bottom : indices_nonempty_bottom.Nonempty := by + simp [Finset.Nonempty] + obtain ⟨i, ⟨⟨ilen, iltj⟩, jlayernotempty⟩⟩ := hbottom + use i + simp [indices_nonempty_bottom] + constructor + · use ilen + · exact jlayernotempty + + obtain ⟨s_top, s_top_min⟩ := Finset.min_of_nonempty nonempty_indices_nonempty_top + have h_s_top := Finset.mem_of_min s_top_min + simp [indices_nonempty_top] at h_s_top + + obtain ⟨s_bottom, s_bottom_max⟩ := Finset.max_of_nonempty nonempty_indices_nonempty_bottom + have h_s_bottom := Finset.mem_of_max s_bottom_max + simp [indices_nonempty_bottom] at h_s_bottom + + have emptylayer : ∀ l ∈ (Finset.range (n + 1)), s_bottom < l → l < s_top → #(𝒜.toFinset # l) = 0 := by + intro l lmem s_bottom_lt_l l_lt_s_top + + have h_top : ⟨l, lmem⟩ ∉ indices_nonempty_top := Finset.not_mem_of_lt_min l_lt_s_top s_top_min + have h_bottom : ⟨l, lmem⟩ ∉ indices_nonempty_bottom := Finset.not_mem_of_max_lt s_bottom_lt_l s_bottom_max + + simp [indices_nonempty_top] at h_top + simp [indices_nonempty_bottom] at h_bottom + + simp + + by_cases jeql : j = ⟨l, lmem⟩ + · rw [←empty_layer, jeql] + · cases (Nat.lt_or_gt_of_ne (fun ass : ↑j = l => jeql (by simp [←ass]))) with + | inl jltl => exact h_top jltl + | inr jgtl => exact h_bottom jgtl + + obtain ⟨e_bottom, ⟨bottom_singleton : 𝒜.toFinset # s_bottom = {e_bottom}, _⟩⟩ := Chain.layer_singleton_of_nonempty maxchain𝒜.left s_bottom h_s_bottom.right + + obtain ⟨e_top, ⟨top_singleton : 𝒜.toFinset # s_top = {e_top}, _⟩⟩ := Chain.layer_singleton_of_nonempty maxchain𝒜.left s_top h_s_top.right + + have extension_candidates_eq : extension_candidates 𝒜 e_bottom = e_top \ e_bottom := by + have ilej_succ_succ : (s_bottom : ℕ) + 2 ≤ (s_top : ℕ) := by + apply Nat.succ_le_of_lt + have : (s_bottom : ℕ) + 1 ≤ ↑j := Nat.succ_le_of_lt h_s_bottom.left + exact Nat.lt_of_le_of_lt this h_s_top.left + exact extension_candidates_characterisation hn ilej_succ_succ maxchain𝒜.left bottom_singleton top_singleton emptylayer + + have e_bottom_mem_card : e_bottom ∈ 𝒜 ∧ #e_bottom = s_bottom := by + have := Finset.mem_singleton_self e_bottom + rw [←bottom_singleton] at this + simp [slice] at this + exact this + + have e_top_mem_card : e_top ∈ 𝒜 ∧ #e_top = s_top := by + have := Finset.mem_singleton_self e_top + rw [←top_singleton] at this + simp [slice] at this + exact this + + have extension_candidates_ne_empty : #(extension_candidates 𝒜 e_bottom) > 0 := by + rw [extension_candidates_eq] + have card_bottom_lt_card_top : #e_bottom < #e_top := by + rw [e_top_mem_card.right, e_bottom_mem_card.right] + exact Nat.lt_trans h_s_bottom.left h_s_top.left + have bottom_subset_top : e_bottom ⊂ e_top := + IsChain.ssubset_of_lt_cardinality maxchain𝒜.left e_bottom_mem_card.left e_top_mem_card.left card_bottom_lt_card_top + have := Finset.card_sdiff_add_card_eq_card bottom_subset_top.left + linarith + simp at extension_candidates_ne_empty + obtain ⟨a, ha⟩ := extension_candidates_ne_empty + simp [extension_candidates, insert_extends_chain] at ha + have := Set.insert_eq_self.mp (maxchain𝒜.right ha.left (by simp)).symm + exact ha.right this + +/- The cardinality of a maximal chain of sets of some 'Fintpype α' is 'Fintype.card α + 1'. -/ +lemma IsMaxChain.card [DecidableEq α] (hn : Fintype.card α = n) + (maxChain𝒜 : IsMaxChain (· ⊂ ·) 𝒜) : #𝒜.toFinset = n + 1 := by + rw [←sum_card_slice 𝒜.toFinset] + calc + ∑ r ∈ Iic (Fintype.card α), #(𝒜.toFinset # r) = ∑ r ∈ Iic (Fintype.card α), 1 := by + apply Finset.sum_congr (by rfl) + intro j jmem + simp [hn] at jmem + exact IsMaxChain.one_elt_max_chain_layer hn maxChain𝒜 ⟨j, by simp [Nat.lt_succ_of_le jmem]⟩ + _ = n + 1 := by rw [←(Finset.card_eq_sum_ones (Iic (Fintype.card α)))]; simp [hn] + +/- The cardinality of a chain of sets of some 'Fintpype α' is at most 'Fintype.card α + 1'. -/ +lemma IsChain.card_le (hn : Fintype.card α = n) (chain𝒜 : IsChain (· ⊂ ·) 𝒜) : #𝒜.toFinset ≤ n + 1 := by + rw [←sum_card_slice 𝒜.toFinset] + calc + ∑ r ∈ Iic (Fintype.card α), #(𝒜.toFinset # r) ≤ ∑ r ∈ Iic (Fintype.card α), 1 := by + apply sum_le_sum + intro j jmem + exact IsChain.max_one_elt_chain_layer chain𝒜 j + _ = n + 1 := by rw [←(Finset.card_eq_sum_ones (Iic (Fintype.card α)))]; simp [hn] + +/- A chain of sets of some 'Fintpype α' is maximal if and only if it contains 'Fintype.card α + 1' sets. -/ +lemma IsMaxChain.iff_card [DecidableEq α] (hn : Fintype.card α = n) + (chain𝒜 : IsChain (· ⊂ ·) 𝒜) : IsMaxChain (· ⊂ ·) 𝒜 ↔ #𝒜.toFinset = n + 1 := by + constructor + · intro maxChain𝒜 + exact IsMaxChain.card hn maxChain𝒜 + · intro card𝒜 + constructor + · exact chain𝒜 + · intro ℬ chainℬ 𝒜ssubℬ + have : DecidablePred (fun e : Finset α ↦ e ∈ ℬ) := by sorry + have := setFintype ℬ + have hcard𝒜 : #ℬ.toFinset ≤ #𝒜.toFinset := by + rw [card𝒜, ←hn] + sorry + exact toFinset_inj.mp ((Finset.subset_iff_eq_of_card_le hcard𝒜).mp (toFinset_subset_toFinset.mpr 𝒜ssubℬ)) + +end ChainSubsetFintype + +section ChainCardinalityOrder + +/-! +# ChainCardinalityOrder + +In this chapter we consider the list of the elements of a finite chain of finite sets with respect to the subset relation. +Further we introduce the total order of the cardinalities of the sets in a chain. + +## Main results + +- `Chain.card_strict_mono`: Given a chain of sets of some 'Fintype α' there exists a permutation of the list of its elements, such that its elements cardinalities are sorted by strict inequalities. +-/ + +variable {α : Type*} {𝒜 : Set (Finset α)} [DecidablePred (· ∈ 𝒜)] [Fintype α] + +instance : Fintype 𝒜 := setFintype 𝒜 + +instance card_le : LE (Finset α) where + le x y := #x ≤ #y + +instance card_lt : LT (Finset α) where + lt x y := #x < #y + +instance card_preorder : Preorder (Finset α) := { + le := (· ≤ ·), + lt := (· < ·), + le_refl := fun x => Nat.le_refl #x, + le_trans := fun _ _ _ hxy hyz => Nat.le_trans hxy hyz, + lt_iff_le_not_le := fun _ _ => Nat.lt_iff_le_not_le +} + +instance card_le_is_total : IsTotal 𝒜 (fun (e₁ e₂ : 𝒜) ↦ e₁.val ≤ e₂.val) := + ⟨fun a b ↦ Nat.le_total #a.val #b.val⟩ + +instance card_le_is_trans : IsTrans 𝒜 (fun (e₁ e₂ : 𝒜) ↦ e₁.val ≤ e₂.val) := + ⟨fun _ _ _ h₁ h₂ ↦ Nat.le_trans h₁ h₂⟩ + +lemma card_strict_mono' (chain𝒜 : IsChain (· ⊂ ·) 𝒜) : ((Finset.univ : Finset 𝒜).toList.insertionSort (fun (e₁ e₂ : 𝒜) ↦ #e₁.val ≤ #e₂.val)).Sorted (fun (e₁ e₂ : 𝒜) ↦ #e₁.val < #e₂.val) := by + apply List.pairwise_iff_get.mpr + intro x y xlty + let elt_x := ((List.insertionSort (fun (e₁ e₂ : 𝒜) => #e₁.val ≤ #e₂.val) univ.toList).get x) + let elt_y := ((List.insertionSort (fun (e₁ e₂ : 𝒜) => #e₁.val ≤ #e₂.val) univ.toList).get y) + have card_le : elt_x.val ≤ elt_y.val := List.pairwise_iff_get.mp (List.sorted_insertionSort (fun (e₁ e₂ : 𝒜) ↦ #e₁.val ≤ #e₂.val) (Finset.univ : Finset 𝒜).toList) x y xlty + by_contra! ass + have card_eq := Nat.le_antisymm card_le ass + + have elt_x_eq_elt_y := Subtype.eq (IsChain.unique_of_cardinality_chain chain𝒜 elt_x.prop elt_y.prop card_eq) + have elt_x_neq_elt_y : elt_x ≠ elt_y := List.pairwise_iff_get.mp (List.Nodup.insertionSort ((Finset.univ : Finset 𝒜).nodup_toList)) x y xlty + + exact elt_x_neq_elt_y elt_x_eq_elt_y + +/- Given a chain of sets of some 'Fintype α' there exists a permutation of the list of its elements, such that its elements cardinalities are sorted by strict inequalities. -/ +theorem Chain.card_strict_mono [DecidableEq α] (chain𝒜 : IsChain (· ⊂ ·) 𝒜) : ∃ l : List (Finset α), l ~ 𝒜.toFinset.toList ∧ l.Sorted (#· < #·) := by + let l' := ((Finset.univ : Finset 𝒜).toList.insertionSort (fun (e₁ e₂ : 𝒜) ↦ #e₁.val ≤ #e₂.val)) + have l'_sorted : l'.Sorted (fun (e₁ e₂ : 𝒜) ↦ #e₁.val < #e₂.val) := card_strict_mono' chain𝒜 + + let l := l'.map Subtype.val + use l + constructor + · calc + l ~ (Finset.univ : Finset 𝒜).toList.map Subtype.val := Perm.map Subtype.val (perm_insertionSort (fun e₁ e₂ => #e₁.val ≤ #e₂.val) (Finset.univ : Finset 𝒜).toList) + _ ~ 𝒜.toFinset.toList := by apply Finset.subtype_toList + · unfold l Sorted + apply List.pairwise_iff_get.mpr + intro i j iltj + simp [List.getElem_map, List.unattach, -List.map_subtype] + + have : (l'.map Subtype.val).length = l'.length := length_map l' Subtype.val + + have iltj_coe : (Fin.cast this i) < (Fin.cast this j) := by + apply Fin.lt_def.mpr + simp + exact iltj + + have := List.pairwise_iff_get.mp l'_sorted (Fin.cast this i) (Fin.cast this j) iltj_coe + exact this + +end ChainCardinalityOrder diff --git a/TheBook/ToMathlib/CliqueNumber.lean b/TheBook/ToMathlib/CliqueNumber.lean index 3874ac8..68ddfb2 100644 --- a/TheBook/ToMathlib/CliqueNumber.lean +++ b/TheBook/ToMathlib/CliqueNumber.lean @@ -44,7 +44,6 @@ lemma maximal_of_maximum (s : Finset α) (M : G.IsMaximumClique s) : G.IsMaximal exact lt_irrefl _ (lt_of_lt_of_le hlt hle) } - variable [Fintype α] private lemma fintype_cliqueNum_bddAbove : BddAbove {n | ∃ s, G.IsNClique n s} := by diff --git a/TheBook/ToMathlib/IndependentSet.lean b/TheBook/ToMathlib/IndependentSet.lean index 2d01ff3..efdede5 100644 --- a/TheBook/ToMathlib/IndependentSet.lean +++ b/TheBook/ToMathlib/IndependentSet.lean @@ -13,8 +13,6 @@ An independent set is a set of vertices that are pairwise nonadjacent. -/ - - open Finset Fintype Function namespace SimpleGraph diff --git a/TheBook/ToMathlib/List.lean b/TheBook/ToMathlib/List.lean new file mode 100644 index 0000000..a09daf6 --- /dev/null +++ b/TheBook/ToMathlib/List.lean @@ -0,0 +1,102 @@ +import Mathlib.Tactic +import Mathlib.Data.List.Perm.Basic + +open Function Finset Nat Set BigOperators List + +/-! +# List + +In this file we introduce `foo` and `bar`, +two main concepts in the theory of xyzzyology. + +## Main results + +- `List.Nodup.orderedInsert`: Inserting a nonpresent element into a list by 'orderedInsert' does not create a list duplicate. +- `List.Nodup.insertionSort`: 'insertionSort' does not create duplicates in lists. +- `Finset.subtype_toList`: Mapping with 'Subtype.val' and the operation 'toList' commute. +-/ + +section Nodup + +variable {α : Type*} (r : α → α → Prop) [LE α] [DecidableRel (fun (x₁ x₂ : α) ↦ x₁ ≤ x₂)] + +/-- Inserting a nonpresent element into a list by 'orderedInsert' does not create a list duplicate. -/ +lemma List.Nodup.orderedInsert + {l : List α} {a : α} (l_nodup : l.Nodup) (a_not_mem : a ∉ l) : + (orderedInsert (· ≤ ·) a l).Nodup := by + induction l with + | nil => + simp [orderedInsert] + | cons x xs ih => + simp [orderedInsert] + simp at a_not_mem + simp at l_nodup + split + · simp [List.Nodup] + constructor + · constructor + · exact a_not_mem.left + · intro u hu + by_contra ass + rw [←ass] at hu + exact a_not_mem.right hu + · constructor + · intro u hu + by_contra ass + rw [←ass] at hu + exact l_nodup.left hu + · exact l_nodup.right + · simp + constructor + · constructor + · exact fun x ↦ a_not_mem.left x.symm + · exact l_nodup.left + · exact ih l_nodup.right a_not_mem.right + +/-- 'insertionSort' does not create duplicates in lists. -/ +theorem List.Nodup.insertionSort {l : List α} (h : l.Nodup) : (l.insertionSort (fun (x₁ x₂ : α) ↦ x₁ ≤ x₂)).Nodup := by + induction l with + | nil => + simp [List.insertionSort, List.Nodup] + | cons x xs ih => + simp [List.insertionSort] + have sorted_nodup : (xs.insertionSort (fun x₁ x₂ => x₁ ≤ x₂)).Nodup := ih h.tail + have x_ne_mem_sorted : x ∉ xs.insertionSort (fun x₁ x₂ => x₁ ≤ x₂) := by + by_contra ass + simp at h + exact h.left ((List.mem_insertionSort (· ≤ ·)).mp ass) + exact List.Nodup.orderedInsert sorted_nodup x_ne_mem_sorted + +end Nodup + + +section Perm + +variable {α : Type*} {𝒜 : Set (Finset α)} [DecidablePred (· ∈ 𝒜)] [Fintype α] [DecidableEq α] + +instance : Fintype 𝒜 := setFintype 𝒜 + +/-- Mapping with 'Subtype.val' and the operation 'toList' commute. -/ +lemma Finset.subtype_toList : List.map Subtype.val (Finset.univ : Finset 𝒜).toList ~ 𝒜.toFinset.toList := by + refine' perm_iff_count.mpr _ + intro a + by_cases h : a ∈ 𝒜.toFinset + case pos => + have count_rhs := nodup_iff_count_eq_one.mp 𝒜.toFinset.nodup_toList a (mem_toList.mpr h) + have count_lhs₀ := count_map_of_injective (Finset.univ : Finset 𝒜).toList Subtype.val Subtype.val_injective ⟨a, mem_toFinset.mp h⟩ + have count_lhs₁ := nodup_iff_count_eq_one.mp (Finset.univ : Finset 𝒜).nodup_toList ⟨a, mem_toFinset.mp h⟩ (mem_toList.mpr (by simp)) + rw [count_rhs, count_lhs₀, count_lhs₁] + case neg => + have count_rhs := List.count_eq_zero_of_not_mem (fun ass ↦ h (mem_toList.mp ass)) + have count_lhs : List.count a (List.map Subtype.val (Finset.univ : Finset 𝒜).toList) = 0 := by + apply List.count_eq_zero_of_not_mem + by_contra! ass + obtain ⟨x, ⟨x_mem_list, x_eq_a⟩⟩ := List.mem_map.mp ass + + have := x.prop + rw [x_eq_a] at this + exact h (mem_toFinset.mpr this) + + rw [count_rhs, count_lhs] + +end Perm diff --git a/TheBook/ToMathlib/Slice.lean b/TheBook/ToMathlib/Slice.lean new file mode 100644 index 0000000..44f2227 --- /dev/null +++ b/TheBook/ToMathlib/Slice.lean @@ -0,0 +1,28 @@ +import Mathlib.Algebra.BigOperators.Group.Finset +import Mathlib.Order.Antichain +import Mathlib.Order.Interval.Finset.Nat +import Mathlib.Data.Finset.Slice + +namespace Slice + +open Finset + +variable {α : Type*} {𝒜 : Finset (Finset α)} {A A₁ A₂ : Finset α} {r r₁ r₂ : ℕ} + +/- Equivalence for a slice to be a singleton. -/ +lemma singleton_explicit : (𝒜 # s) = {layer_s} ↔ layer_s ∈ 𝒜 ∧ #layer_s = s ∧ #(𝒜 # s) = 1 := by + constructor + · intro h + have := Finset.mem_singleton_self layer_s + rw [←h] at this + simp [slice] at this + exact ⟨this.left, this.right, by simp [h]⟩ + · intro h + refine' eq_singleton_iff_unique_mem.mpr _ + constructor + · simp [slice] + constructor + · exact h.left + · exact h.right.left + · intro x hx + sorry diff --git a/TheBook/ToMathlib/fsda.txt b/TheBook/ToMathlib/fsda.txt new file mode 100644 index 0000000..e69de29 diff --git a/elan-init.sh b/elan-init.sh new file mode 100755 index 0000000..d4d978d --- /dev/null +++ b/elan-init.sh @@ -0,0 +1,378 @@ +#!/bin/sh +# Copyright 2016 The Rust Project Developers. See the COPYRIGHT +# file at the top-level directory of this distribution and at +# http://rust-lang.org/COPYRIGHT. +# +# Licensed under the Apache License, Version 2.0 or the MIT license +# , at your +# option. This file may not be copied, modified, or distributed +# except according to those terms. + +# This is just a little script that can be downloaded from the internet to +# install elan. It just does platform detection, downloads the installer +# and runs it. + +set -u + +ELAN_UPDATE_ROOT="https://github.com/leanprover/elan/releases" + +#XXX: If you change anything here, please make the same changes in setup_mode.rs +usage() { + cat 1>&2 < Choose a default toolchain + --default-toolchain none Do not set a default toolchain +EOF +} + +main() { + need_cmd curl + need_cmd awk + need_cmd uname + need_cmd mktemp + need_cmd chmod + need_cmd mkdir + need_cmd rm + need_cmd rmdir + + get_architecture || return 1 + local _arch="$RETVAL" + assert_nz "$_arch" "arch" + + local _ext="" + case "$_arch" in + *windows*) + _ext=".exe" + ;; + esac + + local _dir="$(mktemp -d 2>/dev/null || ensure mktemp -d -t elan)" + local _file="$_dir/elan-init$_ext" + + local _ansi_escapes_are_valid=false + if [ -t 2 ]; then + if [ "${TERM+set}" = 'set' ]; then + case "$TERM" in + xterm*|rxvt*|urxvt*|linux*|vt*) + _ansi_escapes_are_valid=true + ;; + esac + fi + fi + + # check if we have to use /dev/tty to prompt the user + local need_tty=yes + for arg in "$@"; do + case "$arg" in + -h|--help) + usage + exit 0 + ;; + -y) + # user wants to skip the prompt -- we don't need /dev/tty + need_tty=no + ;; + *) + ;; + esac + done + + if $_ansi_escapes_are_valid; then + printf "\33[1minfo:\33[0m downloading installer\n" 1>&2 + else + printf '%s\n' 'info: downloading installer' 1>&2 + fi + + ensure mkdir -p "$_dir" + case "$_arch" in + *windows*) + ensure curl -sSfL "$ELAN_UPDATE_ROOT/latest/download/elan-$_arch.zip" > "$_dir/elan-init.zip" + (cd "$_dir"; ensure unzip elan-init.zip; ignore rm elan-init.zip) + ;; + *) + ensure curl -sSfL "$ELAN_UPDATE_ROOT/latest/download/elan-$_arch.tar.gz" > "$_dir/elan-init.tar.gz" + (cd "$_dir"; ensure tar xf elan-init.tar.gz; ignore rm elan-init.tar.gz) + ;; + esac + + ensure chmod u+x "$_file" + if [ ! -x "$_file" ]; then + printf '%s\n' "Cannot execute $_file (likely because of mounting /tmp as noexec)." 1>&2 + printf '%s\n' "Please copy the file to a location where you can execute binaries and run ./elan-init$_ext." 1>&2 + exit 1 + fi + + + + if [ "$need_tty" = "yes" ]; then + # The installer is going to want to ask for confirmation by + # reading stdin. This script was piped into `sh` though and + # doesn't have stdin to pass to its children. Instead we're going + # to explicitly connect /dev/tty to the installer's stdin. + if [ ! -t 1 ]; then + err "Unable to run interactively. Run with -y to accept defaults, --help for additional options" + fi + + ignore "$_file" "$@" < /dev/tty + else + ignore "$_file" "$@" + fi + + local _retval=$? + + ignore rm "$_file" + ignore rmdir "$_dir" + + return "$_retval" +} + +get_bitness() { + need_cmd head + # Architecture detection without dependencies beyond coreutils. + # ELF files start out "\x7fELF", and the following byte is + # 0x01 for 32-bit and + # 0x02 for 64-bit. + # The printf builtin on some shells like dash only supports octal + # escape sequences, so we use those. + local _current_exe_head=$(head -c 5 /proc/self/exe ) + if [ "$_current_exe_head" = "$(printf '\177ELF\001')" ]; then + echo 32 + elif [ "$_current_exe_head" = "$(printf '\177ELF\002')" ]; then + echo 64 + else + err "unknown platform bitness" + fi +} + +get_endianness() { + local cputype=$1 + local suffix_eb=$2 + local suffix_el=$3 + + # detect endianness without od/hexdump, like get_bitness() does. + need_cmd head + need_cmd tail + + local _current_exe_endianness="$(head -c 6 /proc/self/exe | tail -c 1)" + if [ "$_current_exe_endianness" = "$(printf '\001')" ]; then + echo "${cputype}${suffix_el}" + elif [ "$_current_exe_endianness" = "$(printf '\002')" ]; then + echo "${cputype}${suffix_eb}" + else + err "unknown platform endianness" + fi +} + +get_architecture() { + + local _ostype="$(uname -s)" + local _cputype="$(uname -m)" + + if [ "$_ostype" = Linux ]; then + if [ "$(uname -o)" = Android ]; then + local _ostype=Android + fi + if ldd --version 2>&1 | grep -q 'musl'; then + err "musl-based systems are unsupported at the moment" + fi + fi + + if [ "$_ostype" = Darwin -a "$_cputype" = i386 ]; then + # Darwin `uname -s` lies + if sysctl hw.optional.x86_64 | grep -q ': 1'; then + local _cputype=x86_64 + fi + fi + + case "$_ostype" in + + Android) + local _ostype=linux-android + ;; + + Linux) + local _ostype=unknown-linux-gnu + ;; + + FreeBSD) + local _ostype=unknown-freebsd + ;; + + NetBSD) + local _ostype=unknown-netbsd + ;; + + DragonFly) + local _ostype=unknown-dragonfly + ;; + + Darwin) + local _ostype=apple-darwin + ;; + + MINGW* | MSYS* | CYGWIN*) + local _ostype=pc-windows-msvc + ;; + + *) + err "unrecognized OS type: $_ostype" + ;; + + esac + + case "$_cputype" in + + i386 | i486 | i686 | i786 | x86) + local _cputype=i686 + ;; + + xscale | arm) + local _cputype=arm + if [ "$_ostype" = "linux-android" ]; then + local _ostype=linux-androideabi + fi + ;; + + armv6l) + local _cputype=arm + if [ "$_ostype" = "linux-android" ]; then + local _ostype=linux-androideabi + else + local _ostype="${_ostype}eabihf" + fi + ;; + + armv7l | armv8l) + local _cputype=armv7 + if [ "$_ostype" = "linux-android" ]; then + local _ostype=linux-androideabi + else + local _ostype="${_ostype}eabihf" + fi + ;; + + arm64 | aarch64) + local _cputype=aarch64 + ;; + + x86_64 | x86-64 | x64 | amd64) + local _cputype=x86_64 + ;; + + mips) + local _cputype="$(get_endianness $_cputype "" 'el')" + ;; + + mips64) + local _bitness="$(get_bitness)" + if [ $_bitness = "32" ]; then + if [ $_ostype = "unknown-linux-gnu" ]; then + # 64-bit kernel with 32-bit userland + # endianness suffix is appended later + local _cputype=mips + fi + else + # only n64 ABI is supported for now + local _ostype="${_ostype}abi64" + fi + + local _cputype="$(get_endianness $_cputype "" 'el')" + ;; + + ppc) + local _cputype=powerpc + ;; + + ppc64) + local _cputype=powerpc64 + ;; + + ppc64le) + local _cputype=powerpc64le + ;; + + *) + err "unknown CPU type: $_cputype" + + esac + + # Detect 64-bit linux with 32-bit userland + if [ $_ostype = unknown-linux-gnu -a $_cputype = x86_64 ]; then + if [ "$(get_bitness)" = "32" ]; then + local _cputype=i686 + fi + fi + + # Detect armv7 but without the CPU features Lean needs in that build, + # and fall back to arm. + # See https://github.com/rust-lang-nursery/rustup.rs/issues/587. + if [ $_ostype = "unknown-linux-gnueabihf" -a $_cputype = armv7 ]; then + if ensure grep '^Features' /proc/cpuinfo | grep -q -v neon; then + # At least one processor does not have NEON. + local _cputype=arm + fi + fi + + local _arch="$_cputype-$_ostype" + + RETVAL="$_arch" +} + +say() { + echo "elan: $1" +} + +err() { + say "$1" >&2 + exit 1 +} + +need_cmd() { + if ! check_cmd "$1" + then err "need '$1' (command not found)" + fi +} + +check_cmd() { + command -v "$1" > /dev/null 2>&1 + return $? +} + +need_ok() { + if [ $? != 0 ]; then err "$1"; fi +} + +assert_nz() { + if [ -z "$1" ]; then err "assert_nz $2"; fi +} + +# Run a command that should never fail. If the command fails execution +# will immediately terminate with an error showing the failing +# command. +ensure() { + "$@" + need_ok "command failed: $*" +} + +# This is just for indicating that commands' results are being +# intentionally ignored. Usually, because it's being executed +# as part of error handling. +ignore() { + "$@" +} + +main "$@" || exit 1 diff --git a/package-lock.json b/package-lock.json new file mode 100644 index 0000000..7c59aab --- /dev/null +++ b/package-lock.json @@ -0,0 +1,6 @@ +{ + "name": "thebook.lean", + "lockfileVersion": 3, + "requires": true, + "packages": {} +}