Cleanup phantom types #1046

proux01 · 2023-07-04T16:38:07Z

Motivation for this change

Cleanup phantom types now that reverse coercions make them useless.

We probably want to wait for 8.18 to be out before merging this, in order to get a better interactive experience with nicer printing.

Things done/to do

added corresponding entries in CHANGELOG_UNRELEASED.md

added corresponding documentation in the headers
tried to abide by the contribution guide

Compatibility with MathComp 1.X

I added the label TODO: MC-1 port to make sure someone ports this PR to
the mathcomp-1 branch or I already opened an issue or PR (please cross reference). (while this would be possible, I'm not sure we want to backport that)

Automatic note to reviewers

Read this Checklist and put a milestone if possible.

Overlays (to be merged before the current PR)

CohenCyril · 2023-07-05T07:00:29Z

I agree for merging this only with 8.18...
Maybe we want to keep the old notations with a deprecation as well?

proux01 · 2023-07-05T07:09:14Z

I agree for merging this only with 8.18...

Note that we should also remove phantoms in HB itself.
I should also benchmarks this to check there is no performance regression (but I'd rather wait for the situation to have stabilized on the Elpi/HB front here).

Maybe we want to keep the old notations with a deprecation as well?

That's what the current PR does, the notations remain as parsing only and are deprecated.

proux01 · 2023-07-09T09:13:18Z

Some benchmarks:

Coq without improved printing of reverse coercions (V8.19+alpha aaaf8994b0), mathcomp master (1e6f7e5): 25:43
Coq with improved printing of reverse coercions (aaaf8994b0), mathcomp master (1e6f7e5): 27:28
Coq with improved printing of reverse coercions (aaaf8994b0), mathcomp this branch (498bb9f): 26:24

(common to all three: coq-elpi coq-master + merge master (8be42fa), HB coq-master + batch-accumulation (6d81cdf))

So there doesn't seem to be any dramatic slowdown.

This should be backward compatible

pi8027 · 2023-11-14T12:41:06Z

Do you have any blockers in merging this PR? (Just asking because I wanted to do the same for multinomials.)

proux01 · 2023-11-14T12:43:36Z

We were waiting for 8.18 to be out (because printing is only reasonnable since 8.18) but it should be good now, I guess it's just a matter of rebasing and merging, let's discuss this during the next meeting.

This should be backward compatible

Adapt to math-comp/math-comp#1046

mathcomp/fingroup/perm.v

pi8027 · 2023-11-29T14:33:54Z

@proux01 Do you think this PR is ready for review modulo CI? If so, I will try to review it (since I need this PR to be merged before starting #1128).

proux01 · 2023-11-29T14:40:58Z

@pi8027 yes, I'm just fixing the changelog (and waiting for CI) before clicking on Ready for review but it can already be reviewed.

pi8027 · 2023-11-29T14:48:07Z

mathcomp/algebra/finalg.v

@@ -324,12 +322,13 @@ End UnitsGroup.

 Module Import UnitsGroupExports.
 Bind Scope group_scope with unit_of.
+Arguments unit_of R%type.


In the presence of reverse coercions, I think it makes sense to do

Bind Scope type_scope with finUnitRingType.

(and the same for every structure whose carrier is a Type).

Then we can get rid of this kind of Arguments declarations (but it can be done in a separate PR).

I agree, let's do that in another PR.
In fact, we should probably implement this in HB rather than putting Bind Scope manually everywhere. Cc @CohenCyril

If we do this systematically, the rule of thumb would be that a structure should inherit the Bind Scope declaration from the carrier. For example, a morphism structure should inherit it from its carrier _ -> _ (whose scope is fun(ction)_scope).

Yes, there are already three cases in HB depending on coercion class of the key (SortClass, FunClass and globref), this should guide the binding (to type_scope, fun_scope and ? respectively).

I'm taking care of doing this by hand.

Well, if the interface for binding scopes exists in coq-elpi, it's probably just as easy to improve HB.

mathcomp/algebra/fraction.v

mathcomp/algebra/poly.v

mathcomp/algebra/qpoly.v

mathcomp/algebra/ssralg.v

mathcomp/algebra/vector.v

mathcomp/solvable/alt.v

mathcomp/ssreflect/finset.v

mathcomp/algebra/qpoly.v

mathcomp/algebra/vector.v

pi8027 · 2023-11-29T16:29:32Z

mathcomp/character/classfun.v

@@ -1580,7 +1580,7 @@ Definition cfIsom :=
  locked_with cfIsom_key (cfMorph \o 'Res[G1] : 'CF(G) -> 'CF(R)).
 Canonical cfIsom_unlockable := [unlockable of cfIsom].

-Lemma cfIsomE phi x : x \in G -> cfIsom phi (f x) = phi x.
+Lemma cfIsomE phi (x : aT : finType) : x \in G -> cfIsom phi (f x) = phi x.


Why do you need : finType here?

I don't remember the details but it's needed to keep the type of the lemma unchanged (otherwise, we get x : aT whereas it was x : finGroupType_to_finType aT before removing the phantoms).

strange that finGroupType_to_finType is displayed ... we should investigate (we can merge first and investigate later)

mathcomp/field/falgebra.v

mathcomp/field/fieldext.v

mathcomp/algebra/qpoly.v

mathcomp/algebra/ring_quotient.v

mathcomp/ssreflect/order.v

mathcomp/ssreflect/generic_quotient.v

pi8027

A few questions are left (see my review comments above), but any of them can be addressed in a separate PR. So, this PR seems good enough to merge.

pi8027 · 2023-11-30T15:26:05Z

@proux01 @CohenCyril Shall we merge this one?

CohenCyril

@proux01 amazing work, thank you.

proux01 · 2023-11-30T15:35:35Z

Thanks @pi8027 for the careful review!

proux01 · 2023-11-30T15:39:39Z

Note about the odd-order overlay: math-comp/odd-order#52 it required the addition of a few rewrite patterns, They looked like the usual issue with rewrite not selecting the first occurence, as already encountered when porting MC to HB (for instance with associativity lemmas).

proux01 · 2023-11-30T15:41:37Z

About the CoqEAL overlay: there was some strange exploit of the duplicated phantom canonical instances, this seems to hint to the fact that the dvdRing structure there should be included in the main MC algebraic hierarchy, which would hopefully avoid that terrible hack.

proux01 added kind: clean-up This issure/PR is about cleaning up obsolete code, removing hacks, etc needs: coq 8.18 labels Jul 4, 2023

proux01 force-pushed the hierarchy-builder-rev_coerce branch from 37390a3 to 498bb9f Compare July 4, 2023 23:18

proux01 force-pushed the hierarchy-builder-rev_coerce branch from 498bb9f to c37f71f Compare July 18, 2023 14:37

proux01 force-pushed the hierarchy-builder-rev_coerce branch from c37f71f to 094f9ca Compare September 13, 2023 11:49

proux01 force-pushed the hierarchy-builder-rev_coerce branch from 094f9ca to 91379dd Compare October 3, 2023 09:11

proux01 added a commit to proux01/multinomials that referenced this pull request Oct 5, 2023

Adapt to math-comp/math-comp#1046

f5d7542

This should be backward compatible

proux01 force-pushed the hierarchy-builder-rev_coerce branch from 91379dd to f506320 Compare November 21, 2023 14:05

proux01 added a commit to coq-community/reglang that referenced this pull request Nov 22, 2023

Adapt to math-comp/math-comp#1046

4f16eda

proux01 mentioned this pull request Nov 22, 2023

Adapt to https://github.com/math-comp/math-comp/pull/1046 coq-community/reglang#66

Merged

palmskog pushed a commit to coq-community/reglang that referenced this pull request Nov 22, 2023

Adapt to math-comp/math-comp#1046 (#66)

897778d

proux01 added a commit to proux01/multinomials that referenced this pull request Nov 24, 2023

Adapt to math-comp/math-comp#1046

27a304a

This should be backward compatible

proux01 force-pushed the hierarchy-builder-rev_coerce branch 2 times, most recently from 9962404 to b51c39c Compare November 27, 2023 13:09

pi8027 mentioned this pull request Nov 27, 2023

Refactor qpoly and poly #1128

Open

proux01 force-pushed the hierarchy-builder-rev_coerce branch 2 times, most recently from 1e903ad to ddea82e Compare November 28, 2023 09:13

proux01 added a commit to math-comp/odd-order that referenced this pull request Nov 29, 2023

Adapt to math-comp/math-comp#1046

3a97b71

This was referenced Nov 29, 2023

Adapt to https://github.com/math-comp/math-comp/pull/1046 math-comp/odd-order#52

Merged

Adapt to https://github.com/math-comp/math-comp/pull/1046 math-comp/multinomials#85

Merged

proux01 added a commit to math-comp/odd-order that referenced this pull request Nov 29, 2023

Adapt to math-comp/math-comp#1046

3686ed8

proux01 added a commit to math-comp/odd-order that referenced this pull request Nov 29, 2023

Merge pull request #52 from math-comp/mc_1046

8dbbae0

Adapt to math-comp/math-comp#1046

proux01 force-pushed the hierarchy-builder-rev_coerce branch from ddea82e to 90b9b58 Compare November 29, 2023 14:01

pi8027 added a commit to math-comp/multinomials that referenced this pull request Nov 29, 2023

Merge pull request #85 from proux01/mc_1046

9893f5f

Adapt to math-comp/math-comp#1046

pi8027 reviewed Nov 29, 2023

View reviewed changes

mathcomp/fingroup/perm.v Outdated Show resolved Hide resolved

proux01 force-pushed the hierarchy-builder-rev_coerce branch 2 times, most recently from 365f200 to e4718ec Compare November 29, 2023 14:24

pi8027 reviewed Nov 29, 2023

View reviewed changes

Remove phantom in poly

ea18b9a

proux01 force-pushed the hierarchy-builder-rev_coerce branch from e4718ec to 5128a91 Compare November 29, 2023 15:34

proux01 marked this pull request as ready for review November 29, 2023 15:37

pi8027 reviewed Nov 29, 2023

View reviewed changes

proux01 force-pushed the hierarchy-builder-rev_coerce branch from 5128a91 to 475c9f7 Compare November 30, 2023 09:05

proux01 added 4 commits November 30, 2023 12:19

Remove some phant in ssreflect and fingroup

1c2d5a9

Remove some phant in algebra

5d6e6b5

Remove some phant in solvable

027efa5

Remove some phant in field

c78ea08

proux01 force-pushed the hierarchy-builder-rev_coerce branch from 475c9f7 to c78ea08 Compare November 30, 2023 11:20

pi8027 approved these changes Nov 30, 2023

View reviewed changes

CohenCyril approved these changes Nov 30, 2023

View reviewed changes

pi8027 merged commit 28837b1 into master Nov 30, 2023
149 checks passed

proux01 deleted the hierarchy-builder-rev_coerce branch November 30, 2023 15:35

pi8027 mentioned this pull request Dec 8, 2023

Bind Scope declarations for structure record types #1136

Open

proux01 mentioned this pull request Jan 11, 2024

Adapt to https://github.com/math-comp/math-comp/pull/1046 coq-community/coqeal#84

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Cleanup phantom types #1046

Cleanup phantom types #1046

proux01 commented Jul 4, 2023 •

edited

Loading

CohenCyril commented Jul 5, 2023

proux01 commented Jul 5, 2023

proux01 commented Jul 9, 2023

pi8027 commented Nov 14, 2023

proux01 commented Nov 14, 2023

pi8027 commented Nov 29, 2023 •

edited

Loading

proux01 commented Nov 29, 2023

pi8027 Nov 29, 2023

proux01 Nov 29, 2023

pi8027 Nov 29, 2023

proux01 Nov 30, 2023

pi8027 Nov 30, 2023

proux01 Nov 30, 2023

pi8027 Nov 29, 2023

proux01 Nov 30, 2023

CohenCyril Nov 30, 2023

pi8027 left a comment •

edited

Loading

pi8027 commented Nov 30, 2023

CohenCyril left a comment

proux01 commented Nov 30, 2023

proux01 commented Nov 30, 2023

proux01 commented Nov 30, 2023

Cleanup phantom types #1046

Cleanup phantom types #1046

Conversation

proux01 commented Jul 4, 2023 • edited Loading

Motivation for this change

Things done/to do

Compatibility with MathComp 1.X

Automatic note to reviewers

Overlays (to be merged before the current PR)

CohenCyril commented Jul 5, 2023

proux01 commented Jul 5, 2023

proux01 commented Jul 9, 2023

pi8027 commented Nov 14, 2023

proux01 commented Nov 14, 2023

pi8027 commented Nov 29, 2023 • edited Loading

proux01 commented Nov 29, 2023

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

pi8027 left a comment • edited Loading

Choose a reason for hiding this comment

pi8027 commented Nov 30, 2023

CohenCyril left a comment

Choose a reason for hiding this comment

proux01 commented Nov 30, 2023

proux01 commented Nov 30, 2023

proux01 commented Nov 30, 2023

proux01 commented Jul 4, 2023 •

edited

Loading

pi8027 commented Nov 29, 2023 •

edited

Loading

pi8027 left a comment •

edited

Loading