Automatically generated goal names #20809
Conversation
coqbot-app
bot
added
the
needs: full CI
dhalilov
force-pushed
the
autonaming-goals
branch
3 times, most recently
from
1a989d3 to
ca1c5f5
Compare
|
@coqbot run full ci |
coqbot-app
bot
removed
the
needs: full CI
|
🔴 CI failure at commit ca1c5f5 without any failure in the test-suite ✔️ Corresponding job for the base commit 90e3b7e succeeded ❔ Ask me to try to extract a minimal test case that can be added to the test-suite 🏃
|
dhalilov
force-pushed
the
autonaming-goals
branch
from
ca1c5f5 to
7331b53
Compare
coqbot-app
bot
added
the
needs: full CI
ppedrot
added
needs: merge of dependency
| | WITH OPT ( [ natural | "[" ident "]" ] ":" ) "{" | ||
| | MOVETO simple_tactic OPT ( [ natural | "[" ident "]" ] ":" ) "{" | ||
| | WITH OPT ( [ natural | "[" fullyqualid "]" ] ":" ) "{" | ||
| | MOVETO simple_tactic OPT ( [ natural | "[" fullyqualid "]" ] ":" ) "{" |
There was a problem hiding this comment.
Why "fullyqualid"? Are you prohibiting use of the shortest unique suffix? If so, that behavior is inconsistent with all other qualids--and give your rationale.
Also I didn't see a description of this nonterminal in the doc---IMO that's a requirement.
There was a problem hiding this comment.
Qualified goal names behave differently from other qualids, since there is only one name for them which is the shortest one by construction. That means they are also always fully qualified, so I think fullyqualid makes the distinction clear.
There was a problem hiding this comment.
Qualified goal names behave differently from other quali
That's precisely the problem. While the syntax is the same as qualids, their behavior/use is entirely different. Just call them goal names and explain that they may have multiple dotted components.
|
dhalilov
force-pushed
the
autonaming-goals
branch
2 times, most recently
from
e086bfc to
ff080d7
Compare
|
(Cleaned the history. The PR needs #20813 to be merged first and then will be rebased on master) |
Best to put this in the PR description--reviewers are likely to miss this if it's only in the conversation. |
There was a problem hiding this comment.
I don't see how this feature is really helpful for users. Maybe you can give a better example or (maybe easier) explain in words when/why it's helpful. If you can't make a convincing case, I would not approve this PR. It also seems quite limited since names are generated only for 3 tactics.
If you can make that convincing case, there are details of the behavior and documentation that we'd need to further consider/revise.
engine/evarnames.ml
Outdated
| (** If true, this option enables automatic generation of goal names. *) | ||
| let { Goptions.get = accessible_goal_names } = | ||
| Goptions.declare_bool_option_and_ref | ||
| ~key:["Accessible";"Goal";"Names"] | ||
| ~value:true |
There was a problem hiding this comment.
"Accessible" seems vague, "Generate" may be better.
I would make the default false; I think most users won't enable this option.
This feature / work was presented and discussed at Rocq'n'share last week and got positive feedback, giving a convincing case that this can definitely be useful to users to organize their proofs, and choose to focus on specific subgoals, rather than relying on fragile comments. I guess you were not aware of that @jfehrle. |
The idea behind generating goal names is to provide a more robust alternatives to bullets and numbers. If you are doing case analysis on an inductive with two constructors (say destruct x.
- (* case A *) ...
- (* case B *) ...This proof is bound to break in various ways if you changed the order of the constructors, or added a new one. It is likely that the proof would break in a random bullet, which would be tricky to understand. With named goals, you get a slightly better proof that allows you to write your cases in any order: destruct x.
1: refine ?[A].
2: refine ?[B].
[A]: { ... }
[B]: { ... }but you're still relying on the order of the constructors when you're giving names, and so you have the same problem as before. If we generated goal names This improves both readability, maintainability, and error messages at a low cost. (Note that Lean provides a
Since the mechanism is quite general, it should work for any tactic that unifies with hypotheses, so I expect it to work with some |
github-actions
bot
added
the
needs: rebase
How would I be aware of that if I didn't attend the meeting? |
|
@dhalilov That makes some sense. It would be good to explain this briefly where the option is described, maybe something like
For usability, it's best to make the feature as comprehensive as reasonably possible. It can be annoying to have something work in some cases and not work in other similar cases--it requires more thinking by the user. This annoyance may lead to people not using the feature. To get adoption, you want users to have a great experience the first time they try a feature. If the feature is not comprehensive, the doc could say that the feature is experimental. |
dhalilov
force-pushed
the
autonaming-goals
branch
from
ff080d7 to
ad873cf
Compare
coqbot-app
bot
removed
the
needs: rebase
dhalilov
force-pushed
the
autonaming-goals
branch
from
ad873cf to
6032b00
Compare
ppedrot
added
kind: feature
|
@coqbot run full ci |
coqbot-app
bot
removed
the
needs: full CI
|
@coqbot bench |
|
🏁 Bench results: INFO: failed to install 🐢 Top 25 slow downs┌────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SLOW DOWNS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 31.535 33.616 2.0810 6.60% 97 coq-vst/veric/binop_lemmas5.v.html │ │ 65.9 67.7 1.7251 2.62% 609 coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │ │ 40.618 42.204 1.5860 3.90% 834 coq-vst/veric/binop_lemmas4.v.html │ │ 93.8 94.7 0.8941 0.95% 968 coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │ │ 11.719 12.565 0.8460 7.22% 126 coq-vst/veric/binop_lemmas6.v.html │ │ 2.951 3.757 0.8060 27.31% 431 coq-vst/veric/binop_lemmas3.v.html │ │ 3.569 4.356 0.7870 22.05% 154 coq-vst/veric/binop_lemmas5.v.html │ │ 93.7 94.4 0.7614 0.81% 999 coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │ │ 4.599 5.276 0.6770 14.72% 84 coq-vst/veric/binop_lemmas2.v.html │ │ 1.448 1.953 0.5050 34.88% 60 coq-vst/veric/binop_lemmas2.v.html │ │ 38.7 39.2 0.4935 1.27% 236 coq-rewriter/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v.html │ │ 2.347 2.838 0.4910 20.92% 728 coq-vst/veric/expr_lemmas.v.html │ │ 1.417 1.879 0.4620 32.60% 153 coq-vst/veric/binop_lemmas6.v.html │ │ 45.8 46.2 0.4588 1.00% 115 coq-bedrock2/bedrock2/src/bedrock2Examples/full_mul.v.html │ │ 0.246 0.668 0.4219 171.39% 719 rocq-stdlib/theories/MSets/MSetRBT.v.html │ │ 38.0 38.4 0.4039 1.06% 224 coq-performance-tests-lite/PerformanceExperiments/rewrite_lift_lets_map.v.html │ │ 3.88 4.268 0.3880 10.00% 477 coq-vst/veric/expr_lemmas3.v.html │ │ 0.995 1.369 0.3740 37.59% 937 coq-vst/veric/binop_lemmas2.v.html │ │ 1.23 1.57 0.3343 27.11% 1142 rocq-stdlib/theories/FSets/FMapAVL.v.html │ │ 48.1 48.4 0.3175 0.66% 376 coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html │ │ 0.488 0.802 0.3144 64.47% 747 rocq-stdlib/theories/MSets/MSetRBT.v.html │ │ 1.43 1.73 0.2966 20.70% 313 rocq-stdlib/theories/Strings/Byte.v.html │ │ 36.2 36.5 0.2936 0.81% 139 coq-fiat-parsers/src/Parsers/Refinement/SharpenedJSON.v.html │ │ 0.196 0.481 0.2850 145.55% 374 rocq-stdlib/theories/Sorting/SetoidList.v.html │ │ 0.299 0.577 0.2776 92.75% 1161 rocq-stdlib/theories/Strings/Byte.v.html │ └────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ 🐇 Top 25 speed ups┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SPEED UPS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 200 199 -0.7706 -0.39% 8 coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html │ │ 1.28 0.726 -0.5510 -43.15% 813 rocq-stdlib/theories/MSets/MSetRBT.v.html │ │ 3.98 3.61 -0.3711 -9.32% 492 rocq-stdlib/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v.html │ │ 34.626 34.278 -0.3480 -1.01% 147 coq-vst/veric/expr_lemmas4.v.html │ │ 2.55 2.23 -0.3134 -12.31% 607 rocq-stdlib/theories/Zmod/ZmodBase.v.html │ │ 33.535 33.248 -0.2870 -0.86% 194 coq-vst/veric/expr_lemmas4.v.html │ │ 0.614 0.340 -0.2742 -44.68% 597 rocq-stdlib/theories/Strings/Byte.v.html │ │ 0.319 0.0633 -0.2554 -80.15% 1208 coq-unimath/UniMath/CategoryTheory/DisplayedCats/Examples/StrictTwoSidedDispCat.v.html │ │ 1.04 0.788 -0.2475 -23.91% 736 rocq-stdlib/theories/Reals/Cauchy/ConstructiveCauchyReals.v.html │ │ 8.49 8.24 -0.2454 -2.89% 1331 coq-mathcomp-odd-order/theories/PFsection9.v.html │ │ 24.1 23.8 -0.2362 -0.98% 558 coq-bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html │ │ 21.7 21.5 -0.2323 -1.07% 651 rocq-stdlib/theories/Zmod/ZmodBase.v.html │ │ 1.17 0.942 -0.2238 -19.19% 2109 rocq-stdlib/theories/FSets/FMapFacts.v.html │ │ 23.6 23.4 -0.2229 -0.94% 12 coq-fourcolor/theories/proof/job295to298.v.html │ │ 0.354 0.138 -0.2165 -61.15% 1187 rocq-stdlib/theories/Strings/Byte.v.html │ │ 0.226 0.0129 -0.2134 -94.30% 323 rocq-metarocq-erasure/erasure/theories/Typed/OptimizeCorrectness.v.html │ │ 11.6 11.4 -0.2098 -1.81% 410 coq-verdi-raft/theories/RaftProofs/LeaderLogsLogMatchingProof.v.html │ │ 0.509 0.300 -0.2094 -41.13% 313 rocq-stdlib/theories/Reals/Abstract/ConstructiveLUB.v.html │ │ 0.223 0.0141 -0.2090 -93.66% 112 rocq-metarocq-erasure/erasure/theories/EDeps.v.html │ │ 17.7 17.5 -0.2074 -1.17% 31 coq-engine-bench-lite/coq/PerformanceDemos/pattern.v.html │ │ 9.27 9.07 -0.2068 -2.23% 434 coq-mathcomp-odd-order/theories/PFsection12.v.html │ │ 0.485 0.281 -0.2047 -42.16% 12 rocq-stdlib/theories/MSets/MSets.v.html │ │ 0.208 0.00333 -0.2045 -98.40% 763 rocq-metarocq-erasure/erasure/theories/EWcbvEval.v.html │ │ 0.195 0.00114 -0.1943 -99.41% 90 rocq-metarocq-erasure/erasure/theories/EEtaExpanded.v.html │ │ 0.193 0.000577 -0.1924 -99.70% 121 rocq-metarocq-erasure/erasure/theories/ESubstitution.v.html │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
|
🔴 CI failure at commit 6032b00 without any failure in the test-suite ✔️ Corresponding job for the base commit 7aa1b22 succeeded ❔ Ask me to try to extract a minimal test case that can be added to the test-suite 🏃
|
| .. rocqtop:: all abort | ||
|
|
||
| Set Generate Goal Names. | ||
|
|
||
| Goal forall n m, n + m = m + n. | ||
| Proof. | ||
| intros. induction m. | ||
| [O]: { | ||
| simpl. induction n. |
There was a problem hiding this comment.
This 4 line example expands into more than a page in the documentation, long for a simple example. Would be nice to omit some of the output to shorten it.
Where you have multiple tactics on the same line, the output for both confusingly appears below the tactic line like so (above the red line is simpl, below the red line is induction):
The simplest thing is to put them on separate lines. In this case, maybe better not to show the output for intros and other uninteresting bits, like this:
| .. rocqtop:: all abort | |
| Set Generate Goal Names. | |
| Goal forall n m, n + m = m + n. | |
| Proof. | |
| intros. induction m. | |
| [O]: { | |
| simpl. induction n. | |
| .. rocqtop:: in abort | |
| Set Generate Goal Names. | |
| Goal forall n m, n + m = m + n. | |
| intros. | |
| .. rocqtop:: all | |
| induction m. | |
| .. rocqtop:: in | |
| [O]: { | |
| simpl. | |
| .. rocqtop:: all | |
| induction n. |
There seems to be a bug in the rocqtop directive: the output for [O]: { should appear just below that line.
BTW, do you know you can view the formatted documentation by clicking on this link in the PR?
There was a problem hiding this comment.
There seems to be a bug in the rocqtop directive: the output for [O]: { should appear just below that line.
This is also present in other examples, so it might be a parsing issue.
I'll shorten the output a bit 👍
There was a problem hiding this comment.
It's an bug/limitation in the Python code for the directive.
| .. rocqtop:: all abort | ||
|
|
||
| Set Generate Goal Names. | ||
|
|
||
| Goal forall n m, n + m = m + n. | ||
| Proof. | ||
| intros. induction m. | ||
| [O]: { | ||
| simpl. induction n. |
There was a problem hiding this comment.
If the focus rules remain the same (i.e. switch to S when you're focused in O isn't allowed), it would be nicer if the user could specify only the last component of the goal name--just S below instead of O.S (or O instead of O.O). I don't know how long the qualified names may get in practice, nor whether restructuring a proof might mean changing many qualified names.
There was a problem hiding this comment.
If the focus rules remain the same (i.e. switch to S when you're focused in O isn't allowed)
You can still apply a tactic to S even where O is focused by doing [S]: tac. What is not allowed is to nest focusing braces, so removing the second focusing brace after [S]: in your example should make it work.
it would be nicer if the user could specify only the last component of the goal name--just S below instead of O.S (or O instead of O.O)
I do agree but goal names are global to the proof and thus only specifying S would be ambiguous, which is precisely why qualified names are required. Relying on the focus state for name resolution would introduce unnecessary complexity in my opinion.
I don't know how long the qualified names may get in practice, nor whether restructuring a proof might mean changing many qualified names.
Since we are only working with shortest names, the qualification depth is equal to the number of consecutive destruct/induction that the proof made on the same inductive type, so you can expect names to not be very long (unless you are doing a repeat destruct, but in that case I don't think you would use named goals anyway since you are generating too many cases to handle by hand).
There was a problem hiding this comment.
it would be nicer if the user could specify only the last component of the goal name
I do agree but goal names are global to the proof and thus only specifying
Swould be ambiguous, which is precisely why qualified names are required.
Just check at run time whether there are multiple goal names that match S and, if so, generate an error. If your trie stores the qualified name in reverse order, that should be easy to do. (Similar to qualids for modules: the user generally only needs to provide a suffix that uniquely identifies the module.)
|
|
||
| .. rocqtop:: all reset | ||
|
|
||
| Set Generate Goal Names. |
There was a problem hiding this comment.
If you keep the default "true", maybe not necessary.
There was a problem hiding this comment.
I don't know yet what will be the default value of the option yet, so I keep it in the examples for now
| This option makes it possible to write proofs with multiple subgoals that do | ||
| not depend on the order in which constructors were defined. If you use | ||
| bullets or numbers instead, reordering constructors will break the proof. |
There was a problem hiding this comment.
FWIW: this drops the dependency on the order in which constructors were defined, replacing it with a dependency on the constructor name. If you change a constructor name, a text search will usually make it easy to update the constructor names--unlike depending on the order.
There was a problem hiding this comment.
Yes indeed, might be worth adding to the documentation
| :token:`qualid` (see :ref:`existential-variables`). This works even when | ||
| the goal is not in focus. |
There was a problem hiding this comment.
"This works even when the goal is not in focus." - this isn't true for my example above using S instead of O.S. Maybe the sentence only covers shelved goals?
There was a problem hiding this comment.
I think this sentence meant that you could focus on shelved goals, yes
|
|
||
| This option makes it possible to write proofs with multiple subgoals that do | ||
| not depend on the order in which constructors were defined. If you use | ||
| bullets or numbers instead, reordering constructors will break the proof. |
There was a problem hiding this comment.
Also add a sentence mentioning qualified names here with an in-line example like O.S and a hyperlink to the longer example. It's a key point that should be in the text description, not only in the examples a couple pages below.
There was a problem hiding this comment.
One other thing: it would be nice to show here how to structure the proof when using the feature. Maybe like this, but just quoted text, keep the ellipses, not a rocqtop example. And maybe a sentence of explanation.
induction n.
[O]: { ... }
[S]: { ... }
FWIW, a user could write weird and much less readable things like:
[A]: tac1.
[B]: tac2.
[A]: tac3.
[A]: tac4.
| If several goals generate the same name (e.g. when doing nested case | ||
| analysis or induction), *qualified names* are used to disambiguate them, | ||
| using the qualified name of the parent as the basis for the fully | ||
| qualified name. |
There was a problem hiding this comment.
If you have induction on a bool inside induction on a nat, will the bool cases have names like true or O.true?
I suspect that qualified names are always used for nested cases, but I didn't try an example.
Seems like you should have an example that actually selects a qualified goal name, e.g. [S.O]: {
There was a problem hiding this comment.
They will have names true and false since there's no point in prefixing them with O or S. (This is a consequence of the trie data structure we use to insert new names.)
coqbot-app
bot
added
the
needs: full CI
|
The doc part is coming along. Let me know when you have the "final" version and I'll take another look. That would be a good time to move the PR from draft status. I'll leave the review of the code to others who are more knowledgeable. |
github-actions
bot
added
the
needs: rebase
This PR adds the possibility to have automatically generated goal names through the
Accessible Goal Namesoption. This also includes qualified goal names and showing the difference between accessible and non-accessible printing names inShow Existentials.Requires #20813 to be merged first.
make doc_gram_rsts.