Init.SizeOf

SizeOf structure

(α : Sort u)

Full source

/--
`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.
-/
class SizeOf (α : Sort u) where
  /-- The "size" of an element, a natural number which decreases on fields of
  each inductive type. -/
  sizeOf : α → Nat

Size function for well-founded induction

Informal description

The `SizeOf` typeclass provides a size function that maps elements of a type `α` to natural numbers. This is automatically derived for inductive types, where the size of a constructor is defined as 1 plus the sum of the sizes of its fields. This is primarily used for well-founded induction proofs, ensuring recursive function calls operate on smaller values.

default.sizeOf definition

(α : Sort u) : α → Nat

Full source

/--
Every type `α` has a default `SizeOf` instance that just returns `0`
for every element of `α`.
-/
protected def default.sizeOf (α : Sort u) : α → Nat
  | _ => 0

Default size function

Informal description

The default size function for any type $\alpha$ maps every element of $\alpha$ to $0$.

instSizeOfDefault instance

(α : Sort u) : SizeOf α

Full source

/--
Every type `α` has a low priority default `SizeOf` instance that just returns `0`
for every element of `α`.
-/
instance (priority := low) instSizeOfDefault (α : Sort u) : SizeOf α where
  sizeOf := default.sizeOf α

Default Size Function for Any Type

Informal description

For any type $\alpha$, there is a default size function that assigns $0$ to every element of $\alpha$.

sizeOf_default theorem

(n : α) : sizeOf n = 0

Full source

@[simp] theorem sizeOf_default (n : α) : sizeOf n = 0 := rfl

Default Size Function Yields Zero

Informal description

For any element $n$ of type $\alpha$, the default size function evaluates to $0$, i.e., $\mathrm{sizeOf}(n) = 0$.

instSizeOfNat instance

: SizeOf Nat

Full source

instance : SizeOf Nat where
  sizeOf n := n

Size Function for Natural Numbers

Informal description

The natural numbers $\mathbb{N}$ have a size function where the size of each natural number $n$ is $n$ itself.

sizeOf_nat theorem

(n : Nat) : sizeOf n = n

Full source

@[simp] theorem sizeOf_nat (n : Nat) : sizeOf n = n := rfl

Size of Natural Number Equals Itself

Informal description

For any natural number $n$, the size of $n$ is equal to $n$ itself, i.e., $\mathrm{sizeOf}(n) = n$.

instSizeOfForallUnit instance

[SizeOf α] : SizeOf (Unit → α)

Full source

instance [SizeOf α] : SizeOf (Unit → α) where
  sizeOf f := sizeOf (f ())

Size Function for Functions from Unit

Informal description

For any type $\alpha$ equipped with a size function, the function type $\text{Unit} \to \alpha$ also has a size function.

sizeOf_thunk theorem

[SizeOf α] (f : Unit → α) : sizeOf f = sizeOf (f ())

Full source

@[simp] theorem sizeOf_thunk [SizeOf α] (f : Unit → α) : sizeOf f = sizeOf (f ()) :=
  rfl

Size of Thunk Equals Size of its Evaluation

Informal description

For any type $\alpha$ with a size function and any function $f : \text{Unit} \to \alpha$, the size of $f$ is equal to the size of $f$ applied to the unit value, i.e., $\text{sizeOf}(f) = \text{sizeOf}(f ())$.

Unit.sizeOf theorem

(u : Unit) : sizeOf u = 1

Full source

@[simp] theorem Unit.sizeOf (u : Unit) : sizeOf u = 1 := rfl

Size of Unit Element is One

Informal description

For any element $u$ of the unit type, the size of $u$ is equal to 1, i.e., $\text{sizeOf}(u) = 1$.

Bool.sizeOf_eq_one theorem

(b : Bool) : sizeOf b = 1

Full source

@[simp] theorem Bool.sizeOf_eq_one (b : Bool) : sizeOf b = 1 := by cases b <;> rfl

Size of Boolean Values is One

Informal description

For any boolean value $b$, the size of $b$ is equal to 1, i.e., $\text{sizeOf}(b) = 1$.

Lean.Name.sizeOf definition

: Name → Nat

Full source

/--
We manually define the `Lean.Name` instance because we use
an opaque function for computing the hashcode field.
-/
protected noncomputable def Name.sizeOf : Name → Nat
  | anonymous => 1
  | str p s   => 1 + Name.sizeOf p + sizeOf s
  | num p n   => 1 + Name.sizeOf p + sizeOf n

Size function for Lean names

Informal description

The function assigns a size to each name in the `Lean.Name` type as follows: - The size of the anonymous name is 1. - The size of a string name `str p s` is 1 plus the size of the parent name `p` plus the size of the string `s`. - The size of a numeric name `num p n` is 1 plus the size of the parent name `p` plus the size of the number `n`.

Lean.instSizeOfName instance

: SizeOf Name

Full source

noncomputable instance : SizeOf Name where
  sizeOf n := n.sizeOf

Size Function for Lean Names

Informal description

The type `Lean.Name` has a size function that assigns a natural number to each name, where: - The anonymous name has size 1 - A string name `str p s` has size 1 plus the size of parent name `p` plus the size of string `s` - A numeric name `num p n` has size 1 plus the size of parent name `p` plus the size of number `n`

Lean.Name.anonymous.sizeOf_spec theorem

: sizeOf anonymous = 1

Full source

@[simp] theorem Name.anonymous.sizeOf_spec : sizeOf anonymous = 1 :=
  rfl

Size of Anonymous Name is One

Informal description

The size of the anonymous name in Lean's `Name` type is equal to 1, i.e., $\text{sizeOf}(\text{anonymous}) = 1$.

Lean.Name.str.sizeOf_spec theorem

(p : Name) (s : String) : sizeOf (str p s) = 1 + sizeOf p + sizeOf s

Full source

@[simp] theorem Name.str.sizeOf_spec (p : Name) (s : String) : sizeOf (str p s) = 1 + sizeOf p + sizeOf s :=
  rfl

Size of String Name in Lean: $\mathrm{sizeOf}(\mathrm{str}(p, s)) = 1 + \mathrm{sizeOf}(p) + \mathrm{sizeOf}(s)$

Informal description

For any Lean name $p$ and string $s$, the size of the string name $\mathrm{str}(p, s)$ is equal to $1$ plus the size of $p$ plus the size of $s$, i.e., $\mathrm{sizeOf}(\mathrm{str}(p, s)) = 1 + \mathrm{sizeOf}(p) + \mathrm{sizeOf}(s)$.

Lean.Name.num.sizeOf_spec theorem

(p : Name) (n : Nat) : sizeOf (num p n) = 1 + sizeOf p + sizeOf n

Full source

@[simp] theorem Name.num.sizeOf_spec (p : Name) (n : Nat) : sizeOf (num p n) = 1 + sizeOf p + sizeOf n :=
  rfl

Size of Numeric Lean Name Formula

Informal description

For any Lean name `p` and natural number `n`, the size of the numeric name `num p n` is equal to $1$ plus the size of `p` plus the size of `n$, i.e., $\text{sizeOf}(\text{num}\ p\ n) = 1 + \text{sizeOf}(p) + \text{sizeOf}(n)$.