chore(FiberBundle/Trivialisation): tag with grind#37535
chore(FiberBundle/Trivialisation): tag with grind#37535grunweg wants to merge 1 commit intoleanprover-community:masterfrom
Conversation
|
@chenson2018 We talked about this a bit in person: would you like to take a look from a "grind tagging" perspective? (I'm also happy to read your draft write-up instead, and try to understand and apply it here.) |
PR summary 96c77b07ffImport changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diffNo declarations were harmed in the making of this PR! 🐙 You can run this locally as follows## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>The doc-module for No changes to technical debt.You can run this locally as
|
github-actions
bot
added
the
t-topology
I am unsure if all of these are good grind lemmas; close examination is welcome. I left XXX comments with my questions; there are about 3 different questions repeating a few times.
grunweg
force-pushed
the
fiberbundle-grind
branch
from
7a2d2da to
3ad4893
Compare
chenson2018
left a comment
chenson2018
left a comment
There was a problem hiding this comment.
I picked out the first XXX comment and tried to write out my thought process for picking out a pattern. Hopefully this is helpful and transferable to your other comments.
| theorem mk_proj_snd (ex : x ∈ e.source) : (proj x, (e x).2) = e x := | ||
| Prod.ext (e.coe_fst ex).symm rfl | ||
|
|
||
| -- XXX: grind → errors (but `grind =` doesn't); is this a sensible grind lemma? |
There was a problem hiding this comment.
It might be helpful to see some possible grind_pattern written out:
-- grind =
grind_pattern mk_proj_snd' => (proj x, (e x).2)
-- grind =_
grind_pattern mk_proj_snd' => e x
-- grind =>
grind_pattern mk_proj_snd' => proj x ∈ e.baseSet, (proj x, (e x).2)
-- grind! =>
grind_pattern mk_proj_snd' => e.baseSet, e x
-- patterns beyond what grind? suggests
grind_pattern mk_proj_snd' => proj x ∈ e.baseSet, e xThese are mostly corresponding to what writing grind? in the attribute reports. The choice here is essentially how eagerly this triggers, so a bit of mathematical context required to know when it's useful. Based on your mentioning grind →, maybe grind => might capture your intent?
3 participants
I am unsure if all of these are good grind lemmas; close examination is welcome. I left XXX comments with my questions; there are about 3 different questions repeating a few times.