Grace/Cumulus/GraphTheory/TreePacking/Exchange.g17

Open in Workbench Download source

Imports

Order

Declarations

Source

1-- The exchange step: an edge e of least finite level in an even set of the2-- last colour is traded for an edge of lower level on the even set it closes3-- in the colour refined at that level, and the first k colours stay trees.4-- Part of Cumulus, the Grace17 mathematics library.5-- Copyright (c) 2026 Grant Passmore.6-- Released under the Apache License 2.0. See LICENSE in the repository root.7-- Authors: Grant Passmore89module Grace.Cumulus.GraphTheory.TreePacking.Exchange10import Order1112-- The exchange: e of least finite level m in an even set of T_k, P its class13-- at level m, c_m the colour refined there, e' an edge of least level on the14-- even set closed by e in T_{c_m}. Exchanging e and e' between the two15-- colours keeps the first k colours trees.16def exchange (E T e f : Set, c k : Nat) : Set :=17  { p ∈ succ(k) × 𝒫(E) | ∃ i ∈ succ(k),18    (i = c ∧ p = (i, (T(c) ∪ {e}) ∖ {f})) ∨19    (i = k ∧ p = (i, (T(k) ∪ {f}) ∖ {e})) ∨20    (i ≠ c ∧ i ≠ k ∧ p = (i, T(i))) }2122-- An edge has one colour.23theorem Decomposition.colour_unique (E T g : Set, k i j : Nat)24  requires decomposition : Decomposition(E, T, k)25  requires indexI : i ∈ k26  requires indexJ : j ∈ k27  requires inI : g ∈ T(i)28  requires inJ : g ∈ T(j)29  shows i = j30proof31  by_contra different32  exact decomposition.right.right with33    i, indexI, j, indexJ, different, g, inI, inJ3435-- The facts the exchange rests on: c and k are distinct colours, e and f36-- are distinct edges of E, and the two swapped classes lie in E.37theorem exchange.setting (E T e f : Set, c k : Nat)38  requires decomposition : Decomposition(E, T, succ(k))39  requires colour : c ∈ k40  requires first : e ∈ T(k)41  requires second : f ∈ T(c)42  shows c ≠ k ∧ e ≠ f ∧43    (T(c) ∪ {e}) ∖ {f} ∈ 𝒫(E) ∧ (T(k) ∪ {f}) ∖ {e} ∈ 𝒫(E)44proof45  have less := Less.of_membership at c, k with colour46  have distinct : c ≠ k by arith47  have cIn : c ∈ succ(k) by simp [colour]48  have kIn : k ∈ succ(k) by simp49  have classC := Decomposition.class_subset with decomposition, cIn50  have classK := Decomposition.class_subset with decomposition, kIn51  have eInE := classK with e, first52  have fInE := classC with f, second53  have unionC : T(c) ∪ {e} ⊆ E :=54    Subset.union2_iff.backward with55      ⟨classC, (singleton.subset_iff.backward with eInE)⟩56  have unionK : T(k) ∪ {f} ⊆ E :=57    Subset.union2_iff.backward with58      ⟨classK, (singleton.subset_iff.backward with fInE)⟩59  refine ⟨distinct, ?_, ?_, ?_⟩60  . intro same61    rw same at first62    exact decomposition.right.right with63      c, cIn, k, kIn, distinct, f, second, first64  . exact powerset.membership_iff.backward with65      (Subset.transitive with difference.subset_left, unionC)66  . exact powerset.membership_iff.backward with67      (Subset.transitive with difference.subset_left, unionK)6869-- An entry of the exchange is one of the three kinds of class.70theorem exchange.shape (E T e f x y : Set, c k : Nat)71  requires member : (x, y) ∈ exchange(E, T, e, f, c, k)72  shows (x = c ∧ y = (T(c) ∪ {e}) ∖ {f}) ∨73    (x = k ∧ y = (T(k) ∪ {f}) ∖ {e}) ∨74    (x ≠ c ∧ x ≠ k ∧ y = T(x))75proof76  obtain ⟨_, i, _, cases⟩ := member77  rcases cases with78    ⟨same, shape⟩ | ⟨same, shape⟩ | ⟨notC, notK, shape⟩79  . obtain ⟨xi, yA⟩ := orderedPair.injective with shape80    left81    rw xi82    exact ⟨same, yA⟩83  . obtain ⟨xi, yB⟩ := orderedPair.injective with shape84    right85    left86    rw xi87    exact ⟨same, yB⟩88  . obtain ⟨xi, yC⟩ := orderedPair.injective with shape89    right90    right91    rw xi92    exact ⟨notC, notK, yC⟩9394theorem exchange.function (E T e f : Set, c k : Nat)95  requires decomposition : Decomposition(E, T, succ(k))96  requires colour : c ∈ k97  requires first : e ∈ T(k)98  requires second : f ∈ T(c)99  shows exchange(E, T, e, f, c, k) : succ(k) → 𝒫(E)100proof101  obtain ⟨distinct, _, swappedC, swappedK⟩ :=102    exchange.setting with decomposition, colour, first, second103  constructor104  . intros p member105    exact member.left106  constructor107  . intros x y relatedY z relatedZ108    have shapeY := exchange.shape with relatedY109    have shapeZ := exchange.shape with relatedZ110    -- In each of the nine cases the two values agree or the indices clash.111    rcases shapeY with ⟨xc, yA⟩ | ⟨xk, yB⟩ | ⟨xnc, xnk, yC⟩112    . rcases shapeZ with ⟨zc, zA⟩ | ⟨zk, zB⟩ | ⟨znc, znk, zC⟩; . cc; . cc; . cc113    . rcases shapeZ with ⟨zc, zA⟩ | ⟨zk, zB⟩ | ⟨znc, znk, zC⟩; . cc; . cc; . cc114    . rcases shapeZ with ⟨zc, zA⟩ | ⟨zk, zB⟩ | ⟨znc, znk, zC⟩; . cc; . cc; . cc115  . intros x input116    by_cases xc : x = c117    . refine ⟨(T(c) ∪ {e}) ∖ {f}, swappedC, ?_⟩118      unfold relates119      refine ⟨(product.pair with input, swappedC), x, input, ?_⟩120      left121      exact ⟨xc, rfl⟩122    by_cases xk : x = k123    . refine ⟨(T(k) ∪ {f}) ∖ {e}, swappedK, ?_⟩124      unfold relates125      refine ⟨(product.pair with input, swappedK), x, input, ?_⟩126      right127      left128      exact ⟨xk, rfl⟩129    have class := FunctionBetween.apply_closed with decomposition.left, input130    refine ⟨T(x), class, ?_⟩131    unfold relates132    refine ⟨(product.pair with input, class), x, input, ?_⟩133    right134    right135    exact ⟨xc, xk, rfl⟩136137theorem exchange.value_colour (E T e f : Set, c k : Nat)138  requires decomposition : Decomposition(E, T, succ(k))139  requires colour : c ∈ k140  requires first : e ∈ T(k)141  requires second : f ∈ T(c)142  shows exchange(E, T, e, f, c, k)(c) = (T(c) ∪ {e}) ∖ {f}143proof144  obtain ⟨_, _, swappedC, _⟩ :=145    exchange.setting with decomposition, colour, first, second146  have cIn : c ∈ succ(k) by simp [colour]147  have function := exchange.function with decomposition, colour, first, second148  have related : relates(exchange(E, T, e, f, c, k), c, (T(c) ∪ {e}) ∖ {f})149    unfold relates150    refine ⟨(product.pair with cIn, swappedC), c, cIn, ?_⟩151    left152    exact ⟨rfl, rfl⟩153  exact FunctionBetween.apply_value with function, cIn, related154155theorem exchange.value_last (E T e f : Set, c k : Nat)156  requires decomposition : Decomposition(E, T, succ(k))157  requires colour : c ∈ k158  requires first : e ∈ T(k)159  requires second : f ∈ T(c)160  shows exchange(E, T, e, f, c, k)(k) = (T(k) ∪ {f}) ∖ {e}161proof162  obtain ⟨_, _, _, swappedK⟩ :=163    exchange.setting with decomposition, colour, first, second164  have kIn : k ∈ succ(k) by simp165  have function := exchange.function with decomposition, colour, first, second166  have related : relates(exchange(E, T, e, f, c, k), k, (T(k) ∪ {f}) ∖ {e})167    unfold relates168    refine ⟨(product.pair with kIn, swappedK), k, kIn, ?_⟩169    right170    left171    exact ⟨rfl, rfl⟩172  exact FunctionBetween.apply_value with function, kIn, related173174theorem exchange.value_other (E T e f : Set, c k i : Nat)175  requires decomposition : Decomposition(E, T, succ(k))176  requires colour : c ∈ k177  requires first : e ∈ T(k)178  requires second : f ∈ T(c)179  requires index : i ∈ succ(k)180  requires notC : i ≠ c181  requires notK : i ≠ k182  shows exchange(E, T, e, f, c, k)(i) = T(i)183proof184  have function := exchange.function with decomposition, colour, first, second185  have class := FunctionBetween.apply_closed with decomposition.left, index186  have related : relates(exchange(E, T, e, f, c, k), i, T(i))187    unfold relates188    refine ⟨(product.pair with index, class), i, index, ?_⟩189    right190    right191    exact ⟨notC, notK, rfl⟩192  exact FunctionBetween.apply_value with function, index, related193194-- An edge lies in the exchanged class of a colour when it is e and the195-- colour is c, f and the colour is k, or neither edge and of that colour.196theorem exchange.class_membership (E T e f g : Set, c k i : Nat)197  requires decomposition : Decomposition(E, T, succ(k))198  requires colour : c ∈ k199  requires first : e ∈ T(k)200  requires second : f ∈ T(c)201  requires index : i ∈ succ(k)202  shows g ∈ exchange(E, T, e, f, c, k)(i) ↔203    (g = e ∧ i = c) ∨ (g = f ∧ i = k) ∨204    (g ≠ e ∧ g ≠ f ∧ g ∈ T(i))205proof206  obtain ⟨distinct, edges, _, _⟩ :=207    exchange.setting with decomposition, colour, first, second208  have cIn : c ∈ succ(k) by simp [colour]209  have kIn : k ∈ succ(k) by simp210  have eNotC : ¬e ∈ T(c)211    intro inC212    exact distinct with213      (Decomposition.colour_unique with decomposition, cIn, kIn, inC, first)214  have fNotK : ¬f ∈ T(k)215    intro inK216    exact distinct with217      (Decomposition.colour_unique with decomposition, cIn, kIn, second, inK)218  by_cases ic : i = c219  . rw [ic, (exchange.value_colour with decomposition, colour, first, second)]220    constructor221    . intro member222      simp [union2.membership, singleton.membership] at member223      rcases member with ⟨inC | same, notF⟩224      . right225        right226        refine ⟨?_, notF, inC⟩227        intro same228        rw same at inC229        exact eNotC with inC230      . left231        exact ⟨same, rfl⟩232    . intro cases233      rcases cases with ⟨same, _⟩ | ⟨_, ck⟩ | ⟨_, notF, inC⟩234      . rw same235        simp [edges]236      . exfalso237        exact distinct with ck238      . simp [inC, notF]239  by_cases ik : i = k240  . rw [ik, (exchange.value_last with decomposition, colour, first, second)]241    constructor242    . intro member243      simp [union2.membership, singleton.membership] at member244      rcases member with ⟨inK | same, notE⟩245      . right246        right247        refine ⟨notE, ?_, inK⟩248        intro same249        rw same at inK250        exact fNotK with inK251      . right252        left253        exact ⟨same, rfl⟩254    . intro cases255      rcases cases with ⟨_, kc⟩ | ⟨same, _⟩ | ⟨notE, _, inK⟩256      . exfalso257        cc258      . rw same259        have different : f ≠ e by cc260        simp [different]261      . simp [inK, notE]262  rw (exchange.value_other with263    decomposition, colour, first, second, index, ic, ik)264  constructor265  . intro inT266    right267    right268    refine ⟨?_, ?_, inT⟩269    . intro same270      rw same at inT271      exact ik with (Decomposition.colour_unique with272        decomposition, index, kIn, inT, first)273    . intro same274      rw same at inT275      exact ic with (Decomposition.colour_unique with276        decomposition, index, cIn, inT, second)277  . intro cases278    rcases cases with ⟨_, same⟩ | ⟨_, same⟩ | ⟨_, _, inT⟩279    . exfalso280      exact ic with same281    . exfalso282      exact ik with same283    . exact inT284285theorem exchange.decomposition (V E leftEnd rightEnd T e f : Set, c k : Nat)286  requires decomposition : Decomposition(E, T, succ(k))287  requires colour : c ∈ k288  requires first : e ∈ T(k)289  requires second : f ∈ T(c)290  shows Decomposition(E, exchange(E, T, e, f, c, k), succ(k))291proof292  obtain ⟨_, edges, _, _⟩ :=293    exchange.setting with decomposition, colour, first, second294  have cIn : c ∈ succ(k) by simp [colour]295  have kIn : k ∈ succ(k) by simp296  refine ⟨(exchange.function with decomposition, colour, first, second),297    ?_, ?_⟩298  -- Every edge keeps a colour: e moves to c, f to k, the rest stay.299  . intros g inE300    by_cases ge : g = e301    . refine ⟨c, cIn, ?_⟩302      rw exchange.class_membership with303        decomposition, colour, first, second, cIn304      left305      exact ⟨ge, rfl⟩306    by_cases gf : g = f307    . refine ⟨k, kIn, ?_⟩308      rw exchange.class_membership with309        decomposition, colour, first, second, kIn310      right311      left312      exact ⟨gf, rfl⟩313    obtain ⟨i, index, inT⟩ := decomposition.right.left with g, inE314    have natural := natural.member at succ(k) with i, index315    refine ⟨i, index, ?_⟩316    rw exchange.class_membership with317      decomposition, colour, first, second, index318    right319    right320    exact ⟨ge, gf, inT⟩321  -- And only one colour, as under T.322  . intros i indexI j indexJ different323    have naturalI := natural.member at succ(k) with i, indexI324    have naturalJ := natural.member at succ(k) with j, indexJ325    apply Disjoint.iff.backward326    intros g inI inJ327    rw exchange.class_membership with328      decomposition, colour, first, second, indexI at inI329    rw exchange.class_membership with330      decomposition, colour, first, second, indexJ at inJ331    rcases inI with ⟨ge, ic⟩ | ⟨gf, ik⟩ | ⟨notE, notF, inTi⟩332    . rcases inJ with ⟨_, jc⟩ | ⟨gf, _⟩ | ⟨notE, _, _⟩333      . cc334      . cc335      . exact notE with ge336    . rcases inJ with ⟨ge, _⟩ | ⟨_, jk⟩ | ⟨_, notF, _⟩337      . cc338      . cc339      . exact notF with gf340    . rcases inJ with ⟨ge, _⟩ | ⟨gf, _⟩ | ⟨_, _, inTj⟩341      . exact notE with ge342      . exact notF with gf343      . exact different with344          (Decomposition.colour_unique with345            decomposition, indexI, indexJ, inTi, inTj)346