Simplification rules in Turing.Tape

Stream: mathlib4

[chris477]

I have a question about the simplifications rules in Turing.Tape ( Mathlib/Computability/Tape.lean ). Specifically, the theorem Tape.write_mk' uses R.cons a on the lhs and it would fit in my case, but it turns out that the following theorem from the same file is applied first (because my R is a ListBlank.mk l):

@[simp]
theorem ListBlank.cons_mk {Γ} [Inhabited Γ] (a : Γ) (l : List Γ) :
    ListBlank.cons a (ListBlank.mk l) = ListBlank.mk (a :: l) :=
  rfl

This one rewrites the R.cons a into a different form such that Tape.write_mk' is no longer applicable and there is no similar simplification rule using the ListBlank.mk (a :: l) notation.

Of course I can fix my proof by using simp only etc but it's still a bit unsatisfying. Is there anything that can be done to the simplification rules in this file?

[Kenny Lau]

well you (and the maintainers) will have to choose simp normal forms such that everything has one simp path

[Kenny Lau]

or if there are two simp NFs, make sure that both paths reach the destination

[Kenny Lau]

it's library building and it's a hard decision and it's not always obvious the first time and there's trial and error involved

[Edward van de Meent]

a local solution would be using simp [-ListBlank.cons_mk] instead. A global solution would be to adapt Tape.write_mk' to instead apply to ListBlank.mk (a :: l) (or add that version as an additional simp lemma)

[Edward van de Meent]

i'm a bit surprised that this hasn't been caught earlier, i thought we had a linter checking that simp lemmas are in simp normal form?

[Edward van de Meent]

(which this one evidently isn't is, somewhat surprisingly)

[chris477]

I think one reason could be that ListBlank.cons_mk requires the ListBlank.mk l constructor while Tape.write_mk' works with arbitrary ListBlanks. I can try adding a version of Tape.write_mk' that uses ListBlank.mk (a :: l).

[Edward van de Meent]

ahhh of course, that makes more sense

[chris477]

I’ll create a pr!

[chris477]

-> https://github.com/leanprover-community/mathlib4/pull/30821