---
title: Coq: nat を string で十進表記する
tags: Coq
author: mathink
slide: false
---n: natを十進表記の文字列に変換してみたFunctional Scheme使えば大した手間はかからない。- ソースコード(Gist)
Require Import Arith Ascii String Recdef Wf_nat.最初の三つは言わずもがな。
一桁の数は文字列ではなく文字にしたいので、 Ascii も忘れずに。
Recdef は Function コマンドを使うため、 Wf_nat は < が well-founded であることを利用するためにインポートする。
十進表記をするので、自然数を 10 で割った商と余りを求める函数を定義する。
頑張って S を十個並べる。
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 *)そして、次の補題が後々必要になるので証明しよう。
Lemma div10_lt:
forall (n: nat),
let (q, r) := div10 n in (q < n \/ n = 0).欲しい結論は 0 < n 時の q < n なのだが、 0 < n を仮定に持ってくると証明が大変になるので(気になる人はやってみよう)、結論部に n = 0 を \/ する形にした。
この証明では div10 に関する帰納法を使うので、あらかじめ
Functional Scheme div10_ind := Induction for div10 Sort Prop.というコマンドを実行しておくとよい。
すると、 div10_lt の証明は以下のようになる。
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.大して難しくない。
まず、一桁毎の変換函数を用意する。
それが print_digit である。
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.ダブルクォーテーションで括っているが、 char_scope 内なのでこれは文字を表している。
変換の正当性を示す目的があるのなら引数の型は nat ではなく { n | n < 10 } の方がよいかもしれないが、今回は単純に変換函数を定義することのみを目的としているので、想定していない引数については空文字を返すようにしてある。
そして、この print_nat と div10 を使って、自然数の十進表記をする函数 print_nat が次のように定義できる。
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:) *)二つめについては Wf_nat に lt_wf というそのままの補題があるので、それを使えばよい。
一つめのゴールについても、先程示した div10_lt があれば簡単に証明を終えられる。
実際の証明スクリプトは下記の通りである。
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 *)大丈夫そうである(「そう」？」)。
ちなみに、5001 からはスタックオーバフローとかするかもよという警告が表示され、
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 *)36185 以上になると実際にスタックオーバフローする。
Eval compute in print_nat 36184.
(* = "36184" *)
(* : string *)
Eval compute in print_nat 36185.
(* Stack overflow. *)
なお、 Check の場合にスタックオーバフローするのは
Check 36185.
(* 36185 *)
(* : nat *)
Check 36186.
(* Stack overflow. *)の通り、 36186 からである。
Show クラス作って色々遊ぼうかなぁと思っていたときの名残です。