Skip to content

[coercions] Remove uniform inheritance condition#15789

Merged
coqbot-app[bot] merged 6 commits intorocq-prover:masterfrom
proux01:coercions-no-uniform-cond
Mar 15, 2022
Merged

[coercions] Remove uniform inheritance condition#15789
coqbot-app[bot] merged 6 commits intorocq-prover:masterfrom
proux01:coercions-no-uniform-cond

Conversation

@proux01
Copy link
Copy Markdown
Contributor

@proux01 proux01 commented Mar 10, 2022 •
edited
Loading

This follows a discussion on Zulip: https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Identity.20Coercions
This removes the uniform inheritance condition by using inference (mostly unification, but also canonical structures or typeclasses) to obtain the parameters of coercions.

  • Added / updated test-suite.
  • Added changelog.
  • Added / updated documentation.

Will conflict with #15693 I could rebase whichever is not merged first.

Overlay (should be merged before merging the current PR):

@proux01 proux01 added part: coercions The coercion mechanism. kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. kind: fix This fixes a bug or incorrect documentation. needs: changelog entry This should be documented in doc/changelog. needs: documentation Documentation was not added or updated. labels Mar 10, 2022
@proux01 proux01 force-pushed the coercions-no-uniform-cond branch 2 times, most recently from 5834e84 to 5ce958e Compare March 10, 2022 19:21
proux01 added a commit to proux01/UniMath that referenced this pull request Mar 11, 2022
@proux01
Adapt to rocq-prover/rocq#15789
41cc0bb
proux01 added a commit to proux01/UniMath that referenced this pull request Mar 11, 2022
@proux01
Adapt to rocq-prover/rocq#15789
dd0a667
@proux01 proux01 force-pushed the coercions-no-uniform-cond branch from 5ce958e to fc1eec1 Compare March 11, 2022 11:59
proux01 added a commit to proux01/UniMath that referenced this pull request Mar 11, 2022
@proux01
Adapt to rocq-prover/rocq#15789
25ecf82
This was referenced Mar 11, 2022
Merged
Closed
@Alizter
Copy link
Copy Markdown
Contributor

Alizter commented Mar 11, 2022 •
edited
Loading

Some more:

I have the tests written up, I can push here if you like.

@proux01 proux01 changed the title [coercions] Remove uniform inheritance condition? [coercions] Remove uniform inheritance condition Mar 11, 2022
@proux01
Copy link
Copy Markdown
Contributor Author

proux01 commented Mar 11, 2022

Great, feel free to push

@gares
Copy link
Copy Markdown
Member

gares commented Mar 11, 2022

Please start a bench job from the gitlab pipeline interface and post here the link to the job. If you can't we shall give you rights.

@gares gares self-assigned this Mar 11, 2022
@gares gares added this to the 8.16+rc1 milestone Mar 11, 2022
@Alizter
Copy link
Copy Markdown
Contributor

Alizter commented Mar 11, 2022 •
edited
Loading

For reference all those bugs I mentioned are definitely fixed by this patch and not on master.

@gares
Copy link
Copy Markdown
Member

gares commented Mar 11, 2022

Bench @ https://gitlab.com/coq/coq/-/jobs/2192741710

@proux01 proux01 removed needs: documentation Documentation was not added or updated. needs: changelog entry This should be documented in doc/changelog. labels Mar 11, 2022
gares
gares approved these changes Mar 11, 2022
View reviewed changes
Copy link
Copy Markdown
Member

@gares gares left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Amazing!

@gares
Copy link
Copy Markdown
Member

gares commented Mar 11, 2022 •
edited
Loading

@pi8027 IIRC you had a use case for the uniform inheritance check in the context of packed classes. I believe this PR makes the need to obey the condition (in all contexts, not just packed classes) go away, but it may still be useful to know when the condition is not met (in the contexts where it makes sense).

Is this right, or my memory fails? If I'm right then one may want to be able to turn on the warning manually.

benediktahrens added a commit to UniMath/UniMath that referenced this pull request Mar 11, 2022
@benediktahrens
Merge pull request #1469 from proux01/adapt_coq_15789
59a11fb 
Adapt to rocq-prover/rocq#15789
@gares
Copy link
Copy Markdown
Member

gares commented Mar 11, 2022

@proux01 can you explain here how the failures in CI did manifest? I'd like to understand them, and see if we can add something to help other users understand what failed (if hard to grasp).

@proux01 proux01 added the needs: squashing Some commits should be squashed together. label Mar 12, 2022
@Alizter
Copy link
Copy Markdown
Contributor

Alizter commented Mar 12, 2022

Bench results 
┌─────────────────────────────┬─────────────────────────┬───────────────────────────────────────┬───────────────────────────────────────┬─────────────────────────┬───────────────────┐
│                             │      user time [s]      │              CPU cycles               │           CPU instructions            │  max resident mem [KB]  │    mem faults     │
│                             │                         │                                       │                                       │                         │                   │
│                package_name │     NEW      OLD  PDIFF │            NEW             OLD  PDIFF │            NEW             OLD  PDIFF │     NEW      OLD  PDIFF │ NEW  OLD    PDIFF │
├─────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼───────────────────┤
│                    coq-core │  105.58   106.89  -1.23 │   392735110621    388398300936   1.12 │   441715216451    441972174919  -0.06 │  276572   278144  -0.57 │   2    0      nan │
│                   coq-color │  215.47   216.39  -0.43 │   935834531120    938233550599  -0.26 │  1328188437470   1328131254620   0.00 │ 1152480  1150812   0.14 │   0   23  -100.00 │
│         coq-metacoq-erasure │   65.76    66.02  -0.39 │   282290439839    283793668748  -0.53 │   433491040321    433479465742   0.00 │ 1109776  1108952   0.07 │   0    0      nan │
│              coq-verdi-raft │  576.01   578.17  -0.37 │  2516009058568   2524783318183  -0.35 │  3928281145473   3928539741161  -0.01 │ 1261676  1261804  -0.01 │   0    0      nan │
│                  coq-stdlib │  413.07   414.56  -0.36 │  1487180478677   1491158223461  -0.27 │  1417612518035   1427275586501  -0.68 │  605000   609124  -0.68 │   0    0      nan │
│               coq-perennial │ 4090.30  4104.58  -0.35 │ 17885172004506  17949216154087  -0.36 │ 29784432258092  29768743692079   0.05 │ 2627720  2611332   0.63 │   0    0      nan │
│                  coq-geocoq │  717.04   719.44  -0.33 │  3128933887865   3142664278018  -0.44 │  4990981962857   4990798191609   0.00 │ 1077980  1080152  -0.20 │   3    0      nan │
│                coq-bedrock2 │  226.12   226.86  -0.33 │   988546495874    990956049804  -0.24 │  1795564516173   1794891701626   0.04 │ 2052004  2051988   0.00 │  40   20   100.00 │
│              coq-coquelicot │   34.41    34.52  -0.32 │   148670988643    148522976930   0.10 │   196775085065    196740783063   0.02 │  757304   758036  -0.10 │  83    0      nan │
│  coq-performance-tests-lite │  798.72   800.81  -0.26 │  3476705863907   3486023389349  -0.27 │  5942981804958   5944814495916  -0.03 │ 1826544  1826280   0.01 │   3    0      nan │
│      coq-mathcomp-character │   69.21    69.39  -0.26 │   302686018463    303663938174  -0.32 │   465784266068    463934414558   0.40 │  824196   827716  -0.43 │   0    0      nan │
│ coq-rewriter-perf-SuperFast │  958.33   960.52  -0.23 │  4187862413238   4198135178546  -0.24 │  7266666546354   7268269901301  -0.02 │ 1147084  1146796   0.03 │   4    0      nan │
│               coq-fiat-core │   57.02    57.15  -0.23 │   235581122390    235305416191   0.12 │   332646293950    332663808422  -0.01 │  481400   481344   0.01 │   2    0      nan │
│             coq-fiat-crypto │ 2899.93  2906.22  -0.22 │ 12652494380418  12680320951568  -0.22 │ 23219998245681  23232362004925  -0.05 │ 3849464  3849508  -0.00 │  97   99    -2.02 │
│                  coq-flocq3 │   78.72    78.89  -0.22 │   343118516195    344197866677  -0.31 │   457090441460    457030261410   0.01 │  991372   990932   0.04 │ 129    0      nan │
│            coq-math-classes │   92.92    93.12  -0.21 │   403426869085    403863096506  -0.11 │   571498667565    571473052868   0.00 │  502524   501932   0.12 │   0    0      nan │
│        coq-mathcomp-algebra │   60.26    60.36  -0.17 │   263231472432    263535205393  -0.12 │   362644589718    361741252762   0.25 │  596144   595372   0.13 │   0    0      nan │
│          coq-mathcomp-field │  101.84   101.98  -0.14 │   446271479079    446826200395  -0.12 │   740919765800    739019482204   0.26 │  709700   706012   0.52 │   0    0      nan │
│     coq-metacoq-safechecker │  202.92   203.16  -0.12 │   884477783600    885820683888  -0.15 │  1202886384686   1203313909690  -0.04 │ 1221308  1232708  -0.92 │   3    2    50.00 │
│           coq-iris-examples │  424.61   425.00  -0.09 │  1852960627432   1855194173056  -0.12 │  2839952803989   2839685488579   0.01 │ 1182624  1182280   0.03 │   0    0      nan │
│       coq-engine-bench-lite │  181.60   181.75  -0.08 │   763284430953    764410145130  -0.15 │  1491340451064   1492679789561  -0.09 │ 1234748  1357668  -9.05 │   0    0      nan │
│        coq-metacoq-template │   79.28    79.33  -0.06 │   339589744082    339878522220  -0.08 │   513915299650    513913794871   0.00 │  911172   914676  -0.38 │  11    4   175.00 │
│                coq-compcert │  289.00   289.15  -0.05 │  1256911796342   1257333590731  -0.03 │  1889643116908   1889660062773  -0.00 │ 1104904  1104876   0.00 │   0    9  -100.00 │
│    coq-metacoq-translations │   20.60    20.61  -0.05 │    89143839256     89174164927  -0.03 │   157028516963    156970606348   0.04 │  969832   973948  -0.42 │   0    0      nan │
│                 coq-unimath │ 4437.68  4439.45  -0.04 │ 19430568624581  19441495429905  -0.06 │ 38983167068813  38986606837077  -0.01 │ 3258360  3268956  -0.32 │  10    1   900.00 │
│                coq-rewriter │  384.31   384.31   0.00 │  1677193664167   1677369983320  -0.01 │  2772785082005   2772041259136   0.03 │  982944  1060696  -7.33 │   5    9   -44.44 │
│         coq-category-theory │ 1737.99  1737.60   0.02 │  7612771979457   7609945912845   0.04 │ 15548914521843  15547385180679   0.01 │ 1469052  1469072  -0.00 │   0    0      nan │
│           coq-metacoq-pcuic │  735.37   735.13   0.03 │  3197718308144   3198314419088  -0.02 │  4666615761567   4660760529842   0.13 │ 1645640  1661304  -0.94 │  17    1  1600.00 │
│                    coq-corn │  781.37   780.53   0.11 │  3409889404869   3407670648818   0.07 │  5281731891047   5277864176479   0.07 │  877212   881204  -0.45 │   0    0      nan │
│               coq-fourcolor │ 1499.14  1495.51   0.24 │  6557739102617   6544122069633   0.21 │ 12068548974965  12066626496912   0.02 │  757456   757276   0.02 │   0    0      nan │
│                     coq-vst │ 1091.19  1087.91   0.30 │  4764168216397   4753635591590   0.22 │  7717098382015   7716450184896   0.01 │ 2139028  2140304  -0.06 │   2    0      nan │
│                   coq-verdi │   48.86    48.70   0.33 │   212027960083    211989545500   0.02 │   319130527984    319080477737   0.02 │  839160   840112  -0.11 │   0    0      nan │
│                coq-coqprime │   44.07    43.92   0.34 │   191103587859    190540573222   0.30 │   283469649242    283401850977   0.02 │  763648   761528   0.28 │   1    0      nan │
│                    coq-hott │  168.88   168.30   0.34 │   732766129350    731150049138   0.22 │  1163428643766   1160416011291   0.26 │  617548   618608  -0.17 │   0    0      nan │
│                 coq-bignums │   28.67    28.56   0.39 │   124716495402    124641942309   0.06 │   172004927751    172015780134  -0.01 │  471232   471276  -0.01 │   0    0      nan │
│            coq-fiat-parsers │  345.54   344.03   0.44 │  1488159988323   1483161957682   0.34 │  2455036766283   2454284157636   0.03 │ 2707516  2707512   0.00 │   8   11   -27.27 │
│       coq-mathcomp-solvable │   83.15    82.78   0.45 │   363469943214    362205696439   0.35 │   558580767889    555457597604   0.56 │  665272   700136  -4.98 │   0    0      nan │
│      coq-mathcomp-ssreflect │   25.67    25.54   0.51 │   111646237782    111395698465   0.22 │   140974438703    140574976192   0.28 │  537672   538628  -0.18 │   0    0      nan │
│                 coq-coqutil │   36.27    36.06   0.58 │   155625792022    155241082879   0.25 │   210177853551    210084148856   0.04 │  607456   605504   0.32 │   4    4     0.00 │
│       coq-mathcomp-fingroup │   22.23    22.07   0.72 │    96886209398     96702410448   0.19 │   141506669728    140274898838   0.88 │  486672   483656   0.62 │   0    0      nan │
│      coq-mathcomp-odd-order │  546.15   542.20   0.73 │  2392907826250   2376237728522   0.70 │  4100975093608   4065726686853   0.87 │ 1232480  1209972   1.86 │   0    0      nan │
└─────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴───────────────────────────────────────┴─────────────────────────┴───────────────────┘

Looks to me like no change.

@Alizter
Copy link
Copy Markdown
Contributor

Alizter commented Mar 12, 2022

I'm having a look at #9696 and there is an example there that doesn't quite work with this patch.

Axiom f : forall {A}, option (option A) -> list A.
(* Coq used to accept this with a warning... *)
Coercion f : option >-> list.
(* Coq used to fail here *)
Check (Some (Some 0) : list nat).
Illegal application: 
The term "@f" of type "forall A : Type, option (option A) -> list A"
cannot be applied to the terms
 "option nat" : "Set"
 "Some (Some 0)" : "option (option nat)"
The 2nd term has type "option (option nat)" which should be coercible to "option (option (option nat))".

So it seems to be an issue with implicit arguments in coercions. That is proposed to be fixed by #11327. I guess this patch correctly removes the warning, but doesn't solve the implicit arguments or incorrect documentation.

jfehrle
jfehrle reviewed Mar 14, 2022
View reviewed changes
Copy link
Copy Markdown
Member

@jfehrle jfehrle left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Wording suggestions

@proux01 proux01 force-pushed the coercions-no-uniform-cond branch from e6c574d to 9bc51fb Compare March 14, 2022 20:39
@herbelin
Copy link
Copy Markdown
Member

herbelin commented Mar 14, 2022

For the CI, you may ask a specialist of interpreting such results, but 1.7% for a total of 21s may just be noise. Good to see work on coercions in passing!

@proux01 proux01 force-pushed the coercions-no-uniform-cond branch from 9bc51fb to 1b00631 Compare March 14, 2022 21:43
@Alizter Alizter mentioned this pull request Mar 14, 2022
Open
jfehrle
jfehrle reviewed Mar 14, 2022
View reviewed changes
Copy link
Copy Markdown
Member

@jfehrle jfehrle left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

a few more suggestions

proux01 and others added 5 commits March 15, 2022 09:30
@proux01
Remove uniform inheritance condition for coercions
828bdda 
This removes the uniform inheritance condition by using
inference (mostly unification, but also canonical structures or
typeclasses) to obtain the parameters of coercions.
@Alizter @proux01
add rocq-prover#3115 rocq-prover#4593 rocq-prover#5222 to test-suite
c10a72e
@proux01
Add test for rocq-prover#9696
5f36b30
@proux01
Add changelog
a6634f8
@proux01
[refman] Use example in coercions chapter
0e0c6e0
@proux01 proux01 force-pushed the coercions-no-uniform-cond branch from 1b00631 to 0e0c6e0 Compare March 15, 2022 08:30
@gares
Copy link
Copy Markdown
Member

gares commented Mar 15, 2022

I did push two extra test file about TC and CS resolution which don't seem to be covered elsewhere. It works!

Alizter
Alizter reviewed Mar 15, 2022
View reviewed changes
Copy link
Copy Markdown
Contributor

@Alizter Alizter left a comment •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@gares This will fix the linter

@proux01
Copy link
Copy Markdown
Contributor Author

proux01 commented Mar 15, 2022

I did push two extra test file about TC and CS resolution which don't seem to be covered elsewhere. It works!

Indeed, this was not properly tested, thanks!

@proux01 proux01 force-pushed the coercions-no-uniform-cond branch from 3458c76 to 74812d2 Compare March 15, 2022 16:50
jfehrle
jfehrle approved these changes Mar 15, 2022
View reviewed changes
Copy link
Copy Markdown
Member

@jfehrle jfehrle left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good.

@gares
Copy link
Copy Markdown
Member

gares commented Mar 15, 2022

@coqbot merge now

@coqbot-app coqbot-app bot merged commit 36b23c1 into rocq-prover:master Mar 15, 2022
@proux01 proux01 deleted the coercions-no-uniform-cond branch March 15, 2022 20:38
@proux01 proux01 mentioned this pull request Mar 16, 2022
Merged
6 tasks
@proux01 proux01 mentioned this pull request Mar 24, 2022
Merged
3 tasks
Skantz pushed a commit to Skantz/UniMath that referenced this pull request Nov 12, 2022
@proux01 @Skantz
Adapt to rocq-prover/rocq#15789
cb5dac9
Skantz pushed a commit to Skantz/UniMath that referenced this pull request Nov 12, 2022
@benediktahrens @Skantz
Merge pull request UniMath#1469 from proux01/adapt_coq_15789
331908d 
Adapt to rocq-prover/rocq#15789
Skantz pushed a commit to Skantz/UniMath that referenced this pull request Nov 12, 2022
@proux01 @Skantz
Adapt to rocq-prover/rocq#15789
2e072c0
Skantz pushed a commit to Skantz/UniMath that referenced this pull request Nov 12, 2022
@benediktahrens @Skantz
Merge pull request UniMath#1469 from proux01/adapt_coq_15789
cd8f838 
Adapt to rocq-prover/rocq#15789
@m-lindgren m-lindgren mentioned this pull request Nov 20, 2022
Merged
Columbus240 added a commit to Columbus240/topology that referenced this pull request Aug 20, 2023
@Columbus240
[v8.16] Declare SubspaceTopology as coercion
eb12085 
This depends on coq v8.16 and is not usable on lower versions.

Relevant issues and PRs from the coq repo:
rocq-prover/rocq#15789, rocq-prover/rocq#15853, rocq-prover/rocq#4593, rocq-prover/rocq#3115
Columbus240 added a commit to Columbus240/topology that referenced this pull request Nov 19, 2023
@Columbus240
[v8.16] Declare SubspaceTopology as coercion
e977bb3 
This depends on coq v8.16 and is not usable on lower versions.

Relevant issues and PRs from the coq repo:
rocq-prover/rocq#15789, rocq-prover/rocq#15853, rocq-prover/rocq#4593, rocq-prover/rocq#3115
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@gares gares gares approved these changes

@Alizter Alizter Alizter left review comments

@jfehrle jfehrle jfehrle approved these changes

Assignees

@gares gares

Labels

kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. kind: fix This fixes a bug or incorrect documentation. part: coercions The coercion mechanism.

Projects

None yet

Milestone

8.16+rc1

7 participants

@proux01 @Alizter @gares @SkySkimmer @pi8027 @herbelin @jfehrle