feat(Foundations/Data): Function view for Turing tapes#499
feat(Foundations/Data): Function view for Turing tapes#499crei wants to merge 3 commits intoleanprover:mainfrom
Conversation
|
Seems like a good addition! My only comment is: Should we add tags like @[ext] or |
chenson2018
left a comment
chenson2018
left a comment
There was a problem hiding this comment.
This looks straightforward, thanks! Just some style questions.
| 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 |
There was a problem hiding this comment.
Should StackTape.ext_get and this theorem have ext attributes?
There was a problem hiding this comment.
After adding the attributes to StackTape.ext and StackTape.ext_get, I can use ext1 p here, but how can I be sure that the ext tactic uses StackTape.ext_get instead of StackTape.ext?
| apply StackTape.ext_get | ||
| intro p | ||
| simpa [get] using h_get_eq (Int.negSucc p) | ||
| simp only [h_head, h_left, h_right] |
There was a problem hiding this comment.
No need to squeeze terminal simp. Can also just be grind if you prefer.
| cases d with | ||
| | none => simp | ||
| | some d => | ||
| cases d <;> simp [move, show p + (-1 : ℤ) = p - 1 from by omega] |
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
| 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 =?
There was a problem hiding this comment.
It seems that grind [move] solves the whole thing just after the unfold commands - maybe also because I added some more annotations.
chenson2018
changed the title
Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>
3 participants
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.