Termination proof of mutual rec functions

Stream: new members

[Rikiya Kashiwagi]

This is a rather general question, but I have no idea how to show termination for these mutually recursive functions.

mutual
def loop1 : List α → List α := loop2

def loop2 : List α → List α
  | [] => []
  | a :: as => loop1 as
end

This code fails to show termination because the argument of loop2 in the definition of loop1 does not decrease, but it's obvious that loop1 terminates.
I am now struggled with a more complicated version of this kind of mutual rec functions, so merging the defnitions of the two is not an intended solution.

[nrs]

replace loopx : List a -> List a with loopx (l : List a) : List a in both cases

[nrs]

the termination check does not have anything it can look for otherwise

[Rikiya Kashiwagi]

Thanks. then how to specify termination_by.

def loop1 (l : List α) : List α := loop2 l
termination_by l

def loop2 (l : List α) : List α
  | [] => []
  | a :: as => loop1 as
termination_by l

termination_by is not needed in this example, but it throws an error at loop2 l.

[nrs]

you must use l as follows:

mutual
  def loop1 (l : List α) : List α := loop2 l

  def loop2 (l : List α) : List α :=
  match l with
  | [] => []
  | a :: as => loop1 as
end

[Rikiya Kashiwagi]

Yes. sorry for confusion, but my question is still the same

[nrs]

hm this is not as obvious as i thought do you have an example of the code you need to prove this for? are you sure you cannot just use structural recursion? I am not sure how to prove wellfounded recursion here

[nrs]

duplicate

[nrs]

Rikiya Kashiwagi

here you go!

mutual
  def loop1 (l :List α) : List α := loop2 l
  termination_by (sizeOf l, 1)

  def loop2 (l : List α) : List α :=
  match l with
  | [] => []
  | a :: as => loop1 as
  termination_by (sizeOf l, 0)
end

I used termination_by? to find the argument. the second argument in the termination_by statement specifies which function terminates first. passing this sort of pair to a termination_by statement only exists in mutually recursive definitions (from what I can see so far, only in where and mutual blocks)

[nrs]

here is an example from source I found instructive

mutual
  def f : Nat → Bool → Nat
    | n, true  => 2 * f n false
    | 0, false => 1
    | n, false => n + g n
  termination_by n b => (n, if b then 2 else 1)
  def g (n : Nat) : Nat :=
    if h : n ≠ 0 then
      f (n-1) true
    else
      n
  termination_by (n, 0)
end

[nrs]

but you can ignore these details and just omit the termination_by statement in your case, you only need to worry about these if termination is not automatically inferred

[Rikiya Kashiwagi]

Indexing iterations makes sense!
Thank you for considering the meaningful example.

I am writing a unification algorithm whose termination proof is not obvious. To avoid duplication, I need to implement unification algorithm as mutually recursive functions.