feat(tactic/norm_num): permit disabling the calculation of /, %, …

…`∣` (#16588)

For teaching, I would like to be able to turn off `norm_num`'s power to calculate `/`, `%`, `∣`.  This can be achieved by moving `norm_num.eval_nat_succ_ext` from the core tactic to an extension, so that it can be locally disabled with

```lean
local attribute [-norm_num] norm_num.eval_nat_int_ext
```

(Interested users: note that this is only useful if you also make `int.has_div`, `nat.has_dvd`, etc irreducible with

```lean
local attribute [irreducible] int.has_div nat.has_dvd ...
```

since otherwise many of these goals can be solved by `refl`.)

Zulip:
https://leanprover.zulipchat.com/#narrow/stream/239415-metaprogramming-.2F-tactics/topic/Selectively.20weaken.20norm_num

src/tactic/norm_num.lean

@@ -1177,69 +1177,6 @@ meta def prove_nat_succ (ic : instance_cache) : expr → tactic (instance_cache
   p ← mk_eq_refl e,
   return (ic, n, e, p)
 
-lemma nat_div (a b q r m : ℕ) (hm : q * b = m) (h : r + m = a) (h₂ : r < b) : a / b = q :=
-by rw [← h, ← hm, nat.add_mul_div_right _ _ (lt_of_le_of_lt (nat.zero_le _) h₂),
-       nat.div_eq_of_lt h₂, zero_add]
-
-lemma int_div (a b q r m : ℤ) (hm : q * b = m) (h : r + m = a) (h₁ : 0 ≤ r) (h₂ : r < b) :
-  a / b = q :=
-by rw [← h, ← hm, int.add_mul_div_right _ _ (ne_of_gt (lt_of_le_of_lt h₁ h₂)),
-       int.div_eq_zero_of_lt h₁ h₂, zero_add]
-
-lemma nat_mod (a b q r m : ℕ) (hm : q * b = m) (h : r + m = a) (h₂ : r < b) : a % b = r :=
-by rw [← h, ← hm, nat.add_mul_mod_self_right, nat.mod_eq_of_lt h₂]
-
-lemma int_mod (a b q r m : ℤ) (hm : q * b = m) (h : r + m = a) (h₁ : 0 ≤ r) (h₂ : r < b) :
-  a % b = r :=
-by rw [← h, ← hm, int.add_mul_mod_self, int.mod_eq_of_lt h₁ h₂]
-
-lemma int_div_neg (a b c' c : ℤ) (h : a / b = c') (h₂ : -c' = c) : a / -b = c :=
-h₂ ▸ h ▸ int.div_neg _ _
-
-lemma int_mod_neg (a b c : ℤ) (h : a % b = c) : a % -b = c :=
-(int.mod_neg _ _).trans h
-
-/-- Given `a`,`b` numerals in `nat` or `int`,
-  * `prove_div_mod ic a b ff` returns `(c, ⊢ a / b = c)`
-  * `prove_div_mod ic a b tt` returns `(c, ⊢ a % b = c)`
--/
-meta def prove_div_mod (ic : instance_cache) :
-  expr → expr → bool → tactic (instance_cache × expr × expr)
-| a b mod :=
-  match match_neg b with
-  | some b := do
-    (ic, c', p) ← prove_div_mod a b mod,
-    if mod then
-      return (ic, c', `(int_mod_neg).mk_app [a, b, c', p])
-    else do
-      (ic, c, p₂) ← prove_neg ic c',
-      return (ic, c, `(int_div_neg).mk_app [a, b, c', c, p, p₂])
-  | none := do
-    nb ← b.to_nat,
-    na ← a.to_int,
-    let nq := na / nb,
-    let nr := na % nb,
-    let nm := nq * nr,
-    (ic, q) ← ic.of_int nq,
-    (ic, r) ← ic.of_int nr,
-    (ic, m, pm) ← prove_mul_rat ic q b (rat.of_int nq) (rat.of_int nb),
-    (ic, p) ← prove_add_rat ic r m a (rat.of_int nr) (rat.of_int nm) (rat.of_int na),
-    (ic, p') ← prove_lt_nat ic r b,
-    if ic.α = `(nat) then
-      if mod then return (ic, r, `(nat_mod).mk_app [a, b, q, r, m, pm, p, p'])
-      else        return (ic, q, `(nat_div).mk_app [a, b, q, r, m, pm, p, p'])
-    else if ic.α = `(int) then do
-      (ic, p₀) ← prove_nonneg ic r,
-      if mod then return (ic, r, `(int_mod).mk_app [a, b, q, r, m, pm, p, p₀, p'])
-      else        return (ic, q, `(int_div).mk_app [a, b, q, r, m, pm, p, p₀, p'])
-    else failed
-  end
-
-theorem dvd_eq_nat (a b c : ℕ) (p) (h₁ : b % a = c) (h₂ : (c = 0) = p) : (a ∣ b) = p :=
-(propext $ by rw [← h₁, nat.dvd_iff_mod_eq_zero]).trans h₂
-theorem dvd_eq_int (a b c : ℤ) (p) (h₁ : b % a = c) (h₂ : (c = 0) = p) : (a ∣ b) = p :=
-(propext $ by rw [← h₁, int.dvd_iff_mod_eq_zero]).trans h₂
-
 theorem int_to_nat_pos (a : ℤ) (b : ℕ) (h : (by haveI := @nat.cast_coe ℤ; exact b : ℤ) = a) :
   a.to_nat = b := by rw ← h; simp
 theorem int_to_nat_neg (a : ℤ) (h : 0 < a) : (-a).to_nat = 0 :=
@@ -1254,28 +1191,12 @@ theorem neg_succ_of_nat (a b : ℕ) (c : ℤ) (h₁ : a + 1 = b)
   (h₂ : (by haveI := @nat.cast_coe ℤ; exact b : ℤ) = c) :
   -[1+ a] = -c := by rw [← h₂, ← h₁]; refl
 
-/-- Evaluates some extra numeric operations on `nat` and `int`, specifically
-`nat.succ`, `/` and `%`, and `∣` (divisibility). -/
-meta def eval_nat_int_ext : expr → tactic (expr × expr)
+/-- Evaluates `nat.succ`, `int.to_nat`, `int.nat_abs`, `int.neg_succ_of_nat`. -/
+meta def eval_nat_int : expr → tactic (expr × expr)
 | e@`(nat.succ _) := do
   ic ← mk_instance_cache `(ℕ),
   (_, _, ep) ← prove_nat_succ ic e,
   return ep
-| `(%%a / %%b) := do
-  c ← infer_type a >>= mk_instance_cache,
-  prod.snd <$> prove_div_mod c a b ff
-| `(%%a % %%b) := do
-  c ← infer_type a >>= mk_instance_cache,
-  prod.snd <$> prove_div_mod c a b tt
-| `(%%a ∣ %%b) := do
-  α ← infer_type a,
-  ic ← mk_instance_cache α,
-  th ← if α = `(nat) then return (`(dvd_eq_nat):expr) else
-       if α = `(int) then return `(dvd_eq_int) else failed,
-  (ic, c, p₁) ← prove_div_mod ic b a tt,
-  (ic, z) ← ic.mk_app ``has_zero.zero [],
-  (e', p₂) ← mk_app ``eq [c, z] >>= eval_ineq,
-  return (e', th.mk_app [a, b, c, e', p₁, p₂])
 | `(int.to_nat %%a) := do
   n ← a.to_int,
   ic ← mk_instance_cache `(ℤ),
@@ -1353,7 +1274,7 @@ meta def eval_cast : expr → tactic (expr × expr)
 
 /-- This version of `derive` does not fail when the input is already a numeral -/
 meta def derive.step (e : expr) : tactic (expr × expr) :=
-eval_field e <|> eval_pow e <|> eval_ineq e <|> eval_cast e <|> eval_nat_int_ext e
+eval_field e <|> eval_pow e <|> eval_ineq e <|> eval_cast e <|> eval_nat_int e
 
 /-- An attribute for adding additional extensions to `norm_num`. To use this attribute, put
 `@[norm_num]` on a tactic of type `expr → tactic (expr × expr)`; the tactic will be called on
@@ -1626,3 +1547,94 @@ add_tactic_doc
   tags                     := ["simplification", "arithmetic", "decision procedure"] }
 
 end tactic
+
+namespace norm_num
+section elementary_number_theory
+
+open tactic
+
+lemma nat_div (a b q r m : ℕ) (hm : q * b = m) (h : r + m = a) (h₂ : r < b) : a / b = q :=
+by rw [← h, ← hm, nat.add_mul_div_right _ _ (lt_of_le_of_lt (nat.zero_le _) h₂),
+       nat.div_eq_of_lt h₂, zero_add]
+
+lemma int_div (a b q r m : ℤ) (hm : q * b = m) (h : r + m = a) (h₁ : 0 ≤ r) (h₂ : r < b) :
+  a / b = q :=
+by rw [← h, ← hm, int.add_mul_div_right _ _ (ne_of_gt (lt_of_le_of_lt h₁ h₂)),
+       int.div_eq_zero_of_lt h₁ h₂, zero_add]
+
+lemma nat_mod (a b q r m : ℕ) (hm : q * b = m) (h : r + m = a) (h₂ : r < b) : a % b = r :=
+by rw [← h, ← hm, nat.add_mul_mod_self_right, nat.mod_eq_of_lt h₂]
+
+lemma int_mod (a b q r m : ℤ) (hm : q * b = m) (h : r + m = a) (h₁ : 0 ≤ r) (h₂ : r < b) :
+  a % b = r :=
+by rw [← h, ← hm, int.add_mul_mod_self, int.mod_eq_of_lt h₁ h₂]
+
+lemma int_div_neg (a b c' c : ℤ) (h : a / b = c') (h₂ : -c' = c) : a / -b = c :=
+h₂ ▸ h ▸ int.div_neg _ _
+
+lemma int_mod_neg (a b c : ℤ) (h : a % b = c) : a % -b = c :=
+(int.mod_neg _ _).trans h
+
+/-- Given `a`,`b` numerals in `nat` or `int`,
+  * `prove_div_mod ic a b ff` returns `(c, ⊢ a / b = c)`
+  * `prove_div_mod ic a b tt` returns `(c, ⊢ a % b = c)`
+-/
+meta def prove_div_mod (ic : instance_cache) :
+  expr → expr → bool → tactic (instance_cache × expr × expr)
+| a b mod :=
+  match match_neg b with
+  | some b := do
+    (ic, c', p) ← prove_div_mod a b mod,
+    if mod then
+      return (ic, c', `(int_mod_neg).mk_app [a, b, c', p])
+    else do
+      (ic, c, p₂) ← prove_neg ic c',
+      return (ic, c, `(int_div_neg).mk_app [a, b, c', c, p, p₂])
+  | none := do
+    nb ← b.to_nat,
+    na ← a.to_int,
+    let nq := na / nb,
+    let nr := na % nb,
+    let nm := nq * nr,
+    (ic, q) ← ic.of_int nq,
+    (ic, r) ← ic.of_int nr,
+    (ic, m, pm) ← prove_mul_rat ic q b (rat.of_int nq) (rat.of_int nb),
+    (ic, p) ← prove_add_rat ic r m a (rat.of_int nr) (rat.of_int nm) (rat.of_int na),
+    (ic, p') ← prove_lt_nat ic r b,
+    if ic.α = `(nat) then
+      if mod then return (ic, r, `(nat_mod).mk_app [a, b, q, r, m, pm, p, p'])
+      else        return (ic, q, `(nat_div).mk_app [a, b, q, r, m, pm, p, p'])
+    else if ic.α = `(int) then do
+      (ic, p₀) ← prove_nonneg ic r,
+      if mod then return (ic, r, `(int_mod).mk_app [a, b, q, r, m, pm, p, p₀, p'])
+      else        return (ic, q, `(int_div).mk_app [a, b, q, r, m, pm, p, p₀, p'])
+    else failed
+  end
+
+theorem dvd_eq_nat (a b c : ℕ) (p) (h₁ : b % a = c) (h₂ : (c = 0) = p) : (a ∣ b) = p :=
+(propext $ by rw [← h₁, nat.dvd_iff_mod_eq_zero]).trans h₂
+theorem dvd_eq_int (a b c : ℤ) (p) (h₁ : b % a = c) (h₂ : (c = 0) = p) : (a ∣ b) = p :=
+(propext $ by rw [← h₁, int.dvd_iff_mod_eq_zero]).trans h₂
+
+/-- Evaluates some extra numeric operations on `nat` and `int`, specifically
+`/` and `%`, and `∣` (divisibility). -/
+@[norm_num] meta def eval_nat_int_ext : expr → tactic (expr × expr)
+| `(%%a / %%b) := do
+  c ← infer_type a >>= mk_instance_cache,
+  prod.snd <$> prove_div_mod c a b ff
+| `(%%a % %%b) := do
+  c ← infer_type a >>= mk_instance_cache,
+  prod.snd <$> prove_div_mod c a b tt
+| `(%%a ∣ %%b) := do
+  α ← infer_type a,
+  ic ← mk_instance_cache α,
+  th ← if α = `(nat) then return (`(dvd_eq_nat):expr) else
+       if α = `(int) then return `(dvd_eq_int) else failed,
+  (ic, c, p₁) ← prove_div_mod ic b a tt,
+  (ic, z) ← ic.mk_app ``has_zero.zero [],
+  (e', p₂) ← mk_app ``eq [c, z] >>= eval_ineq,
+  return (e', th.mk_app [a, b, c, e', p₁, p₂])
+| _ := failed
+
+end elementary_number_theory
+end norm_num

test/norm_num.lean

@@ -300,3 +300,29 @@ example : (- ((- (((66 - 86) - 36) / 94) - 3) / - - (77 / (56 - - - 79))) + 87)
   (312254/3619 : α) := by norm_num
 
 example : 2 ^ 13 - 1 = int.of_nat 8191 := by norm_num
+
+/-! Test the behaviour of removing one `norm_num` extension tactic. -/
+section remove_extension
+
+-- turn off the `norm_num` extension which deals with `/`, `%`, `∣`
+local attribute [-norm_num] norm_num.eval_nat_int_ext
+
+example : (5 / 2:ℕ) = 2 := by  success_if_fail { solve1 { norm_num } }; refl
+
+example : 10 = (-1 : ℤ) % 11 := by success_if_fail { solve1 { norm_num } }; refl
+
+example (h : (5 : ℤ) ∣ 2) : false :=
+begin
+  success_if_fail { norm_num at h },
+  have : (2:ℤ) ≠ 0 := by norm_num,
+  exact this (int.mod_eq_zero_of_dvd h),
+end
+
+example : 2^4-1 ∣ 2^16-1 :=
+begin
+  success_if_fail { solve1 { norm_num } },
+  use 4369,
+  norm_num,
+end
+
+end remove_extension