Documentation

Mathlib.Data.FinEnum.Option

FinEnum instance for Option #

Provides a recursor for FinEnum types like Fintype.truncRecEmptyOption, but capable of producing non-truncated data.

TODO #

source
def FinEnum.insertNone (α : Type u) [FinEnum α] (i : Fin (card α + 1)) :
FinEnum (Option α)

Inserting an Option.none anywhere in an enumeration yields another enumeration.

Equations
source
instance FinEnum.instFinEnumOptionLast (α : Type u) [FinEnum α] :
FinEnum (Option α)

This is an arbitrary choice of insertion rank for a default instance. It keeps the mapping of the existing α-inhabitants intact, modulo Fin.castSucc.

Equations
source
@[irreducible]
def FinEnum.recEmptyOption {P : Type u → Sort v} (finChoice : (n : ℕ) → Fin (n + 1)) (congr : {α β : Type u} → (x : FinEnum α) → (x_1 : FinEnum β) → card β = card α → P α → P β) (empty : P PEmpty.{u + 1}) (option : {α : Type u} → FinEnum α → P α → P (Option α)) (α : Type u) [FinEnum α] :
P α

A recursor principle for finite-and-enumerable types, analogous to Nat.rec. It effectively says that every FinEnum is either Empty or Option α, up to an Equiv mediated by Fins of equal cardinality. In contrast to the Fintype case, data can be transported along such an Equiv. Also, since order matters, the choice of element that gets replaced by Option.none has to be provided for every step.

Since every FinEnum instance implies a Fintype instance and Prop is squashed already, Fintype.induction_empty_option can be used if a Prop needs to be constructed. Cf. Data.Fintype.Option

Equations
  • One or more equations did not get rendered due to their size.
source
theorem FinEnum.recEmptyOption_of_card_eq_zero {P : Type u → Sort v} (finChoice : (n : ℕ) → Fin (n + 1)) (congr : {α β : Type u} → (x : FinEnum α) → (x_1 : FinEnum β) → card β = card α → P α → P β) (empty : P PEmpty.{u + 1}) (option : {α : Type u} → FinEnum α → P α → P (Option α)) (α : Type u) [FinEnum α] (h : card α = 0) (x✝ : FinEnum PEmpty.{u + 1}) :
recEmptyOption finChoice (fun {α β : Type u} => congr) empty (fun {α : Type u} => option) α = congr x✝ inst✝ ⋯ empty

For an empty type, the recursion principle evaluates to whatever congr makes of the base case.

source
theorem FinEnum.recEmptyOption_of_card_pos {P : Type u → Sort v} (finChoice : (n : ℕ) → Fin (n + 1)) (congr : {α β : Type u} → (x : FinEnum α) → (x_1 : FinEnum β) → card β = card α → P α → P β) (empty : P PEmpty.{u + 1}) (option : {α : Type u} → FinEnum α → P α → P (Option α)) (α : Type u) [FinEnum α] (h : 0 < card α) :
recEmptyOption finChoice (fun {α β : Type u} => congr) empty (fun {α : Type u} => option) α = congr (insertNone (ULift.{u, 0} (Fin (card α - 1))) ↑↑(finChoice (card α - 1))) inst✝ ⋯ (option ULift.instFinEnum (recEmptyOption finChoice (fun {α β : Type u} => congr) empty (fun {α : Type u} => option) (ULift.{u, 0} (Fin (card α - 1)))))

For a type with positive card, the recursion principle evaluates to whatever congr makes of the step result, where Option.none has been inserted into the (finChoice (card α - 1))th rank of the enumeration.

source
@[reducible, inline]
abbrev FinEnum.recOnEmptyOption {P : Type u → Sort v} {α : Type u} (aenum : FinEnum α) (finChoice : (n : ℕ) → Fin (n + 1)) (congr : {α β : Type u} → (x : FinEnum α) → (x_1 : FinEnum β) → card β = card α → P α → P β) (empty : P PEmpty.{u + 1}) (option : {α : Type u} → FinEnum α → P α → P (Option α)) :
P α

A recursor principle for finite-and-enumerable types, analogous to Nat.recOn. It effectively says that every FinEnum is either Empty or Option α, up to an Equiv mediated by Fins of equal cardinality. In contrast to the Fintype case, data can be transported along such an Equiv. Also, since order matters, the choice of element that gets replaced by Option.none has to be provided for every step.

Equations