feat(tactic/norm_num): make norm_num extensible (#4820)

This allows you to extend `norm_num` by defining additional tactics of type `expr → tactic (expr × expr)` with the `@[norm_num]` attribute. It still requires some tactic proficiency to use correctly, but it at least allows us to move all the possible norm_num extensions to their own files instead of the current dependency cycle problem.

This could potentially become a performance problem if too many things are marked `@[norm_num]`, as they are simply looked through in linear order. It could be improved by having extensions register a finite set of constants that they wish to evaluate, and dispatch to the right extension tactic using a `name_map`.

```lean
def foo : ℕ := 1

@[norm_num] meta def eval_foo : expr → tactic (expr × expr)
| `(foo) := pure (`(1:ℕ), `(eq.refl 1))
| _ := tactic.failed

example : foo = 1 := by norm_num
```

Author: digama0

src/tactic/abel.lean

@@ -136,7 +136,7 @@ meta def eval_add (c : cache) : normal_expr → normal_expr → tactic (normal_e
     (a', h) ← eval_add he₁ a₂,
     return (term' c n₂ x₂ a', c.iapp ``const_add_term [e₁, n₂.1, x₂, a₂, a', h])
   else do
-    (n', h₁) ← mk_app ``has_add.add [n₁.1, n₂.1] >>= norm_num.derive',
+    (n', h₁) ← mk_app ``has_add.add [n₁.1, n₂.1] >>= norm_num.eval_field,
     (a', h₂) ← eval_add a₁ a₂,
     let k := n₁.2 + n₂.2,
     let p₁ := c.iapp ``term_add_term [n₁.1, x₁, a₁, n₂.1, a₂, n', a', h₁, h₂],
@@ -155,7 +155,7 @@ meta def eval_neg (c : cache) : normal_expr → tactic (normal_expr × expr)
   p ← c.mk_app ``neg_zero ``add_group [],
   return (zero' c, p)
 | (nterm e n x a) := do
-  (n', h₁) ← mk_app ``has_neg.neg [n.1] >>= norm_num.derive',
+  (n', h₁) ← mk_app ``has_neg.neg [n.1] >>= norm_num.eval_field,
   (a', h₂) ← eval_neg a,
   return (term' c (n', -n.2) x a',
     c.app ``term_neg c.inst [n.1, x, a, n', a', h₁, h₂])
@@ -183,7 +183,7 @@ meta def eval_smul (c : cache) (k : expr × ℤ) :
   normal_expr → tactic (normal_expr × expr)
 | (zero _) := return (zero' c, c.iapp ``zero_smul [k.1])
 | (nterm e n x a) := do
-  (n', h₁) ← mk_app ``has_mul.mul [k.1, n.1] >>= norm_num.derive',
+  (n', h₁) ← mk_app ``has_mul.mul [k.1, n.1] >>= norm_num.eval_field,
   (a', h₂) ← eval_smul a,
   return (term' c (n', k.2 * n.2) x a',
     c.iapp ``term_smul [k.1, n.1, x, a, n', a', h₁, h₂])

src/tactic/norm_num.lean

@@ -1384,33 +1384,96 @@ meta def eval_prime : expr → tactic (expr × expr)
 | _ := failed
 
 /-- This version of `derive` does not fail when the input is already a numeral -/
-meta def derive' (e : expr) : tactic (expr × expr) :=
+meta def derive.step (e : expr) : tactic (expr × expr) :=
 eval_field e <|> eval_nat_int_ext e <|>
 eval_pow e <|> eval_ineq e <|> eval_prime e
 
-meta def derive : expr → tactic (expr × expr) | 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
+subterms by `norm_num`, and it is responsible for identifying that the expression is a numerical
+function applied to numerals, for example `nat.fib 17`, and should return the reduced numerical
+expression (which must be in `norm_num`-normal form: a natural or rational numeral, i.e. `37`,
+`12 / 7` or `-(2 / 3)`, although this can be an expression in any type), and the proof that the
+original expression is equal to the rewritten expression.
+
+Failure is used to indicate that this tactic does not apply to the term. For performance reasons,
+it is best to detect non-applicability as soon as possible so that the next tactic can have a go,
+so generally it will start with a pattern match and then checking that the arguments to the term
+are numerals or of the appropriate form, followed by proof construction, which should not fail.
+
+Propositions are treated like any other term. The normal form for propositions is `true` or
+`false`, so it should produce a proof of the form `p = true` or `p = false`. `eq_true_intro` can be
+used to help here.
+-/
+@[user_attribute]
+protected meta def attr : user_attribute (expr → tactic (expr × expr)) unit :=
+{ name      := `norm_num,
+  descr     := "Add norm_num derivers",
+  cache_cfg :=
+  { mk_cache := λ ns, do {
+      t ← ns.mfoldl
+        (λ (t : expr → tactic (expr × expr)) n, do
+          t' ← eval_expr (expr → tactic (expr × expr)) (expr.const n []),
+          pure (λ e, t' e <|> t e))
+        (λ _, failed),
+      pure (λ e, derive.step e <|> t e) },
+    dependencies := [] } }
+
+add_tactic_doc
+{ name := "norm_num",
+  category := doc_category.attr,
+  decl_names := [`norm_num.attr],
+  tags := ["arithmetic", "decision_procedure"] }
+
+/-- Look up the `norm_num` extensions in the cache and return a tactic extending `derive.step` with
+additional reduction procedures. -/
+meta def get_step : tactic (expr → tactic (expr × expr)) := norm_num.attr.get_cache
+
+/-- Simplify an expression bottom-up using `step` to simplify the subexpressions. -/
+meta def derive' (step : expr → tactic (expr × expr))
+  : expr → tactic (expr × expr) | e :=
 do e ← instantiate_mvars e,
    (_, e', pr) ←
     ext_simplify_core () {} simp_lemmas.mk (λ _, failed) (λ _ _ _ _ _, failed)
       (λ _ _ _ _ e,
-        do (new_e, pr) ← derive' e,
+        do (new_e, pr) ← step e,
            guard (¬ new_e =ₐ e),
            return ((), new_e, some pr, tt))
       `eq e,
     return (e', pr)
 
+/-- Simplify an expression bottom-up using the default `norm_num` set to simplify the
+subexpressions. -/
+meta def derive (e : expr) : tactic (expr × expr) := do f ← get_step, derive' f e
+
 end norm_num
 
+/-- Basic version of `norm_num` that does not call `simp`. It uses the provided `step` tactic
+to simplify the expression; use `get_step` to get the default `norm_num` set and `derive.step` for
+the basic builtin set of simplifications. -/
+meta def tactic.norm_num1 (step : expr → tactic (expr × expr))
+  (loc : interactive.loc) : tactic unit :=
+do ns ← loc.get_locals,
+   tt ← tactic.replace_at (norm_num.derive' step) ns loc.include_goal
+      | fail "norm_num failed to simplify",
+   when loc.include_goal $ try tactic.triv,
+   when (¬ ns.empty) $ try tactic.contradiction
+
+/-- Normalize numerical expressions. It uses the provided `step` tactic to simplify the expression;
+use `get_step` to get the default `norm_num` set and `derive.step` for the basic builtin set of
+simplifications. -/
+meta def tactic.norm_num (step : expr → tactic (expr × expr))
+  (hs : list simp_arg_type) (l : interactive.loc) : tactic unit :=
+repeat1 $ orelse' (tactic.norm_num1 step l) $
+interactive.simp_core {} (tactic.norm_num1 step (interactive.loc.ns [none]))
+  ff (simp_arg_type.except ``one_div :: hs) [] l
+
 namespace tactic.interactive
 open norm_num interactive interactive.types
 
 /-- Basic version of `norm_num` that does not call `simp`. -/
 meta def norm_num1 (loc : parse location) : tactic unit :=
-do ns ← loc.get_locals,
-   tt ← tactic.replace_at derive ns loc.include_goal
-      | fail "norm_num failed to simplify",
-   when loc.include_goal $ try tactic.triv,
-   when (¬ ns.empty) $ try tactic.contradiction
+do f ← get_step, tactic.norm_num1 f loc
 
 /-- Normalize numerical expressions. Supports the operations
 `+` `-` `*` `/` `^` and `%` over numerical types such as
@@ -1419,8 +1482,7 @@ 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. -/
 meta def norm_num (hs : parse simp_arg_list) (l : parse location) : tactic unit :=
-repeat1 $ orelse' (norm_num1 l) $
-simp_core {} (norm_num1 (loc.ns [none])) ff (simp_arg_type.except ``one_div :: hs) [] l
+do f ← get_step, tactic.norm_num f hs l
 
 add_hint_tactic "norm_num"
 

src/tactic/ring_exp.lean

@@ -627,7 +627,7 @@ with the proof of `expr.of_rat p + expr.of_rat q = expr.of_rat (p + q)`.
 meta def add_coeff (p_p q_p : expr) (p q : coeff) : ring_exp_m (ex prod) := do
   ctx ← get_context,
   pq_o ← mk_add [p_p, q_p],
-  (pq_p, pq_pf) ← lift $ norm_num.derive' pq_o,
+  (pq_p, pq_pf) ← lift $ norm_num.eval_field pq_o,
   pure $ ex.coeff ⟨pq_o, pq_p, pq_pf⟩ ⟨p.1 + q.1⟩
 
 lemma mul_coeff_pf_one_mul (q : α) : 1 * q = q := one_mul q
@@ -654,7 +654,7 @@ match p.1, q.1 with -- Special case to speed up multiplication with 1.
 | _, _ := do
   ctx ← get_context,
   pq' ← mk_mul [p_p, q_p],
-  (pq_p, pq_pf) ← lift $ norm_num.derive' pq',
+  (pq_p, pq_pf) ← lift $ norm_num.eval_field pq',
   pure $ ex.coeff ⟨pq_p, pq_p, pq_pf⟩ ⟨p.1 * q.1⟩
 end
 
@@ -975,7 +975,7 @@ with the proof of `expr.of_rat p ^ expr.of_rat q = expr.of_rat (p ^ q)`.
 meta def pow_coeff (p_p q_p : expr) (p q : coeff) : ring_exp_m (ex prod) := do
   ctx ← get_context,
   pq' ← mk_pow [p_p, q_p],
-  (pq_p, pq_pf) ← lift $ norm_num.derive' pq',
+  (pq_p, pq_pf) ← lift $ norm_num.eval_pow pq',
   pure $ ex.coeff ⟨pq_p, pq_p, pq_pf⟩ ⟨p.1 * q.1⟩
 
 /--

test/norm_num.lean

@@ -91,6 +91,14 @@ example : 100 - 100 = 0 := by norm_num
 example : 5 * (2 - 3) = 0 := by norm_num
 example : 10 - 5 * 5 + (7 - 3) * 6 = 27 - 3 := by norm_num
 
+def foo : ℕ := 1
+
+@[norm_num] meta def eval_foo : expr → tactic (expr × expr)
+| `(foo) := pure (`(1:ℕ), `(eq.refl 1))
+| _ := tactic.failed
+
+example : foo = 1 := by norm_num
+
 -- ordered field examples
 
 variable {α : Type}