SizeOf

class SizeOf (α : Sort u) : Sort (max 1 u)

SizeOf is a typeclass automatically derived for every inductive type, which equips the type with a "size" function to Nat. The default instance defines each constructor to be 1 plus the sum of the sizes of all the constructor fields.

This is used for proofs by well-founded induction, since every field of the constructor has a smaller size than the constructor itself, and in many cases this will suffice to do the proof that a recursive function is only called on smaller values. If the default proof strategy fails, it is recommended to supply a custom size measure using the termination_by argument on the function definition.

• sizeOf : α → Nat

  The "size" of an element, a natural number which decreases on fields of each inductive type.

Declare SizeOf instances and theorems for types declared before SizeOf. From now on, the inductive compiler will automatically generate SizeOf instances and theorems.

def default.sizeOf (α : Sort u) : α → Nat

Every type α has a default SizeOf instance that just returns 0 for every element of α.

Equations

• default.sizeOf α x✝ = 0

@[instance 100]

instance instSizeOfDefault (α : Sort u) : SizeOf α

Every type α has a low priority default SizeOf instance that just returns 0 for every element of α.

Equations

• instSizeOfDefault α = { sizeOf := default.sizeOf α }

@[simp]

theorem sizeOf_default {α : Sort u_1} (n : α) : sizeOf n = 0

instance instSizeOfNat : SizeOf Nat

Equations

• instSizeOfNat = { sizeOf := fun (n : Nat) => n }

@[simp]

theorem sizeOf_nat (n : Nat) : sizeOf n = n

instance instSizeOfForallUnit {α : Sort u_1} [SizeOf α] : SizeOf (Unit → α)

Equations

• instSizeOfForallUnit = { sizeOf := fun (f : Unit → α) => sizeOf (f ()) }

@[simp]

theorem sizeOf_thunk {α : Sort u_1} [SizeOf α] (f : Unit → α) : sizeOf f = sizeOf (f ())

@[simp]

theorem Unit.sizeOf (u : Unit) : SizeOf.sizeOf u = 1

@[simp]

theorem Bool.sizeOf_eq_one (b : Bool) : sizeOf b = 1

noncomputable def Lean.Name.sizeOf : Name → Nat

We manually define the Lean.Name instance because we use an opaque function for computing the hashcode field.

Equations

• Lean.Name.anonymous.sizeOf = 1
• (p.str s).sizeOf = 1 + p.sizeOf + sizeOf s
• (p.num n).sizeOf = 1 + p.sizeOf + sizeOf n

noncomputable instance Lean.instSizeOfName : SizeOf Name

Equations

• Lean.instSizeOfName = { sizeOf := fun (n : Lean.Name) => n.sizeOf }

@[simp]

theorem Lean.Name.anonymous.sizeOf_spec : sizeOf anonymous = 1

@[simp]

theorem Lean.Name.str.sizeOf_spec (p : Name) (s : String) : sizeOf (p.str s) = 1 + sizeOf p + sizeOf s

@[simp]

theorem Lean.Name.num.sizeOf_spec (p : Name) (n : Nat) : sizeOf (p.num n) = 1 + sizeOf p + sizeOf n