diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean index ed9f3236ea7d..7bb2d6157a36 100644 --- a/src/Init/Tactics.lean +++ b/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]. diff --git a/src/Lean/Elab/Tactic/NormCast.lean b/src/Lean/Elab/Tactic/NormCast.lean index f27113cf9355..6e544470ae7a 100644 --- a/src/Lean/Elab/Tactic/NormCast.lean +++ b/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,17 +237,17 @@ 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] @@ -252,14 +255,15 @@ 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]