Stream: Coq users

Topic: General equality operation in coq


view this post on Zulip 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?

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Nov 21 2021 at 11:50):

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

view this post on Zulip 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)

view this post on Zulip 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: Feb 04 2023 at 21:02 UTC