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

feat: try more specific matches first in simp #7195

Draft
wants to merge 4 commits into
base: master
Choose a base branch
from
Draft

feat: try more specific matches first in simp #7195

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
7506cd7
feat: try more specific matches first in `simp`
JovanGerb Feb 23, 2025
f679991
oops, no actually reverse the array
JovanGerb Feb 24, 2025
8282b6a
initiate build
JovanGerb Feb 24, 2025
a544543
increase prio for
JovanGerb Feb 24, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 2 additions & 1 deletion src/Lean/Elab/Tactic/Simp.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -342,7 +342,8 @@ def mkSimpContext (stx : Syntax) (eraseLocal : Bool) (kind := SimpKind.simp)
let dischargeWrapper ← mkDischargeWrapper stx[2]
let simpOnly := !stx[simpOnlyPos].isNone
let simpTheorems ← if simpOnly then
simpOnlyBuiltins.foldlM (·.addConst ·) ({} : SimpTheorems)
-- `eq_self` and `iff_self` are given a priority just above default, since they prove the goal
simpOnlyBuiltins.foldlM (·.addConst · (prio := eval_prio default+10)) ({} : SimpTheorems)
else
simpTheorems
let simprocs ← if simpOnly then pure {} else Simp.getSimprocs
Expand Down
3 changes: 2 additions & 1 deletion src/Lean/Meta/Tactic/Simp/Rewrite.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -216,7 +216,8 @@ where
trace[Debug.Meta.Tactic.simp] "no theorems found for {tag}-rewriting {e}"
return none
else
let candidates := candidates.insertionSort fun e₁ e₂ => e₁.1.priority > e₂.1.priority
-- `candidates` is reversed so that more specific matches are tried first
let candidates := candidates.reverse.insertionSort fun e₁ e₂ => e₁.1.priority > e₂.1.priority
for (thm, numExtraArgs) in candidates do
unless inErasedSet thm || (rflOnly && !thm.rfl) do
if let some result ← tryTheoremWithExtraArgs? e thm numExtraArgs then
Expand Down
Loading