Coq: リストからの削除についての質問

68 views
Skip to first unread message

Akira Nonaka

unread,
Apr 13, 2012, 11:26:42 PM4/13/12
to fm-f...@googlegroups.com
野中です。

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

unread,
Apr 14, 2012, 12:26:59 AM4/14/12
to fm-f...@googlegroups.com
ProofCafeの今井宜洋です。

リストから要素を削除するためには、要素同士の比較(=)が判定できる必要があります。
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

unread,
Apr 14, 2012, 12:49:33 AM4/14/12
to fm-f...@googlegroups.com
今井さん、

ありがとうございます。序に質問です。

私が参照しているドキュメントは 
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 が3引数とは読み取れないのですが、なにか見るところ
を間違っているのでしょうか?

Akira Nonaka


--
Akira Nonaka

姜帆

unread,
Apr 14, 2012, 1:01:52 AM4/14/12
to fm-f...@googlegroups.com
野中さん

姜です, こんにちは.
横から失礼します.

その上の行に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

unread,
Apr 14, 2012, 2:01:48 AM4/14/12
to fm-f...@googlegroups.com
姜さん、

どうもありがとうございました。まだ、いろいろ覚えないといけないことがあり
ますね。精進いたします。:)

のなか


(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

Reply all
Reply to author
Forward
0 new messages