FinEnum instance for Option

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

TODO

• recreate rest of Mathlib.Data.Fintype.Option

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

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

Equations

• FinEnum.insertNone α i = FinEnum.mk (FinEnum.card α + 1) (FinEnum.equiv.optionCongr.trans (finSuccEquiv' i).symm)

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

• FinEnum.instFinEnumOptionLast α = FinEnum.insertNone α (Fin.last (FinEnum.card α))

@[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.

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.

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.

@[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

• aenum.recOnEmptyOption finChoice congr empty option = FinEnum.recEmptyOption finChoice (fun {α β : Type ?u.103} => congr) empty (fun {α : Type ?u.103} => option) α