## Stream: new members

### Topic: Proof of termination and mutual recursion

#### King Crawford (Dec 13 2023 at 00:48):

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 (Dec 13 2023 at 09:32):

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 (Dec 13 2023 at 09:34):

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 (Dec 13 2023 at 09:37):

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 (Dec 13 2023 at 09:42):

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 (Dec 13 2023 at 19:20):

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!

Last updated: Dec 20 2023 at 11:08 UTC