From d152f38518abdbeaf951c20d0ee6c5820bfea2d5 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 30 Apr 2015 17:52:29 -0700 Subject: [PATCH] feat(library/tactic): add 'constructor', 'split', 'left', 'right' and 'existsi' tactics see issue #500 --- hott/init/tactic.hlean | 6 + library/init/tactic.lean | 8 +- src/emacs/lean-syntax.el | 2 +- src/library/tactic/CMakeLists.txt | 2 +- src/library/tactic/constructor_tactic.cpp | 125 ++++++++++++++++++ src/library/tactic/constructor_tactic.h | 11 ++ src/library/tactic/expr_to_tactic.cpp | 39 +++--- src/library/tactic/expr_to_tactic.h | 2 + src/library/tactic/init_module.cpp | 3 + tests/lean/constr_tac_errors.lean | 40 ++++++ .../lean/constr_tac_errors.lean.expected.out | 59 +++++++++ tests/lean/hott/constr_tac.hlean | 45 +++++++ tests/lean/run/constr_tac.lean | 68 ++++++++++ 13 files changed, 387 insertions(+), 23 deletions(-) create mode 100644 src/library/tactic/constructor_tactic.cpp create mode 100644 src/library/tactic/constructor_tactic.h create mode 100644 tests/lean/constr_tac_errors.lean create mode 100644 tests/lean/constr_tac_errors.lean.expected.out create mode 100644 tests/lean/hott/constr_tac.hlean create mode 100644 tests/lean/run/constr_tac.lean diff --git a/hott/init/tactic.hlean b/hott/init/tactic.hlean index e4a7247ca..d552f8420 100644 --- a/hott/init/tactic.hlean +++ b/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 diff --git a/library/init/tactic.lean b/library/init/tactic.lean index f1b939bb4..d04191452 100644 --- a/library/init/tactic.lean +++ b/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 diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el index c6434af9e..b60f61b10 100644 --- a/src/emacs/lean-syntax.el +++ b/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 diff --git a/src/library/tactic/CMakeLists.txt b/src/library/tactic/CMakeLists.txt index 0ae52c612..4d060c56d 100644 --- a/src/library/tactic/CMakeLists.txt +++ b/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}) diff --git a/src/library/tactic/constructor_tactic.cpp b/src/library/tactic/constructor_tactic.cpp new file mode 100644 index 000000000..28b673491 --- /dev/null +++ b/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 num_constructors, list 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(); + } + 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 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 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 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(), list()); + }); + register_tac(name{"tactic", "split"}, + [](type_checker &, elaborate_fn const & fn, expr const &, pos_info_provider const *) { + return constructor_tactic(fn, 0, optional(1), list()); + }); + register_tac(name{"tactic", "left"}, + [](type_checker &, elaborate_fn const & fn, expr const &, pos_info_provider const *) { + return constructor_tactic(fn, 0, optional(2), list()); + }); + register_tac(name{"tactic", "right"}, + [](type_checker &, elaborate_fn const & fn, expr const &, pos_info_provider const *) { + return constructor_tactic(fn, 1, optional(2), list()); + }); + 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(1), list(arg)); + }); +} + +void finalize_constructor_tactic() { +} +} diff --git a/src/library/tactic/constructor_tactic.h b/src/library/tactic/constructor_tactic.h new file mode 100644 index 000000000..a5437f542 --- /dev/null +++ b/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(); +} diff --git a/src/library/tactic/expr_to_tactic.cpp b/src/library/tactic/expr_to_tactic.cpp index 64c735b65..dd958897e 100644 --- a/src/library/tactic/expr_to_tactic.cpp +++ b/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 args; + get_app_args(e, args); + if (i >= args.size()) + throw expr_to_tactic_exception(e, "invalid tactic, insufficient number of arguments"); + optional 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 k = to_num(args[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()); + return f(t, get_unsigned_arg(tc, e, 1)); }); } @@ -296,16 +304,7 @@ void register_num_tac(name const & n, std::function f) { get_app_args(e, args); if (args.size() != 1) throw expr_to_tactic_exception(e, "invalid tactic, it must have one argument"); - optional k = to_num(args[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()); + return f(get_unsigned_arg(tc, e, 0)); }); } diff --git a/src/library/tactic/expr_to_tactic.h b/src/library/tactic/expr_to_tactic.h index 1b5c479af..cd64260d7 100644 --- a/src/library/tactic/expr_to_tactic.h +++ b/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); diff --git a/src/library/tactic/init_module.cpp b/src/library/tactic/init_module.cpp index 0ddb781bc..839d5ec9d 100644 --- a/src/library/tactic/init_module.cpp +++ b/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(); diff --git a/tests/lean/constr_tac_errors.lean b/tests/lean/constr_tac_errors.lean new file mode 100644 index 000000000..b7328959d --- /dev/null +++ b/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 diff --git a/tests/lean/constr_tac_errors.lean.expected.out b/tests/lean/constr_tac_errors.lean.expected.out new file mode 100644 index 000000000..fe57cf41c --- /dev/null +++ b/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 diff --git a/tests/lean/hott/constr_tac.hlean b/tests/lean/hott/constr_tac.hlean new file mode 100644 index 000000000..4112699a4 --- /dev/null +++ b/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 diff --git a/tests/lean/run/constr_tac.lean b/tests/lean/run/constr_tac.lean new file mode 100644 index 000000000..47b353841 --- /dev/null +++ b/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