Proofs for List.diff

Stream: lean4

[Marcus Rossel]

The following function obviously terminates, right?

import Std.Data.List.Lemmas

opaque p : α → Bool

def f [DecidableEq α] [DecidableEq β] (l : List (α × β)) : List (α × β) :=
  let m := l.filter p
  if m.isEmpty then [] else f (l.diff m)

I encourage anyone to try to prove termination by l.length.

Hints

The following lemmas might help:
* docs#List.diff_cons
* docs#List.length_erase_of_mem
* docs#List.mem_filter
* theorem List.diff_length_le [DecidableEq α] (l₁ l₂ : List α) : (l₁.diff l₂).length ≤ l₁.length := sorry

Here's a start that drills right down to the meat of it:

termination_by l.length
decreasing_by
  simp_wf
  cases l <;> simp [List.isEmpty, m] at *
  case cons hd tl h =>
    cases hm : m <;> simp_all [m]
    case cons hd' tl' =>
      simp_arith
      sorry
/-
hm: List.filter someFilter (hd :: tl) = hd' :: tl'
⊢ List.length (List.diff (hd :: tl) (hd' :: tl')) ≤ List.length tl
-/

I found it surprisingly hard to prove this, as many theorems about List.diff require instances of DecidableEq, whereas the function itself only requires BEq. As a result, in my solution I ended up having to specify explicit instances for List.diff and List.erase. Is this just a hole in the API for List.diff, or is there some other problem here?

My Solution

import Std.Data.List.Lemmas

def List.diff' [DecidableEq α] (l₁ l₂ : List α) : List α :=
  @List.diff _ instBEq l₁ l₂

theorem List.diff_length_le [DecidableEq α] (l₁ l₂ : List α) : (List.diff l₁ l₂).length ≤ l₁.length := by
  induction l₂ generalizing l₁ <;> simp [List.diff]
  case cons hd tl hi =>
    split
    case inr   => apply hi
    case inl h => apply Nat.le_trans (hi ..); simp [List.length_erase_of_mem h]

theorem List.length_erase_of_mem' [DecidableEq α] {a : α} {l : List α} (h : a ∈ l) :
    length (l.erase a) = Nat.pred (length l) :=
  List.length_erase_of_mem h

opaque p : α → Bool

def f [DecidableEq α] [DecidableEq β] (l : List (α × β)) : List (α × β) :=
  let m := l.filter p
  if m.isEmpty then [] else f (l.diff' m)
termination_by l.length
decreasing_by
  simp_wf
  cases l <;> simp [List.isEmpty, m] at *
  case cons hd tl h =>
    cases hm : m <;> simp_all [m]
    case cons hd' tl' =>
      simp_arith [List.diff', hm]
      have h₀ := List.diff_length_le (@List.erase _ instBEq (hd :: tl) hd') tl'
      have h₁ := hm.symm ▸ List.mem_cons_self hd' tl'
      have h₂ := (List.mem_filter.mp h₁).left
      have h₃ := List.length_erase_of_mem' h₂
      exact Nat.le_trans h₀ (by simp [h₃])

[François G. Dorais]

std4#716