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

[crei]

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 of Function.update and thus maps everything into a domain that simp and grind can already nicely work with.

[BoltonBailey]

Seems like a good addition! My only comment is: Should we add tags like @[ext] or grind = to some of these to improve integration with tactics?

[chenson2018]

This looks straightforward, thanks! Just some style questions.

[chenson2018]

Should StackTape.ext_get and this theorem have ext attributes?

[crei]

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?

[chenson2018]

You're right, even if you remove both it picks up another usage of ext, so maybe this isn't helpful?

[chenson2018]

A couple more style comments.

[chenson2018]

It seems clearer to use congr here directly rather than have grind infer this:

Suggested change

	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
	cases t₁
	congr
	· simpa [get] using h_get_eq 0
	· apply StackTape.ext_get
	intro p
	simpa [get] using h_get_eq (Int.negSucc p)
	· apply StackTape.ext_get
	intro p
	simpa [get] using h_get_eq (p + 1)

[chenson2018]

For these where you have something like rw [show ... from rfl[, you can also just do

Suggested change

	rw [show Int.ofNat 0 - 1 = Int.negSucc 0 from rfl]
	simp [StackTape.head_eq_getD]
	simp [StackTape.head_eq_getD]
	rfl

[chenson2018]

Fir on one line, and some parentheses can be removed:

Suggested change

	lemma get_move_left (t : BiTape Symbol) (p : ℤ) :
	(t.move_left).get p = t.get (p - 1) := by
	lemma get_move_left (t : BiTape Symbol) (p : ℤ) : t.move_left.get p = t.get (p - 1) := by

[chenson2018]

Suggested change

	lemma get_move_right (t : BiTape Symbol) (p : ℤ) :
	(t.move_right).get p = t.get (p + 1) := by
	lemma get_move_right (t : BiTape Symbol) (p : ℤ) : t.move_right.get p = t.get (p + 1) := by

[chenson2018]

Is this the preferred way to do these proofs in Mathlib? I rarely work with integers, but this seems very low-level.