feat(Foundations/Data): Function view for Turing tapes

Cslib/Foundations/Data/BiTape.lean

@@ -78,6 +78,33 @@ def mk₁ (l : List Symbol) : BiTape Symbol :=
   | [] => ∅
   | h :: t => { head := some h, left := ∅, right := StackTape.map_some t }
 
+open scoped Int in
+/-- Returns the tape symbol at positon `p` relative to the head, where
+positive numbers are right of the head and negative are left of the head. -/
+@[scoped grind]
+def get (t : BiTape Symbol) : ℤ → Option Symbol
+  | 0 => t.head
+  | (p' + 1 : Nat) => t.right.toList[p']?.getD none
+  | -[p'+1] => t.left.toList[p']?.getD none
+
+/-- Two tapes are equal if and only if their `get` functions are equal. This allows to view
+tapes as functions `ℤ → Option Symbol`. -/
+@[ext]
+lemma ext_get (t₁ t₂ : BiTape Symbol) (h_get_eq : ∀ p, t₁.get p = t₂.get p) : t₁ = t₂ := by
+  obtain ⟨head₁, left₁, right₁⟩ := t₁
+  obtain ⟨head₂, left₂, right₂⟩ := t₂
+  have h_head : head₁ = head₂ := by simpa [get] using h_get_eq 0
+  have h_right : right₁ = right₂ := by
+    apply StackTape.ext_get
+    intro p
+    simpa [get] using h_get_eq (p + 1)
+  have h_left : left₁ = left₂ := by
+    apply StackTape.ext_get
+    intro p
+    simpa [get] using h_get_eq (Int.negSucc p)
+  grind
+
+
 section Move
 
 /--
@@ -114,13 +141,81 @@ lemma move_left_move_right (t : BiTape Symbol) : t.move_left.move_right = t := b
 lemma move_right_move_left (t : BiTape Symbol) : t.move_right.move_left = t := by
   simp [move_left, move_right]
 
+/-- Translate an optional direction into a head movement offset, where the positive
+direction is to the right. -/
+@[scoped grind]
+def optionDirToInt (d : Option Dir) : ℤ :=
+  match d with
+  | none => 0
+  | some .left => -1
+  | some .right => 1
+
+@[simp, scoped grind =]
+lemma get_move_left (t : BiTape Symbol) (p : ℤ) :
+    (t.move_left).get p = t.get (p - 1) := by
+  unfold move_left get
+  match p with
+  | Int.ofNat 0 =>
+    rw [show Int.ofNat 0 - 1 = Int.negSucc 0 from rfl]
+    simp [StackTape.head_eq_getD]
+  | Int.ofNat 1 => simp
+  | Int.ofNat (n + 2) =>
+    rw [show Int.ofNat (n + 2) - 1 = Int.ofNat (n + 1) by lia]
+    simp
+  | Int.negSucc n => simp
+
+@[simp, scoped grind =]
+lemma get_move_right (t : BiTape Symbol) (p : ℤ) :
+    (t.move_right).get p = t.get (p + 1) := by
+  unfold move_right get
+  match p with
+  | Int.ofNat n =>
+    rw [show Int.ofNat n + 1 = Int.ofNat (n + 1) by lia]
+    cases n <;> simp [StackTape.head_eq_getD]
+  | Int.negSucc 0 => simp
+  | Int.negSucc (n + 1) =>
+    rw [show Int.negSucc (n + 1) + 1 = Int.negSucc n from rfl]
+    simp
+
+@[simp, scoped grind =]
+lemma get_optionMove (t : BiTape Symbol) (d : Option Dir) (p : ℤ) :
+    (t.optionMove d).get p = t.get (p + optionDirToInt d) := by
+  unfold optionMove optionDirToInt
+  grind [move]
+
+@[simp, scoped grind =]
+lemma get_move_right_iterate (t : BiTape Symbol) (n : ℕ) (p : ℤ) :
+    (move_right^[n] t).get p = t.get (p + n):= by
+  induction n generalizing t p with
+  | zero => simp
+  | succ n ih => simp [Function.iterate_succ_apply, ih, Int.add_assoc]
+
+@[simp, scoped grind =]
+lemma get_move_left_iterate (t : BiTape Symbol) (n : ℕ) (p : ℤ) :
+    (move_left^[n] t).get p = t.get (p - n):= by
+  induction n generalizing t p with
+  | zero => simp
+  | succ n ih =>
+    have : p - n - 1 = p - (n + 1) := by lia
+    simp [Function.iterate_succ_apply, ih, this]
+
 end Move
 
 /--
 Write a value under the head of the `BiTape`.
 -/
 def write (t : BiTape Symbol) (a : Option Symbol) : BiTape Symbol := { t with head := a }
 
+@[simp, scoped grind =]
+lemma get_write (t : BiTape Symbol) (a : Option Symbol) :
+    (t.write a).get = Function.update t.get 0 a := by
+  unfold write get Function.update
+  funext p
+  match p with
+  | Int.ofNat 0 => simp
+  | Int.ofNat (n + 1) => grind
+  | Int.negSucc n => simp
+
 /--
 The space used by a `BiTape` is the number of symbols
 between and including the head, and leftmost and rightmost non-blank symbols on the `BiTape`.

Cslib/Foundations/Data/StackTape.lean

@@ -106,6 +106,25 @@ def head (l : StackTape Symbol) : Option Symbol :=
   | [] => none
   | h :: _ => h
 
+@[scoped grind =]
+lemma head_eq_getD (s : StackTape Symbol) : s.head = s.toList[0]?.getD none := by
+  unfold head; cases s.toList <;> simp
+
+@[simp, scoped grind =]
+lemma tail_getElem? (s : StackTape Symbol) (n : ℕ) :
+    s.tail.toList[n]? = s.toList[n + 1]? := by
+  cases s with | mk l h => cases l <;> simp [tail, nil]
+
+@[simp, scoped grind =]
+lemma cons_getD_zero (x : Option Symbol) (s : StackTape Symbol) :
+    (cons x s).toList[0]?.getD none = x := by
+  cases x <;> (cases s with | mk l h => cases l <;> simp [cons])
+
+@[simp, scoped grind =]
+lemma cons_getD_succ (x : Option Symbol) (s : StackTape Symbol) (n : ℕ) :
+    (cons x s).toList[n + 1]?.getD none = s.toList[n]?.getD none := by
+  cases x <;> (cases s with | mk l h => cases l <;> simp [cons])
+
 lemma eq_iff (l1 l2 : StackTape Symbol) :
     l1 = l2 ↔ l1.head = l2.head ∧ l1.tail = l2.tail := by
   constructor
@@ -115,13 +134,23 @@ lemma eq_iff (l1 l2 : StackTape Symbol) :
     cases l2 with | mk as2 h2 =>
     cases as1 <;> cases as2 <;> grind
 
+@[ext]
+lemma ext (t₁ t₂ : StackTape Symbol) (h_toList_eq : t₁.toList = t₂.toList) : t₁ = t₂ := by
+  obtain ⟨t₁, h₁⟩ := t₁
+  obtain ⟨t₂, h₂⟩ := t₂
+  simpa using h_toList_eq
+
+@[ext]
+lemma ext_get (t₁ t₂ : StackTape Symbol)
+    (h_get_eq : ∀ p : ℕ, t₁.toList[p]?.getD none = t₂.toList[p]?.getD none) :
+    t₁ = t₂ := by
+  obtain ⟨l₁, h₁⟩ := t₁
+  obtain ⟨l₂, h₂⟩ := t₂
+  grind [List.ext_getElem]
+
 @[simp]
 lemma head_cons (o : Option Symbol) (l : StackTape Symbol) : (cons o l).head = o := by
-  cases o with
-  | none =>
-    cases l with | mk toList hl =>
-    cases toList <;> grind
-  | some a => grind
+  grind
 
 @[simp]
 lemma tail_cons (o : Option Symbol) (l : StackTape Symbol) : (cons o l).tail = l := by