Proving sizeOf structure field is less than sizeOf structure

Stream: general

[Mai]

Silly question, but I just don't quite seem to get it.

structure A

structure S where
  a : A

example {s : S} : sizeOf s.a < sizeOf s := by
  sorry

[Violeta Hernández]

structure A

structure S where
  a : A

example {s : S} : sizeOf s.a < sizeOf s := by
  exact Nat.lt_succ_self _

[Violeta Hernández]

I believe sizeOf of a structure is generally defined as the sum of sizes of its fields, plus one

[Théophile]

You can also rely on the lemma S.mk.sizeOf_spec, e.g.

structure A

structure S where
  a : A

example {s : S} : sizeOf s.a < sizeOf s := by
  cases s
  simp only [S.mk.sizeOf_spec]
  -- goal: sizeOf a✝ < 1 + sizeOf a✝
  simp