From 46a8300a2db6c026d5ed7f79a7bb6d1ab38e8669 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 30 Dec 2013 11:02:22 -0800
Subject: [PATCH] refactor(library/arith): move real and special function
 declarations to .lean files

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/builtin/CMakeLists.txt         |   7 +++-
 src/builtin/cast.olean             | Bin 912 -> 924 bytes
 src/builtin/int.lean               |  10 ++---
 src/builtin/nat.lean               |   6 +--
 src/builtin/real.lean              |  46 +++++++++++++++++++++
 src/builtin/real.olean             | Bin 0 -> 1219 bytes
 src/builtin/specialfn.lean         |  19 +++++++++
 src/builtin/specialfn.olean        | Bin 0 -> 1086 bytes
 src/frontends/lean/CMakeLists.txt  |   2 +-
 src/frontends/lean/frontend.cpp    |   1 -
 src/frontends/lean/notation.cpp    |  43 --------------------
 src/frontends/lean/notation.h      |   3 --
 src/library/arith/arith.cpp        |   1 -
 src/library/arith/int.cpp          |  10 ++---
 src/library/arith/real.cpp         |  62 +++++++++--------------------
 src/library/arith/special_fn.cpp   |  32 ++-------------
 tests/lean/elab4.lean.expected.out |   2 +
 tests/lean/elab5.lean.expected.out |   2 +
 18 files changed, 110 insertions(+), 136 deletions(-)
 create mode 100644 src/builtin/real.lean
 create mode 100644 src/builtin/real.olean
 create mode 100644 src/builtin/specialfn.lean
 create mode 100644 src/builtin/specialfn.olean
 delete mode 100644 src/frontends/lean/notation.cpp

diff --git a/src/builtin/CMakeLists.txt b/src/builtin/CMakeLists.txt
index e090fb9b8e..26eda236ce 100644
--- a/src/builtin/CMakeLists.txt
+++ b/src/builtin/CMakeLists.txt
@@ -71,8 +71,13 @@ add_kernel_theory("nat.lean")
 add_dependencies(nat_builtin basic_builtin)
 add_kernel_theory("int.lean")
 add_dependencies(int_builtin nat_builtin)
-add_dependencies(int_builtin basic_builtin)
+add_kernel_theory("real.lean")
+add_dependencies(real_builtin int_builtin)
+add_kernel_theory("specialfn.lean")
+add_dependencies(specialfn_builtin real_builtin)
 add_theory("cast.lean")
 # TODO(Leo): Remove the following dependencies after cleanup
 add_dependencies(cast_builtin nat_builtin)
 add_dependencies(cast_builtin int_builtin)
+add_dependencies(cast_builtin real_builtin)
+add_dependencies(cast_builtin specialfn_builtin)
diff --git a/src/builtin/cast.olean b/src/builtin/cast.olean
index c350c2f47d0986f16ee1c48370e255f661837d0c..59c5f21fcda532bfd1c5e813bfdfd7a42b0b3bce 100644
GIT binary patch
delta 22
dcmbQhK8JmRDYs{CL4HvQLs4pC&PJ0MW&l-k2W|iW

delta 10
RcmbQkK7oCL=|;zBW&jhr15f|}

diff --git a/src/builtin/int.lean b/src/builtin/int.lean
index c698519f45..31d925bb74 100644
--- a/src/builtin/int.lean
+++ b/src/builtin/int.lean
@@ -6,16 +6,16 @@ Alias ℤ : Int.
 
 Builtin Int::numeral.
 
-Builtin Int::add : Int -> Int -> Int.
+Builtin Int::add : Int → Int → Int.
 Infixl 65 + : Int::add.
 
-Builtin Int::mul : Int -> Int -> Int.
+Builtin Int::mul : Int → Int → Int.
 Infixl 70 * : Int::mul.
 
-Builtin Int::div : Int -> Int -> Int.
+Builtin Int::div : Int → Int → Int.
 Infixl 70 div : Int::div.
 
-Builtin Int::le : Int -> Int -> Bool.
+Builtin Int::le : Int → Int → Bool.
 Infix  50 <= : Int::le.
 Infix  50 ≤  : Int::le.
 
@@ -38,7 +38,7 @@ Notation 75 - _ : Int::neg.
 Definition Int::mod (a b : Int) : Int := a - b * (a div b).
 Infixl 70 mod : Int::mod.
 
-Builtin nat_to_int : Nat -> Int.
+Builtin nat_to_int : Nat → Int.
 Coercion nat_to_int.
 
 Definition Int::divides (a b : Int) : Bool := (b mod a) = 0.
diff --git a/src/builtin/nat.lean b/src/builtin/nat.lean
index a256c789b6..efaf7bef7e 100644
--- a/src/builtin/nat.lean
+++ b/src/builtin/nat.lean
@@ -5,13 +5,13 @@ Alias ℕ : Nat.
 
 Builtin Nat::numeral.
 
-Builtin Nat::add : Nat -> Nat -> Nat.
+Builtin Nat::add : Nat → Nat → Nat.
 Infixl 65 +  : Nat::add.
 
-Builtin Nat::mul : Nat -> Nat -> Nat.
+Builtin Nat::mul : Nat → Nat → Nat.
 Infixl 70 *  : Nat::mul.
 
-Builtin Nat::le  : Nat -> Nat -> Bool.
+Builtin Nat::le  : Nat → Nat → Bool.
 Infix  50 <= : Nat::le.
 Infix  50 ≤  : Nat::le.
 
diff --git a/src/builtin/real.lean b/src/builtin/real.lean
new file mode 100644
index 0000000000..63b606d090
--- /dev/null
+++ b/src/builtin/real.lean
@@ -0,0 +1,46 @@
+Import basic.
+Import nat.
+Import int.
+
+Variable Real : Type.
+Alias ℝ : Real.
+
+Builtin Real::numeral.
+
+Builtin Real::add : Real → Real → Real.
+Infixl 65 + : Real::add.
+
+Builtin Real::mul : Real → Real → Real.
+Infixl 70 * : Real::mul.
+
+Builtin Real::div : Real → Real → Real.
+Infixl 70 / : Real::div.
+
+Builtin Real::le : Real → Real → Bool.
+Infix  50 <= : Real::le.
+Infix  50 ≤  : Real::le.
+
+Definition Real::ge (a b : Real) : Bool := b ≤ a.
+Infix 50 >= : Real::ge.
+Infix 50 ≥  : Real::ge.
+
+Definition Real::lt (a b : Real) : Bool := ¬ (a ≥ b).
+Infix 50 <  : Real::lt.
+
+Definition Real::gt (a b : Real) : Bool := ¬ (a ≤ b).
+Infix 50 >  : Real::gt.
+
+Definition Real::sub (a b : Real) : Real := a + -1.0 * b.
+Infixl 65 - : Real::sub.
+
+Definition Real::neg (a : Real) : Real := -1.0 * a.
+Notation 75 - _ : Real::neg.
+
+Definition Real::abs (a : Real) : Real := if (0.0 ≤ a) a (- a).
+Notation 55 | _ | : Real::abs.
+
+Builtin int_to_real : Int → Real.
+Coercion int_to_real.
+
+Definition nat_to_real (a : Nat) : Real := int_to_real (nat_to_int a).
+Coercion nat_to_real.
diff --git a/src/builtin/real.olean b/src/builtin/real.olean
new file mode 100644
index 0000000000000000000000000000000000000000..5e94086d59768405e495b08cc0d560ad9fbc212b
GIT binary patch
literal 1219
zcma)+K}!Nb6vy9=riVP19y%0kR1|6j5tK=8B}AZ6&{bx2m4S69bnMizOCO?JeK9{t
z^WN_2&bmP&!yA47`Tgh3ypg`ggQ4&}h(6Z+_*G66xO^)55KRKE;!p$%UibvqlgE81
zTEJYXpydlb1vdZq0v0ah%!IE*@a!qbO)&KsqMyQfj}HdWk%}uJ1C&_oh_o%157)+o
zlx95hQ<_84v||k>q%;HZmeSNs4JM>Cx*Vpp#uZrF<7v#ndYKvX&+pZgTW<)_Zblvy
z7>}z{U@n!Z#F!(c_PmDE4ID}oZc@05<2sUQZOcS9Q>HXx#ng{!3R4oMe3fOYLPuB*
zJ#8brLY{Ugv>6NZi352nqc@8Tn%){FSA&w=Q6|?;a`zEt6Ze2Z8^^6>MY5<(ld3UE
z>U8F2ZMPQPSYp+XQlqd=Ap!HWO$rO)ZLXdWDpl{Qd4my{G!S^Bq=6*&3}F}lAz<P|
zd=GKOB!RorzX+EoboO#$hygfZCF9;)+%cd!w^ojnv3JnlqL!Y=bfhgiN52d`C41ED
zH`1H*qsE3V-Z-Y;kj3BB39O@EmAE0O;w?1xNCvugE)w8_Lv9vpQr)iME*P}&;ra!!
C6wSH-

literal 0
HcmV?d00001

diff --git a/src/builtin/specialfn.lean b/src/builtin/specialfn.lean
new file mode 100644
index 0000000000..acb71b2671
--- /dev/null
+++ b/src/builtin/specialfn.lean
@@ -0,0 +1,19 @@
+Import real.
+
+Variable exp : Real → Real.
+Variable log : Real → Real.
+Variable pi  : Real.
+Alias π : pi.
+
+Variable sin : Real → Real.
+Definition cos x := sin (x - π / 2).
+Definition tan x := sin x / cos x.
+Definition cot x := cos x / sin x.
+Definition sec x := 1 / cos x.
+Definition csc x := 1 / sin x.
+Definition sinh x := (1 - exp (-2 * x)) / (2 * exp (- x)).
+Definition cosh x := (1 + exp (-2 * x)) / (2 * exp (- x)).
+Definition tanh x := sinh x / cosh x.
+Definition coth x := cosh x / sinh x.
+Definition sech x := 1 / cosh x.
+Definition csch x := 1 / sinh x.
diff --git a/src/builtin/specialfn.olean b/src/builtin/specialfn.olean
new file mode 100644
index 0000000000000000000000000000000000000000..4c47160c6f310fa8e2d1f4915cfcd67969451a16
GIT binary patch
literal 1086
zcma)+!Ab)$5Qe9zbz2K!L8N+7*dii$urFW*74+!AYl*vQUD)oHW-C4VhQ5-SnWRlH
zh<gahO#W~FNy65plGUsz71*!!yja$&23AUz@FrIv)Mg3$LV^&l7z2Sj1?S3o&N+_x
zsb%4I-j{{cAilpi&|#@As)+PK%|K+eHmQx%BfHnZ@c@T@N@Wrli9NQY*Y5x=%xyz?
z@ri4IBo(5P&9tef)DpDK3dTT%8i^h@w6W{@qe=sebw@ZJxq4KA7d<X#-8NfD9|c1q
z9OJa_6Raq}5kadgMmX^aI3JMrTZnkjJ3<$?vWFo~T^BeH35nN*xsH#m3DPm*3}r)Z
zgT}-3H^@8q#o9cPv|UuYBgX~YjO`7f`p#pFZ97Kg?z2*Jd!Oz(M6F#Q%2{(-ndgRt
znXp%55rbTL@^4G1d7+DU4<>4b*wzZ)&MCLci*xUwv$}~QF0oXAu&RLP-b)m5<s)z&
W9zozjXHmrU-w4~)W0gPQKjR0)esYEY

literal 0
HcmV?d00001

diff --git a/src/frontends/lean/CMakeLists.txt b/src/frontends/lean/CMakeLists.txt
index 7c9d2dd4b5..df5a1cd4e8 100644
--- a/src/frontends/lean/CMakeLists.txt
+++ b/src/frontends/lean/CMakeLists.txt
@@ -1,3 +1,3 @@
 add_library(lean_frontend frontend.cpp operator_info.cpp scanner.cpp parser.cpp pp.cpp
-  notation.cpp frontend_elaborator.cpp register_module.cpp environment_scope.cpp coercion.cpp)
+  frontend_elaborator.cpp register_module.cpp environment_scope.cpp coercion.cpp)
 target_link_libraries(lean_frontend ${LEAN_LIBS})
diff --git a/src/frontends/lean/frontend.cpp b/src/frontends/lean/frontend.cpp
index 3a856b6745..d6e06aeccc 100644
--- a/src/frontends/lean/frontend.cpp
+++ b/src/frontends/lean/frontend.cpp
@@ -561,7 +561,6 @@ void init_frontend(environment const & env, io_state & ios, bool kernel_only) {
     ios.set_formatter(mk_pp_formatter(env));
     if (!kernel_only)
         import_all(env);
-    init_builtin_notation(env, ios, kernel_only);
 }
 void init_frontend(environment const & env) {
     io_state ios;
diff --git a/src/frontends/lean/notation.cpp b/src/frontends/lean/notation.cpp
deleted file mode 100644
index db92a688ea..0000000000
--- a/src/frontends/lean/notation.cpp
+++ /dev/null
@@ -1,43 +0,0 @@
-/*
-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 "library/basic_thms.h"
-#include "library/arith/arith.h"
-#include "frontends/lean/frontend.h"
-
-namespace lean {
-/**
-   \brief Initialize builtin notation.
-*/
-void init_builtin_notation(environment const & env, io_state & ios, bool kernel_only) {
-    env->import_builtin(
-        "lean_notation",
-        [&]() {
-            // mark_implicit_arguments(env, mk_if_fn(), 1);
-
-            if (kernel_only)
-                return;
-
-            add_alias(env, "ℝ", Real);
-            add_infixl(env, ios, "+", 65, mk_real_add_fn());
-            add_infixl(env, ios, "-", 65, mk_real_sub_fn());
-            add_prefix(env, ios, "-", 75, mk_real_neg_fn());
-            add_infixl(env, ios, "*", 70, mk_real_mul_fn());
-            add_infixl(env, ios, "/", 70, mk_real_div_fn());
-            add_mixfixc(env, ios, {"|", "|"}, 55, mk_real_abs_fn());
-            add_infix(env, ios, "<=", 50, mk_real_le_fn());
-            add_infix(env, ios, "\u2264", 50, mk_real_le_fn());  // ≤
-            add_infix(env, ios, ">=", 50, mk_real_ge_fn());
-            add_infix(env, ios, "\u2265", 50, mk_real_ge_fn());  // ≥
-            add_infix(env, ios, "<", 50, mk_real_lt_fn());
-            add_infix(env, ios, ">", 50, mk_real_gt_fn());
-
-            add_coercion(env, mk_int_to_real_fn());
-            add_coercion(env, mk_nat_to_real_fn());
-        });
-}
-}
diff --git a/src/frontends/lean/notation.h b/src/frontends/lean/notation.h
index 258fe83d63..6c3cd0f826 100644
--- a/src/frontends/lean/notation.h
+++ b/src/frontends/lean/notation.h
@@ -10,7 +10,4 @@ namespace lean {
 constexpr unsigned g_eq_precedence    = 50;
 constexpr unsigned g_arrow_precedence = 25;
 constexpr unsigned g_app_precedence   = std::numeric_limits<unsigned>::max();
-class environment;
-class io_state;
-void init_builtin_notation(environment const & env, io_state & st, bool kernel_only = false);
 }
diff --git a/src/library/arith/arith.cpp b/src/library/arith/arith.cpp
index 965fc69eb6..67afab7a90 100644
--- a/src/library/arith/arith.cpp
+++ b/src/library/arith/arith.cpp
@@ -11,7 +11,6 @@ void import_arith(environment const & env) {
     import_nat(env);
     import_int(env);
     import_real(env);
-    import_int_to_real_coercions(env);
     import_special_fn(env);
 }
 }
diff --git a/src/library/arith/int.cpp b/src/library/arith/int.cpp
index 53bce6d82d..2af312c887 100644
--- a/src/library/arith/int.cpp
+++ b/src/library/arith/int.cpp
@@ -52,7 +52,7 @@ expr mk_int_value(mpz const & v) {
 }
 expr read_int_value(deserializer & d) { return mk_int_value(read_mpz(d)); }
 static value::register_deserializer_fn int_value_ds("int", read_int_value);
-register_available_builtin_fn g_int_value(name({"Int", "numeral"}), []() { return mk_int_value(mpz(0)); }, true);
+static register_available_builtin_fn g_int_value(name({"Int", "numeral"}), []() { return mk_int_value(mpz(0)); }, true);
 
 bool is_int_value(expr const & e) {
     return is_value(e) && dynamic_cast<int_value_value const *>(&to_value(e)) != nullptr;
@@ -87,7 +87,7 @@ typedef int_bin_op<int_add_name, int_add_eval> int_add_value;
 MK_BUILTIN(int_add_fn, int_add_value);
 expr read_int_add(deserializer & ) { return mk_int_add_fn(); }
 static value::register_deserializer_fn int_add_ds("int_add", read_int_add);
-register_available_builtin_fn g_int_add_value(name({"Int", "add"}), []() { return mk_int_add_fn(); });
+static register_available_builtin_fn g_int_add_value(name({"Int", "add"}), []() { return mk_int_add_fn(); });
 
 constexpr char int_mul_name[] = "mul";
 struct int_mul_eval { mpz operator()(mpz const & v1, mpz const & v2) { return v1 * v2; }; };
@@ -95,7 +95,7 @@ typedef int_bin_op<int_mul_name, int_mul_eval> int_mul_value;
 MK_BUILTIN(int_mul_fn, int_mul_value);
 expr read_int_mul(deserializer & ) { return mk_int_mul_fn(); }
 static value::register_deserializer_fn int_mul_ds("int_mul", read_int_mul);
-register_available_builtin_fn g_int_mul_value(name({"Int", "mul"}), []() { return mk_int_mul_fn(); });
+static register_available_builtin_fn g_int_mul_value(name({"Int", "mul"}), []() { return mk_int_mul_fn(); });
 
 constexpr char int_div_name[] = "div";
 struct int_div_eval {
@@ -110,7 +110,7 @@ typedef int_bin_op<int_div_name, int_div_eval> int_div_value;
 MK_BUILTIN(int_div_fn, int_div_value);
 expr read_int_div(deserializer & ) { return mk_int_div_fn(); }
 static value::register_deserializer_fn int_div_ds("int_div", read_int_div);
-register_available_builtin_fn g_int_div_value(name({"Int", "div"}), []() { return mk_int_div_fn(); });
+static register_available_builtin_fn g_int_div_value(name({"Int", "div"}), []() { return mk_int_div_fn(); });
 
 class int_le_value : public const_value {
 public:
@@ -127,7 +127,7 @@ public:
 MK_BUILTIN(int_le_fn, int_le_value);
 expr read_int_le(deserializer & ) { return mk_int_le_fn(); }
 static value::register_deserializer_fn int_le_ds("int_le", read_int_le);
-register_available_builtin_fn g_int_le_value(name({"Int", "le"}), []() { return mk_int_le_fn(); });
+static register_available_builtin_fn g_int_le_value(name({"Int", "le"}), []() { return mk_int_le_fn(); });
 
 MK_CONSTANT(int_sub_fn, name({"Int", "sub"}));
 MK_CONSTANT(int_neg_fn, name({"Int", "neg"}));
diff --git a/src/library/arith/real.cpp b/src/library/arith/real.cpp
index be8d56b7b3..8d9b765b6f 100644
--- a/src/library/arith/real.cpp
+++ b/src/library/arith/real.cpp
@@ -9,6 +9,7 @@ Author: Leonardo de Moura
 #include "kernel/environment.h"
 #include "kernel/value.h"
 #include "library/kernel_bindings.h"
+#include "library/io_state.h"
 #include "library/arith/real.h"
 #include "library/arith/int.h"
 #include "library/arith/nat.h"
@@ -57,6 +58,7 @@ expr mk_real_value(mpq const & v) {
 }
 expr read_real_value(deserializer & d) { return mk_real_value(read_mpq(d)); }
 static value::register_deserializer_fn real_value_ds("real", read_real_value);
+static register_available_builtin_fn g_real_value(name({"Real", "numeral"}), []() { return mk_real_value(mpq(0)); }, true);
 
 bool is_real_value(expr const & e) {
     return is_value(e) && dynamic_cast<real_value_value const *>(&to_value(e)) != nullptr;
@@ -92,6 +94,8 @@ typedef real_bin_op<real_add_name, real_add_eval> real_add_value;
 MK_BUILTIN(real_add_fn, real_add_value);
 expr read_real_add(deserializer & ) { return mk_real_add_fn(); }
 static value::register_deserializer_fn real_add_ds("real_add", read_real_add);
+static register_available_builtin_fn g_real_add_value(name({"Real", "add"}), []() { return mk_real_add_fn(); });
+
 
 constexpr char real_mul_name[] = "mul";
 /** \brief Evaluator for * : Real -> Real -> Real */
@@ -100,6 +104,7 @@ typedef real_bin_op<real_mul_name, real_mul_eval> real_mul_value;
 MK_BUILTIN(real_mul_fn, real_mul_value);
 expr read_real_mul(deserializer & ) { return mk_real_mul_fn(); }
 static value::register_deserializer_fn real_mul_ds("real_mul", read_real_mul);
+static register_available_builtin_fn g_real_mul_value(name({"Real", "mul"}), []() { return mk_real_mul_fn(); });
 
 constexpr char real_div_name[] = "div";
 /** \brief Evaluator for / : Real -> Real -> Real */
@@ -115,6 +120,7 @@ typedef real_bin_op<real_div_name, real_div_eval> real_div_value;
 MK_BUILTIN(real_div_fn, real_div_value);
 expr read_real_div(deserializer & ) { return mk_real_div_fn(); }
 static value::register_deserializer_fn real_div_ds("real_div", read_real_div);
+static register_available_builtin_fn g_real_div_value(name({"Real", "div"}), []() { return mk_real_div_fn(); });
 
 /**
    \brief Semantic attachment for less than or equal to operator with type
@@ -135,39 +141,7 @@ public:
 MK_BUILTIN(real_le_fn, real_le_value);
 expr read_real_le(deserializer & ) { return mk_real_le_fn(); }
 static value::register_deserializer_fn real_le_ds("real_le", read_real_le);
-
-MK_CONSTANT(real_sub_fn, name({"Real", "sub"}));
-MK_CONSTANT(real_neg_fn, name({"Real", "neg"}));
-MK_CONSTANT(real_abs_fn, name({"Real", "abs"}));
-MK_CONSTANT(real_ge_fn, name({"Real", "ge"}));
-MK_CONSTANT(real_lt_fn, name({"Real", "lt"}));
-MK_CONSTANT(real_gt_fn, name({"Real", "gt"}));
-
-void import_real(environment const & env) {
-    env->import_builtin(
-        "real",
-        [&]() {
-            expr rr_b = Real >> (Real >> Bool);
-            expr rr_r = Real >> (Real >> Real);
-            expr r_r  = Real >> Real;
-            expr x    = Const("x");
-            expr y    = Const("y");
-
-            env->add_var(Real_name, Type());
-            env->add_builtin_set(rVal(0));
-            env->add_builtin(mk_real_add_fn());
-            env->add_builtin(mk_real_mul_fn());
-            env->add_builtin(mk_real_div_fn());
-            env->add_builtin(mk_real_le_fn());
-
-            env->add_opaque_definition(real_sub_fn_name, rr_r, Fun({{x, Real}, {y, Real}}, rAdd(x, rMul(rVal(-1), y))));
-            env->add_opaque_definition(real_neg_fn_name, r_r,  Fun({x, Real}, rMul(rVal(-1), x)));
-            env->add_opaque_definition(real_abs_fn_name, r_r,  Fun({x, Real}, rIf(rLe(rVal(0), x), x, rNeg(x))));
-            env->add_opaque_definition(real_ge_fn_name, rr_b,  Fun({{x, Real}, {y, Real}}, rLe(y, x)));
-            env->add_opaque_definition(real_lt_fn_name, rr_b,  Fun({{x, Real}, {y, Real}}, Not(rLe(y, x))));
-            env->add_opaque_definition(real_gt_fn_name, rr_b,  Fun({{x, Real}, {y, Real}}, Not(rLe(x, y))));
-        });
-}
+static register_available_builtin_fn g_real_le_value(name({"Real", "le"}), []() { return mk_real_le_fn(); });
 
 class int_to_real_value : public const_value {
 public:
@@ -184,19 +158,19 @@ public:
 MK_BUILTIN(int_to_real_fn,  int_to_real_value);
 expr read_int_to_real(deserializer & ) { return mk_int_to_real_fn(); }
 static value::register_deserializer_fn int_to_real_ds("int_to_real", read_int_to_real);
+static register_available_builtin_fn g_int_to_real_value("int_to_real", []() { return mk_int_to_real_fn(); });
+
+MK_CONSTANT(real_sub_fn, name({"Real", "sub"}));
+MK_CONSTANT(real_neg_fn, name({"Real", "neg"}));
+MK_CONSTANT(real_abs_fn, name({"Real", "abs"}));
+MK_CONSTANT(real_ge_fn, name({"Real", "ge"}));
+MK_CONSTANT(real_lt_fn, name({"Real", "lt"}));
+MK_CONSTANT(real_gt_fn, name({"Real", "gt"}));
 MK_CONSTANT(nat_to_real_fn, name("nat_to_real"));
 
-void import_int_to_real_coercions(environment const & env) {
-    env->import_builtin(
-        "real_coercions",
-        [&]() {
-            import_int(env);
-            import_real(env);
-
-            env->add_builtin(mk_int_to_real_fn());
-            expr x    = Const("x");
-            env->add_opaque_definition(nat_to_real_fn_name, Nat >> Real, Fun({x, Nat}, i2r(n2i(x))));
-        });
+void import_real(environment const & env) {
+    io_state ios;
+    env->import("real", ios);
 }
 
 static int mk_real_value(lua_State * L) {
diff --git a/src/library/arith/special_fn.cpp b/src/library/arith/special_fn.cpp
index 223ff2a800..80aa52ed3e 100644
--- a/src/library/arith/special_fn.cpp
+++ b/src/library/arith/special_fn.cpp
@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #include "kernel/environment.h"
 #include "kernel/abstract.h"
+#include "library/io_state.h"
 #include "library/arith/special_fn.h"
 #include "library/arith/real.h"
 
@@ -29,34 +30,7 @@ MK_CONSTANT(sech_fn, name("sech"));
 MK_CONSTANT(csch_fn, name("csch"));
 
 void import_special_fn(environment const & env) {
-    env->import_builtin(
-        "special_fn",
-        [&]() {
-            import_real(env);
-
-            expr r_r  = Real >> Real;
-            expr x    = Const("x");
-
-            env->add_var(exp_fn_name, r_r);
-            env->add_var(log_fn_name, r_r);
-
-            env->add_var(real_pi_name, Real);
-            env->add_definition(name("pi"), Real, mk_real_pi()); // alias for pi
-            env->add_var(sin_fn_name, r_r);
-            env->add_opaque_definition(cos_fn_name, r_r, Fun({x, Real}, Sin(rSub(x, rDiv(mk_real_pi(), rVal(2))))));
-            env->add_opaque_definition(tan_fn_name, r_r, Fun({x, Real}, rDiv(Sin(x), Cos(x))));
-            env->add_opaque_definition(cot_fn_name, r_r, Fun({x, Real}, rDiv(Cos(x), Sin(x))));
-            env->add_opaque_definition(sec_fn_name, r_r, Fun({x, Real}, rDiv(rVal(1), Cos(x))));
-            env->add_opaque_definition(csc_fn_name, r_r, Fun({x, Real}, rDiv(rVal(1), Sin(x))));
-
-            env->add_opaque_definition(sinh_fn_name, r_r, Fun({x, Real}, rDiv(rSub(rVal(1), Exp(rMul(rVal(-2), x))),
-                                                                              rMul(rVal(2), Exp(rNeg(x))))));
-            env->add_opaque_definition(cosh_fn_name, r_r, Fun({x, Real}, rDiv(rAdd(rVal(1), Exp(rMul(rVal(-2), x))),
-                                                                              rMul(rVal(2), Exp(rNeg(x))))));
-            env->add_opaque_definition(tanh_fn_name, r_r, Fun({x, Real}, rDiv(Sinh(x), Cosh(x))));
-            env->add_opaque_definition(coth_fn_name, r_r, Fun({x, Real}, rDiv(Cosh(x), Sinh(x))));
-            env->add_opaque_definition(sech_fn_name, r_r, Fun({x, Real}, rDiv(rVal(1), Cosh(x))));
-            env->add_opaque_definition(csch_fn_name, r_r, Fun({x, Real}, rDiv(rVal(1), Sinh(x))));
-        });
+    io_state ios;
+    env->import("specialfn", ios);
 }
 }
diff --git a/tests/lean/elab4.lean.expected.out b/tests/lean/elab4.lean.expected.out
index 3b8d3ca0c8..18768da3e7 100644
--- a/tests/lean/elab4.lean.expected.out
+++ b/tests/lean/elab4.lean.expected.out
@@ -8,6 +8,8 @@
 Import "basic"
 Import "nat"
 Import "int"
+Import "real"
+Import "specialfn"
 Variable C {A B : Type} (H : @eq Type A B) (a : A) : B
 Variable D {A A' : Type} {B : A → Type} {B' : A' → Type} (H : @eq Type (Π x : A, B x) (Π x : A', B' x)) :
     @eq Type A A'
diff --git a/tests/lean/elab5.lean.expected.out b/tests/lean/elab5.lean.expected.out
index 3b8d3ca0c8..18768da3e7 100644
--- a/tests/lean/elab5.lean.expected.out
+++ b/tests/lean/elab5.lean.expected.out
@@ -8,6 +8,8 @@
 Import "basic"
 Import "nat"
 Import "int"
+Import "real"
+Import "specialfn"
 Variable C {A B : Type} (H : @eq Type A B) (a : A) : B
 Variable D {A A' : Type} {B : A → Type} {B' : A' → Type} (H : @eq Type (Π x : A, B x) (Π x : A', B' x)) :
     @eq Type A A'