English
A general version of pushing recursors inside updates for arbitrary constructors and recursors.
Русский
Обобщённая версия переноса рекурсоров внутрь обновлений для произвольных конструкторов и рекурсоров.
LaTeX
$$$\\text{rec_update}: \\ \\, \\text{(обобщение)}$$$
Lean4
/-- Recursors can be pushed inside `Function.update`.
The `ctor` argument should be a one-argument constructor like `Sum.inl`,
and `recursor` should be an inductive recursor partially applied in all but that constructor,
such as `(Sum.rec · g)`.
In future, we should build some automation to generate applications like `Option.rec_update` for all
inductive types. -/
theorem rec_update {ι κ : Sort*} {α : κ → Sort*} [DecidableEq ι] [DecidableEq κ] {ctor : ι → κ}
(hctor : Function.Injective ctor) (recursor : ((i : ι) → α (ctor i)) → ((i : κ) → α i))
(h : ∀ f i, recursor f (ctor i) = f i) (h2 : ∀ f₁ f₂ k, (∀ i, ctor i ≠ k) → recursor f₁ k = recursor f₂ k)
(f : (i : ι) → α (ctor i)) (i : ι) (x : α (ctor i)) : recursor (update f i x) = update (recursor f) (ctor i) x :=
by
ext k
by_cases h : ∃ i, ctor i = k
· obtain ⟨i', rfl⟩ := h
obtain rfl | hi := eq_or_ne i' i
· simp [h]
· have hk := hctor.ne hi
simp [h, hi, hk, Function.update_of_ne]
· rw [not_exists] at h
rw [h2 _ f _ h]
rw [Function.update_of_ne (Ne.symm <| h i)]
