Induction principles for lists

@[irreducible]

def List.reverseRec {α : Type u_1} {motive : List α → Sort u_2} (nil : motive []) (append_singleton : (l : List α) → (a : α) → motive l → motive (l ++ [a])) (l : List α) : 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.

@[simp]

theorem List.reverseRec_nil {α : Type u_1} {motive : List α → Sort u_2} (nil : motive []) (append_singleton : (l : List α) → (a : α) → motive l → motive (l ++ [a])) : reverseRec nil append_singleton [] = nil

@[simp]

theorem List.reverseRec_concat {α : Type u_1} {motive : List α → Sort u_2} (x : α) (xs : List α) (nil : motive []) (append_singleton : (l : List α) → (a : α) → motive l → motive (l ++ [a])) : reverseRec nil append_singleton (xs ++ [x]) = append_singleton xs x (reverseRec nil append_singleton xs)

@[reducible, inline]

abbrev 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

Like reverseRec, but with the list parameter placed first.

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

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.

@[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

@[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

@[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)

@[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.

def List.recNeNil {α : Type u_1} {motive : (l : List α) → l ≠ [] → Sort u_2} (singleton : (x : α) → motive [x] ⋯) (cons : (x : α) → (xs : List α) → (h : xs ≠ []) → motive xs h → motive (x :: xs) ⋯) (l : List α) (h : l ≠ []) : motive l h

A dependent recursion principle for nonempty lists. Useful for dealing with operations like List.head which are not defined on the empty list.

@[simp]

theorem List.recNeNil_singleton {α : Type u_1} {motive : (l : List α) → l ≠ [] → Sort u_2} (x : α) (singleton : (x : α) → motive [x] ⋯) (cons : (x : α) → (xs : List α) → (h : xs ≠ []) → motive xs h → motive (x :: xs) ⋯) : recNeNil singleton cons [x] ⋯ = singleton x

@[simp]

theorem List.recNeNil_cons {α : Type u_1} {motive : (l : List α) → l ≠ [] → Sort u_2} (x : α) (xs : List α) (h : xs ≠ []) (singleton : (x : α) → motive [x] ⋯) (cons : (x : α) → (xs : List α) → (h : xs ≠ []) → motive xs h → motive (x :: xs) ⋯) : recNeNil singleton cons (x :: xs) ⋯ = cons x xs h (recNeNil singleton cons xs h)

@[reducible, inline]

abbrev List.recOnNeNil {α : Type u_1} {motive : (l : List α) → l ≠ [] → Sort u_2} (l : List α) (h : l ≠ []) (singleton : (x : α) → motive [x] ⋯) (cons : (x : α) → (xs : List α) → (h : xs ≠ []) → motive xs h → motive (x :: xs) ⋯) : motive l h

A dependent recursion principle for nonempty lists. Useful for dealing with operations like List.head which are not defined on the empty list. Same as List.recNeNil, with a more convenient argument order.

@[irreducible]

def List.twoStepInduction {α : Type u_1} {motive : List α → Sort u_2} (nil : motive []) (singleton : (x : α) → motive [x]) (cons_cons : (x y : α) → (xs : List α) → motive xs → ((y : α) → motive (y :: xs)) → motive (x :: y :: xs)) (l : List α) : motive l

A recursion principle for lists which separates the singleton case.

@[simp]

theorem List.twoStepInduction_nil {α : Type u_1} {motive : List α → Sort u_2} (nil : motive []) (singleton : (x : α) → motive [x]) (cons_cons : (x y : α) → (xs : List α) → motive xs → ((y : α) → motive (y :: xs)) → motive (x :: y :: xs)) : twoStepInduction nil singleton cons_cons [] = nil

@[simp]

theorem List.twoStepInduction_singleton {α : Type u_1} {motive : List α → Sort u_2} (x : α) (nil : motive []) (singleton : (x : α) → motive [x]) (cons_cons : (x y : α) → (xs : List α) → motive xs → ((y : α) → motive (y :: xs)) → motive (x :: y :: xs)) : twoStepInduction nil singleton cons_cons [x] = singleton x

@[simp]

theorem List.twoStepInduction_cons_cons {α : Type u_1} {motive : List α → Sort u_2} (x y : α) (xs : List α) (nil : motive []) (singleton : (x : α) → motive [x]) (cons_cons : (x y : α) → (xs : List α) → motive xs → ((y : α) → motive (y :: xs)) → motive (x :: y :: xs)) : twoStepInduction nil singleton cons_cons (x :: y :: xs) = cons_cons x y xs (twoStepInduction nil singleton cons_cons xs) fun (y : α) => twoStepInduction nil singleton cons_cons (y :: xs)