## Stream: Coq users

### Topic: nat to digits

#### Julin Shaji (Feb 01 2022 at 17:32):

I had been trying to convert a nat value into its constituent digits.

Like `nat2nats 1234` giving `[1; 2; 3; 4]`.

So I did:

``````Require Import List.
Import ListNotations.
Fixpoint nat2nats (n : nat) : list nat :=
match n with
| O => []
| _ => ((Nat.modulo n 10) :: nat2nats (Nat.div n 10) )
end.
``````

but couldn't figure out a way to show that `n` is decreasing on recursive calls and got error like:

``````Recursive definition of nat2nats is ill-formed.
In environment
nat2nats : nat -> list nat
n : nat
n0 : nat
Recursive call to nat2nats has principal argument equal to
"Nat.div n 10" instead of "n0".
Recursive definition is:
"fun n : nat =>
match n with
| 0 => []
| S _ => Nat.modulo n 10 :: nat2nats (Nat.div n 10)
end".
``````

How can we get around this?

#### Paolo Giarrusso (Feb 01 2022 at 17:39):

Since `Nat.div n 10` is not a syntactic subterm of `n`, this requires well-founded induction.

#### Li-yao (Feb 01 2022 at 17:39):

Two standard approaches are

• Use well-founded recursion (with Equations (or Program))
• Use fuel: bound the recursion by an auxiliary nat
``````Fixpoint nat2nats_fuel (fuel : nat) (n : nat) : list nat :=
match fuel with
| O => []
| S fuel => ... nat2nats_fuel fuel (n / 10) ...
end.
``````

#### Paolo Giarrusso (Feb 01 2022 at 17:40):

For naturals, aren't there also specialized functions for well-founded induction on smaller numbers?

#### Paolo Giarrusso (Feb 01 2022 at 17:41):

Not sure they're worth learning (indeed I didn't, else I'd have linked them)

#### Li-yao (Feb 01 2022 at 17:51):

Yeah there is a strong induction principle, but it doesn't spare you from the hard part of thinking about dependent types.

#### Kenji Maillard (Feb 01 2022 at 19:55):

To expand on Li-yao's first point, here is an example with well-founded induction using Equations (v1.3) :

``````Require Import List.
Import ListNotations.
Require Import Lia.
From Equations Require Import Equations.

(* The obligation system is slightly getting in our way so we deactivate it *)
Obligation Tactic := idtac.

Equations? nat2nats (n : nat) : list nat by wf n lt :=
| O => []
| _ => ((Nat.modulo n 10) :: nat2nats (Nat.div n 10) ).
Proof.
(* Goal corresponding to the well-founded recursive call :
Nat.div n 10 < S n *)
apply PeanoNat.Nat.div_lt_upper_bound; lia.
Qed.
``````

Last updated: Oct 03 2023 at 02:34 UTC