TakeWhile (· ≠ sep) is Block-Realizable

We prove List.takeWhile (· ≠ sep) is block-realizable by showing:

takeWhile (· ≠ sep) = reverse ∘ dropFromLastSep sep ∘ reverse

and proving dropFromLastSep sep is block-realizable via a simple 7-state TM0 machine that iteratively scans for sep and erases the block prefix up to (and including) the first sep, repeating until no sep remains.

Key results

• dropUntilFirstSep: drops through the first occurrence of sep.
• tm0_dropFromLastSep_direct: realizes dropFromLastSep sep by TM0.
• tm0_takeWhileNeSep': realizes List.takeWhile (· ≠ sep) by TM0.

Mathematical lemmas

theorem takeWhile_eq_rev_dropFromLastSep_rev' {Γ : Type} [Inhabited Γ] [DecidableEq Γ] (sep : Γ) (l : List Γ) : List.takeWhile (fun (x : Γ) => !decide (x = sep)) l = (dropFromLastSep sep l.reverse).reverse

theorem takeWhile_eq_comp_rev_drop_rev {Γ : Type} [Inhabited Γ] [DecidableEq Γ] (sep : Γ) : (fun (l : List Γ) => List.takeWhile (fun (x : Γ) => !decide (x = sep)) l) = List.reverse ∘ dropFromLastSep sep ∘ List.reverse

dropUntilFirstSep

def dropUntilFirstSep {Γ : Type} [DecidableEq Γ] (sep : Γ) : List Γ → List Γ

Drop everything up to and including the FIRST occurrence of sep. If sep ∉ l, returns [].

Equations

• dropUntilFirstSep sep [] = []
• dropUntilFirstSep sep (c :: rest) = if c = sep then rest else dropUntilFirstSep sep rest

theorem dropUntilFirstSep_length_lt {Γ : Type} [DecidableEq Γ] (sep : Γ) (block : List Γ) (hmem : sep ∈ block) : (dropUntilFirstSep sep block).length < block.length

theorem dropUntilFirstSep_ne_default {Γ : Type} [Inhabited Γ] [DecidableEq Γ] (sep : Γ) (block : List Γ) (hblock : ∀ g ∈ block, g ≠ default) (g : Γ) : g ∈ dropUntilFirstSep sep block → g ≠ default

theorem dropUntilFirstSep_append_cons {Γ : Type} [DecidableEq Γ] (sep : Γ) (left right : List Γ) (hleft : ∀ g ∈ left, g ≠ sep) : dropUntilFirstSep sep (left ++ sep :: right) = right

theorem dropFromLastSep_eq_of_dropUntilFirstSep {Γ : Type} [Inhabited Γ] [DecidableEq Γ] (sep : Γ) (block : List Γ) (hmem : sep ∈ block) : dropFromLastSep sep block = dropFromLastSep sep (dropUntilFirstSep sep block)

theorem block_first_sep_decomp {Γ : Type} [DecidableEq Γ] (sep : Γ) (block : List Γ) (hmem : sep ∈ block) : ∃ (pfx : List Γ) (rest : List Γ), block = pfx ++ sep :: rest ∧ (∀ g ∈ pfx, g ≠ sep) ∧ dropUntilFirstSep sep block = rest

Machine definition

inductive DFLState : Type

State type for the dropFromLastSep TM0 machine. Only 7 plain states.

• scan : DFLState
• goBack : DFLState
• erase : DFLState
• wSep : DFLState
• wOther : DFLState
• rewind : DFLState
• done : DFLState

instance instDecidableEqDFLState : DecidableEq DFLState

Equations

• instDecidableEqDFLState x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance instInhabitedDFLState : Inhabited DFLState

Equations

• instInhabitedDFLState = { default := DFLState.scan }

instance instFintypeDFLState : Fintype DFLState

Equations

• One or more equations did not get rendered due to their size.

noncomputable def dflMachine {Γ : Type} [Inhabited Γ] [DecidableEq Γ] (sep : Γ) : Turing.TM0.Machine Γ DFLState

The dropFromLastSep TM0 machine.

Equations

• One or more equations did not get rendered due to their size.
• dflMachine sep DFLState.goBack a = if a = default then some (DFLState.erase, Turing.TM0.Stmt.move Turing.Dir.right) else some (DFLState.goBack, Turing.TM0.Stmt.move Turing.Dir.left)
• dflMachine sep DFLState.erase a = if a = sep then some (DFLState.wSep, Turing.TM0.Stmt.write default) else if a = default then none else some (DFLState.wOther, Turing.TM0.Stmt.write default)
• dflMachine sep DFLState.wSep a = some (DFLState.scan, Turing.TM0.Stmt.move Turing.Dir.right)
• dflMachine sep DFLState.wOther a = some (DFLState.erase, Turing.TM0.Stmt.move Turing.Dir.right)
• dflMachine sep DFLState.rewind a = if a = default then some (DFLState.done, Turing.TM0.Stmt.move Turing.Dir.right) else some (DFLState.rewind, Turing.TM0.Stmt.move Turing.Dir.left)
• dflMachine sep DFLState.done a = none

Key tape lemma

theorem tape_erase_step {Γ : Type} [Inhabited Γ] (c : Γ) (rest : List Γ) : Turing.Tape.move Turing.Dir.right (Turing.Tape.write default (Turing.Tape.mk₁ (c :: rest))) = Turing.Tape.mk₁ rest

theorem tape_move_left_right_mk₁ {Γ : Type} [Inhabited Γ] (l : List Γ) : Turing.Tape.move Turing.Dir.right (Turing.Tape.move Turing.Dir.left (Turing.Tape.mk₁ l)) = Turing.Tape.mk₁ l

Phase lemmas

theorem dfl_scan_right {Γ : Type} [Inhabited Γ] [DecidableEq Γ] (sep : Γ) (_hsep : sep ≠ default) (L pfx rest : List Γ) (hpfx_nsep : ∀ g ∈ pfx, g ≠ sep) (hpfx_nd : ∀ g ∈ pfx, g ≠ default) : Turing.Reaches (Turing.TM0.step (dflMachine sep)) { q := DFLState.scan, Tape := Turing.Tape.mk₂ L (pfx ++ rest) } { q := DFLState.scan, Tape := Turing.Tape.mk₂ (pfx.reverse ++ L) rest }

theorem dfl_goBack_after_left {Γ : Type} [Inhabited Γ] [DecidableEq Γ] (sep : Γ) (L R : List Γ) (hL : ∀ g ∈ L, g ≠ default) : Turing.Reaches (Turing.TM0.step (dflMachine sep)) { q := DFLState.goBack, Tape := Turing.Tape.move Turing.Dir.left (Turing.Tape.mk₂ L R) } { q := DFLState.erase, Tape := Turing.Tape.mk₁ (L.reverse ++ R) }

theorem dfl_erase_loop {Γ : Type} [Inhabited Γ] [DecidableEq Γ] (sep : Γ) (_hsep : sep ≠ default) (pfx rest : List Γ) (hpfx_nsep : ∀ g ∈ pfx, g ≠ sep) (hpfx_nd : ∀ g ∈ pfx, g ≠ default) : Turing.Reaches (Turing.TM0.step (dflMachine sep)) { q := DFLState.erase, Tape := Turing.Tape.mk₁ (pfx ++ sep :: rest) } { q := DFLState.scan, Tape := Turing.Tape.mk₁ rest }

theorem dfl_rewind_after_left {Γ : Type} [Inhabited Γ] [DecidableEq Γ] (sep : Γ) (L R : List Γ) (hL : ∀ g ∈ L, g ≠ default) : Turing.Reaches (Turing.TM0.step (dflMachine sep)) { q := DFLState.rewind, Tape := Turing.Tape.move Turing.Dir.left (Turing.Tape.mk₂ L R) } { q := DFLState.done, Tape := Turing.Tape.mk₁ (L.reverse ++ R) }

Combined iteration lemmas

theorem dfl_one_cycle {Γ : Type} [Inhabited Γ] [DecidableEq Γ] (sep : Γ) (hsep : sep ≠ default) (block' suffix : List Γ) (hblock : ∀ g ∈ block', g ≠ default) (hmem : sep ∈ block') : Turing.Reaches (Turing.TM0.step (dflMachine sep)) { q := DFLState.scan, Tape := Turing.Tape.mk₁ (block' ++ default :: suffix) } { q := DFLState.scan, Tape := Turing.Tape.mk₁ (dropUntilFirstSep sep block' ++ default :: suffix) }

theorem dfl_no_sep_cycle {Γ : Type} [Inhabited Γ] [DecidableEq Γ] (sep : Γ) (hsep : sep ≠ default) (block' suffix : List Γ) (hblock : ∀ g ∈ block', g ≠ default) (hnot : sep ∉ block') : Turing.Reaches (Turing.TM0.step (dflMachine sep)) { q := DFLState.scan, Tape := Turing.Tape.mk₁ (block' ++ default :: suffix) } { q := DFLState.done, Tape := Turing.Tape.mk₁ (block' ++ default :: suffix) }

Full computation

theorem dfl_step_done {Γ : Type} [Inhabited Γ] [DecidableEq Γ] (sep : Γ) (T : Turing.Tape Γ) : Turing.TM0.step (dflMachine sep) { q := DFLState.done, Tape := T } = none

The machine halts in state done.

theorem dfl_full_reaches {Γ : Type} [Inhabited Γ] [DecidableEq Γ] (sep : Γ) (hsep : sep ≠ default) (block suffix : List Γ) (hblock : ∀ g ∈ block, g ≠ default) (_hsuffix : ∀ g ∈ suffix, g ≠ default) : Turing.Reaches (Turing.TM0.step (dflMachine sep)) (Turing.TM0.init (block ++ default :: suffix)) { q := DFLState.done, Tape := Turing.Tape.mk₁ (dropFromLastSep sep block ++ default :: suffix) }

Main results

theorem tm0_dropFromLastSep_direct {Γ : Type} [Inhabited Γ] [DecidableEq Γ] [Fintype Γ] (sep : Γ) (hsep : sep ≠ default) : TM0RealizesBlock Γ (dropFromLastSep sep)

dropFromLastSep sep is block-realizable.

theorem tm0_takeWhileNeSep' {Γ : Type} [Inhabited Γ] [DecidableEq Γ] [Fintype Γ] (sep : Γ) (hsep : sep ≠ default) : TM0RealizesBlock Γ (List.takeWhile fun (x : Γ) => !decide (x = sep))

takeWhile (· ≠ sep) is block-realizable.