From 120c48b1b2bf96708ef14d7e570bf4df22af5c09 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 22 Jun 2016 19:17:08 -0700 Subject: [PATCH] feat(library/tactic): expose congr_lemmas This commit also adds several helper code, and fixes bugs in congr_lemma.cpp --- library/init/meta/congr_lemma.lean | 51 +++++++++ library/init/meta/default.lean | 1 + src/library/congr_lemma.cpp | 8 +- src/library/congr_lemma.h | 2 +- src/library/tactic/CMakeLists.txt | 3 +- src/library/tactic/congr_lemma_tactics.cpp | 127 +++++++++++++++++++++ src/library/tactic/congr_lemma_tactics.h | 11 ++ src/library/tactic/fun_info_tactics.cpp | 48 ++++---- src/library/tactic/init_module.cpp | 3 + src/library/tactic/tactic_state.cpp | 3 +- src/library/tactic/tactic_state.h | 13 +++ tests/lean/run/congr_lemma1.lean | 12 ++ 12 files changed, 254 insertions(+), 28 deletions(-) create mode 100644 library/init/meta/congr_lemma.lean create mode 100644 src/library/tactic/congr_lemma_tactics.cpp create mode 100644 src/library/tactic/congr_lemma_tactics.h create mode 100644 tests/lean/run/congr_lemma1.lean diff --git a/library/init/meta/congr_lemma.lean b/library/init/meta/congr_lemma.lean new file mode 100644 index 0000000000..e90bcbd26c --- /dev/null +++ b/library/init/meta/congr_lemma.lean @@ -0,0 +1,51 @@ +/- +Copyright (c) 2016 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura +-/ +prelude +import init.meta.tactic init.meta.format init.function + +inductive congr_arg_kind := +/- It is a parameter for the congruence lemma, the parameter occurs in the left and right hand sides. -/ +| fixed +/- It is not a parameter for the congruence lemma, the lemma was specialized for this parameter. + This only happens if the parameter is a subsingleton/proposition, and other parameters depend on it. -/ +| fixed_no_param +/- The lemma contains three parameters for this kind of argument a_i, b_i and (eq_i : a_i = b_i). + a_i and b_i represent the left and right hand sides, and eq_i is a proof for their equality. -/ +| eq +/- congr-simp lemma contains only one parameter for this kind of argument, and congr-lemmas contains two. + They correspond to arguments that are subsingletons/propositions. -/ +| cast +/- The lemma contains three parameters for this kind of argument a_i, b_i and (eq_i : a_i == b_i). + a_i and b_i represent the left and right hand sides, and eq_i is a proof for their heterogeneous equality. -/ +| heq + +structure congr_lemma := +(type : expr) (proof : expr) (arg_kids : list congr_arg_kind) + +namespace tactic +meta_constant mk_congr_simp : expr → tactic congr_lemma +meta_constant mk_congr_simp_n : expr → nat → tactic congr_lemma +/- Create a specialized theorem using (a prefix of) the arguments of the given application. -/ +meta_constant mk_specialized_congr_simp : expr → tactic congr_lemma + +meta_constant mk_congr : expr → tactic congr_lemma +meta_constant mk_congr_n : expr → nat → tactic congr_lemma +/- Create a specialized theorem using (a prefix of) the arguments of the given application. -/ +meta_constant mk_specialized_congr : expr → tactic congr_lemma + +meta_constant mk_hcongr : expr → tactic congr_lemma +meta_constant mk_hcongr_n : expr → nat → tactic congr_lemma + +/- If R is an equivalence relation, construct the congruence lemma + R a1 a2 -> R b1 b2 -> (R a1 b1) <-> (R a2 b2) -/ +meta_constant mk_rel_iff_congr : expr → tactic congr_lemma + +/- Similar to mk_rel_iff_congr + It fails if propext is not available. + + R a1 a2 -> R b1 b2 -> (R a1 b1) = (R a2 b2) -/ +meta_constant mk_rel_eq_congr : expr → tactic congr_lemma +end tactic diff --git a/library/init/meta/default.lean b/library/init/meta/default.lean index 08b90f220d..ea619adcef 100644 --- a/library/init/meta/default.lean +++ b/library/init/meta/default.lean @@ -8,3 +8,4 @@ import init.meta.name init.meta.options init.meta.format init.meta.rb_map import init.meta.level init.meta.expr init.meta.base_tactic init.meta.environment import init.meta.tactic init.meta.contradiction_tactic init.meta.constructor_tactic import init.meta.injection_tactic init.meta.relation_tactics init.meta.fun_info +import init.meta.congr_lemma diff --git a/src/library/congr_lemma.cpp b/src/library/congr_lemma.cpp index 7f53c901e5..52afaa66b3 100644 --- a/src/library/congr_lemma.cpp +++ b/src/library/congr_lemma.cpp @@ -72,7 +72,7 @@ struct congr_lemma_manager { return cast(e, type, tail(deps), eqs); } else { expr lhs, rhs; - lean_verify(is_eq(mlocal_type(*major), lhs, rhs)); + lean_verify(is_eq(m_ctx.infer(*major), lhs, rhs)); lean_assert(is_local(lhs)); lean_assert(is_local(rhs)); // We compute the new type by replacing rhs with lhs, and major with (refl lhs). @@ -147,7 +147,7 @@ struct congr_lemma_manager { } else { expr major = *eqs[i]; expr x_1, x_2; - lean_verify(is_eq(mlocal_type(major), x_1, x_2)); + lean_verify(is_eq(m_ctx.infer(major), x_1, x_2)); lean_assert(is_local(x_1)); lean_assert(is_local(x_2)); expr motive_eq = mk_eq(m_ctx, lhs, rhs); @@ -491,9 +491,9 @@ struct congr_lemma_manager { lean_assert(closed(type) && closed(motive)); expr minor = mk_hcongr_proof(type); expr major = eq_pr; - if (is_heq(mlocal_type(eq_pr))) + if (is_heq(m_ctx.infer(eq_pr))) major = mk_eq_of_heq(m_ctx, eq_pr); - motive = Fun(b, motive); + motive = m_ctx.mk_lambda({b}, motive); return m_ctx.mk_lambda({a, b, eq_pr}, mk_eq_rec(m_ctx, motive, minor, major)); } } diff --git a/src/library/congr_lemma.h b/src/library/congr_lemma.h index ace11693c7..ea0c426aa2 100644 --- a/src/library/congr_lemma.h +++ b/src/library/congr_lemma.h @@ -9,7 +9,7 @@ Author: Leonardo de Moura namespace lean { enum class congr_arg_kind { - /* It is a parameter for the congruence lemma, the parit occurs in the left and right hand sides. */ + /* It is a parameter for the congruence lemma, the parameter occurs in the left and right hand sides. */ Fixed, /* It is not a parameter for the congruence lemma, the lemma was specialized for this parameter. This only happens if the parameter is a subsingleton/proposition, and other parameters depend on it. */ diff --git a/src/library/tactic/CMakeLists.txt b/src/library/tactic/CMakeLists.txt index fb7b6b566c..54ee2a64f4 100644 --- a/src/library/tactic/CMakeLists.txt +++ b/src/library/tactic/CMakeLists.txt @@ -2,4 +2,5 @@ add_library(tactic OBJECT tactic_state.cpp intro_tactic.cpp revert_tactic.cpp rename_tactic.cpp clear_tactic.cpp app_builder_tactics.cpp subst_tactic.cpp exact_tactic.cpp change_tactic.cpp assert_tactic.cpp apply_tactic.cpp - fun_info_tactics.cpp elaborate.cpp init_module.cpp) + fun_info_tactics.cpp congr_lemma_tactics.cpp + elaborate.cpp init_module.cpp) diff --git a/src/library/tactic/congr_lemma_tactics.cpp b/src/library/tactic/congr_lemma_tactics.cpp new file mode 100644 index 0000000000..5020856282 --- /dev/null +++ b/src/library/tactic/congr_lemma_tactics.cpp @@ -0,0 +1,127 @@ +/* +Copyright (c) 2016 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "library/congr_lemma.h" +#include "library/vm/vm_list.h" +#include "library/vm/vm_expr.h" +#include "library/vm/vm_nat.h" +#include "library/tactic/tactic_state.h" + +namespace lean { +vm_obj to_obj(congr_arg_kind k) { + return mk_vm_simple(static_cast(k)); +} + +vm_obj to_obj(list const & ls) { + return to_vm_list(ls, [&](congr_arg_kind const & k) { return to_obj(k); }); +} + +/* + structure congr_lemma := + (type : expr) (proof : expr) (arg_kids : list congr_arg_kind) +*/ +vm_obj to_obj(congr_lemma const & c) { + return mk_vm_constructor(0, to_obj(c.get_type()), to_obj(c.get_proof()), to_obj(c.get_arg_kinds())); +} + +static vm_obj mk_result(optional const & l, vm_obj const & s) { + if (l) + return mk_tactic_success(to_obj(*l), to_tactic_state(s)); + else + return mk_tactic_exception("failed to generate congruence lemma, " + "use 'set_option trace.congr_lemma true' to obtain additional information", + to_tactic_state(s)); +} + +#define TRY LEAN_TACTIC_TRY +#define CATCH LEAN_TACTIC_CATCH(to_tactic_state(s)) + +vm_obj tactic_mk_congr_simp(vm_obj const & fn, vm_obj const & s) { + TRY; + type_context_scope ctx(s); + return mk_result(mk_congr_simp(ctx, to_expr(fn)), s); + CATCH; +} + +vm_obj tactic_mk_congr_simp_n(vm_obj const & fn, vm_obj const & n, vm_obj const & s) { + TRY; + type_context_scope ctx(s); + return mk_result(mk_congr_simp(ctx, to_expr(fn), force_to_unsigned(n, 0)), s); + CATCH; +} + +vm_obj tactic_mk_specialized_congr_simp(vm_obj const & a, vm_obj const & s) { + TRY; + type_context_scope ctx(s); + return mk_result(mk_specialized_congr_simp(ctx, to_expr(a)), s); + CATCH; +} + +vm_obj tactic_mk_congr(vm_obj const & fn, vm_obj const & s) { + TRY; + type_context_scope ctx(s); + return mk_result(mk_congr(ctx, to_expr(fn)), s); + CATCH; +} + +vm_obj tactic_mk_congr_n(vm_obj const & fn, vm_obj const & n, vm_obj const & s) { + TRY; + type_context_scope ctx(s); + return mk_result(mk_congr(ctx, to_expr(fn), force_to_unsigned(n, 0)), s); + CATCH; +} + +vm_obj tactic_mk_specialized_congr(vm_obj const & a, vm_obj const & s) { + TRY; + type_context_scope ctx(s); + return mk_result(mk_specialized_congr(ctx, to_expr(a)), s); + CATCH; +} + +vm_obj tactic_mk_hcongr(vm_obj const & fn, vm_obj const & s) { + TRY; + type_context_scope ctx(s); + return mk_result(mk_hcongr(ctx, to_expr(fn)), s); + CATCH; +} + +vm_obj tactic_mk_hcongr_n(vm_obj const & fn, vm_obj const & n, vm_obj const & s) { + TRY; + type_context_scope ctx(s); + return mk_result(mk_hcongr(ctx, to_expr(fn), force_to_unsigned(n, 0)), s); + CATCH; +} + +vm_obj tactic_mk_rel_iff_congr(vm_obj const & r, vm_obj const & s) { + TRY; + type_context_scope ctx(s); + return mk_result(mk_rel_iff_congr(ctx, to_expr(r)), s); + CATCH; +} + +vm_obj tactic_mk_rel_eq_congr(vm_obj const & r, vm_obj const & s) { + TRY; + type_context_scope ctx(s); + return mk_result(mk_rel_eq_congr(ctx, to_expr(r)), s); + CATCH; +} + +void initialize_congr_lemma_tactics() { + DECLARE_VM_BUILTIN(name({"tactic", "mk_congr_simp"}), tactic_mk_congr_simp); + DECLARE_VM_BUILTIN(name({"tactic", "mk_congr_simp_n"}), tactic_mk_congr_simp_n); + DECLARE_VM_BUILTIN(name({"tactic", "mk_specialized_congr_simp"}), tactic_mk_specialized_congr_simp); + DECLARE_VM_BUILTIN(name({"tactic", "mk_congr"}), tactic_mk_congr); + DECLARE_VM_BUILTIN(name({"tactic", "mk_congr_n"}), tactic_mk_congr_n); + DECLARE_VM_BUILTIN(name({"tactic", "mk_specialized_congr"}), tactic_mk_specialized_congr); + DECLARE_VM_BUILTIN(name({"tactic", "mk_hcongr"}), tactic_mk_hcongr); + DECLARE_VM_BUILTIN(name({"tactic", "mk_hcongr_n"}), tactic_mk_hcongr_n); + DECLARE_VM_BUILTIN(name({"tactic", "mk_rel_iff_congr"}), tactic_mk_rel_iff_congr); + DECLARE_VM_BUILTIN(name({"tactic", "mk_rel_eq_congr"}), tactic_mk_rel_eq_congr); +} + +void finalize_congr_lemma_tactics() { +} +} diff --git a/src/library/tactic/congr_lemma_tactics.h b/src/library/tactic/congr_lemma_tactics.h new file mode 100644 index 0000000000..262d840f6f --- /dev/null +++ b/src/library/tactic/congr_lemma_tactics.h @@ -0,0 +1,11 @@ +/* +Copyright (c) 2016 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_congr_lemma_tactics(); +void finalize_congr_lemma_tactics(); +} diff --git a/src/library/tactic/fun_info_tactics.cpp b/src/library/tactic/fun_info_tactics.cpp index 156e034a61..bc0d366829 100644 --- a/src/library/tactic/fun_info_tactics.cpp +++ b/src/library/tactic/fun_info_tactics.cpp @@ -65,32 +65,40 @@ fun_info get_fun_info(type_context & ctx, expr const & fn, unsigned nargs); fun_info get_specialized_fun_info(type_context & ctx, expr const & app); unsigned get_specialization_prefix_size(type_context & ctx, expr const & fn, unsigned nargs); -vm_obj tactic_get_fun_info(vm_obj const & fn, vm_obj const & s0) { - tactic_state const & s = to_tactic_state(s0); - metavar_context mctx_tmp = s.mctx(); - type_context ctx = mk_type_context_for(s, mctx_tmp); - return mk_tactic_success(to_obj(get_fun_info(ctx, to_expr(fn))), s); +#define TRY LEAN_TACTIC_TRY +#define CATCH LEAN_TACTIC_CATCH(to_tactic_state(s)) + +static vm_obj mk_result(fun_info const & info, vm_obj const & s) { + return mk_tactic_success(to_obj(info), to_tactic_state(s)); } -vm_obj tactic_get_fun_info_n(vm_obj const & fn, vm_obj const & n, vm_obj const & s0) { - tactic_state const & s = to_tactic_state(s0); - metavar_context mctx_tmp = s.mctx(); - type_context ctx = mk_type_context_for(s, mctx_tmp); - return mk_tactic_success(to_obj(get_fun_info(ctx, to_expr(fn), force_to_unsigned(n, 0))), s); +vm_obj tactic_get_fun_info(vm_obj const & fn, vm_obj const & s) { + TRY; + type_context_scope ctx(s); + return mk_result(get_fun_info(ctx, to_expr(fn)), s); + CATCH; } -vm_obj tactic_get_spec_fun_info(vm_obj const & app, vm_obj const & s0) { - tactic_state const & s = to_tactic_state(s0); - metavar_context mctx_tmp = s.mctx(); - type_context ctx = mk_type_context_for(s, mctx_tmp); - return mk_tactic_success(to_obj(get_specialized_fun_info(ctx, to_expr(app))), s); +vm_obj tactic_get_fun_info_n(vm_obj const & fn, vm_obj const & n, vm_obj const & s) { + TRY; + type_context_scope ctx(s); + return mk_result(get_fun_info(ctx, to_expr(fn), force_to_unsigned(n, 0)), s); + CATCH; } -vm_obj tactic_get_spec_prefix_size(vm_obj const & fn, vm_obj const & n, vm_obj const & s0) { - tactic_state const & s = to_tactic_state(s0); - metavar_context mctx_tmp = s.mctx(); - type_context ctx = mk_type_context_for(s, mctx_tmp); - return mk_tactic_success(to_obj(get_specialization_prefix_size(ctx, to_expr(fn), force_to_unsigned(n, 0))), s); +vm_obj tactic_get_spec_fun_info(vm_obj const & app, vm_obj const & s) { + TRY; + type_context_scope ctx(s); + return mk_result(get_specialized_fun_info(ctx, to_expr(app)), s); + CATCH; +} + +vm_obj tactic_get_spec_prefix_size(vm_obj const & fn, vm_obj const & n, vm_obj const & s) { + TRY; + type_context_scope ctx(s); + return mk_tactic_success(mk_vm_nat(get_specialization_prefix_size(ctx, to_expr(fn), force_to_unsigned(n, 0))), + to_tactic_state(s)); + CATCH; } void initialize_fun_info_tactics() { diff --git a/src/library/tactic/init_module.cpp b/src/library/tactic/init_module.cpp index 944dbbe12f..927db5a4cd 100644 --- a/src/library/tactic/init_module.cpp +++ b/src/library/tactic/init_module.cpp @@ -16,6 +16,7 @@ Author: Leonardo de Moura #include "library/tactic/assert_tactic.h" #include "library/tactic/apply_tactic.h" #include "library/tactic/fun_info_tactics.h" +#include "library/tactic/congr_lemma_tactics.h" #include "library/tactic/elaborate.h" #include "library/tactic/defeq_simplifier/init_module.h" @@ -33,12 +34,14 @@ void initialize_tactic_module() { initialize_assert_tactic(); initialize_apply_tactic(); initialize_fun_info_tactics(); + initialize_congr_lemma_tactics(); initialize_elaborate(); initialize_defeq_simplifier_module(); } void finalize_tactic_module() { finalize_defeq_simplifier_module(); finalize_elaborate(); + finalize_congr_lemma_tactics(); finalize_fun_info_tactics(); finalize_apply_tactic(); finalize_assert_tactic(); diff --git a/src/library/tactic/tactic_state.cpp b/src/library/tactic/tactic_state.cpp index 2fd554ab1d..2da2900fb6 100644 --- a/src/library/tactic/tactic_state.cpp +++ b/src/library/tactic/tactic_state.cpp @@ -79,8 +79,7 @@ tactic_state set_mctx_goals(tactic_state const & s, metavar_context const & mctx } format tactic_state::pp_expr(formatter_factory const & fmtf, expr const & e) const { - metavar_context mctx_tmp = mctx(); - type_context ctx = mk_type_context_for(*this, mctx_tmp, transparency_mode::All); + type_context_scope ctx(*this, transparency_mode::All); formatter fmt = fmtf(env(), get_options(), ctx); return fmt(e); } diff --git a/src/library/tactic/tactic_state.h b/src/library/tactic/tactic_state.h index 9b22534e11..e2473b1428 100644 --- a/src/library/tactic/tactic_state.h +++ b/src/library/tactic/tactic_state.h @@ -123,6 +123,19 @@ inline type_context mk_type_context_for(tactic_state const & s, metavar_context Code \ }) +struct type_context_scope { + metavar_context m_mctx; + type_context m_ctx; + type_context_scope(tactic_state const & s, transparency_mode m = transparency_mode::Semireducible): + m_mctx(s.mctx()), m_ctx(mk_type_context_for(s, m_mctx, m)) {} + type_context_scope(vm_obj const & s, transparency_mode m = transparency_mode::Semireducible): + type_context_scope(to_tactic_state(s), m) {} + operator type_context &() { return m_ctx; } +}; + +#define LEAN_TACTIC_TRY try { +#define LEAN_TACTIC_CATCH(S) } catch (exception const & ex) { return mk_tactic_exception(ex, S); } + void initialize_tactic_state(); void finalize_tactic_state(); } diff --git a/tests/lean/run/congr_lemma1.lean b/tests/lean/run/congr_lemma1.lean new file mode 100644 index 0000000000..526c2586d1 --- /dev/null +++ b/tests/lean/run/congr_lemma1.lean @@ -0,0 +1,12 @@ +open tactic + +set_option pp.binder_types true + +example : true := +by do + ite ← mk_const "ite", + l ← mk_congr_simp ite, + trace_expr (congr_lemma.type l), + l ← mk_hcongr ite, + trace_expr (congr_lemma.type l), + constructor