Turing.Tape decidable equality

Stream: mathlib4

[Thomas Vigouroux]

Hey there, I came up with an alternative formulation for Turing.Tape S where we can easily have DecidableEq (Turing.Tape S) assuming DecidableEq S only.

Would there be interest for me to open a PR about that ?

[Eric Wieser]

(docs#Turing.Tape for comparison)

[Thomas Vigouroux]

The problem as of today is that the definition is based on an exists, but because the type is list-based, it is possible to have a simple inductive definition, together with a decidability proof

[Eric Wieser]

There's no need to change the definition here for decidable equality:

import Mathlib.Computability.TuringMachine

variable {Γ} [Inhabited Γ]

instance Turing.BlankExtends.instDecidableRel [DecidableEq Γ] : DecidableRel (@Turing.BlankExtends Γ _)
  | [], ys => decidable_of_iff (∀ y ∈ ys, y = default) sorry
  | x :: xs, [] => .isFalse sorry
  | x :: xs, y :: ys =>
    letI := instDecidableRel xs ys
    decidable_of_iff (x = y ∧ Turing.BlankExtends xs ys) sorry

instance Turing.BlankRel.instDecidableRel [DecidableEq Γ] : DecidableRel (@Turing.BlankRel Γ _) :=
  fun _ _ => inferInstanceAs <| Decidable (_ ∨ _)

instance [DecidableEq Γ] : DecidableEq (Turing.ListBlank Γ) :=
  @Quotient.decidableEq _ _ Turing.BlankRel.instDecidableRel

[Eric Wieser]

Your suggestion might still be a sensible idea, but the justification would need to be "it makes proofs about turing machines easier", or "it results in better runtime behavior when executing turing machines.

[Thomas Vigouroux]

I don't know about performances though
Maybe the fact that the original definition is an exists allows erasing it in most cases ?

[Thomas Vigouroux]

I think that simply having the decidability proofs is fine.

Here is my version of the proofs:

instance Turing.BlankExtends.instDecidableRel {Γ} [Inhabited Γ] [DecidableEq Γ] : DecidableRel (@Turing.BlankExtends Γ _)
  | [], ys => decidable_of_iff (∀ y ∈ ys, y = default) (by {
    simp [Turing.BlankExtends]
    constructor
    · intro hy
      exists ys.length
      exact List.eq_replicate_of_mem hy
    · intro ⟨n, hn⟩
      intro y hy
      apply List.eq_of_mem_replicate
      rw [hn] at hy
      exact hy
  })
  | x :: xs, [] => .isFalse (by simp [Turing.BlankExtends])
  | x :: xs, y :: ys =>
    letI := instDecidableRel xs ys
    decidable_of_iff (x = y ∧ Turing.BlankExtends xs ys) (by {
      simp [Turing.BlankExtends]
      intro n _
      constructor <;> {
        intro h
        exact h.symm
      }
    })

instance Turing.BlankRel.instDecidableRel {Γ} [Inhabited Γ] [DecidableEq Γ]: DecidableRel (@Turing.BlankRel Γ _) := by {
  simp [Turing.BlankRel, DecidableRel]
  intro a b
  apply instDecidableOr
}

instance Turing.ListBlank.instDecidableEq {Γ} [Inhabited Γ] [DecidableEq Γ]: DecidableEq (Turing.ListBlank Γ) := by {
  simp [Turing.ListBlank, Turing.BlankRel.setoid]
  refine @instDecidableEqQuotientOfDecidableEquiv _ _ ?_
  intro a b
  simp [instHasEquivOfSetoid, Setoid.r]
  apply inferInstance
}

instance Turing.Tape.instDecidableEq {Γ} [Inhabited Γ] [DecidableEq Γ]: DecidableEq (Turing.Tape Γ) := by {
  unfold DecidableEq
  intro ⟨ha, La, Ra⟩ ⟨hb, Lb, Rb⟩
  simp
  repeat apply instDecidableAnd
}

[Eric Wieser]

Strange that both docs#instDecidableEqQuotientOfDecidableEquiv and docs#Quotient.decidableEq exist!

[Thomas Vigouroux]

Indeed, both with the same definition :thinking:

[Kevin Buzzard]

No wonder there's not a diamond then :-)

[Kyle Miller]

What's the alternative definition @Thomas Vigouroux ? I don't think changing the definition for sake of DecidableEq makes sense, but it's worth evaluating it on its own terms.

[Thomas Vigouroux]

The idea is to directly use the algorithm to decide for BlankExtends. Kind of:

def BlankExtends' {Γ} [Inhabited Γ]: List Γ → List Γ → Prop
| [], [] => True
| _ :: _, [] => False
| [], he :: ta => he = default ∧ BlankExtends' [] ta
| he₁ :: ta₁, he₂ :: ta₂ => he₁ = he₂ ∧ BlankExtends' ta₁ ta₂

[Thomas Vigouroux]

Decidability can then be proven using BlankExtends' induction principle in a very straighforward way

[Kyle Miller]

In that case, there's no need to change the definition of BlankExtends itself. If you think that BlankExtends' is useful for proofs, you could prove that BlankExtends = BlankExtends' and then use it to try to simplify things (including using it to give the Decidable instance).

If you make make BlankExtends' be Bool-valued, then you could even make the Decidable instance using almost no argument at all (beyond proving BlankExtends xs ys <-> BlankExtends' xs ys = true) with docs#decidable_of_bool

[Kyle Miller]

A reason I'm suggesting this is that somewhere you'd want the current formulation of BlankExtends, since in that form it's obviously the right definition. BlankExtends' needs thought to see if it's encoding the correct relation.