feat(tactic/norm_num): new all-lean norm_num (#2589)

This is a first draft of the lean replacement for `tactic.norm_num` in core. This isn't completely polished yet; the rest of `norm_num` can now be a little less "global-recursive" since the primitives for e.g. adding and multiplying natural numbers are exposed.

I'm also trying out a new approach using functions like `match_neg` and `match_numeral` instead of directly pattern matching on exprs, because this generates smaller (and hopefully more efficient) code. (Without this, some of the matches were hitting the equation compiler depth limit.)

I'm open to new feature suggestions as well here. `nat.succ` and coercions seem useful to support in the core part, and additional flexibility using `def_replacer` is also on the agenda.

Author: digama0

src/analysis/specific_limits.lean

@@ -229,7 +229,7 @@ begin
   convert has_sum.mul_left (a / 2) (has_sum_geometric
     (le_of_lt one_half_pos) one_half_lt_one),
   { funext n, simp, refl, },
-  { norm_num, rw div_mul_cancel, norm_num }
+  { norm_num }
 end
 
 lemma summable_geometric_two' (a : ℝ) : summable (λ n:ℕ, (a / 2) / 2 ^ n) :=

src/data/rat/meta_defs.lean

@@ -3,7 +3,7 @@ Copyright (c) 2019 Robert Y. Lewis . All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Robert Y. Lewis
 -/
-import data.rat.basic
+import data.rat.basic tactic.core
 
 /-!
 # Meta operations on ℚ
@@ -55,8 +55,13 @@ end
 /-- Evaluates an expression as a rational number,
 if that expression represents a numeral or the quotient of two numerals. -/
 protected meta def expr.to_nonneg_rat : expr → option ℚ
-| `(%%e₁ / %%e₂) := do m ← e₁.to_nat, n ← e₂.to_nat, some (rat.mk m n)
-| e              := do n ← e.to_nat, return (rat.of_int n)
+| `(%%e₁ / %%e₂) := do
+  m ← e₁.to_nat,
+  n ← e₂.to_nat,
+  if c : m.coprime n then if h : 1 < n then
+    return ⟨m, n, lt_trans zero_lt_one h, c⟩
+  else none else none
+| e := do n ← e.to_nat, return (rat.of_int n)
 
 /-- Evaluates an expression as a rational number,
 if that expression represents a numeral, the quotient of two numerals,
@@ -96,3 +101,26 @@ protected meta def expr.of_rat (α : expr) : ℚ → tactic expr
     e₂ ← expr.of_nat α d,
     tactic.mk_app ``has_div.div [e₁, e₂]),
   tactic.mk_app ``has_neg.neg [e]
+
+namespace tactic
+namespace instance_cache
+
+/-- `c.of_rat q` embeds `q` as a numeral expression inside the type `α`.
+Lean will try to infer the correct type classes on `c.α`, and the tactic will fail if it cannot.
+This function is similar to `rat.mk_numeral` but it takes fewer hypotheses and is tactic valued.
+-/
+protected meta def of_rat (c : instance_cache) : ℚ → tactic (instance_cache × expr)
+| ⟨(n:ℕ), d, _, _⟩   :=
+  if d = 1 then c.of_nat n else do
+    (c, e₁) ← c.of_nat n,
+    (c, e₂) ← c.of_nat d,
+    c.mk_app ``has_div.div [e₁, e₂]
+| ⟨-[1+n], d, _, _⟩ := do
+  (c, e) ← (if d = 1 then c.of_nat (n+1) else do
+    (c, e₁) ← c.of_nat (n+1),
+    (c, e₂) ← c.of_nat d,
+    c.mk_app ``has_div.div [e₁, e₂]),
+  c.mk_app ``has_neg.neg [e]
+
+end instance_cache
+end tactic

src/tactic/core.lean

@@ -529,6 +529,26 @@ do d ← get_decl n,
    (c, l) ← append_typeclasses d.type.binding_body c l,
    return (c, (expr.const n [c.univ]).mk_app (c.α :: l))
 
+/-- `c.of_nat n` creates the `c.α`-valued numeral expression corresponding to `n`. -/
+protected meta def of_nat (c : instance_cache) (n : ℕ) : tactic (instance_cache × expr) :=
+if n = 0 then c.mk_app ``has_zero.zero [] else do
+  (c, ai) ← c.get ``has_add,
+  (c, oi) ← c.get ``has_one,
+  (c, one) ← c.mk_app ``has_one.one [],
+  return (c, n.binary_rec one $ λ b n e,
+    if n = 0 then one else
+    cond b
+      ((expr.const ``bit1 [c.univ]).mk_app [c.α, oi, ai, e])
+      ((expr.const ``bit0 [c.univ]).mk_app [c.α, ai, e]))
+
+/-- `c.of_int n` creates the `c.α`-valued numeral expression corresponding to `n`.
+The output is either a numeral or the negation of a numeral. -/
+protected meta def of_int (c : instance_cache) : ℤ → tactic (instance_cache × expr)
+| (n : ℕ) := c.of_nat n
+| -[1+ n] := do
+  (c, e) ← c.of_nat (n+1),
+  c.mk_app ``has_neg.neg [e]
+
 end instance_cache
 
 private meta def get_expl_pi_arity_aux : expr → tactic nat