Turn class_of records into primitive records and get rid of the xclass idiom

[pi8027]

Motivation for this change

This PR redefines the class_of records as primitive records except for morphisms and finGroupType, and also removes the xclass idiom by following #462 (comment) by @ggonthier.

Fixes #544 and closes #546.

Things done/to do

• added corresponding entries in CHANGELOG_UNRELEASED.md (do not edit former entries)
• [ ] added corresponding documentation in the headers

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

[CohenCyril]

I am curious about the new performances...

[pi8027]

Yes. It will be nice to have benchmarks, including this commented out proof:

math-comp/mathcomp/field/fieldext.v

Lines 1584 to 1592 in c2e7bad

	(*Coq 8.3 processes this shorter proof correctly, but then crashes on Qed.
	In Coq 8.4 Qed takes about 18s.
	In Coq 8.7, everything seems to be all right *)
	(*
	Lemma Xirredp_FAdjoin' (F : fieldType) (p : {poly F}) :
	irreducible_poly p ->
	{L : fieldExtType F & Vector.dim L = (size p).-1 &
	{z | root (map_poly (in_alg L) p) z & <<1; z>>%VS = fullv}}.
	Proof.

[pi8027]

The source of CI failure seems to be coq/coq#9508 which has been fixed in coq/coq#9509. I see there is a possible fix, but since we are about to drop compatibility with Coq (< 8.10), I would rather stop supporting Coq 8.7 and 8.8.

[pi8027]

Here are some benchmarking results using Coq 8.12.0:

• MathComp master (c2e7bad)

  make test-suite  1072.06s user 20.45s system 99% cpu 18:19.47 total
  

• MathComp primitive-class-records (a4cb449)

  make test-suite  1004.05s user 21.26s system 99% cpu 17:12.96 total
  

• Odd order (689f07b) with MathComp master

  make  1323.96s user 11.20s system 99% cpu 22:24.46 total
  

• Odd order with MathComp primitive-class-records

  make  1318.69s user 11.22s system 99% cpu 22:18.43 total
  

So it seems that this PR improves the performance of conversion and/or inference regarding packed classes.

[CohenCyril]

Here are some benchmarking results using Coq 8.12.0:

• MathComp master (c2e7bad)

  make test-suite  1072.06s user 20.45s system 99% cpu 18:19.47 total
  

• MathComp primitive-class-records (a4cb449)

  make test-suite  1004.05s user 21.26s system 99% cpu 17:12.96 total
  

• Odd order (689f07b) with MathComp master

  make  1323.96s user 11.20s system 99% cpu 22:24.46 total
  

• Odd order with MathComp primitive-class-records

  make  1318.69s user 11.22s system 99% cpu 22:18.43 total
  

So it seems that this PR improves the performance of conversion and/or inference regarding packed classes.

I would rather say the benchmark does not reveal significant impact.
What about:

math-comp/mathcomp/field/fieldext.v

Lines 1584 to 1592 in c2e7bad

	(*Coq 8.3 processes this shorter proof correctly, but then crashes on Qed.
	In Coq 8.4 Qed takes about 18s.
	In Coq 8.7, everything seems to be all right *)
	(*
	Lemma Xirredp_FAdjoin' (F : fieldType) (p : {poly F}) :
	irreducible_poly p ->
	{L : fieldExtType F & Vector.dim L = (size p).-1 &
	{z | root (map_poly (in_alg L) p) z & <<1; z>>%VS = fullv}}.
	Proof.

?

[pi8027]

I would rather say the benchmark does not reveal significant impact.
What about:

math-comp/mathcomp/field/fieldext.v

Lines 1584 to 1592 in c2e7bad

	(*Coq 8.3 processes this shorter proof correctly, but then crashes on Qed.
	In Coq 8.4 Qed takes about 18s.
	In Coq 8.7, everything seems to be all right *)
	(*
	Lemma Xirredp_FAdjoin' (F : fieldType) (p : {poly F}) :
	irreducible_poly p ->
	{L : fieldExtType F & Vector.dim L = (size p).-1 &
	{z | root (map_poly (in_alg L) p) z & <<1; z>>%VS = fullv}}.
	Proof.

?

In Coq 8.12 and MathComp master, it takes 4.304 seconds. In this PR, it takes 3.284 seconds.

[CohenCyril]

Looks promising. I'm in favor of merging.

[CohenCyril]

@ggonthier do you agree?

[CohenCyril]

Since merging this PR will make us drop support for Coq < 8.9, I think it should be approved in the next meeting before being merged. But as for me, it's all good.

[pi8027]

Shall we merge?