michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(kernel): export/import (.olean) binary files

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-12-28 17:31:35 -08:00
parent 22bebbf242
commit aee1c6d3f3
23 changed files with 699 additions and 507 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/CMakeLists.txt
View file

@ -189,6 +189,8 @@ FOREACH(FILE ${LEANLIB})
ENDFOREACH(FILE)
include_directories(${LEAN_SOURCE_DIR})
configure_file("${LEAN_SOURCE_DIR}/version.h.in" "${LEAN_BINARY_DIR}/version.h")
include_directories("${LEAN_BINARY_DIR}")
add_subdirectory(util)
set(LEAN_LIBS ${LEAN_LIBS} util)

28
src/frontends/lean/frontend.cpp
View file

@ -78,19 +78,9 @@ struct lean_extension : public environment_extension {
coercion_map m_coercion_map; // mapping from (given_type, expected_type) -> coercion
coercion_set m_coercion_set; // Set of coercions
expr_to_coercions m_type_coercions; // mapping type -> list (to-type, function)
unsigned m_initial_size; // size of the environment after init_frontend was invoked
name_set m_explicit_names; // set of explicit version of constants with implicit parameters
lean_extension() {
m_initial_size = 0;
}
void set_initial_size(unsigned sz) {
m_initial_size = sz;
}
unsigned get_initial_size() const {
return m_initial_size;
}
lean_extension const * get_parent() const {
@ -373,11 +363,14 @@ struct lean_extension : public environment_extension {
m_implicit_table[n] = mk_pair(v, explicit_version);
expr body = mk_explicit_definition_body(type, n, 0, num_args);
m_explicit_names.insert(explicit_version);
if (obj.is_axiom() || obj.is_theorem()) {
env->add_theorem(explicit_version, type, body);
} else {
env->add_definition(explicit_version, type, body);
}
env->add_neutral_object(new mark_implicit_command(n, sz, implicit));
env->auxiliary_section([&]() {
if (obj.is_axiom() || obj.is_theorem()) {
env->add_theorem(explicit_version, type, body);
} else {
env->add_definition(explicit_version, type, body);
}
});
}
bool has_implicit_arguments(name const & n) const {
@ -530,11 +523,6 @@ void init_frontend(environment const & env, io_state & ios) {
ios.set_formatter(mk_pp_formatter(env));
import_all(env);
init_builtin_notation(env, ios);
to_ext(env).set_initial_size(env->get_num_objects(false));
}
unsigned get_initial_size(ro_environment const & env) {
return to_ext(env).get_initial_size();
}
void add_infix(environment const & env, io_state const & ios, name const & opn, unsigned p, expr const & d) {

6
src/frontends/lean/frontend.h
View file

@ -18,12 +18,6 @@ namespace lean {
*/
void init_frontend(environment const & env, io_state & ios);
/**
\brief Return the environment size after init_frontend invocation.
Return 0 if \c init_frontend was not invoked for this environment.
*/
unsigned get_initial_size(ro_environment const & env);
/**
@name Notation for parsing and pretty printing.
*/

190
src/frontends/lean/notation.cpp
View file

@ -19,106 +19,108 @@ void add_alias(environment const & env, name const & n, name const & m) {
\brief Initialize builtin notation.
*/
void init_builtin_notation(environment const & env, io_state & ios) {
if (!env->mark_builtin_imported("lean_notation"))
return;
add_infix(env, ios, "=", 50, mk_homo_eq_fn());
mark_implicit_arguments(env, mk_homo_eq_fn(), 1);
mark_implicit_arguments(env, mk_if_fn(), 1);
env->import_builtin(
"lean_notation",
[&]() {
add_infix(env, ios, "=", 50, mk_homo_eq_fn());
mark_implicit_arguments(env, mk_homo_eq_fn(), 1);
mark_implicit_arguments(env, mk_if_fn(), 1);
add_prefix(env, ios, "\u00ac", 40, mk_not_fn()); // "¬"
add_infixr(env, ios, "&&", 35, mk_and_fn()); // "&&"
add_infixr(env, ios, "/\\", 35, mk_and_fn()); // "/\"
add_infixr(env, ios, "\u2227", 35, mk_and_fn()); // "∧"
add_infixr(env, ios, "||", 30, mk_or_fn()); // "||"
add_infixr(env, ios, "\\/", 30, mk_or_fn()); // "\/"
add_infixr(env, ios, "\u2228", 30, mk_or_fn()); // "∨"
add_infixr(env, ios, "=>", 25, mk_implies_fn()); // "=>"
add_infixr(env, ios, "\u21D2", 25, mk_implies_fn()); // "⇒"
add_infixr(env, ios, "<=>", 25, mk_iff_fn()); // "<=>"
add_infixr(env, ios, "\u21D4", 25, mk_iff_fn()); // "⇔"
add_prefix(env, ios, "\u00ac", 40, mk_not_fn()); // "¬"
add_infixr(env, ios, "&&", 35, mk_and_fn()); // "&&"
add_infixr(env, ios, "/\\", 35, mk_and_fn()); // "/\"
add_infixr(env, ios, "\u2227", 35, mk_and_fn()); // "∧"
add_infixr(env, ios, "||", 30, mk_or_fn()); // "||"
add_infixr(env, ios, "\\/", 30, mk_or_fn()); // "\/"
add_infixr(env, ios, "\u2228", 30, mk_or_fn()); // "∨"
add_infixr(env, ios, "=>", 25, mk_implies_fn()); // "=>"
add_infixr(env, ios, "\u21D2", 25, mk_implies_fn()); // "⇒"
add_infixr(env, ios, "<=>", 25, mk_iff_fn()); // "<=>"
add_infixr(env, ios, "\u21D4", 25, mk_iff_fn()); // "⇔"
add_infixl(env, ios, "+", 65, mk_nat_add_fn());
add_infixl(env, ios, "-", 65, mk_nat_sub_fn());
add_prefix(env, ios, "-", 75, mk_nat_neg_fn());
add_infixl(env, ios, "*", 70, mk_nat_mul_fn());
add_infix(env, ios, "<=", 50, mk_nat_le_fn());
add_infix(env, ios, "\u2264", 50, mk_nat_le_fn()); // ≤
add_infix(env, ios, ">=", 50, mk_nat_ge_fn());
add_infix(env, ios, "\u2265", 50, mk_nat_ge_fn()); // ≥
add_infix(env, ios, "<", 50, mk_nat_lt_fn());
add_infix(env, ios, ">", 50, mk_nat_gt_fn());
add_mixfixc(env, ios, {"|", "|"}, 55, mk_nat_id_fn()); // absolute value for naturals is the identity function
add_infixl(env, ios, "+", 65, mk_nat_add_fn());
add_infixl(env, ios, "-", 65, mk_nat_sub_fn());
add_prefix(env, ios, "-", 75, mk_nat_neg_fn());
add_infixl(env, ios, "*", 70, mk_nat_mul_fn());
add_infix(env, ios, "<=", 50, mk_nat_le_fn());
add_infix(env, ios, "\u2264", 50, mk_nat_le_fn()); // ≤
add_infix(env, ios, ">=", 50, mk_nat_ge_fn());
add_infix(env, ios, "\u2265", 50, mk_nat_ge_fn()); // ≥
add_infix(env, ios, "<", 50, mk_nat_lt_fn());
add_infix(env, ios, ">", 50, mk_nat_gt_fn());
add_mixfixc(env, ios, {"|", "|"}, 55, mk_nat_id_fn()); // absolute value for naturals is the identity function
add_infixl(env, ios, "+", 65, mk_int_add_fn());
add_infixl(env, ios, "-", 65, mk_int_sub_fn());
add_prefix(env, ios, "-", 75, mk_int_neg_fn());
add_infixl(env, ios, "*", 70, mk_int_mul_fn());
add_infixl(env, ios, "div", 70, mk_int_div_fn());
add_infixl(env, ios, "mod", 70, mk_int_mod_fn());
add_infix(env, ios, "|", 50, mk_int_divides_fn());
add_mixfixc(env, ios, {"|", "|"}, 55, mk_int_abs_fn());
add_infix(env, ios, "<=", 50, mk_int_le_fn());
add_infix(env, ios, "\u2264", 50, mk_int_le_fn()); // ≤
add_infix(env, ios, ">=", 50, mk_int_ge_fn());
add_infix(env, ios, "\u2265", 50, mk_int_ge_fn()); // ≥
add_infix(env, ios, "<", 50, mk_int_lt_fn());
add_infix(env, ios, ">", 50, mk_int_gt_fn());
add_infixl(env, ios, "+", 65, mk_int_add_fn());
add_infixl(env, ios, "-", 65, mk_int_sub_fn());
add_prefix(env, ios, "-", 75, mk_int_neg_fn());
add_infixl(env, ios, "*", 70, mk_int_mul_fn());
add_infixl(env, ios, "div", 70, mk_int_div_fn());
add_infixl(env, ios, "mod", 70, mk_int_mod_fn());
add_infix(env, ios, "|", 50, mk_int_divides_fn());
add_mixfixc(env, ios, {"|", "|"}, 55, mk_int_abs_fn());
add_infix(env, ios, "<=", 50, mk_int_le_fn());
add_infix(env, ios, "\u2264", 50, mk_int_le_fn()); // ≤
add_infix(env, ios, ">=", 50, mk_int_ge_fn());
add_infix(env, ios, "\u2265", 50, mk_int_ge_fn()); // ≥
add_infix(env, ios, "<", 50, mk_int_lt_fn());
add_infix(env, ios, ">", 50, mk_int_gt_fn());
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_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_nat_to_int_fn());
add_coercion(env, mk_int_to_real_fn());
add_coercion(env, mk_nat_to_real_fn());
add_coercion(env, mk_nat_to_int_fn());
add_coercion(env, mk_int_to_real_fn());
add_coercion(env, mk_nat_to_real_fn());
// implicit arguments for builtin axioms
mark_implicit_arguments(env, mk_mp_fn(), 2);
mark_implicit_arguments(env, mk_discharge_fn(), 2);
mark_implicit_arguments(env, mk_refl_fn(), 1);
mark_implicit_arguments(env, mk_subst_fn(), 4);
add_alias(env, "Subst", "SubstP");
mark_implicit_arguments(env, "SubstP", 3);
mark_implicit_arguments(env, mk_eta_fn(), 2);
mark_implicit_arguments(env, mk_abst_fn(), 4);
mark_implicit_arguments(env, mk_imp_antisym_fn(), 2);
mark_implicit_arguments(env, mk_hsymm_fn(), 4);
mark_implicit_arguments(env, mk_htrans_fn(), 6);
// implicit arguments for builtin axioms
mark_implicit_arguments(env, mk_mp_fn(), 2);
mark_implicit_arguments(env, mk_discharge_fn(), 2);
mark_implicit_arguments(env, mk_refl_fn(), 1);
mark_implicit_arguments(env, mk_subst_fn(), 4);
add_alias(env, "Subst", "SubstP");
mark_implicit_arguments(env, "SubstP", 3);
mark_implicit_arguments(env, mk_eta_fn(), 2);
mark_implicit_arguments(env, mk_abst_fn(), 4);
mark_implicit_arguments(env, mk_imp_antisym_fn(), 2);
mark_implicit_arguments(env, mk_hsymm_fn(), 4);
mark_implicit_arguments(env, mk_htrans_fn(), 6);
// implicit arguments for basic theorems
mark_implicit_arguments(env, mk_absurd_fn(), 1);
mark_implicit_arguments(env, mk_double_neg_elim_fn(), 1);
mark_implicit_arguments(env, mk_mt_fn(), 2);
mark_implicit_arguments(env, mk_contrapos_fn(), 2);
mark_implicit_arguments(env, mk_eq_mp_fn(), 2);
mark_implicit_arguments(env, mk_not_imp1_fn(), 2);
mark_implicit_arguments(env, mk_not_imp2_fn(), 2);
mark_implicit_arguments(env, mk_conj_fn(), 2);
mark_implicit_arguments(env, mk_conjunct1_fn(), 2);
mark_implicit_arguments(env, mk_conjunct2_fn(), 2);
mark_implicit_arguments(env, mk_disj1_fn(), 1);
mark_implicit_arguments(env, mk_disj2_fn(), 1);
mark_implicit_arguments(env, mk_disj_cases_fn(), 3);
mark_implicit_arguments(env, mk_refute_fn(), 1);
mark_implicit_arguments(env, mk_symm_fn(), 3);
mark_implicit_arguments(env, mk_trans_fn(), 4);
mark_implicit_arguments(env, mk_eqt_elim_fn(), 1);
mark_implicit_arguments(env, mk_eqt_intro_fn(), 1);
mark_implicit_arguments(env, mk_congr1_fn(), 4);
mark_implicit_arguments(env, mk_congr2_fn(), 4);
mark_implicit_arguments(env, mk_congr_fn(), 6);
mark_implicit_arguments(env, mk_forall_elim_fn(), 2);
mark_implicit_arguments(env, mk_forall_intro_fn(), 2);
mark_implicit_arguments(env, mk_exists_elim_fn(), 3);
mark_implicit_arguments(env, mk_exists_intro_fn(), 2);
// implicit arguments for basic theorems
mark_implicit_arguments(env, mk_absurd_fn(), 1);
mark_implicit_arguments(env, mk_double_neg_elim_fn(), 1);
mark_implicit_arguments(env, mk_mt_fn(), 2);
mark_implicit_arguments(env, mk_contrapos_fn(), 2);
mark_implicit_arguments(env, mk_eq_mp_fn(), 2);
mark_implicit_arguments(env, mk_not_imp1_fn(), 2);
mark_implicit_arguments(env, mk_not_imp2_fn(), 2);
mark_implicit_arguments(env, mk_conj_fn(), 2);
mark_implicit_arguments(env, mk_conjunct1_fn(), 2);
mark_implicit_arguments(env, mk_conjunct2_fn(), 2);
mark_implicit_arguments(env, mk_disj1_fn(), 1);
mark_implicit_arguments(env, mk_disj2_fn(), 1);
mark_implicit_arguments(env, mk_disj_cases_fn(), 3);
mark_implicit_arguments(env, mk_refute_fn(), 1);
mark_implicit_arguments(env, mk_symm_fn(), 3);
mark_implicit_arguments(env, mk_trans_fn(), 4);
mark_implicit_arguments(env, mk_eqt_elim_fn(), 1);
mark_implicit_arguments(env, mk_eqt_intro_fn(), 1);
mark_implicit_arguments(env, mk_congr1_fn(), 4);
mark_implicit_arguments(env, mk_congr2_fn(), 4);
mark_implicit_arguments(env, mk_congr_fn(), 6);
mark_implicit_arguments(env, mk_forall_elim_fn(), 2);
mark_implicit_arguments(env, mk_forall_intro_fn(), 2);
mark_implicit_arguments(env, mk_exists_elim_fn(), 3);
mark_implicit_arguments(env, mk_exists_intro_fn(), 2);
});
}
}

33
src/frontends/lean/parser.cpp
View file

@ -2140,7 +2140,7 @@ class parser::imp {
/** \brief Return true iff \c obj is an object that should be ignored by the Show command */
bool is_hidden_object(object const & obj) const {
return obj.is_definition() && is_explicit(m_env, obj.get_name());
return (obj.is_definition() && is_explicit(m_env, obj.get_name())) || !supported_by_pp(obj);
}
/** \brief Parse
@ -2155,7 +2155,8 @@ class parser::imp {
name opt_id = curr_name();
next();
if (opt_id == g_env_kwd) {
unsigned beg = get_initial_size(m_env);
buffer<object> to_display;
bool all = false;
unsigned end = m_env->get_num_objects(false);
unsigned i;
if (curr_is_nat()) {
@ -2163,20 +2164,30 @@ class parser::imp {
} else if (curr_is_identifier() && curr_name() == "all") {
next();
i = std::numeric_limits<unsigned>::max();
beg = 0;
all = true;
} else {
i = std::numeric_limits<unsigned>::max();
}
unsigned it = end;
while (it != beg && i != 0) {
unsigned it = end;
unsigned num_imports = 0;
while (it != 0 && i != 0) {
--it;
if (!is_hidden_object(m_env->get_object(it, false)))
--i;
}
for (; it != end; ++it) {
auto obj = m_env->get_object(it, false);
if (!is_hidden_object(obj))
regular(m_io_state) << obj << endl;
if (is_begin_import(obj)) {
lean_assert(num_imports > 0);
num_imports--;
} else if (is_end_import(obj)) {
num_imports++;
} else if (is_hidden_object(obj)) {
// skip
} else if (num_imports == 0 || all) {
to_display.push_back(obj);
--i;
}
}
std::reverse(to_display.begin(), to_display.end());
for (auto obj : to_display) {
regular(m_io_state) << obj << endl;
}
} else if (opt_id == g_options_kwd) {
regular(m_io_state) << pp(m_io_state.get_options()) << endl;

33
src/frontends/lean/pp.cpp
View file

@ -154,6 +154,18 @@ expr replace_var_with_name(expr const & a, name const & n) {
});
}
bool is_notation_decl(object const & obj) {
return dynamic_cast<notation_declaration const *>(obj.cell());
}
bool is_coercion_decl(object const & obj) {
return dynamic_cast<coercion_declaration const *>(obj.cell());
}
bool supported_by_pp(object const & obj) {
return obj.kind() != object_kind::Neutral || is_notation_decl(obj) || is_coercion_decl(obj);
}
/** \brief Functional object for pretty printing expressions */
class pp_fn {
typedef scoped_map<expr, name, expr_hash_alloc, expr_eqp> aliases;
@ -1375,9 +1387,9 @@ public:
case object_kind::Builtin: return pp_postulate(obj, opts);
case object_kind::BuiltinSet: return pp_builtin_set(obj, opts);
case object_kind::Neutral:
if (dynamic_cast<notation_declaration const *>(obj.cell())) {
if (is_notation_decl(obj)) {
return pp_notation_decl(obj, opts);
} else if (dynamic_cast<coercion_declaration const *>(obj.cell())) {
} else if (is_coercion_decl(obj)) {
return pp_coercion_decl(obj, opts);
} else {
// If the object is not notation or coercion
@ -1392,13 +1404,16 @@ public:
virtual format operator()(ro_environment const & env, options const & opts) {
format r;
bool first = true;
std::for_each(env->begin_objects(),
env->end_objects(),
[&](object const & obj) {
check_interrupted();
if (first) first = false; else r += line();
r += operator()(obj, opts);
});
auto it = env->begin_objects();
auto end = env->end_objects();
for (; it != end; ++it) {
check_interrupted();
auto obj = *it;
if (supported_by_pp(obj)) {
if (first) first = false; else r += line();
r += operator()(obj, opts);
}
}
return r;
}

2
src/frontends/lean/pp.h
View file

@ -14,4 +14,6 @@ class frontend;
class environment;
formatter mk_pp_formatter(ro_environment const & env);
std::ostream & operator<<(std::ostream & out, frontend const & fe);
/** \brief Return true iff the given object is supported by this pretty printer. */
bool supported_by_pp(object const & obj);
}

136
src/kernel/builtin.cpp
View file

@ -220,91 +220,93 @@ MK_CONSTANT(htrans_fn, name("HTrans"));
MK_CONSTANT(hsymm_fn, name("HSymm"));
void import_basic(environment const & env) {
if (!env->mark_builtin_imported("basic"))
return;
env->add_uvar(uvar_name(m_lvl), level() + LEAN_DEFAULT_LEVEL_SEPARATION);
env->add_uvar(uvar_name(u_lvl), m_lvl + LEAN_DEFAULT_LEVEL_SEPARATION);
env->import_builtin
("basic",
[&]() {
env->add_uvar(uvar_name(m_lvl), level() + LEAN_DEFAULT_LEVEL_SEPARATION);
env->add_uvar(uvar_name(u_lvl), m_lvl + LEAN_DEFAULT_LEVEL_SEPARATION);
expr p1 = Bool >> Bool;
expr p2 = Bool >> p1;
expr f = Const("f");
expr g = Const("g");
expr a = Const("a");
expr b = Const("b");
expr c = Const("c");
expr x = Const("x");
expr y = Const("y");
expr A = Const("A");
expr A_pred = A >> Bool;
expr B = Const("B");
expr C = Const("C");
expr q_type = Pi({A, TypeU}, A_pred >> Bool);
expr piABx = Pi({x, A}, B(x));
expr A_arrow_u = A >> TypeU;
expr P = Const("P");
expr H = Const("H");
expr H1 = Const("H1");
expr H2 = Const("H2");
expr p1 = Bool >> Bool;
expr p2 = Bool >> p1;
expr f = Const("f");
expr g = Const("g");
expr a = Const("a");
expr b = Const("b");
expr c = Const("c");
expr x = Const("x");
expr y = Const("y");
expr A = Const("A");
expr A_pred = A >> Bool;
expr B = Const("B");
expr C = Const("C");
expr q_type = Pi({A, TypeU}, A_pred >> Bool);
expr piABx = Pi({x, A}, B(x));
expr A_arrow_u = A >> TypeU;
expr P = Const("P");
expr H = Const("H");
expr H1 = Const("H1");
expr H2 = Const("H2");
env->add_builtin(mk_bool_type());
env->add_builtin(mk_bool_value(true));
env->add_builtin(mk_bool_value(false));
env->add_builtin(mk_if_fn());
env->add_builtin(mk_bool_type());
env->add_builtin(mk_bool_value(true));
env->add_builtin(mk_bool_value(false));
env->add_builtin(mk_if_fn());
// implies(x, y) := if x y True
env->add_opaque_definition(implies_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, bIf(x, y, True)));
// implies(x, y) := if x y True
env->add_opaque_definition(implies_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, bIf(x, y, True)));
// iff(x, y) := x = y
env->add_opaque_definition(iff_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, Eq(x, y)));
// iff(x, y) := x = y
env->add_opaque_definition(iff_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, Eq(x, y)));
// not(x) := if x False True
env->add_opaque_definition(not_fn_name, p1, Fun({x, Bool}, bIf(x, False, True)));
// not(x) := if x False True
env->add_opaque_definition(not_fn_name, p1, Fun({x, Bool}, bIf(x, False, True)));
// or(x, y) := Not(x) => y
env->add_opaque_definition(or_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, Implies(Not(x), y)));
// or(x, y) := Not(x) => y
env->add_opaque_definition(or_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, Implies(Not(x), y)));
// and(x, y) := Not(x => Not(y))
env->add_opaque_definition(and_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, Not(Implies(x, Not(y)))));
// and(x, y) := Not(x => Not(y))
env->add_opaque_definition(and_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, Not(Implies(x, Not(y)))));
// forall : Pi (A : Type u), (A -> Bool) -> Bool
env->add_opaque_definition(forall_fn_name, q_type, Fun({{A, TypeU}, {P, A_pred}}, Eq(P, Fun({x, A}, True))));
// TODO(Leo): introduce epsilon
env->add_definition(exists_fn_name, q_type, Fun({{A, TypeU}, {P, A_pred}}, Not(Forall(A, Fun({x, A}, Not(P(x)))))));
// Aliases for forall and exists
env->add_definition(Forall_fn_name, q_type, Fun({{A, TypeU}, {P, A_pred}}, Forall(A, P)));
env->add_definition(Exists_fn_name, q_type, Fun({{A, TypeU}, {P, A_pred}}, Exists(A, P)));
// forall : Pi (A : Type u), (A -> Bool) -> Bool
env->add_opaque_definition(forall_fn_name, q_type, Fun({{A, TypeU}, {P, A_pred}}, Eq(P, Fun({x, A}, True))));
// TODO(Leo): introduce epsilon
env->add_definition(exists_fn_name, q_type, Fun({{A, TypeU}, {P, A_pred}}, Not(Forall(A, Fun({x, A}, Not(P(x)))))));
// Aliases for forall and exists
env->add_definition(Forall_fn_name, q_type, Fun({{A, TypeU}, {P, A_pred}}, Forall(A, P)));
env->add_definition(Exists_fn_name, q_type, Fun({{A, TypeU}, {P, A_pred}}, Exists(A, P)));
// homogeneous equality
env->add_definition(homo_eq_fn_name, Pi({{A, TypeU}, {x, A}, {y, A}}, Bool), Fun({{A, TypeU}, {x, A}, {y, A}}, Eq(x, y)));
// homogeneous equality
env->add_definition(homo_eq_fn_name, Pi({{A, TypeU}, {x, A}, {y, A}}, Bool), Fun({{A, TypeU}, {x, A}, {y, A}}, Eq(x, y)));
// MP : Pi (a b : Bool) (H1 : a => b) (H2 : a), b
env->add_axiom(mp_fn_name, Pi({{a, Bool}, {b, Bool}, {H1, Implies(a, b)}, {H2, a}}, b));
// MP : Pi (a b : Bool) (H1 : a => b) (H2 : a), b
env->add_axiom(mp_fn_name, Pi({{a, Bool}, {b, Bool}, {H1, Implies(a, b)}, {H2, a}}, b));
// Discharge : Pi (a b : Bool) (H : a -> b), a => b
env->add_axiom(discharge_fn_name, Pi({{a, Bool}, {b, Bool}, {H, a >> b}}, Implies(a, b)));
// Discharge : Pi (a b : Bool) (H : a -> b), a => b
env->add_axiom(discharge_fn_name, Pi({{a, Bool}, {b, Bool}, {H, a >> b}}, Implies(a, b)));
// Case : Pi (P : Bool -> Bool) (H1 : P True) (H2 : P False) (a : Bool), P a
env->add_axiom(case_fn_name, Pi({{P, Bool >> Bool}, {H1, P(True)}, {H2, P(False)}, {a, Bool}}, P(a)));
// Case : Pi (P : Bool -> Bool) (H1 : P True) (H2 : P False) (a : Bool), P a
env->add_axiom(case_fn_name, Pi({{P, Bool >> Bool}, {H1, P(True)}, {H2, P(False)}, {a, Bool}}, P(a)));
// Refl : Pi (A : Type u) (a : A), a = a
env->add_axiom(refl_fn_name, Pi({{A, TypeU}, {a, A}}, Eq(a, a)));
// Refl : Pi (A : Type u) (a : A), a = a
env->add_axiom(refl_fn_name, Pi({{A, TypeU}, {a, A}}, Eq(a, a)));
// Subst : Pi (A : Type u) (a b : A) (P : A -> bool) (H1 : P a) (H2 : a = b), P b
env->add_axiom(subst_fn_name, Pi({{A, TypeU}, {a, A}, {b, A}, {P, A_pred}, {H1, P(a)}, {H2, Eq(a, b)}}, P(b)));
// Subst : Pi (A : Type u) (a b : A) (P : A -> bool) (H1 : P a) (H2 : a = b), P b
env->add_axiom(subst_fn_name, Pi({{A, TypeU}, {a, A}, {b, A}, {P, A_pred}, {H1, P(a)}, {H2, Eq(a, b)}}, P(b)));
// Eta : Pi (A : Type u) (B : A -> Type u), f : (Pi x : A, B x), (Fun x : A => f x) = f
env->add_axiom(eta_fn_name, Pi({{A, TypeU}, {B, A_arrow_u}, {f, piABx}}, Eq(Fun({x, A}, f(x)), f)));
// Eta : Pi (A : Type u) (B : A -> Type u), f : (Pi x : A, B x), (Fun x : A => f x) = f
env->add_axiom(eta_fn_name, Pi({{A, TypeU}, {B, A_arrow_u}, {f, piABx}}, Eq(Fun({x, A}, f(x)), f)));
// ImpliesAntisym : Pi (a b : Bool) (H1 : a => b) (H2 : b => a), a = b
env->add_axiom(imp_antisym_fn_name, Pi({{a, Bool}, {b, Bool}, {H1, Implies(a, b)}, {H2, Implies(b, a)}}, Eq(a, b)));
// ImpliesAntisym : Pi (a b : Bool) (H1 : a => b) (H2 : b => a), a = b
env->add_axiom(imp_antisym_fn_name, Pi({{a, Bool}, {b, Bool}, {H1, Implies(a, b)}, {H2, Implies(b, a)}}, Eq(a, b)));
// Abst : Pi (A : Type u) (B : A -> Type u), f g : (Pi x : A, B x), H : (Pi x : A, (f x) = (g x)), f = g
env->add_axiom(abst_fn_name, Pi({{A, TypeU}, {B, A_arrow_u}, {f, piABx}, {g, piABx}, {H, Pi(x, A, Eq(f(x), g(x)))}}, Eq(f, g)));
// Abst : Pi (A : Type u) (B : A -> Type u), f g : (Pi x : A, B x), H : (Pi x : A, (f x) = (g x)), f = g
env->add_axiom(abst_fn_name, Pi({{A, TypeU}, {B, A_arrow_u}, {f, piABx}, {g, piABx}, {H, Pi(x, A, Eq(f(x), g(x)))}}, Eq(f, g)));
// HSymm : Pi (A B : Type u) (a : A) (b : B) (H1 : a = b), b = a
env->add_axiom(hsymm_fn_name, Pi({{A, TypeU}, {B, TypeU}, {a, A}, {b, B}, {H1, Eq(a, b)}}, Eq(b, a)));
// HSymm : Pi (A B : Type u) (a : A) (b : B) (H1 : a = b), b = a
env->add_axiom(hsymm_fn_name, Pi({{A, TypeU}, {B, TypeU}, {a, A}, {b, B}, {H1, Eq(a, b)}}, Eq(b, a)));
// HTrans : Pi (A B C: Type u) (a : A) (b : B) (c : C) (H1 : a = b) (H2 : b = c), a = c
env->add_axiom(htrans_fn_name, Pi({{A, TypeU}, {B, TypeU}, {C, TypeU}, {a, A}, {b, B}, {c, C}, {H1, Eq(a, b)}, {H2, Eq(b, c)}}, Eq(a, c)));
// HTrans : Pi (A B C: Type u) (a : A) (b : B) (c : C) (H1 : a = b) (H2 : b = c), a = c
env->add_axiom(htrans_fn_name, Pi({{A, TypeU}, {B, TypeU}, {C, TypeU}, {a, A}, {b, B}, {c, C}, {H1, Eq(a, b)}, {H2, Eq(b, c)}}, Eq(a, c)));
});
}
}

119
src/kernel/environment.cpp
View file

@ -8,10 +8,13 @@ Author: Leonardo de Moura
#include <algorithm>
#include <vector>
#include <tuple>
#include <fstream>
#include <string>
#include "util/thread.h"
#include "util/safe_arith.h"
#include "util/realpath.h"
#include "util/sstream.h"
#include "util/lean_path.h"
#include "kernel/for_each_fn.h"
#include "kernel/find_fn.h"
#include "kernel/kernel_exception.h"
@ -19,6 +22,7 @@ Author: Leonardo de Moura
#include "kernel/threadsafe_environment.h"
#include "kernel/type_checker.h"
#include "kernel/normalizer.h"
#include "version.h"
namespace lean {
class set_opaque_command : public neutral_object_cell {
@ -37,6 +41,45 @@ static void read_set_opaque(environment const & env, io_state const &, deseriali
}
static object_cell::register_deserializer_fn set_opaque_ds("SetOpaque", read_set_opaque);
class import_command : public neutral_object_cell {
std::string m_mod_name;
public:
import_command(std::string const & n):m_mod_name(n) {}
virtual ~import_command() {}
virtual char const * keyword() const { return "Import"; }
virtual void write(serializer & s) const { s << "Import" << m_mod_name; }
};
static void read_import(environment const & env, io_state const & ios, deserializer & d) {
std::string n = d.read_string();
env->import(n, ios);
}
static object_cell::register_deserializer_fn import_ds("Import", read_import);
class end_import_mark : public neutral_object_cell {
public:
end_import_mark() {}
virtual ~end_import_mark() {}
virtual char const * keyword() const { return "EndImport"; }
virtual void write(serializer &) const {}
};
// For Importing builtin modules
class begin_import_mark : public neutral_object_cell {
public:
begin_import_mark() {}
virtual ~begin_import_mark() {}
virtual char const * keyword() const { return "BeginImport"; }
virtual void write(serializer &) const {}
};
bool is_begin_import(object const & obj) {
return dynamic_cast<import_command const*>(obj.cell()) || dynamic_cast<begin_import_mark const*>(obj.cell());
}
bool is_end_import(object const & obj) {
return dynamic_cast<end_import_mark const*>(obj.cell());
}
static name g_builtin_module("builtin_module");
class extension_factory {
std::vector<environment_cell::mk_extension> m_makers;
@ -461,8 +504,80 @@ bool environment_cell::mark_imported(char const * fname) {
return mark_imported_core(name(realpath(fname)));
}
bool environment_cell::mark_builtin_imported(char const * id) {
return mark_imported_core(name(g_builtin_module, id));
void environment_cell::auxiliary_section(std::function<void()> fn) {
add_neutral_object(new begin_import_mark());
try {
fn();
add_neutral_object(new end_import_mark());
} catch (...) {
add_neutral_object(new end_import_mark());
throw;
}
}
void environment_cell::import_builtin(char const * id, std::function<void()> fn) {
if (mark_imported_core(name(g_builtin_module, id))) {
auxiliary_section(fn);
}
}
static char const * g_olean_header = "oleanfile";
static char const * g_olean_end_file = "EndFile";
void environment_cell::export_objects(std::string const & fname) {
std::ofstream out(fname);
serializer s(out);
s << g_olean_header << LEAN_VERSION_MAJOR << LEAN_VERSION_MINOR;
auto it = begin_objects();
auto end = end_objects();
unsigned num_imports = 0;
for (; it != end; ++it) {
object const & obj = *it;
if (dynamic_cast<import_command const*>(obj.cell())) {
if (num_imports == 0)
obj.write(s);
num_imports++;
} else if (dynamic_cast<end_import_mark const*>(obj.cell())) {
lean_assert(num_imports > 0);
num_imports--;
} else if (dynamic_cast<begin_import_mark const*>(obj.cell())) {
num_imports++;
} else if (num_imports == 0) {
obj.write(s);
}
}
s << g_olean_end_file;
}
bool environment_cell::import(std::string const & fname, io_state const & ios) {
std::string full_fname = realpath(find_file(fname, {".olean"}).c_str());
if (mark_imported_core(full_fname)) {
std::ifstream in(fname);
deserializer d(in);
std::string header;
d >> header;
if (header != g_olean_header)
throw exception(sstream() << "file '" << full_fname << "' does not seem to be a valid object Lean file");
unsigned major, minor;
// Perhaps we should enforce the right version number
d >> major >> minor;
try {
add_neutral_object(new import_command(fname));
while (true) {
std::string k;
d >> k;
if (k == g_olean_end_file) {
add_neutral_object(new end_import_mark());
return true;
}
read_object(env(), ios, k, d);
}
} catch (...) {
add_neutral_object(new end_import_mark());
throw;
}
} else {
return false;
}
}
environment_cell::environment_cell():

19
src/kernel/environment.h
View file

@ -9,6 +9,7 @@ Author: Leonardo de Moura
#include <memory>
#include <vector>
#include <set>
#include <string>
#include "util/lua.h"
#include "util/shared_mutex.h"
#include "util/name_map.h"
@ -314,11 +315,18 @@ public:
It will also mark the file as imported.
*/
bool mark_imported(char const * fname);
void import_builtin(char const * id, std::function<void()> fn);
void export_objects(std::string const & fname);
bool import(std::string const & fname, io_state const & ios);
/**
\brief Return true iff the given builtin id was not already marked as imported.
It will also mark the id as imported.
\brief Execute function \c fn. Any object created by \c fn
is not exported by the environment.
*/
bool mark_builtin_imported(char const * id);
void auxiliary_section(std::function<void()> fn);
};
/**
@ -382,4 +390,9 @@ public:
environment_cell const * operator->() const { return m_ptr.get(); }
environment_cell const & operator*() const { return *(m_ptr.get()); }
};
/** \brief Return true iff the given object marks the begin of the of a sequence of imported objects. */
bool is_begin_import(object const & obj);
/** \brief Return true iff the given object marks the end of the of a sequence of imported objects. */
bool is_end_import(object const & obj);
}

2
src/kernel/kernel_exception.h
View file

@ -73,7 +73,7 @@ public:
already_declared_exception(ro_environment const & env, name const & n):kernel_exception(env), m_name(n) {}
virtual ~already_declared_exception() noexcept {}
name const & get_name() const { return m_name; }
virtual char const * what() const noexcept { return "invalid object declaration, environment already has an object the given name"; }
virtual char const * what() const noexcept { return "invalid object declaration, environment already has an object with the given name"; }
virtual format pp(formatter const & fmt, options const & opts) const;
virtual exception * clone() const { return new already_declared_exception(m_env, m_name); }
virtual void rethrow() const { throw *this; }

3
src/kernel/object.cpp
View file

@ -22,8 +22,7 @@ void object_cell::register_deserializer(std::string const & k, reader rd) {
lean_assert(readers.find(k) == readers.end());
readers[k] = rd;
}
static void read_object(environment const & env, io_state const & ios, deserializer & d) {
auto k = d.read_string();
void read_object(environment const & env, io_state const & ios, std::string const & k, deserializer & d) {
object_readers & readers = get_object_readers();
auto it = readers.find(k);
lean_assert(it != readers.end());

4
src/kernel/object.h
View file

@ -139,6 +139,8 @@ public:
bool is_builtin_set() const { return m_ptr->is_builtin_set(); }
bool in_builtin_set(expr const & e) const { return m_ptr->in_builtin_set(e); }
void write(serializer & s) const { m_ptr->write(s); }
object_cell const * cell() const { return m_ptr; }
};
@ -155,6 +157,8 @@ object mk_axiom(name const & n, expr const & t);
object mk_var_decl(name const & n, expr const & t);
inline object mk_neutral(neutral_object_cell * c) { lean_assert(c->get_rc() == 1); return object(c); }
void read_object(environment const & env, io_state const & ios, std::string const & k, deserializer & d);
/**
\brief Helper function whether we should unfold an definition or not.

52
src/library/arith/int.cpp
View file

@ -164,34 +164,36 @@ MK_CONSTANT(nat_sub_fn, name({"Nat", "sub"}));
MK_CONSTANT(nat_neg_fn, name({"Nat", "neg"}));
void import_int(environment const & env) {
if (!env->mark_builtin_imported("int"))
return;
import_nat(env);
expr i_i = Int >> Int;
expr ii_b = Int >> (Int >> Bool);
expr ii_i = Int >> (Int >> Int);
expr x = Const("x");
expr y = Const("y");
env->import_builtin(
"int",
[&]() {
import_nat(env);
expr i_i = Int >> Int;
expr ii_b = Int >> (Int >> Bool);
expr ii_i = Int >> (Int >> Int);
expr x = Const("x");
expr y = Const("y");
env->add_builtin(Int);
env->add_builtin_set(iVal(0));
env->add_builtin(mk_int_add_fn());
env->add_builtin(mk_int_mul_fn());
env->add_builtin(mk_int_div_fn());
env->add_builtin(mk_int_le_fn());
env->add_builtin(mk_nat_to_int_fn());
env->add_builtin(Int);
env->add_builtin_set(iVal(0));
env->add_builtin(mk_int_add_fn());
env->add_builtin(mk_int_mul_fn());
env->add_builtin(mk_int_div_fn());
env->add_builtin(mk_int_le_fn());
env->add_builtin(mk_nat_to_int_fn());
env->add_opaque_definition(int_sub_fn_name, ii_i, Fun({{x, Int}, {y, Int}}, iAdd(x, iMul(iVal(-1), y))));
env->add_opaque_definition(int_neg_fn_name, i_i, Fun({x, Int}, iMul(iVal(-1), x)));
env->add_opaque_definition(int_mod_fn_name, ii_i, Fun({{x, Int}, {y, Int}}, iSub(x, iMul(y, iDiv(x, y)))));
env->add_opaque_definition(int_divides_fn_name, ii_b, Fun({{x, Int}, {y, Int}}, Eq(iMod(y, x), iVal(0))));
env->add_opaque_definition(int_ge_fn_name, ii_b, Fun({{x, Int}, {y, Int}}, iLe(y, x)));
env->add_opaque_definition(int_lt_fn_name, ii_b, Fun({{x, Int}, {y, Int}}, Not(iLe(y, x))));
env->add_opaque_definition(int_gt_fn_name, ii_b, Fun({{x, Int}, {y, Int}}, Not(iLe(x, y))));
env->add_opaque_definition(int_abs_fn_name, i_i, Fun({x, Int}, iIf(iLe(iVal(0), x), x, iNeg(x))));
env->add_opaque_definition(int_sub_fn_name, ii_i, Fun({{x, Int}, {y, Int}}, iAdd(x, iMul(iVal(-1), y))));
env->add_opaque_definition(int_neg_fn_name, i_i, Fun({x, Int}, iMul(iVal(-1), x)));
env->add_opaque_definition(int_mod_fn_name, ii_i, Fun({{x, Int}, {y, Int}}, iSub(x, iMul(y, iDiv(x, y)))));
env->add_opaque_definition(int_divides_fn_name, ii_b, Fun({{x, Int}, {y, Int}}, Eq(iMod(y, x), iVal(0))));
env->add_opaque_definition(int_ge_fn_name, ii_b, Fun({{x, Int}, {y, Int}}, iLe(y, x)));
env->add_opaque_definition(int_lt_fn_name, ii_b, Fun({{x, Int}, {y, Int}}, Not(iLe(y, x))));
env->add_opaque_definition(int_gt_fn_name, ii_b, Fun({{x, Int}, {y, Int}}, Not(iLe(x, y))));
env->add_opaque_definition(int_abs_fn_name, i_i, Fun({x, Int}, iIf(iLe(iVal(0), x), x, iNeg(x))));
env->add_opaque_definition(nat_sub_fn_name, Nat >> (Nat >> Int), Fun({{x, Nat}, {y, Nat}}, iSub(n2i(x), n2i(y))));
env->add_opaque_definition(nat_neg_fn_name, Nat >> Int, Fun({x, Nat}, iNeg(n2i(x))));
env->add_opaque_definition(nat_sub_fn_name, Nat >> (Nat >> Int), Fun({{x, Nat}, {y, Nat}}, iSub(n2i(x), n2i(y))));
env->add_opaque_definition(nat_neg_fn_name, Nat >> Int, Fun({x, Nat}, iNeg(n2i(x))));
});
}
static int mk_int_value(lua_State * L) {

30
src/library/arith/nat.cpp
View file

@ -123,22 +123,24 @@ MK_CONSTANT(nat_gt_fn, name({"Nat", "gt"}));
MK_CONSTANT(nat_id_fn, name({"Nat", "id"}));
void import_nat(environment const & env) {
if (!env->mark_builtin_imported("nat"))
return;
expr nn_b = Nat >> (Nat >> Bool);
expr x = Const("x");
expr y = Const("y");
env->import_builtin(
"nat",
[&]() {
expr nn_b = Nat >> (Nat >> Bool);
expr x = Const("x");
expr y = Const("y");
env->add_builtin(Nat);
env->add_builtin_set(nVal(0));
env->add_builtin(mk_nat_add_fn());
env->add_builtin(mk_nat_mul_fn());
env->add_builtin(mk_nat_le_fn());
env->add_builtin(Nat);
env->add_builtin_set(nVal(0));
env->add_builtin(mk_nat_add_fn());
env->add_builtin(mk_nat_mul_fn());
env->add_builtin(mk_nat_le_fn());
env->add_opaque_definition(nat_ge_fn_name, nn_b, Fun({{x, Nat}, {y, Nat}}, nLe(y, x)));
env->add_opaque_definition(nat_lt_fn_name, nn_b, Fun({{x, Nat}, {y, Nat}}, Not(nLe(y, x))));
env->add_opaque_definition(nat_gt_fn_name, nn_b, Fun({{x, Nat}, {y, Nat}}, Not(nLe(x, y))));
env->add_opaque_definition(nat_id_fn_name, Nat >> Nat, Fun({x, Nat}, x));
env->add_opaque_definition(nat_ge_fn_name, nn_b, Fun({{x, Nat}, {y, Nat}}, nLe(y, x)));
env->add_opaque_definition(nat_lt_fn_name, nn_b, Fun({{x, Nat}, {y, Nat}}, Not(nLe(y, x))));
env->add_opaque_definition(nat_gt_fn_name, nn_b, Fun({{x, Nat}, {y, Nat}}, Not(nLe(x, y))));
env->add_opaque_definition(nat_id_fn_name, Nat >> Nat, Fun({x, Nat}, x));
});
}
static int mk_nat_value(lua_State * L) {

56
src/library/arith/real.cpp
View file

@ -150,27 +150,29 @@ MK_CONSTANT(real_lt_fn, name({"Real", "lt"}));
MK_CONSTANT(real_gt_fn, name({"Real", "gt"}));
void import_real(environment const & env) {
if (!env->mark_builtin_imported("real"))
return;
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->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_builtin(Real);
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_builtin(Real);
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))));
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))));
});
}
class int_to_real_value : public const_value {
@ -191,14 +193,16 @@ static register_deserializer_fn int_to_real_ds("int_to_real", read_int_to_real);
MK_CONSTANT(nat_to_real_fn, name("nat_to_real"));
void import_int_to_real_coercions(environment const & env) {
if (!env->mark_builtin_imported("real_coercions"))
return;
import_int(env);
import_real(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))));
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))));
});
}
static int mk_real_value(lua_State * L) {

48
src/library/arith/special_fn.cpp
View file

@ -29,32 +29,34 @@ MK_CONSTANT(sech_fn, name("sech"));
MK_CONSTANT(csch_fn, name("csch"));
void import_special_fn(environment const & env) {
if (!env->mark_builtin_imported("special_fn"))
return;
import_real(env);
env->import_builtin(
"special_fn",
[&]() {
import_real(env);
expr r_r = Real >> Real;
expr x = Const("x");
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(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_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))));
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))));
});
}
}

396
src/library/basic_thms.cpp
View file

@ -47,241 +47,243 @@ MK_CONSTANT(exists_elim_fn, name("ExistsElim"));
MK_CONSTANT(exists_intro_fn, name("ExistsIntro"));
void import_basic_thms(environment const & env) {
if (!env->mark_builtin_imported("basic_thms"))
return;
expr A = Const("A");
expr a = Const("a");
expr b = Const("b");
expr c = Const("c");
expr H = Const("H");
expr H1 = Const("H1");
expr H2 = Const("H2");
expr H3 = Const("H3");
expr B = Const("B");
expr f = Const("f");
expr g = Const("g");
expr h = Const("h");
expr x = Const("x");
expr y = Const("y");
expr z = Const("z");
expr P = Const("P");
expr A1 = Const("A1");
expr B1 = Const("B1");
expr a1 = Const("a1");
expr R = Const("R");
env->import_builtin(
"basic_thms",
[&]() {
expr A = Const("A");
expr a = Const("a");
expr b = Const("b");
expr c = Const("c");
expr H = Const("H");
expr H1 = Const("H1");
expr H2 = Const("H2");
expr H3 = Const("H3");
expr B = Const("B");
expr f = Const("f");
expr g = Const("g");
expr h = Const("h");
expr x = Const("x");
expr y = Const("y");
expr z = Const("z");
expr P = Const("P");
expr A1 = Const("A1");
expr B1 = Const("B1");
expr a1 = Const("a1");
expr R = Const("R");
expr A_pred = A >> Bool;
expr q_type = Pi({A, TypeU}, A_pred >> Bool);
expr piABx = Pi({x, A}, B(x));
expr A_arrow_u = A >> TypeU;
expr A_pred = A >> Bool;
expr q_type = Pi({A, TypeU}, A_pred >> Bool);
expr piABx = Pi({x, A}, B(x));
expr A_arrow_u = A >> TypeU;
// Trivial : True
env->add_theorem(trivial_name, True, Refl(Bool, True));
// Trivial : True
env->add_theorem(trivial_name, True, Refl(Bool, True));
// True_neq_False : Not(True = False)
env->add_theorem(true_neq_false_name, Not(Eq(True, False)), Trivial);
// True_neq_False : Not(True = False)
env->add_theorem(true_neq_false_name, Not(Eq(True, False)), Trivial);
// EM : Pi (a : Bool), Or(a, Not(a))
env->add_theorem(em_fn_name, Pi({a, Bool}, Or(a, Not(a))),
Fun({a, Bool}, Case(Fun({x, Bool}, Or(x, Not(x))), Trivial, Trivial, a)));
// EM : Pi (a : Bool), Or(a, Not(a))
env->add_theorem(em_fn_name, Pi({a, Bool}, Or(a, Not(a))),
Fun({a, Bool}, Case(Fun({x, Bool}, Or(x, Not(x))), Trivial, Trivial, a)));
// FalseElim : Pi (a : Bool) (H : False), a
env->add_theorem(false_elim_fn_name, Pi({{a, Bool}, {H, False}}, a),
Fun({{a, Bool}, {H, False}}, Case(Fun({x, Bool}, x), Trivial, H, a)));
// FalseElim : Pi (a : Bool) (H : False), a
env->add_theorem(false_elim_fn_name, Pi({{a, Bool}, {H, False}}, a),
Fun({{a, Bool}, {H, False}}, Case(Fun({x, Bool}, x), Trivial, H, a)));
// Absurd : Pi (a : Bool) (H1 : a) (H2 : Not a), False
env->add_theorem(absurd_fn_name, Pi({{a, Bool}, {H1, a}, {H2, Not(a)}}, False),
Fun({{a, Bool}, {H1, a}, {H2, Not(a)}},
MP(a, False, H2, H1)));
// Absurd : Pi (a : Bool) (H1 : a) (H2 : Not a), False
env->add_theorem(absurd_fn_name, Pi({{a, Bool}, {H1, a}, {H2, Not(a)}}, False),
Fun({{a, Bool}, {H1, a}, {H2, Not(a)}},
MP(a, False, H2, H1)));
// EqMP : Pi (a b: Bool) (H1 : a = b) (H2 : a), b
env->add_theorem(eq_mp_fn_name, Pi({{a, Bool}, {b, Bool}, {H1, Eq(a, b)}, {H2, a}}, b),
Fun({{a, Bool}, {b, Bool}, {H1, Eq(a, b)}, {H2, a}},
Subst(Bool, a, b, Fun({x, Bool}, x), H2, H1)));
// EqMP : Pi (a b: Bool) (H1 : a = b) (H2 : a), b
env->add_theorem(eq_mp_fn_name, Pi({{a, Bool}, {b, Bool}, {H1, Eq(a, b)}, {H2, a}}, b),
Fun({{a, Bool}, {b, Bool}, {H1, Eq(a, b)}, {H2, a}},
Subst(Bool, a, b, Fun({x, Bool}, x), H2, H1)));
// DoubleNeg : Pi (a : Bool), Eq(Not(Not(a)), a)
env->add_theorem(double_neg_fn_name, Pi({a, Bool}, Eq(Not(Not(a)), a)),
Fun({a, Bool}, Case(Fun({x, Bool}, Eq(Not(Not(x)), x)), Trivial, Trivial, a)));
// DoubleNeg : Pi (a : Bool), Eq(Not(Not(a)), a)
env->add_theorem(double_neg_fn_name, Pi({a, Bool}, Eq(Not(Not(a)), a)),
Fun({a, Bool}, Case(Fun({x, Bool}, Eq(Not(Not(x)), x)), Trivial, Trivial, a)));
// DoubleNegElim : Pi (P : Bool) (H : Not (Not P)), P
env->add_theorem(double_neg_elim_fn_name, Pi({{P, Bool}, {H, Not(Not(P))}}, P),
Fun({{P, Bool}, {H, Not(Not(P))}},
EqMP(Not(Not(P)), P, DoubleNeg(P), H)));
// DoubleNegElim : Pi (P : Bool) (H : Not (Not P)), P
env->add_theorem(double_neg_elim_fn_name, Pi({{P, Bool}, {H, Not(Not(P))}}, P),
Fun({{P, Bool}, {H, Not(Not(P))}},
EqMP(Not(Not(P)), P, DoubleNeg(P), H)));
// ModusTollens : Pi (a b : Bool) (H1 : a => b) (H2 : Not(b)), Not(a)
env->add_theorem(mt_fn_name, Pi({{a, Bool}, {b, Bool}, {H1, Implies(a, b)}, {H2, Not(b)}}, Not(a)),
Fun({{a, Bool}, {b, Bool}, {H1, Implies(a, b)}, {H2, Not(b)}},
Discharge(a, False, Fun({H, a},
Absurd(b, MP(a, b, H1, H), H2)))));
// ModusTollens : Pi (a b : Bool) (H1 : a => b) (H2 : Not(b)), Not(a)
env->add_theorem(mt_fn_name, Pi({{a, Bool}, {b, Bool}, {H1, Implies(a, b)}, {H2, Not(b)}}, Not(a)),
Fun({{a, Bool}, {b, Bool}, {H1, Implies(a, b)}, {H2, Not(b)}},
Discharge(a, False, Fun({H, a},
Absurd(b, MP(a, b, H1, H), H2)))));
// Contrapositive : Pi (a b : Bool) (H : a => b), (Not(b) => Not(a))
env->add_theorem(contrapos_fn_name, Pi({{a, Bool}, {b, Bool}, {H, Implies(a, b)}}, Implies(Not(b), Not(a))),
Fun({{a, Bool}, {b, Bool}, {H, Implies(a, b)}},
Discharge(Not(b), Not(a), Fun({H1, Not(b)}, MT(a, b, H, H1)))));
// Contrapositive : Pi (a b : Bool) (H : a => b), (Not(b) => Not(a))
env->add_theorem(contrapos_fn_name, Pi({{a, Bool}, {b, Bool}, {H, Implies(a, b)}}, Implies(Not(b), Not(a))),
Fun({{a, Bool}, {b, Bool}, {H, Implies(a, b)}},
Discharge(Not(b), Not(a), Fun({H1, Not(b)}, MT(a, b, H, H1)))));
// FalseImpliesAny : Pi (a : Bool), False => a
env->add_theorem(false_imp_any_fn_name, Pi({a, Bool}, Implies(False, a)),
Fun({a, Bool}, Case(Fun({x, Bool}, Implies(False, x)), Trivial, Trivial, a)));
// FalseImpliesAny : Pi (a : Bool), False => a
env->add_theorem(false_imp_any_fn_name, Pi({a, Bool}, Implies(False, a)),
Fun({a, Bool}, Case(Fun({x, Bool}, Implies(False, x)), Trivial, Trivial, a)));
// AbsurdImpliesAny : Pi (a c : Bool) (H1 : a) (H2 : Not a), c
env->add_theorem(absurd_imp_any_fn_name, Pi({{a, Bool}, {c, Bool}, {H1, a}, {H2, Not(a)}}, c),
Fun({{a, Bool}, {c, Bool}, {H1, a}, {H2, Not(a)}},
MP(False, c, FalseImpAny(c), Absurd(a, H1, H2))));
// AbsurdImpliesAny : Pi (a c : Bool) (H1 : a) (H2 : Not a), c
env->add_theorem(absurd_imp_any_fn_name, Pi({{a, Bool}, {c, Bool}, {H1, a}, {H2, Not(a)}}, c),
Fun({{a, Bool}, {c, Bool}, {H1, a}, {H2, Not(a)}},
MP(False, c, FalseImpAny(c), Absurd(a, H1, H2))));
// NotImp1 : Pi (a b : Bool) (H : Not(Implies(a, b))), a
env->add_theorem(not_imp1_fn_name, Pi({{a, Bool}, {b, Bool}, {H, Not(Implies(a, b))}}, a),
Fun({{a, Bool}, {b, Bool}, {H, Not(Implies(a, b))}},
EqMP(Not(Not(a)), a,
DoubleNeg(a),
Discharge(Not(a), False,
Fun({H1, Not(a)},
Absurd(Implies(a, b),
Discharge(a, b,
Fun({H2, a},
FalseElim(b, Absurd(a, H2, H1)))),
H))))));
// NotImp1 : Pi (a b : Bool) (H : Not(Implies(a, b))), a
env->add_theorem(not_imp1_fn_name, Pi({{a, Bool}, {b, Bool}, {H, Not(Implies(a, b))}}, a),
Fun({{a, Bool}, {b, Bool}, {H, Not(Implies(a, b))}},
EqMP(Not(Not(a)), a,
DoubleNeg(a),
Discharge(Not(a), False,
Fun({H1, Not(a)},
Absurd(Implies(a, b),
Discharge(a, b,
Fun({H2, a},
FalseElim(b, Absurd(a, H2, H1)))),
H))))));
// NotImp2 : Pi (a b : Bool) (H : Not(Implies(a, b))), Not(b)
env->add_theorem(not_imp2_fn_name, Pi({{a, Bool}, {b, Bool}, {H, Not(Implies(a, b))}}, Not(b)),
Fun({{a, Bool}, {b, Bool}, {H, Not(Implies(a, b))}},
Discharge(b, False,
Fun({H1, b},
Absurd(Implies(a, b),
// a => b
Discharge(a, b, Fun({H2, a}, H1)),
H)))));
// NotImp2 : Pi (a b : Bool) (H : Not(Implies(a, b))), Not(b)
env->add_theorem(not_imp2_fn_name, Pi({{a, Bool}, {b, Bool}, {H, Not(Implies(a, b))}}, Not(b)),
Fun({{a, Bool}, {b, Bool}, {H, Not(Implies(a, b))}},
Discharge(b, False,
Fun({H1, b},
Absurd(Implies(a, b),
// a => b
Discharge(a, b, Fun({H2, a}, H1)),
H)))));
// Conj : Pi (a b : Bool) (H1 : a) (H2 : b), And(a, b)
env->add_theorem(conj_fn_name, Pi({{a, Bool}, {b, Bool}, {H1, a}, {H2, b}}, And(a, b)),
Fun({{a, Bool}, {b, Bool}, {H1, a}, {H2, b}},
Discharge(Implies(a, Not(b)), False, Fun({H, Implies(a, Not(b))},
Absurd(b, H2, MP(a, Not(b), H, H1))))));
// Conj : Pi (a b : Bool) (H1 : a) (H2 : b), And(a, b)
env->add_theorem(conj_fn_name, Pi({{a, Bool}, {b, Bool}, {H1, a}, {H2, b}}, And(a, b)),
Fun({{a, Bool}, {b, Bool}, {H1, a}, {H2, b}},
Discharge(Implies(a, Not(b)), False, Fun({H, Implies(a, Not(b))},
Absurd(b, H2, MP(a, Not(b), H, H1))))));
// Conjunct1 : Pi (a b : Bool) (H : And(a, b)), a
env->add_theorem(conjunct1_fn_name, Pi({{a, Bool}, {b, Bool}, {H, And(a, b)}}, a),
Fun({{a, Bool}, {b, Bool}, {H, And(a, b)}},
NotImp1(a, Not(b), H)));
// Conjunct1 : Pi (a b : Bool) (H : And(a, b)), a
env->add_theorem(conjunct1_fn_name, Pi({{a, Bool}, {b, Bool}, {H, And(a, b)}}, a),
Fun({{a, Bool}, {b, Bool}, {H, And(a, b)}},
NotImp1(a, Not(b), H)));
// Conjunct2 : Pi (a b : Bool) (H : And(a, b)), b
env->add_theorem(conjunct2_fn_name, Pi({{a, Bool}, {b, Bool}, {H, And(a, b)}}, b),
Fun({{a, Bool}, {b, Bool}, {H, And(a, b)}},
EqMP(Not(Not(b)), b, DoubleNeg(b), NotImp2(a, Not(b), H))));
// Conjunct2 : Pi (a b : Bool) (H : And(a, b)), b
env->add_theorem(conjunct2_fn_name, Pi({{a, Bool}, {b, Bool}, {H, And(a, b)}}, b),
Fun({{a, Bool}, {b, Bool}, {H, And(a, b)}},
EqMP(Not(Not(b)), b, DoubleNeg(b), NotImp2(a, Not(b), H))));
// Disj1 : Pi (a b : Bool) (H : a), Or(a, b)
env->add_theorem(disj1_fn_name, Pi({{a, Bool}, {b, Bool}, {H, a}}, Or(a, b)),
Fun({{a, Bool}, {b, Bool}, {H, a}},
Discharge(Not(a), b, Fun({H1, Not(a)},
FalseElim(b, Absurd(a, H, H1))))));
// Disj1 : Pi (a b : Bool) (H : a), Or(a, b)
env->add_theorem(disj1_fn_name, Pi({{a, Bool}, {b, Bool}, {H, a}}, Or(a, b)),
Fun({{a, Bool}, {b, Bool}, {H, a}},
Discharge(Not(a), b, Fun({H1, Not(a)},
FalseElim(b, Absurd(a, H, H1))))));
// Disj2 : Pi (b a : Bool) (H : b), Or(a, b)
env->add_theorem(disj2_fn_name, Pi({{b, Bool}, {a, Bool}, {H, b}}, Or(a, b)),
Fun({{b, Bool}, {a, Bool}, {H, b}},
Discharge(Not(a), b, Fun({H1, Not(a)}, H))));
// Disj2 : Pi (b a : Bool) (H : b), Or(a, b)
env->add_theorem(disj2_fn_name, Pi({{b, Bool}, {a, Bool}, {H, b}}, Or(a, b)),
Fun({{b, Bool}, {a, Bool}, {H, b}},
Discharge(Not(a), b, Fun({H1, Not(a)}, H))));
// DisjCases : Pi (a b c: Bool) (H1 : Or(a, b)) (H2 : a -> c) (H3 : b -> c), c */
env->add_theorem(disj_cases_fn_name, Pi({{a, Bool}, {b, Bool}, {c, Bool}, {H1, Or(a, b)}, {H2, a >> c}, {H3, b >> c}}, c),
Fun({{a, Bool}, {b, Bool}, {c, Bool}, {H1, Or(a, b)}, {H2, a >> c}, {H3, b >> c}},
EqMP(Not(Not(c)), c, DoubleNeg(c),
Discharge(Not(c), False,
Fun({H, Not(c)},
Absurd(c,
MP(b, c, Discharge(b, c, H3),
MP(Not(a), b, H1,
// Not(a)
MT(a, c, Discharge(a, c, H2), H))),
H))))));
// DisjCases : Pi (a b c: Bool) (H1 : Or(a, b)) (H2 : a -> c) (H3 : b -> c), c */
env->add_theorem(disj_cases_fn_name, Pi({{a, Bool}, {b, Bool}, {c, Bool}, {H1, Or(a, b)}, {H2, a >> c}, {H3, b >> c}}, c),
Fun({{a, Bool}, {b, Bool}, {c, Bool}, {H1, Or(a, b)}, {H2, a >> c}, {H3, b >> c}},
EqMP(Not(Not(c)), c, DoubleNeg(c),
Discharge(Not(c), False,
Fun({H, Not(c)},
Absurd(c,
MP(b, c, Discharge(b, c, H3),
MP(Not(a), b, H1,
// Not(a)
MT(a, c, Discharge(a, c, H2), H))),
H))))));
// Refute : Pi {a : Bool} (H : not a -> false), a */
env->add_theorem(refute_fn_name, Pi({{a, Bool}, {H, Not(a) >> False}}, a),
Fun({{a, Bool}, {H, Not(a) >> False}},
DisjCases(a, Not(a), a, EM(a), Fun({H1, a}, H1), Fun({H1, Not(a)}, FalseElim(a, H(H1))))));
// Refute : Pi {a : Bool} (H : not a -> false), a */
env->add_theorem(refute_fn_name, Pi({{a, Bool}, {H, Not(a) >> False}}, a),
Fun({{a, Bool}, {H, Not(a) >> False}},
DisjCases(a, Not(a), a, EM(a), Fun({H1, a}, H1), Fun({H1, Not(a)}, FalseElim(a, H(H1))))));
// Symm : Pi (A : Type u) (a b : A) (H : a = b), b = a
env->add_theorem(symm_fn_name, Pi({{A, TypeU}, {a, A}, {b, A}, {H, Eq(a, b)}}, Eq(b, a)),
Fun({{A, TypeU}, {a, A}, {b, A}, {H, Eq(a, b)}},
Subst(A, a, b, Fun({x, A}, Eq(x, a)), Refl(A, a), H)));
// Symm : Pi (A : Type u) (a b : A) (H : a = b), b = a
env->add_theorem(symm_fn_name, Pi({{A, TypeU}, {a, A}, {b, A}, {H, Eq(a, b)}}, Eq(b, a)),
Fun({{A, TypeU}, {a, A}, {b, A}, {H, Eq(a, b)}},
Subst(A, a, b, Fun({x, A}, Eq(x, a)), Refl(A, a), H)));
// Trans: Pi (A: Type u) (a b c : A) (H1 : a = b) (H2 : b = c), a = c
env->add_theorem(trans_fn_name, Pi({{A, TypeU}, {a, A}, {b, A}, {c, A}, {H1, Eq(a, b)}, {H2, Eq(b, c)}}, Eq(a, c)),
Fun({{A, TypeU}, {a, A}, {b, A}, {c, A}, {H1, Eq(a, b)}, {H2, Eq(b, c)}},
Subst(A, b, c, Fun({x, A}, Eq(a, x)), H1, H2)));
// Trans: Pi (A: Type u) (a b c : A) (H1 : a = b) (H2 : b = c), a = c
env->add_theorem(trans_fn_name, Pi({{A, TypeU}, {a, A}, {b, A}, {c, A}, {H1, Eq(a, b)}, {H2, Eq(b, c)}}, Eq(a, c)),
Fun({{A, TypeU}, {a, A}, {b, A}, {c, A}, {H1, Eq(a, b)}, {H2, Eq(b, c)}},
Subst(A, b, c, Fun({x, A}, Eq(a, x)), H1, H2)));
// EqTElim : Pi (a : Bool) (H : a = True), a
env->add_theorem(eqt_elim_fn_name, Pi({{a, Bool}, {H, Eq(a, True)}}, a),
Fun({{a, Bool}, {H, Eq(a, True)}},
EqMP(True, a, Symm(Bool, a, True, H), Trivial)));
// EqTElim : Pi (a : Bool) (H : a = True), a
env->add_theorem(eqt_elim_fn_name, Pi({{a, Bool}, {H, Eq(a, True)}}, a),
Fun({{a, Bool}, {H, Eq(a, True)}},
EqMP(True, a, Symm(Bool, a, True, H), Trivial)));
// EqTIntro : Pi (a : Bool) (H : a), a = True
env->add_theorem(eqt_intro_fn_name, Pi({{a, Bool}, {H, a}}, Eq(a, True)),
Fun({{a, Bool}, {H, a}},
ImpAntisym(a, True,
Discharge(a, True, Fun({H1, a}, Trivial)),
Discharge(True, a, Fun({H2, True}, H)))));
// EqTIntro : Pi (a : Bool) (H : a), a = True
env->add_theorem(eqt_intro_fn_name, Pi({{a, Bool}, {H, a}}, Eq(a, True)),
Fun({{a, Bool}, {H, a}},
ImpAntisym(a, True,
Discharge(a, True, Fun({H1, a}, Trivial)),
Discharge(True, a, Fun({H2, True}, H)))));
env->add_theorem(name("OrIdempotent"), Pi({a, Bool}, Eq(Or(a, a), a)),
Fun({a, Bool}, Case(Fun({x, Bool}, Eq(Or(x, x), x)), Trivial, Trivial, a)));
env->add_theorem(name("OrIdempotent"), Pi({a, Bool}, Eq(Or(a, a), a)),
Fun({a, Bool}, Case(Fun({x, Bool}, Eq(Or(x, x), x)), Trivial, Trivial, a)));
env->add_theorem(name("OrComm"), Pi({{a, Bool}, {b, Bool}}, Eq(Or(a, b), Or(b, a))),
Fun({{a, Bool}, {b, Bool}},
Case(Fun({x, Bool}, Eq(Or(x, b), Or(b, x))),
Case(Fun({y, Bool}, Eq(Or(True, y), Or(y, True))), Trivial, Trivial, b),
Case(Fun({y, Bool}, Eq(Or(False, y), Or(y, False))), Trivial, Trivial, b),
a)));
env->add_theorem(name("OrComm"), Pi({{a, Bool}, {b, Bool}}, Eq(Or(a, b), Or(b, a))),
Fun({{a, Bool}, {b, Bool}},
Case(Fun({x, Bool}, Eq(Or(x, b), Or(b, x))),
Case(Fun({y, Bool}, Eq(Or(True, y), Or(y, True))), Trivial, Trivial, b),
Case(Fun({y, Bool}, Eq(Or(False, y), Or(y, False))), Trivial, Trivial, b),
a)));
env->add_theorem(name("OrAssoc"), Pi({{a, Bool}, {b, Bool}, {c, Bool}}, Eq(Or(Or(a, b), c), Or(a, Or(b, c)))),
Fun({{a, Bool}, {b, Bool}, {c, Bool}},
Case(Fun({x, Bool}, Eq(Or(Or(x, b), c), Or(x, Or(b, c)))),
Case(Fun({y, Bool}, Eq(Or(Or(True, y), c), Or(True, Or(y, c)))),
Case(Fun({z, Bool}, Eq(Or(Or(True, True), z), Or(True, Or(True, z)))), Trivial, Trivial, c),
Case(Fun({z, Bool}, Eq(Or(Or(True, False), z), Or(True, Or(False, z)))), Trivial, Trivial, c), b),
Case(Fun({y, Bool}, Eq(Or(Or(False, y), c), Or(False, Or(y, c)))),
Case(Fun({z, Bool}, Eq(Or(Or(False, True), z), Or(False, Or(True, z)))), Trivial, Trivial, c),
Case(Fun({z, Bool}, Eq(Or(Or(False, False), z), Or(False, Or(False, z)))), Trivial, Trivial, c), b), a)));
env->add_theorem(name("OrAssoc"), Pi({{a, Bool}, {b, Bool}, {c, Bool}}, Eq(Or(Or(a, b), c), Or(a, Or(b, c)))),
Fun({{a, Bool}, {b, Bool}, {c, Bool}},
Case(Fun({x, Bool}, Eq(Or(Or(x, b), c), Or(x, Or(b, c)))),
Case(Fun({y, Bool}, Eq(Or(Or(True, y), c), Or(True, Or(y, c)))),
Case(Fun({z, Bool}, Eq(Or(Or(True, True), z), Or(True, Or(True, z)))), Trivial, Trivial, c),
Case(Fun({z, Bool}, Eq(Or(Or(True, False), z), Or(True, Or(False, z)))), Trivial, Trivial, c), b),
Case(Fun({y, Bool}, Eq(Or(Or(False, y), c), Or(False, Or(y, c)))),
Case(Fun({z, Bool}, Eq(Or(Or(False, True), z), Or(False, Or(True, z)))), Trivial, Trivial, c),
Case(Fun({z, Bool}, Eq(Or(Or(False, False), z), Or(False, Or(False, z)))), Trivial, Trivial, c), b), a)));
// Congr1 : Pi (A : Type u) (B : A -> Type u) (f g: Pi (x : A) B x) (a : A) (H : f = g), f a = g a
env->add_theorem(congr1_fn_name, Pi({{A, TypeU}, {B, A_arrow_u}, {f, piABx}, {g, piABx}, {a, A}, {H, Eq(f, g)}}, Eq(f(a), g(a))),
Fun({{A, TypeU}, {B, A_arrow_u}, {f, piABx}, {g, piABx}, {a, A}, {H, Eq(f, g)}},
Subst(piABx, f, g, Fun({h, piABx}, Eq(f(a), h(a))), Refl(B(a), f(a)), H)));
// Congr1 : Pi (A : Type u) (B : A -> Type u) (f g: Pi (x : A) B x) (a : A) (H : f = g), f a = g a
env->add_theorem(congr1_fn_name, Pi({{A, TypeU}, {B, A_arrow_u}, {f, piABx}, {g, piABx}, {a, A}, {H, Eq(f, g)}}, Eq(f(a), g(a))),
Fun({{A, TypeU}, {B, A_arrow_u}, {f, piABx}, {g, piABx}, {a, A}, {H, Eq(f, g)}},
Subst(piABx, f, g, Fun({h, piABx}, Eq(f(a), h(a))), Refl(B(a), f(a)), H)));
// Congr2 : Pi (A : Type u) (B : A -> Type u) (a b : A) (f : Pi (x : A) B x) (H : a = b), f a = f b
env->add_theorem(congr2_fn_name, Pi({{A, TypeU}, {B, A_arrow_u}, {a, A}, {b, A}, {f, piABx}, {H, Eq(a, b)}}, Eq(f(a), f(b))),
Fun({{A, TypeU}, {B, A_arrow_u}, {a, A}, {b, A}, {f, piABx}, {H, Eq(a, b)}},
Subst(A, a, b, Fun({x, A}, Eq(f(a), f(x))), Refl(B(a), f(a)), H)));
// Congr2 : Pi (A : Type u) (B : A -> Type u) (a b : A) (f : Pi (x : A) B x) (H : a = b), f a = f b
env->add_theorem(congr2_fn_name, Pi({{A, TypeU}, {B, A_arrow_u}, {a, A}, {b, A}, {f, piABx}, {H, Eq(a, b)}}, Eq(f(a), f(b))),
Fun({{A, TypeU}, {B, A_arrow_u}, {a, A}, {b, A}, {f, piABx}, {H, Eq(a, b)}},
Subst(A, a, b, Fun({x, A}, Eq(f(a), f(x))), Refl(B(a), f(a)), H)));
// Congr : Pi (A : Type u) (B : A -> Type u) (f g : Pi (x : A) B x) (a b : A) (H1 : f = g) (H2 : a = b), f a = g b
env->add_theorem(congr_fn_name, Pi({{A, TypeU}, {B, A_arrow_u}, {f, piABx}, {g, piABx}, {a, A}, {b, A}, {H1, Eq(f, g)}, {H2, Eq(a, b)}}, Eq(f(a), g(b))),
Fun({{A, TypeU}, {B, A_arrow_u}, {f, piABx}, {g, piABx}, {a, A}, {b, A}, {H1, Eq(f, g)}, {H2, Eq(a, b)}},
HTrans(B(a), B(b), B(b), f(a), f(b), g(b),
Congr2(A, B, a, b, f, H2), Congr1(A, B, f, g, b, H1))));
// Congr : Pi (A : Type u) (B : A -> Type u) (f g : Pi (x : A) B x) (a b : A) (H1 : f = g) (H2 : a = b), f a = g b
env->add_theorem(congr_fn_name, Pi({{A, TypeU}, {B, A_arrow_u}, {f, piABx}, {g, piABx}, {a, A}, {b, A}, {H1, Eq(f, g)}, {H2, Eq(a, b)}}, Eq(f(a), g(b))),
Fun({{A, TypeU}, {B, A_arrow_u}, {f, piABx}, {g, piABx}, {a, A}, {b, A}, {H1, Eq(f, g)}, {H2, Eq(a, b)}},
HTrans(B(a), B(b), B(b), f(a), f(b), g(b),
Congr2(A, B, a, b, f, H2), Congr1(A, B, f, g, b, H1))));
// ForallElim : Pi (A : Type u) (P : A -> bool) (H : (forall A P)) (a : A), P a
env->add_theorem(forall_elim_fn_name, Pi({{A, TypeU}, {P, A_pred}, {H, mk_forall(A, P)}, {a, A}}, P(a)),
Fun({{A, TypeU}, {P, A_pred}, {H, mk_forall(A, P)}, {a, A}},
EqTElim(P(a), Congr1(A, Fun({x, A}, Bool), P, Fun({x, A}, True), a, H))));
// ForallElim : Pi (A : Type u) (P : A -> bool) (H : (forall A P)) (a : A), P a
env->add_theorem(forall_elim_fn_name, Pi({{A, TypeU}, {P, A_pred}, {H, mk_forall(A, P)}, {a, A}}, P(a)),
Fun({{A, TypeU}, {P, A_pred}, {H, mk_forall(A, P)}, {a, A}},
EqTElim(P(a), Congr1(A, Fun({x, A}, Bool), P, Fun({x, A}, True), a, H))));
// ForallIntro : Pi (A : Type u) (P : A -> bool) (H : Pi (x : A), P x), (forall A P)
env->add_theorem(forall_intro_fn_name, Pi({{A, TypeU}, {P, A_pred}, {H, Pi({x, A}, P(x))}}, Forall(A, P)),
Fun({{A, TypeU}, {P, A_pred}, {H, Pi({x, A}, P(x))}},
Trans(A_pred, P, Fun({x, A}, P(x)), Fun({x, A}, True),
Symm(A_pred, Fun({x, A}, P(x)), P, Eta(A, Fun({x, A}, Bool), P)), // P == fun x : A, P x
Abst(A, Fun({x, A}, Bool), Fun({x, A}, P(x)), Fun({x, A}, True), Fun({x, A}, EqTIntro(P(x), H(x)))))));
// ForallIntro : Pi (A : Type u) (P : A -> bool) (H : Pi (x : A), P x), (forall A P)
env->add_theorem(forall_intro_fn_name, Pi({{A, TypeU}, {P, A_pred}, {H, Pi({x, A}, P(x))}}, Forall(A, P)),
Fun({{A, TypeU}, {P, A_pred}, {H, Pi({x, A}, P(x))}},
Trans(A_pred, P, Fun({x, A}, P(x)), Fun({x, A}, True),
Symm(A_pred, Fun({x, A}, P(x)), P, Eta(A, Fun({x, A}, Bool), P)), // P == fun x : A, P x
Abst(A, Fun({x, A}, Bool), Fun({x, A}, P(x)), Fun({x, A}, True), Fun({x, A}, EqTIntro(P(x), H(x)))))));
// ExistsElim : Pi (A : Type U) (P : A -> Bool) (B : Bool) (H1 : exists x : A, P x) (H2 : Pi (a : A) (H : P a), B) : B :=
env->add_theorem(exists_elim_fn_name, Pi({{A, TypeU}, {P, A_pred}, {B, Bool}, {H1, mk_exists(A, P)}, {H2, Pi({{a, A}, {H, P(a)}}, B)}}, B),
Fun({{A, TypeU}, {P, A_pred}, {B, Bool}, {H1, mk_exists(A, P)}, {H2, Pi({{a, A}, {H, P(a)}}, B)}},
Refute(B, Fun({R, Not(B)},
Absurd(mk_forall(A, Fun({x, A}, Not(P(x)))),
ForallIntro(A, Fun({x, A}, Not(P(x))), Fun({a, A}, MT(P(a), B, Discharge(P(a), B, Fun({H, P(a)}, H2(a, H))), R))),
H1)))));
// ExistsElim : Pi (A : Type U) (P : A -> Bool) (B : Bool) (H1 : exists x : A, P x) (H2 : Pi (a : A) (H : P a), B) : B :=
env->add_theorem(exists_elim_fn_name, Pi({{A, TypeU}, {P, A_pred}, {B, Bool}, {H1, mk_exists(A, P)}, {H2, Pi({{a, A}, {H, P(a)}}, B)}}, B),
Fun({{A, TypeU}, {P, A_pred}, {B, Bool}, {H1, mk_exists(A, P)}, {H2, Pi({{a, A}, {H, P(a)}}, B)}},
Refute(B, Fun({R, Not(B)},
Absurd(mk_forall(A, Fun({x, A}, Not(P(x)))),
ForallIntro(A, Fun({x, A}, Not(P(x))), Fun({a, A}, MT(P(a), B, Discharge(P(a), B, Fun({H, P(a)}, H2(a, H))), R))),
H1)))));
// ExistsIntro : Pi (A : Type u) (P : A -> bool) (a : A) (H : P a), exists A P
env->add_theorem(exists_intro_fn_name, Pi({{A, TypeU}, {P, A_pred}, {a, A}, {H, P(a)}}, mk_exists(A, P)),
Fun({{A, TypeU}, {P, A_pred}, {a, A}, {H, P(a)}},
Discharge(mk_forall(A, Fun({x, A}, Not(P(x)))), False,
Fun({H2, mk_forall(A, Fun({x, A}, Not(P(x))))},
Absurd(P(a), H, ForallElim(A, Fun({x, A}, Not(P(x))), H2, a))))));
// ExistsIntro : Pi (A : Type u) (P : A -> bool) (a : A) (H : P a), exists A P
env->add_theorem(exists_intro_fn_name, Pi({{A, TypeU}, {P, A_pred}, {a, A}, {H, P(a)}}, mk_exists(A, P)),
Fun({{A, TypeU}, {P, A_pred}, {a, A}, {H, P(a)}},
Discharge(mk_forall(A, Fun({x, A}, Not(P(x)))), False,
Fun({H2, mk_forall(A, Fun({x, A}, Not(P(x))))},
Absurd(P(a), H, ForallElim(A, Fun({x, A}, Not(P(x))), H2, a))))));
});
}
}

2
src/shell/CMakeLists.txt
View file

@ -7,8 +7,6 @@ add_custom_target(githash
DEPENDS ${LEAN_BINARY_DIR}/githash.h ${LEAN_SOURCE_DIR}/../.git/HEAD ${LEAN_SOURCE_DIR}/../.git/index
)
configure_file("${LEAN_SOURCE_DIR}/shell/version.h.in" "${LEAN_BINARY_DIR}/version.h")
include_directories("${LEAN_BINARY_DIR}")
add_executable(lean lean.cpp)
add_dependencies(lean githash)
target_link_libraries(lean ${EXTRA_LIBS})

34
src/shell/lean.cpp
View file

@ -36,7 +36,7 @@ using lean::notify_assertion_violation;
using lean::environment;
using lean::io_state;
enum class input_kind { Unspecified, Lean, Lua };
enum class input_kind { Unspecified, Lean, OLean, Lua };
static void on_ctrl_c(int ) {
lean::request_interrupt();
@ -51,12 +51,15 @@ static void display_help(std::ostream & out) {
std::cout << "Input format:\n";
std::cout << " --lean use parser for Lean default input format for files,\n";
std::cout << " with unknown extension (default)\n";
std::cout << " --olean use parser for Lean binary input format for files\n";
std::cout << " with unknown extension\n";
std::cout << " --lua use Lua parser for files with unknown extension\n";
std::cout << "Miscellaneous:\n";
std::cout << " --help -h display this message\n";
std::cout << " --version -v display version number\n";
std::cout << " --githash display the git commit hash number used to build this binary\n";
std::cout << " --path display the path used for finding Lean libraries and extensions\n";
std::cout << " --output=file -o save the final environment in binary format in the given file\n";
std::cout << " --luahook=num -c how often the Lua interpreter checks the interrupted flag,\n";
std::cout << " it is useful for interrupting non-terminating user scripts,\n";
std::cout << " 0 means 'do not check'.\n";
@ -83,10 +86,12 @@ static struct option g_long_options[] = {
{"version", no_argument, 0, 'v'},
{"help", no_argument, 0, 'h'},
{"lean", no_argument, 0, 'l'},
{"olean", no_argument, 0, 'b'},
{"lua", no_argument, 0, 'u'},
{"path", no_argument, 0, 'p'},
{"luahook", required_argument, 0, 'c'},
{"githash", no_argument, 0, 'g'},
{"output", required_argument, 0, 'o'},
#if defined(LEAN_USE_BOOST)
{"tstack", required_argument, 0, 's'},
#endif
@ -96,9 +101,11 @@ static struct option g_long_options[] = {
int main(int argc, char ** argv) {
lean::save_stack_info();
lean::register_modules();
bool export_objects = false;
std::string output;
input_kind default_k = input_kind::Lean; // default
while (true) {
int c = getopt_long(argc, argv, "lupgvhc:012s:012", g_long_options, NULL);
int c = getopt_long(argc, argv, "lupgvhc:012s:012o:", g_long_options, NULL);
if (c == -1)
break; // end of command line
switch (c) {
@ -117,6 +124,9 @@ int main(int argc, char ** argv) {
case 'u':
default_k = input_kind::Lua;
break;
case 'b':
default_k = input_kind::OLean;
break;
case 'c':
script_state::set_check_interrupt_freq(atoi(optarg));
break;
@ -126,6 +136,10 @@ int main(int argc, char ** argv) {
case 's':
lean::set_thread_stack_size(atoi(optarg)*1024);
break;
case 'o':
output = optarg;
export_objects = true;
break;
default:
std::cerr << "Unknown command line option\n";
display_help(std::cerr);
@ -146,7 +160,10 @@ int main(int argc, char ** argv) {
init_frontend(env, ios);
script_state S;
shell sh(env, &S);
return sh() ? 0 : 1;
int status = sh() ? 0 : 1;
if (export_objects)
env->export_objects(output);
return status;
} else {
lean_assert(default_k == input_kind::Lua);
script_state S;
@ -164,6 +181,8 @@ int main(int argc, char ** argv) {
if (ext) {
if (strcmp(ext, "lean") == 0) {
k = input_kind::Lean;
} else if (strcmp(ext, "olean") == 0) {
k = input_kind::OLean;
} else if (strcmp(ext, "lua") == 0) {
k = input_kind::Lua;
}
@ -176,6 +195,13 @@ int main(int argc, char ** argv) {
}
if (!parse_commands(env, ios, in, &S, false, false))
ok = false;
} else if (k == input_kind::OLean) {
try {
env->import(std::string(argv[i]), ios);
} catch (lean::exception & ex) {
std::cerr << "Failed to load binary file '" << argv[i] << "': " << ex.what() << "\n";
ok = false;
}
} else if (k == input_kind::Lua) {
try {
S.dofile(argv[i]);
@ -187,6 +213,8 @@ int main(int argc, char ** argv) {
lean_unreachable(); // LCOV_EXCL_LINE
}
}
if (export_objects)
env->export_objects(output);
return ok ? 0 : 1;
}
}

8
src/util/lean_path.cpp
View file

@ -155,7 +155,7 @@ std::string name_to_file(name const & fname) {
return fname.to_string(g_sep_str.c_str());
}
std::string find_file(std::string fname) {
std::string find_file(std::string fname, std::initializer_list<char const *> const & extensions) {
bool is_known = is_known_file_ext(fname);
fname = normalize_path(fname);
for (auto path : g_lean_path_vector) {
@ -163,7 +163,7 @@ std::string find_file(std::string fname) {
if (auto r = check_file(path, fname))
return *r;
} else {
for (auto ext : { ".olean", ".lean", ".lua" }) {
for (auto ext : extensions) {
if (auto r = check_file(path, fname, ext))
return *r;
}
@ -172,6 +172,10 @@ std::string find_file(std::string fname) {
throw exception(sstream() << "file '" << fname << "' not found in the LEAN_PATH");
}
std::string find_file(std::string fname) {
return find_file(fname, {".olean", ".lean", ".lua"});
}
char const * get_lean_path() {
return g_lean_path.c_str();
}

3
src/util/lean_path.h
View file

@ -18,6 +18,9 @@ char const * get_lean_path();
*/
std::string find_file(std::string fname);
std::string find_file(std::string fname, std::initializer_list<char const *> const & exts);
/** \brief Return true iff fname ends with ".lean" */
bool is_lean_file(std::string const & fname);
/** \brief Return true iff fname ends with ".olean" */

0
src/shell/version.h.in → src/version.h.in
View file