1

coq命題（またはそのようなもの...）から証人を抽出しようとしています。

私は次のようなものを持っています

Parameter atom_fresh_for_list :
    forall (xs : list atom), {x : atom | ~ List.In x xs}.

(これは後で証明され、明示的な型でatom:

Lemma atom_fresh_for_list :
    forall (xs : list nat), { n : nat | ~ List.In n xs }.

そのようなものを抽出するにはどうすればよいxですか? ドキュメンテーションによると

そのような (exist xp) から、その証人 x:A を抽出することができます (match などの消去構造を使用)。

しかし、私はこれがどのように機能するのかわかりません....

それはまた言います

A:Type と P:A->Prop を指定すると、構造 {x:A | P x} はタイプです

Parameter C : {x : atom | x \notin xs}しかし、次のようなことを試してみると、

Error: The term "C" has type "{x : atom | x \notin xs}" which should be Set, Prop or Type.
4

1 に答える 1

2

これは、http: //coq.inria.fr/stdlib/Coq.Init.Specif.htmlでよく説明されてい ます。

「sigの投影」の段落の下。(その段落にタイプミスがあることに注意してください: https://coq.inria.fr/bugs/show_bug.cgi?id=2767 )

あなたが望むものはproj1_sig私が信じていると呼ばれています。ドキュメントでどのように定義されているかを確認できます。

于 2012-07-22T08:12:21.910 に答える