feat: restore reduceCtorEq in norm_cast tactic (#5187)

#5167 removed `reduceCtorEq` from the default simproc set. `norm_cast` relies on it, so we add it back in there.
leanprover · Aug 28, 2024 · 0dc317c · 0dc317c
1 parent 4436638
commit 0dc317c
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 1 deletion.
diff --git a/src/Lean/Elab/Tactic/NormCast.lean b/src/Lean/Elab/Tactic/NormCast.lean
@@ -198,10 +198,12 @@ def derive (e : Expr) : MetaM Simp.Result := do
     let post := upwardAndElim (← normCastExt.up.getTheorems)
     r.mkEqTrans (← Simp.main r.expr { config, congrTheorems } (methods := { post })).1
 
+  let simprocs ← ({} : Simp.SimprocsArray).add `reduceCtorEq false
+
   -- step 3: casts are squashed
   let r ← withTrace "squashing" do
     let simpTheorems := #[← normCastExt.squash.getTheorems]
-    r.mkEqTrans (← simp r.expr { simpTheorems, config, congrTheorems }).1
+    r.mkEqTrans (← simp r.expr { simpTheorems, config, congrTheorems } simprocs).1
 
   return r
 

diff --git a/tests/lean/run/norm_cast.lean b/tests/lean/run/norm_cast.lean
@@ -82,3 +82,6 @@ theorem b (_h g : true) : true ∧ true := by
   constructor
   assumption_mod_cast
   assumption_mod_cast
+
+example : ¬n - k + 1 = 0 := by
+  norm_cast