feat: Defining Greedoid

Mathlib.lean

@@ -2261,6 +2261,9 @@ import Mathlib.Data.FunLike.Basic
 import Mathlib.Data.FunLike.Embedding
 import Mathlib.Data.FunLike.Equiv
 import Mathlib.Data.FunLike.Fintype
+import Mathlib.Data.Greedoid.Accessible
+import Mathlib.Data.Greedoid.Basic
+import Mathlib.Data.Greedoid.Exchange
 import Mathlib.Data.Holor
 import Mathlib.Data.Int.AbsoluteValue
 import Mathlib.Data.Int.Align

Mathlib/Data/Greedoid/Accessible.lean

@@ -0,0 +1,116 @@
+/-
+Copyright (c) 2024 Jihoon Hyun. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jihoon Hyun
+-/
+import Mathlib.Data.Finset.Basic
+import Mathlib.Data.Finset.Card
+import Init.Data.Nat.Basic
+
+/-!
+This file contains the definition of `AccessibleProperty` and `Accessible` typeclass,
+along with some main properties of accessible set systems.
+
+# Accessible
+A set system `S` is accessible if there is some `x ∈ s` which `s \ {x} ∈ S` for each `s ∈ S`.
+This is equivalent to saying that `S` is accessible if there is some `t ⊆ s` which `t ∈ S` and
+`t.card + 1 = s.card`, for each `s ∈ S`.
+This file uses the latter definition to remove a `DecidableEq` condition which is required
+when using the former definition.
+-/
+
+namespace Greedoid
+
+open Nat Finset
+
+variable {α : Type*}
+
+/-- The accessible property of greedoid. -/
+def AccessibleProperty (Sys : Finset α → Prop) : Prop :=
+  ⦃s : Finset α⦄ → Sys s → s.Nonempty → ∃ t, t ⊆ s ∧ t.card + 1 = s.card ∧ Sys t
+
+/-- A set system is accessible if there is some element `x` in `s` which `s \ {x}` is also in the
+    set system, for each nonempty set `s` of the set system.
+    This automatically implies that nonempty accessible set systems contain an empty set. -/
+class Accessible (Sys : Finset α → Prop) : Prop where
+  accessible :
+    ⦃s : Finset α⦄ → Sys s → s.Nonempty → ∃ t, t ⊆ s ∧ t.card + 1 = s.card ∧ Sys t
+
+namespace Accessible
+
+variable {Sys : Finset α → Prop} [Accessible Sys]
+
+/-- A helper lemma for `nonempty_contains_emptyset`.-/
+theorem nonempty_contains_emptyset'
+    {s : Finset α} (hs : Sys s) {n : ℕ} (hn : n = s.card) :
+    Sys ∅ := by
+  induction n generalizing s with
+  | zero => exact card_eq_zero.mp hn.symm ▸ hs
+  | succ _ ih =>
+    rcases Accessible.accessible hs (by rw[← card_ne_zero]; omega) with ⟨t, _, _, ht⟩
+    exact ih ht (by omega)
+
+theorem nonempty_contains_emptyset
+    (h : ∃ s, Sys s) :
+    Sys ∅ :=
+  have ⟨_, h⟩ := h; nonempty_contains_emptyset' h rfl
+
+@[simp]
+theorem nonempty_contains_emptyset_iff :
+    (∃ s, Sys s) ↔ Sys ∅ :=
+  ⟨fun h => nonempty_contains_emptyset h, fun h => ⟨∅, h⟩⟩
+
+-- TODO: Find better name.
+-- TODO: Find a better way to inform `hS`.
+--       `hS` can be obtained by `hs`.
+theorem induction_on_accessible
+    (hS : Sys ∅)
+    {p : ⦃s : Finset α⦄ → Sys s → Prop}
+    (empty : p hS)
+    (insert :
+      ∀ ⦃s₁ : Finset α⦄, (hs₁ : Sys s₁) →
+      ∀ ⦃s₂ : Finset α⦄, (hs₂ : Sys s₂) →
+      s₂ ⊆ s₁ → s₂.card + 1 = s₁.card → p hs₂ → p hs₁)
+    {s : Finset α} (hs : Sys s):
+    p hs := by
+  induction' hn : s.card generalizing s
+  case zero => exact card_eq_zero.mp hn ▸ empty
+  case succ n ih =>
+    rcases accessible hs (one_le_card.mp (by omega)) with ⟨t, ht₁, ht₂, ht₃⟩
+    exact insert hs ht₃ ht₁ ht₂ (ih ht₃ (by omega))
+
+-- TODO: Find better name.
+theorem construction_on_accessible
+    [DecidableEq α] {s : Finset α} (hs : Sys s) :
+    ∃ l : List α, l.Nodup ∧ Multiset.ofList l = s.val ∧ ∀ l', l' <:+ l →
+      ∃ s', Multiset.ofList l' = s'.val ∧ Sys s' := by
+  have hS := nonempty_contains_emptyset ⟨s, hs⟩
+  induction hs using induction_on_accessible hS with
+  | empty => use []; simp; use ∅; simp [hS]
+  | insert hs hs₂ h₁ h₂ h₃ =>
+    rename_i s₁ s₂; clear hs₂; rcases h₃ with ⟨l₀, hl₀₁, hl₀₂, hl₀₃⟩
+    have h₃ : ∃! a, a ∈ s₁ ∧ a ∉ l₀ := by
+      have h₃ : (s₁ \ s₂).card = 1 := by rw [card_sdiff h₁]; omega
+      rcases card_eq_one.mp h₃ with ⟨a, ha⟩; rw [eq_singleton_iff_unique_mem] at ha
+      rcases ha with ⟨h₄, h₅⟩; simp at h₄ h₅
+      rw [← @mem_val _ _ s₂, ← hl₀₂, Multiset.mem_coe] at h₄
+      use a; simp [h₄, h₅]; intro _ h₁ h₂; apply h₅ _ h₁
+      intro h; apply h₂; rw [← Multiset.mem_coe, hl₀₂, mem_val]; exact h
+    let x : α := s₁.choose (· ∉ l₀) h₃; have hx : x ∉ l₀ := choose_property _ _ h₃; use x :: l₀
+    have h₄ : ↑(x :: l₀) ≤ s₁.val := by
+      rw [Multiset.le_iff_count]; intro a
+      by_cases ha : a = x
+      · simp_all [Multiset.nodup_iff_count_eq_one.mp s₁.nodup x (choose_mem _ _ h₃)]
+      · simp [ha]; rw [← Multiset.coe_count, hl₀₂]
+        exact Multiset.count_le_of_le _ (val_le_iff.mpr h₁)
+    have h₅ : Multiset.card s₁.val ≤ Multiset.card (Multiset.ofList (x :: l₀)) := by
+      simp [← h₂, ← card_val s₂, ← hl₀₂]
+    have h₆ := Multiset.eq_of_le_of_card_le h₄ h₅
+    apply And.intro (by simp [hl₀₁, hx]) (And.intro h₆ _)
+    intro l' hl'; rw [List.suffix_cons_iff] at hl'; apply hl'.elim _ (fun h => hl₀₃ _ h)
+    intro hl'; use s₁; simp [hs, hl', h₆]
+
+end Accessible
+
+end Greedoid
+

Mathlib/Data/Greedoid/Basic.lean

@@ -0,0 +1,127 @@
+/-
+Copyright (c) 2024 Jihoon Hyun. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jihoon Hyun
+-/
+import Mathlib.Data.Greedoid.Accessible
+import Mathlib.Data.Greedoid.Exchange
+
+/-!
+This file contains the definition of `ExchangeProperty` and `AccessibleProperty`, along with the
+main subject `Greedoid α`.
+
+# Greedoid
+Greedoid is a set system, i.e., a family of sets, over a finite ground set, which satisfies both
+exchange and accessible properties.
+-/
+
+/-- Greedoid is a nonempty (finite) set system satisfying both accessible and exchange property. -/
+structure Greedoid (α : Type*) where
+  /-- The ground set which every element lies on. -/
+  ground_set : Finset α
+  /-- The feasible set of the greedoid. -/
+  feasible : Finset α → Prop
+  contains_emptyset : feasible ∅
+  exchange_property : Greedoid.ExchangeProperty feasible
+  subset_ground : ∀ s, feasible s → s ⊆ ground_set
+
+section Greedoid
+
+variable {α : Type*}
+
+/-- Definition of `Finset` in `Greedoid`.
+    This is often called 'feasible'· -/
+protected def Greedoid.mem (G : Greedoid α) (s : Finset α) := G.feasible s
+
+instance : Membership (Finset α) (Greedoid α) :=
+  ⟨Greedoid.mem⟩
+
+end Greedoid
+
+namespace Greedoid
+
+variable {α : Type*}
+
+open Nat List Finset
+
+theorem eq_of_veq : ∀ {G₁ G₂ : Greedoid α},
+    G₁.ground_set = G₂.ground_set → G₁.feasible = G₂.feasible → G₁ = G₂
+  | ⟨_, _, _, _, _⟩, ⟨_, _, _, _, _⟩, h₁, h₂ => by cases h₁; cases h₂; rfl
+
+@[simp]
+theorem feasible_set_injective :
+    Function.Injective (fun G : Greedoid α => (G.ground_set, G.feasible)) :=
+  fun _ _ => by simp; exact eq_of_veq
+
+@[simp]
+theorem feasible_set_inj {G₁ G₂ : Greedoid α} :
+    G₁.ground_set = G₂.ground_set ∧ G₁.feasible = G₂.feasible ↔ G₁ = G₂ :=
+  ⟨fun h => by apply eq_of_veq <;> simp [h], fun h => by simp [h]⟩
+
+
+
+variable {G : Greedoid α}
+
+variable {s : Finset α}
+variable {s₁ : Finset α} (hs₁ : s₁ ∈ G)
+variable {s₂ : Finset α} (hs₂ : s₂ ∈ G)
+
+protected theorem accessible_property :
+    AccessibleProperty G.feasible := by
+  intro s hs₁ hs₂
+  by_contra h'; simp at h'
+  let F : Set (Finset α) :=
+    {t | G.feasible t ∧ t.card < s.card}
+  have hF : ∅ ∈ F := by simp [F, G.contains_emptyset, hs₂]
+  let F' : Finset α → Prop := fun t ↦
+    t ∈ F ∧ ∀ t', G.feasible t' → t'.card < s.card → t'.card ≤ t.card
+  have hF' : ∃ x, F' x := by
+    by_contra h''; simp [F', F] at h''
+    have h₁ : ∀ n, ∃ t, t ∈ F ∧ t.card = n := by
+      intro n; induction n with
+      | zero => use ∅; simp [hF]
+      | succ n ih =>
+        rcases ih with ⟨t, ht₁, ht₂⟩
+        rcases ht₁ with ⟨ht₁, ht₃⟩
+        rcases h'' t ht₁ ht₃ with ⟨u, hu₁, hu₂, hu₃⟩
+        rcases G.exchange_property hu₁ ht₁ hu₃ with ⟨_, _, hx₁, hx₂⟩
+        use t.cons _ hx₁
+        simp [F, ht₂, hx₂]; omega
+    rcases h₁ s.card with ⟨t, ht₁, ht₂⟩
+    simp [F, ht₂] at ht₁
+  rcases hF' with ⟨u, hu₁, hu₂⟩
+  rcases hu₁ with ⟨_, hu₁⟩
+  rcases ExchangeProperty.exists_superset_of_card_le
+    G.exchange_property hs₁ G.contains_emptyset (le_of_lt hu₁) (zero_le _)
+    with ⟨t, ht₁, _, ht₂, ht₃⟩
+  simp at ht₂
+  rw [← ht₃] at hu₁
+  rcases G.exchange_property hs₁ ht₁ hu₁ with ⟨_, _, hx₁, hx₂⟩
+  have h : (t.cons _ hx₁).card < s.card := by
+    by_contra h''; simp at h''; apply h' _ ht₂ _ ht₁; omega
+  have := card_cons _ ▸ ht₃ ▸ hu₂ _ hx₂ h; omega
+
+instance : Accessible G.feasible := ⟨G.accessible_property⟩
+
+section Membership
+
+@[simp]
+theorem system_feasible_set_mem_mem : G.feasible s ↔ s ∈ G := by rfl
+
+theorem mem_accessible
+    (hs₁ : s ∈ G) (hs₂ : s.Nonempty) :
+    ∃ t, t ⊆ s ∧ t.card + 1 = s.card ∧ t ∈ G :=
+  G.accessible_property hs₁ hs₂
+
+theorem mem_exchange
+    (hs₁ : G.feasible s₁) (hs₂ : G.feasible s₂) (hs : s₂.card < s₁.card) :
+    ∃ x ∈ s₁, ∃ h : x ∉ s₂, cons x s₂ h ∈ G :=
+  G.exchange_property hs₁ hs₂ hs
+
+end Membership
+
+@[simp]
+theorem emptyset_feasible : ∅ ∈ G := G.contains_emptyset
+
+end Greedoid
+

Mathlib/Data/Greedoid/Exchange.lean

@@ -0,0 +1,81 @@
+/-
+Copyright (c) 2024 Jihoon Hyun. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jihoon Hyun
+-/
+import Mathlib.Data.Finset.Basic
+import Mathlib.Data.Finset.Card
+import Init.Data.Nat.Basic
+
+/-!
+This file contains the definition of `ExchangeProperty`,
+along with some main properties of set systems with the exchange property.
+Not to be confused with 'Exchange System'. [Brylawski & Dieter, 1986]
+
+# Exchange property
+A set system `S` satisfies the exchange property if there is some `x ∈ s \ t` for `s, t ∈ S`
+which `t.card < s.card`, that `t ∪ {x} ∈ S`.
+-/
+
+namespace Greedoid
+
+open Nat Finset
+
+variable {α : Type*}
+
+-- TODO: Is typeclass `Exchange` required?
+/-- The exchange property of greedoid.
+    Note that the exchange property also hold for (finite) matroids.
+
+    A set system satisfies the exchange property if there is some element `x` in some feasible
+    `s₁`, which is not in `s₂` with smaller cardinaliy, and `s₂ ∪ {x}` is also feasible.
+    This implies that all maximal feasible sets are actually maximum. -/
+def ExchangeProperty (Sys : Finset α → Prop) : Prop :=
+  ⦃s₁ : Finset α⦄ → Sys s₁ →
+  ⦃s₂ : Finset α⦄ → Sys s₂ →
+  s₂.card < s₁.card →
+    ∃ x ∈ s₁, ∃ h : x ∉ s₂, Sys (cons x s₂ h)
+
+namespace ExchangeProperty
+
+open Nat Finset
+
+variable {Sys : Finset α → Prop}
+variable {s₁ : Finset α} {s₂ : Finset α}
+
+-- TODO: Find a better name.
+theorem exists_superset_of_card_le
+    (hS : ExchangeProperty Sys) (hs₁ : Sys s₁) (hs₂ : Sys s₂)
+    {n : ℕ} (hn₁ : n ≤ s₁.card) (hn₂ : s₂.card ≤ n) :
+    ∃ s, Sys s ∧ s₂ ⊆ s ∧ (∀ e ∈ s, e ∈ s₁ ∨ e ∈ s₂) ∧ s.card = n := by
+    induction n, hn₂ using le_induction with
+    | base => use s₂; simp [hs₂]; intro _ h; exact .inr h
+    | succ _ h ih =>
+      rcases ih (by omega) with ⟨s, hs, h₁, h₂, rfl⟩
+      rcases hS hs₁ hs hn₁ with ⟨a, ha₁, ha₂, ha₃⟩
+      use cons a s ha₂; simp_all
+      intro _ h; simp [h₁ h]
+
+-- TODO: Find a better name.
+theorem exists_feasible_superset_add_element_feasible
+    (hS : ExchangeProperty Sys) (hs₁ : Sys s₁) (hs₂ : Sys s₂) (hs : s₂ ⊆ s₁)
+    {a : α} (ha₁ : a ∈ s₁) (ha₂ : a ∉ s₂) :
+    ∃ s, Sys s ∧ s₂ ⊆ s ∧ s ⊆ s₁ ∧ ∃ h : a ∉ s, Sys (cons a s h) := by
+  induction' hn : s₁.card - s₂.card generalizing s₂
+  case zero =>
+    exact False.elim ((eq_of_subset_of_card_le hs (Nat.le_of_sub_eq_zero hn) ▸ ha₂) ha₁)
+  case succ _ ih =>
+    rcases exists_superset_of_card_le hS hs₁ hs₂ (by omega) (le_succ _)
+      with ⟨s, hs₃, hs₄, hs₅, hs₆⟩
+    by_cases h : a ∈ s
+    · use s₂; simp [hs₂, hs, ha₂]
+      exact (eq_of_subset_of_card_le
+        ((@cons_subset _ _ _ _ ha₂).mpr ⟨h, hs₄⟩)  (hs₆ ▸ card_cons ha₂ ▸ le_rfl)) ▸ hs₃
+    · rcases ih hs₃ (fun e h ↦ (hs₅ _ h).elim id (fun f ↦ hs f)) h (by omega)
+        with ⟨t, ht⟩
+      use t; simp [ht, subset_trans hs₄]
+
+end ExchangeProperty
+
+end Greedoid
+