### 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

- 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

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

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

Instances For

source
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) ⋯)

Instances For

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

Instances For

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

Instances For

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