From c3dfabf7418b29d1e9e94feae2c599cddd8219f8 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 31 Dec 2015 15:00:38 -0800
Subject: [PATCH] feat(library/blast/strategies/portfolio): add 'rec_simp'

recursors followed by simplification
---
 library/data/nat/basic.lean                | 20 ++++++++++----------
 library/init/tactic.lean                   |  1 +
 src/library/blast/strategies/portfolio.cpp |  6 ++++++
 3 files changed, 17 insertions(+), 10 deletions(-)

diff --git a/library/data/nat/basic.lean b/library/data/nat/basic.lean
index a29f05541d..8c4ea0a530 100644
--- a/library/data/nat/basic.lean
+++ b/library/data/nat/basic.lean
@@ -116,21 +116,21 @@ the associated [simp] lemmas from algebra
 local attribute nat.add_zero nat.add_succ [simp]
 
 protected theorem zero_add (n : ℕ) : 0 + n = n :=
-nat.induction_on n (by simp) (by simp)
+by rec_simp
 
 theorem succ_add (n m : ℕ) : (succ n) + m = succ (n + m) :=
-nat.induction_on m (by simp) (by simp)
+by rec_simp
 
 local attribute nat.zero_add nat.succ_add [simp]
 
 protected theorem add_comm (n m : ℕ) : n + m = m + n :=
-nat.induction_on m (by simp) (by simp)
+by rec_simp
 
 theorem succ_add_eq_succ_add (n m : ℕ) : succ n + m = n + succ m :=
 by simp
 
 protected theorem add_assoc (n m k : ℕ) : (n + m) + k = n + (m + k) :=
-nat.induction_on k (by simp) (by simp)
+by rec_simp
 
 protected theorem add_left_comm : Π (n m k : ℕ), n + (m + k) = m + (n + k) :=
 left_comm nat.add_comm nat.add_assoc
@@ -179,26 +179,26 @@ local attribute nat.mul_zero nat.mul_succ [simp]
 -- commutativity, distributivity, associativity, identity
 
 protected theorem zero_mul (n : ℕ) : 0 * n = 0 :=
-nat.induction_on n (by simp) (by simp)
+by rec_simp
 
 theorem succ_mul (n m : ℕ) : (succ n) * m = (n * m) + m :=
-nat.induction_on m (by simp) (by simp)
+by rec_simp
 
 local attribute nat.zero_mul nat.succ_mul [simp]
 
 protected theorem mul_comm (n m : ℕ) : n * m = m * n :=
-nat.induction_on m (by simp) (by simp)
+by rec_simp
 
 protected theorem right_distrib (n m k : ℕ) : (n + m) * k = n * k + m * k :=
-nat.induction_on k (by simp) (by simp)
+by rec_simp
 
 protected theorem left_distrib (n m k : ℕ) : n * (m + k) = n * m + n * k :=
-nat.induction_on k (by simp) (by simp)
+by rec_simp
 
 local attribute nat.mul_comm nat.right_distrib nat.left_distrib [simp]
 
 protected theorem mul_assoc (n m k : ℕ) : (n * m) * k = n * (m * k) :=
-nat.induction_on k (by simp) (by simp)
+by rec_simp
 
 local attribute nat.mul_assoc [simp]
 
diff --git a/library/init/tactic.lean b/library/init/tactic.lean
index c17bf02402..cb06353db2 100644
--- a/library/init/tactic.lean
+++ b/library/init/tactic.lean
@@ -111,6 +111,7 @@ definition simp          : tactic := #tactic with_options [blast.strategy "simp"
 definition simp_nohyps   : tactic := #tactic with_options [blast.strategy "simp_nohyps"] blast
 definition simp_topdown  : tactic := #tactic with_options [blast.strategy "simp", simplify.top_down true] blast
 definition inst_simp     : tactic := #tactic with_options [blast.strategy "ematch_simp"] blast
+definition rec_simp      : tactic := #tactic with_options [blast.strategy "rec_simp"] blast
 definition rec_inst_simp : tactic := #tactic with_options [blast.strategy "rec_ematch_simp"] blast
 
 definition cases (h : expr) (ids : opt_identifier_list) : tactic := builtin
diff --git a/src/library/blast/strategies/portfolio.cpp b/src/library/blast/strategies/portfolio.cpp
index 8eccff41ec..772e119489 100644
--- a/src/library/blast/strategies/portfolio.cpp
+++ b/src/library/blast/strategies/portfolio.cpp
@@ -59,6 +59,10 @@ static optional<expr> apply_ematch_simp() {
                               ematch_simp_action)();
 }
 
+static optional<expr> apply_rec_simp() {
+    return rec_and_then(apply_simp)();
+}
+
 static optional<expr> apply_rec_ematch_simp() {
     return rec_and_then(apply_ematch_simp)();
 }
@@ -112,6 +116,8 @@ optional<expr> apply_strategy() {
         return apply_ematch_simp();
     } else if (s_name == "rec_ematch_simp") {
         return apply_rec_ematch_simp();
+    } else if (s_name == "rec_simp") {
+        return apply_rec_simp();
     } else if (s_name == "constructor") {
         return apply_constructor();
     } else if (s_name == "unit") {