English
Let f : α → γ and g : β → γ be families of values on the left and right branches, respectively. Then recursing with an update on the left is the same as updating the recursion on the left branch: Sum.rec (update f a x) g = update (Sum.rec f g) (inl a) x.
Русский
Пусть f и g — семейства значений на левой и правой ветвях. Тогда рекурсивное определение, обновляющее слева, эквивалентно обновлению рекурсивной функции на левой ветви.
LaTeX
$$$$ \\operatorname{Sum.rec}(\\operatorname{update} f a x)\; g = \\operatorname{update}(\\operatorname{Sum.rec} f g)\; (\\mathrm{inl} a)\; x. $$$$
Lean4
@[simp]
theorem rec_update_left {γ : α ⊕ β → Sort*} [DecidableEq α] [DecidableEq β] (f : ∀ a, γ (.inl a)) (g : ∀ b, γ (.inr b))
(a : α) (x : γ (.inl a)) : Sum.rec (update f a x) g = update (Sum.rec f g) (.inl a) x :=
Function.rec_update Sum.inl_injective (Sum.rec · g) (fun _ _ => rfl)
(fun
| _, _, .inl _, h => (h _ rfl).elim
| _, _, .inr _, _ => rfl)
_ _ _
