bug of functional induction?

Stream: lean4

[Asei Inoue]

open Std

variable {α : Type} [LE α] [DecidableLE α]

@[simp]
def stalinSort (l : List α) : List α :=
  match l with
  | [] => []
  | [x] => [x]
  | x :: y :: xs =>
    if x ≤ y then
      x :: stalinSort (y :: xs)
    else
      stalinSort (x :: xs)

@[grind <=]
theorem stalinSort_cons_mem (x : α) (xs : List α) :
    x ∈ stalinSort (x :: xs) := by
  induction xs with
  | nil => simp
  | cons x xs ih =>
    grind [stalinSort]

example (x : α) (xs : List α) :
    x ∈ stalinSort (x :: xs) := by
  fun_induction stalinSort (x :: xs) with
  | case1 =>
    -- impossible to show
    sorry
  | case2 x1 =>
    -- impossible to show
    sorry
  | case3 x1 x2 xs ih =>
    grind [stalinSort]
  | case4 x1 x2 xs ih =>
    grind [stalinSort]

[Asei Inoue]

Using fun_induction generates a goal which is impossible to show...
using induction works well. I don't know why this occurs.

[Asei Inoue]

@Joachim Breitner I think you were working on functional induction.

[Aaron Liu]

It's because you're inducting on x :: xs

[Asei Inoue]

sorry I don't understand what breaks the proof

[Asei Inoue]

Is there way to write a correct proof using fun_induction?

[Edward van de Meent]

sort of...
lean needs to know which case xs is in in order to know which branch to take. if you want to be able to (almost) directly use fun-induction, you can redefine stalinSortAux like so:

open Std

variable {α : Type} [LE α] [DecidableLE α]

@[simp]
def stalinSortAux (x : α) (l : List α) : List α :=
  match l with
  | [] => [x]
  | y :: ys => if x ≤ y then
    x :: stalinSortAux y ys else
    stalinSortAux x ys

@[simp]
def stalinSort (l : List α) : List α :=
  match l with
  | [] => []
  | x :: ys => stalinSortAux x ys

@[grind <=]
theorem stalinSort_cons_mem (x : α) (xs : List α) :
    x ∈ stalinSort (x :: xs) := by
  induction xs with
  | nil => simp
  | cons x xs ih =>
    grind [stalinSort, stalinSortAux]

example (x : α) (xs : List α) :
    x ∈ stalinSort (x :: xs) := by
  rw [stalinSort]
  fun_induction stalinSortAux x xs with
  | case1 =>
    grind
    -- -- impossible to show
    -- sorry
  | case2 x1 =>
    grind
    -- -- impossible to show
    -- sorry
  | case3 x1 x2 xs ih =>
    grind [stalinSort]

[Edward van de Meent]

it is expected that in your case, fun_inducition fails, because the proof of your theorem depends on the fact that you aren't in the case where x :: xs = []

[Robin Arnez]

You can also generalize before using functional induction to get an equality hypothesis:

open Std

variable {α : Type} [LE α] [DecidableLE α]

@[simp]
def stalinSort (l : List α) : List α :=
  match l with
  | [] => []
  | [x] => [x]
  | x :: y :: xs =>
    if x ≤ y then
      x :: stalinSort (y :: xs)
    else
      stalinSort (x :: xs)

@[grind <=]
theorem stalinSort_cons_mem (x : α) (xs : List α) :
    x ∈ stalinSort (x :: xs) := by
  induction xs with
  | nil => simp
  | cons x xs ih =>
    grind [stalinSort]

example (x : α) (xs : List α) :
    x ∈ stalinSort (x :: xs) := by
  generalize hxxs : x :: xs = xxs
  fun_induction stalinSort xxs with
  | case1 => contradiction
  | case2 x1 => simp_all
  | case3 x1 x2 xs ih => grind [stalinSort]
  | case4 x1 x2 xs ih => grind [stalinSort]