# Zulip Chat Archive

## 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