chore: add simp configuration to norm_cast syntax

src/Init/Tactics.lean

@@ -1309,7 +1309,7 @@ macro "bv_omega" : tactic => `(tactic| (try simp only [bv_toNat] at *) <;> omega
 syntax (name := acNf0) "ac_nf0" (location)? : tactic
 
 /-- Implementation of `norm_cast` (the full `norm_cast` calls `trivial` afterwards). -/
-syntax (name := normCast0) "norm_cast0" (location)? : tactic
+syntax (name := normCast0) "norm_cast0" optConfig (location)? : tactic
 
 /-- `assumption_mod_cast` is a variant of `assumption` that solves the goal
 using a hypothesis. Unlike `assumption`, it first pre-processes the goal and
@@ -1358,23 +1358,6 @@ See also `push_cast`, which moves casts inwards rather than lifting them outward
 macro "norm_cast" loc:(location)? : tactic =>
   `(tactic| norm_cast0 $[$loc]? <;> try trivial)
 
-/--
-`ac_nf` normalizes equalities up to application of an associative and commutative operator.
-- `ac_nf` normalizes all hypotheses and the goal target of the goal.
-- `ac_nf at l` normalizes at location(s) `l`, where `l` is either `*` or a
-  list of hypotheses in the local context. In the latter case, a turnstile `⊢` or `|-`
-  can also be used, to signify the target of the goal.
-```
-instance : Associative (α := Nat) (.+.) := ⟨Nat.add_assoc⟩
-instance : Commutative (α := Nat) (.+.) := ⟨Nat.add_comm⟩
-
-example (a b c d : Nat) : a + b + c + d = d + (b + c) + a := by
- ac_nf
- -- goal: a + (b + (c + d)) = a + (b + (c + d))
-```
--/
-macro "ac_nf" loc:(location)? : tactic =>
-  `(tactic| ac_nf0 $[$loc]? <;> try trivial)
 
 /--
 `push_cast` rewrites the goal to move certain coercions (*casts*) inward, toward the leaf nodes.
@@ -1417,6 +1400,24 @@ syntax (name := pushCast) "push_cast" optConfig (discharger)? (&" only")?
 -/
 syntax (name := normCastAddElim) "norm_cast_add_elim" ident : command
 
+/--
+`ac_nf` normalizes equalities up to application of an associative and commutative operator.
+- `ac_nf` normalizes all hypotheses and the goal target of the goal.
+- `ac_nf at l` normalizes at location(s) `l`, where `l` is either `*` or a
+  list of hypotheses in the local context. In the latter case, a turnstile `⊢` or `|-`
+  can also be used, to signify the target of the goal.
+```
+instance : Associative (α := Nat) (.+.) := ⟨Nat.add_assoc⟩
+instance : Commutative (α := Nat) (.+.) := ⟨Nat.add_comm⟩
+
+example (a b c d : Nat) : a + b + c + d = d + (b + c) + a := by
+ ac_nf
+ -- goal: a + (b + (c + d)) = a + (b + (c + d))
+```
+-/
+macro "ac_nf" loc:(location)? : tactic =>
+  `(tactic| ac_nf0 $[$loc]? <;> try trivial)
+
 /--
 * `symm` applies to a goal whose target has the form `t ~ u` where `~` is a symmetric relation,
   that is, a relation which has a symmetry lemma tagged with the attribute [symm].

src/Lean/Elab/Tactic/NormCast.lean

@@ -168,20 +168,23 @@ def numeralToCoe (e : Expr) : MetaM Simp.Result := do
   let some pr ← proveEqUsingDown e newE | failure
   return pr
 
+structure Config extends Simp.Config where
+    zeta := false
+    beta := false
+    eta  := false
+    proj := false
+    iota := false
+
+declare_config_elab elabNormCastConfig Config
+
 /--
 The core simplification routine of `normCast`.
 -/
-def derive (e : Expr) : MetaM Simp.Result := do
+def derive (e : Expr) (config : Config := {}) : MetaM Simp.Result := do
   withTraceNode `Tactic.norm_cast (fun _ => return m!"{e}") do
   let e ← instantiateMVars e
 
-  let config : Simp.Config := {
-    zeta := false
-    beta := false
-    eta  := false
-    proj := false
-    iota := false
-  }
+  let config := config.toConfig
   let congrTheorems ← Meta.getSimpCongrTheorems
 
   let r : Simp.Result := { expr := e }
@@ -193,13 +196,13 @@ def derive (e : Expr) : MetaM Simp.Result := do
   -- step 1: pre-processing of numerals
   let r ← withTrace "pre-processing numerals" do
     let post e := return Simp.Step.done (← try numeralToCoe e catch _ => pure {expr := e})
-    let ctx ← Simp.mkContext (config := config) (congrTheorems := congrTheorems)
+    let ctx ← Simp.mkContext config (congrTheorems := congrTheorems)
     r.mkEqTrans (← Simp.main r.expr ctx (methods := { post })).1
 
   -- step 2: casts are moved upwards and eliminated
   let r ← withTrace "moving upward, splitting and eliminating" do
     let post := upwardAndElim (← normCastExt.up.getTheorems)
-    let ctx ← Simp.mkContext (config := config) (congrTheorems := congrTheorems)
+    let ctx ← Simp.mkContext config (congrTheorems := congrTheorems)
     r.mkEqTrans (← Simp.main r.expr ctx (methods := { post })).1
 
   let simprocs ← ({} : Simp.SimprocsArray).add `reduceCtorEq false
@@ -234,32 +237,33 @@ open Term
   | _ => throwUnsupportedSyntax
 
 /-- Implementation of the `norm_cast` tactic when operating on the main goal. -/
-def normCastTarget : TacticM Unit :=
+def normCastTarget (cfg : Config) : TacticM Unit :=
   liftMetaTactic1 fun goal => do
     let tgt ← instantiateMVars (← goal.getType)
-    let prf ← derive tgt
+    let prf ← derive tgt cfg
     applySimpResultToTarget goal tgt prf
 
 /-- Implementation of the `norm_cast` tactic when operating on a hypothesis. -/
-def normCastHyp (fvarId : FVarId) : TacticM Unit :=
+def normCastHyp (cfg : Config) (fvarId : FVarId) : TacticM Unit :=
   liftMetaTactic1 fun goal => do
     let hyp ← instantiateMVars (← fvarId.getDecl).type
-    let prf ← derive hyp
+    let prf ← derive hyp cfg
     return (← applySimpResultToLocalDecl goal fvarId prf false).map (·.snd)
 
 @[builtin_tactic normCast0]
 def evalNormCast0 : Tactic := fun stx => do
   match stx with
   | `(tactic| norm_cast0 $[$loc?]?) =>
     let loc := if let some loc := loc? then expandLocation loc else Location.targets #[] true
+    let cfg : Config := {} -- TODO: `← elabNormCastConfig cfg`
     withMainContext do
       match loc with
       | Location.targets hyps target =>
-        if target then normCastTarget
-        (← getFVarIds hyps).forM normCastHyp
+        if target then (normCastTarget cfg)
+        (← getFVarIds hyps).forM (normCastHyp cfg)
       | Location.wildcard =>
-        normCastTarget
-        (← (← getMainGoal).getNondepPropHyps).forM normCastHyp
+        normCastTarget cfg
+        (← (← getMainGoal).getNondepPropHyps).forM (normCastHyp cfg)
   | _ => throwUnsupportedSyntax
 
 @[builtin_tactic Lean.Parser.Tactic.Conv.normCast]