From 7506cd7752097d66c44c6533559bd9bfe4034388 Mon Sep 17 00:00:00 2001 From: Jovan Gerbscheid Date: Sun, 23 Feb 2025 17:41:11 +0000 Subject: [PATCH 1/4] feat: try more specific matches first in `simp` --- src/Lean/Meta/Tactic/Simp/Rewrite.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/src/Lean/Meta/Tactic/Simp/Rewrite.lean b/src/Lean/Meta/Tactic/Simp/Rewrite.lean index 595222601741..bad6de4d1d3c 100644 --- a/src/Lean/Meta/Tactic/Simp/Rewrite.lean +++ b/src/Lean/Meta/Tactic/Simp/Rewrite.lean @@ -216,6 +216,7 @@ where trace[Debug.Meta.Tactic.simp] "no theorems found for {tag}-rewriting {e}" return none else + -- `candidates` is reversed so that more specific matches are tried first let candidates := candidates.insertionSort fun e₁ e₂ => e₁.1.priority > e₂.1.priority for (thm, numExtraArgs) in candidates do unless inErasedSet thm || (rflOnly && !thm.rfl) do From f67999196e4f9518303a87d7fe7fc734c03beebf Mon Sep 17 00:00:00 2001 From: Jovan Gerbscheid Date: Mon, 24 Feb 2025 14:29:06 +0000 Subject: [PATCH 2/4] oops, no actually reverse the array --- src/Lean/Meta/Tactic/Simp/Rewrite.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Meta/Tactic/Simp/Rewrite.lean b/src/Lean/Meta/Tactic/Simp/Rewrite.lean index bad6de4d1d3c..f630f6d1ab3e 100644 --- a/src/Lean/Meta/Tactic/Simp/Rewrite.lean +++ b/src/Lean/Meta/Tactic/Simp/Rewrite.lean @@ -217,7 +217,7 @@ where return none else -- `candidates` is reversed so that more specific matches are tried first - let candidates := candidates.insertionSort fun e₁ e₂ => e₁.1.priority > e₂.1.priority + 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 From 8282b6ab93cfff866eae83a8b245cdce5e9ebd37 Mon Sep 17 00:00:00 2001 From: Jovan Gerbscheid Date: Mon, 24 Feb 2025 18:23:21 +0000 Subject: [PATCH 3/4] initiate build From a544543dc6672ed7a3ca09857aba668a64b369f8 Mon Sep 17 00:00:00 2001 From: Jovan Gerbscheid Date: Mon, 24 Feb 2025 19:44:36 +0000 Subject: [PATCH 4/4] increase prio for --- src/Lean/Elab/Tactic/Simp.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/Lean/Elab/Tactic/Simp.lean b/src/Lean/Elab/Tactic/Simp.lean index 1616aa69e1c0..8373be635d2b 100644 --- a/src/Lean/Elab/Tactic/Simp.lean +++ b/src/Lean/Elab/Tactic/Simp.lean @@ -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