Grace/Cumulus/GraphTheory/TreePacking/Order.g17

Open in Workbench Download source

Imports

LastColour

Declarations

Source

1-- The order on decompositions: T precedes U when their partition sequences2-- and chosen colours agree below some stage at which U is strictly coarser3-- or chooses a larger colour. A finite family of decompositions into trees4-- and a rest has a maximal member.5-- Part of Cumulus, the Grace17 mathematics library.6-- Copyright (c) 2026 Grant Passmore.7-- Released under the Apache License 2.0. See LICENSE in the repository root.8-- Authors: Grant Passmore910module Grace.Cumulus.GraphTheory.TreePacking.Order11import LastColour1213-- The least natural of the empty set is ∅, so leastNatural(S) is a natural14-- for every set S of naturals, inhabited or not.15theorem leastNatural.empty16  shows leastNatural(∅) = ∅17proof18  unfold leastNatural19  have none : leastNatural.candidates(∅) = ∅20    ext n21    constructor22    . intro member23      exfalso24      exact set.empty with member.right.left25    . intro member26      exfalso27      exact set.empty with member28  rw none29  exact union.empty3031theorem leastNatural.natural (S : Set)32  requires naturals : S ⊆ ℕ33  shows Nat(leastNatural(S))34proof35  by_cases empty : S = ∅36  . rw [empty, leastNatural.empty, ← nat.zero]37    exact Naturals.constructor.zero38  . have inhabited := Nonempty.of_ne_empty with empty39    have member := leastNatural.member with inhabited, naturals40    exact nat.omega.backward with (naturals with leastNatural(S), member)4142-- A term named by a variable, to shorten long proofs.43theorem exists_eq (x : Set)44  shows ∃ c, c = x45proof46  witness x47  rfl4849-- The colour chosen at a stage: the least disconnected colour, or k once50-- every colour is internally connected, as the least of the disconnected51-- colours with k adjoined.52def stageColour (leftEnd rightEnd T P : Set, k : Nat) : Set :=53  leastNatural(disconnectedColour(leftEnd, rightEnd, T, P, k) ∪ {k})5455theorem stageColour.subset (leftEnd rightEnd T P : Set, k : Nat)56  shows disconnectedColour(leftEnd, rightEnd, T, P, k) ∪ {k} ⊆ ℕ57proof58  intros i member59  simp at member60  have subset := disconnectedColour.subset at leftEnd, rightEnd, T, P, k61  rcases member with colour | same62  . exact subset with i, colour63  . rw same64    exact nat.omega.forward at k with *6566theorem stageColour.inhabited (leftEnd rightEnd T P : Set, k : Nat)67  shows Nonempty(disconnectedColour(leftEnd, rightEnd, T, P, k) ∪ {k})68proof69  have member : k ∈ disconnectedColour(leftEnd, rightEnd, T, P, k) ∪ {k}70    by simp71  exact ⟨k, member⟩7273theorem stageColour.natural (leftEnd rightEnd T P : Set, k : Nat)74  shows Nat(stageColour(leftEnd, rightEnd, T, P, k))75proof76  unfold stageColour77  exact leastNatural.natural with stageColour.subset7879theorem stageColour.member (leftEnd rightEnd T P : Set, k : Nat)80  shows stageColour(leftEnd, rightEnd, T, P, k) ∈81    disconnectedColour(leftEnd, rightEnd, T, P, k) ∪ {k}82proof83  unfold stageColour84  exact leastNatural.member with stageColour.inhabited, stageColour.subset8586theorem stageColour.least (leftEnd rightEnd T P x : Set, k : Nat)87  requires member : x ∈ disconnectedColour(leftEnd, rightEnd, T, P, k) ∪ {k}88  shows stageColour(leftEnd, rightEnd, T, P, k) ≤ x89proof90  have subset := stageColour.subset at leftEnd, rightEnd, T, P, k91  have xNat := nat.omega.backward with (subset with x, member)92  unfold stageColour93  exact leastNatural.least with stageColour.inhabited, subset, member9495-- The chosen colour is k exactly when every colour is internally connected,96-- and otherwise the least disconnected colour.97theorem stageColour.of_none (leftEnd rightEnd T P : Set, k : Nat)98  requires none : disconnectedColour(leftEnd, rightEnd, T, P, k) = ∅99  shows stageColour(leftEnd, rightEnd, T, P, k) = k100proof101  have member := stageColour.member at leftEnd, rightEnd, T, P, k102  rw none at member103  simp at member104  exact member105106theorem stageColour.of_some (leftEnd rightEnd T P : Set, k : Nat)107  requires some : disconnectedColour(leftEnd, rightEnd, T, P, k) ≠ ∅108  shows stageColour(leftEnd, rightEnd, T, P, k) =109    leastNatural(disconnectedColour(leftEnd, rightEnd, T, P, k))110proof111  have inhabited := Nonempty.of_ne_empty with some112  have subsetColours := disconnectedColour.subset at leftEnd, rightEnd, T, P, k113  have chosen := leastNatural.member with inhabited, subsetColours114  have chosenNat := leastNatural.natural with subsetColours115  have stageNat := stageColour.natural at leftEnd, rightEnd, T, P, k116  have chosenIn :117      leastNatural(disconnectedColour(leftEnd, rightEnd, T, P, k)) ∈118        disconnectedColour(leftEnd, rightEnd, T, P, k) ∪ {k} by simp [chosen]119  have below := stageColour.least with chosenIn120  have member := stageColour.member at leftEnd, rightEnd, T, P, k121  simp at member122  have above : leastNatural(disconnectedColour(leftEnd, rightEnd, T, P, k)) ≤123      stageColour(leftEnd, rightEnd, T, P, k)124    rcases member with inColours | isK125    . exact leastNatural.least with inhabited, subsetColours, inColours126    . rw isK127      have less := Less.of_membership128        at leastNatural(disconnectedColour(leftEnd, rightEnd, T, P, k)), k129        with chosen.left130      arith131  exact LessEqual.antisymmetric with below, above132133-- The order on decompositions, as in the paper: T precedes T' when the134-- partition sequences and the chosen colours agree below some stage j, and135-- at j the partition of T' is strictly coarser or the colour of T' is larger.136predicate Precedes (V leftEnd rightEnd T U : Set, k : Nat) :=137  ∃ j ∈ ℕ, (∀ i ∈ j,138      partitionSequence(V, leftEnd, rightEnd, T, k, i) =139        partitionSequence(V, leftEnd, rightEnd, U, k, i) ∧140      stageColour(leftEnd, rightEnd, T,141          partitionSequence(V, leftEnd, rightEnd, T, k, i), k) =142        stageColour(leftEnd, rightEnd, U,143          partitionSequence(V, leftEnd, rightEnd, U, k, i), k)) ∧144    ((Refines(partitionSequence(V, leftEnd, rightEnd, T, k, j),145        partitionSequence(V, leftEnd, rightEnd, U, k, j)) ∧146      partitionSequence(V, leftEnd, rightEnd, T, k, j) ≠147        partitionSequence(V, leftEnd, rightEnd, U, k, j)) ∨148     (partitionSequence(V, leftEnd, rightEnd, T, k, j) =149        partitionSequence(V, leftEnd, rightEnd, U, k, j) ∧150      stageColour(leftEnd, rightEnd, T,151          partitionSequence(V, leftEnd, rightEnd, T, k, j), k) <152        stageColour(leftEnd, rightEnd, U,153          partitionSequence(V, leftEnd, rightEnd, U, k, j), k)))154155-- The order is strict: no decomposition precedes itself, since at the stage156-- j the partition would differ from itself or the colour be below itself.157theorem Precedes.irreflexive (V leftEnd rightEnd T : Set, k : Nat)158  shows ¬Precedes(V, leftEnd, rightEnd, T, T, k)159proof160  intro precedes161  obtain ⟨j, _, _, step⟩ := precedes162  rcases step with ⟨_, different⟩ | ⟨_, less⟩163  . exact different with rfl164  . have natural := stageColour.natural at leftEnd, rightEnd, T,165      partitionSequence(V, leftEnd, rightEnd, T, k, j), k166    exact Less.irreflexive with natural, less167168-- Agreement of partitions and chosen colours below a stage composes, up to169-- the earlier of the two stages.170theorem Precedes.agree_below (V leftEnd rightEnd T U W : Set, k j l n : Nat)171  requires first : ∀ i ∈ j,172    partitionSequence(V, leftEnd, rightEnd, T, k, i) =173      partitionSequence(V, leftEnd, rightEnd, U, k, i) ∧174    stageColour(leftEnd, rightEnd, T,175        partitionSequence(V, leftEnd, rightEnd, T, k, i), k) =176      stageColour(leftEnd, rightEnd, U,177        partitionSequence(V, leftEnd, rightEnd, U, k, i), k)178  requires second : ∀ i ∈ l,179    partitionSequence(V, leftEnd, rightEnd, U, k, i) =180      partitionSequence(V, leftEnd, rightEnd, W, k, i) ∧181    stageColour(leftEnd, rightEnd, U,182        partitionSequence(V, leftEnd, rightEnd, U, k, i), k) =183      stageColour(leftEnd, rightEnd, W,184        partitionSequence(V, leftEnd, rightEnd, W, k, i), k)185  requires boundJ : n ≤ j186  requires boundL : n ≤ l187  shows ∀ i ∈ n,188    partitionSequence(V, leftEnd, rightEnd, T, k, i) =189      partitionSequence(V, leftEnd, rightEnd, W, k, i) ∧190    stageColour(leftEnd, rightEnd, T,191        partitionSequence(V, leftEnd, rightEnd, T, k, i), k) =192      stageColour(leftEnd, rightEnd, W,193        partitionSequence(V, leftEnd, rightEnd, W, k, i), k)194proof195  intros i member196  have iNat := natural.member at n with i, member197  have less := Less.of_membership at i, n with member198  have belowJ : i < j by arith199  have belowL : i < l by arith200  obtain ⟨sameTU, coloursTU⟩ :=201    first with i, (membership.of_Less at i, j with *, belowJ)202  obtain ⟨sameUW, coloursUW⟩ :=203    second with i, (membership.of_Less at i, l with *, belowL)204  constructor205  . rw [sameTU, sameUW]206  . rw [coloursTU, coloursUW]207208-- Transitivity: the stage of the composed comparison is the earlier of the209-- two stages; at an equal stage the two partition drops compose by a strict210-- count, and the two colour drops by the order of ℕ.211theorem Precedes.transitive (V E leftEnd rightEnd T U W : Set, k : Nat)212  requires graph : Graph(V, E, leftEnd, rightEnd)213  requires finiteVertices : Finite(V)214  requires nonempty : V ≠ ∅215  requires decompositionT : Decomposition(E, T, k)216  requires decompositionU : Decomposition(E, U, k)217  requires decompositionW : Decomposition(E, W, k)218  requires first : Precedes(V, leftEnd, rightEnd, T, U, k)219  requires second : Precedes(V, leftEnd, rightEnd, U, W, k)220  shows Precedes(V, leftEnd, rightEnd, T, W, k)221proof222  obtain ⟨j, jNatural, agreeTU, stepTU⟩ := first223  obtain ⟨l, lNatural, agreeUW, stepUW⟩ := second224  have jNat := nat.omega.backward with jNatural225  have lNat := nat.omega.backward with lNatural226  have order := Less.trichotomy at j, l with *227  rcases order with before | same | after228  . -- The first comparison decides, since U and W still agree at stage j.229    have inL := membership.of_Less at j, l with *, before230    obtain ⟨sameUW, coloursUW⟩ := agreeUW with j, inL231    have below : j ≤ l by arith232    refine ⟨j, jNatural, (Precedes.agree_below with233      agreeTU, agreeUW, (LessEqual.reflexive at j), below), ?_⟩234    rw [coloursUW, sameUW] at stepTU235    exact stepTU236  . -- Equal stages: the drops compose.237    rw under same at agreeTU238    rw same at stepTU239    refine ⟨l, lNatural, (Precedes.agree_below with agreeTU, agreeUW,240      (LessEqual.reflexive at l), (LessEqual.reflexive at l)), ?_⟩241    have partitionT : Partition(V,242        partitionSequence(V, leftEnd, rightEnd, T, k, l)) :=243      partitionSequence.partition with graph, nonempty, decompositionT244    have partitionU : Partition(V,245        partitionSequence(V, leftEnd, rightEnd, U, k, l)) :=246      partitionSequence.partition with graph, nonempty, decompositionU247    have partitionW : Partition(V,248        partitionSequence(V, leftEnd, rightEnd, W, k, l)) :=249      partitionSequence.partition with graph, nonempty, decompositionW250    rcases stepTU with ⟨refinesTU, differentTU⟩ | ⟨sameTU, lessTU⟩251    . rcases stepUW with ⟨refinesUW, differentUW⟩ | ⟨sameUW, lessUW⟩252      . -- Two strict refinements: the class counts strictly increase twice.253        left254        refine ⟨(Refines.transitive with refinesTU, refinesUW), ?_⟩255        have dropTU := Refines.cardinality_lt with256          finiteVertices, partitionU, partitionT, refinesTU, differentTU257        have dropUW := Refines.cardinality_lt with258          finiteVertices, partitionW, partitionU, refinesUW, differentUW259        have finiteU := Partition.finite with finiteVertices, partitionU260        have finiteW := Partition.finite with finiteVertices, partitionW261        intro sameTW262        rw sameTW at dropTU263        arith264      . left265        rw sameUW at refinesTU, differentTU266        exact ⟨refinesTU, differentTU⟩267    . rcases stepUW with ⟨refinesUW, differentUW⟩ | ⟨sameUW, lessUW⟩268      . left269        rw ← sameTU at refinesUW, differentUW270        exact ⟨refinesUW, differentUW⟩271      . right272        have naturalT := stageColour.natural at leftEnd, rightEnd, T,273          partitionSequence(V, leftEnd, rightEnd, T, k, l), k274        have naturalU := stageColour.natural at leftEnd, rightEnd, U,275          partitionSequence(V, leftEnd, rightEnd, U, k, l), k276        have naturalW := stageColour.natural at leftEnd, rightEnd, W,277          partitionSequence(V, leftEnd, rightEnd, W, k, l), k278        constructor279        . rw [sameTU, sameUW]280        . exact Less.transitive with naturalT, naturalU, naturalW,281            lessTU, lessUW282  . -- The second comparison decides, since T and U still agree at stage l.283    have inJ := membership.of_Less at l, j with *, after284    obtain ⟨sameTU, coloursTU⟩ := agreeTU with l, inJ285    have below : l ≤ j by arith286    refine ⟨l, lNatural, (Precedes.agree_below with287      agreeTU, agreeUW, below, (LessEqual.reflexive at l)), ?_⟩288    rw [← coloursTU, ← sameTU] at stepUW289    exact stepUW290291-- A nonempty finite family of decompositions has a maximal member: adjoin292-- the members one at a time, keeping the old maximal element unless the new293-- one lies above it.294theorem Precedes.exists_maximal (V E leftEnd rightEnd S : Set, k : Nat)295  requires graph : Graph(V, E, leftEnd, rightEnd)296  requires finiteVertices : Finite(V)297  requires nonempty : V ≠ ∅298  requires finite : Finite(S)299  requires members : ∀ T ∈ S, Decomposition(E, T, k)300  shows S ≠ ∅ →301    ∃ T ∈ S, ∀ U ∈ S, ¬Precedes(V, leftEnd, rightEnd, T, U, k)302proof303  induction finite with G a304  | empty =>305    intro inhabited306    exfalso307    exact inhabited with rfl308  | insert using ih =>309    intro _310    have aIn : a ∈ G ∪ {a} by simp311    have decompositionA := members with a, aMember312    by_cases emptyG : G = ∅313    . refine ⟨a, aIn, ?_⟩314      intros U member above315      rw emptyG at member316      simp at member317      rw member at above318      exact Precedes.irreflexive with above319    . obtain ⟨M, inG, maximal⟩ := ih with emptyG320      have decompositionM := members with M, (GSubset with M, inG)321      by_cases better : Precedes(V, leftEnd, rightEnd, M, a, k)322      . -- a is maximal: a member above a would lie above M.323        refine ⟨a, aIn, ?_⟩324        intros U member above325        simp at member326        rcases member with inG2 | same327        . have decompositionU := members with U, (GSubset with U, inG2)328          have chain := Precedes.transitive with graph, finiteVertices,329            nonempty, decompositionM, decompositionA, decompositionU,330            better, above331          exact maximal with U, inG2, chain332        . rw same at above333          exact Precedes.irreflexive with above334      . have mIn : M ∈ G ∪ {a} by simp [inG]335        refine ⟨M, mIn, ?_⟩336        intros U member above337        simp at member338        rcases member with inG2 | same339        . exact maximal with U, inG2, above340        . rw same at above341          exact better with above342343-- The decompositions into succ(k) colours whose first k colours are trees:344-- a finite family, as a set of subsets of succ(k) × 𝒫(E).345def treeDecompositions (V E leftEnd rightEnd : Set, k : Nat) : Set :=346  { T ∈ 𝒫(succ(k) × 𝒫(E)) | Decomposition(E, T, succ(k)) ∧347    (∀ i ∈ k, SpanningTree(V, leftEnd, rightEnd, T(i))) }348349theorem treeDecompositions.finite (V E leftEnd rightEnd : Set, k : Nat)350  requires finiteEdges : Finite(E)351  shows Finite(treeDecompositions(V, E, leftEnd, rightEnd, k))352proof353  have subset : treeDecompositions(V, E, leftEnd, rightEnd, k) ⊆354      𝒫(succ(k) × 𝒫(E))355    intros T member356    exact member.left357  have finiteIndex : Finite(succ(k)) := Finite.natural at succ(k)358  have finiteProduct := Finite.product with359    finiteIndex, (Finite.powerset with finiteEdges)360  exact Finite.subset with (Finite.powerset with finiteProduct), subset361362-- The order is a strict partial order on the finitely many decompositions,363-- so a maximal one exists among those whose first k colours are trees.364theorem Precedes.maximal (V E leftEnd rightEnd : Set, k : Nat)365  requires graph : Graph(V, E, leftEnd, rightEnd)366  requires finiteVertices : Finite(V)367  requires finiteEdges : Finite(E)368  requires nonempty : V ≠ ∅369  requires some : ∃ T, Decomposition(E, T, succ(k)) ∧370    (∀ i ∈ k, SpanningTree(V, leftEnd, rightEnd, T(i)))371  shows ∃ T, Decomposition(E, T, succ(k)) ∧372    (∀ i ∈ k, SpanningTree(V, leftEnd, rightEnd, T(i))) ∧373    ¬(∃ U, Decomposition(E, U, succ(k)) ∧374      (∀ i ∈ k, SpanningTree(V, leftEnd, rightEnd, U(i))) ∧375      Precedes(V, leftEnd, rightEnd, T, U, succ(k)))376proof377  obtain ⟨T₀, decomposition₀, trees₀⟩ := some378  have finiteFamily := treeDecompositions.finite379    at V, E, leftEnd, rightEnd, k with finiteEdges380  have members : ∀ T ∈ treeDecompositions(V, E, leftEnd, rightEnd, k),381      Decomposition(E, T, succ(k))382    intros T member383    exact member.right.left384  have inhabited : treeDecompositions(V, E, leftEnd, rightEnd, k) ≠ ∅385    apply Nonempty.ne_empty386    witness T₀387    have relation : T₀ ⊆ succ(k) × 𝒫(E) := decomposition₀.left.left388    exact ⟨(powerset.membership_iff.backward with relation),389      decomposition₀, trees₀⟩390  have step := Precedes.exists_maximal with391    graph, finiteVertices, nonempty, finiteFamily, members392  obtain ⟨T, member, maximal⟩ := step with inhabited393  obtain ⟨_, decomposition, trees⟩ := member394  refine ⟨T, decomposition, trees, ?_⟩395  intro worse396  obtain ⟨U, decompositionU, treesU, precedes⟩ := worse397  have relation : U ⊆ succ(k) × 𝒫(E) := decompositionU.left.left398  have memberU : U ∈ treeDecompositions(V, E, leftEnd, rightEnd, k) :=399    ⟨(powerset.membership_iff.backward with relation),400      decompositionU, treesU⟩401  exact maximal with U, memberU, precedes402