chore(Topology): replace continuity -> fun_prop#13994
chore(Topology): replace continuity -> fun_prop#13994
Conversation
This is almost (but not fully exhaustive). This changes the default values for Homeomorph... let's see if this breaks. One proof gets partially un-automated (cont. -> partial fun_prop); if desired, I can revert this change.
PR summary 9aac757c82Import 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/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for |
| · continuity | ||
| · continuity | ||
| · continuity | ||
| -- TODO: can the auto-param be converted to use `fun_prop` (instead of `continuity`)? |
There was a problem hiding this comment.
The current auto-param uses continuity, which is slower... so, a good follow-up would be to make that use fun_prop as well. (This causes some breakage, which is why I'd like to not do so in this PR.)
| def genLoopEquivOfUnique (N) [Unique N] : Ω^ N X x ≃ Ω X x where | ||
| toFun p := | ||
| Path.mk ⟨fun t => p fun _ => t, by continuity⟩ | ||
| Path.mk ⟨fun t => p fun _ => t, by |
There was a problem hiding this comment.
My impression is that this version is significantly faster. That said, it would be great to reduce this to one line... perhaps mk_apply should be tagged with fun_prop?
6630106 to
3cdc4bf
Compare
1be9017 to
693fb50
Compare
|
CI is done (except for the linter), so let's benchmark this |
|
!bench |
|
Here are the benchmark results for commit 693fb50. Benchmark Metric Change
=============================================================================
+ ~Mathlib.Topology.ContinuousFunction.StoneWeierstrass instructions -12.6%
+ ~Mathlib.Topology.Homotopy.HomotopyGroup instructions -15.8%
+ ~Mathlib.Topology.MetricSpace.Perfect instructions -72.0% |
|
General information: No file got slower by at least 10⁹ instructions. No file got slower by at least 10%. 5 files got faster by at least 10⁹ instructions: 3 files got faster by at least 10%: |
|
I would like this PR to wait for #11092. I don't think we should be making I have added this as a dependency to this PR, even though it isn't technically required in order to reflect this. Another maintainer can override me if they wish with an explanation. |
|
If I find the time, I can also take out the default value changes (as the other ones are clearly good already). I'll see. |
|
This PR/issue depends on:
|
|
Closing in favour of #35273. |
leanprover-community#35273) Resurrected version of leanprover-community#13994. Let's look at the current fall-out and performance effect.
Addresses a few porting notes; I expect also a substantial speed-up of some proofs.
Change a few default values of proof fields from
continuitytofun_prop; this required a few fix-ups downstream. (I checked a few instances; the failure seems related toContinuous.subtype_mknot always firing.)This is almost (but not fully) exhaustive.
One proof gets partially un-automated (cont. -> partial fun_prop); if desired, I can revert this change.