From f57bb82a750c5d3dac3d4f7ed0c5e164a3f4f6c0 Mon Sep 17 00:00:00 2001 From: crei Date: Sat, 18 Apr 2026 18:08:59 +0200 Subject: [PATCH 1/3] Function view for tapes. --- Cslib/Foundations/Data/BiTape.lean | 95 +++++++++++++++++++++++++++ Cslib/Foundations/Data/StackTape.lean | 36 ++++++++++ 2 files changed, 131 insertions(+) diff --git a/Cslib/Foundations/Data/BiTape.lean b/Cslib/Foundations/Data/BiTape.lean index de7a9c8fa..91730dccb 100644 --- a/Cslib/Foundations/Data/BiTape.lean +++ b/Cslib/Foundations/Data/BiTape.lean @@ -78,6 +78,31 @@ def mk₁ (l : List Symbol) : BiTape Symbol := | [] => ∅ | h :: t => { head := some h, left := ∅, right := StackTape.map_some t } +/-- 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. -/ +def get (t : BiTape Symbol) : ℤ → Option Symbol + | Int.ofNat 0 => t.head + | Int.ofNat (Nat.succ p') => t.right.toList[p']?.getD none + | Int.negSucc p' => 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`. -/ +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.succ + have h_left : left₁ = left₂ := by + apply StackTape.ext_get + intro p + simpa [get] using h_get_eq (Int.negSucc p) + simp only [h_head, h_left, h_right] + + section Move /-- @@ -114,6 +139,66 @@ 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. -/ +def optionDirToInt (d : Option Dir) : ℤ := + match d with + | none => 0 + | some .left => -1 + | some .right => 1 + +@[simp] +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) from by grind] + simp + | Int.negSucc n => simp + +@[simp] +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) from by grind] + 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] +lemma get_optionMove (t : BiTape Symbol) (d : Option Dir) (p : ℤ) : + (t.optionMove d).get p = t.get (p + optionDirToInt d) := by + unfold optionMove optionDirToInt + cases d with + | none => simp + | some d => + cases d <;> simp [move, show p + (-1 : ℤ) = p - 1 from by omega] + +@[simp] +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] +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 grind + simp [Function.iterate_succ_apply, ih, this] + end Move /-- @@ -121,6 +206,16 @@ Write a value under the head of the `BiTape`. -/ def write (t : BiTape Symbol) (a : Option Symbol) : BiTape Symbol := { t with head := a } +@[simp] +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) => simp; 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`. diff --git a/Cslib/Foundations/Data/StackTape.lean b/Cslib/Foundations/Data/StackTape.lean index 049d52a19..e64758dba 100644 --- a/Cslib/Foundations/Data/StackTape.lean +++ b/Cslib/Foundations/Data/StackTape.lean @@ -106,6 +106,25 @@ def head (l : StackTape Symbol) : Option Symbol := | [] => none | h :: _ => h +lemma head_eq_getD (s : StackTape Symbol) : + s.head = s.toList[0]?.getD none := by + unfold head; cases s.toList <;> simp + +@[simp] +lemma tail_getD (s : StackTape Symbol) (n : ℕ) : + s.tail.toList[n]?.getD none = s.toList[n + 1]?.getD none := by + cases s with | mk l h => cases l <;> simp [tail, nil] + +@[simp] +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] +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,6 +134,23 @@ lemma eq_iff (l1 l2 : StackTape Symbol) : cases l2 with | mk as2 h2 => cases as1 <;> cases as2 <;> grind +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 + +lemma ext_get (t₁ t₂ : StackTape Symbol) + (h_get_eq : ∀ p, t₁.toList.getD p none = t₂.toList.getD p none) : + t₁ = t₂ := by + apply ext + obtain ⟨l₁, h₁⟩ := t₁ + obtain ⟨l₂, h₂⟩ := t₂ + simp only [List.getD_eq_getElem?_getD] at h_get_eq + have hlen : l₁.length = l₂.length := by grind + apply List.ext_getElem hlen + grind + @[simp] lemma head_cons (o : Option Symbol) (l : StackTape Symbol) : (cons o l).head = o := by cases o with From 642162c56369302365a23c8e2507fe9d164355e8 Mon Sep 17 00:00:00 2001 From: crei Date: Mon, 20 Apr 2026 11:38:51 +0200 Subject: [PATCH 2/3] Apply suggestions from code review Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com> --- Cslib/Foundations/Data/BiTape.lean | 17 +++++++++-------- 1 file changed, 9 insertions(+), 8 deletions(-) diff --git a/Cslib/Foundations/Data/BiTape.lean b/Cslib/Foundations/Data/BiTape.lean index 91730dccb..c2621771d 100644 --- a/Cslib/Foundations/Data/BiTape.lean +++ b/Cslib/Foundations/Data/BiTape.lean @@ -78,12 +78,13 @@ 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. -/ def get (t : BiTape Symbol) : ℤ → Option Symbol - | Int.ofNat 0 => t.head - | Int.ofNat (Nat.succ p') => t.right.toList[p']?.getD none - | Int.negSucc p' => t.left.toList[p']?.getD none + | 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`. -/ @@ -95,7 +96,7 @@ lemma ext_get (t₁ t₂ : BiTape Symbol) (h_get_eq : ∀ p, t₁.get p = t₂.g have h_right : right₁ = right₂ := by apply StackTape.ext_get intro p - simpa [get] using h_get_eq p.succ + simpa [get] using h_get_eq (p + 1) have h_left : left₁ = left₂ := by apply StackTape.ext_get intro p @@ -157,7 +158,7 @@ lemma get_move_left (t : BiTape Symbol) (p : ℤ) : simp [StackTape.head_eq_getD] | Int.ofNat 1 => simp | Int.ofNat (n + 2) => - rw [show Int.ofNat (n + 2) - 1 = Int.ofNat (n + 1) from by grind] + rw [show Int.ofNat (n + 2) - 1 = Int.ofNat (n + 1) by lia] simp | Int.negSucc n => simp @@ -167,7 +168,7 @@ lemma get_move_right (t : BiTape Symbol) (p : ℤ) : unfold move_right get match p with | Int.ofNat n => - rw [show Int.ofNat n + 1 = Int.ofNat (n + 1) from by grind] + 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) => @@ -196,7 +197,7 @@ lemma get_move_left_iterate (t : BiTape Symbol) (n : ℕ) (p : ℤ) : induction n generalizing t p with | zero => simp | succ n ih => - have : p - n - 1 = p - (n + 1) := by grind + have : p - n - 1 = p - (n + 1) := by lia simp [Function.iterate_succ_apply, ih, this] end Move @@ -213,7 +214,7 @@ lemma get_write (t : BiTape Symbol) (a : Option Symbol) : funext p match p with | Int.ofNat 0 => simp - | Int.ofNat (n + 1) => simp; grind + | Int.ofNat (n + 1) => grind | Int.negSucc n => simp /-- From be6855a82b58c4690c37837976eb4c44dc22469b Mon Sep 17 00:00:00 2001 From: crei Date: Mon, 20 Apr 2026 13:07:33 +0200 Subject: [PATCH 3/3] Simplify some proofs and add annotations. --- Cslib/Foundations/Data/BiTape.lean | 25 +++++++++---------- Cslib/Foundations/Data/StackTape.lean | 35 +++++++++++---------------- 2 files changed, 26 insertions(+), 34 deletions(-) diff --git a/Cslib/Foundations/Data/BiTape.lean b/Cslib/Foundations/Data/BiTape.lean index c2621771d..74c6a8190 100644 --- a/Cslib/Foundations/Data/BiTape.lean +++ b/Cslib/Foundations/Data/BiTape.lean @@ -81,6 +81,7 @@ def mk₁ (l : List Symbol) : BiTape Symbol := 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 @@ -88,8 +89,8 @@ def get (t : BiTape Symbol) : ℤ → Option Symbol /-- Two tapes are equal if and only if their `get` functions are equal. This allows to view tapes as functions `ℤ → Option Symbol`. -/ -lemma ext_get (t₁ t₂ : BiTape Symbol) (h_get_eq : ∀ p, t₁.get p = t₂.get p) : - t₁ = t₂ := by +@[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 @@ -101,7 +102,7 @@ lemma ext_get (t₁ t₂ : BiTape Symbol) (h_get_eq : ∀ p, t₁.get p = t₂.g apply StackTape.ext_get intro p simpa [get] using h_get_eq (Int.negSucc p) - simp only [h_head, h_left, h_right] + grind section Move @@ -142,13 +143,14 @@ lemma move_right_move_left (t : BiTape Symbol) : t.move_right.move_left = t := b /-- 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] +@[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 @@ -162,7 +164,7 @@ lemma get_move_left (t : BiTape Symbol) (p : ℤ) : simp | Int.negSucc n => simp -@[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 @@ -175,23 +177,20 @@ lemma get_move_right (t : BiTape Symbol) (p : ℤ) : rw [show Int.negSucc (n + 1) + 1 = Int.negSucc n from rfl] simp -@[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 - cases d with - | none => simp - | some d => - cases d <;> simp [move, show p + (-1 : ℤ) = p - 1 from by omega] + grind [move] -@[simp] +@[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] +@[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 @@ -207,7 +206,7 @@ Write a value under the head of the `BiTape`. -/ def write (t : BiTape Symbol) (a : Option Symbol) : BiTape Symbol := { t with head := a } -@[simp] +@[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 diff --git a/Cslib/Foundations/Data/StackTape.lean b/Cslib/Foundations/Data/StackTape.lean index e64758dba..add0b18ed 100644 --- a/Cslib/Foundations/Data/StackTape.lean +++ b/Cslib/Foundations/Data/StackTape.lean @@ -106,21 +106,21 @@ def head (l : StackTape Symbol) : Option Symbol := | [] => none | h :: _ => h -lemma head_eq_getD (s : StackTape Symbol) : - s.head = s.toList[0]?.getD none := by +@[scoped grind =] +lemma head_eq_getD (s : StackTape Symbol) : s.head = s.toList[0]?.getD none := by unfold head; cases s.toList <;> simp -@[simp] -lemma tail_getD (s : StackTape Symbol) (n : ℕ) : - s.tail.toList[n]?.getD none = s.toList[n + 1]?.getD none := by +@[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] +@[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] +@[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]) @@ -134,30 +134,23 @@ lemma eq_iff (l1 l2 : StackTape Symbol) : cases l2 with | mk as2 h2 => cases as1 <;> cases as2 <;> grind -lemma ext (t₁ t₂ : StackTape Symbol) (h_toList_eq : t₁.toList = t₂.toList) : - t₁ = t₂ := by +@[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.getD p none = t₂.toList.getD p none) : - t₁ = t₂ := by - apply ext + (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₂ - simp only [List.getD_eq_getElem?_getD] at h_get_eq - have hlen : l₁.length = l₂.length := by grind - apply List.ext_getElem hlen - grind + 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