feat(library/tactic): add norm_num_tactic

library/init/algebra/norm_num.lean

@@ -16,6 +16,12 @@ a + 1
 local attribute [reducible] bit0 bit1 add1
 local attribute [simp] right_distrib left_distrib
 
+private meta def u : tactic unit :=
+`[unfold bit0 bit1 add1]
+
+private meta def usimp : tactic unit :=
+u >> `[simp]
+
 lemma mul_zero [mul_zero_class α] (a : α) : a * 0 = 0 :=
 by simp
 
@@ -107,11 +113,11 @@ lemma div_mul_helper [field α] (n d c v : α) (hd : d ≠ 0) (h : (n * c) / d =
         (n / d) * c = v :=
 by rw [-h, field.div_mul_eq_mul_div_comm _ _ hd, mul_div_assoc]
 
-lemma mul_div_helper [s : field α] (a n d v : α) (hd : d ≠ 0) (h : (a * n) / d = v) :
+lemma mul_div_helper [field α] (a n d v : α) (hd : d ≠ 0) (h : (a * n) / d = v) :
         a * (n / d) = v :=
 by rw [-h, mul_div_assoc]
 
-lemma nonzero_of_div_helper [s : field α] (a b : α) (ha : a ≠ 0) (hb : b ≠ 0) : a / b ≠ 0 :=
+lemma nonzero_of_div_helper [field α] (a b : α) (ha : a ≠ 0) (hb : b ≠ 0) : a / b ≠ 0 :=
 begin
   intro hab,
   assert habb : (a / b) * b = 0, rw [hab, zero_mul],
@@ -119,14 +125,14 @@ begin
   exact ha habb
 end
 
-lemma div_helper [s : field α] (n d v : α) (hd : d ≠ 0) (h : v * d = n) : n / d = v :=
+lemma div_helper [field α] (n d v : α) (hd : d ≠ 0) (h : v * d = n) : n / d = v :=
 begin
   apply eq_of_mul_eq_mul_of_nonzero_right hd,
   rw (div_mul_cancel _ hd),
   exact eq.symm h
 end
 
-lemma div_eq_div_helper [s : field α] (a b c d v : α) (h1 : a * d = v) (h2 : c * b = v)
+lemma div_eq_div_helper [field α] (a b c d v : α) (h1 : a * d = v) (h2 : c * b = v)
         (hb : b ≠ 0) (hd : d ≠ 0) : a / b = c / d :=
 begin
   apply eq_div_of_mul_eq,
@@ -138,8 +144,98 @@ begin
   rw [h1, h2]
 end
 
-lemma subst_into_div [s : has_div α] (a₁ b₁ a₂ b₂ v : α) (h : a₁ / b₁ = v) (h1 : a₂ = a₁)
+lemma subst_into_div [has_div α] (a₁ b₁ a₂ b₂ v : α) (h : a₁ / b₁ = v) (h1 : a₂ = a₁)
       (h2 : b₂ = b₁) : a₂ / b₂ = v :=
 by rw [h1, h2, h]
 
+
+lemma add_comm_four [add_comm_semigroup α] (a b : α) : a + a + (b + b) = (a + b) + (a + b) :=
+by simp
+
+lemma add_comm_middle [add_comm_semigroup α] (a b c : α) : a + b + c = a + c + b :=
+by simp
+
+lemma bit0_add_bit0 [add_comm_semigroup α] (a b : α) : bit0 a + bit0 b = bit0 (a + b) :=
+by usimp
+
+lemma bit0_add_bit0_helper [add_comm_semigroup α] (a b t : α) (h : a + b = t) :
+        bit0 a + bit0 b = bit0 t :=
+begin rw -h, usimp end
+
+lemma bit1_add_bit0 [add_comm_semigroup α] [has_one α] (a b : α) : bit1 a + bit0 b = bit1 (a + b) :=
+by usimp
+
+lemma bit1_add_bit0_helper [add_comm_semigroup α] [has_one α] (a b t : α)
+        (h : a + b = t) : bit1 a + bit0 b = bit1 t :=
+begin rw -h, usimp end
+
+lemma bit0_add_bit1 [add_comm_semigroup α] [has_one α] (a b : α) :
+        bit0 a + bit1 b = bit1 (a + b) :=
+by usimp
+
+lemma bit0_add_bit1_helper [add_comm_semigroup α] [has_one α] (a b t : α)
+        (h : a + b = t) : bit0 a + bit1 b = bit1 t :=
+begin rw -h, usimp end
+
+lemma bit1_add_bit1 [add_comm_semigroup α] [has_one α] (a b : α) :
+        bit1 a + bit1 b = bit0 (add1 (a + b)) :=
+by usimp
+
+lemma bit1_add_bit1_helper [add_comm_semigroup α] [has_one α] (a b t s : α)
+        (h : (a + b) = t) (h2 : add1 t = s) : bit1 a + bit1 b = bit0 s :=
+begin rw -h at h2, rw -h2, usimp end
+
+lemma bin_add_zero [add_monoid α] (a : α) : a + zero = a :=
+by simp
+
+lemma bin_zero_add [add_monoid α] (a : α) : zero + a = a :=
+by simp
+
+lemma one_add_bit0 [add_comm_semigroup α] [has_one α] (a : α) : one + bit0 a = bit1 a :=
+begin unfold bit0 bit1, simp end
+
+lemma bit0_add_one [has_add α] [has_one α] (a : α) : bit0 a + one = bit1 a :=
+rfl
+
+lemma bit1_add_one [has_add α] [has_one α] (a : α) : bit1 a + one = add1 (bit1 a) :=
+rfl
+
+lemma bit1_add_one_helper [has_add α] [has_one α] (a t : α) (h : add1 (bit1 a) = t) :
+        bit1 a + one = t :=
+by rw -h
+
+lemma one_add_bit1 [add_comm_semigroup α] [has_one α] (a : α) : one + bit1 a = add1 (bit1 a) :=
+begin unfold bit0 bit1 add1, simp end
+
+lemma one_add_bit1_helper [add_comm_semigroup α] [has_one α] (a t : α)
+        (h : add1 (bit1 a) = t) : one + bit1 a = t :=
+begin rw -h, usimp end
+
+lemma add1_bit0 [has_add α] [has_one α] (a : α) : add1 (bit0 a) = bit1 a :=
+rfl
+
+lemma add1_bit1 [add_comm_semigroup α] [has_one α] (a : α) :
+        add1 (bit1 a) = bit0 (add1 a) :=
+by usimp
+
+lemma add1_bit1_helper [add_comm_semigroup α] [has_one α] (a t : α) (h : add1 a = t) :
+        add1 (bit1 a) = bit0 t :=
+begin rw -h, usimp end
+
+lemma add1_one [has_add α] [has_one α] : add1 (one : α) = bit0 one :=
+rfl
+
+lemma add1_zero [add_monoid α] [has_one α] : add1 (zero : α) = one :=
+by usimp
+
+lemma one_add_one [has_add α] [has_one α] : (one : α) + one = bit0 one :=
+rfl
+
+lemma subst_into_sum [has_add α] (l r tl tr t : α) (prl : l = tl) (prr : r = tr)
+        (prt : tl + tr = t) : l + r = t :=
+by rw [-prt, prr, prl]
+
+lemma neg_zero_helper [add_group α] (a : α) (h : a = 0) : - a = 0 :=
+begin rw h, simp end
+
 end norm_num

library/init/meta/simp_tactic.lean

@@ -309,6 +309,9 @@ meta def join_user_simp_lemmas : list name → tactic simp_lemmas
 | []         := simp_lemmas.mk_default
 | attr_names := join_user_simp_lemmas_core simp_lemmas.mk attr_names
 
+/- Normalize numerical expression, returns a pair (n, pr) where n is the resultant numeral,
+   and pr is a proof that the input argument is equal to n. -/
+meta constant norm_num : expr → tactic (expr × expr)
 end tactic
 
 export tactic (mk_simp_attr)

src/library/tactic/CMakeLists.txt

@@ -8,4 +8,4 @@ add_library(tactic OBJECT occurrences.cpp kabstract.cpp tactic_state.cpp
   hsubstitution.cpp gexpr.cpp elaborate.cpp init_module.cpp
   simp_result.cpp user_attribute.cpp eval.cpp
   simp_lemmas.cpp eqn_lemmas.cpp dsimplify.cpp simplify.cpp
-  vm_monitor.cpp)
+  vm_monitor.cpp norm_num_tactic.cpp)

src/library/tactic/init_module.cpp

@@ -33,6 +33,7 @@ Author: Leonardo de Moura
 #include "library/tactic/dsimplify.h"
 #include "library/tactic/simplify.h"
 #include "library/tactic/vm_monitor.h"
+#include "library/tactic/norm_num_tactic.h"
 #include "library/tactic/backward/init_module.h"
 
 namespace lean {
@@ -66,10 +67,12 @@ void initialize_tactic_module() {
     initialize_simp_lemmas();
     initialize_eqn_lemmas();
     initialize_dsimplify();
+    initialize_norm_num_tactic();
     initialize_vm_monitor();
 }
 void finalize_tactic_module() {
     finalize_vm_monitor();
+    finalize_norm_num_tactic();
     finalize_dsimplify();
     finalize_eqn_lemmas();
     finalize_simp_lemmas();

src/library/tactic/norm_num_tactic.cpp

@@ -0,0 +1,28 @@
+/*
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Robert Y. Lewis, Leonardo de Moura
+*/
+#include "library/norm_num.h"
+#include "library/type_context.h"
+#include "library/vm/vm_expr.h"
+#include "library/tactic/tactic_state.h"
+
+namespace lean {
+vm_obj tactic_norm_num(vm_obj const & e, vm_obj const & _s) {
+    tactic_state const & s = to_tactic_state(_s);
+    type_context ctx = mk_type_context_for(s);
+    try {
+        pair<expr, expr> p = mk_norm_num(ctx, to_expr(e));
+        return mk_tactic_success(mk_vm_pair(to_obj(p.first), to_obj(p.second)), s);
+    } catch (exception & ex) {
+        return mk_tactic_exception(ex, s);
+    }
+}
+
+void initialize_norm_num_tactic() {
+    DECLARE_VM_BUILTIN(name({"tactic", "norm_num"}), tactic_norm_num);
+}
+void finalize_norm_num_tactic() {
+}
+}

src/library/tactic/norm_num_tactic.h

@@ -0,0 +1,10 @@
+/*
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Robert Y. Lewis, Leonardo de Moura
+*/
+#pragma once
+namespace lean {
+void initialize_norm_num_tactic();
+void finalize_norm_num_tactic();
+}