Transparent definition and rw

Stream: general

[Patrick Johnson]

Which tags have to be added to T.len and T.push such that the example proof works without simp_rw [T.len]? In other words, how to introduce a definition that can be automatically unfolded by rw?

import tactic

structure T :=
(s : list ℕ)

@[reducible, inline]
def T.len (t : T) : ℕ := t.s.length

@[reducible, inline]
def T.push (t : T) (n : ℕ) : T := ⟨t.s ++ [n]⟩

lemma length_push {α : Type*} {xs : list α} {x : α} :
  (xs ++ [x]).length = xs.length + 1 :=
list.length_append _ _

example {t : T} : t.len < (t.push 0).len :=
begin
  -- simp_rw [T.len],
  rw length_push,
  apply lt_add_one,
end

[Kevin Buzzard]

Does abbreviation work?

[Patrick Johnson]

No. With abbreviations, we still have to change list.length _ < list.length _ before rw.

[Eric Wieser]

abbreviation doesn't generate equation lemmas