# 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:** 5\
**Page:** 1

<div class="post-metadata">

**Author:** ![Lys](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/lys/32/48_2.png) [@Lys](https://discourse.rocq-prover.org/u/Lys)\
**Post date:** [December 31, 2019, 2:34am UTC](https://discourse.rocq-prover.org/t/fixpoint-with-two-decreasing-arguments/544/1 "2019-12-31T02:34:57Z")

</div>

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

```coq
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.

---

<div class="post-metadata">

**Author:** ![MSoegtrop](https://avatars.discourse-cdn.com/v4/letter/m/ea5d25/32.png) [@MSoegtrop](https://discourse.rocq-prover.org/u/MSoegtrop)\
**Post date:** [December 31, 2019, 8:53am UTC](https://discourse.rocq-prover.org/t/fixpoint-with-two-decreasing-arguments/544/2 "2019-12-31T08:53:07Z")

</div>

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

---

<div class="post-metadata">

**Author:** ![SkySkimmer](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/skyskimmer/32/369_2.png) [@SkySkimmer](https://discourse.rocq-prover.org/u/SkySkimmer)\
**Post date:** [December 31, 2019, 10:14am UTC](https://discourse.rocq-prover.org/t/fixpoint-with-two-decreasing-arguments/544/3 "2019-12-31T10:14:11Z")

</div>

You can use an internal auxiliary fixpoint

```coq
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.

```

---

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

```

---

<div class="post-metadata">

**Author:** ![MSoegtrop](https://avatars.discourse-cdn.com/v4/letter/m/ea5d25/32.png) [@MSoegtrop](https://discourse.rocq-prover.org/u/MSoegtrop)\
**Post date:** [January 13, 2020, 6:01pm UTC](https://discourse.rocq-prover.org/t/fixpoint-with-two-decreasing-arguments/544/5 "2020-01-13T18:01:52Z")

</div>

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.