Conversation
… update on the branch
…a stage0 update on the branch" This reverts commit 9535f2e.
Rob23oba
reviewed
May 20, 2025
f694af3 to
88c553f
Compare
ghost
pushed a commit
to leanprover-community/batteries
that referenced
this pull request
May 20, 2025
ghost
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
May 20, 2025
|
Mathlib CI status (docs):
|
ghost
pushed a commit
to leanprover-community/batteries
that referenced
this pull request
May 20, 2025
ghost
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
May 20, 2025
ghost
pushed a commit
to leanprover-community/batteries
that referenced
this pull request
May 21, 2025
ghost
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
May 21, 2025
f89aad0 to
1f2edc1
Compare
Collaborator
|
Here are the benchmark results for commit f89aad0. Benchmark Metric Change
=================================================================================
+ Init.Data.BitVec.Lemmas re-elab branch-misses -2.1% (-39.1 σ)
+ Init.Data.List.Sublist re-elab -j4 branch-misses -2.6% (-23.5 σ)
+ Std.Data.DHashMap.Internal.RawLemmas branch-misses -3.6% (-48.3 σ)
+ binarytrees.st task-clock -9.3% (-21.5 σ)
+ binarytrees.st wall-clock -9.3% (-21.5 σ)
- bv_decide_inequality.lean maxrss 2.4% (192.9 σ)
- lake build no-op maxrss 7.0% (49.1 σ)
- riscv-ast.lean branches 2.4% (153.2 σ)
- riscv-ast.lean instructions 2.1% (73.4 σ)
+ stdlib blocked -96.3% (-1160.9 σ)
- stdlib blocked (unaccounted) 37.5% (33.8 σ) |
Rob23oba
reviewed
Jun 5, 2025
| def validateDefEqAttr (declName : Name) : AttrM Unit := do | ||
| let info ← getConstVal declName | ||
| MetaM.run' do | ||
| withTransparency .all do -- we want to look through defs in `info.type` all the way to `Eq` |
Contributor
There was a problem hiding this comment.
If I understand this correctly,
def P := 1 = 1
@[defeq, simp]
theorem p_true : P := rflwould get accepted and then
/-
(kernel) application type mismatch: In the application
@id P True.intro
the final argument
True.intro
has type
True
but is expected to have type
P
-/
example : P := by dsimp(because it thinks P = True is defeq)
May have misunderstood how this attribute is supposed to work exactly though
Collaborator
Author
There was a problem hiding this comment.
I get
def Q := 1 = 1
@[defeq, simp] theorem Q_true : Q := rfl
/-- error: dsimp made no progress -/
#guard_msgs in example : Q := by dsimp [Q_true]
on this branch (and also before).
I think this is expected: Q_true when used by simp is turned into eq_true Q_true : Q = True, and that isn't a rfl lemma.
Contributor
There was a problem hiding this comment.
Hmm, that will make support for Iff a bit difficult though, won't it?
Collaborator
Author
There was a problem hiding this comment.
Is this a regression, or are you worried about difficulties when adding new features? (I’m not worried about refactoring any of this after it lands.)
Contributor
There was a problem hiding this comment.
Adding new features; but I guess yeah, it's fine to refactor so this can probably land like this for now.
1f2edc1 to
af15d77
Compare
Collaborator
Author
|
!bench |
Collaborator
|
Here are the benchmark results for commit af15d77. Benchmark Metric Change
=================================================================================
- Init.Data.BitVec.Lemmas maxrss 16.1% (20.9 σ)
+ Init.Data.BitVec.Lemmas wall-clock -38.8% (-119.9 σ)
+ Init.Data.BitVec.Lemmas re-elab branches -2.4% (-89.4 σ)
+ Init.Data.BitVec.Lemmas re-elab instructions -2.3% (-95.2 σ)
+ Std.Data.DHashMap.Internal.RawLemmas wall-clock -13.4% (-32.3 σ)
- riscv-ast.lean branches 2.6% (58.8 σ)
- riscv-ast.lean instructions 2.3% (44.3 σ)
- stdlib attribute application 16.0% (56.6 σ)
+ stdlib blocked -93.4% (-1430.0 σ)
- stdlib tactic execution 8.7% (31.3 σ)
+ stdlib wall-clock -4.1% (-145.6 σ) |
This reverts commit b6838f8.
af15d77 to
8f798af
Compare
ghost
pushed a commit
to leanprover-community/batteries
that referenced
this pull request
Jun 5, 2025
ghost
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
Jun 5, 2025
8f798af to
f6db92f
Compare
kim-em
added a commit
to leanprover/lean4checker
that referenced
this pull request
Jun 12, 2025
jcommelin
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Jun 16, 2025
* Update lean-toolchain for testing leanprover/lean4#8584 * chore: adaptations for nightly-2025-06-02 * change phrasing of comments * chore(Geometry/Manifold): two simp-lemmas can be proven by simp * fix two lint problems * Trigger CI for leanprover/lean4#8519 * chore: bump to nightly-2025-06-03 * fix * fix * Update lean-toolchain for testing leanprover/lean4#8610 * fix * revert change in `Mathlib.Data.ZMOD.Basic` * fix Mathlib/Data/List/EditDistance/Estimator.lean * give specialized simp lemmas higher prio * simp can prove these * simp can prove these * chore: bump to nightly-2025-06-04 * bump toolchain * Adapt eqns * Revert "Adapt eqns" This reverts commit 34f1f7f. * Simply remove check for now * fix a bunch * fixes? * chore: adaptations for nightly-2025-06-04 * add `simp low` lemma `injOn_of_eq_iff_eq` * wip * wip * wip * fix * Trigger CI for leanprover-community/batteries#1220 * Merge master into nightly-testing * chore: bump to nightly-2025-06-05 * Kick CI * Bump lean4-cli * Bump import-graph * Kick CI * update lakefile * chore: use more robust syntax quotation in Shake * Trigger CI for leanprover/lean4#8419 * Revert "chore: use more robust syntax quotation in Shake" This reverts commit cd87328. * fix(Shake): fix import syntax @Kha this is deliberately using this approach because syntax quotations are also not robust but for a different reason: they fail to parse the new versions of the syntax (and do so at run time). And using all the optional doohickeys will not be future proof. The current setup is explicitly meant to ping me when there is a syntax change so I can evaluate the right way to handle it. In this case we want all the module options to be ignored (treated the same as a regular import for the purpose of dependency tracking), we don't want to fail. * cleanup lakefile * chore: bump to nightly-2025-06-06 * Update lean-toolchain for testing leanprover/lean4#8653 * fix * how did this get dropped?!?! * chore: bump to nightly-2025-06-07 * chore: bump to nightly-2025-06-08 * chore: bump to nightly-2025-06-09 * fix lakefile * fix lint-style for new Lean.Options API * chore: bump to nightly-2025-06-10 * chore: bump to nightly-2025-06-09 * merge lean-pr-testing-4 * chore: bump to nightly-2025-06-11 * chore: adaptations for nightly-2025-06-11 * Update Shake/Main.lean Co-authored-by: Johan Commelin <johan@commelin.net> * Apply suggestions from code review * revert * chore: adaptations for nightly-2025-06-11 * cleanup grind tests * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8419 * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8653 * adaptation note * oops * chore: adaptations for nightly-2025-06-12 * remove nolint simpNF * remove spurious file * Update lean-toolchain for testing leanprover/lean4#8751 * fix * chore: bump to nightly-2025-06-13 * Merge master into nightly-testing * fix * remove upstreamed * drop no-op `show` * chore: bump to nightly-2025-06-14 * chore: bump to nightly-2025-06-15 * intentionally left blank * fix tests --------- Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch> Co-authored-by: Jovan Gerbscheid <jovan.gerbscheid@gmail.com> Co-authored-by: Joachim Breitner <mail@joachim-breitner.de> Co-authored-by: Mario Carneiro <di.gama@gmail.com> Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr> Co-authored-by: Kyle Miller <kmill31415@gmail.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR introduces an explicit
defeqattribute to mark theorems that can be used bydsimp. The benefit of an explicit attribute over the prior logic of looking at the proof body is that we can reliably omit theorem bodies across module boundaries. It also helps with intra-file parallelism.If a theorem is syntactically defined by
:= rfl, then the attribute is assumed and need not given explicitly. This is a purely syntactic check and can be fooled, e.g. if in the current namespace,rflis not actually “the”rflofEq. In that case, some other syntax has be used, such as:= (rfl). This is also the way to go if a theorem can be proved bydefeq, but one does not actually wantdsimpto use this fact.The
defeqattribute will look at the type of the declaration, not the body, to check if it really holds definitionally. Because of different reduction settings, this can sometimes go wrong. Then one should also write:= (rfl), if one does not want this to be a defeq theorem. (If one does then this is currently not possible, but it’s probably a bad idea anyways).The
set_option debug.tactic.simp.checkDefEqAttr true,dsimpwill warn if could not apply a lemma due to a missingdefeqattribute.With
set_option backward.dsimp.useDefEqAttr.get falseone can revert to the old behavior of inferring rfl-ness based on the theorem body.Both options will go away eventually (too bad we can’t mark them as deprecated right away, see #7969)
Meta programs that generate theorems (e.g. equational theorems) can use
inferDefEqAttrto set the attribute based on the theorem body of the just created declaration.This builds on #8501 to update Init to
@[expose]a fair amount of definitions that, if not exposed, would prevent some existing:= rfltheorems from beingdefeqtheorems. In the interest of starting backwards compatible, I exposed these function. Hopefully many can be un-exposed later again.A mathlib adaption branch exists that includes both the meta programming fixes and changes to the theorems (e.g. changing
:= by rflto:= rfl).With the module system there is now no special handling for
defeqtheorem bodies, because we don’t look at the body anymore. The previous hack is removed. Thedefeq-ness of the theorem needs to be checked in the context of the theorem’s type; the error message contains a hint if the defeq check fails because of the exported context.