feat: Add elaboration of elimination constraints #21417
Conversation
coqbot-app
bot
added
the
needs: full CI
github-actions
bot
added
the
needs: rebase
TDiazT
force-pushed
the
elab-elim-constraints
branch
2 times, most recently
from
a49439b to
a83f6ad
Compare
coqbot-app
bot
removed
the
needs: rebase
SkySkimmer
left a comment
SkySkimmer
left a comment
There was a problem hiding this comment.
With the current syntax @{|+} means allow both extra level constraints and extra elimination constraints, I wonder if we should have some way to allow one but not the other.
test-suite/output/bug_16219.out
Outdated
| because strict proofs can be eliminated only to build strict proofs. | ||
| The quality constraints are inconsistent: cannot enforce SProp -> Type | ||
| because it would identify Type and SProp which is inconsistent. | ||
| This is introduced by the constraints SProp -> Type |
There was a problem hiding this comment.
this seems a bit verbose (repeating "SProp -> Type")
Maybe it's less redundant when transitive constraints are involved? We don't seem to have an output test involving transitive constraints.
If so then maybe we could avoid the repetition when transitivity isn't involved?
There was a problem hiding this comment.
also we may want to have a custom error message for the "Prop -> Type" (and "SProp -> Type"?) case as that can easily be hit by noobs (eg Goal False \/ False -> nat. intros x; destruct x.) who seem likely to get confused by -> not meaning implication.
|
@coqbot run full ci |
coqbot-app
bot
removed
the
needs: full CI
test-suite/output/ShowUnivs.out
Outdated
| α1 := Type | ||
| α2 := Type | ||
| α3 := α1 | ||
| α3 := α1 |= α1 -> α2 , α1 -> α3 , α1 -> Prop , α1 -> SProp , α1 -> Type , α2 -> α1 , α2 -> α3 , α2 -> Prop , α2 -> SProp , α2 -> Type , α3 -> α1 , α3 -> α2 , α3 -> Prop , α3 -> SProp , α3 -> Type , Prop -> SProp , Type -> α1 , Type -> α2 , Type -> α3 , Type -> Prop , Type -> SProp |
There was a problem hiding this comment.
this is pretty verbose and could use some line break hints
we probably shouldn't be printing tautologies (Prop -> SProp, Type -> anything)
and maybe when a variable eliminates to grounds we should only print the strongest constraint (here we have both α1 -> Prop and α1 -> SProp, α1 -> Prop implies α1 -> SProp)
There was a problem hiding this comment.
This is not the normalized result, so for me it makes sense that it is "verbose". Below we print the normalized version (I'm adding a fix because the normalized version does not include elimination constraints...). The normalized output is simply:
Normalized constraints:
{ ; ShowUnivs.26 ShowUnivs.25 } |= ShowUnivs.25 < ShowUnivs.26which matches what you are saying.
I think another question is whether we want to actually print the non-normalized one ?
There was a problem hiding this comment.
"normalized" means after minimization so it's very lossy
Mmhh, I have no idea if that would be a desired feature, to be honest. I can't think of a case where one would specifically want the system only to elaborate the constraints for levels or qualities, but not the other 🤷 . In any case, if we want that we would first need to adjust the parser to distinguish the two types of constraints, right? As of now, there is no restriction on the order in which you can define the constraints, just that they are separated by a comma. |
TDiazT
force-pushed
the
elab-elim-constraints
branch
from
a83f6ad to
4e2674d
Compare
coqbot-app
bot
added
the
needs: full CI
|
@coqbot run full ci |
coqbot-app
bot
removed
the
needs: full CI
|
@coqbot bench |
|
🏁 Bench results: INFO: failed to install rocq-mathcomp-boot (dependency rocq-elpi failed) 🐢 Top 25 slow downs┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SLOW DOWNS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 175 177 1.5950 0.91% 233 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeByExtension.v.html │ │ 65.0 66.2 1.1752 1.81% 608 coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │ │ 64.7 65.8 1.1427 1.77% 608 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │ │ 201 202 0.9196 0.46% 8 coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html │ │ 58.7 59.6 0.8329 1.42% 27 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html │ │ 119 120 0.6336 0.53% 22 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html │ │ 6.81 7.43 0.6207 9.11% 165 coq-fiat-crypto-with-bedrock/src/Curves/Montgomery/XZProofs.v.html │ │ 21.2 21.7 0.5189 2.45% 24 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/MultiRetSplit.v.html │ │ 42.2 42.7 0.5102 1.21% 223 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Coord32.v.html │ │ 83.3 83.8 0.4782 0.57% 48 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html │ │ 36.3 36.7 0.4545 1.25% 224 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Coord32.v.html │ │ 30.6 31.0 0.4080 1.33% 225 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Coord32.v.html │ │ 34.155 34.552 0.3970 1.16% 97 coq-vst/veric/binop_lemmas5.v.html │ │ 31.0 31.4 0.3786 1.22% 148 coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html │ │ 46.3 46.7 0.3744 0.81% 115 coq-bedrock2/bedrock2/src/bedrock2Examples/full_mul.v.html │ │ 30.7 31.1 0.3681 1.20% 139 coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html │ │ 64.5 64.9 0.3549 0.55% 716 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JacobianCoZ.v.html │ │ 0.340 0.690 0.3497 102.92% 1 rocq-stdlib/theories/btauto/Algebra.v.html │ │ 36.6 37.0 0.3469 0.95% 835 coq-fiat-crypto-with-bedrock/src/Fancy/Compiler.v.html │ │ 29.2 29.5 0.3242 1.11% 715 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html │ │ 25.2 25.5 0.3188 1.27% 226 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Coord32.v.html │ │ 12.4 12.7 0.3026 2.44% 505 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvCommon.v.html │ │ 21.6 21.9 0.2976 1.38% 244 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Coord32.v.html │ │ 0.287 0.584 0.2969 103.34% 36 rocq-stdlib/theories/MSets/MSetAVL.v.html │ │ 35.1 35.4 0.2943 0.84% 174 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html │ └───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ 🐇 Top 25 speed ups┌────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SPEED UPS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 22.8 21.4 -1.3767 -6.05% 49 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html │ │ 40.5 39.9 -0.6668 -1.64% 1423 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.v.html │ │ 27.8 27.2 -0.6076 -2.18% 148 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoorTop.v.html │ │ 44.7 44.1 -0.6046 -1.35% 578 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/MMIO.v.html │ │ 44.7 44.2 -0.5349 -1.20% 3 coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/WithBedrock/fiat_crypto.v.html │ │ 1.84 1.38 -0.4578 -24.94% 75 rocq-stdlib/theories/Numbers/HexadecimalString.v.html │ │ 48.9 48.4 -0.4484 -0.92% 376 coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html │ │ 1.43 1.02 -0.4087 -28.67% 813 rocq-stdlib/theories/MSets/MSetRBT.v.html │ │ 18.7 18.3 -0.3862 -2.06% 481 coq-verdi-raft/theories/RaftProofs/EndToEndLinearizability.v.html │ │ 21.6 21.3 -0.3571 -1.65% 651 rocq-stdlib/theories/Zmod/ZmodBase.v.html │ │ 45.0 44.7 -0.3570 -0.79% 3 coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/bedrock2_fiat_crypto.v.html │ │ 0.527 0.171 -0.3561 -67.54% 592 rocq-stdlib/theories/MSets/MSetAVL.v.html │ │ 1.11 0.777 -0.3357 -30.18% 816 rocq-stdlib/theories/MSets/MSetRBT.v.html │ │ 39.1 38.7 -0.3274 -0.84% 239 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html │ │ 29.3 29.0 -0.3236 -1.10% 145 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoorTop.v.html │ │ 14.2 13.9 -0.3114 -2.20% 216 coq-fiat-crypto-with-bedrock/src/Fancy/Barrett256.v.html │ │ 97.2 96.9 -0.3082 -0.32% 999 coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │ │ 31.2 30.9 -0.2732 -0.88% 214 coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html │ │ 0.853 0.597 -0.2555 -29.95% 690 rocq-stdlib/theories/setoid_ring/Field_theory.v.html │ │ 0.585 0.344 -0.2407 -41.15% 13 rocq-stdlib/theories/Numbers/DecimalFacts.v.html │ │ 0.459 0.220 -0.2384 -51.96% 11 rocq-stdlib/theories/QArith/Qcanon.v.html │ │ 0.499 0.262 -0.2369 -47.49% 13 rocq-stdlib/theories/ZArith/Zmax.v.html │ │ 0.443 0.213 -0.2299 -51.87% 246 rocq-stdlib/theories/Structures/OrdersEx.v.html │ │ 12.1 11.9 -0.2270 -1.87% 388 coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/Logic/Existential.v.html │ │ 0.519 0.301 -0.2174 -41.90% 1161 rocq-stdlib/theories/Strings/Byte.v.html │ └────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
TDiazT
force-pushed
the
elab-elim-constraints
branch
from
1b773df to
969220d
Compare
jrosain
force-pushed
the
elab-elim-constraints
branch
from
969220d to
7d5e87c
Compare
SkySkimmer
removed
needs: squashing
|
This change makes this error message Lines 301 to 307 in 8613ed9 Set Universe Polymorphism.
Inductive Box@{s s';+} (A:Type@{s;_}) : Type@{s';_} := box (_:A).
Definition unbox@{s s'; +| Prop -> s', s -> Type} A (x:Box@{s s';_} A) := match x with box _ v => v end.
(*
Error:
Incorrect elimination of "x" in the inductive type "Box@{s s' ; foo.25}":
the return type has sort "Type@{s ; foo.25}" while it should be in a sort s' eliminates to.
Elimination of a sort polymorphic inductive object instantiated to a variable sort quality
is only allowed on itself or with an explicit elimination constraint to the target sort.
*)The message should probably be changed, at least it isn't true anymore that elim constraints must be explicit. |
Yeah, I would actually simply remove the second part of this message. That's all there is to know about the error. edit: Or actually, maybe give a hint on how to solve: (*
Error:
Incorrect elimination of "x" in the inductive type "Box@{s s' ; foo.25}":
the return type has sort "Type@{s ; foo.25}" while it should be in a sort s' eliminates to.
Either adjust the sort qualities accordingly or add an explicit elimination constraint from
s' to s.
*) |
github-actions
bot
added
the
needs: rebase
| @@ -0,0 +1,4 @@ | |||
| - **Added:** | |||
| implicit elaboration of elimination constraints | |||
There was a problem hiding this comment.
should have a link to the doc section about this
| implicit elaboration of elimination constraints | |
| implicit elaboration of :ref:`elimination constraints <elim-constraints>` |
together with my other requested change
| instance is sort polymorphic, the return type of the elimination must | ||
| be at the same quality. These restrictions ignore :flag:`Definitional | ||
| UIP`. | ||
| Elimination of Sort-Polymorphic Inductives |
There was a problem hiding this comment.
makes this a target for the :ref: I suggest in the changelog
| Elimination of Sort-Polymorphic Inductives | |
| .. _elim-constraints: | |
| Elimination of Sort-Polymorphic Inductives |
We could also try to keep the qgraph error, eg 652ebda produces (however too verbose IMO, probably we shouldn't say the "is only allowed" sentence when we have a qgraph error) |
TDiazT
force-pushed
the
elab-elim-constraints
branch
from
7d5e87c to
ef3588a
Compare
coqbot-app
bot
removed
the
needs: rebase
Yeah, although in your example it would be weird for a user to read that the qualities are inconsistent. Maybe it would be ok with the part stating that it is trying to enforce In this case I feel the first part of the error is enough to understand what is happening: You don't need to know it's trying to enforce it under the hood and the "is allowed sentence" sentence is not completely correct. We could replace the second sentence with suggestions on how to fix? |
What suggestions could we make? |
|
So what do we do about the error messages? |
github-actions
bot
added
the
needs: rebase
"Either adjust the sort qualities accordingly or add an explicit elimination constraint from s' to s"? |
Whenever an elimination constraint is not satisfied, then it adds the constraint as a new local one for the definition. Currently behind a flag to avoid backward compatibility for the moment. fix: Reintroduce QElimTo to univProblem It was replaced by QLeq to deal only with cumulativity constraints. refactor: Remove unnecessary abstraction of code Maybe it's using a more general API than it should, considering PConstraints instead of simply UnivConstrants. fix: Handle new EliminationError exception in cases and inductiveops print: Improve printing of qGraph and elimination errors refactor: Printing suggestions from code review Co-authored-by: Gaëtan Gilbert <[email protected]> refactor: Printing suggestion
Remove overlay for hb
TDiazT
force-pushed
the
elab-elim-constraints
branch
from
ef3588a to
fa7a374
Compare
coqbot-app
bot
removed
the
needs: rebase
|
@coqbot run full ci |
coqbot-app
bot
removed
the
needs: full CI
SkySkimmer
added
the
kind: enhancement
7 participants
This PR adds implicit elaboration of elimination constraints. Only elimination constraints, not qualities.
(Also some fixes in printing + some refactoring/renaming that don't change the API)
Associated RFC : rocq-prover/rfcs#111.
Examples
Main API Changes
univProblem.mli: Extending constraints to includeQElimToevd.mli: Adding aset_elim_tofunctionOverlays