Coqでリストを再帰的に検索する

Question

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

しかし、私が思いついたのは間違っています。私は本当にいくつかの指導を感謝します。リストの先頭を要素と比較することで要素のリストを検索する機能が必要です。一致しない場合は、リストの残りの部分を再帰的に関数に渡して繰り返します。

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

ご援助いただきありがとうございます。

は、うーん、事前

Answer 1

にありがとう、私は、作業コードを与えることによって、楽しみを台無しではないでしょう:)。あなたは明らかに何かが欠けています。 Coqでコード化する方法の問題か、より一般的ですか？擬似コードでどのように記述しますか？またはあなたがよく知っている他の言語で？

Answer 2

標準ライブラリのList理論には非常に類似した機能があります。この関数は、引数として述語をとります。つまり、要素タイプからboolに関数fを取り込み、xが見つかった場合はSome x、見つからない場合はNoneを返します。

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. 

特定のオブジェクトaと等しい要素を探しています。つまり、あなたの述語がeq_Interface aであることを意味します。よりも好きなことはeq_Interfaceです。

等価の定義が多いため、型に等価関数を定義するのはあなた次第です。 Coqは=と定義されています。これはLeibniz equalityです。区別する方法がない場合、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. 

だけでなく、その引数が等しいかどうかがわかりますが、また、引数が同じであることや、彼らが異なっていることの証明が付属しています。

あなたはその平等の機能を持っていたら、標準ライブラリ関数の面であなたのfind関数を定義することができます：ご返信用

Definition Interface_is_in x := if List.find (Interface_eq x) then true else false.