Lean4
/-- Induction principle from the right for lists: if a property holds for the empty list, and
for `l ++ [a]` if it holds for `l`, then it holds for all lists. The principle is given for
a `Sort`-valued predicate, i.e., it can also be used to construct data. -/
@[elab_as_elim]
def reverseRecOn {motive : List α → Sort*} (l : List α) (nil : motive [])
(append_singleton : ∀ (l : List α) (a : α), motive l → motive (l ++ [a])) : motive l :=
match h : reverse l with
| [] => cast (congr_arg motive <| by simpa using congr(reverse $h.symm)) <| nil
| head :: tail =>
cast (congr_arg motive <| by simpa using congr(reverse $h.symm)) <|
append_singleton _ head <| reverseRecOn (reverse tail) nil append_singleton
termination_by l.length
decreasing_by
simp_wf
rw [← length_reverse (as := l), h, length_cons]
simp
