2

私はこのCoq チュートリアルに取り組んでいますが、最後の演習の 1 つで立ち往生しています。自然数のバイナリ表現のデータ型を定義しましたが、自然数をこの表現に変換したいと思います。

Inductive bin : Type :=
  | BO : bin
  | TO : bin -> bin
  | T1 : bin -> bin.

私の最初の素朴なアプローチはこれでした：

Fixpoint divmod_2 (n : nat) :=
  match n with
  | O => (O, 0)
  | S O => (O, 1)
  | S (S n') => match (divmod_2 n') with
                | (q, u') => ((S q), u')
                end
  end.

Fixpoint to_bin (n : nat) : bin :=
  match n with
  | O => BO
  | S n' => match divmod_2 n' with
            | (q, 0) => TO (to_bin q)
            | (q, 1) => T1 (to_bin q)
            | (_, _) => BO
            end
  end.

Coq は、次のように定義して停止しto_binます。

Error:
Recursive definition of to_bin is ill-formed.
In environment
to_bin : nat -> bin
n : nat
n' : nat
q : nat
n0 : nat
Recursive call to to_bin has principal argument equal to "q" instead of
"n'".

ここで質問です: このto_bin関数を修正するにはどうすればよいですか? here で
説明されているように、十分に確立された再帰の証明を提供する必要がありますか? 初心者向けのチュートリアルなので、もっと簡単な解決策があると思いますか?

4

1 に答える 1

4

最も簡単な解決策は、最初に 2 項ナチュラルの後続関数を定義し、それを使用して単項ナチュラルの後続を変換することだと思います。

于 2013-02-21T21:45:46.290 に答える