Fixpoint with two decreasing arguments

Using Coq
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