feat(library/tactic): add 'constructor', 'split', 'left', 'right' and 'existsi' tactics

see issue #500

hott/init/tactic.hlean

@@ -100,6 +100,12 @@ opaque definition assert_hypothesis (id : identifier) (e : expr) : tactic := bui
 
 opaque definition lettac (id : identifier) (e : expr) : tactic := builtin
 
+opaque definition constructor (k : num) : tactic := builtin
+opaque definition existsi (e : expr)    : tactic := builtin
+opaque definition split                 : tactic := builtin
+opaque definition left                  : tactic := builtin
+opaque definition right                 : tactic := builtin
+
 definition try         (t : tactic) : tactic := or_else t id
 definition repeat1     (t : tactic) : tactic := and_then t (repeat t)
 definition focus       (t : tactic) : tactic := focus_at t 0

library/init/tactic.lean

@@ -43,7 +43,7 @@ opaque definition beta        : tactic := builtin
 opaque definition info        : tactic := builtin
 opaque definition whnf        : tactic := builtin
 opaque definition contradiction : tactic := builtin
-opaque definition exfalso : tactic := builtin
+opaque definition exfalso     : tactic := builtin
 opaque definition rotate_left (k : num) := builtin
 opaque definition rotate_right (k : num) := builtin
 definition rotate (k : num) := rotate_left k
@@ -100,6 +100,12 @@ opaque definition assert_hypothesis (id : identifier) (e : expr) : tactic := bui
 
 opaque definition lettac (id : identifier) (e : expr) : tactic := builtin
 
+opaque definition constructor (k : num) : tactic := builtin
+opaque definition existsi (e : expr)    : tactic := builtin
+opaque definition split                 : tactic := builtin
+opaque definition left                  : tactic := builtin
+opaque definition right                 : tactic := builtin
+
 definition try         (t : tactic) : tactic := or_else t id
 definition repeat1     (t : tactic) : tactic := and_then t (repeat t)
 definition focus       (t : tactic) : tactic := focus_at t 0

src/emacs/lean-syntax.el

@@ -135,7 +135,7 @@
                 "apply" "fapply" "rename" "intro" "intros" "all_goals" "fold"
                 "generalize" "generalizes" "clear" "clears" "revert" "reverts" "back" "beta" "done" "exact" "rexact"
                 "refine" "repeat" "whnf" "rotate" "rotate_left" "rotate_right" "inversion" "cases" "rewrite" "esimp"
-                "unfold" "change" "check_expr" "contradiction" "exfalso"))
+                "unfold" "change" "check_expr" "contradiction" "exfalso" "split" "existsi" "constructor" "left" "right"))
            word-end)
       (1 'font-lock-constant-face))
      ;; Types

src/library/tactic/CMakeLists.txt

@@ -5,6 +5,6 @@ inversion_tactic.cpp whnf_tactic.cpp revert_tactic.cpp
 assert_tactic.cpp clear_tactic.cpp expr_to_tactic.cpp location.cpp
 rewrite_tactic.cpp util.cpp class_instance_synth.cpp init_module.cpp
 change_tactic.cpp check_expr_tactic.cpp let_tactic.cpp contradiction_tactic.cpp
-exfalso_tactic.cpp)
+exfalso_tactic.cpp constructor_tactic.cpp)
 
 target_link_libraries(tactic ${LEAN_LIBS})

src/library/tactic/constructor_tactic.cpp

@@ -0,0 +1,125 @@
+/*
+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 "kernel/instantiate.h"
+#include "kernel/inductive/inductive.h"
+#include "library/constants.h"
+#include "library/util.h"
+#include "library/reducible.h"
+#include "library/tactic/expr_to_tactic.h"
+
+namespace lean {
+/**
+   \brief Implement multiple variations of the constructor tactic.
+   It tries to solve the goal by applying the i-th constructor.
+   If \c num_constructors is not none, then the tactic checks wether the inductive datatype has
+   the expected number of constructors.
+   If \c given_args is provided, then the tactic fixes the given arguments.
+   It creates a subgoal for each remaining argument.
+*/
+tactic constructor_tactic(elaborate_fn const & elab, unsigned i, optional<unsigned> num_constructors, list<expr> const & given_args) {
+    auto fn = [=](environment const & env, io_state const & ios, proof_state const & s) {
+        goals const & gs = s.get_goals();
+        if (empty(gs)) {
+            throw_no_goal_if_enabled(s);
+            return optional<proof_state>();
+        }
+        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;
+        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();
+        }
+        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();
+        }
+        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();
+        }
+        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();
+        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;
+        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();
+            }
+            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;
+                } else {
+                    return none_proof_state();
+                }
+            } catch (exception &) {
+                if (new_s.report_failure())
+                    throw;
+                return none_proof_state();
+            }
+        }
+        buffer<goal> new_goals;
+        while (is_pi(C_type)) {
+            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);
+}
+
+void initialize_constructor_tactic() {
+    register_tac(name{"tactic", "constructor"},
+                 [](type_checker & tc, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
+                     unsigned i = get_unsigned_arg(tc, e, 0);
+                     return constructor_tactic(fn, i, optional<unsigned>(), list<expr>());
+                 });
+    register_tac(name{"tactic", "split"},
+                 [](type_checker &, elaborate_fn const & fn, expr const &, pos_info_provider const *) {
+                     return constructor_tactic(fn, 0, optional<unsigned>(1), list<expr>());
+                 });
+    register_tac(name{"tactic", "left"},
+                 [](type_checker &, elaborate_fn const & fn, expr const &, pos_info_provider const *) {
+                     return constructor_tactic(fn, 0, optional<unsigned>(2), list<expr>());
+                 });
+    register_tac(name{"tactic", "right"},
+                 [](type_checker &, elaborate_fn const & fn, expr const &, pos_info_provider const *) {
+                     return constructor_tactic(fn, 1, optional<unsigned>(2), list<expr>());
+                 });
+    register_tac(name{"tactic", "existsi"},
+                 [](type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
+                     check_tactic_expr(app_arg(e), "invalid 'existsi' tactic, invalid argument");
+                     expr arg = get_tactic_expr_expr(app_arg(e));
+                     return constructor_tactic(fn, 0, optional<unsigned>(1), list<expr>(arg));
+                 });
+}
+
+void finalize_constructor_tactic() {
+}
+}

src/library/tactic/constructor_tactic.h

@@ -0,0 +1,11 @@
+/*
+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
+namespace lean {
+void initialize_constructor_tactic();
+void finalize_constructor_tactic();
+}

src/library/tactic/expr_to_tactic.cpp

@@ -228,6 +228,23 @@ static name_generator next_name_generator() {
     return name_generator(name(*g_tmp_prefix, r));
 }
 
+unsigned get_unsigned_arg(type_checker & tc, expr const & e, unsigned i) {
+    buffer<expr> args;
+    get_app_args(e, args);
+    if (i >= args.size())
+        throw expr_to_tactic_exception(e, "invalid tactic, insufficient number of arguments");
+    optional<mpz> k = to_num(args[i]);
+    if (!k)
+        k = to_num(tc.whnf(args[1]).first);
+    if (!k)
+        throw expr_to_tactic_exception(e, "invalid tactic, second argument must be a numeral");
+    if (!k->is_unsigned_int())
+        throw expr_to_tactic_exception(e,
+                                       "invalid tactic, second argument does not fit in "
+                                       "a machine unsigned integer");
+    return k->get_unsigned_int();
+}
+
 tactic expr_to_tactic(environment const & env, elaborate_fn const & fn, expr const & e, pos_info_provider const * p) {
     bool memoize             = false;
     type_checker tc(env, next_name_generator(), memoize);
@@ -277,16 +294,7 @@ void register_unary_num_tac(name const & n, std::function<tactic(tactic const &,
             if (args.size() != 2)
                 throw expr_to_tactic_exception(e, "invalid tactic, it must have two arguments");
             tactic t = expr_to_tactic(tc, fn, args[0], p);
-            optional<mpz> k = to_num(args[1]);
+            return f(t, get_unsigned_arg(tc, e, 1));
-            if (!k)
-                k = to_num(tc.whnf(args[1]).first);
-            if (!k)
-                throw expr_to_tactic_exception(e, "invalid tactic, second argument must be a numeral");
-            if (!k->is_unsigned_int())
-                throw expr_to_tactic_exception(e,
-                                               "invalid tactic, second argument does not fit in "
-                                               "a machine unsigned integer");
-            return f(t, k->get_unsigned_int());
         });
 }
 
@@ -296,16 +304,7 @@ void register_num_tac(name const & n, std::function<tactic(unsigned k)> f) {
             get_app_args(e, args);
             if (args.size() != 1)
                 throw expr_to_tactic_exception(e, "invalid tactic, it must have one argument");
-            optional<mpz> k = to_num(args[0]);
+            return f(get_unsigned_arg(tc, e, 0));
-            if (!k)
-                k = to_num(tc.whnf(args[0]).first);
-            if (!k)
-                throw expr_to_tactic_exception(e, "invalid tactic, argument must be a numeral");
-            if (!k->is_unsigned_int())
-                throw expr_to_tactic_exception(e,
-                                               "invalid tactic, argument does not fit in "
-                                               "a machine unsigned integer");
-            return f(k->get_unsigned_int());
         });
 }
 

src/library/tactic/expr_to_tactic.h

@@ -29,6 +29,8 @@ tactic expr_to_tactic(environment const & env, elaborate_fn const & fn, expr con
 
 name const & get_tactic_name();
 
+unsigned get_unsigned_arg(type_checker & tc, expr const & e, unsigned i);
+
 expr const & get_tactic_expr_type();
 expr const & get_tactic_identifier_type();
 expr mk_tactic_expr(expr const & e);

src/library/tactic/init_module.cpp

@@ -25,6 +25,7 @@ Author: Leonardo de Moura
 #include "library/tactic/let_tactic.h"
 #include "library/tactic/contradiction_tactic.h"
 #include "library/tactic/exfalso_tactic.h"
+#include "library/tactic/constructor_tactic.h"
 
 namespace lean {
 void initialize_tactic_module() {
@@ -49,9 +50,11 @@ void initialize_tactic_module() {
     initialize_let_tactic();
     initialize_contradiction_tactic();
     initialize_exfalso_tactic();
+    initialize_constructor_tactic();
 }
 
 void finalize_tactic_module() {
+    finalize_constructor_tactic();
     finalize_exfalso_tactic();
     finalize_contradiction_tactic();
     finalize_let_tactic();

tests/lean/constr_tac_errors.lean

@@ -0,0 +1,40 @@
+example : nat :=
+begin
+  split -- ERROR
+end
+
+example : nat :=
+by left
+
+example (a b : Prop) : a → b → a ∧ b :=
+begin
+  intro Ha Hb,
+  left -- ERROR
+end
+
+example (a b : Prop) : a → b → a ∧ b :=
+begin
+  intro Ha Hb,
+  right -- ERROR
+end
+
+example (a b : Prop) : a → b → a ∧ b :=
+begin
+  intro Ha Hb,
+  existsi Ha,  -- weird, but it is accepted
+  assumption
+end
+
+example (a b : Prop) : a → b → unit :=
+begin
+  intro Ha Hb,
+  existsi Ha, -- ERROR
+end
+
+example : unit :=
+by split -- weird, but it is accepted
+
+example : nat → nat :=
+begin
+  split -- ERROR
+end

tests/lean/constr_tac_errors.lean.expected.out

@@ -0,0 +1,59 @@
+constr_tac_errors.lean:3:2: error:invalid 'constructor' tactic, goal is an inductive datatype, but it does not have 1 constructor(s)
+proof state:
+
+⊢ nat
+constr_tac_errors.lean:4:0: error: don't know how to synthesize placeholder
+
+⊢ nat
+constr_tac_errors.lean:4:0: error: failed to add declaration '14.0' to environment, value has metavariables
+remark: set 'formatter.hide_full_terms' to false to see the complete term
+  ?M_1
+constr_tac_errors.lean:12:2: error:invalid 'constructor' tactic, goal is an inductive datatype, but it does not have 2 constructor(s)
+proof state:
+a b : Prop,
+Ha : a,
+Hb : b
+⊢ a ∧ b
+constr_tac_errors.lean:13:0: error: don't know how to synthesize placeholder
+a b : Prop
+⊢ a → b → a ∧ b
+constr_tac_errors.lean:13:0: error: failed to add declaration '14.2' to environment, value has metavariables
+remark: set 'formatter.hide_full_terms' to false to see the complete term
+  λ (a b : Prop),
+    ?M_1
+constr_tac_errors.lean:18:2: error:invalid 'constructor' tactic, goal is an inductive datatype, but it does not have 2 constructor(s)
+proof state:
+a b : Prop,
+Ha : a,
+Hb : b
+⊢ a ∧ b
+constr_tac_errors.lean:19:0: error: don't know how to synthesize placeholder
+a b : Prop
+⊢ a → b → a ∧ b
+constr_tac_errors.lean:19:0: error: failed to add declaration '14.3' to environment, value has metavariables
+remark: set 'formatter.hide_full_terms' to false to see the complete term
+  λ (a b : Prop),
+    ?M_1
+constr_tac_errors.lean:31:2: error:invalid 'constructor' tactic, too many arguments have been provided
+proof state:
+a b : Prop,
+Ha : a,
+Hb : b
+⊢ unit
+constr_tac_errors.lean:32:0: error: don't know how to synthesize placeholder
+a b : Prop
+⊢ a → b → unit
+constr_tac_errors.lean:32:0: error: failed to add declaration '14.5' to environment, value has metavariables
+remark: set 'formatter.hide_full_terms' to false to see the complete term
+  λ (a b : Prop),
+    ?M_1
+constr_tac_errors.lean:39:2: error:invalid 'constructor' tactic, goal is not an inductive datatype
+proof state:
+
+⊢ nat → nat
+constr_tac_errors.lean:40:0: error: don't know how to synthesize placeholder
+
+⊢ nat → nat
+constr_tac_errors.lean:40:0: error: failed to add declaration '14.7' to environment, value has metavariables
+remark: set 'formatter.hide_full_terms' to false to see the complete term
+  ?M_1

tests/lean/hott/constr_tac.hlean

@@ -0,0 +1,45 @@
+open prod
+
+example (a b c : Type) : a → b → c → a × b × c :=
+begin
+  intro Ha Hb Hc,
+  split,
+  assumption,
+  split,
+  assumption
+end
+
+example (a b : Type) : a → sum a b :=
+begin
+  intro Ha,
+  left,
+  assumption
+end
+
+example (a b : Type) : b → sum a b :=
+begin
+  intro Ha,
+  right,
+  assumption
+end
+
+open nat
+
+example (a : nat) : a > 0 → Σ x, x > 0 :=
+begin
+  intro Ha,
+  existsi a,
+  apply Ha
+end
+
+example : nat :=
+begin
+  constructor 0
+end
+
+example : nat :=
+begin
+  constructor 1,
+  constructor 1,
+  constructor 0
+end

tests/lean/run/constr_tac.lean

@@ -0,0 +1,68 @@
+import data.list
+
+example (a b c : Prop) : a → b → c → a ∧ b ∧ c :=
+begin
+  intro Ha Hb Hc,
+  split,
+  assumption,
+  split,
+  assumption
+end
+
+example (a b c : Type) : a → b → c → a × b × c :=
+begin
+  intro Ha Hb Hc,
+  split,
+  assumption,
+  split,
+  assumption
+end
+
+example (a b : Type) : a → sum a b :=
+begin
+  intro Ha,
+  left,
+  assumption
+end
+
+example (a b : Type) : b → sum a b :=
+begin
+  intro Ha,
+  right,
+  assumption
+end
+
+example (a b : Prop) : a → a ∨ b :=
+begin
+  intro Ha,
+  left,
+  assumption
+end
+
+example (a b : Prop) : b → a ∨ b :=
+begin
+  intro Ha,
+  right,
+  assumption
+end
+
+open nat
+
+example (a : nat) : a > 0 → ∃ x, x > 0 :=
+begin
+  intro Ha,
+  existsi a,
+  apply Ha
+end
+
+example : list nat :=
+begin
+  constructor 0
+end
+
+example : list nat :=
+begin
+  constructor 1,
+  constructor 0,
+  constructor 0
+end