English
A precise implementation of the recursion principle for FinEnum, coordinating the insertions of Option.none with an inductive step.
Русский
В точной реализации рекурсии FinEnum координируются вставки Option.none и шаг индукции.
LaTeX
$$$\\text{FinEnum.recEmptyOption}(...) : P α$$$
Lean4
/-- 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 `Fin`s 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`
-/
def recEmptyOption {P : Type u → Sort v} (finChoice : (n : ℕ) → Fin (n + 1))
(congr : {α β : Type u} → (_ : FinEnum α) → (_ : FinEnum β) → card β = card α → P α → P β)
(empty : P PEmpty.{u + 1}) (option : {α : Type u} → FinEnum α → P α → P (Option α)) (α : Type u) [FinEnum α] :
P α :=
match cardeq : card α with
| 0 => congr _ _ cardeq empty
| n + 1 =>
let fN := ULift.instFinEnum (α := Fin n)
have : card (ULift.{u} <| Fin n) = n := card_ulift.trans card_fin
congr (insertNone _ <| finChoice n) _ (cardeq.trans <| congrArg Nat.succ this.symm) <|
option fN (recEmptyOption finChoice congr empty option _)
termination_by card α
