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

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

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.

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.
 

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.

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.

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

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;

src/frontends/lean/notation.cpp

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

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

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

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

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

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

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'

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'