From 07059b0531352ada86d4130d46d34c12748ae017 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 14 Jan 2014 16:10:49 -0800 Subject: [PATCH] feat(library): add if_then_else Lean/C++ interface Signed-off-by: Leonardo de Moura --- src/builtin/CMakeLists.txt | 9 ++--- src/builtin/if_then_else.lean | 13 +++++++ src/builtin/obj/if_then_else.olean | Bin 2143 -> 3020 bytes src/kernel/builtin.cpp | 38 -------------------- src/library/CMakeLists.txt | 2 +- src/library/if_then_else_decls.cpp | 15 ++++++++ src/library/if_then_else_decls.h | 26 ++++++++++++++ src/library/ite.cpp | 55 +++++++++++++++++++++++++++++ src/library/ite.h | 16 +++++++++ 9 files changed, 131 insertions(+), 43 deletions(-) create mode 100644 src/library/if_then_else_decls.cpp create mode 100644 src/library/if_then_else_decls.h create mode 100644 src/library/ite.cpp create mode 100644 src/library/ite.h diff --git a/src/builtin/CMakeLists.txt b/src/builtin/CMakeLists.txt index 2670aca66..16dd5d3e3 100644 --- a/src/builtin/CMakeLists.txt +++ b/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" "") \ No newline at end of file +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" "") \ No newline at end of file diff --git a/src/builtin/if_then_else.lean b/src/builtin/if_then_else.lean index ad5f76853..a7a9a03ef 100644 --- a/src/builtin/if_then_else.lean +++ b/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 \ No newline at end of file diff --git a/src/builtin/obj/if_then_else.olean b/src/builtin/obj/if_then_else.olean index 438a5a495bfa486c8d7a0548a8cd794c224e5f01..b6f6a6011050eb3e886484842bb0b94bf1a4b701 100644 GIT binary patch delta 878 zcmZ`&Jxjw-6un8>v`ay#AZ8H3S_EDE8vGg@)H*(Zd|lKR^PafTLl`AlnDNO!38_kw06)_BSVT1RQG$T%CKNY$SlAcgRpUQrWZ+=gQar0MMSO2MUCC*8D Je;UO~egR1*JkS6D delta 26 hcmX>jeqUgNFNctSK_UZFW=SdoqibG@TV_rw0|0Ze2j&0( diff --git a/src/kernel/builtin.cpp b/src/kernel/builtin.cpp index ffb33a973..1da2866fd 100644 --- a/src/kernel/builtin.cpp +++ b/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 - Pi (A : Type), Bool -> A -> A -> A -*/ -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 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); } diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index 142aea695..687d75052 100644 --- a/src/library/CMakeLists.txt +++ b/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}) diff --git a/src/library/if_then_else_decls.cpp b/src/library/if_then_else_decls.cpp new file mode 100644 index 000000000..57c5b08dc --- /dev/null +++ b/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")); +} diff --git a/src/library/if_then_else_decls.h b/src/library/if_then_else_decls.h new file mode 100644 index 000000000..cc511ccca --- /dev/null +++ b/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}); } +} diff --git a/src/library/ite.cpp b/src/library/ite.cpp new file mode 100644 index 000000000..e171635e8 --- /dev/null +++ b/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 + Pi (A : Type), Bool -> A -> A -> A +*/ +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 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); +} +} diff --git a/src/library/ite.h b/src/library/ite.h new file mode 100644 index 000000000..14e47891d --- /dev/null +++ b/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); +}