Alex Herve (Jul 19 2022 at 21:41): 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.
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}.
*)
Thank you for your help. It seems to work now!
Last updated: Apr 19 2024 at 06:02 UTC