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] *)
```

Would a solution using the `refine`

tactic be better?

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

The reason is that `Nat.div n 2`

isn't _structurally_ smaller than `n`

, according to the built-in order between terms and subterms.

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

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

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.

there's also https://coq.github.io/doc/master/refman/language/coq-library.html#well-founded-recursion

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

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.

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

And isn't the term `n`

available during pattern matching inside `Equations`

? I had to use `S n'`

instead.

you need to specify the well-founded measure

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

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.

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)

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

?

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

.

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`

.

Is `change`

a tactic that is built-in coq? Or is it from the `Equations`

module? Couldn't find the docs for it.

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

?

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

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

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.

Ju-sh has marked this topic as resolved.

Thanks.

Last updated: Jun 15 2024 at 05:01 UTC