From 4a14ea3a5cefe30bdd5cc1887c5f5130cc21745c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 26 Feb 2024 12:18:07 -0800 Subject: [PATCH] fix: rewrite tactic should not try to synthesize instances that have been inferred by unification (#3509) --- src/Lean/Meta/Tactic/Rewrite.lean | 2 +- tests/lean/run/rw_inst_implicit_args.lean | 15 +++++++++++++++ 2 files changed, 16 insertions(+), 1 deletion(-) create mode 100644 tests/lean/run/rw_inst_implicit_args.lean diff --git a/src/Lean/Meta/Tactic/Rewrite.lean b/src/Lean/Meta/Tactic/Rewrite.lean index 118c636d87..1ef19af389 100644 --- a/src/Lean/Meta/Tactic/Rewrite.lean +++ b/src/Lean/Meta/Tactic/Rewrite.lean @@ -52,7 +52,7 @@ def _root_.Lean.MVarId.rewrite (mvarId : MVarId) (e : Expr) (heq : Expr) let u1 ← getLevel α let u2 ← getLevel eType let eqPrf := mkApp6 (.const ``congrArg [u1, u2]) α eType lhs rhs motive heq - postprocessAppMVars `rewrite mvarId newMVars binderInfos + postprocessAppMVars `rewrite mvarId newMVars binderInfos (synthAssignedInstances := false) let newMVarIds ← newMVars.map Expr.mvarId! |>.filterM fun mvarId => not <$> mvarId.isAssigned let otherMVarIds ← getMVarsNoDelayed eqPrf let otherMVarIds := otherMVarIds.filter (!newMVarIds.contains ·) diff --git a/tests/lean/run/rw_inst_implicit_args.lean b/tests/lean/run/rw_inst_implicit_args.lean new file mode 100644 index 0000000000..7736b37b9d --- /dev/null +++ b/tests/lean/run/rw_inst_implicit_args.lean @@ -0,0 +1,15 @@ +/- +This test ensures `rw` will not try to synthesize instance implicit arguments when they can +be inferred by unification. Note that in some cases the inferred instance may not even be +definitionally equal to the inferred one, and would prevent the rewrite from being applied. +-/ +theorem dec_and (p q : Prop) [Decidable (p ∧ q)] [Decidable p] [Decidable q] : decide (p ∧ q) = (p && q) := by + by_cases p <;> by_cases q <;> simp [*] + +theorem dec_not (p : Prop) [Decidable (¬p)] [Decidable p] : decide (¬p) = !p := by + by_cases p <;> simp [*] + +example [Decidable u] [Decidable v] : decide (u ∧ (v → False)) = (decide u && !decide v) := by + simp only [imp_false] + rw [dec_and] + rw [dec_not]