The windows of a run are locally consistent #
localCfgOf M acc c js is the local configuration read off a configuration c and its
successor at the window js; its encoding is the assignment of the run on the window's
variables (encode_localCfgOf), and it is locally consistent
(locallyConsistent_localCfgOf): the completeness half of the tableau's correctness
(planning/succinct-cook-levin.md, S1). The proof is the case analysis of the paper's
lem:correct-tableau on where the heads are, with the clamping of the input heads
(Turing.moveInputPos) matched against the tableau's rule (newOffset).
Positions #
The local configuration of a run #
def
MIPRE.TM.CookLevin.localCfgOf
{i w : ℕ}
{Symbol : Type u_1}
{State : Type u_2}
[DecidableEq Symbol]
{S : ℕ}
(M : Turing.MultiInputTM i w Symbol State)
(acc : Symbol)
{input : Fin i → List Symbol}
(c : Turing.MultiInputTM.Cfg i w Symbol State input)
(js : Tape i w → Center S)
:
LocalCfg i w Symbol State
The local configuration of a configuration and its successor at the window js.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
MIPRE.TM.CookLevin.cfgAt_succ
{i w : ℕ}
{Symbol : Type u_1}
{State : Type u_2}
(M : Turing.MultiInputTM i w Symbol State)
{input : Fin i → List Symbol}
(t : ℕ)
:
theorem
MIPRE.TM.CookLevin.encode_localCfgOf
{i w : ℕ}
{Symbol : Type u_1}
{State : Type u_2}
[DecidableEq Symbol]
[DecidableEq State]
{S : ℕ}
(M : Turing.MultiInputTM i w Symbol State)
(acc : Symbol)
{input : Fin i → List Symbol}
(G : ℕ)
(t : Fin S)
(js : Tape i w → Center S)
(v : WinVar i w Symbol State)
:
The encoding of the local configuration of the run at (t, js) is the run's assignment
on the window's variables.
Heads #
theorem
MIPRE.TM.CookLevin.headPre_localCfgOf
{i w : ℕ}
{Symbol : Type u_1}
{State : Type u_2}
[DecidableEq Symbol]
{S : ℕ}
(M : Turing.MultiInputTM i w Symbol State)
(acc : Symbol)
{input : Fin i → List Symbol}
(c : Turing.MultiInputTM.Cfg i w Symbol State input)
(js : Tape i w → Center S)
(d : Tape i w)
(δ : Fin 5)
:
The head of tape d is in the window at offset δ iff its cell is that cell.
theorem
MIPRE.TM.CookLevin.headAt_localCfgOf
{i w : ℕ}
{Symbol : Type u_1}
{State : Type u_2}
[DecidableEq Symbol]
{S : ℕ}
(M : Turing.MultiInputTM i w Symbol State)
(acc : Symbol)
{input : Fin i → List Symbol}
(c : Turing.MultiInputTM.Cfg i w Symbol State input)
(js : Tape i w → Center S)
(d : Tape i w)
(δ : Fin 5)
(h : headCell c d = ↑↑(cellIdx (js d) δ))
:
(localCfgOf M acc c js).HeadAt d δ
theorem
MIPRE.TM.CookLevin.not_twoHeads_localCfgOf
{i w : ℕ}
{Symbol : Type u_1}
{State : Type u_2}
[DecidableEq Symbol]
{S : ℕ}
(M : Turing.MultiInputTM i w Symbol State)
(acc : Symbol)
{input : Fin i → List Symbol}
(c : Turing.MultiInputTM.Cfg i w Symbol State input)
(js : Tape i w → Center S)
(d : Tape i w)
:
¬(localCfgOf M acc c js).TwoHeads d
No two heads of a tape in a window of a run.
The step, componentwise #
theorem
MIPRE.TM.CookLevin.step_state
{i w : ℕ}
{Symbol : Type u_1}
{State : Type u_2}
(M : Turing.MultiInputTM i w Symbol State)
{input : Fin i → List Symbol}
(c : Turing.MultiInputTM.Cfg i w Symbol State input)
{q : State}
(hst : c.state = some q)
:
theorem
MIPRE.TM.CookLevin.step_inputPos
{i w : ℕ}
{Symbol : Type u_1}
{State : Type u_2}
(M : Turing.MultiInputTM i w Symbol State)
{input : Fin i → List Symbol}
(c : Turing.MultiInputTM.Cfg i w Symbol State input)
{q : State}
(hst : c.state = some q)
(j : Fin i)
:
(Turing.MultiInputTM.step c).inputPos j = Turing.MultiTapeTM.moveInputPos (c.inputPos j) ((M.tr q c.inputSymbols c.workTapeSymbols).inputMoves j)
theorem
MIPRE.TM.CookLevin.step_workTapePos
{i w : ℕ}
{Symbol : Type u_1}
{State : Type u_2}
(M : Turing.MultiInputTM i w Symbol State)
{input : Fin i → List Symbol}
(c : Turing.MultiInputTM.Cfg i w Symbol State input)
{q : State}
(hst : c.state = some q)
(j : Fin w)
:
(Turing.MultiInputTM.step c).workTapePos j = c.workTapePos j + ↑((M.tr q c.inputSymbols c.workTapeSymbols).workActions j).2
theorem
MIPRE.TM.CookLevin.step_workTapes
{i w : ℕ}
{Symbol : Type u_1}
{State : Type u_2}
(M : Turing.MultiInputTM i w Symbol State)
{input : Fin i → List Symbol}
(c : Turing.MultiInputTM.Cfg i w Symbol State input)
{q : State}
(hst : c.state = some q)
(j : Fin w)
:
(Turing.MultiInputTM.step c).workTapes j = match (motive := Option (Option Symbol) → ℤ → Option Symbol)
((M.tr q c.inputSymbols c.workTapeSymbols).workActions j).1 with
| none => c.workTapes j
| some s => Function.update (c.workTapes j) (c.workTapePos j) s
theorem
MIPRE.TM.CookLevin.moveInputPos_sub_le
{n : ℕ}
(p : Fin (n + 2))
(m : SignType)
:
-1 ≤ ↑↑(Turing.MultiTapeTM.moveInputPos p m) - ↑↑p ∧ ↑↑(Turing.MultiTapeTM.moveInputPos p m) - ↑↑p ≤ 1
theorem
MIPRE.TM.CookLevin.headCell_step_le
{i w : ℕ}
{Symbol : Type u_1}
{State : Type u_2}
{S : ℕ}
(M : Turing.MultiInputTM i w Symbol State)
{input : Fin i → List Symbol}
(c : Turing.MultiInputTM.Cfg i w Symbol State input)
(d : Tape i w)
:
A head moves by at most one cell in a step.
theorem
MIPRE.TM.CookLevin.far_localCfgOf
{i w : ℕ}
{Symbol : Type u_1}
{State : Type u_2}
[DecidableEq Symbol]
{S : ℕ}
(M : Turing.MultiInputTM i w Symbol State)
(acc : Symbol)
{input : Fin i → List Symbol}
(c : Turing.MultiInputTM.Cfg i w Symbol State input)
(js : Tape i w → Center S)
(d : Tape i w)
(hfar : (localCfgOf M acc c js).HeadFar d)
:
(localCfgOf M acc c js).cellPost d = (localCfgOf M acc c js).cellPre d 2 ∧ (localCfgOf M acc c js).headPost d = false
A tape whose head is not near the center keeps its center cell and has no head there after the step.
The cells under the heads #
theorem
MIPRE.TM.CookLevin.inputCellVal_eq
{Symbol : Type u_1}
{S : ℕ}
(x : List Symbol)
(p : Pos S)
(hnb : ¬p.IsBdry)
:
inputCellVal x p = if 3 ≤ ↑p then
match x[↑p - 3]? with
| some s => CellVal.sym s
| none => CellVal.blank
else CellVal.blank
An interior input cell: the symbol of the input at index p - 3, if any, else a blank.
theorem
MIPRE.TM.CookLevin.inputCellVal_bdry_iff
{Symbol : Type u_1}
{S : ℕ}
(x : List Symbol)
(p : Pos S)
:
theorem
MIPRE.TM.CookLevin.toOpt_inputCellVal_headCell
{i w : ℕ}
{Symbol : Type u_1}
{State : Type u_2}
{S : ℕ}
{input : Fin i → List Symbol}
(c : Turing.MultiInputTM.Cfg i w Symbol State input)
(j : Fin i)
(p : Pos S)
(hp : ↑p = ↑(c.inputPos j) + 2)
(hnb : ¬p.IsBdry)
:
The symbol under an input head is the cell of the tableau at the head's cell.
Head positions #
structure
MIPRE.TM.CookLevin.HeadsIn
{i w : ℕ}
{Symbol : Type u_1}
{State : Type u_2}
{input : Fin i → List Symbol}
(c : Turing.MultiInputTM.Cfg i w Symbol State input)
(S : ℕ)
:
The bounds under which every head is on an interior cell; they hold at every time
t ≤ S of a run (headsIn_cfgAt), since a head moves at most one position per step.
Instances For
The full step #
theorem
MIPRE.TM.CookLevin.fullStep_localCfgOf
{i w : ℕ}
{Symbol : Type u_1}
{State : Type u_2}
[DecidableEq Symbol]
{S : ℕ}
(M : Turing.MultiInputTM i w Symbol State)
(acc : Symbol)
{input : Fin i → List Symbol}
(c : Turing.MultiInputTM.Cfg i w Symbol State input)
(js : Tape i w → Center S)
(hin : HeadsIn c S)
(δ : Tape i w → Fin 5)
(hδ : ∀ (d : Tape i w), 1 ≤ ↑(δ d) ∧ ↑(δ d) ≤ 3 ∧ (localCfgOf M acc c js).HeadAt d (δ d))
:
FullStep M acc (localCfgOf M acc c js) δ
When every head is at an offset 1..3, the local configuration of the run satisfies the
full transition check.
theorem
MIPRE.TM.CookLevin.locallyConsistent_localCfgOf
{i w : ℕ}
{Symbol : Type u_1}
{State : Type u_2}
[DecidableEq Symbol]
{S : ℕ}
(M : Turing.MultiInputTM i w Symbol State)
(acc : Symbol)
{input : Fin i → List Symbol}
(c : Turing.MultiInputTM.Cfg i w Symbol State input)
(js : Tape i w → Center S)
(hin : HeadsIn c S)
:
LocallyConsistent M acc (localCfgOf M acc c js)
The windows of a run are locally consistent.