Stream: math-comp users

Topic: What is the problem with `seq A` if just has `EqType`?

walker (Oct 25 2022 at 13:39):

So the sinnet I am struggling with is something similar to this:

From mathcomp Require Import all_ssreflect.

Section FOO.
Context {A B: Type}.
Context {eqA: A -> A -> bool}.
Context {eqAP: Equality.axiom eqA}.
Context `{!EqType A (EqMixin eqAP)}.

Lemma foo: forall (a: A) (acc: seq A),
    a \in acc.
Admitted.
End FOO.

the error message does not make sense:

The term "acc" has type "seq A" while it is expected to have type
 "pred_sort ?pT".

When I try to replace A with nat, everything works flawlessly, that means the problem is with A and not with seq

Cyril Cohen (Oct 25 2022 at 13:41):

eqType is noi a typeclass, what you wrote does not work in the current state of affairs.
Here is the context that makes it work:

From mathcomp Require Import all_ssreflect.

Section FOO.
Context {A : eqType}.
Lemma foo: forall (a: A) (acc: seq A), a \in acc.
Admitted.
End FOO.

walker (Oct 25 2022 at 14:05):

pardon me!
I am struggling to understand how this work given that line:

https://math-comp.github.io/htmldoc/mathcomp.ssreflect.eqtype.html#Equality.Exports.eqType

walker (Oct 25 2022 at 14:05):

What is the difference between

Context {A : eqType}.

and

Context {A : Type}.

Cyril Cohen (Oct 25 2022 at 14:07):

Context {A : eqType}. introduces an element of a structure (eqType) which contains a Type (accessible though a coercion, hence you can write x : A and Coq will automatically understand x : Equality.sort);, an operator (==) and a proof that this equality is "the same" as =, but as a boolean.

Paolo Giarrusso (Oct 25 2022 at 14:08):

:+1: given your link, I wonder if I should point out that type is https://math-comp.github.io/htmldoc/mathcomp.ssreflect.eqtype.html#Equality.type

walker (Oct 25 2022 at 14:10):

I misread type as Type thanks everyone!

Paolo Giarrusso (Oct 25 2022 at 14:11):

and I'm tempted to recommend https://hal.inria.fr/hal-00816703v1/document to see a quick introduction to canonical structures and their use in math-comp

Enrico Tassi (Oct 25 2022 at 14:18):

Also https://zenodo.org/record/7118596#.Y1fwAUpBy8Q part 2 should help (but is longer)

Last updated: Feb 08 2023 at 08:02 UTC