## Stream: Coq users

### Topic: Equality in count_occ

#### Alex Herve (Jul 19 2022 at 21:41):

I've recently started using Coq and after following and completing some tutorials I realized that I still know nothing. I've got the following code:

``````Require Import List.

Inductive Square := B | W | E.

Definition count_black (l : list Square) : nat :=
count_occ eq l B.
``````

And it gives me the following error:

``````Error:
In environment
l : list Square
The term "eq" has type "?A0 -> ?A0 -> Prop" while it is expected to have type "forall x y : ?A, {x = y} + {x <> y}".
``````

I've seen this {x = y} + {x <> y} before but I don't know what it means exactly, and more importantly how to get such an equality function for my custom type.
Can anyone help me out?

#### Paolo Giarrusso (Jul 19 2022 at 21:49):

``````Require Import List.

Inductive Square := B | W | E.

Definition Square_eq_dec (x y : Square) : {x = y} + {x <> y}.
Proof. decide equality. Defined.

Definition count_black (l : list Square) : nat :=
count_occ Square_eq_dec l B.
``````

#### Paolo Giarrusso (Jul 19 2022 at 21:57):

A value of type `{ A } + { B }.` contains either a proof of `A`, or a proof of `B` (see inductive definition below, if it helps) — here, value of type `{x = y} + {x <> y}` are either proofs that `x = y` or that `x <> y`, and `Square_eq_dec` is a function that takes arguments `x : Square` and `y : Square` and _decides_ whether they're equal or not — that is, it computes and returns a proof that they're equal, or a proof that they're not.

The following is more formal, but it might not make sense yet depending on the tutorials. Formally, `{ A } + { B }` is a notation for type `sumbool`:

``````Locate "{ _ } + { _ }".
(*
Notation "{ A } + { B }" := (sumbool A B) : type_scope
(default interpretation)
*)
``````

and `sumbool` is defined as the following inductive type:

``````Print sumbool.
(*
Inductive sumbool (A B : Prop) : Set :=
left : A -> {A} + {B} | right : B -> {A} + {B}.
*)
``````

#### Alex Herve (Jul 19 2022 at 22:13):

Thank you for your help. It seems to work now!

Last updated: Sep 26 2023 at 12:02 UTC