Search code examples
coq

How can I compare (equality) of two elements of same Set in Coq?

Inductive ty: Set :=
| I
| O.

Definition f (x: ty) (y: ty): nat :=
  if x = y then 0 else 1.

I want the function f to compare two terms of type ty but it does not compile and I see this error:

The term x = y has type Prop which is not a (co-)inductive type.

Solution

  • You need to prove that equality is decidable for ty (which can be done automatically using decide equality) and then use that definition in the if ... then ... else ... statement. Concretely:

    Inductive ty: Set :=
| I
| O.

Definition ty_eq_dec : forall (x y : ty), { x = y } + { x <> y }.
Proof.
decide equality.
Defined.

Definition f (x: ty) (y: ty): nat :=
  if ty_eq_dec x y then 0 else 1.