Question

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:list 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

Answer 1

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.

Answer 2

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?

友情链接