Coq: リストからの削除についての質問
Akira Nonaka
Coqの勉強を細々と続けています。標準ライブラリでのリストからの要素の削除
がうまくいかず悩んでおります。いろいろ探してみたのですが、エ ラーメッ
セージの意味もわかっておりません。やりたいのはリストから要素を削除するこ
となのですが、どなたかご教授いただけないでしょうか？
どうぞよろしくお願いします。
[ソース]
Require Import List.
Eval compute in remove 3 3::2::1::nil.
[実行結果]
Toplevel input, characters 23-24:
Error: The term "3" has type "nat" while it is expected to have type
"forall x y : ?2, {x = y} + {x <> y}".
Yoshihiro Imai
リストから要素を削除するためには、要素同士の比較(=)が判定できる必要があります。
Coqのremove関数は第一引数に判定関数を渡す必要があるようです。
remove関数
第一引数 (eq_dec : forall x y : A, {x = y} + {x <> y}) : (=)の判定関数
第二引数 (x : A) : 削除する値
第三引数 (l : list A) : 元のリスト
リストの要素としてnat型を考える場合は、nat用の判定関数がArithモジュールに
あるので、それを使います。(*1)
eq_nat_dec
: forall n m : nat, {n = m} + {n <> m}
この例では次のように呼び出せばうまくいきます。
Require Import List.
Require Import Arith.
Eval compute in remove eq_nat_dec 3 (3::2::1::nil).
*1) 「SearchPattern (forall (_ _:nat), { _ = _ } + { _ <> _}).」で判定関数がスコープ内に
あるかどうか探すことができます。
2012年4月14日12:26 Akira Nonaka <akira....@gmail.com>:
--
Yoshihiro Imai
mail: yim...@gmail.com, y.i...@ocaml.jp
twitter: @yoshihiro503
Akira Nonaka
ありがとうございます。序に質問です。
私が参照しているドキュメントは
http://coq.inria.fr/library/Coq.Lists.List.html です。
ここにremoveの定義が書いてあり、以下のようになっています。
Fixpoint remove (x : A) (l : list A) : list A :=
match l with
| [] => []
| y::tl => if (eq_dec x y) then remove x tl else y::(remove x tl)
end.
ここだけ見ると remove が３引数とは読み取れないのですが、なにか見るところ
を間違っているのでしょうか？
Akira Nonaka
--
Akira Nonaka
姜帆
姜です, こんにちは.
横から失礼します.
その上の行にHypothesis eq_dec ...というのがあります.
こちらのドキュメントでは明示的にSectionが書かれていませんが,
別のドキュメント(http://coq.inria.fr/V8.1/stdlib/Coq.Lists.List.html)では,
Sectionを用いています.
外部からSection内の関数を利用するには,
HypothesisやVariableで宣言されている型に,
値を与える必要があります.
マニュアルのこちらの例をごらんになってください.
http://coq.inria.fr/doc/Reference-Manual004.html#toc17
このSection s1の中でx'という関数があります.
このx'はSection内では引数を取りません.
しかし定義から明確にVariable x:natに依存していますよね.
するとSection外部で関数x'の定義をPrintしてみると,
xを与えよ, と書かれています.
2012年4月14日13:49 Akira Nonaka <akira....@gmail.com>:
Akira Nonaka
どうもありがとうございました。まだ、いろいろ覚えないといけないことがあり
ますね。精進いたします。:)
のなか
(2012/04/14 14:01), 姜帆 wrote:
> 野中さん
>
> 姜です, こんにちは.
> 横から失礼します.
>
> その上の行にHypothesis eq_dec ...というのがあります.
> こちらのドキュメントでは明示的にSectionが書かれていませんが,
> 別のドキュメント(http://coq.inria.fr/V8.1/stdlib/Coq.Lists.List.html)では,
> Sectionを用いています.
>
> 外部からSection内の関数を利用するには,
> HypothesisやVariableで宣言されている型に,
> 値を与える必要があります.
>
> マニュアルのこちらの例をごらんになってください.
> http://coq.inria.fr/doc/Reference-Manual004.html#toc17
> このSection s1の中でx'という関数があります.
> このx'はSection内では引数を取りません.
> しかし定義から明確にVariable x:natに依存していますよね.
> するとSection外部で関数x'の定義をPrintしてみると,
> xを与えよ, と書かれています.
> Akira Nonaka
--
Akira Nonaka