Proof of termination and mutual recursion

Stream: new members

[King Crawford]

Hi everyone. I wrote the following function to merge two sorted arrays and am struggling with the termination proof. The loop function calls choose with smaller arguments, but choose just arranges the arguments to loop; they don’t get any smaller. What’s the correct way to go about this?

namespace merge_sorted_arrays
mutual
  def loop (i j : Nat) (ar1 ar2 : Array Nat) (curr : Array Nat) : Array Nat :=
    if hi : i < ar1.size then
      if hj : j < ar2.size then
        if ar1[i] ≤ ar2[j] then
          choose (i + 1) j ar1 ar2 (curr.push ar1[i])
        else
          choose i (j + 1) ar1 ar2 (curr.push ar2[j])
      else
        -- have : Array.size ar1 + Array.size ar2 - (Array.size curr + 1) < Array.size ar1 + Array.size ar2 - Array.size curr := sorry
        choose (i + 1) j ar1 ar2 (curr.push ar1[i])
    else
      curr
  def choose (i j : Nat) (ar1 ar2 : Array Nat) (curr : Array Nat) : Array Nat :=
    if (ar2.size - j) < (ar1.size - i) then
      loop i j ar1 ar2 curr
    else
      loop j i ar2 ar1 curr
end
termination_by
  loop i j ar1 ar2 _ => (ar1.size - i) + (ar2.size - j) -- ar1.size + ar2.size - curr.size
  choose i j ar1 ar2 curr => (ar1.size - i) + (ar2.size - j)

[Joachim Breitner]

It’s a good start! But if I add

decreasing_by
  simp_wf

to the bottom I see this proof goal:

5 goals
ij: ℕ
ar1ar2curr: Array ℕ
hi: i < Array.size ar1
hj: j < Array.size ar2
h✝: ar1[i] ≤ ar2[j]
⊢ Array.size ar1 - (i + 1) < Array.size ar1 - i
ij: ℕ
ar1ar2curr: Array ℕ
hi: i < Array.size ar1
hj: j < Array.size ar2
h✝: ¬ar1[i] ≤ ar2[j]
⊢ Array.size ar2 - (j + 1) < Array.size ar2 - j
ij: ℕ
ar1ar2curr: Array ℕ
hi: i < Array.size ar1
hj: ¬j < Array.size ar2
⊢ Array.size ar1 - (i + 1) < Array.size ar1 - i
ij: ℕ
ar1ar2curr: Array ℕ
h✝: Array.size ar2 - j < Array.size ar1 - i
⊢ False
ij: ℕ
ar1ar2curr: Array ℕ
h✝: ¬Array.size ar2 - j < Array.size ar1 - i
⊢ Array.size ar2 - j + (Array.size ar1 - i) < Array.size ar1 - i + (Array.size ar2 - j)

and note the False; so your termination metric doesn't seem to work at the 4rth recursive call.

[Joachim Breitner]

You’ll make more progress if you tell it that loop is “below” choose like this:

termination_by
  loop i j ar1 ar2 _ => ((ar1.size - i) + (ar2.size - j), 0) -- ar1.size + ar2.size - curr.size
  choose i j ar1 ar2 curr => ((ar1.size - i) + (ar2.size - j), 1)

[Joachim Breitner]

Now you have obligations like

ij: ℕ
ar1ar2curr: Array ℕ
hi: i < Array.size ar1
hj: j < Array.size ar2
h✝: ar1[i] ≤ ar2[j]
⊢ Array.size ar1 - (i + 1) + (Array.size ar2 - j) < Array.size ar1 - i + (Array.size ar2 - j)

which look true, but which I don’t know how to solve easily. Maybe someone else knows which tactic solves that easily? I hope that soon™ you can write

decreasing_by  decreasing_with omega

and it’ll just work (or it’ll even be the default.)

[Joachim Breitner]

Ah, and even with that you’ll run into problem in the last recursive call, because decreasing_with uses

    repeat (first | apply PSigma.Lex.right | apply PSigma.Lex.left)

but in your case you need apply PSigma.Lex.right'. So you’d have to unpack that tactic as well.

All a bit tedious, agreed! But at least doable.

[King Crawford]

Thanks a lot Joachim for the thorough response. I didn't know about the decreasing_by trick, or that the order of the arguments to termination_by matters.
I had an idea yesterday to eliminate the choose function by substituting the definition, trying to prove that function terminates, and to use what I learn to finish the definition using mutual. I'm sure I can use what you've shown me to help with that.
I'll reply with what I come up with.
Thanks!