From c8e1ec87d2aabce91df905b1b6b8eb3d1cee6c3f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 14 Jan 2014 18:22:33 -0800 Subject: [PATCH] feat(library/simplifier): add to_ceqs function that converts a theorem into a sequence of conditional equations Signed-off-by: Leonardo de Moura --- src/CMakeLists.txt | 2 + src/frontends/lua/register_modules.cpp | 2 + src/library/ite.h | 1 + src/library/kernel_bindings.cpp | 2 + src/library/simplifier/CMakeLists.txt | 2 + src/library/simplifier/ceq.cpp | 127 +++++++++++++++++++++++ src/library/simplifier/ceq.h | 29 ++++++ src/library/simplifier/register_module.h | 18 ++++ tests/lua/ceq1.lua | 37 +++++++ 9 files changed, 220 insertions(+) create mode 100644 src/library/simplifier/CMakeLists.txt create mode 100644 src/library/simplifier/ceq.cpp create mode 100644 src/library/simplifier/ceq.h create mode 100644 src/library/simplifier/register_module.h create mode 100644 tests/lua/ceq1.lua diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 2acc77f0f..22eea3a4d 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -219,6 +219,8 @@ add_subdirectory(library/arith) set(LEAN_LIBS ${LEAN_LIBS} arithlib) add_subdirectory(library/rewriter) set(LEAN_LIBS ${LEAN_LIBS} rewriter) +add_subdirectory(library/simplifier) +set(LEAN_LIBS ${LEAN_LIBS} simplifier) add_subdirectory(library/elaborator) set(LEAN_LIBS ${LEAN_LIBS} elaborator) add_subdirectory(library/tactic) diff --git a/src/frontends/lua/register_modules.cpp b/src/frontends/lua/register_modules.cpp index 3218718f4..cbe60038b 100644 --- a/src/frontends/lua/register_modules.cpp +++ b/src/frontends/lua/register_modules.cpp @@ -10,6 +10,7 @@ Author: Leonardo de Moura #include "library/register_module.h" #include "library/io_state_stream.h" #include "library/arith/register_module.h" +#include "library/simplifier/register_module.h" #include "library/tactic/register_module.h" #include "frontends/lean/register_module.h" @@ -19,6 +20,7 @@ void register_modules() { register_sexpr_module(); register_core_module(); register_arith_module(); + register_simplifier_module(); register_tactic_module(); register_frontend_lean_module(); } diff --git a/src/library/ite.h b/src/library/ite.h index 098b2015c..9238a97e5 100644 --- a/src/library/ite.h +++ b/src/library/ite.h @@ -11,6 +11,7 @@ Author: Leonardo de Moura namespace lean { expr mk_ite_fn(); bool is_ite_fn(expr const & e); +inline bool is_ite(expr const & e) { return is_app(e) && is_ite_fn(arg(e, 0)); } inline expr mk_ite(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app(mk_ite_fn(), e1, e2, e3, e4); } void import_ite(environment const & env, io_state const & ios); void open_ite(lua_State * L); diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp index c34aeba56..7307a434b 100644 --- a/src/library/kernel_bindings.cpp +++ b/src/library/kernel_bindings.cpp @@ -452,6 +452,7 @@ EXPR_PRED(is_and) EXPR_PRED(is_or) EXPR_PRED(is_implies) EXPR_PRED(is_exists) +EXPR_PRED(is_eq) /** \brief Iterator (closure base function) for application args. See \c expr_args @@ -652,6 +653,7 @@ static const struct luaL_Reg expr_m[] = { {"is_or", safe_function}, {"is_implies", safe_function}, {"is_exists", safe_function}, + {"is_eq", safe_function}, {0, 0} }; diff --git a/src/library/simplifier/CMakeLists.txt b/src/library/simplifier/CMakeLists.txt new file mode 100644 index 000000000..103193e20 --- /dev/null +++ b/src/library/simplifier/CMakeLists.txt @@ -0,0 +1,2 @@ +add_library(simplifier ceq.cpp) +target_link_libraries(simplifier ${LEAN_LIBS}) diff --git a/src/library/simplifier/ceq.cpp b/src/library/simplifier/ceq.cpp new file mode 100644 index 000000000..9d91d4049 --- /dev/null +++ b/src/library/simplifier/ceq.cpp @@ -0,0 +1,127 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "util/list_fn.h" +#include "kernel/builtin.h" +#include "kernel/free_vars.h" +#include "library/expr_pair.h" +#include "library/ite.h" +#include "library/kernel_bindings.h" + +namespace lean { +static name g_Hc("Hc"); // auxiliary name for if-then-else + +/** + \brief Auxiliary functional object for creating "conditional equations" +*/ +class to_ceqs_fn { + ro_environment const & m_env; + unsigned m_idx; + + static list mk_singleton(expr const & e, expr const & H) { + return list(mk_pair(e, H)); + } + + bool imported_ite() { + return m_env->imported("if_then_else"); + } + + name mk_aux_name() { + if (m_idx == 0) { + m_idx = 1; + return g_Hc; + } else { + name r = name(g_Hc, m_idx); + m_idx++; + return r; + } + } + + list apply(expr const & e, expr const & H) { + if (is_eq(e) || is_heq(e)) { + return mk_singleton(e, H); + } else if (is_not(e)) { + expr a = arg(e, 1); + expr new_e = mk_heq(a, False); + expr new_H = mk_eqf_intro_th(a, H); + return mk_singleton(new_e, new_H); + } else if (is_and(e)) { + expr a1 = arg(e, 1); + expr a2 = arg(e, 2); + expr new_H1 = mk_and_eliml_th(a1, a2, H); + expr new_H2 = mk_and_elimr_th(a1, a2, H); + return append(apply(a1, new_H1), apply(a2, new_H2)); + } else if (is_pi(e)) { + expr new_e = abst_body(e); + expr new_H = mk_app(lift_free_vars(H, 1), mk_var(0)); + auto ceqs = apply(new_e, new_H); + if (length(ceqs) == 1 && new_e == car(ceqs).first) { + return mk_singleton(e, H); + } else { + return map(ceqs, [&](expr_pair const & e_H) -> expr_pair { + expr new_e = mk_pi(abst_name(e), abst_domain(e), e_H.first); + expr new_H = mk_lambda(abst_name(e), abst_domain(e), e_H.second); + return mk_pair(new_e, new_H); + }); + } + } else if (is_ite(e) && imported_ite()) { + expr c = arg(e, 2); + expr not_c = mk_not(c); + expr c1 = lift_free_vars(c, 1); + expr a1 = lift_free_vars(arg(e, 3), 1); + expr b1 = lift_free_vars(arg(e, 4), 1); + expr H1 = lift_free_vars(H, 1); + auto then_ceqs = apply(a1, mk_if_imp_then_th(c1, a1, b1, H1, mk_var(0))); + auto else_ceqs = apply(b1, mk_if_imp_else_th(c1, a1, b1, H1, mk_var(0))); + name Hc = mk_aux_name(); + auto new_then_ceqs = map(then_ceqs, [&](expr_pair const & e_H) { + expr new_e = mk_pi(Hc, c, e_H.first); + expr new_H = mk_lambda(Hc, c, e_H.second); + return mk_pair(new_e, new_H); + }); + auto new_else_ceqs = map(else_ceqs, [&](expr_pair const & e_H) { + expr new_e = mk_pi(Hc, not_c, e_H.first); + expr new_H = mk_lambda(Hc, not_c, e_H.second); + return mk_pair(new_e, new_H); + }); + return append(new_then_ceqs, new_else_ceqs); + } else { + return mk_singleton(mk_heq(e, True), mk_eqt_intro_th(e, H)); + } + } +public: + to_ceqs_fn(ro_environment const & env):m_env(env), m_idx(0) {} + + list operator()(expr const & e, expr const & H) { + return apply(e, H); + } +}; + +list to_ceqs(ro_environment const & env, expr const & e, expr const & H) { + return to_ceqs_fn(env)(e, H); +} + +static int to_ceqs(lua_State * L) { + ro_shared_environment env(L, 1); + auto r = to_ceqs(env, to_expr(L, 2), to_expr(L, 3)); + lua_newtable(L); + int i = 1; + for (auto p : r) { + lua_newtable(L); + push_expr(L, p.first); + lua_rawseti(L, -2, 1); + push_expr(L, p.second); + lua_rawseti(L, -2, 2); + lua_rawseti(L, -2, i); + i = i + 1; + } + return 1; +} + +void open_ceq(lua_State * L) { + SET_GLOBAL_FUN(to_ceqs, "to_ceqs"); +} +} diff --git a/src/library/simplifier/ceq.h b/src/library/simplifier/ceq.h new file mode 100644 index 000000000..64d5ff3f6 --- /dev/null +++ b/src/library/simplifier/ceq.h @@ -0,0 +1,29 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "util/lua.h" +#include "kernel/environment.h" +#include "library/expr_pair.h" +namespace lean { +/** + \brief Given a proposition \c e and its proof H, return a list of conditional equations (and proofs) extracted from \c e. + + The following rules are used to convert \c e into conditional equations. + + [not P] ---> P = false + [P /\ Q] ---> [P], [Q] + [if P then Q else R] ---> P -> [Q], not P -> [Q] + [P -> Q] ---> P -> [Q] + [forall x : A, P] ---> forall x : A, [P] + + P ---> P = true (if none of the rules above apply and P is not an equality) +*/ +list to_ceqs(ro_environment const & env, expr const & e, expr const & H); +void open_ceq(lua_State * L); +} + + diff --git a/src/library/simplifier/register_module.h b/src/library/simplifier/register_module.h new file mode 100644 index 000000000..89e643b00 --- /dev/null +++ b/src/library/simplifier/register_module.h @@ -0,0 +1,18 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "util/script_state.h" +#include "library/simplifier/ceq.h" + +namespace lean { +inline void open_simplifier_module(lua_State * L) { + open_ceq(L); +} +inline void register_simplifier_module() { + script_state::register_module(open_simplifier_module); +} +} diff --git a/tests/lua/ceq1.lua b/tests/lua/ceq1.lua new file mode 100644 index 000000000..6a319428a --- /dev/null +++ b/tests/lua/ceq1.lua @@ -0,0 +1,37 @@ +local env = get_environment() + +function is_ceq(e) + while e:is_pi() do + _, _, e = e:fields() + end + return e:is_eq() or e:is_heq() +end + +function show_ceqs(ceqs) + for i = 1, #ceqs do + print(ceqs[i][1], ceqs[i][2]) + env:type_check(ceqs[i][2]) + assert(is_ceq(ceqs[i][1])) + end +end + +function test_ceq(name, expected) + local obj = env:find_object(name) + local r = to_ceqs(env, obj:get_type(), Const(name)) + show_ceqs(r) + assert(#r == expected) +end + +parse_lean_cmds([[ + import if_then_else + variable f : Nat -> Nat + axiom Ax1 : forall x : Nat, x > 0 -> f x < 0 /\ not (f x = 1) + axiom Ax2 : forall x : Nat, x < 0 -> f (f x) = x + variable g : Nat -> Nat -> Nat + axiom Ax3 : forall x : Nat, not (x = 1) -> if (x < 0) then (g x x = 0) else (g x x < 0 /\ g x 0 = 1 /\ g 0 x = 2) +]]) + +test_ceq("Ax1", 2) +test_ceq("Ax2", 1) +test_ceq("Ax3", 4) +