Coq: nat を string で十進表記する

  • 3
    いいね
  • 0
    コメント

まとめ

  • n: nat を十進表記の文字列に変換してみた
  • Functional Scheme 使えば大した手間はかからない。
  • ソースコード(Gist)

必要なライブラリ

Require Import Arith Ascii String Recdef Wf_nat.

最初の三つは言わずもがな。
一桁の数は文字列ではなく文字にしたいので、 Ascii も忘れずに。

RecdefFunction コマンドを使うため、 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_natdiv10 を使って、自然数の十進表記をする函数 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_natlt_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 クラス作って色々遊ぼうかなぁと思っていたときの名残です。