Functional induction cannot be performed on `List.getLast?`

Stream: lean4

[Asei Inoue]

Recently, I wrote the following proof:

variable {α : Type}

inductive List.IsChain (R : α → α → Prop) : List α → Prop
  | nil : IsChain R []
  | single (a : α) : IsChain R [a]
  | cons_cons {a b : α} {l : List α} (hab : R a b) (hchain : IsChain R (b :: l)) :
    IsChain R (a :: b :: l)

open List

attribute [grind cases] IsChain
attribute [simp] IsChain.nil IsChain.single
attribute [grind <=] IsChain.cons_cons IsChain.single IsChain.nil

namespace List

variable {R : α → α → Prop}

def List.last? (xs : List α) : Option α :=
  match xs with
  | [] => none
  | [a] => some a
  | _ :: b :: bs => last? (b :: bs)

theorem List.last?_cons_exists (xs : List α) (x : α) :
    ∃ y : α, some y = last? (x :: xs) := by
  induction xs generalizing x with
  | nil => exists x
  | cons a as ih =>
    obtain ⟨y, ih⟩ := ih a
    dsimp [last?]
    exists y

grind_pattern List.last?_cons_exists => List.last? (x :: xs)

@[grind =]
theorem IsChain.append {xs ys : List α} :
  IsChain R (xs ++ ys) ↔
    match xs.last?, ys with
    | none, _ => IsChain R ys
    | _, [] => IsChain R xs
    | some x, b :: _ => IsChain R xs ∧ R x b ∧ IsChain R ys := by
  fun_induction List.last? xs with grind

theorem IsChain.append_two {a b : α} {l : List α} :
    IsChain R (l ++ [a, b]) ↔ IsChain R (l ++ [a]) ∧ R a b := by
  induction l with grind

The auxiliary function List.last? that appears in this proof had to be newly defined specifically for this proof.
Although the standard library already provides a function List.getLast?, that function does not have an .induct theorem, so it cannot be used for functional induction.

It seems inconvenient that such a theorem does not exist, but is there a reason why it should not exist, or some fundamental difficulty in rewriting things so that such a theorem could exist?

[Aaron Liu]

it's not a recursive function

[Asei Inoue]

@Aaron Liu Thank you. You are right.

[Asei Inoue]

why it is not recursive? for performance?

[Aaron Liu]

I guess?

[Asei Inoue]

Thanks.

[Markus Himmel]

Non-recursive functions have a fun_cases theorem instead of a fun_induction theorem, and you can use the fun_cases tactic in place of the fun_induction tactic.