3

リスト内のオブジェクトを検索しようとしていますが、見つかった場合はtrueを返します。それ以外の場合はfalse。

しかし、私が思いついたのは間違っています。いくつかのガイダンスを本当にいただければ幸いです。リストの先頭を関連する要素と比較して要素のリストを検索する関数が必要です。一致しない場合は、リストの残りの部分を関数に再帰的に配置し、リストの先頭を照合して繰り返します。

Fixpoint find (li:list Interface){struct li}: list Interface :=
match li with
| nil => nil
| y::rest => find rest 
end.

あなたの指導と援助は大歓迎です。

前もって感謝します

4

2 に答える 2

3

List標準ライブラリの理論には非常によく似た関数があります。その関数は引数として述語、つまりf要素型から への関数を取り、一致する要素が見つかった場合、または見つからなかった場合boolに戻ります。Some xxNone

Variable A : Type.
Fixpoint find (f:A->bool) (l:list A) : option A :=
  match l with
    | nil => None
    | x :: tl => if f x then Some x else find tl
  end.

特定の object と等しい要素を探していますa。つまり、述語はeq_Interface aであり、eq_Interfaceは に対して必要な等式ですInterface。

等値の定義が多数存在する可能性があるため、型に等値関数を定義するのはあなた次第です。Coq は=、ライプニッツの等式である を定義しています。2 つの値は、それらを区別する方法がない場合は等しいです。=このプロパティは一般に決定可能ではないため、ブール値ではなく命題です。また、型の同等性が常に望ましいとは限りません。場合によっては、2 つのオブジェクトが異なる方法で構築されていても同じ意味を持つ場合に同等と見なすことができるように、より粗い同等関係が必要になることがあります。

単純なデータ型 (直観的に言えばInterface、命題が埋め込まれていないデータ構造) の場合、型定義から構造的等値関数を構築する組み込みの戦術があります。decide equalityリファレンスマニュアルで調べてください。

Definition Interface_dec : forall x y : Interface, {x=y} + {x <> y}.
Proof. decide equality. Defined.
Definition Interface_eq x y := if Interface_dec x y then true else false.

Interface_dec引数が等しいかどうかを示すだけでなく、引数が等しいか異なるかの証明も付属しています。

その等価関数を取得したらfind、標準ライブラリ関数に関して関数を定義できます。

Definition Interface_is_in x := if List.find (Interface_eq x) then true else false.
于 2011-07-10T14:03:34.607 に答える
-1

うーん、動作するコードを与えることで楽しみを台無しにすることはありません:)。あなたは明らかに何かが欠けています。Coqでそれをコーディングする方法の問題ですか、それともより一般的ですか？どのように擬似コードでそれを書きますか？または、あなたが精通している他の言語で？

于 2011-07-09T19:50:57.067 に答える