feat(library/tactic): add 'induction' tactic skeleton

hott/init/tactic.hlean

@@ -62,7 +62,7 @@ inductive expr_list : Type :=
 -- auxiliary type used to mark optional list of arguments
 definition opt_expr_list := expr_list
 
--- auxiliary types used to mark that the expression (list) is an identifier (list)
+-- auxiliary types used to mark that the expression is suppose to be an identifier, optional, or a list.
 definition identifier := expr
 definition identifier_list := expr_list
 definition opt_identifier_list := expr_list
@@ -88,6 +88,9 @@ definition rewrite_tac (e : expr_list) : tactic := builtin
 
 definition cases (id : identifier) (ids : opt_identifier_list) : tactic := builtin
 
+definition induction (h : identifier) (ids : opt_identifier_list) : tactic := builtin
+definition induction_using (h : identifier) (rec : expr) (ids : opt_identifier_list) : tactic := builtin
+
 definition intros (ids : opt_identifier_list) : tactic := builtin
 
 definition generalizes (es : expr_list) : tactic := builtin

library/init/tactic.lean

@@ -62,7 +62,7 @@ inductive expr_list : Type :=
 -- auxiliary type used to mark optional list of arguments
 definition opt_expr_list := expr_list
 
--- auxiliary types used to mark that the expression (list) is an identifier (list)
+-- auxiliary types used to mark that the expression is suppose to be an identifier, optional, or a list.
 definition identifier := expr
 definition identifier_list := expr_list
 definition opt_identifier_list := expr_list
@@ -88,6 +88,9 @@ definition rewrite_tac (e : expr_list) : tactic := builtin
 
 definition cases (id : identifier) (ids : opt_identifier_list) : tactic := builtin
 
+definition induction (h : identifier) (ids : opt_identifier_list) : tactic := builtin
+definition induction_using (h : identifier) (rec : expr) (ids : opt_identifier_list) : tactic := builtin
+
 definition intros (ids : opt_identifier_list) : tactic := builtin
 
 definition generalizes (es : expr_list) : tactic := builtin

src/emacs/lean-syntax.el

@@ -138,7 +138,7 @@
                 "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" "split" "existsi" "constructor" "left" "right"
-                "injection" "congruence" "reflexivity" "symmetry" "transitivity" "state"))
+                "injection" "congruence" "reflexivity" "symmetry" "transitivity" "state" "induction" "induction_using"))
            word-end)
       (1 'font-lock-constant-face))
      ;; Types

src/library/constants.cpp

@@ -96,6 +96,7 @@ name const * g_tactic_expr_list_cons = nullptr;
 name const * g_tactic_expr_list_nil = nullptr;
 name const * g_tactic_identifier = nullptr;
 name const * g_tactic_identifier_list = nullptr;
+name const * g_tactic_opt_expr = nullptr;
 name const * g_tactic_opt_identifier_list = nullptr;
 name const * g_tactic_fail = nullptr;
 name const * g_tactic_fixpoint = nullptr;
@@ -224,6 +225,7 @@ void initialize_constants() {
     g_tactic_expr_list_nil = new name{"tactic", "expr_list", "nil"};
     g_tactic_identifier = new name{"tactic", "identifier"};
     g_tactic_identifier_list = new name{"tactic", "identifier_list"};
+    g_tactic_opt_expr = new name{"tactic", "opt_expr"};
     g_tactic_opt_identifier_list = new name{"tactic", "opt_identifier_list"};
     g_tactic_fail = new name{"tactic", "fail"};
     g_tactic_fixpoint = new name{"tactic", "fixpoint"};
@@ -353,6 +355,7 @@ void finalize_constants() {
     delete g_tactic_expr_list_nil;
     delete g_tactic_identifier;
     delete g_tactic_identifier_list;
+    delete g_tactic_opt_expr;
     delete g_tactic_opt_identifier_list;
     delete g_tactic_fail;
     delete g_tactic_fixpoint;
@@ -481,6 +484,7 @@ name const & get_tactic_expr_list_cons_name() { return *g_tactic_expr_list_cons;
 name const & get_tactic_expr_list_nil_name() { return *g_tactic_expr_list_nil; }
 name const & get_tactic_identifier_name() { return *g_tactic_identifier; }
 name const & get_tactic_identifier_list_name() { return *g_tactic_identifier_list; }
+name const & get_tactic_opt_expr_name() { return *g_tactic_opt_expr; }
 name const & get_tactic_opt_identifier_list_name() { return *g_tactic_opt_identifier_list; }
 name const & get_tactic_fail_name() { return *g_tactic_fail; }
 name const & get_tactic_fixpoint_name() { return *g_tactic_fixpoint; }

src/library/constants.h

@@ -98,6 +98,7 @@ name const & get_tactic_expr_list_cons_name();
 name const & get_tactic_expr_list_nil_name();
 name const & get_tactic_identifier_name();
 name const & get_tactic_identifier_list_name();
+name const & get_tactic_opt_expr_name();
 name const & get_tactic_opt_identifier_list_name();
 name const & get_tactic_fail_name();
 name const & get_tactic_fixpoint_name();

src/library/constants.txt

@@ -91,6 +91,7 @@ tactic.expr_list.cons
 tactic.expr_list.nil
 tactic.identifier
 tactic.identifier_list
+tactic.opt_expr
 tactic.opt_identifier_list
 tactic.fail
 tactic.fixpoint

src/library/tactic/CMakeLists.txt

@@ -6,6 +6,6 @@ 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 constructor_tactic.cpp injection_tactic.cpp
-congruence_tactic.cpp equivalence_tactics.cpp)
+congruence_tactic.cpp equivalence_tactics.cpp induction_tactic.cpp)
 
 target_link_libraries(tactic ${LEAN_LIBS})

src/library/tactic/induction_tactic.cpp

@@ -0,0 +1,41 @@
+/*
+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 "library/tactic/tactic.h"
+#include "library/tactic/expr_to_tactic.h"
+
+namespace lean {
+tactic induction_tactic(name const & H, optional<name> const & rec, list<name> const & ids) {
+    // TODO(Leo)
+    name rec1 = "unknown";
+    if (rec) rec1 = *rec;
+    std::cout << "induction: " << H << " " << rec1 << " " << ids << "\n";
+    return id_tactic();
+}
+
+void initialize_induction_tactic() {
+    register_tac(name{"tactic", "induction"},
+                 [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) {
+                     name H = tactic_expr_to_id(app_arg(app_fn(e)), "invalid 'induction' tactic, argument must be an identifier");
+                     buffer<name> ids;
+                     get_tactic_id_list_elements(app_arg(e), ids, "invalid 'induction' tactic, list of identifiers expected");
+                     return induction_tactic(H, optional<name>(), to_list(ids.begin(), ids.end()));
+                 });
+    register_tac(name{"tactic", "induction_using"},
+                 [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) {
+                     name H = tactic_expr_to_id(app_arg(app_fn(app_fn(e))), "invalid 'induction' tactic, argument must be an identifier");
+                     check_tactic_expr(app_arg(app_fn(e)), "invalid 'induction' tactic, invalid argument");
+                     expr rec = get_tactic_expr_expr(app_arg(app_fn(e)));
+                     if (!is_constant(rec))
+                         throw expr_to_tactic_exception(app_arg(app_fn(e)), "invalid 'induction' tactic, constant expected");
+                     buffer<name> ids;
+                     get_tactic_id_list_elements(app_arg(e), ids, "invalid 'induction' tactic, list of identifiers expected");
+                     return induction_tactic(H, optional<name>(const_name(rec)), to_list(ids.begin(), ids.end()));
+                 });
+}
+void finalize_induction_tactic() {
+}
+}

src/library/tactic/induction_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_induction_tactic();
+void finalize_induction_tactic();
+}

src/library/tactic/init_module.cpp

@@ -29,6 +29,7 @@ Author: Leonardo de Moura
 #include "library/tactic/injection_tactic.h"
 #include "library/tactic/congruence_tactic.h"
 #include "library/tactic/equivalence_tactics.h"
+#include "library/tactic/induction_tactic.h"
 
 namespace lean {
 void initialize_tactic_module() {
@@ -57,9 +58,11 @@ void initialize_tactic_module() {
     initialize_injection_tactic();
     initialize_congruence_tactic();
     initialize_equivalence_tactics();
+    initialize_induction_tactic();
 }
 
 void finalize_tactic_module() {
+    finalize_induction_tactic();
     finalize_equivalence_tactics();
     finalize_congruence_tactic();
     finalize_injection_tactic();