From 3ab0e07ba96974e5b1f39ca9a2d296b725bd406f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 14 Jul 2015 09:54:53 -0400
Subject: [PATCH] feat(frontends/lean): add simp tactic frontend stub

This commit also removes the fake_simplifier. It doesn't work anymore
because simp is now a reserved word.
---
 library/data/int/basic.lean              |  3 +--
 library/data/int/order.lean              |  1 -
 library/data/nat/div.lean                |  4 ++--
 library/data/nat/gcd.lean                |  2 +-
 library/data/nat/sub.lean                |  2 --
 library/data/pnat.lean                   |  8 ++++----
 library/data/quotient/util.lean          |  3 ---
 library/data/rat/order.lean              |  4 ++--
 library/data/real/basic.lean             |  8 ++++----
 library/init/tactic.lean                 |  2 +-
 library/tools/fake_simplifier.lean       |  8 --------
 src/frontends/lean/CMakeLists.txt        |  3 ++-
 src/frontends/lean/builtin_tactics.cpp   |  6 ++++++
 src/frontends/lean/parse_simp_tactic.cpp | 17 +++++++++++++++++
 src/frontends/lean/parse_simp_tactic.h   | 13 +++++++++++++
 src/frontends/lean/token_table.cpp       |  2 +-
 src/library/simplifier/CMakeLists.txt    |  2 +-
 src/library/simplifier/simp_tactic.cpp   | 15 +++++++++++++++
 src/library/simplifier/simp_tactic.h     | 21 +++++++++++++++++++++
 tests/lean/run/div2.lean                 |  3 +--
 tests/lean/run/univ_bug1.lean            |  4 ++--
 21 files changed, 94 insertions(+), 37 deletions(-)
 delete mode 100644 library/tools/fake_simplifier.lean
 create mode 100644 src/frontends/lean/parse_simp_tactic.cpp
 create mode 100644 src/frontends/lean/parse_simp_tactic.h
 create mode 100644 src/library/simplifier/simp_tactic.cpp
 create mode 100644 src/library/simplifier/simp_tactic.h

diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean
index 2f0b18c75..b9da0a1b5 100644
--- a/library/data/int/basic.lean
+++ b/library/data/int/basic.lean
@@ -27,10 +27,9 @@ following:
 -/
 import data.nat.basic data.nat.order data.nat.sub data.prod
 import algebra.relation algebra.binary algebra.ordered_ring
-import tools.fake_simplifier
 open eq.ops
 open prod relation nat
-open decidable binary fake_simplifier
+open decidable binary
 
 /- the type of integers -/
 
diff --git a/library/data/int/order.lean b/library/data/int/order.lean
index 0e11aec92..617ddc8b0 100644
--- a/library/data/int/order.lean
+++ b/library/data/int/order.lean
@@ -9,7 +9,6 @@ and transfer the results.
 import .basic algebra.ordered_ring
 open nat
 open decidable
-open fake_simplifier
 open int eq.ops
 
 namespace int
diff --git a/library/data/nat/div.lean b/library/data/nat/div.lean
index 86f02cb27..37c1a0342 100644
--- a/library/data/nat/div.lean
+++ b/library/data/nat/div.lean
@@ -5,8 +5,8 @@ Authors: Jeremy Avigad, Leonardo de Moura
 
 Definitions and properties of div and mod. Much of the development follows Isabelle's library.
 -/
-import data.nat.sub tools.fake_simplifier
-open eq.ops well_founded decidable fake_simplifier prod
+import data.nat.sub
+open eq.ops well_founded decidable prod
 
 namespace nat
 
diff --git a/library/data/nat/gcd.lean b/library/data/nat/gcd.lean
index 8a6c8b869..6c17efc77 100644
--- a/library/data/nat/gcd.lean
+++ b/library/data/nat/gcd.lean
@@ -6,7 +6,7 @@ Authors: Jeremy Avigad, Leonardo de Moura
 Definitions and properties of gcd, lcm, and coprime.
 -/
 import .div
-open eq.ops well_founded decidable fake_simplifier prod
+open eq.ops well_founded decidable prod
 
 namespace nat
 
diff --git a/library/data/nat/sub.lean b/library/data/nat/sub.lean
index 98006e87b..8a18a5c56 100644
--- a/library/data/nat/sub.lean
+++ b/library/data/nat/sub.lean
@@ -6,9 +6,7 @@ Authors: Floris van Doorn, Jeremy Avigad
 Subtraction on the natural numbers, as well as min, max, and distance.
 -/
 import .order
-import tools.fake_simplifier
 open eq.ops
-open fake_simplifier
 
 namespace nat
 
diff --git a/library/data/pnat.lean b/library/data/pnat.lean
index 4073069af..b171b42a3 100644
--- a/library/data/pnat.lean
+++ b/library/data/pnat.lean
@@ -219,9 +219,9 @@ theorem add_halves (p : ℕ+) : (2 * p)⁻¹ + (2 * p)⁻¹ = p⁻¹ :=
 
 theorem add_halves_double (m n : ℕ+) :
         m⁻¹ + n⁻¹ = ((2 * m)⁻¹ + (2 * n)⁻¹) + ((2 * m)⁻¹ + (2 * n)⁻¹) :=
-  have simp [visible] : ∀ a b : ℚ, (a + a) + (b + b) = (a + b) + (a + b),
+  have hsimp [visible] : ∀ a b : ℚ, (a + a) + (b + b) = (a + b) + (a + b),
     by intros; rewrite [rat.add.assoc, -(rat.add.assoc a b b), {_+b}rat.add.comm, -*rat.add.assoc],
-  by rewrite [-add_halves m, -add_halves n, simp]
+  by rewrite [-add_halves m, -add_halves n, hsimp]
 
 theorem inv_mul_eq_mul_inv {p q : ℕ+} : (p * q)⁻¹ = p⁻¹ * q⁻¹ :=
   by rewrite [↑inv, pnat_to_rat_mul, one_div_mul_one_div''']
@@ -297,8 +297,8 @@ theorem div_le_pnat (q : ℚ) (n : ℕ+) (H : q ≥ n⁻¹) : 1 / q ≤ rat_of_p
 
 theorem pnat_cancel' (n m : ℕ+) : (n * n * m)⁻¹ * (rat_of_pnat n * rat_of_pnat n) = m⁻¹ :=
   begin
-    have simp : ∀ a b c : ℚ, (a * a * (b * b * c)) = (a * b) * (a * b) * c, from sorry, -- simp
-    rewrite [rat.mul.comm, *inv_mul_eq_mul_inv, simp, *inv_cancel_left, *rat.one_mul]
+    have hsimp : ∀ a b c : ℚ, (a * a * (b * b * c)) = (a * b) * (a * b) * c, from sorry, -- simp
+    rewrite [rat.mul.comm, *inv_mul_eq_mul_inv, hsimp, *inv_cancel_left, *rat.one_mul]
   end
 
 definition pceil (a : ℚ) : ℕ+ := pnat.pos (ubound a) !ubound_pos
diff --git a/library/data/quotient/util.lean b/library/data/quotient/util.lean
index 898d9e564..174bd121b 100644
--- a/library/data/quotient/util.lean
+++ b/library/data/quotient/util.lean
@@ -4,10 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Floris van Doorn
 -/
 import logic ..prod algebra.relation
-import tools.fake_simplifier
-
 open prod eq.ops
-open fake_simplifier
 
 namespace quotient
 
diff --git a/library/data/rat/order.lean b/library/data/rat/order.lean
index d375c2c20..6be4c4128 100644
--- a/library/data/rat/order.lean
+++ b/library/data/rat/order.lean
@@ -324,10 +324,10 @@ section migrate_algebra
 end migrate_algebra
 
 theorem rat_of_nat_abs (a : ℤ) : abs (of_int a) = of_nat (int.nat_abs a) :=
-  have simp [visible] : ∀ n : ℕ, of_int (int.neg_succ_of_nat n) = - of_nat (nat.succ n), from λ n, rfl,
+  have hsimp [visible] : ∀ n : ℕ, of_int (int.neg_succ_of_nat n) = - of_nat (nat.succ n), from λ n, rfl,
   int.induction_on a
     (take b, abs_of_nonneg (!of_nat_nonneg))
-    (take b, by rewrite [simp, abs_neg, abs_of_nonneg (!of_nat_nonneg)])
+    (take b, by rewrite [hsimp, abs_neg, abs_of_nonneg (!of_nat_nonneg)])
 
 definition ubound : ℚ → ℕ := λ a : ℚ, nat.succ (int.nat_abs (num a))
 
diff --git a/library/data/real/basic.lean b/library/data/real/basic.lean
index 91273bfec..5c1b7fb7c 100644
--- a/library/data/real/basic.lean
+++ b/library/data/real/basic.lean
@@ -164,9 +164,9 @@ theorem eq_of_bdd {s t : seq} (Hs : regular s) (Ht : regular t)
       apply rat.add_le_add,
       apply HNj (max j Nj) (max_right j Nj),
       apply Ht,
-      have simp : ∀ m : ℕ+, n⁻¹ + m⁻¹ + (j⁻¹ + (m⁻¹ + n⁻¹)) = (n⁻¹ + n⁻¹ + j⁻¹) + (m⁻¹ + m⁻¹),
+      have hsimp : ∀ m : ℕ+, n⁻¹ + m⁻¹ + (j⁻¹ + (m⁻¹ + n⁻¹)) = (n⁻¹ + n⁻¹ + j⁻¹) + (m⁻¹ + m⁻¹),
         from sorry, -- simplifier
-      rewrite simp,
+      rewrite hsimp,
       have Hms : (max j Nj)⁻¹ + (max j Nj)⁻¹ ≤ j⁻¹ + j⁻¹, begin
         apply rat.add_le_add,
         apply inv_ge_of_le (max_left j Nj),
@@ -733,7 +733,7 @@ theorem mul_neg_equiv_neg_mul {s t : seq} : smul s (sneg t) ≡ sneg (smul s t)
 theorem equiv_of_diff_equiv_zero {s t : seq} (Hs : regular s) (Ht : regular t)
         (H : sadd s (sneg t) ≡ zero) : s ≡ t :=
   begin
-    have simp : ∀ a b c d e : ℚ, a + b + c + (d + e) = (b + d) + a + e + c, from sorry,
+    have hsimp : ∀ a b c d e : ℚ, a + b + c + (d + e) = (b + d) + a + e + c, from sorry,
     apply eq_of_bdd Hs Ht,
     intros,
     let He := bdd_of_eq H,
@@ -749,7 +749,7 @@ theorem equiv_of_diff_equiv_zero {s t : seq} (Hs : regular s) (Ht : regular t)
     let He' := λ a b c, !rat.sub_zero ▸ (He a b c),
     apply (He' _ _ Hn),
     apply Ht,
-    rewrite [simp, add_halves, -(add_halves j), -(add_halves (2 * j)), -*rat.add.assoc],
+    rewrite [hsimp, add_halves, -(add_halves j), -(add_halves (2 * j)), -*rat.add.assoc],
     apply rat.add_le_add_right,
     apply add_le_add_three,
     repeat (apply rat.le.trans; apply inv_ge_of_le Hn; apply inv_two_mul_le_inv)
diff --git a/library/init/tactic.lean b/library/init/tactic.lean
index 6539d9f45..bd27e8193 100644
--- a/library/init/tactic.lean
+++ b/library/init/tactic.lean
@@ -99,7 +99,7 @@ definition krewrite_tac (e : expr_list) : tactic := builtin
 --  - x : exclude the give global rewrites
 --  - t : tactic for discharging conditions
 --  - l : location
-definition simp_tac (d a : bool) (e : expr_list) (n : identifier_list) (x : identifier_list) (t : option tactic) (l : expr) : tactic := builtin
+definition simp_tac (e : expr_list) (n : identifier_list) (x : identifier_list) (t : option tactic) (l : expr) : tactic := builtin
 
 -- with_options_tac is just a marker for the builtin 'with_options' notation
 definition with_options_tac (o : expr) (t : tactic) : tactic := builtin
diff --git a/library/tools/fake_simplifier.lean b/library/tools/fake_simplifier.lean
deleted file mode 100644
index ff5bf6273..000000000
--- a/library/tools/fake_simplifier.lean
+++ /dev/null
@@ -1,8 +0,0 @@
-open tactic
-
-namespace fake_simplifier
-
--- until we have the simplifier...
-definition simp : tactic := apply sorry
-
-end fake_simplifier
diff --git a/src/frontends/lean/CMakeLists.txt b/src/frontends/lean/CMakeLists.txt
index a18a53b25..1501bf1c2 100644
--- a/src/frontends/lean/CMakeLists.txt
+++ b/src/frontends/lean/CMakeLists.txt
@@ -9,6 +9,7 @@ coercion_elaborator.cpp info_tactic.cpp
 init_module.cpp elaborator_context.cpp calc_proof_elaborator.cpp
 parse_tactic_location.cpp parse_rewrite_tactic.cpp builtin_tactics.cpp
 type_util.cpp elaborator_exception.cpp migrate_cmd.cpp local_ref_info.cpp
-obtain_expr.cpp decl_attributes.cpp nested_declaration.cpp parse_with_options_tactic.cpp)
+obtain_expr.cpp decl_attributes.cpp nested_declaration.cpp
+parse_with_options_tactic.cpp parse_simp_tactic.cpp)
 
 target_link_libraries(lean_frontend ${LEAN_LIBS})
diff --git a/src/frontends/lean/builtin_tactics.cpp b/src/frontends/lean/builtin_tactics.cpp
index 9359f43d2..765ea0964 100644
--- a/src/frontends/lean/builtin_tactics.cpp
+++ b/src/frontends/lean/builtin_tactics.cpp
@@ -10,6 +10,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/parser.h"
 #include "frontends/lean/parse_rewrite_tactic.h"
 #include "frontends/lean/parse_with_options_tactic.h"
+#include "frontends/lean/parse_simp_tactic.h"
 
 namespace lean {
 namespace notation {
@@ -52,6 +53,10 @@ static expr parse_with_options_tactic_expr(parser & p, unsigned, expr const *, p
     return p.save_pos(parse_with_options_tactic(p), pos);
 }
 
+static expr parse_simp_tactic_expr(parser & p, unsigned, expr const *, pos_info const & pos) {
+    return p.save_pos(parse_simp_tactic(p), pos);
+}
+
 static expr parse_generalize_tactic(parser & p, unsigned, expr const *, pos_info const & pos) {
     expr e = p.parse_tactic_expr_arg();
     name id;
@@ -83,6 +88,7 @@ parse_table init_tactic_nud_table() {
     r = r.add({transition("fold",         mk_ext_action(parse_fold_tactic_expr))}, x0);
     r = r.add({transition("let",          mk_ext_action(parse_let_tactic))}, x0);
     r = r.add({transition("with_options", mk_ext_action(parse_with_options_tactic_expr))}, x0);
+    r = r.add({transition("simp",         mk_ext_action(parse_simp_tactic_expr))}, x0);
     return r;
 }
 
diff --git a/src/frontends/lean/parse_simp_tactic.cpp b/src/frontends/lean/parse_simp_tactic.cpp
new file mode 100644
index 000000000..f66eb3bbf
--- /dev/null
+++ b/src/frontends/lean/parse_simp_tactic.cpp
@@ -0,0 +1,17 @@
+/*
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "library/tactic/exact_tactic.h"
+#include "frontends/lean/parser.h"
+
+namespace lean {
+expr parse_simp_tactic(parser & p) {
+    // TODO(Leo)
+    auto pos = p.pos();
+    expr sorry = p.mk_sorry(pos);
+    return p.mk_app(get_exact_tac_fn(), sorry, pos);
+}
+}
diff --git a/src/frontends/lean/parse_simp_tactic.h b/src/frontends/lean/parse_simp_tactic.h
new file mode 100644
index 000000000..fafa4ceaf
--- /dev/null
+++ b/src/frontends/lean/parse_simp_tactic.h
@@ -0,0 +1,13 @@
+/*
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "kernel/expr.h"
+
+namespace lean {
+class parser;
+expr parse_simp_tactic(parser & p);
+}
diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp
index fefde9c92..a3acf93e0 100644
--- a/src/frontends/lean/token_table.cpp
+++ b/src/frontends/lean/token_table.cpp
@@ -95,7 +95,7 @@ void init_token_table(token_table & t) {
          {"{|", g_max_prec}, {"|}", 0}, {"⊢", 0}, {"⟨", g_max_prec}, {"⟩", 0}, {"^", 0}, {"↑", 0}, {"▸", 0},
          {"using", 0}, {"|", 0}, {"!", g_max_prec}, {"?", 0},  {"with", 0}, {"...", 0}, {",", 0},
          {".", 0}, {":", 0}, {"::", 0}, {"calc", 0}, {"rewrite", 0}, {"xrewrite", 0}, {"krewrite", 0},
-         {"esimp", 0}, {"fold", 0}, {"unfold", 0}, {"with_options", 0},
+         {"esimp", 0}, {"fold", 0}, {"unfold", 0}, {"with_options", 0}, {"simp", 0},
          {"generalize", 0}, {"as", 0}, {":=", 0}, {"--", 0}, {"#", 0},
          {"(*", 0}, {"/-", 0}, {"begin", g_max_prec}, {"begin+", g_max_prec}, {"abstract", g_max_prec},
          {"proof", g_max_prec}, {"qed", 0}, {"@", g_max_prec},
diff --git a/src/library/simplifier/CMakeLists.txt b/src/library/simplifier/CMakeLists.txt
index dde092baf..c9a1ac96c 100644
--- a/src/library/simplifier/CMakeLists.txt
+++ b/src/library/simplifier/CMakeLists.txt
@@ -1,2 +1,2 @@
-add_library(simplifier ceqv.cpp rewrite_rule_set.cpp init_module.cpp)
+add_library(simplifier ceqv.cpp rewrite_rule_set.cpp init_module.cpp simp_tactic.cpp)
 target_link_libraries(simplifier ${LEAN_LIBS})
diff --git a/src/library/simplifier/simp_tactic.cpp b/src/library/simplifier/simp_tactic.cpp
new file mode 100644
index 000000000..8662b0907
--- /dev/null
+++ b/src/library/simplifier/simp_tactic.cpp
@@ -0,0 +1,15 @@
+/*
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "library/simplifier/simp_tactic.h"
+
+namespace lean {
+expr mk_simp_tactic_expr(buffer<expr> const & /* ls */, buffer<name> const & /* ns */,
+                         buffer<name> const & /* ex */, optional<expr> const & /* pre_tac */,
+                         location const & /* loc */) {
+    return expr();
+}
+}
diff --git a/src/library/simplifier/simp_tactic.h b/src/library/simplifier/simp_tactic.h
new file mode 100644
index 000000000..16d3478c3
--- /dev/null
+++ b/src/library/simplifier/simp_tactic.h
@@ -0,0 +1,21 @@
+/*
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "kernel/expr.h"
+#include "library/tactic/location.h"
+
+namespace lean {
+/** \brief Create a simp tactic expression where
+    - ls is a collection of pre-terms representing additional lemmas that should be used as rewriting rules.
+    - ns is a collection of namespaces that should provide rewriting rules for this tactic.
+    - ex is a collection of global rewriting rules that should be excluded.
+    - pre_tac (if provided) is a tactic used to discharge assumptions in conditional rewriting rules.
+    - loc is the scope of the tactic (i.e., which hypothesis and/or conclusion will be simplified).
+*/
+expr mk_simp_tactic_expr(buffer<expr> const & ls, buffer<name> const & ns, buffer<name> const & ex,
+                         optional<expr> const & pre_tac, location const & loc);
+}
diff --git a/tests/lean/run/div2.lean b/tests/lean/run/div2.lean
index e03c137c6..47bcb42a7 100644
--- a/tests/lean/run/div2.lean
+++ b/tests/lean/run/div2.lean
@@ -1,8 +1,7 @@
 import logic data.nat.sub algebra.relation data.prod
-import tools.fake_simplifier
 
 open nat relation relation.iff_ops prod
-open fake_simplifier decidable
+open decidable
 open eq.ops
 
 namespace nat
diff --git a/tests/lean/run/univ_bug1.lean b/tests/lean/run/univ_bug1.lean
index 61e13da32..2919ddf0a 100644
--- a/tests/lean/run/univ_bug1.lean
+++ b/tests/lean/run/univ_bug1.lean
@@ -7,7 +7,7 @@
 import logic data.nat
 open nat
 
-namespace simp
+namespace nsimp
 -- set_option pp.universes true
 -- set_option pp.implicit true
 
@@ -25,4 +25,4 @@ theorem simp_app [instance] (S T : Type) (f1 f2 : S → T) (s1 s2 : S)
    (C1 : simplifies_to f1 f2) (C2 : simplifies_to s1 s2) : simplifies_to (f1 s1) (f2 s2) :=
 simplifies_to.mk (congr (get_eq C1) (get_eq C2))
 
-end simp
+end nsimp