feat: simp config opts in norm_num (#7112)

This adds support for `norm_num (config := ...)`, which just forwards the config args to `simp`. The case of `{decide := false}` came up in https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Prove.20decidable.20statement.20by.20evaluation/near/390390131 .



Co-authored-by: Mario Carneiro <di.gama@gmail.com>

Author: digama0

Mathlib/Tactic/NormNum/Core.lean

@@ -270,13 +270,13 @@ def normNumAt (g : MVarId) (ctx : Simp.Context) (fvarIdsToSimp : Array FVarId)
 
 open Tactic in
 /-- Constructs a simp context from the simp argument syntax. -/
-def getSimpContext (args : Syntax) (simpOnly := false) :
-    TacticM Simp.Context := do
+def getSimpContext (cfg args : Syntax) (simpOnly := false) : TacticM Simp.Context := do
+  let config ← elabSimpConfigCore cfg
   let simpTheorems ←
     if simpOnly then simpOnlyBuiltins.foldlM (·.addConst ·) {} else getSimpTheorems
   let mut { ctx, simprocs := _, starArg } ←
     elabSimpArgs args[0] (eraseLocal := false) (kind := .simp) (simprocs := {})
-    { simpTheorems := #[simpTheorems], congrTheorems := ← getSimpCongrTheorems }
+      { config, simpTheorems := #[simpTheorems], congrTheorems := ← getSimpCongrTheorems }
   unless starArg do return ctx
   let mut simpTheorems := ctx.simpTheorems
   for h in ← getPropHyps do
@@ -294,9 +294,8 @@ Elaborates a call to `norm_num only? [args]` or `norm_num1`.
   of `simp` will be used, not any of the post-processing that `simp only` does without lemmas
 -/
 -- FIXME: had to inline a bunch of stuff from `mkSimpContext` and `simpLocation` here
-def elabNormNum (args : Syntax) (loc : Syntax)
-    (simpOnly := false) (useSimp := true) : TacticM Unit := do
-  let ctx ← getSimpContext args (!useSimp || simpOnly)
+def elabNormNum (cfg args loc : Syntax) (simpOnly := false) (useSimp := true) : TacticM Unit := do
+  let ctx ← getSimpContext cfg args (!useSimp || simpOnly)
   let g ← getMainGoal
   let res ← match expandOptLocation loc with
   | .targets hyps simplifyTarget => normNumAt g ctx (← getFVarIds hyps) simplifyTarget useSimp
@@ -316,27 +315,29 @@ over numerical types such as `ℕ`, `ℤ`, `ℚ`, `ℝ`, `ℂ` and some general
 and can prove goals of the form `A = B`, `A ≠ B`, `A < B` and `A ≤ B`, where `A` and `B` are
 numerical expressions. It also has a relatively simple primality prover.
 -/
-elab (name := normNum) "norm_num" only:&" only"? args:(simpArgs ?) loc:(location ?) : tactic =>
-  elabNormNum args loc (simpOnly := only.isSome) (useSimp := true)
+elab (name := normNum)
+    "norm_num" cfg:(config ?) only:&" only"? args:(simpArgs ?) loc:(location ?) : tactic =>
+  elabNormNum cfg args loc (simpOnly := only.isSome) (useSimp := true)
 
 /-- Basic version of `norm_num` that does not call `simp`. -/
 elab (name := normNum1) "norm_num1" loc:(location ?) : tactic =>
-  elabNormNum mkNullNode loc (simpOnly := true) (useSimp := false)
+  elabNormNum mkNullNode mkNullNode loc (simpOnly := true) (useSimp := false)
 
 open Lean Elab Tactic
 
 @[inherit_doc normNum1] syntax (name := normNum1Conv) "norm_num1" : conv
 
 /-- Elaborator for `norm_num1` conv tactic. -/
 @[tactic normNum1Conv] def elabNormNum1Conv : Tactic := fun _ ↦ withMainContext do
-  let ctx ← getSimpContext mkNullNode true
+  let ctx ← getSimpContext mkNullNode mkNullNode true
   Conv.applySimpResult (← deriveSimp ctx (← instantiateMVars (← Conv.getLhs)) (useSimp := false))
 
-@[inherit_doc normNum] syntax (name := normNumConv) "norm_num" &" only"? (simpArgs)? : conv
+@[inherit_doc normNum] syntax (name := normNumConv)
+    "norm_num" (config)? &" only"? (simpArgs)? : conv
 
 /-- Elaborator for `norm_num` conv tactic. -/
 @[tactic normNumConv] def elabNormNumConv : Tactic := fun stx ↦ withMainContext do
-  let ctx ← getSimpContext stx[2] !stx[1].isNone
+  let ctx ← getSimpContext stx[1] stx[3] !stx[2].isNone
   Conv.applySimpResult (← deriveSimp ctx (← instantiateMVars (← Conv.getLhs)) (useSimp := true))
 
 /--
@@ -355,6 +356,6 @@ Unlike `norm_num`, this command does not fail when no simplifications are made.
 
 `#norm_num` understands local variables, so you can use them to introduce parameters.
 -/
-macro (name := normNumCmd) "#norm_num" o:(&" only")?
+macro (name := normNumCmd) "#norm_num" cfg:(config)? o:(&" only")?
     args:(Parser.Tactic.simpArgs)? " :"? ppSpace e:term : command =>
-  `(command| #conv norm_num $[only%$o]? $(args)? => $e)
+  `(command| #conv norm_num $(cfg)? $[only%$o]? $(args)? => $e)

test/norm_num_ext.lean

@@ -105,6 +105,8 @@ set_option maxRecDepth 8000 in
 example : Nat.Prime (2 ^ 25 - 39) := by norm_num1
 example : ¬ Nat.Prime ((2 ^ 19 - 1) * (2 ^ 25 - 39)) := by norm_num1
 
+example : Nat.Prime 317 := by norm_num (config := {decide := false})
+
 example : Nat.minFac 0 = 2 := by norm_num1
 example : Nat.minFac 1 = 1 := by norm_num1
 example : Nat.minFac (9 - 7) = 2 := by norm_num1
@@ -266,43 +268,40 @@ example : Nat.minFac 851 = 23 := by norm_num1
 -- example : Nat.factors 851 = [23, 37] := by norm_num1
 
 /-
-example : ¬ squarefree 0 := by norm_num
-example : squarefree 1 := by norm_num
-example : squarefree 2 := by norm_num
-example : squarefree 3 := by norm_num
-example : ¬ squarefree 4 := by norm_num
-example : squarefree 5 := by norm_num
-example : squarefree 6 := by norm_num
-example : squarefree 7 := by norm_num
-example : ¬ squarefree 8 := by norm_num
-example : ¬ squarefree 9 := by norm_num
-example : squarefree 10 := by norm_num
-example : squarefree (2*3*5*17) := by norm_num
-example : ¬ squarefree (2*3*5*5*17) := by norm_num
-example : squarefree 251 := by norm_num
-example : squarefree (3 : ℤ) :=
-begin
+example : ¬ Squarefree 0 := by norm_num1
+example : Squarefree 1 := by norm_num1
+example : Squarefree 2 := by norm_num1
+example : Squarefree 3 := by norm_num1
+example : ¬ Squarefree 4 := by norm_num1
+example : Squarefree 5 := by norm_num1
+example : Squarefree 6 := by norm_num1
+example : Squarefree 7 := by norm_num1
+example : ¬ Squarefree 8 := by norm_num1
+example : ¬ Squarefree 9 := by norm_num1
+example : Squarefree 10 := by norm_num1
+example : Squarefree (2*3*5*17) := by norm_num1
+example : ¬ Squarefree (2*3*5*5*17) := by norm_num1
+example : Squarefree 251 := by norm_num1
+example : Squarefree (3 : ℤ) := by
   -- `norm_num` should fail on this example, instead of producing an incorrect proof.
-  success_if_fail { norm_num },
-  exact irreducible.squarefree (prime.irreducible
-    (Int.prime_iff_Nat_abs_prime.mpr (by norm_num)))
-end
-example : @squarefree ℕ multiplicative.monoid 1 :=
-begin
+  fail_if_success norm_num1
+  exact Irreducible.squarefree (Prime.irreducible
+    (Int.prime_iff_natAbs_prime.mpr (by norm_num)))
+
+example : @Squarefree ℕ Multiplicative.monoid 1 := by
   -- `norm_num` should fail on this example, instead of producing an incorrect proof.
-  success_if_fail { norm_num },
+  -- fail_if_success norm_num1
   -- the statement was deliberately wacky, let's fix it
-  change squarefree (multiplicative.of_add 1 : multiplicative ℕ),
-  rIntros x ⟨dx, hd⟩,
-  revert x dx,
-  rw multiplicative.of_add.surjective.forall₂,
-  Intros x dx h,
-  simp_rw [←of_add_add, multiplicative.of_add.injective.eq_iff] at h,
-  cases x,
-  { simp [is_unit_one], exact is_unit_one },
-  { simp only [Nat.succ_add, Nat.add_succ] at h,
-    cases h },
-end
+  change Squarefree (Multiplicative.ofAdd 1 : Multiplicative ℕ)
+  rintro x ⟨dx, hd⟩
+  revert x dx
+  rw [Multiplicative.ofAdd.surjective.forall₂]
+  intros x dx h
+  simp_rw [← ofAdd_add, Multiplicative.ofAdd.injective.eq_iff] at h
+  cases x
+  · simp [isUnit_one]
+  · simp only [Nat.succ_add, Nat.add_succ] at h
+    cases h
 -/
 
 example : Nat.fib 0 = 0 := by norm_num1
@@ -331,23 +330,22 @@ open BigOperators
 
 -- Lists:
 -- `by decide` closes the three goals below.
-/-
-example : ([1, 2, 1, 3]).sum = 7 := by norm_num only
-example : (List.range 10).sum = 45 := by norm_num only
-example : (List.finRange 10).sum = 45 := by norm_num only
--/
--- example : (([1, 2, 1, 3] : List ℚ).map (fun i => i^2)).sum = 15 := by norm_num [-List.map] --TODO
+example : ([1, 2, 1, 3]).sum = 7 := by norm_num (config := {decide := true}) only
+example : (List.range 10).sum = 45 := by norm_num (config := {decide := true}) only
+example : (List.finRange 10).sum = 45 := by norm_num (config := {decide := true}) only
+
+example : (([1, 2, 1, 3] : List ℚ).map (fun i => i^2)).sum = 15 := by norm_num
 
 -- Multisets:
 -- `by decide` closes the three goals below.
-/-
-example : (1 ::ₘ 2 ::ₘ 1 ::ₘ 3 ::ₘ {}).sum = 7 := by norm_num only
-example : ((1 ::ₘ 2 ::ₘ 1 ::ₘ 3 ::ₘ {}).map (fun i => i^2)).sum = 15 := by norm_num only
-example : (Multiset.range 10).sum = 45 := by norm_num only
-example : (↑[1, 2, 1, 3] : Multiset ℕ).sum = 7 := by norm_num only
--/
--- example : (({1, 2, 1, 3} : Multiset ℚ).map (fun i => i^2)).sum = 15 := by -- TODO
---   norm_num [-Multiset.map_cons]
+example : (1 ::ₘ 2 ::ₘ 1 ::ₘ 3 ::ₘ {}).sum = 7 := by norm_num (config := {decide := true}) only
+example : ((1 ::ₘ 2 ::ₘ 1 ::ₘ 3 ::ₘ {}).map (fun i => i^2)).sum = 15 := by
+  norm_num (config := {decide := true}) only
+example : (Multiset.range 10).sum = 45 := by norm_num (config := {decide := true}) only
+example : (↑[1, 2, 1, 3] : Multiset ℕ).sum = 7 := by norm_num (config := {decide := true}) only
+
+example : (({1, 2, 1, 3} : Multiset ℚ).map (fun i => i^2)).sum = 15 := by
+  norm_num
 
 -- Finsets:
 example : Finset.prod (Finset.cons 2 ∅ (Finset.not_mem_empty _)) (λ x => x) = 2 := by norm_num1
@@ -384,14 +382,12 @@ example (f : ℕ → α) : ∑ i in Finset.mk {0, 1, 2} dec_trivial, f i = f 0 +
 -/
 
 -- Combined with other `norm_num` extensions:
-/-
 example : ∏ i in Finset.range 9, Nat.sqrt (i + 1) = 96 := by norm_num1
-example : ∏ i in {1, 4, 9, 16}, Nat.sqrt i = 24 := by norm_num1
-example : ∏ i in Finset.Icc 0 8, Nat.sqrt (i + 1) = 96 := by norm_num1
+-- example : ∏ i in {1, 4, 9, 16}, Nat.sqrt i = 24 := by norm_num1
+-- example : ∏ i in Finset.Icc 0 8, Nat.sqrt (i + 1) = 96 := by norm_num1
 
 -- Nested operations:
-example : ∑ i : Fin 2, ∑ j : Fin 2, ![![0, 1], ![2, 3]] i j = 6 := by norm_num1
--/
+-- example : ∑ i : Fin 2, ∑ j : Fin 2, ![![0, 1], ![2, 3]] i j = 6 := by norm_num1
 
 end big_operators