LeanPool.FormalizationOfBoundedArithmetic.IsEnum

class IsEnum (α : Type u) : Type u

A finite type equipped with explicit encodings to and from a finite index type.

• size : ℕ

  The number of elements in the enumeration.

• toIdx : α → Fin (size α)

  Encode an element as an index.

• fromIdx : Fin (size α) → α

  Decode an index as an element.

• to_from_id (i : Fin (size α)) : toIdx (fromIdx i) = i

  Decoding and then encoding gives back the same index.

• from_to_id (x : α) : fromIdx (toIdx x) = x

  Encoding and then decoding gives back the same element.

def deriveIsEnum (declNames : Array Lean.Name) : Lean.Elab.Command.CommandElabM Bool

Deriving handler for IsEnum on finite inductive types.

Equations

• One or more equations did not get rendered due to their size.

theorem IsEnum.left_inv {α : Type u_1} {enum : IsEnum α} : Function.LeftInverse fromIdx toIdx

The index decoder is a left inverse of the encoder.

theorem IsEnum.right_inv {α : Type u_1} {enum : IsEnum α} : Function.RightInverse fromIdx toIdx

The index decoder is a right inverse of the encoder.

def IsEnum.equiv {α : Type u_1} {enum : IsEnum α} : α ≃ Fin (size α)

The equivalence between an enumerated type and its finite index type.

Equations

• IsEnum.equiv = { toFun := IsEnum.toIdx, invFun := IsEnum.fromIdx, left_inv := ⋯, right_inv := ⋯ }

theorem IsEnum.finite {α : Type u_1} (enum : IsEnum α) : Finite α

An enumerated type is finite.

theorem IsEnum.fromIdx_injective {α : Type u_1} {enum : IsEnum α} : Function.Injective fromIdx

The decoder from indices is injective.

theorem IsEnum.toIdx_injective {α : Type u_1} {enum : IsEnum α} : Function.Injective toIdx

The encoder to indices is injective.

def IsEnum.toList {α : Type u_1} {enum : IsEnum α} : List α

List all elements of an enumerated type in index order.

Equations

• IsEnum.toList = List.ofFn IsEnum.fromIdx

theorem IsEnum.nodup_toList {α : Type u_1} {enum : IsEnum α} : toList.Nodup