feat(tactic/norm_num): add support for {nat,int}.div

Author: digama0

data/rat.lean

@@ -137,9 +137,9 @@ begin
       a / nat.gcd a b = c / nat.gcd c d ∧ b / nat.gcd a b = d / nat.gcd c d,
     { intros a c h,
       have bd : b / nat.gcd a b = d / nat.gcd c d,
-      { have : ∀ {a c} (b>0) (d>0),
+      { suffices : ∀ {a c} (b>0) (d>0),
           a * d = c * b → b / nat.gcd a b ≤ d / nat.gcd c d,
-        tactic.swap, { exact le_antisymm (this _ hb _ hd h) (this _ hd _ hb h.symm) },
+        { exact le_antisymm (this _ hb _ hd h) (this _ hd _ hb h.symm) },
         intros a c b hb d hd h,
         have gb0 := nat.gcd_pos_of_pos_right a hb,
         have gd0 := nat.gcd_pos_of_pos_right c hd,
@@ -159,10 +159,8 @@ begin
           nat.mul_div_assoc _ (nat.gcd_dvd_right _ _), bd,
           ← nat.mul_div_assoc _ (nat.gcd_dvd_right _ _), h, mul_comm,
           nat.mul_div_assoc _ (nat.gcd_dvd_left _ _)] },
-    have ha := this a.nat_abs c.nat_abs begin
-      have := congr_arg int.nat_abs h,
-      simp [int.nat_abs_mul] at this, exact this
-    end,
+    have ha := this a.nat_abs c.nat_abs
+      (by simpa [int.nat_abs_mul] using congr_arg int.nat_abs h),
     tactic.congr_core,
     { have hs := congr_arg int.sign h,
       simp [int.sign_eq_one_of_pos (int.coe_nat_lt.2 hb),

tactic/norm_num.lean

@@ -27,13 +27,17 @@ protected meta def to_pos_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)
 
+protected meta def to_int : expr → option ℤ
+| `(has_neg.neg %%e) := do n ← e.to_nat, some (-n)
+| e                  := do n ← e.to_nat, return n
+
 protected meta def to_rat : expr → option ℚ
 | `(has_neg.neg %%e) := do q ← e.to_pos_rat, some (-q)
 | e                  := e.to_pos_rat
 
 protected meta def of_nat (α : expr) : ℕ → tactic expr :=
 nat.binary_rec
-  (tactic.mk_app ``has_zero.zero [α])
+  (tactic.mk_mapp ``has_zero.zero [some α, none])
   (λ b n tac, if n = 0 then mk_mapp ``has_one.one [some α, none] else
     do e ← tac, tactic.mk_app (cond b ``bit1 ``bit0) [e])
 
@@ -91,6 +95,14 @@ lemma lt_add_of_pos_helper [ordered_cancel_comm_monoid α]
   (a b c : α) (h : a + b = c) (h₂ : 0 < b) : a < c :=
 h ▸ (lt_add_iff_pos_right _).2 h₂
 
+lemma nat_div_helper (a b q r : ℕ) (h : r + q * b = a) (h₂ : r < b) : a / b = q :=
+by rw [← h, 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_helper (a b q r : ℤ) (h : r + q * b = a) (h₁ : 0 ≤ r) (h₂ : r < b) : a / b = q :=
+by rw [← h, 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]
+
 meta structure instance_cache :=
 (α : expr)
 (univ : level)
@@ -123,17 +135,6 @@ do d ← get_decl n,
 
 end instance_cache
 
-meta def eval_inv (simp : expr → tactic (expr × expr)) : expr → tactic (expr × expr)
-| `(has_inv.inv %%e) := do
-  c ← infer_type e >>= mk_instance_cache,
-  (c, p₁) ← c.mk_app ``inv_eq_one_div [e],
-  (c, o) ← c.mk_app ``has_one.one [],
-  (c, e') ← c.mk_app ``has_div.div [o, e],
-  (do (e'', p₂) ← simp e',
-    p ← mk_eq_trans p₁ p₂,
-    return (e'', p)) <|> return (e', p₁)
-| _ := failed
-
 meta def eval_pow (simp : expr → tactic (expr × expr)) : expr → tactic (expr × expr)
 | `(monoid.pow %%e₁ 0) := do
   p ← mk_app ``pow_zero [e₁],
@@ -247,9 +248,62 @@ meta def eval_ineq (simp : expr → tactic (expr × expr)) : expr → tactic (ex
 | `(%%e₁ ≠ %%e₂) := do e ← mk_app ``eq [e₁, e₂], mk_app ``not [e] >>= simp
 | _ := failed
 
+meta def eval_div_ext (simp : expr → tactic (expr × expr)) : expr → tactic (expr × expr)
+| `(has_inv.inv %%e) := do
+  c ← infer_type e >>= mk_instance_cache,
+  (c, p₁) ← c.mk_app ``inv_eq_one_div [e],
+  (c, o) ← c.mk_app ``has_one.one [],
+  (c, e') ← c.mk_app ``has_div.div [o, e],
+  (do (e'', p₂) ← simp e',
+    p ← mk_eq_trans p₁ p₂,
+    return (e'', p)) <|> return (e', p₁)
+| `(%%e₁ / %%e₂) := do
+  α ← infer_type e₁,
+  c ← mk_instance_cache α,
+  match α with
+  | `(nat) := do
+    n₁ ← e₁.to_nat, n₂ ← e₂.to_nat,
+    q ← expr.of_nat α (n₁ / n₂),
+    r ← expr.of_nat α (n₁ % n₂),
+    (c, e₃) ← c.mk_app ``has_mul.mul [q, e₂],
+    (c, e₃) ← c.mk_app ``has_add.add [r, e₃],
+    (e₁', p) ← norm_num e₃,
+    guard (e₁' =ₐ e₁),
+    (c, p') ← prove_lt simp c r e₂,
+    p ← mk_app ``norm_num.nat_div_helper [e₁, e₂, q, r, p, p'],
+    return (q, p)
+  | `(int) := match e₂ with
+    | `(- %%e₂') := do
+      (c, p₁) ← c.mk_app ``int.div_neg [e₁, e₂'],
+      (c, e) ← c.mk_app ``has_div.div [e₁, e₂'],
+      (c, e) ← c.mk_app ``has_neg.neg [e],
+      (e', p₂) ← simp e,
+      p ← mk_eq_trans p₁ p₂,
+      return (e', p)
+    | _ := do
+      n₁ ← e₁.to_int,
+      n₂ ← e₂.to_int,
+      q ← expr.of_rat α $ rat.of_int (n₁ / n₂),
+      r ← expr.of_rat α $ rat.of_int (n₁ % n₂),
+      (c, e₃) ← c.mk_app ``has_mul.mul [q, e₂],
+      (c, e₃) ← c.mk_app ``has_add.add [r, e₃],
+      (e₁', p) ← norm_num e₃,
+      guard (e₁' =ₐ e₁),
+      (c, r0) ← c.mk_app ``has_zero.zero [],
+      (c, r0) ← c.mk_app ``has_le.le [r0, r],
+      (_, p₁) ← simp r0,
+      p₁ ← mk_app ``of_eq_true [p₁],
+      (c, p₂) ← prove_lt simp c r e₂,
+      p ← mk_app ``norm_num.int_div_helper [e₁, e₂, q, r, p, p₁, p₂],
+      return (q, p)
+    end
+  | _ := failed
+  end
+| _ := failed
+
 meta def derive1 (simp : expr → tactic (expr × expr)) (e : expr) :
   tactic (expr × expr) :=
-norm_num e <|> eval_inv simp e <|> eval_pow simp e <|> eval_ineq simp e
+norm_num e <|> eval_div_ext simp e <|> eval_pow simp e <|> eval_ineq simp e
 
 meta def derive : expr → tactic (expr × expr) | e :=
 do (_, e', pr) ←

tests/norm_num.lean

@@ -24,6 +24,10 @@ example : (6:real) < 10 := by norm_num
 example : (7:real)/2 > 3 := by norm_num
 example : (4:real)⁻¹ < 1 := by norm_num
 
+example : (5 / 2:ℕ) = 2 := by norm_num
+example : (5 / -2:ℤ) < -1 := by norm_num
+example : (0 + 1) / 2 < 0 + 1 := by norm_num
+
 example (x : ℤ) (h : 1000 + 2000 < x) : 100 * 30 < x :=
 by norm_num at *; try_for 100 {exact h}