# Fixpoint with two decreasing arguments

How do I define a fixpoint function with two arguments, with guaranteed decreasing of either argument?

``````Parameter b : bool.
Fixpoint foo (fuel : nat) (xs : list unit) : unit :=
match fuel with
| O => tt
| S fuel' =>
match xs with
| [] => tt
| x :: xs' =>
if b then foo fuel xs' else foo fuel' xs
end
end.
``````

Error: Cannot guess decreasing argument of fix.

You have to give a measure function and show that it is decreasing, e.g.:

``````Require Import List.
Require Import Program.Wf.
Require Import Lia.
Import List.ListNotations.

Parameter b : bool.

Program Fixpoint foo (fuel : nat) (xs : list unit) {measure (fuel + (length xs))} : unit :=
match fuel with
| O => tt
| S fuel' =>
match xs with
| [] => tt
| x :: xs' =>
if b then foo fuel xs' else foo fuel' xs
end
end.
Next Obligation.
induction xs'; (cbn; lia).
Qed.``````

You can use an internal auxiliary fixpoint

``````Fixpoint foo (fuel : nat) : list unit -> unit :=
fix foo_aux (xs : list unit) : unit :=
match fuel with
| O => tt
| S fuel' =>
match xs with
| [] => tt
| x :: xs' =>
if b then foo_aux xs' else foo fuel' xs
end
end.
``````
3 Likes

I guess this is beating a dead (solved) horse at this point, but it’s interesting to also look at the Equations version, which is arguably the most succinct and natural:

``````Require Import List.
Import ListNotations.
Require Import Lia.
From Equations Require Import Equations.

Parameter b : bool.
Equations foo (fuel : nat) (xs : list unit) : unit by wf (fuel + (length xs)) :=
foo O _ := tt;
foo _ [] := tt;
foo (S fuel') (x :: xs') := if b then foo (S fuel') xs' else foo fuel' (x :: xs').
Next Obligation.
induction xs'; (cbn; lia).
Qed.
``````

If there was only some syntax for referring to `S fuel'` and `x :: xs`, with single variable names, this would look even better.

One interesting aspect is the readability of the extracted code. Here I would argue that the inner fixpoint wins, Equations comes second, and Program Fixpoint last.

### inner fixpoint

``````let rec foo b fuel =
let rec foo_aux xs =
match fuel with
| O -> ()
| S fuel' -> (match xs with
| [] -> ()
| _ :: xs' -> if b then foo_aux xs' else foo b fuel' xs)
in foo_aux
``````

### Equations

``````let foo b a b0 =
let rec fix_F x =
match pr1 x with
| O -> ()
| S n -> (match pr2 x with
| [] -> ()
| u :: l -> if b then let y = (S n),l in fix_F y else let y = n,(u :: l) in fix_F y)
in fix_F (a,b0)
``````

### Program Fixpoint

``````let rec foo_func b x =
let fuel = projT1 x in
let xs = projT2 x in
let foo0 = fun fuel0 xs0 -> foo_func b (ExistT (fuel0, xs0)) in
(match fuel with
| O -> ()
| S fuel' -> (match xs with
| [] -> ()
| _ :: xs' -> if b then foo0 fuel xs' else foo0 fuel' xs))

let foo b fuel xs =
foo_func b (ExistT (fuel, xs))
``````
2 Likes

I guess this was just a minimal toy case. That the inner fixpoint trick works is not that common in such cases. It would be very interesting to see how the extracted code looks for a real world example.