termination in Lean

Stream: general

[Pedro Antonino]

Hi there,

I am new to Lean and I am trying to formalise some basic things to learn it.

I am struggling with to find a way to prove termination for the following function:

noncomputable def inter2 (l0 : List α) (l1 : List α ) : Set (List α) :=
  match (l0,l1) with
  | ([], []) => {[]}
  | (a::as, []) => {a::as}
  | ([], b::bs) => {b::bs}
  | (a::as, b::bs) => (inter2 as (b::bs)) ∪ (inter2 (a::as) bs)

I am aware that Lean can prove termination if I turn (l0,l1) into l0, l1 but I wanted, for the sake of exercise, learn how to deal with this case above.

Many thanks in advance!

[Joachim Breitner]

Try termination_by (l0.length, l1.length)

[Pedro Antonino]

I sill get the error "failed to prove termination" :-(

[Mario Carneiro]

this works:

noncomputable def inter2 (l0 : List α) (l1 : List α ) : Set (List α) :=
  match e : (l0,l1) with
  | ([], []) => {[]}
  | (a::as, []) => {a::as}
  | ([], b::bs) => {b::bs}
  | (a::as, b::bs) => (inter2 as (b::bs)) ∪ (inter2 (a::as) bs)
termination_by (l0.length, l1.length)
decreasing_by all_goals cases e; decreasing_with decreasing_trivial

Lean really doesn't like matches on tuples though, the default decreasing tactic doesn't do what you want

[Pedro Antonino]

Thank you!