CubicPathwidth.Alg.Proofs2.N2AlgoT1NoFallback

Source file CubicPathwidth/Alg/Proofs2/N2AlgoT1NoFallback.lean of the Lean project (how it is built).

import CubicPathwidth.Alg.Plan2

/-!
# N2: `AlgoT1NoFallback` (Spec.lean §7), from the connector statement

Route. The flag of `algo_T1` is the flag of `connector_order` applied to
`Qs = G.nodes.filter Wp` and the items `P.map e`, where `P` are the vertices of `Up \ D`
with a neighbour in `Wp`, and `e u = (G.nbrs u).filter Wp`. Each item is nodup, nonempty
(`u ∈ P` has a `Wp`-neighbour), inside `Qs`, and has at most two elements: if `u` had three
`Wp`-neighbours, then `deg u = 3` (degree bound) and all three neighbours are non-low,
so `inD u` holds, contradicting `u ∉ D`.

The statement is `algoT1NoFallback_of (hN : ConnectorNoFallback)`; the hypothesis is
the Stage 2 task N1.
-/

namespace CubicPathwidth.Alg

open Graph

theorem and_true_iff' (a b : Bool) : (a && b) = true ↔ a = true ∧ b = true := by
  cases a <;> cases b <;> simp

/-- The items of `switched_layout` have one or two elements, inside `Wp`. -/
theorem switched_items_ok (G : Graph) (hG : G.WF) (hdeg : G.MaxDegLE 3) (Y : Labels) :
    ∀ e' ∈ ((G.nodes.filter fun u => inU G Y u && !inD G Y u &&
        (G.nbrs u).any (fun x => inW G Y x && !inD G Y x)).map
          fun u => (G.nbrs u).filter (fun x => inW G Y x && !inD G Y x)),
      e'.Nodup ∧ 1 ≤ e'.length ∧ e'.length ≤ 2 ∧
        ∀ z ∈ e', z ∈ G.nodes.filter (fun x => inW G Y x && !inD G Y x) := by
  intro e' he'
  obtain ⟨u, hu, rfl⟩ := List.mem_map.mp he'
  obtain ⟨hu1, hu2⟩ := List.mem_filter.mp hu
  obtain ⟨hA, hany⟩ := (and_true_iff' _ _).mp hu2
  obtain ⟨hinU, hnDn⟩ := (and_true_iff' _ _).mp hA
  have hnD : inD G Y u = false := by simpa using hnDn
  have hlowU : isLow Y u = true := by
    have h := hinU
    unfold inU at h
    exact ((and_true_iff' _ _).mp h).1
  have hnd : ((G.nbrs u).filter (fun x => inW G Y x && !inD G Y x)).Nodup :=
    List.Nodup.filter _ (hG.nbrs_nodup u)
  have hpos : 1 ≤ ((G.nbrs u).filter (fun x => inW G Y x && !inD G Y x)).length := by
    obtain ⟨x, hx, hWx⟩ := List.any_eq_true.mp hany
    exact List.length_pos_of_mem (List.mem_filter.mpr ⟨hx, hWx⟩)
  have hsub : ∀ z ∈ (G.nbrs u).filter (fun x => inW G Y x && !inD G Y x),
      z ∈ G.nodes.filter (fun x => inW G Y x && !inD G Y x) := by
    intro z hz
    obtain ⟨hz1, hz2⟩ := List.mem_filter.mp hz
    exact List.mem_filter.mpr ⟨hG.nbrs_sub u z hz1, hz2⟩
  have hle : ((G.nbrs u).filter (fun x => inW G Y x && !inD G Y x)).length ≤ 2 := by
    have hdu : G.degree u ≤ 3 := hdeg u hu1
    have hlenF := List.length_filter_le (fun x => inW G Y x && !inD G Y x) (G.nbrs u)
    have hdeg_eq : (G.nbrs u).length = G.degree u := rfl
    by_cases hall : ∀ x ∈ G.nbrs u, (inW G Y x && !inD G Y x) = true
    · by_cases h2 : G.degree u ≤ 2
      · omega
      · exfalso
        have hd3 : G.degree u = 3 := by omega
        have hallx : (G.nbrs u).all (fun x => isLow Y x != isLow Y u) = true := by
          rw [List.all_eq_true]
          intro x hx
          have hWx' : inW G Y x = true := ((and_true_iff' _ _).mp (hall x hx)).1
          have hlowx : isLow Y x = false := by
            have h2' := hWx'
            unfold inW at h2'
            have h3 := ((and_true_iff' _ _).mp h2').1
            simpa using h3
          rw [hlowx, hlowU]
          rfl
        have hinDu : inD G Y u = true := by
          unfold inD
          exact (and_true_iff' _ _).mpr ⟨beq_iff_eq.mpr hd3, hallx⟩
        rw [hinDu] at hnD
        exact Bool.noConfusion hnD
    · have hex : ∃ x ∈ G.nbrs u, ¬ ((inW G Y x && !inD G Y x) = true) := by
        by_contra hcon
        exact hall (fun x hx => by
          by_contra h'
          exact hcon ⟨x, hx, h'⟩)
      obtain ⟨x, hx, hWx⟩ := hex
      have hlt : ((G.nbrs u).filter (fun x => inW G Y x && !inD G Y x)).length <
          (G.nbrs u).length :=
        List.length_filter_lt_length_iff_exists.mpr ⟨x, hx, hWx⟩
      omega
  exact ⟨hnd, hpos, hle, hsub⟩

/-- Theorem 1 algorithm: no fallback for maximum degree at most three. -/
theorem algoT1NoFallback_of (hN : ConnectorNoFallback) : AlgoT1NoFallback := by
  intro G hG hdeg Y
  have hQs : (G.nodes.filter fun x => inW G Y x && !inD G Y x).Nodup :=
    List.Nodup.filter _ hG.nodup
  have key := hN (G.nodes.filter fun x => inW G Y x && !inD G Y x)
    ((G.nodes.filter fun u => inU G Y u && !inD G Y u &&
        (G.nbrs u).any (fun x => inW G Y x && !inD G Y x)).map
          fun u => (G.nbrs u).filter (fun x => inW G Y x && !inD G Y x))
    hQs (switched_items_ok G hG hdeg Y)
  unfold algoT1F switchedLayoutF
  exact key

end CubicPathwidth.Alg

#print axioms CubicPathwidth.Alg.algoT1NoFallback_of
Back to top