CODEWITHSUNDEEP
coq
abhishek
abhishek

Reputation: 880

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.

Upvotes: 2

Views: 1403

Answers (2)

larsr
larsr

Reputation: 5811

You can use match to compare the elements of inductive data types.

Definition f x y := match x,y with I, I | O, O => 0 | _,_ => 1 end.

decide equality is a more general tactic and works for infinite sets, but it is good to know that it is match that is doing the real work.

Upvotes: 1

gallais
gallais

Reputation: 12093

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.

Upvotes: 3

Related Questions