Non-structural recursivity, termination_by arguments

Stream: new members

[Philippe Duchon]

I am trying to write a very basic, but non-structurally recursive function: the merging of two sorted lists. I know which measure to use (the sum of lengths ot the two lists), but I cannot prove the goals because (I believe) I don't know how to tell Lean to "remember equations" about the arguments.

MWE:

import Mathlib

def ms (l1 l2: List ℕ) : List ℕ :=
match l1, l2 with
| [], _ => l2
| _, [] => l1
| (v1::l1'), (v2::l2') => if v1 ≤ v2 then v1::(ms l1' l2) else v2::(ms l1 l2')
termination_by (List.length l1 + List.length l2)
decreasing_by
  simp_wf
  sorry -- l1'.length + l2.length < l1'.length + 1 + (l2'.length + 1)
  simp_wf
  sorry -- l1.length + l2'.length < l1'.length + 1 + (l2'.length + 1)

In both sorrys above, I have no way to conclude because I have no hypothesis linking l2 and l2' (its tail), or l1 and l1' (again, its tail).

Very likely this is a completely standard problem and I'm just missing some annotation somewhere...

Of course I could just reconstruct l1 as v1::l1' and l2 as v2::l2', but I'm pretty sure there is a simpler way to do this...

[Aaron Liu]

You can try
match h1 : l1, h2 : l2 with

[Philippe Duchon]

Perfect, thanks!

(the linter still underlines the h1 and h2 as unused variables, even though they are used in the proofs)

[Aaron Liu]

Then you can also do
match _ : l1, _ : l2 with
to shut it up

[Philippe Duchon]

If I do this, then I cannot rewrite them! They are really used, just not in the definition of the function, only in the proof of its termination (I'd say they really should not be considered unused variables, but I have no idea how the option works and can be changed)