feat(library): add if_then_else Lean/C++ interface

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

src/builtin/CMakeLists.txt

@@ -95,7 +95,8 @@ add_theory("Real.lean"         "${CMAKE_CURRENT_BINARY_DIR}/Int.olean")
 add_theory("specialfn.lean"    "${CMAKE_CURRENT_BINARY_DIR}/Real.olean")
 add_theory("cast.lean"         "${CMAKE_CURRENT_BINARY_DIR}/Nat.olean")
 
-update_interface("kernel.olean" "kernel" "-n")
-update_interface("Nat.olean"    "library/arith" "-n")
-update_interface("Int.olean"    "library/arith" "")
-update_interface("Real.olean"   "library/arith" "")
+update_interface("kernel.olean"       "kernel" "-n")
+update_interface("Nat.olean"          "library/arith" "-n")
+update_interface("Int.olean"          "library/arith" "")
+update_interface("Real.olean"         "library/arith" "")
+update_interface("if_then_else.olean" "library" "")

src/builtin/if_then_else.lean

@@ -1,3 +1,5 @@
+import macros
+
 -- if_then_else expression support
 builtin ite {A : (Type U)} : Bool → A → A → A
 notation 60 if _ then _ else _ : ite
@@ -25,4 +27,15 @@ theorem if_congr {A : TypeU} {b c : Bool} {x y u v : A} (H_bc : b = c) (H_xu :
                                          ...  = (if false then u else v) : symm (if_false _ _)
                                          ...  = (if c then u else v)     : { symm (eqf_intro H_nc) })
 
+theorem if_imp_then {a b c : Bool} (H : if a then b else c) : a → b
+:= assume Ha : a, eqt_elim (calc   b = (if true then b else c) : symm (if_true b c)
+                                 ... = (if a then b else c)    : { symm (eqt_intro Ha) }
+                                 ... = true                    : eqt_intro H)
+
+theorem if_imp_else {a b c : Bool} (H : if a then b else c) : ¬ a → c
+:= assume Hna : ¬ a, eqt_elim (calc   c = (if false then b else c) : symm (if_false b c)
+                                    ... = (if a then b else c)     : { symm (eqf_intro Hna) }
+                                    ... = true                     : eqt_intro H)
+
+
 set_opaque ite true

src/kernel/builtin.cpp

@@ -78,44 +78,6 @@ bool is_false(expr const & e) {
 }
 // =======================================
 
-// =======================================
-// If-then-else builtin operator
-static name   g_if_name("ite");
-static format g_if_fmt(g_if_name);
-/**
-   \brief Semantic attachment for if-then-else operator with type
-   <code>Pi (A : Type), Bool -> A -> A -> A</code>
-*/
-class if_fn_value : public value {
-    expr m_type;
-    static expr mk_type() {
-        expr A    = Const("A");
-        // Pi (A: Type), bool -> A -> A -> A
-        return Pi({A, TypeU}, Bool >> (A >> (A >> A)));
-    }
-public:
-    if_fn_value():m_type(mk_type()) {}
-    virtual ~if_fn_value() {}
-    virtual expr get_type() const { return m_type; }
-    virtual name get_name() const { return g_if_name; }
-    virtual optional<expr> normalize(unsigned num_args, expr const * args) const {
-        if (num_args == 5 && is_bool_value(args[2]) && is_value(args[3]) && is_value(args[4])) {
-            if (to_bool(args[2]))
-                return some_expr(args[3]); // if A true a b  --> a
-            else
-                return some_expr(args[4]); // if A false a b --> b
-        } else {
-            return none_expr();
-        }
-    }
-    virtual void write(serializer & s) const { s << "ite"; }
-};
-MK_BUILTIN(if_fn, if_fn_value);
-MK_IS_BUILTIN(is_if_fn, mk_if_fn());
-static register_builtin_fn if_blt("ite", []() { return mk_if_fn(); });
-static value::register_deserializer_fn if_ds("ite", [](deserializer & ) { return mk_if_fn(); });
-// =======================================
-
 void import_kernel(environment const & env, io_state const & ios) {
     env->import("kernel", ios);
 }

src/library/CMakeLists.txt

@@ -1,6 +1,6 @@
 add_library(library kernel_bindings.cpp deep_copy.cpp
   context_to_lambda.cpp placeholder.cpp expr_lt.cpp substitution.cpp
   fo_unify.cpp bin_op.cpp eq_heq.cpp io_state_stream.cpp printer.cpp
-  hop_match.cpp)
+  hop_match.cpp ite.cpp)
 
 target_link_libraries(library ${LEAN_LIBS})

src/library/if_then_else_decls.cpp

@@ -0,0 +1,15 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+*/
+// Automatically generated file, DO NOT EDIT
+#include "kernel/environment.h"
+#include "kernel/decl_macros.h"
+namespace lean {
+MK_CONSTANT(if_true_fn, name("if_true"));
+MK_CONSTANT(if_false_fn, name("if_false"));
+MK_CONSTANT(if_a_a_fn, name("if_a_a"));
+MK_CONSTANT(if_congr_fn, name("if_congr"));
+MK_CONSTANT(if_imp_then_fn, name("if_imp_then"));
+MK_CONSTANT(if_imp_else_fn, name("if_imp_else"));
+}

src/library/if_then_else_decls.h

@@ -0,0 +1,26 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+*/
+// Automatically generated file, DO NOT EDIT
+#include "kernel/expr.h"
+namespace lean {
+expr mk_if_true_fn();
+bool is_if_true_fn(expr const & e);
+inline expr mk_if_true_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_if_true_fn(), e1, e2, e3}); }
+expr mk_if_false_fn();
+bool is_if_false_fn(expr const & e);
+inline expr mk_if_false_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_if_false_fn(), e1, e2, e3}); }
+expr mk_if_a_a_fn();
+bool is_if_a_a_fn(expr const & e);
+inline expr mk_if_a_a_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_if_a_a_fn(), e1, e2, e3}); }
+expr mk_if_congr_fn();
+bool is_if_congr_fn(expr const & e);
+inline expr mk_if_congr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6, expr const & e7, expr const & e8, expr const & e9, expr const & e10) { return mk_app({mk_if_congr_fn(), e1, e2, e3, e4, e5, e6, e7, e8, e9, e10}); }
+expr mk_if_imp_then_fn();
+bool is_if_imp_then_fn(expr const & e);
+inline expr mk_if_imp_then_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_if_imp_then_fn(), e1, e2, e3, e4, e5}); }
+expr mk_if_imp_else_fn();
+bool is_if_imp_else_fn(expr const & e);
+inline expr mk_if_imp_else_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_if_imp_else_fn(), e1, e2, e3, e4, e5}); }
+}

src/library/ite.cpp

@@ -0,0 +1,55 @@
+/*
+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 "kernel/builtin.h"
+#include "kernel/abstract.h"
+#include "kernel/decl_macros.h"
+#include "library/if_then_else_decls.h"
+#include "library/if_then_else_decls.cpp"
+
+namespace lean {
+// =======================================
+// If-then-else builtin operator
+static name   g_if_name("ite");
+static format g_if_fmt(g_if_name);
+/**
+   \brief Semantic attachment for if-then-else operator with type
+   <code>Pi (A : Type), Bool -> A -> A -> A</code>
+*/
+class if_fn_value : public value {
+    expr m_type;
+    static expr mk_type() {
+        expr A    = Const("A");
+        // Pi (A: Type), bool -> A -> A -> A
+        return Pi({A, TypeU}, Bool >> (A >> (A >> A)));
+    }
+public:
+    if_fn_value():m_type(mk_type()) {}
+    virtual ~if_fn_value() {}
+    virtual expr get_type() const { return m_type; }
+    virtual name get_name() const { return g_if_name; }
+    virtual optional<expr> normalize(unsigned num_args, expr const * args) const {
+        if (num_args == 5 && is_bool_value(args[2]) && is_value(args[3]) && is_value(args[4])) {
+            if (to_bool(args[2]))
+                return some_expr(args[3]); // if A true a b  --> a
+            else
+                return some_expr(args[4]); // if A false a b --> b
+        } else {
+            return none_expr();
+        }
+    }
+    virtual void write(serializer & s) const { s << "ite"; }
+};
+MK_BUILTIN(if_fn, if_fn_value);
+MK_IS_BUILTIN(is_if_fn, mk_if_fn());
+static register_builtin_fn if_blt("ite", []() { return mk_if_fn(); });
+static value::register_deserializer_fn if_ds("ite", [](deserializer & ) { return mk_if_fn(); });
+// =======================================
+
+void import_ite(environment const & env, io_state const & ios) {
+    env->import("if_then_else", ios);
+}
+}

src/library/ite.h

@@ -0,0 +1,16 @@
+/*
+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 "kernel/io_state.h"
+#include "library/if_then_else_decls.h"
+
+namespace lean {
+expr mk_ite_fn();
+bool is_ite_fn(expr const & e);
+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);
+}