Stream: math-comp users

Topic: code snippets of section 7.6 to 7.8


view this post on Zulip liuty (May 27 2024 at 14:39):

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.

view this post on Zulip liuty (May 29 2024 at 08:48):

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:

at the Definition pval ... line

view this post on Zulip Quentin VERMANDE (May 29 2024 at 08:59):

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.

view this post on Zulip liuty (May 29 2024 at 09:06):

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

view this post on Zulip grianneau (May 29 2024 at 11:08):

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

view this post on Zulip liuty (May 29 2024 at 11:32):

@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:

  1. the source code could not work, is that the problem of the version of Coq (8.17) I used?
  2. 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

view this post on Zulip liuty (May 29 2024 at 11:35):

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

view this post on Zulip grianneau (May 29 2024 at 13:35):

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

view this post on Zulip liuty (May 29 2024 at 13:54):

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

view this post on Zulip grianneau (May 29 2024 at 14:15):

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.

view this post on Zulip grianneau (May 29 2024 at 15:28):

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.

view this post on Zulip Enrico Tassi (May 29 2024 at 19:08):

Unfortunately we did not port the book to HB yet.

view this post on Zulip liuty (May 30 2024 at 06:48):

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.

view this post on Zulip grianneau (May 30 2024 at 07:19):

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.

view this post on Zulip liuty (May 30 2024 at 07:30):

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

view this post on Zulip Enrico Tassi (May 31 2024 at 07:42):

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

view this post on Zulip liuty (Jun 01 2024 at 04:54):

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?

view this post on Zulip Enrico Tassi (Jun 01 2024 at 06:38):

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

view this post on Zulip grianneau (Jun 01 2024 at 08:53):

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.

view this post on Zulip liuty (Jun 01 2024 at 13:11):

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?

view this post on Zulip grianneau (Jun 02 2024 at 08:38):

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.

view this post on Zulip liuty (Jun 02 2024 at 09:23):

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.

view this post on Zulip Pierre Roux (Jun 03 2024 at 08:52):

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

view this post on Zulip Pierre Roux (Jun 03 2024 at 08:54):

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.

view this post on Zulip grianneau (Jun 03 2024 at 09:34):

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:

view this post on Zulip Pierre Roux (Jun 03 2024 at 09:47):

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

view this post on Zulip liuty (Jun 04 2024 at 05:22):

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.

view this post on Zulip liuty (Jun 04 2024 at 05:30):

And so do other sections like 7.3 7.4.

view this post on Zulip grianneau (Jun 04 2024 at 09:56):

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.

view this post on Zulip liuty (Jun 06 2024 at 10:57):

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.

view this post on Zulip Pierre Roux (Jun 06 2024 at 11:05):

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

view this post on Zulip liuty (Jun 06 2024 at 11:38):

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.

view this post on Zulip Pierre Roux (Jun 06 2024 at 11:43):

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.

view this post on Zulip liuty (Jun 06 2024 at 11:48):

I see...


Last updated: Jul 25 2024 at 15:02 UTC