Coq の nat を十進表記で string に変換

print_nat.v

Require Import Arith Ascii String Recdef Wf_nat.

Fixpoint div10 (n: nat): nat * nat :=
  match n with
  | S (S (S (S (S (S (S (S (S (S n'))))))))) =>
    let (q, r) := div10 n' in (S q, r)
  | digit => (0, digit)
  end.

Eval compute in div10 8.
(* = (0, 8) *)
(* : nat * nat *)

Eval compute in div10 12.
(* = (1, 2) *)
(* : nat * nat *)

Functional Scheme div10_ind := Induction for div10 Sort Prop.

Lemma div10_lt:
  forall (n: nat),
    let (q, r) := div10 n in (q < n \/ n = 0).
Proof.
  intros n.
  functional induction div10 n; auto with arith.
  left.
  rewrite e9 in IHp.
  destruct IHp.
  - apply lt_n_S.
    now repeat apply lt_S.
  - subst; simpl in *.
    injection e9; intros; subst; auto with arith.
Qed.

Open Scope char_scope.
Definition print_digit (n: nat): ascii :=
  match n with 
  | 0 => "0"
  | 1 => "1"
  | 2 => "2"
  | 3 => "3"
  | 4 => "4"
  | 5 => "5"
  | 6 => "6"
  | 7 => "7"
  | 8 => "8"
  | 9 => "9"
  | _ => " "
  end.

Open Scope string_scope.
Function print_nat (n: nat){wf lt n}: string :=
  let (q, r) := div10 n in
  match q with
  | O => String (print_digit r) ""
  | S _ => print_nat q ++ String (print_digit r) ""
  end.
(* 2 subgoals, subgoal 1 (ID 832) *)
  
(*   ============================ *)
(*   forall n q r n0 : nat, q = S n0 -> div10 n = (S n0, r) -> S n0 < n *)

(* subgoal 2 (ID 833) is: *)
(*  well_founded lt *)
(* (dependent evars:) *)


Proof.
  - intros; subst.
    generalize (div10_lt n); rewrite teq.
    intros [Hlt | Heq]; auto.
    subst; simpl in *; discriminate.
  - now apply lt_wf.
Defined.

Eval compute in print_nat 0.
(* = "0" *)
(* : string *)

Eval compute in print_nat 23.
(* = "23" *)
(* : string *)

Eval compute in print_nat 256.
(* = "256" *)
(* : string *)

Eval compute in print_nat 4230.
(* = "4230" *)
(* : string *)

Eval compute in print_nat 5001.
(* Warning: Stack overflow or segmentation fault happens when working with *)
(*  large numbers in nat (observed threshold may vary from 5000 to 70000 *)
(*  depending on your system limits and on the command executed). *)
(* = "5001" *)
(* : string *)

Eval compute in print_nat 36184.
(* = "36184" *)
(* : string *)

Eval compute in print_nat 36185.
(* Stack overflow. *)

Check 36185.
(* 36185 *)
(*      : nat *)

Check 36186.
(* Stack overflow. *)