Matroid greedy algorithm

DefinitionGreedy scan with an independence oracle#✓fully proved

Given an oracle \(O\) that accepts or rejects each finite subset of a type \(\alpha\), a finite set \(S \subseteq \alpha\) and a list \(e_1, \dots, e_n\) of elements of \(\alpha\), the greedy scan processes \(e_1, \dots, e_n\) in order, starting with \(S\) as the current set: it replaces the current set \(T\) by \(T \cup \{e_i\}\) if \(O\) accepts \(T \cup \{e_i\}\), and leaves it unchanged otherwise. It returns the final current set and charges one unit of time per element processed.

def matroidGreedyScan (indep : Finset α → Bool) (S : Finset α) : List α → TimeM ℕ (Finset α)
  | [] => pure S
  | e :: es => do
      ✓
      if indep (insert e S) then matroidGreedyScan indep (insert e S) es
      else matroidGreedyScan indep S es
Used by 10
Used byGreedy optimality gives the augmentation axiom · Threshold counts of the matroid greedy result · Greedy algorithm on a matroid · The matroid greedy result is independent · The matroid greedy result is a base · The greedy scan over a concatenation · A scan that accepts nothing · A scan inside an independent set keeps everything · Invariant of the greedy scan · Running time of the greedy scan

DefinitionGreedy algorithm on a matroid#✓fully proved

Given an oracle \(O\) that accepts or rejects each finite subset of a type \(\alpha\) and a list \(L\) of elements of \(\alpha\), the greedy algorithm starts from the empty set, processes the elements of \(L\) in order, adds an element \(e\) to the current set \(T\) when \(O\) accepts \(T \cup \{e\}\) and leaves \(T\) unchanged otherwise, and returns the final set. It charges one unit of time per element processed.

def matroidGreedy (indep : Finset α → Bool) (es : List α) : TimeM ℕ (Finset α) :=
  matroidGreedyScan indep ∅ es
Sources
  • CLRS, third edition, Section 16.4, procedure GREEDY, without its sorting step.
Uses 1 · Used by 10
Statement usesGreedy scan with an independence oracle
Used byKruskal's algorithm returns a maximal forest · Kruskal's algorithm returns a forest · Optimality of Kruskal's algorithm · Greedy optimality gives the augmentation axiom · Threshold counts of the matroid greedy result · Greedy optimality · The matroid greedy result is independent · The matroid greedy result is a base · Optimality of the matroid greedy algorithm · Running time of the matroid greedy algorithm

TheoremRunning time of the greedy scan#✓fully proved

For every oracle \(O\) on finite subsets of a type \(\alpha\), every finite set \(S \subseteq \alpha\) and every list \(L\) of elements of \(\alpha\), the greedy scan with oracle \(O\) from \(S\) over \(L\) takes time exactly the length of \(L\).

@[simp]
theorem matroidGreedyScan_time (indep : Finset α → Bool) (S : Finset α) (es : List α) :
    (matroidGreedyScan indep S es).time = es.length
Uses 1 · Used by 1
Statement usesGreedy scan with an independence oracle
Used byRunning time of the matroid greedy algorithm

TheoremRunning time of the matroid greedy algorithm#✓fully proved

For every oracle \(O\) on finite subsets of a type \(\alpha\) and every list \(L\) of elements of \(\alpha\), the greedy algorithm with oracle \(O\) on \(L\) takes time exactly the length of \(L\), one oracle query per element.

@[simp]
theorem matroidGreedy_time (indep : Finset α → Bool) (es : List α) :
    (matroidGreedy indep es).time = es.length
Uses 2
Statement usesGreedy algorithm on a matroid
Proof usesRunning time of the greedy scan

TheoremThe greedy scan over a concatenation#✓fully proved

For every oracle \(O\) on finite subsets of a type \(\alpha\), every finite set \(S \subseteq \alpha\) and all lists \(P\) and \(Q\) of elements of \(\alpha\), the set returned by the greedy scan with oracle \(O\) from \(S\) over \(P\) followed by \(Q\) equals the set returned by the greedy scan with oracle \(O\) over \(Q\) starting from the set that the scan with oracle \(O\) from \(S\) over \(P\) returns.

theorem matroidGreedyScan_append (indep : Finset α → Bool) (S : Finset α) (P Q : List α) :
    (matroidGreedyScan indep S (P ++ Q)).ret =
      (matroidGreedyScan indep (matroidGreedyScan indep S P).ret Q).ret
Uses 1 · Used by 2
Statement usesGreedy scan with an independence oracle
Used byGreedy optimality gives the augmentation axiom · Threshold counts of the matroid greedy result

TheoremInvariant of the greedy scan#✓fully proved

Let \(M\) be a matroid on a type \(\alpha\), let \(O\) be an oracle that accepts a finite set \(A \subseteq \alpha\) exactly when \(A\) is independent in \(M\), let \(S\) be a finite independent set of \(M\) and \(L\) a list of elements of \(\alpha\), and let \(T\) be the set returned by the greedy scan with oracle \(O\) from \(S\) over \(L\). Then \(T\) is independent in \(M\), and for every element \(e\) of \(L\) with \(e \notin T\), the set \(T \cup \{e\}\) is not independent in \(M\).

theorem matroidGreedyScan_spec (hind : ∀ S, indep S = true ↔ M.Indep ↑S) {S : Finset α}
    (hS : M.Indep ↑S) (es : List α) :
    M.Indep ↑(matroidGreedyScan indep S es).ret ∧
      ∀ e ∈ es, e ∉ (matroidGreedyScan indep S es).ret →
        ¬ M.Indep (insert e ↑(matroidGreedyScan indep S es).ret)
Uses 1 · Used by 3
Statement usesGreedy scan with an independence oracle
Used byThreshold counts of the matroid greedy result · The matroid greedy result is independent · The matroid greedy result is a base

TheoremThe matroid greedy result is independent#✓fully proved

Let \(M\) be a matroid on a type \(\alpha\) and let \(O\) be an oracle that accepts a finite set \(A \subseteq \alpha\) exactly when \(A\) is independent in \(M\). For every list \(L\) of elements of \(\alpha\), the set returned by the greedy algorithm with oracle \(O\) on \(L\) is independent in \(M\), and each of its elements occurs in \(L\).

theorem matroidGreedy_indep (hind : ∀ S, indep S = true ↔ M.Indep ↑S) (es : List α) :
    M.Indep ↑(matroidGreedy indep es).ret ∧ ∀ x ∈ (matroidGreedy indep es).ret, x ∈ es
Uses 3 · Used by 2
Statement usesGreedy algorithm on a matroid
Proof usesGreedy scan with an independence oracle · Invariant of the greedy scan
Used byKruskal's algorithm returns a forest · Optimality of the matroid greedy algorithm

TheoremThe matroid greedy result is a base#✓fully proved

Let \(M\) be a matroid on a type \(\alpha\) with ground set \(E\), and let \(O\) be an oracle that accepts a finite set \(A \subseteq \alpha\) exactly when \(A\) is independent in \(M\). For every list \(L\) in which an element of \(\alpha\) occurs if and only if it lies in \(E\), the set returned by the greedy algorithm with oracle \(O\) on \(L\) is a base of \(M\).

theorem matroidGreedy_isBase (hind : ∀ S, indep S = true ↔ M.Indep ↑S) (es : List α)
    (hground : ∀ x, x ∈ M.E ↔ x ∈ es) : M.IsBase ↑(matroidGreedy indep es).ret
Uses 3 · Used by 1
Statement usesGreedy algorithm on a matroid
Proof usesGreedy scan with an independence oracle · Invariant of the greedy scan
Used byKruskal's algorithm returns a maximal forest

TheoremThreshold counts of the matroid greedy result#✓fully proved

Let \(M\) be a matroid on a type \(\alpha\), let \(O\) be an oracle that accepts a finite set \(A \subseteq \alpha\) exactly when \(A\) is independent in \(M\), and let \(w : \alpha \to \mathbb{N}\) be a weight function. Let \(L\) be a list of elements of \(\alpha\) in nonincreasing order of weight (whenever \(a\) occurs before \(b\) in \(L\), \(w(b) \le w(a)\)), and let \(G\) be the set returned by the greedy algorithm with oracle \(O\) on \(L\). Then for every finite independent set \(I\) of \(M\) whose elements all occur in \(L\) and every \(t \in \mathbb{N}\), the number of \(x \in I\) with \(w(x) > t\) is at most the number of \(x \in G\) with \(w(x) > t\).

theorem card_filter_le_matroidGreedy (hind : ∀ S, indep S = true ↔ M.Indep ↑S) (w : α → ℕ)
    {es : List α} (hsorted : es.Pairwise fun a b => w b ≤ w a) {I : Finset α}
    (hI : M.Indep ↑I) (hIes : ∀ x ∈ I, x ∈ es) (t : ℕ) :
    (I.filter fun x => t < w x).card ≤
      ((matroidGreedy indep es).ret.filter fun x => t < w x).card
Uses 4 · Used by 1
Statement usesGreedy algorithm on a matroid
Proof usesGreedy scan with an independence oracle · The greedy scan over a concatenation · Invariant of the greedy scan
Used byOptimality of the matroid greedy algorithm

TheoremOptimality of the matroid greedy algorithm#✓fully proved

Let \(M\) be a matroid on a type \(\alpha\), let \(O\) be an oracle that accepts a finite set \(A \subseteq \alpha\) exactly when \(A\) is independent in \(M\), and let \(w : \alpha \to \mathbb{N}\) be a weight function. Let \(L\) be a list of elements of \(\alpha\) in nonincreasing order of weight (whenever \(a\) occurs before \(b\) in \(L\), \(w(b) \le w(a)\)), and let \(G\) be the set returned by the greedy algorithm with oracle \(O\) on \(L\). Then every finite independent set \(I\) of \(M\) whose elements all occur in \(L\) satisfies \(\sum_{x \in I} w(x) \le \sum_{x \in G} w(x)\).

theorem matroidGreedy_optimal (hind : ∀ S, indep S = true ↔ M.Indep ↑S) (w : α → ℕ)
    {es : List α} (hsorted : es.Pairwise fun a b => w b ≤ w a) {I : Finset α}
    (hI : M.Indep ↑I) (hIes : ∀ x ∈ I, x ∈ es) :
    ∑ x ∈ I, w x ≤ ∑ x ∈ (matroidGreedy indep es).ret, w x
Sources
  • CLRS, third edition, Theorem 16.11.
Uses 3 · Used by 2
Statement usesGreedy algorithm on a matroid
Proof usesThreshold counts of the matroid greedy result · The matroid greedy result is independent
Used byOptimality of Kruskal's algorithm · Rado–Edmonds theorem

StructureIndependence system#✓fully proved

A predicate \(\mathrm{indep}\) on the finite subsets of a type \(\alpha\) is an independence system when the empty set is independent and every subset of an independent set is independent.

structure IsIndepSystem (indep : Finset α → Bool) : Prop where
  empty : indep ∅ = true
  subset : ∀ ⦃S T : Finset α⦄, T ⊆ S → indep S = true → indep T = true
Used by 4
Used byGreedy optimality gives the augmentation axiom · Greedy-optimal independence systems are matroids · Rado–Edmonds theorem · A scan inside an independent set keeps everything

TheoremA scan inside an independent set keeps everything#✓fully proved

Let \(\alpha\) be a type, let \(\mathrm{indep}\) be an independence system on the finite subsets of \(\alpha\) and let \(I\) be an independent set. For every list \(L\) of elements of \(I\) and every finite set \(S \subseteq I\), the greedy scan of \(L\) starting from \(S\) returns \(S\) together with all elements of \(L\).

theorem matroidGreedyScan_of_subset {indep : Finset α → Bool} (hsys : IsIndepSystem indep)
    {I : Finset α} (hI : indep I = true) :
    ∀ (L : List α) (S : Finset α), S ⊆ I → (∀ e ∈ L, e ∈ I) →
      (matroidGreedyScan indep S L).ret = S ∪ L.toFinset
Uses 2 · Used by 1
Statement usesIndependence system · Greedy scan with an independence oracle
Used byGreedy optimality gives the augmentation axiom

TheoremA scan that accepts nothing#✓fully proved

Let \(\alpha\) be a type, let \(\mathrm{indep}\) be an independence oracle on the finite subsets of \(\alpha\), let \(S\) be a finite subset of \(\alpha\) and let \(L\) be a list of elements of \(\alpha\) such that \(\mathrm{indep}\) rejects \(S \cup \{e\}\) for every \(e\) in \(L\). Then the greedy scan of \(L\) starting from \(S\) returns \(S\).

theorem matroidGreedyScan_of_forall_not {indep : Finset α → Bool} (S : Finset α) :
    ∀ L : List α, (∀ e ∈ L, indep (insert e S) = false) → (matroidGreedyScan indep S L).ret = S
Uses 1 · Used by 1
Statement usesGreedy scan with an independence oracle
Used byGreedy optimality gives the augmentation axiom

DefinitionGreedy optimality#✓fully proved

Let \(\alpha\) be a finite type and let \(\mathrm{indep}\) be an independence oracle on the finite subsets of \(\alpha\). The greedy algorithm is optimal for \(\mathrm{indep}\) when, for every weight function \(w : \alpha \to \mathbb{N}\) and every list \(L\) that contains every element of \(\alpha\) exactly once, in nonincreasing order of \(w\), the set \(T\) returned by the matroid greedy algorithm on \(L\) with oracle \(\mathrm{indep}\) satisfies \(\sum_{x \in I} w(x) \le \sum_{x \in T} w(x)\) for every finite set \(I\) independent under \(\mathrm{indep}\).

Finiteness of \(\alpha\) keeps this from holding vacuously: on an infinite type no list contains every element.

@[nolint unusedArguments]
def GreedyOptimal [Finite α] (indep : Finset α → Bool) : Prop :=
  ∀ (w : α → ℕ) (es : List α), es.Nodup → (∀ x, x ∈ es) →
    (es.Pairwise fun a b => w b ≤ w a) →
      ∀ I, indep I = true → ∑ x ∈ I, w x ≤ ∑ x ∈ (matroidGreedy indep es).ret, w x
Uses 1 · Used by 3
Statement usesGreedy algorithm on a matroid
Used byGreedy optimality gives the augmentation axiom · Greedy-optimal independence systems are matroids · Rado–Edmonds theorem

TheoremGreedy optimality gives the augmentation axiom#✓fully proved

Let \(\alpha\) be a finite type and let \(\mathrm{indep}\) be an independence system on the finite subsets of \(\alpha\) for which the greedy algorithm is optimal. If \(I\) and \(J\) are independent sets with \(|I| < |J|\), then some element \(e \in J\) with \(e \notin I\) makes \(I \cup \{e\}\) independent.

theorem augment_of_greedyOptimal {indep : Finset α → Bool} (hsys : IsIndepSystem indep)
    (hopt : GreedyOptimal indep) {I J : Finset α} (hI : indep I = true) (hJ : indep J = true)
    (hlt : I.card < J.card) : ∃ e ∈ J, e ∉ I ∧ indep (insert e I) = true
Uses 7 · Used by 1
Statement usesGreedy optimality · Independence system
Proof usesGreedy algorithm on a matroid · Greedy scan with an independence oracle · The greedy scan over a concatenation · A scan that accepts nothing · A scan inside an independent set keeps everything
Used byGreedy-optimal independence systems are matroids

TheoremGreedy-optimal independence systems are matroids#✓fully proved

Let \(\alpha\) be a finite type and let \(\mathrm{indep}\) be an independence system on the finite subsets of \(\alpha\) for which the greedy algorithm is optimal. Then there is a matroid \(M\) on \(\alpha\) whose ground set is all of \(\alpha\) such that a finite set \(S \subseteq \alpha\) is independent in \(M\) exactly when \(S\) is independent under \(\mathrm{indep}\).

theorem exists_matroid_of_greedyOptimal {indep : Finset α → Bool} (hsys : IsIndepSystem indep)
    (hopt : GreedyOptimal indep) :
    ∃ M : Matroid α, M.E = Set.univ ∧ ∀ S : Finset α, M.Indep ↑S ↔ indep S = true
Uses 3 · Used by 1
Statement usesGreedy optimality · Independence system
Proof usesGreedy optimality gives the augmentation axiom
Used byRado–Edmonds theorem

TheoremRado–Edmonds theorem#✓fully proved

Let \(\alpha\) be a finite type and let \(\mathrm{indep}\) be an independence system on the finite subsets of \(\alpha\). The greedy algorithm is optimal for \(\mathrm{indep}\) if and only if there is a matroid \(M\) on \(\alpha\) whose ground set is all of \(\alpha\) such that a finite set \(S \subseteq \alpha\) is independent in \(M\) exactly when \(S\) is independent under \(\mathrm{indep}\).

theorem greedyOptimal_iff_exists_matroid {indep : Finset α → Bool} (hsys : IsIndepSystem indep) :
    GreedyOptimal indep ↔
      ∃ M : Matroid α, M.E = Set.univ ∧ ∀ S : Finset α, M.Indep ↑S ↔ indep S = true
Uses 4
Statement usesGreedy optimality · Independence system
Proof usesGreedy-optimal independence systems are matroids · Optimality of the matroid greedy algorithm
17 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.