Termination of simple recursive function

Stream: new members

[amzorc]

Hey, I am currently playing around with Lean for some functional programming, which has been mostly great so far! ATM, I am struggling to prove termination of this very simple function (actual version has more interesting logic ofc):

def foo {α} (p : α → Bool) : List α → ℕ
| [] => 0
| _ :: xs => let (as, bs) := xs.span p; foo p bs

I tried termination_by foo p xs => xs.length, but I am not able to prove that List.length bs < Nat.succ (List.length xs) in decreasing_by, mostly (I think) because I don't know how to tell Lean that bs = (xs.span p).2. Am I missing sth obvious?

(Termination is automatic when using separate takeWhile/dropWhile instead of span, but I would really like to know how to prove it for span as above.)

[Shreyas Srinivas]

I am guessing this can be significantly shortened. But here you go:

import Mathlib.Tactic

lemma list_drop_length : ∀ l : List α, ∀ p : α → Bool,
  (l.dropWhile p).length < Nat.succ l.length := by
  simp [Nat.succ_eq_one_add]
  intro l p
  unfold List.dropWhile
  induction l with
  | nil => simp
  | cons head tail ih =>
      simp
      cases (p head) with
      | false => simp
      | true =>
          simp
          unfold List.dropWhile
          trans 1 + List.length tail
          exact ih
          rw [Nat.succ_eq_one_add]
          simp

def foo {α} (p : α → Bool) (l : List α) : ℕ :=
  match l with
  | [] => 0
  | x :: xs =>
      let abs := xs.span p
      foo p abs.2
  termination_by foo p l => l.length
  decreasing_by
    simp_wf
    cases xs with
    | nil =>
        simp [List.dropWhile]
    | cons head tail =>
        apply list_drop_length

[Shreyas Srinivas]

You are losing the hypothesis for span by destructuring the tuple at that let

[amzorc]

Thanks! So the takeaway is that there is just no way to use destructuring let here?

Also FTR, I proved your list_drop_length like this:

lemma list_drop_length : ∀ l : List α, ∀ p : α → Bool,
  (l.dropWhile p).length < Nat.succ l.length := by
  intro l p
  rw [Nat.lt_succ]
  nth_rw 2 [← List.takeWhile_append_dropWhile p l]
  rw [List.length_append]
  linarith

[Shreyas Srinivas]

I would argue that destructuring should work better by introducing hypothesis. At the very least it could add the hypothesesas = (xs.span p).fst and bs = (xs.span p).snd.

[Shreyas Srinivas]

Yeah that proof is much neater than mine

[amzorc]

Shreyas Srinivas said:

I would argue that destructuring should work better by introducing hypothesis. At the very least it could add the hypothesesas = (xs.span p).fst and bs = (xs.span p).snd.

That would be nice, maybe something like let (as, bs) := xs.span p with h and then you get h : (as, bs) = xs.span p? I guess the closest thing is to use match, ie

      match h : xs.span p with
      | (as, bs) => foo p bs

[Notification Bot]

amzorc has marked this topic as resolved.

[Shreyas Srinivas]

Please don't mark topics resolved btw. It messes with zulip links.

[amzorc]

Woops, does it help if I unresolve it?

[Shreyas Srinivas]

I guess. Not sure. I can't test it on my phone

[Notification Bot]

amzorc has marked this topic as unresolved.