chore: call dsimp in the default tactic of ContinuousLinearMap#37386
chore: call dsimp in the default tactic of ContinuousLinearMap#37386gasparattila wants to merge 3 commits intoleanprover-community:masterfrom
dsimp in the default tactic of ContinuousLinearMap#37386Conversation
PR summary d194281a48Import 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
|
| cont : Continuous toFun := by | ||
| first | fun_prop | eta_expand; dsimp -failIfUnchanged; fun_prop |
There was a problem hiding this comment.
why not just the following? (is it slower?)
| cont : Continuous toFun := by | |
| first | fun_prop | eta_expand; dsimp -failIfUnchanged; fun_prop | |
| cont : Continuous toFun := by eta_expand; dsimp -failIfUnchanged; fun_prop |
There was a problem hiding this comment.
CStarMatrix.toCLM fails if we use eta_expand. The issue seems to be that after eta_expand, the function isn't well-typed under reducible transparency. This particular example doesn't work with with_reducible eta_expand; dsimp either because of defeq abuse around WithCStarModule.
There could also be some continuous map that is the composition of non-continuous maps such that its simp normal form uses the non-continuous maps. I didn't find such a definition involving linear maps, though.
|
Once #37009 gets merged, can you merge master and remove the |
themathqueen
added
the
t-topology
themathqueen
left a comment
themathqueen
left a comment
There was a problem hiding this comment.
Looks reasonable, thanks!
I'm not an expert in fun_prop attributions, so will let someone else review these as well.
Co-authored-by: Monica Omar <[email protected]>
3 participants
This will also reduce the breakage in #35548.