Stream: math-comp users

Topic: Problem with @Pack


view this post on Zulip Étienne Miquey (Jun 19 2023 at 10:18):

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

view this post on Zulip Pierre Roux (Jun 19 2023 at 10:58):

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.

view this post on Zulip Étienne Miquey (Jun 19 2023 at 12:16):

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... ?

view this post on Zulip Pierre Roux (Jun 19 2023 at 12:23):

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?

view this post on Zulip Étienne Miquey (Jun 19 2023 at 14:43):

In the section 6.3, page 120 of the book :

image.png

view this post on Zulip Cyril Cohen (Jun 19 2023 at 14:47):

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

view this post on Zulip Cyril Cohen (Jun 19 2023 at 14:48):

The ad-hoc eqType record is defined a the beginning of section 6.3, but it was never defined like this in the library.

view this post on Zulip Cyril Cohen (Jun 19 2023 at 14:48):

(Or at least not since 2009)

view this post on Zulip Cyril Cohen (Jun 19 2023 at 14:49):

See 6.4:

view this post on Zulip Cyril Cohen (Jun 19 2023 at 14:49):

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.

view this post on Zulip Étienne Miquey (Jun 19 2023 at 14:50):

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


Last updated: Jul 25 2024 at 16:02 UTC