English
The bidirectionalRec function returns the base nil value on the empty list.
Русский
Функция bidirectionalRec возвращает базовое nil на пустом списке.
LaTeX
$$$$ \operatorname{bidirectionalRec} (\text{nil}) \; [] = nil. $$$$
Lean4
/-- Bidirectional induction principle for lists: if a property holds for the empty list, the
singleton list, and `a :: (l ++ [b])` from `l`, then it holds for all lists. This can be used to
prove statements about palindromes. The principle is given for a `Sort`-valued predicate, i.e., it
can also be used to construct data. -/
@[elab_as_elim]
def bidirectionalRec {motive : List α → Sort*} (nil : motive []) (singleton : ∀ a : α, motive [a])
(cons_append : ∀ (a : α) (l : List α) (b : α), motive l → motive (a :: (l ++ [b]))) : ∀ l, motive l
| [] => nil
| [a] => singleton a
| a :: b :: l =>
let l' := dropLast (b :: l)
let b' := getLast (b :: l) (cons_ne_nil _ _)
cast (by rw [← dropLast_append_getLast (cons_ne_nil b l)]) <|
cons_append a l' b' (bidirectionalRec nil singleton cons_append l')
termination_by l => l.length
