# Fixpoint with two decreasing arguments

**URL:** <https://discourse.rocq-prover.org/t/fixpoint-with-two-decreasing-arguments/544>\
**Category:** Using Rocq\
**Tags:** fixpoint\
**Created:** [December 31, 2019, 2:34am UTC](https://discourse.rocq-prover.org/t/fixpoint-with-two-decreasing-arguments/544 "2019-12-31T02:34:57Z")\
**Posts on this page:** 1\
**Showing post:** 4

<div class="post-metadata">

**Author:** ![palmskog](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/palmskog/32/38_2.png) [@palmskog](https://discourse.rocq-prover.org/u/palmskog)\
**Post date:** [January 1, 2020, 4:42pm UTC](https://discourse.rocq-prover.org/t/fixpoint-with-two-decreasing-arguments/544/4 "2020-01-01T16:42:55Z")

</div>

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:

```auto
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

```ocaml
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

```ocaml
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

```ocaml
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))

```

---

_[View the full topic](https://discourse.rocq-prover.org/t/fixpoint-with-two-decreasing-arguments/544)._