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