fix(library/tactic/constructor_tactic): bug in constructor tactic

see example (constr_tac2.lean) in comment at issue #500

src/library/tactic/apply_tactic.cpp

@@ -67,8 +67,6 @@ static void remove_redundant_metas(buffer<expr> & metas) {
 
 enum subgoals_action_kind { IgnoreSubgoals, AddRevSubgoals, AddSubgoals, AddAllSubgoals };
 
-
-
 static proof_state_seq apply_tactic_core(environment const & env, io_state const & ios, proof_state const & s,
                                          expr const & _e, buffer<constraint> & cs,
                                          bool add_meta, subgoals_action_kind subgoals_action) {
@@ -178,6 +176,12 @@ static proof_state_seq apply_tactic_core(environment const & env, io_state const
     return apply_tactic_core(env, ios, s, e, cs, add_meta, subgoals_action);
 }
 
+proof_state_seq apply_tactic_core(environment const & env, io_state const & ios, proof_state const & s, expr const & e, constraint_seq const & cs) {
+    buffer<constraint> tmp_cs;
+    cs.linearize(tmp_cs);
+    return apply_tactic_core(env, ios, s, e, tmp_cs, true, AddAllSubgoals);
+}
+
 tactic eassumption_tactic() {
     return tactic([=](environment const & env, io_state const & ios, proof_state const & s) {
             goals const & gs = s.get_goals();

src/library/tactic/apply_tactic.h

@@ -8,6 +8,7 @@ Author: Leonardo de Moura
 #include "util/lua.h"
 #include "library/tactic/elaborate.h"
 namespace lean {
+proof_state_seq apply_tactic_core(environment const & env, io_state const & ios, proof_state const & s, expr const & e, constraint_seq const & cs);
 tactic apply_tactic(elaborate_fn const & fn, expr const & e);
 tactic fapply_tactic(elaborate_fn const & fn, expr const & e);
 tactic eassumption_tactic();

src/library/tactic/constructor_tactic.cpp

@@ -10,6 +10,7 @@ Author: Leonardo de Moura
 #include "library/util.h"
 #include "library/reducible.h"
 #include "library/tactic/expr_to_tactic.h"
+#include "library/tactic/apply_tactic.h"
 
 namespace lean {
 /**
@@ -25,78 +26,69 @@ tactic constructor_tactic(elaborate_fn const & elab, unsigned _i, optional<unsig
         goals const & gs = s.get_goals();
         if (empty(gs)) {
             throw_no_goal_if_enabled(s);
-            return optional<proof_state>();
+            return proof_state_seq();
         }
         if (_i == 0) {
             throw_tactic_exception_if_enabled(s, "invalid 'constructor' tactic, index must be greater than zero");
-            return optional<proof_state>();
+            return proof_state_seq();
         }
+        constraint_seq cs;
         unsigned i = _i - 1;
         name_generator ngen = s.get_ngen();
         auto tc             = mk_type_checker(env, ngen.mk_child(), s.relax_main_opaque());
         goal const & g      = head(gs);
-        expr t              = tc->whnf(g.get_type()).first;
+        expr t              = tc->whnf(g.get_type(), cs);
         buffer<expr> I_args;
         expr I              = get_app_args(t, I_args);
         if (!is_constant(I) || !inductive::is_inductive_decl(env, const_name(I))) {
             throw_tactic_exception_if_enabled(s, "invalid 'constructor' tactic, goal is not an inductive datatype");
-            return none_proof_state();
+            return proof_state_seq();
         }
         buffer<name> c_names;
         get_intro_rule_names(env, const_name(I), c_names);
         if (num_constructors && c_names.size() != *num_constructors) {
             throw_tactic_exception_if_enabled(s, sstream() << "invalid 'constructor' tactic, goal is an inductive datatype, "
                                               << "but it does not have " << *num_constructors << " constructor(s)");
-            return none_proof_state();
+            return proof_state_seq();
         }
         if (i >= c_names.size()) {
             throw_tactic_exception_if_enabled(s, sstream() << "invalid 'constructor' tactic, goal is an inductive datatype, "
                                               << "but it has only " << c_names.size() << " constructor(s)");
-            return none_proof_state();
+            return proof_state_seq();
         }
         expr C              = mk_constant(c_names[i], const_levels(I));
         unsigned num_params = *inductive::get_num_params(env, const_name(I));
         if (I_args.size() < num_params)
-            return none_proof_state();
+            return proof_state_seq();
         proof_state new_s(s, ngen);
         C = mk_app(C, num_params, I_args.data());
-        expr C_type = tc->whnf(tc->infer(C).first).first;
+        expr C_type = tc->whnf(tc->infer(C, cs), cs);
         bool report_unassigned = true;
         bool enforce_type      = true;
         for (expr const & arg : given_args) {
             if (!is_pi(C_type)) {
                 throw_tactic_exception_if_enabled(s, sstream() << "invalid 'constructor' tactic, "
                                                   << "too many arguments have been provided");
-                return none_proof_state();
+                return proof_state_seq();
             }
             try {
                 if (auto new_arg = elaborate_with_respect_to(env, ios, elab, new_s, arg, some_expr(binding_domain(C_type)),
                                                            report_unassigned, enforce_type)) {
                     C = mk_app(C, *new_arg);
-                    C_type = tc->whnf(instantiate(binding_body(C_type), *new_arg)).first;
+                    C_type = tc->whnf(instantiate(binding_body(C_type), *new_arg), cs);
                 } else {
-                    return none_proof_state();
+                    return proof_state_seq();
                 }
             } catch (exception &) {
                 if (new_s.report_failure())
                     throw;
-                return none_proof_state();
+                return proof_state_seq();
             }
         }
-        buffer<goal> new_goals;
+
-        while (is_pi(C_type)) {
+        return apply_tactic_core(env, ios, new_s, C, cs);
-            expr new_type = binding_domain(C_type);
-            expr new_meta = g.mk_meta(tc->mk_fresh_name(), new_type);
-            goal new_goal(new_meta, new_type);
-            new_goals.push_back(new_goal);
-            C      = mk_app(C, new_meta);
-            C_type = tc->whnf(instantiate(binding_body(C_type), new_meta)).first;
-        }
-        substitution new_subst = new_s.get_subst();
-        assign(new_subst, g, C);
-        return some_proof_state(proof_state(new_s, to_list(new_goals.begin(), new_goals.end(), tail(gs)), new_subst));
     };
-    return tactic01(fn);
+    return tactic(fn);
 }
 
 void initialize_constructor_tactic() {

tests/lean/run/constr_tac2.lean

@@ -0,0 +1,7 @@
+open nat
+
+example (n m : ℕ) (H : n < m) : n < succ m :=
+begin
+  constructor 2,
+  exact H
+end