feat(library/tactic): automate "generalize-intro-induction/cases" idiom

closes #645

hott/init/tactic.hlean

@@ -91,9 +91,9 @@ definition rewrite_tac  (e : expr_list) : tactic := builtin
 definition xrewrite_tac (e : expr_list) : tactic := builtin
 definition krewrite_tac (e : expr_list) : tactic := builtin
 
-definition cases (id : identifier) (ids : opt_identifier_list) : tactic := builtin
+definition cases (h : expr) (ids : opt_identifier_list) : tactic := builtin
 
-definition induction (h : identifier) (rec : using_expr) (ids : opt_identifier_list) : tactic := builtin
+definition induction (h : expr) (rec : using_expr) (ids : opt_identifier_list) : tactic := builtin
 
 definition intros (ids : opt_identifier_list) : tactic := builtin
 

library/init/tactic.lean

@@ -91,9 +91,9 @@ definition rewrite_tac  (e : expr_list) : tactic := builtin
 definition xrewrite_tac (e : expr_list) : tactic := builtin
 definition krewrite_tac (e : expr_list) : tactic := builtin
 
-definition cases (id : identifier) (ids : opt_identifier_list) : tactic := builtin
+definition cases (h : expr) (ids : opt_identifier_list) : tactic := builtin
 
-definition induction (h : identifier) (rec : using_expr) (ids : opt_identifier_list) : tactic := builtin
+definition induction (h : expr) (rec : using_expr) (ids : opt_identifier_list) : tactic := builtin
 
 definition intros (ids : opt_identifier_list) : tactic := builtin
 

src/frontends/lean/parser.cpp

@@ -1588,7 +1588,8 @@ expr parser::parse_tactic_nud() {
                     r = mk_app(r, parse_tactic_option_num(), id_pos);
                 } else {
                     unsigned rbp;
-                    if (arity == 1 || (arity == 2 && i == 0 && is_tactic_opt_identifier_list_type(ds[1])))
+                    if ((arity == 1) ||
+                        (arity >= 2 && i == 0 && (is_tactic_opt_identifier_list_type(ds[1]) || is_tactic_using_expr(ds[1]))))
                         rbp = 0;
                     else
                         rbp = get_max_prec();

src/library/tactic/generalize_tactic.cpp

@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #include "library/constants.h"
 #include "kernel/abstract.h"
+#include "kernel/instantiate.h"
 #include "kernel/kernel_exception.h"
 #include "library/reducible.h"
 #include "library/util.h"
@@ -18,50 +19,73 @@ expr mk_generalize_tactic_expr(expr const & e, name const & id) {
                   e, mk_constant(id));
 }
 
+optional<proof_state> generalize_core(environment const & env, io_state const & ios, elaborate_fn const & elab,
+                                      expr const & e, name const & x, proof_state const & s, name const & tac_name,
+                                      bool intro) {
+    proof_state new_s = s;
+    if (auto new_e = elaborate_with_respect_to(env, ios, elab, new_s, e)) {
+        name_generator ngen = new_s.get_ngen();
+        substitution subst  = new_s.get_subst();
+        goals const & gs    = new_s.get_goals();
+        goal const & g      = head(gs);
+        auto tc     = mk_type_checker(env, ngen.mk_child());
+        auto e_t_cs = tc->infer(*new_e);
+        if (e_t_cs.second) {
+            throw_tactic_exception_if_enabled(s, sstream() << "invalid '" << tac_name << "' tactic, unification constraints "
+                                              "have been generated when inferring type");
+            return none_proof_state(); // constraints were generated
+        }
+        expr e_t    = e_t_cs.first;
+        expr t      = subst.instantiate(g.get_type());
+        name n;
+        if (is_constant(e))
+            n = const_name(e);
+        else if (is_local(e))
+            n = local_pp_name(e);
+        else
+            n = x;
+        expr new_t, new_m, new_val;
+        if (intro) {
+            buffer<expr> hyps;
+            g.get_hyps(hyps);
+            expr new_h = mk_local(ngen.next(), get_unused_name(x, hyps), e_t, binder_info());
+            new_t   = instantiate(abstract(t, *new_e), new_h);
+            new_m   = mk_metavar(ngen.next(), Pi(hyps, Pi(new_h, new_t)));
+            new_m   = mk_app(new_m, hyps);
+            new_val = mk_app(new_m, *new_e);
+            new_m   = mk_app(new_m, new_h);
+        } else {
+            new_t   = mk_pi(n, e_t, abstract(t, *new_e));
+            new_m   = g.mk_meta(ngen.next(), new_t);
+            new_val = mk_app(new_m, *new_e);
+        }
+        try {
+            check_term(*tc, g.abstract(new_t));
+        } catch (kernel_exception const & ex) {
+            std::shared_ptr<kernel_exception> ex_ptr(static_cast<kernel_exception*>(ex.clone()));
+            throw_tactic_exception_if_enabled(s, [=](formatter const & fmt) {
+                    format r = format("invalid '") + format(tac_name) + format("' tactic, type error");
+                    r       += line();
+                    r       += ex_ptr->pp(fmt);
+                    return r;
+                });
+            return none_proof_state();
+        }
+        assign(subst, g, new_val);
+        goal new_g(new_m, new_t);
+        return some(proof_state(new_s, goals(new_g, tail(gs)), subst, ngen));
+    }
+    return none_proof_state();
+}
+
+optional<proof_state> generalize(environment const & env, io_state const & ios, elaborate_fn const & elab,
+                                 expr const & e, name const & x, proof_state const & s) {
+    return generalize_core(env, ios, elab, e, x, s, "generalize", false);
+}
+
 tactic generalize_tactic(elaborate_fn const & elab, expr const & e, name const & x) {
     return tactic01([=](environment const & env, io_state const & ios, proof_state const & s) {
-            proof_state new_s = s;
+            return generalize(env, ios, elab, e, x, s);
-            if (auto new_e = elaborate_with_respect_to(env, ios, elab, new_s, e)) {
-                name_generator ngen = new_s.get_ngen();
-                substitution subst  = new_s.get_subst();
-                goals const & gs    = new_s.get_goals();
-                goal const & g      = head(gs);
-                auto tc     = mk_type_checker(env, ngen.mk_child());
-                auto e_t_cs = tc->infer(*new_e);
-                if (e_t_cs.second) {
-                    throw_tactic_exception_if_enabled(s, "invalid 'generalize' tactic, unification constraints "
-                                                      "have been generated when inferring type");
-                    return none_proof_state(); // constraints were generated
-                }
-                expr e_t    = e_t_cs.first;
-                expr t      = subst.instantiate(g.get_type());
-                name n;
-                if (is_constant(e))
-                    n = const_name(e);
-                else if (is_local(e))
-                    n = local_pp_name(e);
-                else
-                    n = x;
-                expr new_t = mk_pi(n, e_t, abstract(t, *new_e));
-                expr new_m = g.mk_meta(ngen.next(), new_t);
-                try {
-                    check_term(*tc, g.abstract(new_t));
-                } catch (kernel_exception const & ex) {
-                    std::shared_ptr<kernel_exception> ex_ptr(static_cast<kernel_exception*>(ex.clone()));
-                    throw_tactic_exception_if_enabled(s, [=](formatter const & fmt) {
-                            format r = format("invalid 'generalize' tactic, type error");
-                            r       += line();
-                            r       += ex_ptr->pp(fmt);
-                            return r;
-                        });
-                    return none_proof_state();
-                }
-
-                assign(subst, g, mk_app(new_m, *new_e));
-                goal new_g(new_m, new_t);
-                return some(proof_state(new_s, goals(new_g, tail(gs)), subst, ngen));
-            }
-            return none_proof_state();
         });
 }
 

src/library/tactic/generalize_tactic.h

@@ -9,6 +9,9 @@ Author: Leonardo de Moura
 
 namespace lean {
 expr mk_generalize_tactic_expr(expr const & e, name const & id);
+optional<proof_state> generalize_core(environment const & env, io_state const & ios, elaborate_fn const & elab,
+                                      expr const & e, name const & x, proof_state const & s, name const & tac_name,
+                                      bool intro);
 void initialize_generalize_tactic();
 void finalize_generalize_tactic();
 }

src/library/tactic/induction_tactic.cpp

@@ -14,6 +14,7 @@ Author: Leonardo de Moura
 #include "library/locals.h"
 #include "library/tactic/tactic.h"
 #include "library/tactic/expr_to_tactic.h"
+#include "library/tactic/generalize_tactic.h"
 #include "library/tactic/class_instance_synth.h"
 
 namespace lean {
@@ -386,14 +387,30 @@ tactic induction_tactic(name const & H, optional<name> rec, list<name> const & i
     return tactic01(fn);
 }
 
+tactic induction_tactic(elaborate_fn const & elab, expr const & H, optional<name> rec, list<name> const & ids, expr const & ref) {
+    auto fn = [=](environment const & env, io_state const & ios, proof_state const & ps) {
+        name Haux{"H", "ind"};
+        auto new_ps = generalize_core(env, ios, elab, H, Haux, ps, "induction", true);
+        if (!new_ps)
+            return proof_state_seq();
+        goal g      = head(new_ps->get_goals());
+        expr new_H  = app_arg(g.get_meta());
+        lean_assert(is_local(new_H));
+        name H_name = local_pp_name(new_H);
+        return induction_tactic(H_name, rec, ids, ref)(env, ios, *new_ps);
+    };
+    return tactic(fn);
+}
+
 void initialize_induction_tactic() {
     register_tac(name{"tactic", "induction"},
-                 [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) {
+                 [](type_checker &, elaborate_fn const & elab, expr const & e, pos_info_provider const *) {
                      buffer<expr> args;
                      get_app_args(e, args);
                      if (args.size() != 3)
                          throw expr_to_tactic_exception(e, "invalid 'induction' tactic, insufficient number of arguments");
-                     name H = tactic_expr_to_id(args[0], "invalid 'induction' tactic, argument must be an identifier");
+                     check_tactic_expr(args[0], "invalid 'induction' tactic, argument must be an expression");
+                     expr H = get_tactic_expr_expr(args[0]);
                      buffer<name> ids;
                      get_tactic_id_list_elements(args[2], ids, "invalid 'induction' tactic, list of identifiers expected");
                      check_tactic_expr(args[1], "invalid 'induction' tactic, invalid argument");
@@ -403,9 +420,15 @@ void initialize_induction_tactic() {
                      }
                      name const & cname = const_name(rec);
                      if (cname == get_tactic_none_expr_name()) {
-                         return induction_tactic(H, optional<name>(), to_list(ids.begin(), ids.end()), e);
+                         if (is_local(H))
+                             return induction_tactic(local_pp_name(H), optional<name>(), to_list(ids.begin(), ids.end()), e);
+                         else
+                             return induction_tactic(elab, H, optional<name>(), to_list(ids.begin(), ids.end()), e);
                      } else {
-                         return induction_tactic(H, optional<name>(cname), to_list(ids.begin(), ids.end()), e);
+                         if (is_local(H))
+                             return induction_tactic(local_pp_name(H), optional<name>(cname), to_list(ids.begin(), ids.end()), e);
+                         else
+                             return induction_tactic(elab, H, optional<name>(), to_list(ids.begin(), ids.end()), e);
                      }
                  });
 }

src/library/tactic/inversion_tactic.cpp

@@ -19,6 +19,7 @@ Author: Leonardo de Moura
 #include "library/tactic/expr_to_tactic.h"
 #include "library/tactic/class_instance_synth.h"
 #include "library/tactic/inversion_tactic.h"
+#include "library/tactic/generalize_tactic.h"
 #include "library/tactic/clear_tactic.h"
 
 namespace lean {
@@ -1112,13 +1113,32 @@ tactic inversion_tactic(name const & n, list<name> const & ids) {
     return tactic01(fn);
 }
 
+tactic inversion_tactic(elaborate_fn const & elab, expr const & H, list<name> const & ids) {
+    auto fn = [=](environment const & env, io_state const & ios, proof_state const & ps) {
+        name Haux{"H", "cases"};
+        auto new_ps = generalize_core(env, ios, elab, H, Haux, ps, "cases", true);
+        if (!new_ps)
+            return proof_state_seq();
+        goal g      = head(new_ps->get_goals());
+        expr new_H  = app_arg(g.get_meta());
+        lean_assert(is_local(new_H));
+        name H_name = local_pp_name(new_H);
+        return inversion_tactic(H_name, ids)(env, ios, *new_ps);
+    };
+    return tactic(fn);
+}
+
 void initialize_inversion_tactic() {
     register_tac(get_tactic_cases_name(),
-                 [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) {
+                 [](type_checker &, elaborate_fn const & elab, expr const & e, pos_info_provider const *) {
-                     name n = tactic_expr_to_id(app_arg(app_fn(e)), "invalid 'cases' tactic, argument must be an identifier");
+                     check_tactic_expr(app_arg(app_fn(e)), "invalid 'cases' tactic, argument must be an expression");
+                     expr H = get_tactic_expr_expr(app_arg(app_fn(e)));
                      buffer<name> ids;
                      get_tactic_id_list_elements(app_arg(e), ids, "invalid 'cases' tactic, list of identifiers expected");
-                     return inversion_tactic(n, to_list(ids.begin(), ids.end()));
+                     if (is_local(H))
+                         return inversion_tactic(local_pp_name(H), to_list(ids.begin(), ids.end()));
+                     else
+                         return inversion_tactic(elab, H, to_list(ids.begin(), ids.end()));
                  });
 }
 void finalize_inversion_tactic() {}

tests/lean/errors.lean.expected.out

@@ -1,6 +1,6 @@
 errors.lean:4:0: error: unknown identifier 'a'
 tst1 : nat → nat → nat
-errors.lean:12:16: error: invalid 'begin-end' expression, ',' expected
+errors.lean:12:8: error: unknown identifier 'add'
 errors.lean:22:12: error: unknown identifier 'b'
 tst3 : A → A → A
 foo.tst1 : ℕ → ℕ → ℕ

tests/lean/run/645a.lean

@@ -0,0 +1,22 @@
+open bool
+
+definition to_pred {A : Type} (p : A → bool) : A → Prop :=
+λ a, p a = tt
+
+definition to_pred_dec₁ [instance] {A : Type} (p : A → bool)
+                : decidable_pred (to_pred p) :=
+begin
+  intro a, unfold to_pred,
+  induction p a,
+    right, contradiction,
+    left, reflexivity
+end
+
+definition to_pred_dec₂ [instance] {A : Type} (p : A → bool)
+                : decidable_pred (to_pred p) :=
+begin
+  intro a, unfold to_pred,
+  cases p a,
+    right, contradiction,
+    left, reflexivity
+end