From e4f0f6a9b4f7094be47148faa503322a7aebf054 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 8 Oct 2015 12:49:12 -0700
Subject: [PATCH] feat(library): numeral normalization skeleton

---
 library/algebra/numeral.lean           | 23 +++++++++++
 library/init/tactic.lean               |  1 +
 src/library/CMakeLists.txt             |  2 +-
 src/library/norm_num.cpp               | 18 +++++++++
 src/library/norm_num.h                 | 27 +++++++++++++
 src/library/tactic/CMakeLists.txt      |  3 +-
 src/library/tactic/init_module.cpp     |  3 ++
 src/library/tactic/norm_num_tactic.cpp | 53 ++++++++++++++++++++++++++
 src/library/tactic/norm_num_tactic.h   | 12 ++++++
 tests/lean/extra/num_norm1.lean        | 11 ++++++
 10 files changed, 151 insertions(+), 2 deletions(-)
 create mode 100644 library/algebra/numeral.lean
 create mode 100644 src/library/norm_num.cpp
 create mode 100644 src/library/norm_num.h
 create mode 100644 src/library/tactic/norm_num_tactic.cpp
 create mode 100644 src/library/tactic/norm_num_tactic.h
 create mode 100644 tests/lean/extra/num_norm1.lean

diff --git a/library/algebra/numeral.lean b/library/algebra/numeral.lean
new file mode 100644
index 000000000..964e1e813
--- /dev/null
+++ b/library/algebra/numeral.lean
@@ -0,0 +1,23 @@
+import algebra.ring -- has_add, has_one, ... will be moved to init in the future
+open algebra
+
+variable {A : Type}
+
+definition zero [s : has_zero A] : A :=
+has_zero.zero A
+
+definition one [s : has_one A] : A :=
+has_one.one A
+
+definition add [s : has_add A] : A → A → A :=
+has_add.add
+
+definition bit0 [s : has_add A] (a : A) : A :=
+add a a
+
+definition bit1 [s₁ : has_add A] [s₂ : has_one A] (a : A) : A :=
+add (add a a) one
+
+-- variables [s : ring A]
+-- set_option pp.all true
+-- check bit1 (bit0 (one : A))
diff --git a/library/init/tactic.lean b/library/init/tactic.lean
index a005e8ca4..1ac506c8d 100644
--- a/library/init/tactic.lean
+++ b/library/init/tactic.lean
@@ -46,6 +46,7 @@ definition congruence  : tactic := builtin
 definition rotate_left (k : num) := builtin
 definition rotate_right (k : num) := builtin
 definition rotate (k : num) := rotate_left k
+definition norm_num    : tactic := builtin
 
 -- This is just a trick to embed expressions into tactics.
 -- The nested expressions are "raw". They tactic should
diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt
index 79bf7b8d7..1cb422200 100644
--- a/src/library/CMakeLists.txt
+++ b/src/library/CMakeLists.txt
@@ -15,4 +15,4 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp occurs.cpp
   unfold_macros.cpp app_builder.cpp projection.cpp abbreviation.cpp
   relation_manager.cpp export.cpp user_recursors.cpp
   class_instance_synth.cpp idx_metavar.cpp composition_manager.cpp
-  tc_multigraph.cpp noncomputable.cpp aux_recursors.cpp)
+  tc_multigraph.cpp noncomputable.cpp aux_recursors.cpp norm_num.cpp)
diff --git a/src/library/norm_num.cpp b/src/library/norm_num.cpp
new file mode 100644
index 000000000..f203a02ab
--- /dev/null
+++ b/src/library/norm_num.cpp
@@ -0,0 +1,18 @@
+/*
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Rob Lewis
+*/
+#include "library/norm_num.h"
+namespace lean {
+bool norm_num_context::is_numeral(expr const &) const {
+    // TODO(Rob)
+    return false;
+}
+
+pair<expr, expr> norm_num_context::mk_norm(expr const &) {
+    // TODO(Rob)
+    throw exception("not implemented yet - norm_num`");
+}
+}
diff --git a/src/library/norm_num.h b/src/library/norm_num.h
new file mode 100644
index 000000000..59481928b
--- /dev/null
+++ b/src/library/norm_num.h
@@ -0,0 +1,27 @@
+/*
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Rob Lewis
+*/
+#pragma once
+#include "kernel/environment.h"
+
+namespace lean {
+class norm_num_context {
+    environment m_env;
+public:
+    norm_num_context(environment const & env):m_env(env) {}
+
+    bool is_numeral(expr const & e) const;
+    pair<expr, expr> mk_norm(expr const & e);
+};
+
+inline bool is_numeral(environment const & env, expr const & e) {
+    return norm_num_context(env).is_numeral(e);
+}
+
+inline pair<expr, expr> mk_norm_num(environment const & env, expr const & e) {
+    return norm_num_context(env).mk_norm(e);
+}
+}
diff --git a/src/library/tactic/CMakeLists.txt b/src/library/tactic/CMakeLists.txt
index ed9bcac47..469fe60de 100644
--- a/src/library/tactic/CMakeLists.txt
+++ b/src/library/tactic/CMakeLists.txt
@@ -6,4 +6,5 @@ expr_to_tactic.cpp location.cpp rewrite_tactic.cpp util.cpp
 init_module.cpp change_tactic.cpp check_expr_tactic.cpp let_tactic.cpp
 contradiction_tactic.cpp exfalso_tactic.cpp constructor_tactic.cpp
 injection_tactic.cpp congruence_tactic.cpp relation_tactics.cpp
-induction_tactic.cpp subst_tactic.cpp unfold_rec.cpp with_options_tactic.cpp)
+induction_tactic.cpp subst_tactic.cpp unfold_rec.cpp with_options_tactic.cpp
+norm_num_tactic.cpp)
diff --git a/src/library/tactic/init_module.cpp b/src/library/tactic/init_module.cpp
index 76c457dd7..1ad835195 100644
--- a/src/library/tactic/init_module.cpp
+++ b/src/library/tactic/init_module.cpp
@@ -32,6 +32,7 @@ Author: Leonardo de Moura
 #include "library/tactic/subst_tactic.h"
 #include "library/tactic/location.h"
 #include "library/tactic/with_options_tactic.h"
+#include "library/tactic/norm_num_tactic.h"
 
 namespace lean {
 void initialize_tactic_module() {
@@ -62,9 +63,11 @@ void initialize_tactic_module() {
     initialize_subst_tactic();
     initialize_location();
     initialize_with_options_tactic();
+    initialize_norm_num_tactic();
 }
 
 void finalize_tactic_module() {
+    finalize_norm_num_tactic();
     finalize_with_options_tactic();
     finalize_location();
     finalize_subst_tactic();
diff --git a/src/library/tactic/norm_num_tactic.cpp b/src/library/tactic/norm_num_tactic.cpp
new file mode 100644
index 000000000..bcfde814c
--- /dev/null
+++ b/src/library/tactic/norm_num_tactic.cpp
@@ -0,0 +1,53 @@
+/*
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Rob Lewis
+*/
+#include "library/util.h"
+#include "library/norm_num.h"
+#include "library/tactic/expr_to_tactic.h"
+
+namespace lean {
+tactic norm_num_tactic() {
+    return tactic01([=](environment const & env, io_state const &, proof_state const & s) {
+            goals const & gs = s.get_goals();
+            if (empty(gs)) {
+                throw_no_goal_if_enabled(s);
+                return none_proof_state();
+            }
+            goal const & g = head(gs);
+            expr const & c = g.get_type();
+            expr lhs, rhs;
+            if (!is_eq(c, lhs, rhs)) {
+                throw_tactic_exception_if_enabled(s, "norm_num tactic failed, conclusion is not an equality");
+                return none_proof_state();
+            }
+
+            try {
+                pair<expr, expr> p = mk_norm_num(env, lhs);
+                expr new_lhs = p.first;
+                expr new_pr  = p.second;
+                if (new_lhs != rhs) {
+                    throw_tactic_exception_if_enabled(s, "norm_num tactic failed, lhs normal form doesn't match rhs");
+                    return none_proof_state();
+                }
+                substitution new_subst = s.get_subst();
+                assign(new_subst, g, new_pr);
+                return some_proof_state(proof_state(s, tail(gs), new_subst));
+            } catch (exception & ex) {
+                throw_tactic_exception_if_enabled(s, ex.what());
+                return none_proof_state();
+            }
+        });
+}
+
+void initialize_norm_num_tactic() {
+    register_tac(name{"tactic", "norm_num"},
+                 [](type_checker &, elaborate_fn const &, expr const &, pos_info_provider const *) {
+                     return norm_num_tactic();
+                 });
+}
+void finalize_norm_num_tactic() {
+}
+}
diff --git a/src/library/tactic/norm_num_tactic.h b/src/library/tactic/norm_num_tactic.h
new file mode 100644
index 000000000..45871b630
--- /dev/null
+++ b/src/library/tactic/norm_num_tactic.h
@@ -0,0 +1,12 @@
+/*
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Rob Lewis
+*/
+#pragma once
+
+namespace lean {
+void initialize_norm_num_tactic();
+void finalize_norm_num_tactic();
+}
diff --git a/tests/lean/extra/num_norm1.lean b/tests/lean/extra/num_norm1.lean
new file mode 100644
index 000000000..b4f0838c1
--- /dev/null
+++ b/tests/lean/extra/num_norm1.lean
@@ -0,0 +1,11 @@
+import algebra.numeral algebra.ring
+open algebra
+
+variable {A : Type}
+variable [s : ring A]
+include s
+
+example : add (bit0 (one:A)) one = bit1 one :=
+begin
+  norm_num
+end