## Stream: Coq users

### Topic: General equality operation in coq

#### Julin S (Nov 21 2021 at 11:38):

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?

#### Paolo Giarrusso (Nov 21 2021 at 11:44):

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).

#### Paolo Giarrusso (Nov 21 2021 at 11:46):

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.

#### Julin S (Nov 21 2021 at 11:48):

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

#### Paolo Giarrusso (Nov 21 2021 at 11:50):

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

#### Paolo Giarrusso (Nov 21 2021 at 11:51):

The type might look like `Fixpoint isin {A : eqType} ...` (math-comp, IIRC) or `Fixpoint isin {A} `{EqDecision A} ...` (stdpp)

#### Paolo Giarrusso (Nov 21 2021 at 11:53):

In both cases, you are assuming that `A` satisfies something equivalent to `forall (x y : A), {x = y} + {x <> y}.`

Last updated: Oct 03 2023 at 19:01 UTC