CubicPathwidth.Alg.Proofs2.R1ReduceFuel

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

import CubicPathwidth.Alg.Plan2
import CubicPathwidth.Alg.Proofs.Targets

/-!
# R1: `reduce_record` never runs out of fuel

Task R1 of the formalisation (§6.2, statement `ReduceRecordNoFallback` of
`Spec.lean` §7). Proves

* `reduceLoop_flag_false`: for every fuel, if `|stack| + 2·numNodes ≤ fuel` then the
  flag of `reduceLoop` is `false` (general lemma, any well-formed start graph);
* `reduceRecordNoFallback : ReduceRecordNoFallback`, from fuel `3·numNodes + 1` and
  `|initial stack| ≤ numNodes`.

Measure. `μ(G, stack) = |stack| + 2·numNodes(G)`. A skipped pop decreases `|stack|` by
one. A reduction at `v` (a node with `≤ 2` neighbours) removes one node and pushes the
`≤ 2` neighbours: `μ` drops by at least one.

Reusable helpers (namespace `CubicPathwidth.Alg.R1`): `length_eq_of_mem_iff`,
`numNodes_removeNode`, `stepL`, `stepL_props`, `redStep_wf_numNodes`, `redStep_eq`,
`reduceLoop_red_eq`, `reduceLoop_flag_false`.
-/

noncomputable section

namespace CubicPathwidth.Alg

open Graph

namespace R1

/-- Two lists without repeats and with the same members have the same length. -/
theorem length_eq_of_mem_iff {l l' : List Nat} (hl : l.Nodup) (hl' : l'.Nodup)
    (h : ∀ x, x ∈ l ↔ x ∈ l') : l.length = l'.length :=
  ((List.perm_ext_iff_of_nodup hl hl').2 h).length_eq

/-- Two well-formed graphs with the same nodes have the same number of nodes. -/
theorem numNodes_eq_of_mem_iff {G H : Graph} (hG : G.WF) (hH : H.WF)
    (h : ∀ x, x ∈ G.nodes ↔ x ∈ H.nodes) : G.numNodes = H.numNodes :=
  length_eq_of_mem_iff hG.nodup hH.nodup h

/-- Removing a node lowers the node count by one. -/
theorem numNodes_removeNode {G : Graph} (hG : G.WF) {v : Nat} (hv : v ∈ G.nodes) :
    (G.removeNode v).numNodes + 1 = G.numNodes := by
  have hR := removeNodeSpec G v hG
  have hperm : (G.removeNode v).nodes.length = (G.nodes.erase v).length :=
    length_eq_of_mem_iff hR.1.nodup (hG.nodup.erase v) (fun x => by
      rw [hR.2.1 x, hG.nodup.mem_erase_iff]
      tauto)
  simp only [Graph.numNodes]
  rw [hperm, List.length_erase_of_mem hv]
  have := List.length_pos_of_mem hv
  omega

/-- The graph part of one step of `reduceLoop` (`G1` = `G` after `removeNode v`, `nb`
= the neighbour list of `v`). Same as `C5.stepG`. -/
def stepL (G1 : Graph) (nb : List Nat) : Graph :=
  match nb with
  | [a, b] => G1.addEdge a b
  | _ => G1

theorem redStep_eq (G : Graph) (v : Nat) :
    redStep G v = stepL (G.removeNode v) (G.nbrs v) := rfl

/-- A reduction step on a well-formed graph keeps well-formedness; the node count is
unchanged when the neighbours are nodes of `G1` (distinct). -/
theorem stepL_props {G1 : Graph} (hG1 : G1.WF) {nb : List Nat} (hnd : nb.Nodup)
    (hl : ∀ a ∈ nb, a ∈ G1.nodes) :
    (stepL G1 nb).WF ∧ (stepL G1 nb).numNodes = G1.numNodes := by
  rcases nb with _ | ⟨a, _ | ⟨b, _ | ⟨c, t⟩⟩⟩
  · exact ⟨hG1, rfl⟩
  · exact ⟨hG1, rfl⟩
  · have hab : a ≠ b := by
      intro h
      subst h
      simp at hnd
    have ha : a ∈ G1.nodes := hl a (by simp)
    have hb : b ∈ G1.nodes := hl b (by simp)
    obtain ⟨hw, hn, _⟩ := addEdgeSpec G1 a b hG1 hab
    have hcount : (G1.addEdge a b).numNodes = G1.numNodes := by
      apply numNodes_eq_of_mem_iff hw hG1
      intro x
      rw [hn x]
      constructor
      · rintro (h | rfl | rfl)
        · exact h
        · exact ha
        · exact hb
      · intro h
        exact Or.inl h
    exact ⟨hw, hcount⟩
  · exact ⟨hG1, rfl⟩

/-- `redStep` keeps well-formedness and removes exactly one node, for `v` a node. -/
theorem redStep_wf_numNodes {G : Graph} (hG : G.WF) {v : Nat} (hv : v ∈ G.nodes) :
    (redStep G v).WF ∧ (redStep G v).numNodes + 1 = G.numNodes := by
  have hRem := removeNodeSpec G v hG
  have hl : ∀ a ∈ G.nbrs v, a ∈ (G.removeNode v).nodes := by
    intro a ha
    have hav : a ≠ v := fun h => hG.loopless v (h ▸ ha)
    exact (hRem.2.1 a).2 ⟨hG.nbrs_sub v a ha, hav⟩
  obtain ⟨hw, hcount⟩ := stepL_props hRem.1 (hG.nbrs_nodup v) hl
  refine ⟨?_, ?_⟩
  · rw [redStep_eq]
    exact hw
  · rw [redStep_eq, hcount]
    exact numNodes_removeNode hG hv

/-- One non-skipped pop of `reduceLoop`, written with `redStep`. -/
theorem reduceLoop_red_eq (fuel : Nat) (G : Graph) (v : Nat) (rest : List Nat)
    (opsRev : List Op) (hm : G.mem v = true) (hd : G.degree v ≤ 2) :
    reduceLoop (fuel + 1) G (v :: rest) opsRev =
      reduceLoop fuel (redStep G v) ((G.nbrs v).reverse ++ rest)
        (Op.red v (G.nbrs v) :: opsRev) := by
  have hc : (!G.mem v || decide (G.degree v > 2)) = false := by
    simp only [hm, Bool.not_true, Bool.false_or, decide_eq_false_iff_not, not_lt]
    exact hd
  simp only [reduceLoop, hc, Bool.false_eq_true, ↓reduceIte]
  rfl

/-- The general measure lemma: if `|stack| + 2·numNodes ≤ fuel`, then the loop never
runs out of fuel. -/
theorem reduceLoop_flag_false : ∀ (fuel : Nat) (G : Graph) (stack : List Nat)
    (opsRev : List Op), G.WF → stack.length + 2 * G.numNodes ≤ fuel →
    (reduceLoop fuel G stack opsRev).2.2 = false
  | 0, G, stack, opsRev, _, hfuel => by
      cases stack with
      | nil => rfl
      | cons v rest =>
        exfalso
        simp only [List.length_cons] at hfuel
        omega
  | fuel + 1, G, stack, opsRev, hG, hfuel => by
      cases stack with
      | nil => rfl
      | cons v rest =>
        simp only [List.length_cons] at hfuel
        by_cases hm : G.mem v = true
        · by_cases hd : G.degree v ≤ 2
          · -- a reduction
            rw [reduceLoop_red_eq fuel G v rest opsRev hm hd]
            obtain ⟨hw, hcount⟩ := redStep_wf_numNodes hG ((hG.mem_iff v).1 hm)
            apply reduceLoop_flag_false fuel (redStep G v) _ _ hw
            have hlen : (G.nbrs v).length ≤ 2 := hd
            simp only [List.length_append, List.length_reverse]
            omega
          · -- degree above two: the pop is skipped
            have hc : (!G.mem v || decide (G.degree v > 2)) = true := by
              simp only [hm, Bool.not_true, Bool.false_or, decide_eq_true_eq]
              omega
            have hskip : reduceLoop (fuel + 1) G (v :: rest) opsRev =
                reduceLoop fuel G rest opsRev := by
              simp only [reduceLoop, hc, ↓reduceIte]
            rw [hskip]
            apply reduceLoop_flag_false fuel G rest opsRev hG
            omega
        · -- not a node: skipped
          have hm' : G.mem v = false := by simpa using hm
          have hc : (!G.mem v || decide (G.degree v > 2)) = true := by
            simp [hm']
          have hskip : reduceLoop (fuel + 1) G (v :: rest) opsRev =
              reduceLoop fuel G rest opsRev := by
            simp only [reduceLoop, hc, ↓reduceIte]
          rw [hskip]
          apply reduceLoop_flag_false fuel G rest opsRev hG
          omega

/-- `reduce_record` (`reduceRecordF`) never falls back. The initial stack has at most
`numNodes` entries and the fuel is `3·numNodes + 1`. -/
theorem reduceRecordNoFallback_aux : ∀ G : Graph, G.WF → (reduceRecordF G).2.2 = false := by
  intro G hG
  unfold reduceRecordF
  apply reduceLoop_flag_false _ G _ [] hG
  have hfilt := List.length_filter_le (fun v => decide (G.degree v ≤ 2)) G.nodes
  simp only [List.length_reverse]
  simp only [Graph.numNodes]
  omega

end R1

/-- `reduce_record` never falls back (`Spec.lean` §7). -/
theorem reduceRecordNoFallback : ReduceRecordNoFallback :=
  R1.reduceRecordNoFallback_aux

#print axioms reduceRecordNoFallback

end CubicPathwidth.Alg