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?

Since `Nat.div n 10`

is not a syntactic subterm of `n`

, this requires well-founded induction.

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

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

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

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

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: Jun 24 2024 at 12:02 UTC