Mathlib.Data.List.Induction

List.reverseRecOn definition

 {motive : List α → Sort*} (l : List α) (nil : motive [])
  (append_singleton : ∀ (l : List α) (a : α), motive l → motive (l ++ [a])) : motive l

Full source

/-- 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. -/
@[elab_as_elim]
def reverseRecOn {motive : List α → Sort*} (l : List α) (nil : motive [])
    (append_singleton : ∀ (l : List α) (a : α), motive l → motive (l ++ [a])) : motive l :=
  match h : reverse l with
  | [] => cast (congr_arg motive <| by simpa using congr(reverse $h.symm)) <|
      nil
  | head :: tail =>
    cast (congr_arg motive <| by simpa using congr(reverse $h.symm)) <|
      append_singleton _ head <| reverseRecOn (reverse tail) nil append_singleton
termination_by l.length
decreasing_by
  simp_wf
  rw [← length_reverse (as := l), h, length_cons]
  simp [Nat.lt_succ]

Right induction principle for lists

Informal description

Given a property `motive` defined on lists of type `α` and valued in an arbitrary type universe, to prove that `motive` holds for all lists `l`, it suffices to show: 1. Base case: `motive` holds for the empty list `[]`. 2. Inductive step: For any list `l` and element `a`, if `motive` holds for `l`, then it also holds for `l ++ [a]`. This is a right induction principle for lists, allowing both proofs and constructions of data.

List.reverseRecOn_nil theorem

 {motive : List α → Sort*} (nil : motive []) (append_singleton : ∀ (l : List α) (a : α), motive l → motive (l ++ [a])) :
  reverseRecOn [] nil append_singleton = nil

Full source

@[simp]
theorem reverseRecOn_nil {motive : List α → Sort*} (nil : motive [])
    (append_singleton : ∀ (l : List α) (a : α), motive l → motive (l ++ [a])) :
    reverseRecOn [] nil append_singleton = nil := reverseRecOn.eq_1 ..

Base Case of Right Induction for Lists: `reverseRecOn [] = nil`

Informal description

For any property `motive` defined on lists of type $\alpha$ and valued in an arbitrary type universe, when applying the right induction principle `reverseRecOn` to the empty list `[]` with base case proof `nil` and inductive step proof `append_singleton`, the result is equal to the base case proof `nil`. In other words, the induction principle correctly handles the base case.

List.reverseRecOn_concat theorem

 {motive : List α → Sort*} (x : α) (xs : List α) (nil : motive [])
  (append_singleton : ∀ (l : List α) (a : α), motive l → motive (l ++ [a])) :
  reverseRecOn (motive := motive) (xs ++ [x]) nil append_singleton =
    append_singleton _ _ (reverseRecOn (motive := motive) xs nil append_singleton)

Full source

@[simp, nolint unusedHavesSuffices]
theorem reverseRecOn_concat {motive : List α → Sort*} (x : α) (xs : List α) (nil : motive [])
    (append_singleton : ∀ (l : List α) (a : α), motive l → motive (l ++ [a])) :
    reverseRecOn (motive := motive) (xs ++ [x]) nil append_singleton =
      append_singleton _ _ (reverseRecOn (motive := motive) xs nil append_singleton) := by
  suffices ∀ ys (h : reverse (reverse xs) = ys),
      reverseRecOn (motive := motive) (xs ++ [x]) nil append_singleton =
        cast (by simp [(reverse_reverse _).symm.trans h])
          (append_singleton _ x (reverseRecOn (motive := motive) ys nil append_singleton)) by
    exact this _ (reverse_reverse xs)
  intros ys hy
  conv_lhs => unfold reverseRecOn
  split
  next h => simp at h
  next heq =>
    revert heq
    simp only [reverse_append, reverse_cons, reverse_nil, nil_append, singleton_append, cons.injEq]
    rintro ⟨rfl, rfl⟩
    subst ys
    rfl

Recursion Formula for Reverse Induction on Lists

Informal description

For any property `motive` on lists of type $\alpha$, given an element $x$ and a list $xs$, the reverse recursion principle `reverseRecOn` satisfies: \[ \text{reverseRecOn}(xs \mathbin{+\!\!+} [x]) = \text{append\_singleton} \, xs \, x \, (\text{reverseRecOn} \, xs) \] where: - `reverseRecOn` is applied to the concatenation of $xs$ and $[x]$, - `append_singleton` is the inductive step function, - The base case `nil` is the proof for the empty list.

List.bidirectionalRec definition

 {motive : List α → Sort*} (nil : motive []) (singleton : ∀ a : α, motive [a])
  (cons_append : ∀ (a : α) (l : List α) (b : α), motive l → motive (a :: (l ++ [b]))) : ∀ l, motive l

Full source

/-- 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. -/
@[elab_as_elim]
def bidirectionalRec {motive : List α → Sort*} (nil : motive []) (singleton : ∀ a : α, motive [a])
    (cons_append : ∀ (a : α) (l : List α) (b : α), motive l → motive (a :: (l ++ [b]))) :
    ∀ l, motive l
  | [] => nil
  | [a] => singleton a
  | a :: b :: l =>
    let l' := dropLast (b :: l)
    let b' := getLast (b :: l) (cons_ne_nil _ _)
    cast (by rw [← dropLast_append_getLast (cons_ne_nil b l)]) <|
      cons_append a l' b' (bidirectionalRec nil singleton cons_append l')
termination_by l => l.length

Bidirectional induction for lists

Informal description

The bidirectional induction principle for lists states that if a property holds for the empty list, for any singleton list, and for a list of the form $a :: (l ++ [b])$ assuming it holds for $l$, then the property holds for all lists. More formally, given: - A property `motive` on lists of type $\alpha$, - A proof that `motive` holds for the empty list (`nil`), - A proof that `motive` holds for any singleton list `[a]` (`singleton`), - A proof that for any elements $a, b$ and list $l$, if `motive` holds for $l$, then it holds for $a :: (l ++ [b])$ (`cons_append`), then `motive` holds for every list $l$.

List.bidirectionalRec_nil theorem

 {motive : List α → Sort*} (nil : motive []) (singleton : ∀ a : α, motive [a])
  (cons_append : ∀ (a : α) (l : List α) (b : α), motive l → motive (a :: (l ++ [b]))) :
  bidirectionalRec nil singleton cons_append [] = nil

Full source

@[simp]
theorem bidirectionalRec_nil {motive : List α → Sort*}
    (nil : motive []) (singleton : ∀ a : α, motive [a])
    (cons_append : ∀ (a : α) (l : List α) (b : α), motive l → motive (a :: (l ++ [b]))) :
    bidirectionalRec nil singleton cons_append [] = nil := bidirectionalRec.eq_1 ..

Base Case of Bidirectional Recursion on Empty List

Informal description

For any property `motive` defined on lists of type $\alpha$, if: 1. `motive` holds for the empty list (`nil`), 2. `motive` holds for any singleton list `[a]` (`singleton`), and 3. For any elements $a, b$ and list $l$, if `motive` holds for $l$, then it holds for $a :: (l ++ [b])$ (`cons_append`), then the application of the bidirectional recursion principle `bidirectionalRec` to the empty list `[]` yields the proof `nil`.

List.bidirectionalRec_singleton theorem

 {motive : List α → Sort*} (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

Full source

@[simp]
theorem bidirectionalRec_singleton {motive : List α → Sort*}
    (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 := by
  simp [bidirectionalRec]

Bidirectional Recursion on Singleton Lists

Informal description

For any property `motive` defined on lists of type $\alpha$, if: 1. `motive` holds for the empty list (`nil`), 2. `motive` holds for any singleton list `[a]` (`singleton`), and 3. For any elements $a, b$ and list $l$, if `motive` holds for $l$, then it holds for $a :: (l ++ [b])$ (`cons_append`), then the application of the bidirectional recursion principle `bidirectionalRec` to a singleton list `[a]` yields the proof `singleton a`.

List.bidirectionalRec_cons_append theorem

 {motive : List α → Sort*} (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)

Full source

@[simp]
theorem bidirectionalRec_cons_append {motive : List α → Sort*}
    (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) := by
  conv_lhs => unfold bidirectionalRec
  cases l with
  | nil => rfl
  | cons x xs =>
  simp only [List.cons_append]
  dsimp only [← List.cons_append]
  suffices ∀ (ys init : List α) (hinit : init = ys) (last : α) (hlast : last = b),
      (cons_append a init last
        (bidirectionalRec nil singleton cons_append init)) =
      cast (congr_arg motive <| by simp [hinit, hlast])
        (cons_append a ys b (bidirectionalRec nil singleton cons_append ys)) by
    rw [this (x :: xs) _ (by rw [dropLast_append_cons, dropLast_single, append_nil]) _ (by simp)]
    simp
  rintro ys init rfl last rfl
  rfl

Recursion Step for Bidirectional Induction on Lists

Informal description

For any property `motive` defined on lists of type $\alpha$, given: - A proof that `motive` holds for the empty list (`nil`), - A proof that `motive` holds for any singleton list `[a]` (`singleton`), - A proof that for any elements $a, b$ and list $l$, if `motive` holds for $l$, then it holds for $a :: (l ++ [b])$ (`cons_append`), the application of the bidirectional recursion principle `bidirectionalRec` to the list `a :: (l ++ [b])` is equal to the result of applying `cons_append` to $a$, $l$, $b$, and the recursive application of `bidirectionalRec` to $l$. In other words, the recursion step satisfies: $$\text{bidirectionalRec nil singleton cons\_append (a :: (l ++ [b]))} = \text{cons\_append a l b (bidirectionalRec nil singleton cons\_append l)}$$

List.bidirectionalRecOn abbrev

 {C : List α → Sort*} (l : List α) (H0 : C []) (H1 : ∀ a : α, C [a])
  (Hn : ∀ (a : α) (l : List α) (b : α), C l → C (a :: (l ++ [b]))) : C l

Full source

/-- Like `bidirectionalRec`, but with the list parameter placed first. -/
@[elab_as_elim]
abbrev bidirectionalRecOn {C : List α → Sort*} (l : List α) (H0 : C []) (H1 : ∀ a : α, C [a])
    (Hn : ∀ (a : α) (l : List α) (b : α), C l → C (a :: (l ++ [b]))) : C l :=
  bidirectionalRec H0 H1 Hn l

Bidirectional Induction Principle for Lists (On-version)

Informal description

Given a property $C$ on lists of type $\alpha$, to prove $C(l)$ for any list $l$, it suffices to show: 1. $C$ holds for the empty list $[]$, 2. $C$ holds for any singleton list $[a]$ where $a \in \alpha$, 3. For any elements $a, b \in \alpha$ and list $l$, if $C$ holds for $l$, then $C$ holds for the list $a :: (l ++ [b])$.