Round-six κ development, definitions part 10

-- Round-six κ development (integer-multiplication-kappa), generated by skeleton subtraction.

import Definitions.Def_IntMul_Kappa_K_Defs33
import Definitions.Def_IntMul_Kappa_R6_Defs1
import Mathlib
import Definitions.Def_IntMul_HvdH_M_Defs8
import Definitions.Def_IntMul_MultitapeModel
import Definitions.Def_IntMul_HvdH_M_Defs1
import Definitions.Def_IntMul_HvdH_M_Defs2

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

section
-- Source module: NLogN.Logic
/-!
# Program logic for stack programs

`Runs I prog s σ σ' c`: `s` takes `σ` to `σ'` with cost at most `c`.  Besides the rules for each
statement this file provides

* `caseTops`: branch on the tops of several stacks (constant cost);
* `opsStmt`: straight-line lists of primitive operations;
* `machine`: a finite-state transducer whose state lives on a dedicated stack; its correctness
  reduces to iterating a plain Lean function `mstep`.
-/

namespace NLogN

variable {S P : ℕ} {I : List Sym} {prog : Fin P → Stmt S P}

namespace Runs

theorem mono {s : Stmt S P} {σ σ' : St S} {c c' : ℕ} (h : Runs I prog s σ σ' c) (hc : c ≤ c') :
    Runs I prog s σ σ' c' := by
  obtain ⟨d, hd, h⟩ := h; exact ⟨d, by omega, h⟩

theorem mono' {s : Stmt S P} {σ σ' σ'' : St S} {c c' : ℕ} (h : Runs I prog s σ σ' c)
    (he : σ' = σ'') (hc : c ≤ c') : Runs I prog s σ σ'' c' := he ▸ h.mono hc

theorem skip (σ : St S) : Runs I prog .skip σ σ 1 := ⟨1, le_rfl, .skip σ⟩
theorem push (σ : St S) (i a) : Runs I prog (.push i a) σ (σ.push i a) 1 := ⟨1, le_rfl, .push σ i a⟩
theorem pop (σ : St S) (i) : Runs I prog (.pop i) σ (σ.pop i) 1 := ⟨1, le_rfl, .pop σ i⟩
theorem inRd (σ : St S) (i) : Runs I prog (.inRd i) σ (σ.inRd I i) 1 := ⟨1, le_rfl, .inRd σ i⟩
theorem out (σ : St S) (b) : Runs I prog (.out b) σ (σ.outB b) 1 := ⟨1, le_rfl, .out σ b⟩

theorem seq {p q : Stmt S P} {σ σ₁ σ₂ : St S} {c₁ c₂ : ℕ} (h₁ : Runs I prog p σ σ₁ c₁)
    (h₂ : Runs I prog q σ₁ σ₂ c₂) : Runs I prog (.seq p q) σ σ₂ (c₁ + c₂) := by
  obtain ⟨d₁, hd₁, h₁⟩ := h₁; obtain ⟨d₂, hd₂, h₂⟩ := h₂
  exact ⟨d₁ + d₂, by omega, .seq h₁ h₂⟩

theorem iteT {i f} {p q : Stmt S P} {σ σ' : St S} {c : ℕ} (hf : f (σ.top i) = true)
    (h : Runs I prog p σ σ' c) : Runs I prog (.ite i f p q) σ σ' (c + 1) := by
  obtain ⟨d, hd, h⟩ := h; exact ⟨d + 1, by omega, .iteT hf h⟩

theorem iteF {i f} {p q : Stmt S P} {σ σ' : St S} {c : ℕ} (hf : f (σ.top i) = false)
    (h : Runs I prog q σ σ' c) : Runs I prog (.ite i f p q) σ σ' (c + 1) := by
  obtain ⟨d, hd, h⟩ := h; exact ⟨d + 1, by omega, .iteF hf h⟩

theorem call {j : Fin P} {σ σ' : St S} {c : ℕ} (h : Runs I prog (prog j) σ σ' c) :
    Runs I prog (.call j) σ σ' (c + 2) := by
  obtain ⟨d, hd, h⟩ := h; exact ⟨d + 2, by omega, .call h⟩

theorem loopF {i f} {p : Stmt S P} {σ : St S} (hf : f (σ.top i) = false) :
    Runs I prog (.loop i f p) σ σ 1 := ⟨1, le_rfl, .loopF hf⟩

/-- A loop running through the states `σs 0, σs 1, …, σs m`. -/
theorem loop {i f} {p : Stmt S P} (σs : ℕ → St S) (cs : ℕ → ℕ) (m : ℕ)
    (hT : ∀ k < m, f ((σs k).top i) = true) (hF : f ((σs m).top i) = false)
    (hb : ∀ k < m, Runs I prog p (σs k) (σs (k + 1)) (cs k)) :
    Runs I prog (.loop i f p) (σs 0) (σs m) ((∑ k ∈ Finset.range m, (cs k + 1)) + 1) := by
  suffices H : ∀ r j, j + r = m → Runs I prog (.loop i f p) (σs j) (σs m)
      ((∑ k ∈ Finset.Ico j m, (cs k + 1)) + 1) by
    have := H m 0 (by omega)
    rwa [Finset.range_eq_Ico]
  intro r
  induction r with
  | zero => intro j hj; subst hj; simpa using loopF hF
  | succ r ih =>
    intro j hj
    have hjm : j < m := by omega
    obtain ⟨d₁, hd₁, h₁⟩ := hb j hjm
    obtain ⟨d₂, hd₂, h₂⟩ := ih (j + 1) (by omega)
    refine ⟨d₁ + d₂ + 1, ?_, .loopT (hT j hjm) h₁ h₂⟩
    rw [Finset.sum_eq_sum_Ico_succ_bot hjm]
    omega

/-- Loop with a uniform bound on the cost of each iteration. -/
theorem loop' {i f} {p : Stmt S P} (σs : ℕ → St S) (c m : ℕ)
    (hT : ∀ k < m, f ((σs k).top i) = true) (hF : f ((σs m).top i) = false)
    (hb : ∀ k < m, Runs I prog p (σs k) (σs (k + 1)) c) :
    Runs I prog (.loop i f p) (σs 0) (σs m) (m * (c + 1) + 1) := by
  have := loop σs (fun _ => c) m hT hF hb
  simpa [Finset.sum_const, Finset.card_range, smul_eq_mul] using this

end Runs

/-! ## Branching on stack tops -/

theorem Runs.caseList {i : Fin S} {k : Option Sym → Stmt S P} {σ σ' : St S} {c : ℕ} {a : Sym}
    (ha : σ.top i = some a) (h : Runs I prog (k (some a)) σ σ' c) :
    ∀ l : List Sym, a ∈ l → Runs I prog (NLogN.caseList i k l) σ σ' (c + l.length) := by
  intro l hl
  induction l with
  | nil => simp at hl
  | cons b l ih =>
    simp only [NLogN.caseList, List.length_cons]
    by_cases hb : a = b
    · subst hb
      exact (Runs.iteT (by simp [ha]) h).mono (by omega)
    · have hl' : a ∈ l := by simpa [hb] using hl
      exact (Runs.iteF (by simp [ha, hb]) (ih hl')).mono (by omega)

theorem Runs.caseTop {i : Fin S} {k : Option Sym → Stmt S P} {σ σ' : St S} {c : ℕ}
    (h : Runs I prog (k (σ.top i)) σ σ' c) : Runs I prog (NLogN.caseTop i k) σ σ' (c + 17) := by
  unfold NLogN.caseTop
  rcases ht : σ.top i with _ | a
  · rw [ht] at h; exact (Runs.iteT (by simp [ht]) h).mono (by omega)
  · rw [ht] at h
    have := Runs.caseList ht h (List.finRange 16) (List.mem_finRange a)
    exact (Runs.iteF (by simp [ht]) this).mono (by simp)

theorem Runs.caseTops {σ σ' : St S} {c : ℕ} :
    ∀ (w : List (Fin S)) (k : List (Option Sym) → Stmt S P),
      Runs I prog (k (σ.tops w)) σ σ' c →
        Runs I prog (NLogN.caseTops w k) σ σ' (c + 17 * w.length)
  | [], k, h => by simpa [NLogN.caseTops, St.tops] using h
  | i :: w, k, h => by
    simp only [NLogN.caseTops, List.length_cons]
    have := Runs.caseTops w (fun os => k (σ.top i :: os)) (by simpa [St.tops] using h)
    exact (Runs.caseTop this).mono (by ring_nf; omega)

/-! ## Straight-line operations -/

theorem Runs.op (o : Op S) (σ : St S) : Runs I prog (o.stmt : Stmt S P) σ (o.run I σ) 1 := by
  cases o <;> simp only [Op.stmt, Op.run]
  · exact Runs.push _ _ _
  · exact Runs.pop _ _
  · exact Runs.inRd _ _
  · exact Runs.out _ _

theorem Runs.ops : ∀ (l : List (Op S)) (σ : St S),
    Runs I prog (opsStmt l : Stmt S P) σ (runOps I l σ) (l.length + 1)
  | [], σ => by simpa [opsStmt, runOps] using Runs.skip σ
  | o :: l, σ => by
    simp only [opsStmt, runOps, List.length_cons]
    exact (Runs.seq (Runs.op o σ) (Runs.ops l _)).mono (by omega)

/-! ## Finite-state transducers -/

theorem Runs.machine {q : Fin S} {w : List (Fin S)} {q0 : Sym}
    {δ : List (Option Sym) → List (Op S)} (B : ℕ) (hB : ∀ os, (δ os).length ≤ B)
    (σ : St S) (m : ℕ)
    (hrun : ∀ k < m, ((mstep I q w δ)^[k] (σ.push q q0)).top q ≠ some hlt)
    (hstop : ((mstep I q w δ)^[m] (σ.push q q0)).top q = some hlt) :
    Runs I prog (NLogN.machine q w q0 δ : Stmt S P) σ
      (((mstep I q w δ)^[m] (σ.push q q0)).pop q) (m * (B + 17 * w.length + 19) + 3) := by
  unfold NLogN.machine
  have hl := Runs.loop' (I := I) (prog := prog) (i := q) (f := fun o => decide (o ≠ some hlt))
    (p := NLogN.caseTops (q :: w) fun os => opsStmt (δ os))
    (fun k => (mstep I q w δ)^[k] (σ.push q q0)) (B + 17 * w.length + 18) m
    (fun k hk => by simpa using hrun k hk) (by simpa using hstop) (fun k _ => by
      rw [Function.iterate_succ_apply']
      have := Runs.ops (I := I) (prog := prog) (δ (((mstep I q w δ)^[k] (σ.push q q0)).tops
        (q :: w))) ((mstep I q w δ)^[k] (σ.push q q0))
      have h2 := Runs.caseTops (I := I) (prog := prog) (q :: w) (fun os => opsStmt (δ os)) this
      refine h2.mono ?_
      have := hB (((mstep I q w δ)^[k] (σ.push q q0)).tops (q :: w))
      simp only [List.length_cons]; omega)
  simp only [Function.iterate_zero, id] at hl
  have := Runs.seq (Runs.push (I := I) (prog := prog) σ q q0)
    (Runs.seq hl (Runs.pop (I := I) (prog := prog) _ q))
  exact this.mono (by ring_nf; omega)

end NLogN

namespace NLogN

variable {S P : ℕ} {I : List Sym} {prog : Fin P → Stmt S P}

end NLogN

namespace NLogN

variable {S P : ℕ} {I : List Sym} {prog : Fin P → Stmt S P}

namespace Reaches

variable {q : Fin S} {w : List (Fin S)} {δ : List (Option Sym) → List (Op S)}

theorem refl (σ : St S) : Reaches I q w δ σ σ 0 := ⟨rfl, fun _ h => absurd h (by omega)⟩

theorem step {σ σf : St S} {m : ℕ} (h : σ.top q ≠ some hlt)
    (h' : Reaches I q w δ (mstep I q w δ σ) σf m) : Reaches I q w δ σ σf (m + 1) := by
  refine ⟨by rw [Function.iterate_succ_apply]; exact h'.1, fun k hk => ?_⟩
  rcases k with _ | k
  · simpa using h
  · rw [Function.iterate_succ_apply]; exact h'.2 k (by omega)

theorem step' {σ σ₁ σf : St S} {m : ℕ} (h : σ.top q ≠ some hlt) (e : mstep I q w δ σ = σ₁)
    (h' : Reaches I q w δ σ₁ σf m) : Reaches I q w δ σ σf (m + 1) := step h (e ▸ h')

theorem trans {σ σ₁ σf : St S} {m₁ m₂ : ℕ} (h₁ : Reaches I q w δ σ σ₁ m₁)
    (h₂ : Reaches I q w δ σ₁ σf m₂) : Reaches I q w δ σ σf (m₁ + m₂) := by
  refine ⟨by rw [add_comm, Function.iterate_add_apply, h₁.1, h₂.1], fun k hk => ?_⟩
  by_cases hk1 : k < m₁
  · exact h₁.2 k hk1
  · obtain ⟨j, rfl⟩ := Nat.exists_eq_add_of_le (not_lt.mp hk1)
    rw [add_comm, Function.iterate_add_apply, h₁.1]; exact h₂.2 j (by omega)

end Reaches

theorem Runs.machine_reach {q : Fin S} {w : List (Fin S)} {q0 : Sym}
    {δ : List (Option Sym) → List (Op S)} (B : ℕ) (hB : ∀ os, (δ os).length ≤ B)
    (σ σf : St S) (m : ℕ) (hR : Reaches I q w δ (σ.push q q0) σf m)
    (hstop : σf.top q = some hlt) :
    Runs I prog (NLogN.machine q w q0 δ : Stmt S P) σ (σf.pop q)
      (m * (B + 17 * w.length + 19) + 3) := by
  have := Runs.machine (I := I) (prog := prog) B hB σ m hR.2 (by rw [hR.1]; exact hstop)
  rwa [hR.1] at this

end NLogN

end

section
-- Source module: NLogN.Move
/-!
# Basic transducers: moving stack contents
-/

namespace NLogN

variable {S P : ℕ} {I : List Sym} {prog : Fin P → Stmt S P}

@[simp] theorem St.set_stk (σ : St S) (i j : Fin S) (l : List Sym) :
    (σ.set i l).stk j = if j = i then l else σ.stk j := by
  simp [St.set, Function.update_apply]

/-! ### Normalising chains of `set` -/

@[simp] theorem St.push_set_same (σ : St S) (i : Fin S) (l : List Sym) (a : Sym) :
    (σ.set i l).push i a = σ.set i (a :: l) := by
  simp [St.push, St.set]

theorem St.push_set_ne (σ : St S) {i j : Fin S} (l : List Sym) (a : Sym) (h : j ≠ i) :
    (σ.set i l).push j a = (σ.push j a).set i l := by
  simp only [St.push, St.set, St.mk.injEq, and_true]
  funext k; simp only [Function.update_apply]; split_ifs <;> simp_all

@[simp] theorem St.pop_set_same (σ : St S) (i : Fin S) (l : List Sym) :
    (σ.set i l).pop i = σ.set i l.tail := by
  simp [St.pop, St.set]

theorem St.pop_set_ne (σ : St S) {i j : Fin S} (l : List Sym) (h : j ≠ i) :
    (σ.set i l).pop j = (σ.pop j).set i l := by
  simp only [St.pop, St.set, St.mk.injEq, and_true]
  funext k; simp only [Function.update_apply]; split_ifs <;> simp_all

theorem St.top_set (σ : St S) (i j : Fin S) (l : List Sym) :
    (σ.set i l).top j = if j = i then l.head? else σ.top j := by
  simp [St.top, St.set, Function.update_apply]; split_ifs <;> rfl

@[simp] theorem St.top_set_same (σ : St S) (i : Fin S) (l : List Sym) :
    (σ.set i l).top i = l.head? := by simp [St.top_set]

/-- Simp set for stepping transducers; add the needed `≠` facts. -/
theorem St.push_eq_set (σ : St S) (i : Fin S) (a : Sym) : σ.push i a = σ.set i (a :: σ.stk i) :=
  rfl

theorem St.set_of_eq (σ : St S) (i : Fin S) (l : List Sym) (h : σ.stk i = l) : σ.set i l = σ := by
  subst h; simp [St.set]

@[simp] theorem St.set_self (σ : St S) (i : Fin S) : σ.set i (σ.stk i) = σ := St.set_of_eq _ _ _ rfl

/-! ## Moving symbols from one stack to another -/

end NLogN

end

section
-- Source module: NLogN.Add
/-!
# Binary words on stacks; addition

A word `A : List Bool` (least significant bit first) sits on a stack as `A.map codeBit`, so its
least significant bit is on top.  A word ends where the stack stops showing bits.
-/

namespace NLogN

variable {S P : ℕ} {I : List Sym} {prog : Fin P → Stmt S P}

@[simp] theorem bitOf_codeBit (b : Bool) : bitOf (some (codeBit b)) = some b := by
  cases b <;> rfl

theorem codeBit_ne_hlt (b : Bool) : codeBit b ≠ hlt := by cases b <;> decide

/-- Ripple-carry addition with carry-in `c`. -/
def addL : Bool → List Bool → List Bool → List Bool
  | c, [], [] => if c then [true] else []
  | c, x :: A, [] => (x ^^ c) :: addL (x && c) A []
  | c, [], y :: B => (y ^^ c) :: addL (y && c) [] B
  | c, x :: A, y :: B => (x ^^ y ^^ c) :: addL ((x && y) || (c && (x ^^ y))) A B

/-- Transition of `add`: the state is the carry (`codeBit`). -/
def addδ (q a b d e : Fin S) : List (Option Sym) → List (Op S)
  | [some c, ta, tb] =>
    if bitOf ta = none ∧ bitOf tb = none then
      (if c = 1 then [.push d 1] else []) ++ [.pop q, .push q hlt]
    else
      let x := (bitOf ta).getD false
      let y := (bitOf tb).getD false
      let cb := decide (c = 1)
      (if (bitOf ta).isSome then [.pop a] else []) ++
        (if (bitOf tb).isSome then [.pop b, .push e (codeBit y)] else []) ++
        [.push d (codeBit (x ^^ y ^^ cb)), .pop q,
          .push q (codeBit ((x && y) || (cb && (x ^^ y))))]
  | _ => [.pop q, .push q hlt]

theorem addδ_length (q a b d e : Fin S) (os) : (addδ q a b d e os).length ≤ 6 := by
  unfold addδ; split
  · split_ifs <;> simp
  · simp

/-- `add`: pops the words on `a` and `b`, pushes their sum on `d` (most significant bit on top)
and the word of `b` on `e` (reversed). -/
def add (q a b d e : Fin S) : Stmt S P := machine q [a, b] 0 (addδ q a b d e)

def addCost (m : ℕ) : ℕ := (m + 1) * 59 + 3

section
variable {q a b d e : Fin S} (hqa : q ≠ a) (hqb : q ≠ b) (hqd : q ≠ d) (hqe : q ≠ e)
  (hab : a ≠ b) (had : a ≠ d) (hae : a ≠ e) (hbd : b ≠ d) (hbe : b ≠ e) (hde : d ≠ e)
  (ra rb Q : List Sym) (hra : bitOf ra.head? = none) (hrb : bitOf rb.head? = none)

/-- Configuration of `add` with carry `c`, remaining words `A`, `B`. -/
def addCfg (σ : St S) (c : Sym) (A B : List Bool) (D E : List Sym) : St S :=
  ((((σ.set a (A.map codeBit ++ ra)).set b (B.map codeBit ++ rb)).set d D).set e E).set q (c :: Q)

include hqa hqb hqd hqe hab had hae hbd hbe hde hra hrb in
theorem add_reaches (σ : St S) : ∀ (A B : List Bool) (c : Bool) (D E : List Sym),
    Reaches I q [a, b] (addδ q a b d e)
      (addCfg (q := q) (a := a) (b := b) (d := d) (e := e) ra rb Q σ (codeBit c) A B D E)
      (addCfg (q := q) (a := a) (b := b) (d := d) (e := e) ra rb Q σ hlt [] []
        (((addL c A B).map codeBit).reverse ++ D) ((B.map codeBit).reverse ++ E))
      (max A.length B.length + 1) := by
  have hqa' := Ne.symm hqa; have hqb' := Ne.symm hqb; have hqd' := Ne.symm hqd
  have hqe' := Ne.symm hqe; have hab' := Ne.symm hab; have had' := Ne.symm had
  have hae' := Ne.symm hae; have hbd' := Ne.symm hbd; have hbe' := Ne.symm hbe
  have hde' := Ne.symm hde
  have htop : ∀ (c : Bool) A B D E, (addCfg (q := q) (a := a) (b := b) (d := d) (e := e) ra rb Q
      σ (codeBit c) A B D E).top q ≠ some hlt := by
    intro c A B D E
    simp only [addCfg, St.top_set_same, List.head?_cons, ne_eq, Option.some.injEq]
    exact codeBit_ne_hlt c
  -- the tops seen by one step
  have htops : ∀ (c : Sym) A B D E, (addCfg (q := q) (a := a) (b := b) (d := d) (e := e) ra rb Q
      σ c A B D E).tops [q, a, b] = [some c, (A.map codeBit ++ ra).head?,
        (B.map codeBit ++ rb).head?] := by
    intro c A B D E
    simp only [St.tops, addCfg, List.map_cons, List.map_nil, St.top_set, hqa, hqb, hqd, hqe, hab,
      had, hae, hbd, hbe, hde, hqa', hqb', hqd', hqe', hab', had', hae', hbd', hbe', hde',
      if_true, if_false, List.head?_cons]
  intro A
  induction A with
  | nil =>
    intro B
    induction B with
    | nil =>
      intro c D E
      refine Reaches.step' (htop c [] [] D E) ?_ (Reaches.refl _)
      rw [mstep, htops]
      simp only [List.map_nil, List.nil_append]
      rw [addδ, if_pos ⟨hra, hrb⟩]
      cases c <;> simp [codeBit, addL, runOps, Op.run, addCfg, St.push_set_ne, St.pop_set_ne,
        hqa, hqb, hqd, hqe, hab, had, hae, hbd, hbe, hde, hqa', hqb', hqd', hqe', hab', had',
        hae', hbd', hbe', hde'] <;> rfl
    | cons y B ih =>
      intro c D E
      refine Reaches.step' (σ₁ := addCfg (q := q) (a := a) (b := b) (d := d) (e := e) ra rb Q σ
        (codeBit (y && c)) [] B (codeBit (y ^^ c) :: D) (codeBit y :: E))
        (htop c [] (y :: B) D E) ?_ ?_
      · rw [mstep, htops]
        simp only [List.map_nil, List.nil_append, List.map_cons, List.cons_append,
          List.head?_cons]
        rw [addδ, if_neg (by simp)]
        cases c <;> cases y <;> simp [codeBit, runOps, Op.run, addCfg, St.push_set_ne,
          St.pop_set_ne, hra, hqa, hqb, hqd, hqe, hab, had, hae, hbd, hbe, hde, hqa', hqb', hqd',
          hqe', hab', had', hae', hbd', hbe', hde']
      · have := ih (y && c) (codeBit (y ^^ c) :: D) (codeBit y :: E)
        simp only [List.length_nil, List.length_cons, addL, List.map_cons, List.reverse_cons,
          List.append_assoc, List.singleton_append] at this ⊢
        simpa using this
  | cons x A ih =>
    intro B
    cases B with
    | nil =>
      intro c D E
      refine Reaches.step' (σ₁ := addCfg (q := q) (a := a) (b := b) (d := d) (e := e) ra rb Q σ
        (codeBit (x && c)) A [] (codeBit (x ^^ c) :: D) E) (htop c (x :: A) [] D E) ?_ ?_
      · rw [mstep, htops]
        simp only [List.map_nil, List.nil_append, List.map_cons, List.cons_append,
          List.head?_cons]
        rw [addδ, if_neg (by simp)]
        cases c <;> cases x <;> simp [codeBit, runOps, Op.run, addCfg, St.push_set_ne,
          St.pop_set_ne, hrb, hqa, hqb, hqd, hqe, hab, had, hae, hbd, hbe, hde, hqa', hqb', hqd',
          hqe', hab', had', hae', hbd', hbe', hde']
      · have := ih [] (x && c) (codeBit (x ^^ c) :: D) E
        simp only [List.length_nil, List.length_cons, addL, List.map_cons, List.reverse_cons,
          List.append_assoc, List.singleton_append, List.map_nil, List.reverse_nil,
          List.nil_append] at this ⊢
        simpa using this
    | cons y B =>
      intro c D E
      refine Reaches.step' (σ₁ := addCfg (q := q) (a := a) (b := b) (d := d) (e := e) ra rb Q σ
          (codeBit ((x && y) || (c && (x ^^ y)))) A B (codeBit (x ^^ y ^^ c) :: D)
          (codeBit y :: E)) (htop c (x :: A) (y :: B) D E) ?_ ?_
      · rw [mstep, htops]
        simp only [List.map_cons, List.cons_append, List.head?_cons]
        rw [addδ, if_neg (by simp)]
        cases c <;> cases x <;> cases y <;> simp [codeBit, runOps, Op.run, addCfg,
          St.push_set_ne, St.pop_set_ne, hqa, hqb, hqd, hqe, hab, had, hae, hbd, hbe, hde, hqa',
          hqb', hqd', hqe', hab', had', hae', hbd', hbe', hde']
      · have := ih B ((x && y) || (c && (x ^^ y))) (codeBit (x ^^ y ^^ c) :: D) (codeBit y :: E)
        simp only [List.length_cons, addL, List.map_cons, List.reverse_cons,
          List.append_assoc, List.singleton_append] at this ⊢
        simpa [Nat.succ_max_succ] using this

include hqa hqb hqd hqe hab had hae hbd hbe hde hra hrb in
theorem Runs.add (σ : St S) (A B : List Bool) (hA : σ.stk a = A.map codeBit ++ ra)
    (hB : σ.stk b = B.map codeBit ++ rb) :
    Runs I prog (NLogN.add q a b d e : Stmt S P) σ
      ((((σ.set a ra).set b rb).set d (((addL false A B).map codeBit).reverse ++ σ.stk d)).set e
        ((B.map codeBit).reverse ++ σ.stk e)) (addCost (max A.length B.length)) := by
  have h := add_reaches (I := I) hqa hqb hqd hqe hab had hae hbd hbe hde ra rb (σ.stk q) hra hrb σ
    A B false (σ.stk d) (σ.stk e)
  have e0 : σ.push q 0 = addCfg (q := q) (a := a) (b := b) (d := d) (e := e) ra rb (σ.stk q) σ
      (codeBit false) A B (σ.stk d) (σ.stk e) := by
    simp only [addCfg, ← hA, ← hB, St.set_self, St.push_eq_set]; rfl
  rw [← e0] at h
  have := Runs.machine_reach (prog := prog) 6 (addδ_length q a b d e) σ _ _ h
    (by simp [addCfg, St.top_set_same])
  have e1 : (addCfg (q := q) (a := a) (b := b) (d := d) (e := e) ra rb (σ.stk q) σ hlt [] []
      (((addL false A B).map codeBit).reverse ++ σ.stk d) ((B.map codeBit).reverse ++ σ.stk e)).pop q
      = ((((σ.set a ra).set b rb).set d (((addL false A B).map codeBit).reverse ++ σ.stk d)).set e
        ((B.map codeBit).reverse ++ σ.stk e)) := by
    simp only [addCfg, St.pop_set_same, List.tail_cons, List.map_nil, List.nil_append]
    apply St.set_of_eq
    simp [hqa, hqb, hqd, hqe]
  rw [e1] at this
  exact this.mono (by simp [addCost])

end

end NLogN

end

section
-- Source module: NLogN.Item
/-!
# Integer items on stacks

An item is an integer (sign–magnitude, minimal binary, least significant bit nearest the header)
or a mark.  On a stack an item is its header symbol followed by its magnitude bits; the next
item's header ends the bits.
-/

namespace NLogN

variable {S P : ℕ} {I : List Sym} {prog : Fin P → Stmt S P}

/-! ## Minimal binary -/

theorem nbits_zero : nbits 0 = [] := by rw [nbits]; simp

theorem nbits_pos {m : ℕ} (h : m ≠ 0) : nbits m = decide (m % 2 = 1) :: nbits (m / 2) := by
  rw [nbits]; simp [h]

theorem wval_nbits (m : ℕ) : wval (nbits m) = m := by
  induction m using Nat.strong_induction_on with
  | _ m ih =>
    rcases Nat.eq_zero_or_pos m with rfl | hm
    · simp [nbits_zero, wval]
    · rw [nbits_pos hm.ne', wval, ih _ (Nat.div_lt_self hm (by norm_num))]
      by_cases h : m % 2 = 1 <;> simp [h] <;> omega

/-! ## Items -/

end NLogN

namespace NLogN

/-! ## Bit-level functions for `zip` -/

theorem wval_lt_pow (A : List Bool) : wval A < 2 ^ A.length := by
  induction A with
  | nil => simp [wval]
  | cons b A ih => simp only [wval, List.length_cons, pow_succ]; cases b <;> simp <;> omega

end NLogN

end

section
-- Source module: NLogN.Arith
/-!
# Signed addition of integer items
-/

namespace NLogN

variable {S P : ℕ} {I : List Sym} {prog : Fin P → Stmt S P}

end NLogN

namespace NLogN

variable {S P : ℕ} {I : List Sym} {prog : Fin P → Stmt S P}

theorem wval_zbits (z : ℤ) : wval (zbits z) = z.natAbs := wval_nbits _

end NLogN

end

section
-- Source module: NLogN.Basic
/-!
# A relaxed machine layer over `IntMul.MultitapeTM`

`Prog Γ k` is a deterministic `k`-tape machine over an arbitrary alphabet whose transition
function returns `none` to halt.  Its step semantics silently enforce the platform rules
(`▷` is kept and never written elsewhere, no left move from `▷`, tape `0` is read-only), so
`compile` turns any program into a `MultitapeTM` with one extra step.
-/

namespace IntMul.Mach

open IntMul

variable {Γ : Type} {k : ℕ}

namespace Tapes

end Tapes

attribute [instance] Prog.fintypeQ

section Sem

variable [DecidableEq Γ] (st : Γ)

variable {st}

/-- Transport along a state map that commutes with the transition function. -/
theorem Halts.map {P R : Prog Γ k} (f : P.Q → R.Q)
    (hf : ∀ q a, R.δ (f q) a = (P.δ q a).map (fun r => (f r.1, r.2)))
    {q : P.Q} {T T' : Tapes Γ k} {t : ℕ} (h : Halts st P q T t T') :
    Halts st R (f q) T t T' := by
  induction h with
  | done h0 => exact Halts.done (by rw [hf, h0]; rfl)
  | step h0 _ ih => exact Halts.step (by rw [hf, h0]; rfl) ih

end Sem

/-! ## Combinators -/

/-- Run `P₁`, then `P₂` (no extra step at the junction). -/
def seq (P₁ P₂ : Prog Γ k) : Prog Γ k where
  Q := P₁.Q ⊕ P₂.Q
  q0 := Sum.inl P₁.q0
  δ q a := match q with
    | Sum.inl q => match P₁.δ q a with
      | some r => some (Sum.inl r.1, r.2)
      | none => (P₂.δ P₂.q0 a).map (fun r => (Sum.inr r.1, r.2))
    | Sum.inr q => (P₂.δ q a).map (fun r => (Sum.inr r.1, r.2))

/-- Branch on the scanned symbols, then run `P₁` or `P₂`. -/
def ite (c : (Fin k → Γ) → Bool) (P₁ P₂ : Prog Γ k) : Prog Γ k where
  Q := Option (P₁.Q ⊕ P₂.Q)
  q0 := none
  δ q a := match q with
    | none => if c a then (P₁.δ P₁.q0 a).map (fun r => (some (Sum.inl r.1), r.2))
        else (P₂.δ P₂.q0 a).map (fun r => (some (Sum.inr r.1), r.2))
    | some (Sum.inl q) => (P₁.δ q a).map (fun r => (some (Sum.inl r.1), r.2))
    | some (Sum.inr q) => (P₂.δ q a).map (fun r => (some (Sum.inr r.1), r.2))

/-- `while c do B`: the test is made on the scanned symbols before every pass. -/
def loop (c : (Fin k → Γ) → Bool) (B : Prog Γ k) : Prog Γ k where
  Q := Option B.Q
  q0 := none
  δ q a := match q with
    | none => if c a then (B.δ B.q0 a).map (fun r => (some r.1, r.2)) else none
    | some q => match B.δ q a with
      | some r => some (some r.1, r.2)
      | none => if c a then (B.δ B.q0 a).map (fun r => (some r.1, r.2)) else none

/-- A program with a single step. -/
def act (f : (Fin k → Γ) → Fin k → Γ × Move) : Prog Γ k where
  Q := Bool
  q0 := false
  δ q a := if q then none else some (true, f a)

/-- The empty program. -/
def skip : Prog Γ k where
  Q := Unit
  q0 := ()
  δ _ _ := none

/-! ## Compilation to the platform model -/

variable [DecidableEq Γ] [Fintype Γ]

end IntMul.Mach

end

section
-- Source module: NLogN.IntOps2
/-!
# More integer item operations: negate, duplicate, shifts
-/

namespace NLogN

variable {S P : ℕ} {I : List Sym} {prog : Fin P → Stmt S P}

theorem zbits_neg (z : ℤ) : zbits (-z) = zbits z := by simp [zbits]

/-! ## Negation -/

end NLogN

namespace NLogN

variable {S P : ℕ} {I : List Sym} {prog : Fin P → Stmt S P}

/-! ## Duplication -/

end NLogN

end

section
-- Source module: NLogN.Shift
/-!
# Shifting and splitting integers by a power of two given as an item

A "ruler" is the item `int (2 ^ m)`; its bits are `m` zeros and a one.
-/

namespace NLogN

variable {S P : ℕ} {I : List Sym} {prog : Fin P → Stmt S P}

/-! ## Bit lemmas -/

theorem nbits_two_pow (m : ℕ) : nbits (2 ^ m) = List.replicate m false ++ [true] := by
  induction m with
  | zero => rw [nbits_pos (by norm_num)]; simp [nbits_zero]
  | succ m ih =>
    rw [nbits_pos (by positivity), pow_succ, List.replicate_succ]
    simp [ih, Nat.mul_mod_left]

theorem zbits_two_pow (m : ℕ) : zbits (2 ^ m : ℕ) = List.replicate m false ++ [true] := by
  simp [zbits, nbits_two_pow]

theorem nbits_mul_two_pow {x : ℕ} (hx : x ≠ 0) (m : ℕ) :
    nbits (x * 2 ^ m) = List.replicate m false ++ nbits x := by
  induction m with
  | zero => simp
  | succ m ih =>
    rw [nbits_pos (by positivity), List.replicate_succ, pow_succ, ← mul_assoc]
    simp [Nat.mul_mod_left, ih]

theorem nbits_drop (x m : ℕ) : (nbits x).drop m = nbits (x / 2 ^ m) := by
  induction m generalizing x with
  | zero => simp
  | succ m ih =>
    rcases Nat.eq_zero_or_pos x with rfl | hx
    · simp [nbits_zero]
    · rw [nbits_pos hx.ne', List.drop_succ_cons, ih, pow_succ, Nat.div_div_eq_div_mul,
        mul_comm 2]

theorem natAbs_mul_two_pow (z : ℤ) (m : ℕ) : (z * 2 ^ m).natAbs = z.natAbs * 2 ^ m := by
  rw [Int.natAbs_mul]; simp

theorem zbits_mul_two_pow {z : ℤ} (hz : z ≠ 0) (m : ℕ) :
    zbits (z * 2 ^ m) = List.replicate m false ++ zbits z := by
  rw [zbits, natAbs_mul_two_pow, nbits_mul_two_pow (by omega)]; rfl

/-! ## Moving the zeros of a ruler -/

end NLogN

namespace NLogN

variable {S P : ℕ} {I : List Sym} {prog : Fin P → Stmt S P}

/-! ## Shift left by a ruler -/

/-! ## Split by a ruler -/

end NLogN

end

section
-- Source module: NLogN.Flat
/-!
# Flat code with jumps, and compilation of structured programs into it

Instructions carry absolute addresses. `ret` with an empty control stack halts.
`exec_flat`: a structured run of cost `c` is `c` flat steps.
-/

namespace NLogN

variable {S P : ℕ}

theorem Steps.trans {I : List Sym} {code : ℕ → Instr S} {c₁ c₂ c₃ : Cfg S} {m n : ℕ}
    (h₁ : Steps I code c₁ m c₂) (h₂ : Steps I code c₂ n c₃) : Steps I code c₁ (m + n) c₃ := by
  induction h₁ with
  | refl => simpa using h₂
  | step h _ ih => rw [Nat.add_right_comm]; exact Steps.step h (ih h₂)

/-! ## Layout -/

/-! ## A concrete layout -/

end NLogN

end

section
-- Source module: NLogN.Walk
/-!
# Scans, copies and finite-state walks

Generic single-loop programs and their exact running times.
-/

namespace IntMul.Mach

open IntMul

set_option linter.unusedSectionVars false

variable {Γ : Type} {k : ℕ} [DecidableEq Γ]

/-! ## Tape lemmas -/

/-! ## Writing with `fix` -/

/-! ## Scans -/

/-! ## Copy -/

/-! ## Finite-state walks to the left -/

/-! ## Single moves -/

/-- Move head `i` one cell. -/
def mv (i : Fin k) (m : Move) : Prog Γ k := act (fun a => wr1 a i (a i) m)

end IntMul.Mach

end

section
-- Source module: NLogN.TM
/-!
# Running flat code on the platform's Turing machines

Tapes: `0` input, `1` output, `2` control stack (return addresses), `3 + i` stack `i`.
On every stack tape the head rests on the top symbol (on `▷` when empty), so `push` is two
steps, `pop` and tests are one step, and a call is two steps.  Each flat step is at most two
machine steps (`flat_tm`).
-/

namespace NLogN

open IntMul IntMul.Mach

variable {S L : ℕ}

/-! ## Encoding of configurations -/

end NLogN

namespace NLogN

open IntMul IntMul.Mach

variable {S L : ℕ}

/-! ## Partial runs -/

theorem Reach.trans {Γ' : Type} [DecidableEq Γ'] {k : ℕ} {st : Γ'} {P : Prog Γ' k}
    {q₁ q₂ q₃ : P.Q} {T₁ T₂ T₃ : Tapes Γ' k} {m n : ℕ}
    (h₁ : Reach st P q₁ T₁ m q₂ T₂) (h₂ : Reach st P q₂ T₂ n q₃ T₃) : Reach st P q₁ T₁ (m + n) q₃ T₃ := by
  induction h₁ with
  | refl => simpa using h₂
  | step h _ ih => rw [Nat.add_right_comm]; exact Reach.step h (ih h₂)

attribute [simp] tst_ne_tin tst_ne_tout tst_ne_tctl tin_ne_tout tin_ne_tctl tout_ne_tctl

/-! ## One flat step -/

end NLogN

end

section
-- Source module: NLogN.Prims
/-!
# Constants, input and output of integer items
-/

namespace NLogN

open IntMul

variable {S P : ℕ} {I : List Sym} {prog : Fin P → Stmt S P}

/-! ## Constants -/

/-! ## Output -/

theorem length_nbits_le {n m : ℕ} (h : n < 2 ^ m) : (nbits n).length ≤ m := by
  have := nbits_drop n m
  rw [Nat.div_eq_of_lt h, nbits_zero, List.drop_eq_nil_iff] at this
  exact this

/-! ## Input -/

end NLogN

end

section
-- Source module: NLogN.ILang
/-!
# The item language

Programs over `S` stacks of items (integers and marks), compiled to stack programs over `S + 4`
stacks (the last four are scratch).  `compile_correct` turns item-level executions into
`Runs` of the compiled program, with the same cost.
-/

namespace NLogN

open IntMul

variable {S P : ℕ}

/-! ## Stacks of the compiled program -/

/-! ## Operations -/

variable {I : List Sym} {prog : Fin P → Stmt (S + 4) P}

theorem addIntCost_mono {L L' : ℕ} (h : L ≤ L') : addIntCost L ≤ addIntCost L' := by
  simp only [addIntCost, addMagCost, subMagCost, zipCost, moveCost]; nlinarith

end NLogN

end

section
-- Source module: NLogN.IRuns
/-!
# Reasoning about item-language programs
-/

namespace NLogN

open IntMul

variable {S P : ℕ} {I : List Sym} {iprog : Fin P → IStmt S P}

namespace IRuns

theorem mono_r6c {p : IStmt S P} {s s' : IState S} {c c' : ℕ} (h : IRuns I iprog p s s' c)
    (hc : c ≤ c') : IRuns I iprog p s s' c' := by
  obtain ⟨d, hd, h⟩ := h; exact ⟨d, by omega, h⟩

theorem mono' {p : IStmt S P} {s s' s'' : IState S} {c c' : ℕ} (h : IRuns I iprog p s s' c)
    (he : s' = s'') (hc : c ≤ c') : IRuns I iprog p s s'' c' := he ▸ h.mono_r6c hc

theorem skip_r6c (s : IState S) : IRuns I iprog .skip s s 1 := ⟨1, le_rfl, .skip s⟩

theorem op {o : IOp S} {s s' : IState S} {c : ℕ} (h : o.Step I s s' c) :
    IRuns I iprog (.op o) s s' c := ⟨c, le_rfl, .op h⟩

theorem seq_r6c {p q : IStmt S P} {s s₁ s₂ : IState S} {c₁ c₂ : ℕ} (h₁ : IRuns I iprog p s s₁ c₁)
    (h₂ : IRuns I iprog q s₁ s₂ c₂) : IRuns I iprog (.seq p q) s s₂ (c₁ + c₂) := by
  obtain ⟨d₁, hd₁, h₁⟩ := h₁; obtain ⟨d₂, hd₂, h₂⟩ := h₂
  exact ⟨d₁ + d₂, by omega, .seq h₁ h₂⟩

theorem iteT {i f} {p q : IStmt S P} {s s' : IState S} {c : ℕ} (hf : f (s.cl i) = true)
    (h : IRuns I iprog p s s' c) : IRuns I iprog (.ite i f p q) s s' (c + 25) := by
  obtain ⟨d, hd, h⟩ := h; exact ⟨d + 25, by omega, .iteT hf h⟩

theorem iteF {i f} {p q : IStmt S P} {s s' : IState S} {c : ℕ} (hf : f (s.cl i) = false)
    (h : IRuns I iprog q s s' c) : IRuns I iprog (.ite i f p q) s s' (c + 25) := by
  obtain ⟨d, hd, h⟩ := h; exact ⟨d + 25, by omega, .iteF hf h⟩

theorem ite {i f} {p q : IStmt S P} {s s' : IState S} {c : ℕ}
    (h : IRuns I iprog (if f (s.cl i) then p else q) s s' c) :
    IRuns I iprog (.ite i f p q) s s' (c + 25) := by
  by_cases hf : f (s.cl i)
  · rw [if_pos hf] at h; exact iteT hf h
  · rw [if_neg hf] at h; exact iteF (by simpa using hf) h

theorem call {j : Fin P} {s s' : IState S} {c : ℕ} (h : IRuns I iprog (iprog j) s s' c) :
    IRuns I iprog (.call j) s s' (c + 2) := by
  obtain ⟨d, hd, h⟩ := h; exact ⟨d + 2, by omega, .call h⟩

theorem loopF {i f} {p : IStmt S P} {s : IState S} (hf : f (s.cl i) = false) :
    IRuns I iprog (.loop i f p) s s 30 := ⟨30, le_rfl, .loopF hf⟩

theorem loopT {i f} {p : IStmt S P} {s s₁ s₂ : IState S} {c₁ c₂ : ℕ} (hf : f (s.cl i) = true)
    (h₁ : IRuns I iprog p s s₁ c₁) (h₂ : IRuns I iprog (.loop i f p) s₁ s₂ c₂) :
    IRuns I iprog (.loop i f p) s s₂ (c₁ + c₂ + 30) := by
  obtain ⟨d₁, hd₁, h₁⟩ := h₁; obtain ⟨d₂, hd₂, h₂⟩ := h₂
  exact ⟨d₁ + d₂ + 30, by omega, .loopT hf h₁ h₂⟩

/-- A loop running through the states `ss 0, …, ss m`. -/
theorem loop {i f} {p : IStmt S P} (ss : ℕ → IState S) (cs : ℕ → ℕ) (m : ℕ)
    (hT : ∀ k < m, f ((ss k).cl i) = true) (hF : f ((ss m).cl i) = false)
    (hb : ∀ k < m, IRuns I iprog p (ss k) (ss (k + 1)) (cs k)) :
    IRuns I iprog (.loop i f p) (ss 0) (ss m) ((∑ k ∈ Finset.range m, (cs k + 30)) + 30) := by
  suffices H : ∀ r j, j + r = m → IRuns I iprog (.loop i f p) (ss j) (ss m)
      ((∑ k ∈ Finset.Ico j m, (cs k + 30)) + 30) by
    have := H m 0 (by omega)
    rwa [Finset.range_eq_Ico]
  intro r
  induction r with
  | zero => intro j hj; subst hj; simpa using loopF hF
  | succ r ih =>
    intro j hj
    have hjm : j < m := by omega
    have := loopT (hT j hjm) (hb j hjm) (ih (j + 1) (by omega))
    refine this.mono_r6c ?_
    rw [Finset.sum_eq_sum_Ico_succ_bot hjm]
    omega

/-- Loop with a uniform bound on the cost of each iteration. -/
theorem loop' {i f} {p : IStmt S P} (ss : ℕ → IState S) (c m : ℕ)
    (hT : ∀ k < m, f ((ss k).cl i) = true) (hF : f ((ss m).cl i) = false)
    (hb : ∀ k < m, IRuns I iprog p (ss k) (ss (k + 1)) c) :
    IRuns I iprog (.loop i f p) (ss 0) (ss m) (m * (c + 30) + 30) := by
  have := loop ss (fun _ => c) m hT hF hb
  simpa [Finset.sum_const, Finset.card_range, smul_eq_mul] using this

end IRuns

/-! ## Operations as `IRuns` -/

namespace IRuns

theorem add {s : IState S} {i j k : Fin S} {a b : ℤ} {Li Lj : List Item} (hij : i ≠ j)
    (hi : s.G i = .int a :: Li) (hj : s.G j = .int b :: Lj) :
    IRuns I iprog (.op (.add i j k)) s
      (((s.upd i Li).upd j Lj).upd k (.int (a + b) :: ((s.upd i Li).upd j Lj).G k))
      (addIntCost (zsz a + zsz b)) := op (.add hij hi hj)

theorem neg {s : IState S} {i : Fin S} {a : ℤ} {L : List Item} (hi : s.G i = .int a :: L) :
    IRuns I iprog (.op (.neg i)) s (s.upd i (.int (-a) :: L)) 20 := op (.neg hi)

theorem dup_r6c {s : IState S} {i j : Fin S} {a : ℤ} {L : List Item} (hij : i ≠ j)
    (hi : s.G i = .int a :: L) :
    IRuns I iprog (.op (.dup i j)) s (s.upd j (.int a :: s.G j)) (dupCost (zsz a) + 17) :=
  op (.dup hij hi)

theorem drop_r6c {s : IState S} {i : Fin S} {a : ℤ} {L : List Item} (hi : s.G i = .int a :: L) :
    IRuns I iprog (.op (.drop i)) s (s.upd i L) (2 * zsz a + 2) := op (.drop hi)

theorem mv_r6c {s : IState S} {i j : Fin S} {a : ℤ} {L : List Item} (hij : i ≠ j)
    (hi : s.G i = .int a :: L) :
    IRuns I iprog (.op (.mv i j)) s ((s.upd i L).upd j (.int a :: s.G j))
      (2 * moveCost (zsz a) + 19) := op (.mv hij hi)

theorem const_r6c {s : IState S} (i : Fin S) (c : ℤ) :
    IRuns I iprog (.op (.const i c)) s (s.upd i (.int c :: s.G i)) (zsz c + 2) := op (.const c)

theorem mark {s : IState S} (i : Fin S) :
    IRuns I iprog (.op (.mark i)) s (s.upd i (.mark :: s.G i)) 1 := op .mark

theorem unmark {s : IState S} {i : Fin S} {L : List Item} (hi : s.G i = .mark :: L) :
    IRuns I iprog (.op (.unmark i)) s (s.upd i L) 1 := op (.unmark hi)

theorem shl {s : IState S} {i j : Fin S} {a : ℤ} {m : ℕ} {Li Lj : List Item} (hij : i ≠ j)
    (hi : s.G i = .int a :: Li) (hj : s.G j = .int (2 ^ m) :: Lj) :
    IRuns I iprog (.op (.shl i j)) s (s.upd i (.int (a * 2 ^ m) :: Li)) (shlCost m) :=
  op (.shl hij hi hj)

theorem split {s : IState S} {i j k : Fin S} {a : ℤ} {m : ℕ} {Li Lj : List Item} (hij : i ≠ j)
    (hik : i ≠ k) (hjk : j ≠ k) (hi : s.G i = .int a :: Li) (hj : s.G j = .int (2 ^ m) :: Lj) :
    IRuns I iprog (.op (.split i j k)) s
      ((s.upd i (.int (sg a (a.natAbs / 2 ^ m)) :: Li)).upd k
        (.int (sg a (a.natAbs % 2 ^ m)) :: s.G k)) (splitCost m + 17) :=
  op (.split hij hik hjk hi hj)

theorem cat {s : IState S} {i j k : Fin S} {a : ℤ} {b m : ℕ} {Li Lj Lk : List Item} (hij : i ≠ j)
    (hik : i ≠ k) (hjk : j ≠ k) (ha : a ≠ 0) (hb : b < 2 ^ m) (hi : s.G i = .int a :: Li)
    (hj : s.G j = .int (2 ^ m) :: Lj) (hk : s.G k = .int (b : ℤ) :: Lk) :
    IRuns I iprog (.op (.cat i j k)) s
      ((s.upd i (.int (sg a (a.natAbs * 2 ^ m + b)) :: Li)).upd k Lk) (catCost m) :=
  op (.cat hij hik hjk ha hb hi hj hk)

end IRuns

/-! ## State lemmas -/

@[simp] theorem IState.upd_upd_same (s : IState S) (i : Fin S) (L L' : List Item) :
    (s.upd i L).upd i L' = s.upd i L' := by
  simp [IState.upd]

@[simp] theorem IState.upd_self (s : IState S) (i : Fin S) : s.upd i (s.G i) = s := by
  simp [IState.upd]

theorem IState.ext' {s t : IState S} (hG : ∀ x, s.G x = t.G x) (hip : s.ip = t.ip)
    (hout : s.out = t.out) : s = t := by
  cases s; cases t; simp only [IState.mk.injEq]; exact ⟨funext hG, hip, hout⟩

@[simp] theorem cl_int (s : IState S) (i : Fin S) (z : ℤ) (L : List Item) (h : s.G i = .int z :: L) :
    s.cl i = if z = 0 then .zero else if z < 0 then .neg else .pos := by
  simp [IState.cl, h, cls]

end NLogN

end

section
-- Source module: NLogN.Costs
/-! # Linear bounds on the costs of item operations -/

namespace NLogN

theorem addIntCost_le (L : ℕ) : addIntCost L ≤ 400 * (L + 1) := by
  simp only [addIntCost, addMagCost, subMagCost, zipCost, moveCost]; omega
theorem dupCost_le (L : ℕ) : dupCost L + 17 ≤ 300 * (L + 1) := by
  simp only [dupCost, zipCost, moveCost]; ring_nf; omega
theorem moveIntCost_le (L : ℕ) : 2 * moveCost L + 19 ≤ 110 * (L + 1) := by
  simp only [moveCost]; omega
theorem shlCost_le (m : ℕ) : shlCost m ≤ 200 * (m + 1) := by
  simp only [shlCost, zipCost, moveCost]; omega
theorem splitCost_le (m : ℕ) : splitCost m + 17 ≤ 200 * (m + 1) := by
  simp only [splitCost, takeCost, moveCost]; omega

/-! ## Sizes -/

theorem zsz_le_of_lt {z : ℤ} {m : ℕ} (h : z.natAbs < 2 ^ m) : zsz z ≤ m := length_nbits_le h

theorem natAbs_lt_zsz (z : ℤ) : z.natAbs < 2 ^ zsz z := by
  have := wval_lt_pow (zbits z); rwa [wval_zbits] at this

theorem zsz_le_iff {z : ℤ} {m : ℕ} : zsz z ≤ m ↔ z.natAbs < 2 ^ m :=
  ⟨fun h => lt_of_lt_of_le (natAbs_lt_zsz z) (Nat.pow_le_pow_right (by norm_num) h),
    zsz_le_of_lt⟩

theorem zsz_mul_le (a b : ℤ) : zsz (a * b) ≤ zsz a + zsz b := by
  apply zsz_le_of_lt
  rw [Int.natAbs_mul, pow_add]
  exact Nat.mul_lt_mul'' (natAbs_lt_zsz a) (natAbs_lt_zsz b)

theorem zsz_add_le (a b : ℤ) : zsz (a + b) ≤ max (zsz a) (zsz b) + 1 := by
  apply zsz_le_of_lt
  have ha := natAbs_lt_zsz a; have hb := natAbs_lt_zsz b
  have ha' : 2 ^ zsz a ≤ 2 ^ max (zsz a) (zsz b) := Nat.pow_le_pow_right (by norm_num) (le_max_left _ _)
  have hb' : 2 ^ zsz b ≤ 2 ^ max (zsz a) (zsz b) := Nat.pow_le_pow_right (by norm_num) (le_max_right _ _)
  have := Int.natAbs_add_le a b
  rw [pow_succ]; omega

theorem zsz_two_pow_r6c (m : ℕ) : zsz ((2 : ℤ) ^ m) = m + 1 := by
  have : ((2 : ℤ) ^ m) = ((2 ^ m : ℕ) : ℤ) := by push_cast; rfl
  rw [this, zsz, zbits_two_pow]; simp

theorem zsz_neg_r6c (z : ℤ) : zsz (-z) = zsz z := by simp [zsz, zbits_neg]

theorem zsz_zero_r6c : zsz 0 = 0 := by simp [zsz, zbits, nbits_zero]

theorem zsz_one_r6c : zsz 1 = 1 := by
  simp [zsz, zbits]; rw [nbits_pos (by norm_num)]; simp [nbits_zero]

theorem zsz_mono_r6c {a b : ℤ} (h : a.natAbs ≤ b.natAbs) : zsz a ≤ zsz b :=
  zsz_le_of_lt (lt_of_le_of_lt h (natAbs_lt_zsz b))

theorem natAbs_sg (z : ℤ) (n : ℕ) : (sg z n).natAbs = n := by
  unfold sg; split_ifs <;> simp

theorem sg_add (z : ℤ) (a b : ℕ) : sg z (a + b) = sg z a + sg z b := by
  unfold sg; split_ifs <;> push_cast <;> ring

theorem sg_mul (z : ℤ) (c a : ℕ) : sg z (c * a) = c * sg z a := by
  unfold sg; split_ifs <;> push_cast <;> ring

theorem sg_sg {z : ℤ} {n : ℕ} (hn : n ≠ 0) (m : ℕ) : sg (sg z n) m = sg z m := by
  unfold sg; split_ifs <;> first | rfl | omega

theorem sg_natAbs (z : ℤ) : sg z z.natAbs = z := by unfold sg; split_ifs <;> omega

theorem sg_zero (z : ℤ) : sg z 0 = 0 := by unfold sg; split_ifs <;> simp

theorem sg_eq_zero {z : ℤ} {n : ℕ} : sg z n = 0 ↔ n = 0 := by
  unfold sg; split_ifs <;> omega

end NLogN

end

section
-- Source module: NLogN.ISchool
/-!
# Schoolbook multiplication in the item language (base case)
-/

namespace NLogN

open IntMul

variable {S P : ℕ} {I : List Sym} {iprog : Fin P → IStmt S P}

theorem nat_mod_two_pow_succ (n k : ℕ) : n % 2 ^ (k + 1) = n % 2 ^ k + 2 ^ k * (n / 2 ^ k % 2) := by
  rw [pow_succ, Nat.mod_mul, mul_comm]

theorem div_two_pow_ne_zero {n k : ℕ} (hk : k < (nbits n).length) : n / 2 ^ k ≠ 0 := by
  intro h
  have := nbits_drop n k
  rw [h, nbits_zero, List.drop_eq_nil_iff] at this; omega

theorem div_two_pow_zsz (n : ℕ) : n / 2 ^ (nbits n).length = 0 := by
  have := wval_lt_pow (nbits n); rw [wval_nbits] at this
  exact Nat.div_eq_of_lt this

theorem smulBody_runs_r6c {A X Y W Q R T : Fin S} (hd : [A, X, Y, W, Q, R, T].Nodup)
    (s : IState S) (L : List Item) (a b c : ℤ) (hb : b ≠ 0) (N : ℕ)
    (ha : zsz a ≤ N) (hc : zsz c ≤ N) :
    IRuns I iprog (smulBody X Y W Q R T) (schoolSt s A X Y W Q L a b c)
      (schoolSt s A X Y W Q L (a * 2) (sg b (b.natAbs / 2))
        (c + a * sg b (b.natAbs % 2))) (schoolIter N) := by
  simp only [List.nodup_cons, List.mem_cons, List.not_mem_nil, not_or,
    not_false_eq_true, List.nodup_nil, and_true, or_false] at hd
  obtain ⟨⟨hAX, hAY, hAW, hAQ, hAR, hAT⟩, ⟨hXY, hXW, hXQ, hXR, hXT⟩, ⟨hYW, hYQ, hYR, hYT⟩,
    ⟨hWQ, hWR, hWT⟩, ⟨hQR, hQT⟩, hRT⟩ := hd
  have hAX' := Ne.symm hAX; have hAY' := Ne.symm hAY; have hAW' := Ne.symm hAW; have hAQ' := Ne.symm hAQ; have hAR' := Ne.symm hAR; have hAT' := Ne.symm hAT; have hXY' := Ne.symm hXY; have hXW' := Ne.symm hXW; have hXQ' := Ne.symm hXQ; have hXR' := Ne.symm hXR; have hXT' := Ne.symm hXT; have hYW' := Ne.symm hYW; have hYQ' := Ne.symm hYQ; have hYR' := Ne.symm hYR; have hYT' := Ne.symm hYT; have hWQ' := Ne.symm hWQ; have hWR' := Ne.symm hWR; have hWT' := Ne.symm hWT; have hQR' := Ne.symm hQR; have hQT' := Ne.symm hQT; have hRT' := Ne.symm hRT
  set s0 := schoolSt s A X Y W Q L a b c
  have hY : s0.G Y = .int b :: s.G Y := by simp [s0, schoolSt, hYQ, hYW]
  have hQ : s0.G Q = .int (2 ^ 1) :: s.G Q := by simp [s0, schoolSt]
  have h1 := IRuns.split (I := I) (iprog := iprog) (s := s0) (k := R) hYQ hYR hQR hY hQ
  set r := sg b (b.natAbs % 2 ^ 1)
  set s1 := (s0.upd Y (.int (sg b (b.natAbs / 2 ^ 1)) :: s.G Y)).upd R (.int r :: s0.G R)
  have hR1 : s1.G R = .int r :: s.G R := by
    simp [s1, s0, schoolSt, hYR', hWR', hQR', hXR', hAR']
  have hX1 : s1.G X = .int a :: s.G X := by simp [s1, s0, schoolSt, hXR, hXY, hXW, hXQ]
  have hW1 : s1.G W = .int c :: s.G W := by simp [s1, s0, schoolSt, hWR, hYW', hWQ]
  have hr : r = 0 ∨ r = 1 ∨ r = -1 := by
    simp only [r, sg]; split_ifs <;> omega
  -- the branch
  have hbr : IRuns I iprog (.ite R (fun c => c == .zero) .skip
      (.ite R (fun c => c == .pos) (.seq (.op (.dup X T)) (.op (.add T W W)))
        (.seq (.op (.dup X T)) (.seq (.op (.neg T)) (.op (.add T W W)))))) s1
      (s1.upd W (.int (c + a * r) :: s.G W)) (50 + 20 + 300 * (N + 1) + 400 * (2 * N + 2)) := by
    rcases hr with h0 | h1 | hm
    · refine (IRuns.iteT (by rw [cl_int _ _ _ _ hR1]; simp [h0]) (IRuns.skip_r6c _)).mono' ?_ (by omega)
      rw [h0, mul_zero, add_zero, ← hW1, IState.upd_self]
    · have hcl1 : s1.cl R = .pos := by rw [cl_int _ _ _ _ hR1]; simp [h1]
      have e1 := IRuns.dup_r6c (I := I) (iprog := iprog) (s := s1) (j := T) hXT hX1
      have e2 := IRuns.add (I := I) (iprog := iprog) (s := s1.upd T (.int a :: s1.G T))
        (i := T) (j := W) (k := W) (a := a) (b := c) (Li := s1.G T) (Lj := s.G W)
        hWT' (by simp) (by simp [hW1, hWT])
      refine (IRuns.iteF (by rw [hcl1]; rfl) (IRuns.iteT (by rw [hcl1]; rfl) (IRuns.seq_r6c e1 e2))).mono' ?_ ?_
      · apply IState.ext' <;> intros <;> simp [h1] <;> split_ifs <;> simp_all <;> ring
      · have := dupCost_le (zsz a)
        have := addIntCost_mono (show zsz a + zsz c ≤ 2 * N + 1 by omega)
        have := addIntCost_le (2 * N + 1)
        omega
    · have hcl1 : s1.cl R = .neg := by rw [cl_int _ _ _ _ hR1]; simp [hm]
      have e1 := IRuns.dup_r6c (I := I) (iprog := iprog) (s := s1) (j := T) hXT hX1
      have e2 := IRuns.neg (I := I) (iprog := iprog) (s := s1.upd T (.int a :: s1.G T)) (i := T)
        (a := a) (L := s1.G T) (by simp)
      have e3 := IRuns.add (I := I) (iprog := iprog)
        (s := (s1.upd T (.int a :: s1.G T)).upd T (.int (-a) :: s1.G T))
        (i := T) (j := W) (k := W) (a := -a) (b := c) (Li := s1.G T) (Lj := s.G W)
        hWT' (by simp) (by simp [hW1, hWT])
      refine (IRuns.iteF (by rw [hcl1]; rfl) (IRuns.iteF (by rw [hcl1]; rfl)
        (IRuns.seq_r6c e1 (IRuns.seq_r6c e2 e3)))).mono' ?_ ?_
      · apply IState.ext' <;> intros <;> simp [hm] <;> split_ifs <;> simp_all <;> ring
      · have := dupCost_le (zsz a)
        have := addIntCost_mono (show zsz (-a) + zsz c ≤ 2 * N + 1 by rw [zsz_neg_r6c]; omega)
        have := addIntCost_le (2 * N + 1)
        omega
  set s2 := s1.upd W (.int (c + a * r) :: s.G W)
  have hR2 : s2.G R = .int r :: s.G R := by simp [s2, hWR', hR1]
  have h3 := IRuns.drop_r6c (I := I) (iprog := iprog) (s := s2) hR2
  have hX3 : (s2.upd R (s.G R)).G X = .int a :: s.G X := by simp [s2, hXR, hXW, hX1]
  have hQ3 : (s2.upd R (s.G R)).G Q = .int (2 ^ 1) :: s.G Q := by
    simp [s2, s1, s0, schoolSt, hQR, hWQ', hYQ']
  have h4 := IRuns.shl (I := I) (iprog := iprog) hXQ hX3 hQ3
  refine (IRuns.seq_r6c h1 (IRuns.seq_r6c hbr (IRuns.seq_r6c h3 h4))).mono' ?_ ?_
  · apply IState.ext' <;> intros <;> simp [s2, s1, s0, schoolSt, r] <;> split_ifs <;> simp_all
  · have hr' : zsz r ≤ 1 := by
      rcases hr with h | h | h <;> rw [h] <;> simp [zsz_zero_r6c, zsz_one_r6c, zsz_neg_r6c]
    have := splitCost_le 1; have := shlCost_le 1
    simp only [schoolIter]; omega

end NLogN

namespace NLogN

variable {S P : ℕ} {I : List Sym} {iprog : Fin P → IStmt S P}

theorem zsz_le_add_of_natAbs_le {a : ℤ} {n : ℕ} (h : a.natAbs ≤ n) (z : ℤ) :
    zsz (z * a) ≤ zsz z + (nbits n).length := by
  refine le_trans (zsz_mul_le z a) ?_
  have : zsz a ≤ zsz (n : ℤ) := zsz_mono_r6c (by simpa using h)
  simp only [zsz, zbits, Int.natAbs_natCast] at this ⊢
  omega

theorem smul_runs {A X Y W Q R T : Fin S} (hd : [A, X, Y, W, Q, R, T].Nodup)
    (s : IState S) (x y : ℤ) (L : List Item) (hA : s.G A = .int x :: .int y :: L) :
    IRuns I iprog (smul A X Y W Q R T) s (s.upd A (.int (x * y) :: L))
      (smulCost (zsz x + zsz y)) := by
  have hd' := hd
  simp only [List.nodup_cons, List.mem_cons, List.not_mem_nil, not_or,
    not_false_eq_true, List.nodup_nil, and_true, or_false] at hd'
  obtain ⟨⟨hAX, hAY, hAW, hAQ, hAR, hAT⟩, ⟨hXY, hXW, hXQ, hXR, hXT⟩, ⟨hYW, hYQ, hYR, hYT⟩,
    ⟨hWQ, hWR, hWT⟩, ⟨hQR, hQT⟩, hRT⟩ := hd'
  have hAX' := Ne.symm hAX; have hAY' := Ne.symm hAY; have hAW' := Ne.symm hAW; have hAQ' := Ne.symm hAQ; have hAR' := Ne.symm hAR; have hAT' := Ne.symm hAT; have hXY' := Ne.symm hXY; have hXW' := Ne.symm hXW; have hXQ' := Ne.symm hXQ; have hXR' := Ne.symm hXR; have hXT' := Ne.symm hXT; have hYW' := Ne.symm hYW; have hYQ' := Ne.symm hYQ; have hYR' := Ne.symm hYR; have hYT' := Ne.symm hYT; have hWQ' := Ne.symm hWQ; have hWR' := Ne.symm hWR; have hWT' := Ne.symm hWT; have hQR' := Ne.symm hQR; have hQT' := Ne.symm hQT; have hRT' := Ne.symm hRT
  set N := zsz x + zsz y with hN
  set m := zsz y with hm
  -- prologue
  have h1 := IRuns.mv_r6c (I := I) (iprog := iprog) (s := s) (j := X) hAX hA
  set s1 := (s.upd A (.int y :: L)).upd X (.int x :: s.G X)
  have h2 := IRuns.mv_r6c (I := I) (iprog := iprog) (s := s1) (i := A) (j := Y) (a := y) (L := L) hAY
    (by simp [s1, hAX])
  set s2 := (s1.upd A L).upd Y (.int y :: s1.G Y)
  have h3 := IRuns.const_r6c (I := I) (iprog := iprog) (s := s2) W 0
  have h4 := IRuns.const_r6c (I := I) (iprog := iprog) (s := s2.upd W (.int 0 :: s2.G W)) Q 2
  let ss : ℕ → IState S := fun k => schoolSt s A X Y W Q L (x * 2 ^ k) (sg y (y.natAbs / 2 ^ k))
    (x * sg y (y.natAbs % 2 ^ k))
  have e0 : (s2.upd W (.int 0 :: s2.G W)).upd Q (.int 2 :: (s2.upd W (.int 0 :: s2.G W)).G Q) =
      ss 0 := by
    apply IState.ext' <;> intros <;> simp [ss, schoolSt, s2, s1, sg_natAbs, sg_zero, Nat.mod_one] <;>
      split_ifs <;> simp_all
  rw [e0] at h4
  have hloop := IRuns.loop' (I := I) (iprog := iprog) (i := Y) (f := fun c => c != .zero)
    (p := smulBody X Y W Q R T) ss (schoolIter N) m
    (by
      intro k hk
      have hne := div_two_pow_ne_zero (n := y.natAbs) hk
      have : (ss k).G Y = .int (sg y (y.natAbs / 2 ^ k)) :: s.G Y := by
        simp [ss, schoolSt, hYQ, hYW]
      rw [cl_int _ _ _ _ this]; simp only [sg_eq_zero, hne, if_false]; split_ifs <;> simp)
    (by
      have : (ss m).G Y = .int (sg y (y.natAbs / 2 ^ m)) :: s.G Y := by
        simp [ss, schoolSt, hYQ, hYW]
      rw [cl_int _ _ _ _ this]; simp [m, zsz, zbits, div_two_pow_zsz, sg_zero])
    (by
      intro k hk
      have hne := div_two_pow_ne_zero (n := y.natAbs) hk
      have hb : sg y (y.natAbs / 2 ^ k) ≠ 0 := by rwa [Ne, sg_eq_zero]
      have := smulBody_runs_r6c (I := I) (iprog := iprog) hd s L (x * 2 ^ k) (sg y (y.natAbs / 2 ^ k))
        (x * sg y (y.natAbs % 2 ^ k)) hb N
        (by
          by_cases hx : x = 0
          · simp [hx, zsz_zero_r6c]
          · rw [zsz, zbits_mul_two_pow hx]; simp only [List.length_append, List.length_replicate]
            have : zsz x = (zbits x).length := rfl
            omega)
        (le_trans (zsz_le_add_of_natAbs_le (by rw [natAbs_sg]; exact Nat.mod_le _ _) x) le_rfl)
      refine this.mono' ?_ le_rfl
      simp only [natAbs_sg, sg_sg hne]
      congr 1
      · ring
      · rw [Nat.div_div_eq_div_mul, ← pow_succ]
      · rw [nat_mod_two_pow_succ, sg_add, sg_mul, show y.natAbs / 2 ^ k % 2 =
          y.natAbs / 2 ^ k % 2 ^ 1 by norm_num]
        push_cast; ring)
  -- epilogue
  have hz : y.natAbs / 2 ^ m = 0 := by simp only [m, zsz, zbits]; exact div_two_pow_zsz _
  have hfull : y.natAbs % 2 ^ m = y.natAbs := Nat.mod_eq_of_lt (by
    have := Nat.div_add_mod y.natAbs (2 ^ m); rw [hz] at this; omega)
  set sm := ss m
  have hY5 : sm.G Y = .int 0 :: s.G Y := by simp [sm, ss, schoolSt, hYQ, hYW, hz, sg_zero]
  have h5 := IRuns.drop_r6c (I := I) (iprog := iprog) hY5
  have h6 := IRuns.drop_r6c (I := I) (iprog := iprog) (s := sm.upd Y (s.G Y)) (i := X)
    (a := x * 2 ^ m) (L := s.G X) (by simp [sm, ss, schoolSt, hXY, hXW, hXQ])
  have h7 := IRuns.drop_r6c (I := I) (iprog := iprog) (s := (sm.upd Y (s.G Y)).upd X (s.G X)) (i := Q)
    (a := 2) (L := s.G Q) (by simp [sm, ss, schoolSt, hYQ', hXQ'])
  have h8 := IRuns.mv_r6c (I := I) (iprog := iprog)
    (s := ((sm.upd Y (s.G Y)).upd X (s.G X)).upd Q (s.G Q)) (i := W) (j := A)
    (a := x * sg y (y.natAbs % 2 ^ m)) (L := s.G W) hAW'
    (by simp [sm, ss, schoolSt, hYW', hXW', hWQ])
  refine (IRuns.seq_r6c h1 (IRuns.seq_r6c h2 (IRuns.seq_r6c h3 (IRuns.seq_r6c h4 (IRuns.seq_r6c hloop
    (IRuns.seq_r6c h5 (IRuns.seq_r6c h6 (IRuns.seq_r6c h7 h8)))))))).mono' ?_ ?_
  · clear h1 h2 h3 h4 hloop h5 h6 h7 h8
    rw [hfull, sg_natAbs]
    apply IState.ext' <;> intros <;> simp [sm, ss, schoolSt] <;> split_ifs <;> simp_all
  · clear h1 h2 h3 h4 hloop h5 h6 h7 h8
    have hxm : zsz (x * 2 ^ m) ≤ N := by
      by_cases hx : x = 0
      · simp [hx, zsz_zero_r6c]
      · rw [zsz, zbits_mul_two_pow hx]; simp [N, zsz, m]; omega
    have hacc : zsz (x * sg y (y.natAbs % 2 ^ m)) ≤ N := by
      rw [hfull, sg_natAbs]; exact zsz_mul_le x y
    have := moveIntCost_le (zsz x); have := moveIntCost_le (zsz y)
    have := moveIntCost_le (zsz (x * sg y (y.natAbs % 2 ^ m)))
    have hc2 : zsz (2 : ℤ) = 2 := by
      rw [show (2 : ℤ) = 2 ^ 1 by norm_num, zsz_two_pow_r6c]
    simp only [smulCost, schoolIter, zsz_zero_r6c, hc2]
    have hmN : m ≤ N := by omega
    have := Nat.mul_le_mul_right (1500 * (N + 2) + 30) hmN
    nlinarith

end NLogN

end

section
-- Source module: NLogN.IEval
/-!
# A functional evaluator for item-language programs

`IOp.run` and `IStmt.run` compute the result state and cost of a program (with fuel for loops and
calls).  A successful evaluation gives an execution (`IStmt.run_exec`), so straight-line code can
be checked by `simp` evaluation instead of step-by-step reasoning.  Input and output operations
are not evaluated (`none`).
-/

namespace NLogN

open IntMul

variable {S P : ℕ}

@[simp] theorem rulerExp_two_pow (m : ℕ) : rulerExp ((2 : ℤ) ^ m) = some m := by
  have h : ((2 : ℤ) ^ m).toNat = 2 ^ m := by
    rw [show ((2 : ℤ) ^ m) = ((2 ^ m : ℕ) : ℤ) by push_cast; rfl, Int.toNat_natCast]
  simp [rulerExp, h, Nat.log2_two_pow]

theorem rulerExp_eq {r : ℤ} {m : ℕ} (h : rulerExp r = some m) : r = 2 ^ m := by
  unfold rulerExp at h; split_ifs at h with h1
  · cases h; exact h1

theorem IOp.run_step {I : List Sym} {o : IOp S} {s s' : IState S} {c : ℕ}
    (h : o.run s = some (s', c)) : o.Step I s s' c := by
  cases o with
  | add i j k =>
    simp only [IOp.run] at h
    split at h
    · rename_i a Li b Lj hi hj
      split_ifs at h with hij
      simp only [Option.some.injEq, Prod.mk.injEq] at h
      obtain ⟨rfl, rfl⟩ := h; exact .add hij hi hj
    · simp at h
  | neg i =>
    simp only [IOp.run] at h; split at h <;> simp at h
    rename_i a L hi; obtain ⟨rfl, rfl⟩ := h; exact .neg hi
  | dup i j =>
    simp only [IOp.run] at h; split at h <;> simp at h
    rename_i a L hi; obtain ⟨hij, rfl, rfl⟩ := h; exact .dup hij hi
  | drop i =>
    simp only [IOp.run] at h; split at h <;> simp at h
    rename_i a L hi; obtain ⟨rfl, rfl⟩ := h; exact .drop hi
  | mv i j =>
    simp only [IOp.run] at h; split at h <;> simp at h
    rename_i a L hi; obtain ⟨hij, rfl, rfl⟩ := h; exact .mv hij hi
  | const i c => simp only [IOp.run, Option.some.injEq, Prod.mk.injEq] at h
                 obtain ⟨rfl, rfl⟩ := h; exact .const c
  | mark i => simp only [IOp.run, Option.some.injEq, Prod.mk.injEq] at h
              obtain ⟨rfl, rfl⟩ := h; exact .mark
  | unmark i =>
    simp only [IOp.run] at h; split at h <;> simp at h
    rename_i L hi; obtain ⟨rfl, rfl⟩ := h; exact .unmark hi
  | shl i j =>
    simp only [IOp.run] at h; split at h
    · rename_i a Li r Lj hi hj
      split at h
      · rename_i m hm
        simp at h; obtain ⟨hij, rfl, rfl⟩ := h
        exact .shl hij hi (by rw [hj, rulerExp_eq hm])
      · simp at h
    · simp at h
  | split i j k =>
    simp only [IOp.run] at h; split at h
    · rename_i a Li r Lj hi hj
      split at h
      · rename_i m hm
        simp at h; obtain ⟨⟨h1, h2, h3⟩, rfl, rfl⟩ := h
        exact .split h1 h2 h3 hi (by rw [hj, rulerExp_eq hm])
      · simp at h
    · simp at h
  | cat i j k =>
    simp only [IOp.run] at h; split at h
    · rename_i a Li r Lj b Lk hi hj hk
      split at h
      · rename_i m hm
        simp at h; obtain ⟨⟨h1, h2, h3, h4, h5, h6⟩, rfl, rfl⟩ := h
        have hb : b = ((b.toNat : ℕ) : ℤ) := by omega
        have e2 : ((2 ^ m : ℕ) : ℤ) = (2 : ℤ) ^ m := by push_cast; rfl
        refine .cat (b := b.toNat) h1 h2 h3 h4 (by omega) hi (by rw [hj, rulerExp_eq hm])
          (by rw [hk, ← hb])
      · simp at h
    · simp at h
  | read => simp [IOp.run] at h
  | write => simp [IOp.run] at h

theorem IStmt.run_exec {I : List Sym} {iprog : Fin P → IStmt S P} :
    ∀ (n : ℕ) (p : IStmt S P) (s s' : IState S) (c : ℕ), IStmt.run iprog n p s = some (s', c) →
      IExec I iprog p s s' c := by
  intro n
  induction n using Nat.strong_induction_on with
  | _ n ihn =>
  intro p
  induction p with
  | skip => intro s s' c h; simp [IStmt.run] at h; obtain ⟨rfl, rfl⟩ := h; exact .skip s
  | op o => intro s s' c h; simp only [IStmt.run] at h; exact .op (IOp.run_step h)
  | seq p q ihp ihq =>
    intro s s' c h
    simp only [IStmt.run] at h
    split at h <;> try simp at h
    rename_i s₁ c₁ h₁
    split at h <;> try simp at h
    rename_i s₂ c₂ h₂
    obtain ⟨rfl, rfl⟩ := h
    exact .seq (ihp _ _ _ h₁) (ihq _ _ _ h₂)
  | ite i f p q ihp ihq =>
    intro s s' c h
    simp only [IStmt.run] at h
    split_ifs at h with hf
    · obtain ⟨⟨s₁, c₁⟩, h₁, he⟩ := Option.map_eq_some_iff.mp h
      simp only [Prod.mk.injEq] at he; obtain ⟨rfl, rfl⟩ := he
      exact .iteT hf (ihp _ _ _ h₁)
    · obtain ⟨⟨s₁, c₁⟩, h₁, he⟩ := Option.map_eq_some_iff.mp h
      simp only [Prod.mk.injEq] at he; obtain ⟨rfl, rfl⟩ := he
      exact .iteF (by simpa using hf) (ihq _ _ _ h₁)
  | loop i f p ihp =>
    intro s s' c h
    rcases n with _ | n
    · simp [IStmt.run] at h
    simp only [IStmt.run] at h
    split_ifs at h with hf
    · split at h <;> try simp at h
      rename_i s₁ c₁ h₁
      split at h <;> try simp at h
      rename_i s₂ c₂ h₂
      obtain ⟨rfl, rfl⟩ := h
      exact .loopT hf (ihp _ _ _ h₁) (ihn n (by omega) _ _ _ _ h₂)
    · simp at h; obtain ⟨rfl, rfl⟩ := h; exact .loopF (by simpa using hf)
  | call j =>
    intro s s' c h
    rcases n with _ | n
    · simp [IStmt.run] at h
    simp only [IStmt.run] at h
    obtain ⟨⟨s₁, c₁⟩, h₁, he⟩ := Option.map_eq_some_iff.mp h
    simp only [Prod.mk.injEq] at he; obtain ⟨rfl, rfl⟩ := he
    exact .call (ihn n (by omega) _ _ _ _ h₁)

theorem IRuns.of_run {I : List Sym} {iprog : Fin P → IStmt S P} {p : IStmt S P} {s t : IState S}
    {c : ℕ} (n : ℕ) {r : IState S × ℕ} (h : IStmt.run iprog n p s = some r) (ht : r.1 = t)
    (hc : r.2 ≤ c) : IRuns I iprog p s t c :=
  ⟨r.2, hc, ht ▸ IStmt.run_exec n p s r.1 r.2 (by rw [h])⟩

end NLogN

end

section
-- Source module: NLogN.SSBase
/-!
# Schönhage–Strassen in the item language: stack layout and Fermat-ring arithmetic

The program uses `NS` item stacks with fixed roles, so that stack (in)equalities are decided by
`simp`.  The current ring `ℤ/(2^n+1)` is given by the ruler `2^n` on top of `RN` and the modulus
`2^n+1` on top of `RF`.
-/

namespace NLogN

open IntMul

@[simp] theorem runsTo_some {S : ℕ} (r : IState S × ℕ) (t : IState S) (c : ℕ) :
    runsTo (some r) t c ↔ r.1 = t ∧ r.2 ≤ c := Iff.rfl

theorem IRuns.of_runsTo_r6c {S P : ℕ} {I : List Sym} {iprog : Fin P → IStmt S P} {p : IStmt S P}
    {s t : IState S} {c : ℕ} (n : ℕ) (h : runsTo (IStmt.run iprog n p s) t c) :
    IRuns I iprog p s t c := by
  unfold runsTo at h
  split at h
  · rename_i r hr; exact IRuns.of_run n hr h.1 h.2
  · exact h.elim

theorem cls_int (z : ℤ) : cls (some (.int z)) =
    if z = 0 then .zero else if z < 0 then .neg else .pos := rfl

@[simp] theorem cls_int_neg (z : ℤ) : cls (some (.int z)) = .neg ↔ z < 0 := by
  rw [cls_int]; split_ifs <;> simp_all <;> omega

@[simp] theorem IState.self_eq_upd {S : ℕ} (s : IState S) (i : Fin S) (L : List Item) :
    s = s.upd i L ↔ s.G i = L := by
  constructor
  · intro h; rw [h]; simp
  · intro h; rw [← h]; simp

@[simp] theorem IState.upd_eq_self {S : ℕ} (s : IState S) (i : Fin S) (L : List Item) :
    s.upd i L = s ↔ s.G i = L := by
  rw [eq_comm]; exact IState.self_eq_upd s i L

/-! ## Fermat reduction -/

variable {P : ℕ}

end NLogN

namespace NLogN

open IntMul

variable {P : ℕ} {I : List Sym} {iprog : Fin P → IStmt NS P}

end NLogN

end

section
-- Source module: NLogN.HExpr
/-!
# Expressions over register stacks

`Ex S` are integer expressions whose leaves read the top item of a register stack.  `Ex.code z e`
evaluates `e` onto the value stack `z.V`, using the scratch stacks of `z` and leaving every other
stack unchanged (`Ex.code_runs`).
-/

namespace NLogN

open IntMul

variable {S P : ℕ} {I : List Sym} {iprog : Fin P → IStmt S P}

theorem IState.top_eq_r6c {s : IState S} {i : Fin S} {a : ℤ} {L : List Item} (h : s.G i = .int a :: L) :
    s.top i = a := by simp [IState.top, h]

namespace Ex

end Ex

/-! ## Long division -/

namespace Ex

end Ex

/-! ## Code -/

namespace Ex

end Ex

end NLogN

end