Conversation
PR summary 224861affcImport changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diff
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 No changes to technical debt.You can run this locally as
|
grunweg
left a comment
There was a problem hiding this comment.
I have one comment, about possible simplifications. Otherwise, the changes look good to me; I haven't checked yet if the simp tagging is fine etc.
| This one instead uses a `NeZero n` typeclass hypothesis. | ||
| -/ | ||
| @[simp] | ||
| theorem mk_zero' (n : ℕ) (hn : 0 < n) : (⟨0, hn⟩ : Fin n) = haveI : NeZero n := .of_pos hn; 0 := rfl |
There was a problem hiding this comment.
I'm not sure whether we want this @[simp] lemma to apply to any (⟨0, hn⟩ : Fin n) (as it is written now) or only if [NeZero n] is in the context. In the former case (as it's written now), it forces us to write LHS of other simp lemmas as haveI : NeZero expr := _; ... (0 : Fin expr) instead of (⟨0, _⟩ : Fin expr).
There was a problem hiding this comment.
@kim-em WDYT? This lemma (in this form or in the (n : Nat) [NeZero n] form) is an obvious candidate for replacing Fin.mk_zero in the Lean core. Which form has more chances to get accepted?
There was a problem hiding this comment.
I think I'd prefer the NeZero version.
There was a problem hiding this comment.
Both versions have NeZero, just at different places. In one case, simp can lead to expressions that use NeZero instances that aren't in the context. In another case, adding a local NeZero instance may break simp calls.
There was a problem hiding this comment.
I went through git grep 'haveI.*NeZero', and found that Fin.cast_zero and PNat.mk_ofNat are the only lemmas that introduce an inline NeZero instance to state the lemma.
Cherry-picked from #21112
Cherry-picked parts of #21112 that don't rely on a decision about inline `haveI : NeZero n := _`
Cherry-picked parts of #21112 that don't rely on a decision about inline `haveI : NeZero n := _`
... adding `[NeZero n]` as needed. Cherry-picked from #21112
This is a version of #21112 that doesn't use inline `NeZero` instances, thus doesn't break `simp` normal forms all over the place.
This is a version of #21112 that doesn't use inline `NeZero` instances, thus doesn't break `simp` normal forms all over the place.
Motivated by an upcoming refactor of the Faa Di Bruno formula.
Fin n.succtoFin n#21193