Searching through a list recursively in Coq

Im trying to search for an object in a list, and then perhaps return true if it is found; false otherwise.

However, what I have tried to come up with is incorrect. I would really appreciate some guidance. I need the function to search through the list of elements by comparing the head of the list with the element concerned, if not a match, then recursively put the rest of the list through the function and repeat, by matching the head of the list.

Fixpoint find (li:lis开发者_JS百科t Interface){struct li}: list Interface :=
match li with
| nil => nil
| y::rest => find rest 
end.

Your guidance and assistance is much appreciated.

Thank you in advance

There is a very similar function in the List theory in the standard library. That function takes a predicate as an argument, i.e. a function f from the element type to bool, and it returns Some x if a matching element x is found, or None if none is found.

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.

You're looking for an element that's equal to a particular object a. That means your predicate is eq_Interface a, where eq_Interface is the equality you want over the Interface.

It's up to you to define an equality function on your type, because there can be many definitions of equality. Coq defines =, which is Leibniz equality: two values are equal iff there is no way to distinguish between them. = is a proposition, not a boolean, because this property is not decidable in general. It's also not always the desirable equality on a type, sometimes you want a coarser equivalence relation, so that two objects can be considered equal if they were constructed in different ways but nonetheless have the same meaning.

If Interface is a simple datatype — intuitively, a data structure with no embedded proposition — there's a built-in tactic to build a structural equality function from the type definition. Look up decide equality in the reference manual.

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 not only tells you whether its arguments are equal, but also comes with a proof that the arguments are equal or that they're different.

Once you have that equality function, you can define your find function in terms of the standard library function:

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

Hmmm, I'll not spoil the fun by giving working code :). You are obviously missing something. Is your problem of how to code it in Coq or is it more general? How would you write it in pseudo-code? Or in some other language that you are familiar with?