Stream: Coq users

Topic: nat to digits


view this post on Zulip Julin S (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?

view this post on Zulip 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.

view this post on Zulip Li-yao (Feb 01 2022 at 17:39):

Two standard approaches are

Fixpoint nat2nats_fuel (fuel : nat) (n : nat) : list nat :=
  match fuel with
  | O => []
  | S fuel => ... nat2nats_fuel fuel (n / 10) ...
  end.

view this post on Zulip Paolo Giarrusso (Feb 01 2022 at 17:40):

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

view this post on Zulip Paolo Giarrusso (Feb 01 2022 at 17:41):

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

view this post on Zulip 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.

view this post on Zulip 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: Feb 06 2023 at 11:03 UTC