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 diff --git a/src/Lean/Meta/Tactic/Simp/Rewrite.lean b/src/Lean/Meta/Tactic/Simp/Rewrite.lean index 595222601741..f630f6d1ab3e 100644 --- a/src/Lean/Meta/Tactic/Simp/Rewrite.lean +++ b/src/Lean/Meta/Tactic/Simp/Rewrite.lean @@ -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