Documentation

Mathlib.Data.List.Induction

Induction principles for lists #

source
@[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
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem List.reverseRecOn_nil {α : Type u_1} {motive : List α → Sort u_2} (nil : motive []) (append_singleton : (l : List α) → (a : α) → motive l → motive (l ++ [a])) :
    reverseRecOn [] nil append_singleton = nil
    source
    @[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)
    source
    @[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
      source
      @[simp]
      theorem List.bidirectionalRec_nil {α : 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]))) :
      bidirectionalRec nil singleton cons_append [] = nil
      source
      @[simp]
      theorem List.bidirectionalRec_singleton {α : 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 : α) :
      bidirectionalRec nil singleton cons_append [a] = singleton a
      source
      @[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)
      source
      @[reducible, inline]
      abbrev List.bidirectionalRecOn {α : Type u_1} {C : List α → Sort u_2} (l : List α) (H0 : C []) (H1 : (a : α) → C [a]) (Hn : (a : α) → (l : List α) → (b : α) → C l → C (a :: (l ++ [b]))) :
      C l

      Like bidirectionalRec, but with the list parameter placed first.

      Equations
      Instances For