From 921d72b6c46c1c0bb336be4e370d967525efeabc Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 24 Feb 2017 16:26:47 -0800
Subject: [PATCH] feat(library/init/meta): add helper tactics

---
 library/init/meta/attribute.lean |  8 +++++---
 library/init/meta/tactic.lean    |  3 +++
 tests/lean/run/cpdt.lean         | 21 ++++++++++-----------
 3 files changed, 18 insertions(+), 14 deletions(-)

diff --git a/library/init/meta/attribute.lean b/library/init/meta/attribute.lean
index b8479bc2c7..a963246c64 100644
--- a/library/init/meta/attribute.lean
+++ b/library/init/meta/attribute.lean
@@ -25,14 +25,16 @@ meta constant caching_user_attribute.get_cache : Π {α : Type}, caching_user_at
 
 open tactic
 
+meta def register_attribute := attribute.register
+
 meta def mk_name_set_attr (attr_name : name) : command :=
 do t ← to_expr ``(caching_user_attribute name_set),
    v ← to_expr ``({name     := %%(quote attr_name),
                    descr    := "name_set attribute",
-                   mk_cache := λ ns, return $ name_set.of_list ns,
+                   mk_cache := λ ns, return (name_set.of_list ns),
                    dependencies := [] } : caching_user_attribute name_set),
-   add_decl (declaration.defn attr_name [] t v reducibility_hints.abbrev ff),
-   attribute.register attr_name
+   add_meta_definition attr_name [] t v,
+   register_attribute attr_name
 
 meta def get_name_set_for_attr (attr_name : name) : tactic name_set :=
 do
diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean
index 3c00e05c5f..547ccc017c 100644
--- a/library/init/meta/tactic.lean
+++ b/library/init/meta/tactic.lean
@@ -930,6 +930,9 @@ match _root_.try_for max (tac s) with
 | none   := mk_exception "try_for tactic failed, timeout" none s
 end
 
+meta def add_meta_definition (n : name) (lvls : list name) (type value : expr) : tactic unit :=
+add_decl (declaration.defn n lvls type value reducibility_hints.abbrev ff)
+
 end tactic
 
 notation [parsing_only] `command`:max := tactic unit
diff --git a/tests/lean/run/cpdt.lean b/tests/lean/run/cpdt.lean
index 4f9fce5232..086c8b7f50 100644
--- a/tests/lean/run/cpdt.lean
+++ b/tests/lean/run/cpdt.lean
@@ -1,4 +1,3 @@
-import tools.mini_crush
 /- "Proving in the Large" chapter of CPDT -/
 
 inductive exp : Type
@@ -8,21 +7,16 @@ inductive exp : Type
 
 open exp
 
-def exp_eval : exp → nat
+def eeval : exp → nat
 | (Const n)    := n
-| (Plus e1 e2) := exp_eval e1 + exp_eval e2
-| (Mult e1 e2) := exp_eval e1 * exp_eval e2
+| (Plus e1 e2) := eeval e1 + eeval e2
+| (Mult e1 e2) := eeval e1 * eeval e2
 
 def times (k : nat) : exp → exp
 | (Const n)    := Const (k * n)
 | (Plus e1 e2) := Plus (times e1) (times e2)
 | (Mult e1 e2) := Mult (times e1) e2
 
-attribute [simp] mul_add
-
-@[simp] theorem eval_times : ∀ (k e), exp_eval (times k e) = k * exp_eval e :=
-by mini_crush
-
 def reassoc : exp → exp
 | (Const n)    := (Const n)
 | (Plus e1 e2) :=
@@ -40,5 +34,10 @@ def reassoc : exp → exp
   | _              := Mult e1' e2'
   end
 
-theorem reassoc_correct (e) : exp_eval (reassoc e) = exp_eval e :=
-by mini_crush
+attribute [simp] mul_add times reassoc eeval
+
+theorem eeval_times (k e) : eeval (times k e) = k * eeval e :=
+by induction e; simph
+
+theorem reassoc_correct (e) : eeval (reassoc e) = eeval e :=
+by induction e; simph; cases (reassoc e2); rsimp