feat(library/simplifier): add to_ceqs function that converts a theorem into a sequence of conditional equations

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

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)

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();
 }

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);

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<expr_is_or>},
     {"is_implies",       safe_function<expr_is_implies>},
     {"is_exists",        safe_function<expr_is_exists>},
+    {"is_eq",            safe_function<expr_is_eq>},
     {0, 0}
 };
 

src/library/simplifier/CMakeLists.txt

@@ -0,0 +1,2 @@
+add_library(simplifier ceq.cpp)
+target_link_libraries(simplifier ${LEAN_LIBS})

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<expr_pair> mk_singleton(expr const & e, expr const & H) {
+        return list<expr_pair>(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<expr_pair> 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<expr_pair> operator()(expr const & e, expr const & H) {
+        return apply(e, H);
+    }
+};
+
+list<expr_pair> 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");
+}
+}

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<expr_pair> to_ceqs(ro_environment const & env, expr const & e, expr const & H);
+void open_ceq(lua_State * L);
+}
+
+

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);
+}
+}

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)
+