feat(Foundations/Data): Function view for Turing tapes#499
Open
crei wants to merge 1 commit intoleanprover:mainfrom
Open
feat(Foundations/Data): Function view for Turing tapes#499crei wants to merge 1 commit intoleanprover:mainfrom
crei wants to merge 1 commit intoleanprover:mainfrom
Conversation
Contributor
|
Seems like a good addition! My only comment is: Should we add tags like @[ext] or |
chenson2018
requested changes
Apr 18, 2026
Collaborator
chenson2018
left a comment
chenson2018
left a comment
There was a problem hiding this comment.
This looks straightforward, thanks! Just some style questions.
Comment on lines
+81
to
+86
| /-- 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 |
Collaborator
There was a problem hiding this comment.
Usually the notation for these matches is used, right? I.e.
Suggested change
| /-- 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 | |
| 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 | |
| | 0 => t.head | |
| | (p' + 1 : Nat) => t.right.toList[p']?.getD none | |
| | -[p'+1] => t.left.toList[p']?.getD none |
| 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 |
Collaborator
There was a problem hiding this comment.
Should StackTape.ext_get and this theorem have ext attributes?
| have h_right : right₁ = right₂ := by | ||
| apply StackTape.ext_get | ||
| intro p | ||
| simpa [get] using h_get_eq p.succ |
Collaborator
There was a problem hiding this comment.
Again, is notation preferred?
Suggested change
| simpa [get] using h_get_eq p.succ | |
| simpa [get] using h_get_eq (p + 1) |
| apply StackTape.ext_get | ||
| intro p | ||
| simpa [get] using h_get_eq (Int.negSucc p) | ||
| simp only [h_head, h_left, h_right] |
Collaborator
There was a problem hiding this comment.
No need to squeeze terminal simp. Can also just be grind if you prefer.
| 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] |
Collaborator
There was a problem hiding this comment.
Suggested change
| 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] |
| unfold move_right get | ||
| match p with | ||
| | Int.ofNat n => | ||
| rw [show Int.ofNat n + 1 = Int.ofNat (n + 1) from by grind] |
Collaborator
There was a problem hiding this comment.
Suggested change
| 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 d with | ||
| | none => simp | ||
| | some d => | ||
| cases d <;> simp [move, show p + (-1 : ℤ) = p - 1 from by omega] |
Collaborator
There was a problem hiding this comment.
I'm not a fan of nested simp and grind. Here it seems particularly not needed because you can write
Suggested change
| cases d <;> simp [move, show p + (-1 : ℤ) = p - 1 from by omega] | |
| cases d | |
| · grind [move, get_move_left] | |
| · grind [move, get_move_right] |
maybe some of these should be simp/grind =?
| induction n generalizing t p with | ||
| | zero => simp | ||
| | succ n ih => | ||
| have : p - n - 1 = p - (n + 1) := by grind |
Collaborator
There was a problem hiding this comment.
Suggested change
| have : p - n - 1 = p - (n + 1) := by grind | |
| have : p - n - 1 = p - (n + 1) := by lia |
| funext p | ||
| match p with | ||
| | Int.ofNat 0 => simp | ||
| | Int.ofNat (n + 1) => simp; grind |
Collaborator
There was a problem hiding this comment.
simp; grind is technically allowed, but not needed here
Suggested change
| | Int.ofNat (n + 1) => simp; grind | |
| | Int.ofNat (n + 1) => grind |
chenson2018
changed the title
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
The central addition in this PR is
BiTape.get: it allows (integer) index-based access to the Turing tape cells.In addition, adds several lemmas that make it easier to work with
BiTapes by viewing them as functionsℤ → Option Symbol. A sequence of moves and writes translates into a sequence ofFunction.updateand thus maps everything into a domain thatsimpandgrindcan already nicely work with.