Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

fix: allow simp dischargers to add aux decls to the environment #7362

Merged
merged 5 commits into from
Mar 6, 2025
Merged

fix: allow simp dischargers to add aux decls to the environment #7362

merged 5 commits into from
Mar 6, 2025

Conversation

nomeata
Copy link
Collaborator

@nomeata nomeata commented Mar 6, 2025 •
edited
Loading

This PR allows simp dischargers to add aux decls to the environment. This enables tactics like native_decide to be used here, and unblocks improvements to omega in #5998.

Fixes #7318

nomeata added 2 commits March 6, 2025 11:51
@nomeata
fix: allow simp dischargers to add aux decls to the environment
93868f9 
This PR allows simp dischargers to add aux decls to the environment.
This enables tactics like `native_decide` to be used here, and unblocks
imporvements to omega in #5998.

Fixes #7318
@nomeata
More test
9eea468
@nomeata nomeata mentioned this pull request Mar 6, 2025
Merged
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc March 6, 2025 11:11 Inactive
@nomeata nomeata force-pushed the joachim/simp-discharge-env branch 2 times, most recently from bb3c583 to abbb6aa Compare March 6, 2025 11:35
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc March 6, 2025 11:43 Inactive
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Mar 6, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Mar 6, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#7362
ab9f8a3
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Mar 6, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#7362
143d532
@leanprover-community-bot leanprover-community-bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Mar 6, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Mar 6, 2025 •
edited
Loading

Mathlib CI status (docs):

@nomeata nomeata marked this pull request as ready for review March 6, 2025 13:00
@nomeata nomeata requested a review from kim-em as a code owner March 6, 2025 13:00
@nomeata nomeata enabled auto-merge March 6, 2025 15:02
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc March 6, 2025 15:09 Inactive
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Mar 6, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#7362
eef3011
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Mar 6, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#7362
a76307c
@nomeata nomeata added the changelog-language Language features, tactics, and metaprograms label Mar 6, 2025
@nomeata nomeata added this pull request to the merge queue Mar 6, 2025
Merged via the queue into master with commit 20d191b Mar 6, 2025
20 of 21 checks passed
github-merge-queue bot pushed a commit that referenced this pull request Mar 10, 2025
@nomeata
feat: omega to abstract its own proofs (#5998)
754bab4 
This PR lets `omega` always abstract its own proofs into an auxiliary
definition. The size of the olean of Vector.Extract goes down from 20MB
to 5MB with this, overall stdlib olean size and build instruction count
go down 5%.

Needs #7362.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@kim-em kim-em Awaiting requested review from kim-em kim-em is a code owner

Assignees
No one assigned
Labels
builds-mathlib CI has verified that Mathlib builds against this PR changelog-language Language features, tactics, and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

cannot use ax_aux_lemma or native_decide in simp discharger
2 participants
@nomeata @leanprover-community-bot