modifyLast_concat — Mathlib

English

For any function f, element a, and list l, modifying the last element after appending a to l equals appending the last element of the transformed list: modifyLast f (l ++ [a]) = l ++ [f a].

Русский

Для любой функции f, элемента a и списка l, преобразование последнего элемента после добавления a к l эквивалентно добавлению в конец списка преобразованного элемента: modifyLast f (l ++ [a]) = l ++ [f a].

LaTeX

$$$\\forall {\\alpha} {\\beta} {\\List}(\\alpha) {\\to} {\\List}(\\alpha), \\forall f : \\alpha \\to \\alpha, \\forall a \\in \\alpha, \\forall l : \\List(\\alpha),\\left(\\mathrm{modifyLast} f (l ++ [a]) = l ++ [f a]\\right)$$$

Lean4

theorem modifyLast_concat (f : α → α) (a : α) (l : List α) : modifyLast f (l ++ [a]) = l ++ [f a] := by
  cases l with
  | nil => simp only [nil_append, modifyLast, modifyLast.go, Array.toListAppend_eq]
  | cons _ tl =>
    simp only [cons_append, modifyLast]
    rw [modifyLast.go]
    case x_3 => exact append_ne_nil_of_right_ne_nil tl (cons_ne_nil a [])
    rw [modifyLast.go_concat, Array.toListAppend_eq, Array.toList_push, List.toList_toArray, nil_append, cons_append,
      nil_append, cons_inj_right]
    exact modifyLast_concat _ _ tl

Похожие утверждения