From f954ddbdbfad168e7e8a42617eeca14d38ff0c97 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 6 Sep 2016 18:01:09 -0700 Subject: [PATCH] feat(library/injectivity): add injectivity attribute --- src/library/CMakeLists.txt | 2 +- src/library/init_module.cpp | 3 + src/library/injectivity.cpp | 124 +++++++++++++++++++++++++++++++ src/library/injectivity.h | 22 ++++++ tests/lean/run/pack_unpack1.lean | 35 +++++++++ 5 files changed, 185 insertions(+), 1 deletion(-) create mode 100644 src/library/injectivity.cpp create mode 100644 src/library/injectivity.h create mode 100644 tests/lean/run/pack_unpack1.lean diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index 976c24d855..dd124d94b4 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -14,7 +14,7 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp local_context.cpp metavar_context.cpp type_context.cpp export_decl.cpp delayed_abstraction.cpp fun_info.cpp congr_lemma.cpp defeq_canonizer.cpp scope_pos_info_provider.cpp inductive.cpp mpq_macro.cpp arith_instance_manager.cpp replace_visitor_with_tc.cpp - aux_definition.cpp + aux_definition.cpp injectivity.cpp # Legacy -- The following files will be eventually deleted normalize.cpp justification.cpp constraint.cpp metavar.cpp choice.cpp locals.cpp diff --git a/src/library/init_module.cpp b/src/library/init_module.cpp index acd219fec1..51baa5fbfa 100644 --- a/src/library/init_module.cpp +++ b/src/library/init_module.cpp @@ -49,6 +49,7 @@ Author: Leonardo de Moura #include "library/inductive.h" #include "library/mpq_macro.h" #include "library/arith_instance_manager.h" +#include "library/injectivity.h" // #include "library/congr_lemma_manager.h" // #include "library/light_lt_manager.h" @@ -129,9 +130,11 @@ void initialize_library_module() { initialize_library_inductive(); initialize_mpq_macro(); initialize_arith_instance_manager(); + initialize_injectivity(); } void finalize_library_module() { + finalize_injectivity(); finalize_arith_instance_manager(); finalize_mpq_macro(); finalize_library_inductive(); diff --git a/src/library/injectivity.cpp b/src/library/injectivity.cpp new file mode 100644 index 0000000000..c59a8a1bc3 --- /dev/null +++ b/src/library/injectivity.cpp @@ -0,0 +1,124 @@ +/* +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 "kernel/type_checker.h" +#include "library/util.h" +#include "library/scoped_ext.h" +#include "library/attribute_manager.h" +#include "library/injectivity.h" + +namespace lean { +struct injectivity_entry { + name m_fn; + injectivity_info m_info; + injectivity_entry() {} + injectivity_entry(name const & fn, injectivity_info const & info): + m_fn(fn), m_info(info) {} +}; + +struct injectivity_state { + name_map m_fn_info; /* mapping from function to its inverse and lemma */ + name_map m_inv_info; /* mapping from inverse to function */ + + void add(injectivity_entry const & e) { + m_fn_info.insert(e.m_fn, e.m_info); + m_inv_info.insert(e.m_info.m_inv, e.m_fn); + } +}; + +static name * g_injectivity_name = nullptr; +static std::string * g_key = nullptr; + +struct injectivity_config { + typedef injectivity_state state; + typedef injectivity_entry entry; + static void add_entry(environment const &, io_state const &, state & s, entry const & e) { + s.add(e); + } + static name const & get_class_name() { + return *g_injectivity_name; + } + static std::string const & get_serialization_key() { + return *g_key; + } + static void write_entry(serializer & s, entry const & e) { + s << e.m_fn << e.m_info.m_arity << e.m_info.m_inv << e.m_info.m_lemma; + } + static entry read_entry(deserializer & d) { + entry e; + d >> e.m_fn >> e.m_info.m_arity >> e.m_info.m_inv >> e.m_info.m_lemma; + return e; + } + static optional get_fingerprint(entry const & e) { + return some(e.m_info.m_lemma.hash()); + } +}; + +template class scoped_ext; +typedef scoped_ext injectivity_ext; + +optional has_inverse(environment const & env, name const & fn) { + if (auto r = injectivity_ext::get_state(env).m_fn_info.find(fn)) + return optional(*r); + else + return optional(); +} + +optional is_inverse(environment const & env, name const & inv) { + if (auto r = injectivity_ext::get_state(env).m_inv_info.find(inv)) + return optional(*r); + else + return optional(); +} + +void throw_injectivity_error() { + throw exception("invalid injectivity lemma, " + "it should be of the form: (f ... (g ... x)) = x"); +} + +environment add_injectivity_lemma(environment const & env, name const & lemma, bool persistent) { + type_checker tc(env); + declaration d = env.get(lemma); + buffer tele; + expr type = to_telescope(tc, d.get_type(), tele); + expr lhs, rhs; + if (!is_eq(type, lhs, rhs) || !is_app(lhs) || !is_constant(get_app_fn(lhs)) || !is_local(rhs)) + throw_injectivity_error(); + injectivity_info info; + buffer lhs_args; + expr const & lhs_fn = get_app_args(lhs, lhs_args); + info.m_inv = const_name(lhs_fn); + info.m_lemma = lemma; + expr const & last_arg = lhs_args.back(); + if (!is_app(last_arg) || !is_constant(get_app_fn(last_arg))) + throw_injectivity_error(); + buffer last_arg_args; + expr const & fn = get_app_args(last_arg, last_arg_args); + if (last_arg_args.back() != rhs) + throw_injectivity_error(); + info.m_arity = last_arg_args.size(); + return injectivity_ext::add_entry(env, get_dummy_ios(), injectivity_entry(const_name(fn), info), persistent); +} + +void initialize_injectivity() { + g_injectivity_name = new name("injectivity"); + g_key = new std::string("injectivity"); + injectivity_ext::initialize(); + + register_system_attribute(basic_attribute("injectivity", "attribute for marking injectivity lemmas " + "used by the equation compiler", + [](environment const & env, io_state const &, name const & d, unsigned, + bool persistent) { + return add_injectivity_lemma(env, d, persistent); + })); +} + +void finalize_injectivity() { + injectivity_ext::finalize(); + delete g_key; + delete g_injectivity_name; +} +} diff --git a/src/library/injectivity.h b/src/library/injectivity.h new file mode 100644 index 0000000000..5ce1ade3a2 --- /dev/null +++ b/src/library/injectivity.h @@ -0,0 +1,22 @@ +/* +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 +#include "kernel/environment.h" + +namespace lean { +struct injectivity_info { + unsigned m_arity; + name m_inv; + name m_lemma; +}; + +optional has_inverse(environment const & env, name const & fn); +optional is_inverse(environment const & env, name const & inv); +environment add_injectivity_lemma(environment const & env, name const & lemma, bool persistent); +void initialize_injectivity(); +void finalize_injectivity(); +} diff --git a/tests/lean/run/pack_unpack1.lean b/tests/lean/run/pack_unpack1.lean new file mode 100644 index 0000000000..de9002598c --- /dev/null +++ b/tests/lean/run/pack_unpack1.lean @@ -0,0 +1,35 @@ +set_option new_elaborator true + +inductive tree_core (A : Type) : bool → Type +| leaf' : A → tree_core ff +| node' : tree_core tt → tree_core ff +| nil' {} : tree_core tt +| cons' : tree_core ff → tree_core tt → tree_core tt + +attribute [reducible] +definition tree (A : Type) := tree_core A ff + +attribute [reducible] +definition tree_list (A : Type) := tree_core A tt + +open tree_core + +definition pack {A : Type} : list (tree A) → tree_core A tt +| [] := nil' +| (a::l) := cons' a (pack l) + +definition unpack {A : Type} : ∀ {b}, tree_core A b → list (tree A) +| .tt nil' := [] +| .tt (cons' a t) := a :: unpack t +| .ff (leaf' a) := [] +| .ff (node' l) := [] + +attribute [injectivity] +lemma unpack_pack {A : Type} : ∀ (l : list (tree A)), unpack (pack l) = l +| [] := rfl +| (a::l) := + show a :: unpack (pack l) = a :: l, from + congr_arg (λ x, a :: x) (unpack_pack l) + +definition tree.node {A : Type} (l : list (tree A)) : tree A := +tree_core.node' (pack l)