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.

Equations

• List.reverseRec nil append_singleton [] = nil
• List.reverseRec nil append_singleton (a :: l) = ⋯ ▸ append_singleton (a :: l).dropLast ((a :: l).getLast ⋯) (List.reverseRec nil append_singleton (a :: l).dropLast)

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

Equations

• List.reverseRecOn l nil append_singleton = List.reverseRec nil append_singleton l

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.

Equations

• One or more equations did not get rendered due to their size.
• List.bidirectionalRec nil singleton cons_append [] = nil
• List.bidirectionalRec nil singleton cons_append [a] = singleton a

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

Equations

• l.bidirectionalRecOn H0 H1 Hn = List.bidirectionalRec H0 H1 Hn l

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.

Equations

• List.recNeNil singleton cons [x] h_2 = singleton x
• List.recNeNil singleton cons (x :: y :: xs) h_2 = cons x (y :: xs) ⋯ (List.recNeNil singleton cons (y :: xs) ⋯)

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

Equations

• List.recOnNeNil l h singleton cons = List.recNeNil singleton cons l h

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

Equations

• One or more equations did not get rendered due to their size.
• List.twoStepInduction nil singleton cons_cons [] = nil
• List.twoStepInduction nil singleton cons_cons [a] = singleton a

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