Is there a generalized way to do an equality check between two elements of the same type in coq?

I was trying to make a function to see if an element is part of a list and did

```
Fixpoint isin {A : Type} (x : A) (l : list A) : bool.
match s with
| nil => false
| cons x xs => (* How to do equality check? *)
end.
```

But I couldn't figure a way to do the equality check there. How can it be done? Or is my approach towards this problem wrong?

Your hole can only be filled if you demand a proof that A has decidable equality (not all types do, and you can't magic the implementation out of thin air).

In the stdlib, list_eq_dec shows how that can look like; again, other libraries (eg stdpp and math-comp etc.) have more convenient ways to thread such proofs around.

All right, if not all types have this decidable equality property, I guess there is no 'generalized' way to do this.

But "generalized over the types with decidable equality" is still pretty good!

The type might look like `Fixpoint isin {A : eqType} ...`

(math-comp, IIRC) or `Fixpoint isin {A} `

{EqDecision A} ...` (stdpp)

In both cases, you are assuming that `A`

satisfies something equivalent to `forall (x y : A), {x = y} + {x <> y}.`

Last updated: Oct 13 2024 at 01:02 UTC