Termination of last

Stream: new members

[Iocta]

I thought this would work because I'm shrinking the argument. What do I need to do?

def last {T : Type} (xs : List T) (h : xs ≠ []) : T :=
  match xs.tail with
  | [] => xs.head h
  | x'::xs' => last (x'::xs') (xs'.cons_ne_nil x')
/-

fail to show termination for
  last
with errors
failed to infer structural recursion:
Not considering parameter T of last:
  it is unchanged in the recursive calls
Not considering parameter h of last:
  its type is not an inductive
Cannot use parameter xs:
  failed to eliminate recursive application
    last (x' :: xs') ⋯


failed to prove termination, possible solutions:
  - Use `have`-expressions to prove the remaining goals
  - Use `termination_by` to specify a different well-founded relation
  - Use `decreasing_by` to specify your own tactic for discharging this kind of goal
T : Type
xs : List T
h : xs ≠ []
x' : T
xs' : List T
⊢ 1 + sizeOf xs' < sizeOf xs
 -/

[Eric Wieser]

Does match h : xs.tail with help?

[Iocta]

This doesn't work if that's what you mean

def last {T : Type} (xs : List T) (ne_nil : xs ≠ []) : T :=
  match h : xs.tail with
  | [] => (xs.head ne_nil)
  | x'::xs' => last (x'::xs') (xs'.cons_ne_nil x')

[Kyle Miller]

Lean doesn't know that xs.last is smaller. Matching on the result of a function rather than matching on an argument tends to cause problems like this.

Any reason you wouldn't want to write it like this?

def last {T : Type} (xs : List T) (h : xs ≠ []) : T :=
  match xs, h with
  | [x],            _ => x
  | _ :: x' :: xs', _ => last (x'::xs') (xs'.cons_ne_nil x')

[Kyle Miller]

For your original one, the error message suggests some solutions. It says if you add a have with the sizeOf goal, you can get prove termination.

Using Eric's suggestion is the key to being able to prove that goal.

def last {T : Type} (xs : List T) (ne_nil : xs ≠ []) : T :=
  match h : xs.tail with
  | [] => (xs.head ne_nil)
  | x'::xs' =>
    have : 1 + sizeOf xs' < sizeOf xs := by
      cases xs <;> cases h <;> simp
    last (x'::xs') (xs'.cons_ne_nil x')

[Iocta]

def last {T : Type} (xs : List T) (h : xs ≠ []) : T :=
  match xs with
  | [x] => x
  | _ :: x' :: xs' => last (x'::xs') (xs'.cons_ne_nil x')

works yeah