Fixpoint with two decreasing arguments

Using Coq
1

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.

2

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.
3

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
4

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
5

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.