From 63eb155c7e5792930ae8a88ee1304aeab39bb5e3 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 1 May 2015 12:45:21 -0700 Subject: [PATCH] feat(library/tactic): add 'injection' tactic see issue #500 --- hott/init/tactic.hlean | 2 + library/init/tactic.lean | 2 + src/emacs/lean-syntax.el | 3 +- src/library/tactic/CMakeLists.txt | 2 +- src/library/tactic/apply_tactic.cpp | 6 + src/library/tactic/apply_tactic.h | 1 + src/library/tactic/init_module.cpp | 3 + src/library/tactic/injection_tactic.cpp | 204 ++++++++++++++++++++++++ src/library/tactic/injection_tactic.h | 11 ++ src/library/util.cpp | 18 +++ src/library/util.h | 3 + tests/lean/hott/inj_tac.hlean | 24 +++ tests/lean/run/inj_tac.lean | 29 ++++ 13 files changed, 306 insertions(+), 2 deletions(-) create mode 100644 src/library/tactic/injection_tactic.cpp create mode 100644 src/library/tactic/injection_tactic.h create mode 100644 tests/lean/hott/inj_tac.hlean create mode 100644 tests/lean/run/inj_tac.lean diff --git a/hott/init/tactic.hlean b/hott/init/tactic.hlean index c1d90cee14..d0778a4a8d 100644 --- a/hott/init/tactic.hlean +++ b/hott/init/tactic.hlean @@ -106,6 +106,8 @@ opaque definition split : tactic := builtin opaque definition left : tactic := builtin opaque definition right : tactic := builtin +opaque definition injection (e : expr) (ids : opt_identifier_list) : 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 7c8ed0d725..7c127bcc10 100644 --- a/library/init/tactic.lean +++ b/library/init/tactic.lean @@ -106,6 +106,8 @@ opaque definition split : tactic := builtin opaque definition left : tactic := builtin opaque definition right : tactic := builtin +opaque definition injection (e : expr) (ids : opt_identifier_list) : 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 b60f61b106..24f4bcf355 100644 --- a/src/emacs/lean-syntax.el +++ b/src/emacs/lean-syntax.el @@ -135,7 +135,8 @@ "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" "split" "existsi" "constructor" "left" "right")) + "unfold" "change" "check_expr" "contradiction" "exfalso" "split" "existsi" "constructor" "left" "right" + "injection")) word-end) (1 'font-lock-constant-face)) ;; Types diff --git a/src/library/tactic/CMakeLists.txt b/src/library/tactic/CMakeLists.txt index 4d060c56d5..afa0e24a6e 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 constructor_tactic.cpp) +exfalso_tactic.cpp constructor_tactic.cpp injection_tactic.cpp) target_link_libraries(tactic ${LEAN_LIBS}) diff --git a/src/library/tactic/apply_tactic.cpp b/src/library/tactic/apply_tactic.cpp index 27cf3c825c..feb509b3ef 100644 --- a/src/library/tactic/apply_tactic.cpp +++ b/src/library/tactic/apply_tactic.cpp @@ -182,6 +182,12 @@ proof_state_seq apply_tactic_core(environment const & env, io_state const & ios, return apply_tactic_core(env, ios, s, e, tmp_cs, true, AddSubgoals); } +tactic apply_tactic_core(expr const & e, constraint_seq const & cs) { + return tactic([=](environment const & env, io_state const & ios, proof_state const & s) { + return apply_tactic_core(env, ios, s, e, cs); + }); +} + tactic eassumption_tactic() { return tactic([=](environment const & env, io_state const & ios, proof_state const & s) { goals const & gs = s.get_goals(); diff --git a/src/library/tactic/apply_tactic.h b/src/library/tactic/apply_tactic.h index 41815b7b14..8211a97a03 100644 --- a/src/library/tactic/apply_tactic.h +++ b/src/library/tactic/apply_tactic.h @@ -9,6 +9,7 @@ Author: Leonardo de Moura #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_core(expr const & e, constraint_seq const & cs = constraint_seq()); tactic apply_tactic(elaborate_fn const & fn, expr const & e); tactic fapply_tactic(elaborate_fn const & fn, expr const & e); tactic eassumption_tactic(); diff --git a/src/library/tactic/init_module.cpp b/src/library/tactic/init_module.cpp index 839d5ec9d6..a2f2788a16 100644 --- a/src/library/tactic/init_module.cpp +++ b/src/library/tactic/init_module.cpp @@ -26,6 +26,7 @@ Author: Leonardo de Moura #include "library/tactic/contradiction_tactic.h" #include "library/tactic/exfalso_tactic.h" #include "library/tactic/constructor_tactic.h" +#include "library/tactic/injection_tactic.h" namespace lean { void initialize_tactic_module() { @@ -51,9 +52,11 @@ void initialize_tactic_module() { initialize_contradiction_tactic(); initialize_exfalso_tactic(); initialize_constructor_tactic(); + initialize_injection_tactic(); } void finalize_tactic_module() { + finalize_injection_tactic(); finalize_constructor_tactic(); finalize_exfalso_tactic(); finalize_contradiction_tactic(); diff --git a/src/library/tactic/injection_tactic.cpp b/src/library/tactic/injection_tactic.cpp new file mode 100644 index 0000000000..468f1d0cc3 --- /dev/null +++ b/src/library/tactic/injection_tactic.cpp @@ -0,0 +1,204 @@ +/* +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/abstract.h" +#include "kernel/inductive/inductive.h" +#include "library/constants.h" +#include "library/util.h" +#include "library/reducible.h" +#include "library/tactic/elaborate.h" +#include "library/tactic/expr_to_tactic.h" +#include "library/tactic/apply_tactic.h" + +namespace lean { +/** \brief Introduce num hypotheses, if _ns is not nil use it to name the hypothesis, + + New hypothesis of the form (a = a) and (a == a) are discarded. + New hypothesis of the form (a == b) where (a b : A), are converted into (a = b). +*/ +tactic intros_num_tactic(list _ns, unsigned num) { + auto fn = [=](environment const & env, io_state const &, proof_state const & s) { + if (num == 0) + return some_proof_state(s); + list ns = _ns; + goals const & gs = s.get_goals(); + if (empty(gs)) { + throw_no_goal_if_enabled(s); + return optional(); + } + goal const & g = head(gs); + name_generator ngen = s.get_ngen(); + auto tc = mk_type_checker(env, ngen.mk_child(), s.relax_main_opaque()); + expr t = g.get_type(); + expr m = g.get_meta(); + buffer hyps; + g.get_hyps(hyps); + buffer new_hyps; // extra hypotheses for the new goal + buffer args; // arguments to be provided to new goal + buffer intros; // locals being introduced + + auto mk_name = [&](name const & n) { + if (is_nil(ns)) { + return get_unused_name(n, new_hyps); + } else { + name r = head(ns); + ns = tail(ns); + return r; + } + }; + + // introduce a value of type t + auto add_intro = [&](expr const & t) { + expr i = mk_local(ngen.next(), t); + intros.push_back(i); + return i; + }; + + auto add_hyp = [&](name const & n, expr const & t) { + expr l = mk_local(mk_name(n), t); + new_hyps.push_back(l); + intros.push_back(l); + args.push_back(l); + return l; + }; + + try { + for (unsigned i = 0; i < num; i++) { + t = tc->ensure_pi(t).first; + name const & Hname = binding_name(t); + constraint_seq Hcs; + expr Htype = tc->whnf(binding_domain(t), Hcs); + optional new_Htype; + expr A, B, lhs, rhs; + if (!closed(binding_body(t))) { + // rest depends on Hname : Htype + expr H = add_hyp(Hname, Htype); + t = instantiate(binding_body(t), H); + } else { + if (is_eq(Htype, lhs, rhs)) { + if (!tc->is_def_eq(lhs, rhs, justification(), Hcs) || Hcs) + add_hyp(Hname, Htype); + else + add_intro(Htype); // discard + } else if (is_standard(env) && is_heq(Htype, A, lhs, B, rhs)) { + if (tc->is_def_eq(A, B, justification(), Hcs) && !Hcs) { + if (!tc->is_def_eq(lhs, rhs, justification(), Hcs) || Hcs) { + // convert to homogenous equality + expr H = mk_local(ngen.next(), Htype); + expr newHtype = mk_eq(*tc, lhs, rhs); + expr newH = mk_local(mk_name(Hname), newHtype); + new_hyps.push_back(newH); + intros.push_back(H); + levels heq_lvl = const_levels(get_app_fn(Htype)); + args.push_back(mk_app(mk_constant(get_heq_to_eq_name(), heq_lvl), A, lhs, rhs, H)); + } else { + add_intro(Htype); // discard + } + } else { + add_hyp(Hname, Htype); + } + } else { + add_hyp(Hname, Htype); + } + t = binding_body(t); + } + } + substitution new_subst = s.get_subst(); + expr new_mvar = mk_metavar(ngen.next(), Pi(hyps, Pi(new_hyps, t))); + expr new_aux = mk_app(new_mvar, hyps); + expr new_meta = mk_app(new_aux, new_hyps); + goal new_goal(new_meta, t); + assign(new_subst, g, Fun(intros, mk_app(new_aux, args))); + return some_proof_state(proof_state(s, cons(new_goal, tail(gs)), new_subst, ngen)); + } catch (exception &) { + return none_proof_state(); + } + }; + return tactic01(fn); +} + +tactic injection_tactic(elaborate_fn const & elab, expr const & e, list const & ids) { + auto fn = [=](environment const & env, io_state const & ios, proof_state const & s) { + proof_state new_s = s; + goals const & gs = new_s.get_goals(); + if (!gs) { + throw_no_goal_if_enabled(s); + return proof_state_seq(); + } + expr t = head(gs).get_type(); + bool report_unassigned = true; + bool enforce_type = false; + if (optional new_e = elaborate_with_respect_to(env, ios, elab, new_s, e, none_expr(), + report_unassigned, enforce_type)) { + constraint_seq cs; + name_generator ngen = new_s.get_ngen(); + auto tc = mk_type_checker(env, ngen.mk_child(), new_s.relax_main_opaque()); + expr new_e_type = tc->whnf(tc->infer(*new_e, cs), cs); + expr lhs, rhs; + if (!is_eq(new_e_type, lhs, rhs)) { + throw_tactic_exception_if_enabled(new_s, "invalid 'injection' tactic, " + "given argument is not an equality proof"); + return proof_state_seq(); + } + lhs = tc->whnf(lhs, cs); + rhs = tc->whnf(rhs, cs); + expr A = tc->whnf(tc->infer(lhs, cs), cs); + buffer I_args; + expr I = get_app_args(A, I_args); + if (!is_constant(I) || !inductive::is_inductive_decl(env, const_name(I))) { + throw_tactic_exception_if_enabled(new_s, "invalid 'injection' tactic, " + "it is not an equality between inductive values"); + return proof_state_seq(); + } + expr lhs_fn = get_app_fn(lhs); + expr rhs_fn = get_app_fn(rhs); + if (!is_constant(lhs_fn) || !is_constant(rhs_fn) || const_name(lhs_fn) != const_name(rhs_fn) || + !inductive::is_intro_rule(env, const_name(lhs_fn))) { + throw_tactic_exception_if_enabled(new_s, "invalid 'injection' tactic, " + "the given equality is not of the form (f ...) = (f ...) " + "where f is a constructor"); + return proof_state_seq(); + } + unsigned num_params = *inductive::get_num_params(env, const_name(I)); + unsigned cnstr_arity = get_arity(env.get(const_name(lhs_fn)).get_type()); + lean_assert(cnstr_arity >= num_params); + unsigned num_new_eqs = cnstr_arity - num_params; + level t_lvl = sort_level(tc->ensure_type(t, cs)); + expr N = mk_constant(name(const_name(I), "no_confusion"), cons(t_lvl, const_levels(I))); + N = mk_app(mk_app(N, I_args), t, lhs, rhs, *new_e); + if (is_standard(env)) { + tactic tac = then(apply_tactic_core(N, cs), + intros_num_tactic(ids, num_new_eqs)); + return tac(env, ios, new_s); + } else { + level n_lvl = mk_meta_univ(tc->mk_fresh_name()); + expr lift_down = mk_app(mk_constant(get_lift_down_name(), {t_lvl, n_lvl}), t); + tactic tac = then(apply_tactic_core(lift_down), + then(apply_tactic_core(N, cs), + intros_num_tactic(ids, num_new_eqs))); + return tac(env, ios, new_s); + } + } else { + return proof_state_seq(); + } + }; + return tactic(fn); +} + +void initialize_injection_tactic() { + register_tac(name{"tactic", "injection"}, + [](type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) { + check_tactic_expr(app_arg(app_fn(e)), "invalid 'injection' tactic, invalid argument"); + buffer ids; + get_tactic_id_list_elements(app_arg(e), ids, "invalid 'injection' tactic, list of identifiers expected"); + return injection_tactic(fn, get_tactic_expr_expr(app_arg(app_fn(e))), to_list(ids)); + }); +} + +void finalize_injection_tactic() { +} +} diff --git a/src/library/tactic/injection_tactic.h b/src/library/tactic/injection_tactic.h new file mode 100644 index 0000000000..9b9d72fdb4 --- /dev/null +++ b/src/library/tactic/injection_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_injection_tactic(); +void finalize_injection_tactic(); +} diff --git a/src/library/util.cpp b/src/library/util.cpp index b69f3c6fe7..679c4bbaa7 100644 --- a/src/library/util.cpp +++ b/src/library/util.cpp @@ -467,6 +467,24 @@ bool is_eq_a_a(type_checker & tc, expr const & e) { return d.first && !d.second; } +bool is_heq(expr const & e) { + expr const & fn = get_app_fn(e); + return is_constant(fn) && const_name(fn) == get_heq_name(); +} + +bool is_heq(expr const & e, expr & A, expr & lhs, expr & B, expr & rhs) { + if (is_heq(e)) { + buffer args; + get_app_args(e, args); + if (args.size() != 4) + return false; + A = args[0]; lhs = args[1]; B = args[2]; rhs = args[3]; + return true; + } else { + return false; + } +} + void mk_telescopic_eq(type_checker & tc, buffer const & t, buffer const & s, buffer & eqs) { lean_assert(t.size() == s.size()); lean_assert(std::all_of(s.begin(), s.end(), is_local)); diff --git a/src/library/util.h b/src/library/util.h index eb333fa808..b8f42117cc 100644 --- a/src/library/util.h +++ b/src/library/util.h @@ -149,6 +149,9 @@ bool is_eq_a_a(expr const & e); /** \brief Return true iff \c e is of the form (eq A a a') where \c a and \c a' are definitionally equal */ bool is_eq_a_a(type_checker & tc, expr const & e); +bool is_heq(expr const & e); +bool is_heq(expr const & e, expr & A, expr & lhs, expr & B, expr & rhs); + bool is_iff(expr const & e); expr mk_iff(expr const & lhs, expr const & rhs); expr mk_iff_refl(expr const & a); diff --git a/tests/lean/hott/inj_tac.hlean b/tests/lean/hott/inj_tac.hlean new file mode 100644 index 0000000000..a556713c0e --- /dev/null +++ b/tests/lean/hott/inj_tac.hlean @@ -0,0 +1,24 @@ +import data.vector +open nat vector + +example (a b : nat) : succ a = succ b → a + 2 = b + 2 := +begin + intro H, + injection H, + rewrite e_1 +end + +example (A : Type) (n : nat) (v w : vector A n) (a : A) (b : A) : + a :: v = b :: w → b = a := +begin + intro H, injection H with aeqb beqw, + rewrite aeqb +end + +open prod + +example (A : Type) (a₁ a₂ a₃ b₁ b₂ b₃ : A) : (a₁, a₂, a₃) = (b₁, b₂, b₃) → b₁ = a₁ := +begin + intro H, injection H with H₁, injection H₁ with a₁b₁, + rewrite a₁b₁ +end diff --git a/tests/lean/run/inj_tac.lean b/tests/lean/run/inj_tac.lean new file mode 100644 index 0000000000..40f7790c93 --- /dev/null +++ b/tests/lean/run/inj_tac.lean @@ -0,0 +1,29 @@ +import data.vector +open nat vector + +example (a b : nat) : succ a = succ b → a + 2 = b + 2 := +begin + intro H, + injection H with aeqb, + rewrite aeqb +end + +example (A : Type) (n : nat) (v w : vector A n) (a : A) (b : A) : + a :: v = a :: w → b :: v = b :: w := +begin + intro H, injection H with veqw, + rewrite veqw +end + +example (A : Type) (n : nat) (v w : vector A n) (a : A) (b : A) : + a :: v = b :: w → b :: v = a :: w := +begin + intro H, injection H with aeqb veqw, + rewrite [aeqb, veqw] +end + +example (A : Type) (a₁ a₂ a₃ b₁ b₂ b₃ : A) : (a₁, a₂, a₃) = (b₁, b₂, b₃) → b₁ = a₁ := +begin + intro H, injection H with H₁, injection H₁ with a₁b₁, + rewrite a₁b₁ +end