Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

UIP in SProp #10390

Merged
merged 2 commits into from
Jul 3, 2020
Merged

UIP in SProp #10390

merged 2 commits into from
Jul 3, 2020

Conversation

SkySkimmer
Copy link
Contributor

@SkySkimmer SkySkimmer commented Jun 17, 2019 •
edited
Loading

@SkySkimmer SkySkimmer added needs: progress Work in progress: awaiting action from the author. kind: feature New user-facing feature request or implementation. kind: documentation Additions or improvement to documentation. needs: squashing Some commits should be squashed together. part: kernel labels Jun 17, 2019
@JasonGross
Copy link
Member

It seems strange to me that UIP of sprop equality gives UIP of Prop equality. What causes this, and that does the HoTT flag disable?

@SkySkimmer SkySkimmer added the needs: overlay This is breaking external developments we track in CI. label Jun 18, 2019
@SkySkimmer
Copy link
Contributor Author

It seems strange to me that UIP of sprop equality gives UIP of Prop equality. What causes this, and that does the HoTT flag disable?

You can define f : eq a b -> seq a b and g : seq a b -> eq a b with g (f p) = p, then f p = f q by sprop so p = g (f p) = g (f q) = q

On second thought -indices-matter does what I want so there may be no need for a new flag, unless someone wants to have identities in Prop without UIP.

SkySkimmer added a commit to SkySkimmer/unicoq that referenced this pull request Jun 18, 2019
@SkySkimmer
Adapt to coq/coq#10390 (UIP in SProp)
c9d374c
SkySkimmer added a commit to SkySkimmer/Mtac2 that referenced this pull request Jun 18, 2019
@SkySkimmer
Adapt to coq/coq#10390 (UIP in SProp)
df131f2
SkySkimmer added a commit to SkySkimmer/coq-elpi that referenced this pull request Jun 18, 2019
@SkySkimmer
Adapt to coq/coq#10390 (UIP in SProp)
1e390be
SkySkimmer added a commit to SkySkimmer/Coq-Equations that referenced this pull request Jun 18, 2019
@SkySkimmer
Adapt to coq/coq#10390 (UIP in SProp)
dd999c5
SkySkimmer added a commit to SkySkimmer/paramcoq that referenced this pull request Jun 18, 2019
@SkySkimmer
Adapt to coq/coq#10390 (UIP in SProp)
202ffb1
SkySkimmer added a commit to SkySkimmer/relation-algebra that referenced this pull request Jun 18, 2019
@SkySkimmer
Adapt to coq/coq#10390 (UIP in SProp)
b99a9b7
SkySkimmer added a commit to SkySkimmer/coq-dpdgraph that referenced this pull request Jun 19, 2019
@SkySkimmer
Adapt to coq/coq#10390 (UIP in SProp)
526fd52
SkySkimmer added a commit to SkySkimmer/coqhammer that referenced this pull request Jun 19, 2019
@SkySkimmer
Adapt to coq/coq#10390 (UIP in SProp)
be4c47e
SkySkimmer added a commit to SkySkimmer/Coq-Equations that referenced this pull request Jun 19, 2019
@SkySkimmer
Adapt to coq/coq#10390 (UIP in SProp)
a2e70cd
@andres-erbsen-sifive
Copy link

as of before this change, was it not possible to prove that any two proofs of the same seq are equal? I thought the entire point of SProp was that proofs are convertible.

@SkySkimmer
Copy link
Contributor Author

as of before this change, was it not possible to prove that any two proofs of the same seq are equal? I thought the entire point of SProp was that proofs are convertible.

It was possible, however seq was a weaker statement than eq.

@SkySkimmer
Copy link
Contributor Author

SkySkimmer commented Jun 21, 2019 •
edited
Loading

Bench is not great https://ci.inria.fr/coq/view/benchmarking/job/benchmark-part-of-the-branch/734/console


┌────────────────────────┬─────────────────────────┬─────────────────────────────────────────────┬─────────────────────────────────────────────┬───────────────────────────────┬───────────────────────────┐
│                        │      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-math-classes │  217.95  217.78 +0.08 % │      608237830980      608025709972 +0.03 % │      767963442228      767142083146 +0.11 % │     513656     513664 -0.00 % │      44      20 +120.00 % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼───────────────────────────┤
│ coq-mathcomp-ssreflect │   40.05   39.98 +0.18 % │      110704560148      110343847162 +0.33 % │      133881431626      133185436518 +0.52 % │     521460     520372 +0.21 % │      12      61  -80.33 % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼───────────────────────────┤
│               coq-hott │  336.16  335.25 +0.27 % │      915707484558      911289006389 +0.48 % │     1386507853816     1383250690928 +0.24 % │     476528     476552 -0.01 % │     472     246  +91.87 % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼───────────────────────────┤
│               coq-corn │ 1460.44 1455.51 +0.34 % │     4077947090988     4063989423131 +0.34 % │     6025817695426     5999824371955 +0.43 % │     881296     892612 -1.27 % │       1      77  -98.70 % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼───────────────────────────┤
│  coq-mathcomp-fingroup │   51.52   51.31 +0.41 % │      143638102088      142987158250 +0.46 % │      186286998785      185151246638 +0.61 % │     562380     562364 +0.00 % │      91       7 +1200.00 % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼───────────────────────────┤
│            coq-unimath │ 3004.22 2987.81 +0.55 % │     8371779234380     8324420961898 +0.57 % │    14978391128021    14926910297261 +0.34 % │    3661112    3548824 +3.16 % │     596     466  +27.90 % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼───────────────────────────┤
│   coq-mathcomp-algebra │  165.24  164.28 +0.58 % │      460744687116      458405544290 +0.51 % │      568436352054      565186038301 +0.58 % │     610324     609732 +0.10 % │      16       0    +nan % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼───────────────────────────┤
│              coq-color │  700.91  696.49 +0.63 % │     1960553516237     1948374036995 +0.63 % │     2332796375755     2321810325889 +0.47 % │    1381808    1382560 -0.05 % │     235     234   +0.43 % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼───────────────────────────┤
│          coq-fourcolor │ 2179.05 2165.26 +0.64 % │     6074940722740     6039260202322 +0.59 % │    11370023210293    11351690128073 +0.16 % │     927424     927172 +0.03 % │       1       0    +nan % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼───────────────────────────┤
│          coq-fiat-core │  108.54  107.84 +0.65 % │      309380064126      308453045153 +0.30 % │      385840033002      384481201688 +0.35 % │     484716     484572 +0.03 % │     393     233  +68.67 % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼───────────────────────────┤
│       coq-fiat-parsers │  639.74  635.44 +0.68 % │     1789913199684     1777413182533 +0.70 % │     2699654563489     2683286163751 +0.61 % │    3211944    3231800 -0.61 % │     528     663  -20.36 % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼───────────────────────────┤
│             coq-sf-plf │   44.10   43.74 +0.82 % │      123468527172      122539141154 +0.76 % │      159273381757      158340314305 +0.59 % │     490660     481116 +1.98 % │      89      19 +368.42 % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼───────────────────────────┤
│ coq-mathcomp-character │  182.37  180.78 +0.88 % │      507721592740      503652180746 +0.81 % │      668129658478      662605779276 +0.83 % │     849088     842752 +0.75 % │       0      11 -100.00 % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼───────────────────────────┤
│         coq-coquelicot │   75.99   75.29 +0.93 % │      208921394288      207074100990 +0.89 % │      252618433700      250099281427 +1.01 % │     655308     653068 +0.34 % │     444     142 +212.68 % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼───────────────────────────┤
│  coq-mathcomp-solvable │  190.27  188.23 +1.08 % │      530873726286      525243270595 +1.07 % │      708748447234      700087577414 +1.24 % │     784452     786340 -0.24 % │       9      17  -47.06 % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼───────────────────────────┤
│            coq-bignums │   69.82   69.04 +1.13 % │      193949060348      192222374280 +0.90 % │      255073196451      252778170117 +0.91 % │     492912     491140 +0.36 % │     178     145  +22.76 % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼───────────────────────────┤
│         coq-verdi-raft │ 1334.70 1319.68 +1.14 % │     3723259698651     3681443829178 +1.14 % │     5034031140340     4986774689057 +0.95 % │    1812392    1811192 +0.07 % │       0       0    +nan % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼───────────────────────────┤
│              coq-flocq │  463.84  458.10 +1.25 % │     1291143096357     1274946705314 +1.27 % │     1780229475994     1773408957910 +0.38 % │    1163620    1161464 +0.19 % │     281      74 +279.73 % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼───────────────────────────┤
│     coq-mathcomp-field │  232.55  229.56 +1.30 % │      648248379216      640405481048 +1.22 % │      923173973096      913958664695 +1.01 % │     745700     746612 -0.12 % │       0      75 -100.00 % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼───────────────────────────┤
│        coq-fiat-crypto │ 3836.86 3782.08 +1.45 % │    10657622802812    10500105910583 +1.50 % │    16664231748892    16476051692552 +1.14 % │    2334020    2341364 -0.31 % │    1169     733  +59.48 % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼───────────────────────────┤
│        coq-lambda-rust │ 1560.58 1534.83 +1.68 % │     4351532492092     4277301311848 +1.74 % │     5750097885420     5658005580098 +1.63 % │    1488764    1526244 -2.46 % │       0       0    +nan % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼───────────────────────────┤
│             coq-geocoq │ 1970.90 1936.77 +1.76 % │     5499823659928     5406826395001 +1.72 % │     7913760965635     7827202355417 +1.11 % │    1253824    1253924 -0.01 % │     148     214  -30.84 % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼───────────────────────────┤
│ coq-mathcomp-odd-order │ 1469.70 1443.68 +1.80 % │     4097067845402     4023341181720 +1.83 % │     6945756642947     6865934126922 +1.16 % │    1263636    1252560 +0.88 % │     158      46 +243.48 % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼───────────────────────────┤
│              coq-verdi │  121.00  118.18 +2.39 % │      336327175254      329305412513 +2.13 % │      426214954771      417107005360 +2.18 % │     557236     559536 -0.41 % │       8       6  +33.33 % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼───────────────────────────┤
│ coq-fiat-crypto-legacy │ 6449.70 6270.40 +2.86 % │    17959570538672    17454770201690 +2.89 % │    29120223661135    28403347658290 +2.52 % │    2418956    2339932 +3.38 % │    1011    1243  -18.66 % │
└────────────────────────┴─────────────────────────┴─────────────────────────────────────────────┴─────────────────────────────────────────────┴───────────────────────────────┴───────────────────────────┘

@ejgallego
Copy link
Member

@SkySkimmer how about flambda ?

@SkySkimmer SkySkimmer removed the needs: squashing Some commits should be squashed together. label Jun 25, 2019
@SkySkimmer
Copy link
Contributor Author

@SkySkimmer how about flambda ?

Can you start the bench, I don't know how to get flambda in there.

@SkySkimmer SkySkimmer removed the needs: overlay This is breaking external developments we track in CI. label Jun 25, 2019
@SkySkimmer
Copy link
Contributor Author

Overlays rebased (mtac2 is missing Mtac2/Mtac2#272)

@coqbot
Copy link
Contributor

coqbot commented Jun 29, 2020

For your complete information, the following job in allow failure mode has failed: test-suite:4.12+trunk+dune

SkySkimmer added a commit to SkySkimmer/Mtac2 that referenced this pull request Jul 1, 2020
@SkySkimmer
Adapt to coq/coq#10390 (UIP in SProp)
49626a4
SkySkimmer added a commit to SkySkimmer/metacoq that referenced this pull request Jul 1, 2020
@SkySkimmer
Adapt to coq/coq#10390 (UIP in SProp)
9c0e9b9
SkySkimmer added a commit to SkySkimmer/relation-algebra that referenced this pull request Jul 1, 2020
@SkySkimmer
Adapt to coq/coq#10390 (UIP in SProp)
316c251
SkySkimmer added a commit to SkySkimmer/Coq-Equations that referenced this pull request Jul 1, 2020
@SkySkimmer
Adapt to coq/coq#10390 (UIP in SProp)
91b8e96
@XVilka
Copy link

XVilka commented Jul 2, 2020

Only one metacoq failure:

File "src/g_metacoq_safechecker.mlg", line 73, characters 6-261:
Warning 8: this pattern-matching is not exhaustive.
Here is an example of a case that is not matched:
UIP _
File "src/g_metacoq_safechecker.ml", line 1:
Error: Some fatal warnings were triggered (1 occurrences)
Command exited with non-zero status 2
src/g_metacoq_safechecker.cmx (real: 0.42, user: 0.08, sys: 0.02, mem: 34968 ko)
Makefile.plugin:667: recipe for target 'src/g_metacoq_safechecker.cmx' failed

SkySkimmer added a commit to SkySkimmer/metacoq that referenced this pull request Jul 2, 2020
@SkySkimmer
Adapt to coq/coq#10390 (UIP in SProp)
314a757
@SkySkimmer
Copy link
Contributor Author

All green!

@maximedenes maximedenes merged commit 3358163 into coq:master Jul 3, 2020
proux01 added a commit to coq-community/paramcoq that referenced this pull request Jul 3, 2020
@proux01
Merge pull request #36 from SkySkimmer/uip
9e3bbc9 
Adapt to coq/coq#10390 (UIP in SProp)
@SkySkimmer SkySkimmer deleted the uip branch July 3, 2020 09:04
ppedrot added a commit to unicoq/unicoq that referenced this pull request Jul 3, 2020
@ppedrot
Merge pull request #31 from SkySkimmer/uip
66178ea 
Adapt to coq/coq#10390 (UIP in SProp)
lukaszcz pushed a commit to lukaszcz/coqhammer that referenced this pull request Jul 3, 2020
@SkySkimmer @lukaszcz
Adapt to coq/coq#10390 (UIP in SProp)
fc47952
bors bot added a commit to Mtac2/Mtac2 that referenced this pull request Jul 3, 2020
@bors @SkySkimmer
Merge #216
ceeea47 
216: Adapt to coq/coq#10390 (UIP in SProp) r=Janno a=SkySkimmer



Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Janno added a commit to Mtac2/Mtac2 that referenced this pull request Jul 3, 2020
@Janno
Merge pull request #216 from SkySkimmer/uip
4166bcd 
Adapt to coq/coq#10390 (UIP in SProp)
@XVilka XVilka mentioned this pull request Jul 3, 2020
Open
ybertot added a commit to coq-community/coq-dpdgraph that referenced this pull request Jul 3, 2020
@ybertot
Merge pull request #66 from SkySkimmer/uip
f8985dc 
Adapt to coq/coq#10390 (UIP in SProp)
gares added a commit to LPCIC/coq-elpi that referenced this pull request Jul 3, 2020
@gares
Merge pull request #152 from SkySkimmer/uip
f2b6054 
Adapt to coq/coq#10390 (UIP in SProp)
SimonBoulier pushed a commit to MetaCoq/metacoq that referenced this pull request Jul 3, 2020
@SkySkimmer @SimonBoulier
Adapt to coq/coq#10390 (UIP in SProp)
44430c8
chdoc pushed a commit to damien-pous/relation-algebra that referenced this pull request Jul 5, 2020
Merge pull request #9 Adapt to coq/coq#10390 (UIP in SProp)
33f99fb
ejgallego pushed a commit to ejgallego/Mtac2 that referenced this pull request Jul 8, 2020
@SkySkimmer @ejgallego
Adapt to coq/coq#10390 (UIP in SProp)
36b1df6
beta-ziliani added a commit to unicoq/unicoq that referenced this pull request Aug 12, 2020
@beta-ziliani
Revert "Adapt to coq/coq#10390 (UIP in SProp)" to downgrade to 8.12
006601e 
This reverts commit dfd9d83.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@ejgallego ejgallego ejgallego left review comments

@maximedenes maximedenes maximedenes approved these changes

@Zimmi48 Zimmi48 Zimmi48 approved these changes

Assignees

@maximedenes maximedenes

Labels
kind: feature New user-facing feature request or implementation. part: kernel part: SProp Proof irrelevance and strict propositions.
Projects
None yet
Milestone
8.13+beta1
Development

Successfully merging this pull request may close these issues.
10 participants
@SkySkimmer @JasonGross @andres-erbsen-sifive @ejgallego @mattam82 @maximedenes @ppedrot @Zimmi48 @coqbot @XVilka