chore(Tactic/{Positivity,NormNum}): remove support for non-canonical spellings (#10344)

`Mul.mul` or `Nat.mul` etc should not ever appear in a goal, so there is little reason for these tactics to support them.
If these are in your goal, then something has already gone wrong and `norm_num` isn't responsible for saving you; that's `simp` or `dsimp`'s job.


[Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.2310344.20removing.20norm_num.20support.20for.20Nat.2Esub.2C.20Sub.2Esub.2C.20etc/near/420507739)

Author: eric-wieser

Mathlib/Analysis/SpecialFunctions/Pow/Real.lean

@@ -350,7 +350,7 @@ open Lean Meta Qq
 
 /-- Extension for the `positivity` tactic: exponentiation by a real number is positive (namely 1)
 when the exponent is zero. The other cases are done in `evalRpow`. -/
-@[positivity (_ : ℝ) ^ (0 : ℝ), Pow.pow (_ : ℝ) (0 : ℝ), Real.rpow (_ : ℝ) (0 : ℝ)]
+@[positivity (_ : ℝ) ^ (0 : ℝ)]
 def evalRpowZero : PositivityExt where eval {_ _} _ _ e := do
   let .app (.app (f : Q(ℝ → ℝ → ℝ)) (a : Q(ℝ))) (_ : Q(ℝ)) ← withReducible (whnf e)
     | throwError "not Real.rpow"
@@ -359,7 +359,7 @@ def evalRpowZero : PositivityExt where eval {_ _} _ _ e := do
 
 /-- Extension for the `positivity` tactic: exponentiation by a real number is nonnegative when
 the base is nonnegative and positive when the base is positive. -/
-@[positivity (_ : ℝ) ^ (_ : ℝ), Pow.pow (_ : ℝ) (_ : ℝ), Real.rpow (_ : ℝ) (_ : ℝ)]
+@[positivity (_ : ℝ) ^ (_ : ℝ)]
 def evalRpow : PositivityExt where eval {_ _} zα pα e := do
   let .app (.app (f : Q(ℝ → ℝ → ℝ)) (a : Q(ℝ))) (b : Q(ℝ)) ← withReducible (whnf e)
     | throwError "not Real.rpow"

Mathlib/Tactic/NormNum/Basic.lean

@@ -202,7 +202,7 @@ instance : MonadLift Option MetaM where
 
 /-- The `norm_num` extension which identifies expressions of the form `a + b`,
 such that `norm_num` successfully recognises both `a` and `b`. -/
-@[norm_num _ + _, Add.add _ _] def evalAdd : NormNumExt where eval {u α} e := do
+@[norm_num _ + _] def evalAdd : NormNumExt where eval {u α} e := do
   let .app (.app (f : Q($α → $α → $α)) (a : Q($α))) (b : Q($α)) ← whnfR e | failure
   let ra ← derive a; let rb ← derive b
   match ra, rb with
@@ -310,7 +310,7 @@ theorem isRat_sub {α} [Ring α] {f : α → α → α} {a b : α} {na nb nc : 
 
 /-- The `norm_num` extension which identifies expressions of the form `a - b` in a ring,
 such that `norm_num` successfully recognises both `a` and `b`. -/
-@[norm_num _ - _, Sub.sub _ _] def evalSub : NormNumExt where eval {u α} e := do
+@[norm_num _ - _] def evalSub : NormNumExt where eval {u α} e := do
   let .app (.app (f : Q($α → $α → $α)) (a : Q($α))) (b : Q($α)) ← whnfR e | failure
   let rα ← inferRing α
   let ⟨(_f_eq : $f =Q HSub.hSub)⟩ ← withNewMCtxDepth <| assertDefEqQ _ _
@@ -380,7 +380,7 @@ theorem isRat_mul {α} [Ring α] {f : α → α → α} {a b : α} {na nb nc : 
 
 /-- The `norm_num` extension which identifies expressions of the form `a * b`,
 such that `norm_num` successfully recognises both `a` and `b`. -/
-@[norm_num _ * _, Mul.mul _ _] def evalMul : NormNumExt where eval {u α} e := do
+@[norm_num _ * _] def evalMul : NormNumExt where eval {u α} e := do
   let .app (.app (f : Q($α → $α → $α)) (a : Q($α))) (b : Q($α)) ← whnfR e | failure
   let sα ← inferSemiring α
   let ra ← derive a; let rb ← derive b
@@ -433,7 +433,7 @@ def inferDivisionRing (α : Q(Type u)) : MetaM Q(DivisionRing $α) :=
 
 /-- The `norm_num` extension which identifies expressions of the form `a / b`,
 such that `norm_num` successfully recognises both `a` and `b`. -/
-@[norm_num _ / _, Div.div _ _] def evalDiv : NormNumExt where eval {u α} e := do
+@[norm_num _ / _] def evalDiv : NormNumExt where eval {u α} e := do
   let .app (.app f (a : Q($α))) (b : Q($α)) ← whnfR e | failure
   let dα ← inferDivisionRing α
   haveI' : $e =Q $a / $b := ⟨⟩
@@ -509,7 +509,7 @@ theorem isNat_natSub : {a b : ℕ} → {a' b' c : ℕ} →
 
 /-- The `norm_num` extension which identifies expressions of the form `Nat.sub a b`,
 such that `norm_num` successfully recognises both `a` and `b`. -/
-@[norm_num (_ : ℕ) - _, Sub.sub (_ : ℕ) _, Nat.sub _ _] def evalNatSub :
+@[norm_num (_ : ℕ) - _] def evalNatSub :
     NormNumExt where eval {u α} e := do
   let .app (.app f (a : Q(ℕ))) (b : Q(ℕ)) ← whnfR e | failure
   -- We assert that the default instance for `HSub` is `Nat.sub` when the first parameter is `ℕ`.
@@ -528,7 +528,7 @@ theorem isNat_natMod : {a b : ℕ} → {a' b' c : ℕ} →
 
 /-- The `norm_num` extension which identifies expressions of the form `Nat.mod a b`,
 such that `norm_num` successfully recognises both `a` and `b`. -/
-@[norm_num (_ : ℕ) % _, Mod.mod (_ : ℕ) _, Nat.mod _ _] def evalNatMod :
+@[norm_num (_ : ℕ) % _] def evalNatMod :
     NormNumExt where eval {u α} e := do
   let .app (.app f (a : Q(ℕ))) (b : Q(ℕ)) ← whnfR e | failure
   haveI' : u =QL 0 := ⟨⟩; haveI' : $α =Q ℕ := ⟨⟩
@@ -547,7 +547,7 @@ theorem isNat_natDiv : {a b : ℕ} → {a' b' c : ℕ} →
 
 /-- The `norm_num` extension which identifies expressions of the form `Nat.div a b`,
 such that `norm_num` successfully recognises both `a` and `b`. -/
-@[norm_num (_ : ℕ) / _, Div.div (_ : ℕ) _, Nat.div _ _]
+@[norm_num (_ : ℕ) / _]
 def evalNatDiv : NormNumExt where eval {u α} e := do
   let .app (.app f (a : Q(ℕ))) (b : Q(ℕ)) ← whnfR e | failure
   haveI' : u =QL 0 := ⟨⟩; haveI' : $α =Q ℕ := ⟨⟩

Mathlib/Tactic/NormNum/DivMod.lean

@@ -42,7 +42,7 @@ lemma isNat_neg_of_isNegNat {a : ℤ} {b : ℕ} (h : IsInt a (.negOfNat b)) : Is
 
 /-- The `norm_num` extension which identifies expressions of the form `Int.ediv a b`,
 such that `norm_num` successfully recognises both `a` and `b`. -/
-@[norm_num (_ : ℤ) / _, Div.div (_ : ℤ) _, Int.ediv _ _]
+@[norm_num (_ : ℤ) / _, Int.ediv _ _]
 partial def evalIntDiv : NormNumExt where eval {u α} e := do
   let .app (.app f (a : Q(ℤ))) (b : Q(ℤ)) ← whnfR e | failure
   -- We assert that the default instance for `HDiv` is `Int.div` when the first parameter is `ℤ`.
@@ -100,7 +100,7 @@ lemma isInt_emod_neg {a b : ℤ} {r : ℕ} (h : IsNat (a % -b) r) : IsNat (a % b
 
 /-- The `norm_num` extension which identifies expressions of the form `Int.emod a b`,
 such that `norm_num` successfully recognises both `a` and `b`. -/
-@[norm_num (_ : ℤ) % _, Mod.mod (_ : ℤ) _, Int.emod _ _]
+@[norm_num (_ : ℤ) % _, Int.emod _ _]
 partial def evalIntMod : NormNumExt where eval {u α} e := do
   let .app (.app f (a : Q(ℤ))) (b : Q(ℤ)) ← whnfR e | failure
   -- We assert that the default instance for `HMod` is `Int.mod` when the first parameter is `ℤ`.

Mathlib/Tactic/NormNum/Eq.lean

@@ -36,7 +36,7 @@ theorem isRat_eq_false [Ring α] [CharZero α] : {a b : α} → {na nb : ℤ} 
 
 /-- The `norm_num` extension which identifies expressions of the form `a = b`,
 such that `norm_num` successfully recognises both `a` and `b`. -/
-@[norm_num _ = _, Eq _ _] def evalEq : NormNumExt where eval {v β} e := do
+@[norm_num _ = _] def evalEq : NormNumExt where eval {v β} e := do
   haveI' : v =QL 0 := ⟨⟩; haveI' : $β =Q Prop := ⟨⟩
   let .app (.app f a) b ← whnfR e | failure
   let ⟨u, α, a⟩ ← inferTypeQ' a

Mathlib/Tactic/NormNum/Pow.lean

@@ -163,7 +163,7 @@ theorem isRat_pow {α} [Ring α] {f : α → ℕ → α} {a : α} {an cn : ℤ}
 
 /-- The `norm_num` extension which identifies expressions of the form `a ^ b`,
 such that `norm_num` successfully recognises both `a` and `b`, with `b : ℕ`. -/
-@[norm_num (_ : α) ^ (_ : ℕ), Pow.pow _ (_ : ℕ)]
+@[norm_num (_ : α) ^ (_ : ℕ)]
 def evalPow : NormNumExt where eval {u α} e := do
   let .app (.app (f : Q($α → ℕ → $α)) (a : Q($α))) (b : Q(ℕ)) ← whnfR e | failure
   let ⟨nb, pb⟩ ← deriveNat b q(instAddMonoidWithOneNat)

Mathlib/Tactic/Positivity/Basic.lean

@@ -148,7 +148,7 @@ is nonnegative, strictly positive if at least one is positive, and nonzero if bo
 
 /-- The `positivity` extension which identifies expressions of the form `a + b`,
 such that `positivity` successfully recognises both `a` and `b`. -/
-@[positivity _ + _, Add.add _ _] def evalAdd : PositivityExt where eval {u α} zα pα e := do
+@[positivity _ + _] def evalAdd : PositivityExt where eval {u α} zα pα e := do
   let .app (.app (f : Q($α → $α → $α)) (a : Q($α))) (b : Q($α)) ← withReducible (whnf e)
     | throwError "not +"
   let _e_eq : $e =Q $f $a $b := ⟨⟩
@@ -189,7 +189,7 @@ private theorem mul_ne_zero_of_pos_of_ne_zero [OrderedSemiring α] [NoZeroDiviso
 
 /-- The `positivity` extension which identifies expressions of the form `a * b`,
 such that `positivity` successfully recognises both `a` and `b`. -/
-@[positivity _ * _, Mul.mul _ _] def evalMul : PositivityExt where eval {u α} zα pα e := do
+@[positivity _ * _] def evalMul : PositivityExt where eval {u α} zα pα e := do
   let .app (.app (f : Q($α → $α → $α)) (a : Q($α))) (b : Q($α)) ← withReducible (whnf e)
     | throwError "not *"
   let _e_eq : $e =Q $f $a $b := ⟨⟩
@@ -251,7 +251,7 @@ private theorem pow_zero_pos [OrderedSemiring α] [Nontrivial α] (a : α) : 0 <
 
 /-- The `positivity` extension which identifies expressions of the form `a ^ (0:ℕ)`.
 This extension is run in addition to the general `a ^ b` extension (they are overlapping). -/
-@[positivity (_ : α) ^ (0:ℕ), Pow.pow _ (0:ℕ)]
+@[positivity (_ : α) ^ (0:ℕ)]
 def evalPowZeroNat : PositivityExt where eval {u α} _zα _pα e := do
   let .app (.app _ (a : Q($α))) _ ← withReducible (whnf e) | throwError "not ^"
   _ ← synthInstanceQ (q(OrderedSemiring $α) : Q(Type u))
@@ -261,7 +261,7 @@ def evalPowZeroNat : PositivityExt where eval {u α} _zα _pα e := do
 set_option linter.deprecated false in
 /-- The `positivity` extension which identifies expressions of the form `a ^ (b : ℕ)`,
 such that `positivity` successfully recognises both `a` and `b`. -/
-@[positivity (_ : α) ^ (_ : ℕ), Pow.pow _ (_ : ℕ)]
+@[positivity (_ : α) ^ (_ : ℕ)]
 def evalPow : PositivityExt where eval {u α} zα pα e := do
   let .app (.app _ (a : Q($α))) (b : Q(ℕ)) ← withReducible (whnf e) | throwError "not ^"
   let result ← catchNone do

test/norm_num.lean

@@ -415,7 +415,7 @@ example : 10 / 1 = 10 := by norm_num1
 example : 5 / 4 = 1 := by norm_num1
 example : 9 / 4 = 2 := by norm_num1
 example : 0 / 1 = 0 := by norm_num1
-example : Nat.div 10 9 = 1 := by norm_num1
+example : 10 / 9 = 1 := by norm_num1
 example : 1099 / 100 = 10 := by norm_num1
 
 end Nat.div
@@ -521,18 +521,6 @@ section
   example : - (-4 / 3) = 1 / (3 / (4 : α)) := by norm_num1
 end
 
-section Transparency
-
-example : Add.add 10 2 = 12 := by norm_num1
-example : Nat.sub 10 1 = 9 := by norm_num1
-example : Nat.mod 10 5 = 0 := by norm_num1
-example : Sub.sub 10 1 = 9 := by norm_num1
-example : Sub.sub 10 (-2) = 12 := by norm_num1
-example : Mul.mul 10 1 = 10 := by norm_num1
-example : (Div.div 10 1 : ℚ) = 10 := by norm_num1
-
-end Transparency
-
 -- user command
 
 /-- info: True -/