feat(MultiTapeTM): the identity is computable in linear time and zero space

[crei]

As a combinator, this might not look like a useful lemma, but it will together with some more results: It for example allows us to copy from one tape to another.

[BoltonBailey]

I think this seems like a good addition. My only feedback is that it looked like the proofs could be golfed a bit (I asked Claude and it indeed came up with some proofs that look shorter and cleaner to me, attached below if you want to use them).

Code

/-- Over an input symbol, the copy machine emits it and moves right. -/
lemma step_scan {n : ℕ} (hn : n < input.length) (out : List Symbol) :
    copy.step (cfg input (some ()) ⟨n + 1, by omega⟩ out) =
      cfg input (some ()) ⟨n + 2, by omega⟩ (out ++ [input[n]]) := by
  rw [step, inputSymbolInner n (by simp only [cfg]; omega) hn]
  refine cfg_ext rfl ?_ rfl
  simp only [Action.apply]
  exact moveInputPos_pos_of_ne_right _ (by simp [cfg]; omega)

/-- On the blank at the right end of the input, the copy machine halts in place. -/
lemma step_halt (out : List Symbol) :
    copy.step (cfg input (some ()) ⟨input.length + 1, by omega⟩ out) =
      cfg input none ⟨input.length + 1, by omega⟩ out := by
  rw [step, inputSymbol_eq_none_of_boundary (Or.inr rfl)]
  exact cfg_ext rfl (by simp [cfg, copy, Action.apply]) (by simp [cfg, copy, Action.apply])

/-- After `n ≤ input.length` steps, the copy machine has copied the first `n` input symbols to the
output and its head is over the `n`-th cell of the input. -/
lemma runFrom_scan (n : ℕ) (hn : n ≤ input.length) :
    copy.runFrom (copy.initCfg input) n =
      cfg input (some ()) ⟨n + 1, by omega⟩ (input.take n) := by
  induction n with
  | zero => exact cfg_ext rfl rfl rfl
  | succ n ih =>
    rw [runFrom_succ_eq_step', ih (by omega), step_scan (by omega), List.take_add_one,
      List.getElem?_eq_getElem (by omega), Option.toList_some]

/-- The complete run: after `input.length + 1` steps the copy machine has halted with the input
copied to the output. -/
lemma runFrom_full (input : List Symbol) :
    copy.runFrom (copy.initCfg input) (input.length + 1) =
      cfg input none ⟨input.length + 1, by omega⟩ input := by
  rw [runFrom_succ_eq_step', runFrom_scan input.length le_rfl, List.take_length, step_halt]

/-- The copy machine outputs its input unchanged, in `input.length + 1` steps and zero space. -/
theorem computesInTimeAndSpace (input : List Symbol) :
    ComputesInTimeAndSpace copy input input (input.length + 1) 0 := by
  refine ⟨?_, ?_, copy.spaceUsed_zero_tapes_eq_zero _ _ rfl⟩ <;> rw [runFrom_full] <;> rfl

end Copy

variable {α : Type*}

/-- The identity function is computable in one step per input symbol and zero space. -/
public theorem computableInTimeAndSpace_id {enc : α ↪ List Bool} :
    ComputableInTimeAndSpace (id : α → α) enc enc
      (fun a => (enc a).length + 1) (fun _ => 0) :=
  ⟨0, Unit, inferInstance, copy, fun a =>
    ⟨_, le_rfl, _, le_rfl, Copy.computesInTimeAndSpace (enc a)⟩⟩

end Turing.MultiTapeTM

[barni120400]

Consider using a more concise definition of the cfg:

def cfg (input : List Symbol) (q : Option Unit) (n : ℕ) : Cfg 0 Symbol Unit input := ⟨q, ⟨min n input.length + 1, by omega⟩, fun _ _ => none, fun _ => 0, input.take n⟩

the rest of the lemmas also benefit from it

[barni120400]

This is a general lemma, now specific for Unit. Is there a better place for this lemma?

[barni120400]

Suggested change

	copy.step (cfg input (some ()) ⟨input.length + 1, by omega⟩ out) =
	cfg input none ⟨input.length + 1, by omega⟩ out := by
	have hsym : (cfg input (some ()) ⟨input.length + 1, by omega⟩ out).inputSymbol =
	copy.step (cfg input (some ()) (Fin.last _) out) =
	cfg input none (Fin.last _) out := by
	have hsym : (cfg input (some ()) (Fin.last _) out).inputSymbol =

[barni120400]

Suggested change

	cfg input none ⟨input.length + 1, by omega⟩ input := by
	rw [runFrom_succ_eq_step', runFrom_scan input.length le_rfl, List.take_length, step_halt]
	cfg input none (Fin.last _) input := by
	rw [runFrom_succ_eq_step', runFrom_scan input.length le_rfl, List.take_length]
	exact step_halt input