## Stream: Coq users

### Topic: ✔ Making well-formed recursion for a function

#### Julin S (Nov 25 2021 at 09:02):

I was trying to make a function that finds the binary representation of a `nat`. The binary represent being a list of `nat`s whose every element is either a `0` or a `1`. The MSB of the binary representation is the last element of the list.

This is what I tried:

``````Fixpoint bin (n : nat) : list nat :=
match n with
| O => []%list
| S n' => Nat.modulo n 2 :: bin (Nat.div n 2)
end.
``````

got error saying primitive recursion couldn't be figured out:

``````Recursive definition of bin is ill-formed.
In environment
bin : nat -> list nat
n : nat
n' : nat
Recursive call to bin has principal argument equal to
"Nat.div n 2" instead of "n'".
Recursive definition is:
"fun n : nat => if n is 0 then [] else Nat.modulo n 2 :: bin (Nat.div n 2)".
``````

How can I make the recursion well formed?

Result that I was aiming at was like:

``````bin 4.  (* [0; 0; 1] *)
bin 10.  (* [0; 1; 0; 1] *)
``````

#### Julin S (Nov 25 2021 at 09:03):

Would a solution using the `refine` tactic be better?

#### Paolo Giarrusso (Nov 25 2021 at 09:32):

You need well-founded recursion, and I recommend using the support in the Equations plugin.

#### Paolo Giarrusso (Nov 25 2021 at 09:33):

The reason is that `Nat.div n 2` isn't _structurally_ smaller than `n`, according to the built-in order between terms and subterms.

#### Paolo Giarrusso (Nov 25 2021 at 09:34):

But it is a smaller number (when n is nonzero), which is enough for well-founded recursion

#### Julin S (Nov 25 2021 at 09:49):

Would it be too tedious to do using built-in constructs available in coq?

#### Karl Palmskog (Nov 25 2021 at 09:55):

the "built-in constructs" are generally more verbose than Equations, and they typically have the same status (implemented using the OCaml interface to Coq). And Equations may become "built-in" in the not-too-distant future. Since Equations is part of the Coq Platform, it will generally be available for Coq releases going forward.

#### Paolo Giarrusso (Nov 25 2021 at 12:27):

@Ju-sh it's tedious, error-prone, and you'd have to relearn various tricks used by the implementation. At the very least, you do _not_ want to allow `simpl` or even `unfold` to reduce a well-founded definition.

#### Paolo Giarrusso (Nov 25 2021 at 12:29):

what you want to get is a fully opaque function which satisfies your defining equations — `bin 0 = []` and `bin n@(S _) = Nat.modulo n 2 :: bin (Nat.div n 2)`; that's what Equations will produce.

#### Julin S (Nov 25 2021 at 15:33):

Thanks folks.

I tried

``````From Equations Require Import Equations.

Equations bin (n : nat) : list nat :=
bin O := List.nil;
bin (S n') := Nat.modulo (S n') 2 :: bin (Nat.div (S n') 2).
``````

but again ran into the error:

``````Recursive definition of bin is ill-formed.
In environment
bin : nat -> list nat
n : nat
n0 : nat
Recursive call to bin has principal argument equal to
"Nat.div (S n0) 2" instead of "n0".
Recursive definition is:
"fun n : nat =>
match n with
| 0 => Datatypes.nil
| S n0 => (Nat.modulo (S n0) 2 :: bin (Nat.div (S n0) 2))%list
end".
``````

How can I fix this?

This is my first foray into the equations module. :D

#### Julin S (Nov 25 2021 at 15:34):

And isn't the term `n` available during pattern matching inside `Equations`? I had to use `S n'` instead.

#### Alexander Gryzlov (Nov 25 2021 at 15:43):

you need to specify the well-founded measure

#### Alexander Gryzlov (Nov 25 2021 at 15:43):

e.g.

``````Equations bin (n : nat) : list nat by wf n lt :=
bin O := List.nil;
bin (S n') := Nat.modulo (S n') 2 :: bin (Nat.div (S n') 2).
Next Obligation.
...
``````

#### Alexander Gryzlov (Nov 25 2021 at 15:44):

Ju-sh said:

And isn't the term `n` available during pattern matching inside `Equations`? I had to use `S n'` instead.

you can actually write
`bin n := Nat.modulo n 2 :: bin (Nat.div n 2).`
it'll expand `n` to `S n0` behind the scenes.

#### Julin S (Nov 25 2021 at 16:16):

How can I solve off the obligation?

The goal becomes:

``````1 subgoal

n0 : nat
bin : forall x : nat, x < S n0 -> list nat

========================= (1 / 1)

fst (Nat.divmod n0 1 0 0) < S n0
``````

But I couldn't figure how to dispose of it. Tried random tactics (like `lia`, `simpl`, etc).

(I'm particularly unfamiliar with doing proofs with inequalities)

#### Julin S (Nov 25 2021 at 16:18):

And what does the `by wf n lt` signify in `Equations bin (n : nat) : list nat by wf n lt`?

Is it a way of telling coq the recursion is well-founded on n by `<`?

#### Li-yao (Nov 25 2021 at 16:24):

Yes, and then you need to prove that the recursive calls are indeed applied to arguments smaller than `n`.

#### Li-yao (Nov 25 2021 at 16:30):

The goal is too simplified here, it's really `S n0 / 2 < S n0` (which you can get back by `change (S n0 / 2 < S n0)`) and a good lemma to apply then is `Nat.div_lt`.

#### Julin S (Nov 26 2021 at 05:46):

Is `change` a tactic that is built-in coq? Or is it from the `Equations` module? Couldn't find the docs for it.

#### Julin S (Nov 26 2021 at 05:47):

How do we figure out that the goal that we needed was really `S n0 / 2 < S n0`?

#### Julin S (Nov 26 2021 at 05:48):

It worked perfect. But I was curious as to how the solution was figured out.

``````Equations bin (n : nat) : list nat by wf n lt :=
bin O := List.nil;
bin n := Nat.modulo n 2 :: bin (Nat.div n 2).
Next Obligation.
change (S n0 / 2 < S n0).
apply Nat.div_lt; lia.
Qed.
``````

#### Paolo Giarrusso (Nov 26 2021 at 07:40):

To check whether change is built-in, you can find it here: https://coq.inria.fr/refman/coq-tacindex.html#cap-c

#### Paolo Giarrusso (Nov 26 2021 at 08:02):

Regarding `S n0 / 2 < S n0`, that asserts the input of `bin (Nat.div n 2)` is smaller (via `<`) than the input to `bin n`: the input of the recursive call is smaller than the input to the original call. I assume `n0` comes up because `n` expands to `S n0` as @Alexander Gryzlov mentioned.

#### Notification Bot (Nov 27 2021 at 06:04):

Ju-sh has marked this topic as resolved.

#### Julin S (Nov 27 2021 at 06:04):

Thanks.

Last updated: Jun 15 2024 at 05:01 UTC