Induction principles for lists #
@[irreducible]
def
List.reverseRecOn
{α : Type u_1}
{motive : List α → Sort u_2}
(l : List α)
(nil : motive [])
(append_singleton : (l : List α) → (a : α) → motive l → motive (l ++ [a]))
:
motive l
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.
Equations
Instances For
@[simp]
theorem
List.reverseRecOn_concat
{α : Type u_1}
{motive : List α → Sort u_2}
(x : α)
(xs : List α)
(nil : motive [])
(append_singleton : (l : List α) → (a : α) → motive l → motive (l ++ [a]))
:
reverseRecOn (xs ++ [x]) nil append_singleton = append_singleton xs x (reverseRecOn xs nil append_singleton)
@[irreducible]
def
List.bidirectionalRec
{α : Type u_1}
{motive : List α → Sort u_2}
(nil : motive [])
(singleton : (a : α) → motive [a])
(cons_append : (a : α) → (l : List α) → (b : α) → motive l → motive (a :: (l ++ [b])))
(l : List α)
:
motive l
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.
Equations
Instances For
@[simp]
@[simp]
theorem
List.bidirectionalRec_cons_append
{α : Type u_1}
{motive : List α → Sort u_2}
(nil : motive [])
(singleton : (a : α) → motive [a])
(cons_append : (a : α) → (l : List α) → (b : α) → motive l → motive (a :: (l ++ [b])))
(a : α)
(l : List α)
(b : α)
:
bidirectionalRec nil singleton cons_append (a :: (l ++ [b])) = cons_append a l b (bidirectionalRec nil singleton cons_append l)