From 79d03477217f2a5c3c745290a0d2db2ee02985a7 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 23 Oct 2014 22:40:15 -0700 Subject: [PATCH] feat(library/tactic): add generalize tactic, closes #34 Remark: the intros tactic has been added in a different commit: 7d0100a3400b70c19422c --- library/tools/tactic.lean | 1 + src/emacs/lean-syntax.el | 2 +- src/library/tactic/CMakeLists.txt | 4 +- src/library/tactic/generalize_tactic.cpp | 56 ++++++++++++++++++++++++ src/library/tactic/generalize_tactic.h | 14 ++++++ src/library/tactic/init_module.cpp | 3 ++ tests/lean/run/get_tac1.lean | 11 +++++ 7 files changed, 88 insertions(+), 3 deletions(-) create mode 100644 src/library/tactic/generalize_tactic.cpp create mode 100644 src/library/tactic/generalize_tactic.h create mode 100644 tests/lean/run/get_tac1.lean diff --git a/library/tools/tactic.lean b/library/tools/tactic.lean index 38468d85dd..032e9beb76 100644 --- a/library/tools/tactic.lean +++ b/library/tools/tactic.lean @@ -48,6 +48,7 @@ opaque definition apply (e : expr) : tactic := builtin opaque definition rapply (e : expr) : tactic := builtin opaque definition rename (a b : expr) : tactic := builtin opaque definition intro (e : expr) : tactic := builtin +opaque definition generalize (e : expr) : tactic := builtin inductive expr_list : Type := nil : expr_list, diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el index 6f0698ddb0..f69a431923 100644 --- a/src/emacs/lean-syntax.el +++ b/src/emacs/lean-syntax.el @@ -119,7 +119,7 @@ ;; tactics (,(rx (not (any "\.")) word-start (or "\\b.*_tac" "Cond" "or_else" "then" "try" "when" "assumption" "rapply" "apply" "rename" "intro" "intros" - "back" "beta" "done" "exact" "repeat") + "generalize" "back" "beta" "done" "exact" "repeat") word-end) . 'font-lock-constant-face) ;; Types diff --git a/src/library/tactic/CMakeLists.txt b/src/library/tactic/CMakeLists.txt index e065f39d3f..fc26b122c5 100644 --- a/src/library/tactic/CMakeLists.txt +++ b/src/library/tactic/CMakeLists.txt @@ -1,6 +1,6 @@ add_library(tactic goal.cpp proof_state.cpp tactic.cpp elaborate.cpp apply_tactic.cpp intros_tactic.cpp rename_tactic.cpp trace_tactic.cpp -exact_tactic.cpp unfold_tactic.cpp expr_to_tactic.cpp util.cpp -init_module.cpp) +exact_tactic.cpp unfold_tactic.cpp generalize_tactic.cpp +expr_to_tactic.cpp util.cpp init_module.cpp) target_link_libraries(tactic ${LEAN_LIBS}) diff --git a/src/library/tactic/generalize_tactic.cpp b/src/library/tactic/generalize_tactic.cpp new file mode 100644 index 0000000000..6b11820530 --- /dev/null +++ b/src/library/tactic/generalize_tactic.cpp @@ -0,0 +1,56 @@ +/* +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "kernel/abstract.h" +#include "library/reducible.h" +#include "library/tactic/elaborate.h" +#include "library/tactic/expr_to_tactic.h" + +namespace lean { +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; + 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) + 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); + expr new_v = g.abstract(mk_app(new_m, *new_e)); + subst.assign(g.get_name(), new_v); + goal new_g(new_m, new_t); + return some(proof_state(new_s, goals(new_g, tail(gs)), subst, ngen)); + } + return none_proof_state(); + }); +} + +void initialize_generalize_tactic() { + register_tac(name({"tactic", "generalize"}), + [](type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) { + check_tactic_expr(app_arg(e), "invalid 'generalize' tactic, invalid argument"); + // TODO(Leo): allow user to provide name to abstract variable + return generalize_tactic(fn, get_tactic_expr_expr(app_arg(e)), "x"); + }); +} + +void finalize_generalize_tactic() { +} +} diff --git a/src/library/tactic/generalize_tactic.h b/src/library/tactic/generalize_tactic.h new file mode 100644 index 0000000000..ad74f1b228 --- /dev/null +++ b/src/library/tactic/generalize_tactic.h @@ -0,0 +1,14 @@ +/* +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "library/tactic/elaborate.h" + +namespace lean { +tactic generalize_tactic(elaborate_fn const & elab, expr const & e); +void initialize_generalize_tactic(); +void finalize_generalize_tactic(); +} diff --git a/src/library/tactic/init_module.cpp b/src/library/tactic/init_module.cpp index 1bc57c5b2d..79f819fcad 100644 --- a/src/library/tactic/init_module.cpp +++ b/src/library/tactic/init_module.cpp @@ -12,6 +12,7 @@ Author: Leonardo de Moura #include "library/tactic/trace_tactic.h" #include "library/tactic/exact_tactic.h" #include "library/tactic/unfold_tactic.h" +#include "library/tactic/generalize_tactic.h" namespace lean { void initialize_tactic_module() { @@ -23,9 +24,11 @@ void initialize_tactic_module() { initialize_trace_tactic(); initialize_exact_tactic(); initialize_unfold_tactic(); + initialize_generalize_tactic(); } void finalize_tactic_module() { + finalize_generalize_tactic(); finalize_unfold_tactic(); finalize_exact_tactic(); finalize_trace_tactic(); diff --git a/tests/lean/run/get_tac1.lean b/tests/lean/run/get_tac1.lean new file mode 100644 index 0000000000..25f7e05730 --- /dev/null +++ b/tests/lean/run/get_tac1.lean @@ -0,0 +1,11 @@ +import hott.path tools.tactic +open path + +definition concat_pV_p {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) : (p ⬝ q⁻¹) ⬝ q ≈ p := +begin + generalize p, + apply (path.induction_on q), + intro p, + apply (path.induction_on p), + apply idp +end