Hi, I haven't seen the code snippets (from section 7.6 to 7.8 ) of Mathematical Components and I could not have a correct result following the book directly.

Could anyone give me some suggestions? Thanks

I would like to use sequential relations and permutations, maybe need more examples like in book like there already given.

For example, I type below as section 7.7

From mathcomp Require Import all_ssreflect.

Set Implicit Arguments.

Unset Strict Implicit.

Unset Printing Implicit.

Inductive perm_of (T : finType) : Type :=

Perm (pval : {ffun T -> T}) & injectiveb pval.

Definition pval p := let: Perm f _ := p in f.

Notation "{ ’perm’ T }" := (perm_of T).

there report

The following term contains unresolved implicit arguments:

(fun '(@Perm _ f _) => f)

More precisely:

- ?t: Cannot infer ?t in the partial instance "{ffun ?t -> ?t}" found for the

type of this pattern-matching problem.

at the Definition pval ... line

Coq guesses that the type of `p`

has the form `perm_of ?t`

but can not find a suitable `?t`

. You can do `Definition pval (T : finType) (p : perm_of T) := let: Perm f _ := p in f.`

Thanks @Quentin VERMANDE , it works.

While there reports:

The term "pval" has type "forall T : finType, { ’perm’ T} -> {ffun T -> T}"

while it is expected to have type "?sub_sort -> ?T"

(unable to find a well-typed instantiation for "?sub_sort": cannot ensure that

"Type@{max(Set,Equality.axiom.u0,Equality.type.u0,Finite.type.u0+1,pred.u0,rel.u0)}"

is a subtype of "Type@{subType.u0}").

at following this line:

Canonical perm_subType := Eval hnf in [subType for pval].

I get the same issue sometimes when I try to run code examples, because I don't start from exactly the same situation and it is not always 100% clear.

Fortunately the source code can serve as reference. In this case, the file coq-mathcomp-ssreflect.2.2.0/mathcomp/fingroup/perm.v

There is a slight difference between this source file and the example in the mathcomp book: the declaration of the variable T.

A possible code could be:

```
From mathcomp Require Import all_ssreflect.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit.
Inductive perm_of (T : finType) : Type :=
Perm (pval : {ffun T -> T}) & injectiveb pval.
Definition pval (T : finType) (p : perm_of T) := let: Perm f _ := p in f.
Notation "{ ’perm’ T }" := (perm_of T).
```

@grianneau Thanks for your reply, I just found to source file you mentioned.

And the code you give is same as this answer https://coq.zulipchat.com/#narrow/stream/237664-math-comp-users/topic/code.20snippets.20of.20section.207.2E6.20to.207.2E8/near/441196683

and it could work.

While the problems I newly met are:

- the source code could not work, is that the problem of the version of Coq (8.17) I used?
- the line

Canonical perm_subType := Eval hnf in [subType for pval].

following also report an error like https://coq.zulipchat.com/#narrow/stream/237664-math-comp-users/topic/code.20snippets.20of.20section.207.2E6.20to.207.2E8/near/441197799

and shall I start it from former sections? I've tried but have no change.

Oh yes Quentin provided this solution indeed.

I can usually play (in an interactive session) '.v' source files that are shipped with my opam install.

I'm currently using Coq 8.19.1 and can play ~/.opam/test/.opam-switch/.opam-switch/sources/coq-mathcomp-ssreflect.2.2.0/mathcomp/fingroup/perm.v

The name of my switch here is 'test' and it is the one currently set in the environment.

I had to install fingroup, otherwise both imports of fingroup and morphism fail.

I cannot find `perm_subType`

in the source code. Still the question remains how to make the `Canonical`

command work. I wonder whether such commands are going to be completely replaced by HB.

Strange it is, could the problem placing here be solved?

With Coq 8.19.1, I see no use of `subType for`

except in test-suite/prerequisite/ssr_mini_mathcomp.v

Now I'm wondering which version of Coq one is supposed to use to make the code examples from the book to work.

I can see that the syntax `[subType for`

is still in use for the version 8.14.1.

With Coq 8.14.1 (and OCaml 4.14.2) the following piece of code works:

```
From mathcomp Require Import all_ssreflect.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit.
Inductive perm_of (T : finType) : Type :=
Perm (pval : {ffun T -> T}) & injectiveb pval.
Definition pval (T : finType) (p : perm_of T) := let: Perm f _ := p in f.
Notation "{ ’perm’ T }" := (perm_of T).
Canonical perm_subType (T : finType) := Eval hnf in [subType for (@pval T)].
```

One may try to follow more strictly the code of the book with an older version of Coq. One may prefer to use a more recent version of Coq and replace some parts of the code examples with new code - probably using HB.

Unfortunately we did not port the book to HB yet.

The code you gave here also could work at my Coq 8.17 platform.

There are some code after that still report

```
The reference perm_type was not found in the current environment.
```

And I can't solve that with adding `(T : finType)`

simply. Is the older version still support that?

Thanks!

grianneau said:

I can see that the syntax

`[subType for`

is still in use for the version 8.14.1.With Coq 8.14.1 (and OCaml 4.14.2) the following piece of code works:

`From mathcomp Require Import all_ssreflect. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit. Inductive perm_of (T : finType) : Type := Perm (pval : {ffun T -> T}) & injectiveb pval. Definition pval (T : finType) (p : perm_of T) := let: Perm f _ := p in f. Notation "{ ’perm’ T }" := (perm_of T). Canonical perm_subType (T : finType) := Eval hnf in [subType for (@pval T)].`

One may try to follow more strictly the code of the book with an older version of Coq. One may prefer to use a more recent version of Coq and replace some parts of the code examples with new code - probably using HB.

Thank you for the information about Coq 8.17. I just tried my luck with some older versions but I don't know the latest versions that one could use.

Following the code of the book, I get the error:

`Error: The reference perm_type was not found in the current environment.`

In the source file one can see that the definition of `perm_type`

is purposely duplicated (for some reasons) to `perm_of`

. I cannot see any definition of `perm_type`

in the book.

I would rather refer to the source code (corresponding to current version of Coq) to start from a working code in an interactive session and experiment from there.

Thanks, it may be a generic question, and other sections could also work if it is solved.

As I said the book has not been ported to recent MC, bit the sources of the library yes.

Here a link to perm, as you can see it is similar but one uses HB is order to declare instances in a more compact way:

https://github.com/math-comp/math-comp/blob/6a2791d233a529d7d11d697e917669bbd26cb545/mathcomp/fingroup/perm.v#L45

I see, I just have no idea about how to change the code into HB strucutre. Maybe I could use former MC, which version of Coq and MC shall I use?

MC 1.x should do. HB was introduced in MC 2.0

When using Coq 8.14.1, opam installed coq-mathcomp-ssreflect 1.16.0, finmap 1.5.2 and fingroup 1.16.0. That's what I used to run the code. I hope you can get versions working with Coq 8.17.

I've tried MC 1.16.0 with Coq 8.14.1 and got the same result, perhaps it is not the problem of HB, because HB doesn't use in MC 1.16.0?

If one uses a recent MC then it goes with HB. Otherwise one can use some older version of MC - which is without HB - and try to run the code from the current version of the MC book (which does not use HB).

One can examine the source code and see whether it uses some specific syntax (such

as `[subType for`

) as in the book or whether it uses HB.

Thanks for your notices.

Well, it is exactly what I did, whatever the MC 2.2.0 or 1.16.0 I tried could not have the correct output of the following part of section 7.6. So I guess it is not the reason HB that cause the problem.

Is it difficult to update these section with the latest library? I think it may easier than find solutions through all of these versions.

There is a tutorial on porting to MC2: https://github.com/math-comp/math-comp/tree/master/etc/porting_to_mathcomp2

The reason the book hasn't been ported yet is not so much the code but rather the text that needs a serious overhaul with the simplification bring by hierarchy-builder.

From sections 7.6 to 7.8, the current version of the book uses code from files finset.v, perm.v and matrix.v.

It's a code extract that is also slightly modified, hiding some technical details such as the use of `Phant`

.

One can run each of the three files entirely and focus more on the parts that correspond to the code extracts in the book.

To be able to do this I also installed:

- fingroup to be able to import fingroup and morphism
- algebra to be able to import ssralg, finalg, zmodp and countalg.

I hope this helps.

Note that, idependently of HB, there is no more Phant now. That's another simplification that requires work in the book.

Thanks, but it's still not solved yet.

Section 7.2 seems similar to section 7.7, and doesn't use `Equality`

to replace `eqMixin`

as the tutorial said.

I has imported `all_ssreflect`

and something else at the beginning, I guess there is no other package requirement.

And so do other sections like 7.3 7.4.

I don't know which versions of Coq and MC are the closest to the code of the book 1.0.2.

It seems that the code of 8.14.1 is closer to the book than 8.17.

It could help to share the first encountered problem with the code of the section 7.2.

One can find that the code is related to tuple.v and run this file step-by-step in an interactive session.

Section 7.2 doesn't have any problem yet, because the code snippet of it has been updated. What I mean is both section 7.2 and section 7.7 have similar structure in the book, like

```
Canonical tuple_subType := [subType for tval].
Definition tuple_eqMixin := [eqMixin of n.-tuple T by <:].
Canonical tuple_eqType := EqType (n.-tuple T) tuple_eqMixin
```

in section 7.2, and

```
Canonical perm_subType := Eval hnf in [subType for pval].
Definition perm_eqMixin := Eval hnf in [eqMixin of perm_type by <:].
Canonical perm_eqType := Eval hnf in EqType perm_type perm_eqMixin.
Definition perm_finMixin := [finMixin of perm_type by <:].
Canonical perm_finType := Eval hnf in FinType perm_type perm_finMixin.
```

in section 7.7.

And I guess the code snippets in section 7.7 could work if it updated as what section 7.2 did, while just a deduction.

At worst you can just look into the source file https://github.com/math-comp/math-comp/blob/mathcomp-1/mathcomp/ssreflect/tuple.v (branch mathcomp_1 or branch master) to see what the real code looks like (it might just be a bit more complicated than the version in the book).

Thanks @Pierre Roux , it is indeed a little bit more complicated, and I will take some time to understand it along with the finset.v, perm.v as @grianneau mentioned.

And also expect the book and code snipptets would be coming soon.

Well, no one found time to update the book since MC2 release in May 2023 and AFAIK no one is currently working on it, so that may require quite a bit more waiting.

I see...

Last updated: Jul 25 2024 at 15:02 UTC