Hi, I'm trying to learn how to use EqType, finType etc... following the mathcomp book, and following the code snippets I have an issue with

```
From mathcomp Require Import all_ssreflect.
Definition eqb (a b : bool) := if a then b else ~~ b.
Definition bool_eqType : eqType := @Pack bool eqb.
```

Coq tells me that Pack cannot be found in the current environment, and when I replace it with `@Equality.Pack`

, I get the following error message:

```
The term "eqb" has type "bool -> bool -> bool"
while it is expected to have type "Equality.mixin_of bool".
```

Any idea on what might be the problem here? Thanks !

PS/ *I'm running coq 8.16.1 with coq-mathcomp-ssreflect 1.17.0 installed through opam*

`Equality.Pack`

expects (as shown by `About Equality.Pack`

) an equality mixin which embodies the equality with a proof of corectness:

```
From mathcomp Require Import all_ssreflect.
Definition eqb (a b : bool) := if a then b else ~~ b.
Lemma eqb_correct a b : reflect (a = b) (eqb a b). Admitted.
Definition bool_eqMixin := Equality.Mixin eqb_correct.
Definition bool_eqType : eqType := Equality.Pack bool_eqMixin.
(* or with explicit arguments
Definition bool_eqMixin := @Equality.Mixin bool eqb eqb_correct.
Definition bool_eqType : eqType := @Equality.Pack bool bool_eqMixin.
*)
(* Then the eqType can be made canonical *)
Canonical bool_eqType.
```

Thanks for the answer, actually by unfolding the definitions and so I did manage to do this (for another type than bool), I guess my question should rather be : *the snippet looks quite easier to write (even if some left goals corresponding to the defs/lemmas you mentioned are left to prove, is it still the case that such a thing can be written down or was it only for previous versions of mathcomp/coq etc... ?*

Your initial snippet looks strange because it does not involve anywhere the proof of correctness of the equality (`eqb_correct`

) which has always been in MathComp as far as I know. Maybe it is some intermediate version to ease the explanations in the book, i don't know. From which page of the book did you take it / took inspiration from?

In the section 6.3, page 120 of the book :

Unfortunately this is a fictive example simplified for the purpose of pedagogy and this particular definition was never in the library.

The ad-hoc `eqType`

record is defined a the beginning of section 6.3, but it was never defined like this in the library.

(Or at least not since 2009)

See 6.4:

6.4 Records as (first-class) interfaces

When we define an overloaded notation, we convey through it more than just the arity (or

the type) of the associated operation. We associate to it a property, or a collection thereof.

For example, in the context of group theory, the infix + symbol is typically preferred to *

whenever the group law is commutative.

Going back to our running example, the actual definition of eqType used in the Mathe-

matical Components library also contains a property which enforces the correctness and

the completeness of the comparison test.

Thanks Cyril, I missed the previous definition indeed, my bad!

Last updated: Jul 25 2024 at 16:02 UTC