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

feat(kernel/builtin): add is_* functions

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-11-29 11:35:58 -08:00
parent 18eb9e427f
commit a9eb2a9307
4 changed files with 83 additions and 22 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

36
src/kernel/builtin.cpp
View file

@ -66,9 +66,7 @@ public:
};
expr const Bool = mk_value(*(new bool_type_value()));
expr mk_bool_type() { return Bool; }
bool is_bool(expr const & e) {
return e == Bool || (is_constant(e) && const_name(e) == to_value(Bool).get_name());
}
MK_IS_BUILTIN(is_bool, Bool)
// =======================================
// =======================================
@ -153,16 +151,48 @@ public:
}
};
MK_BUILTIN(if_fn, if_fn_value);
MK_IS_BUILTIN(is_if_fn, mk_if_fn());
bool is_if(expr const & n, expr & c, expr & t, expr & e) {
if (is_if(n)) {
c = arg(n, 2);
t = arg(n, 3);
e = arg(n, 4);
return true;
} else {
return false;
}
}
// =======================================
MK_CONSTANT(implies_fn, name("implies"));
MK_IS_BINARY_APP(is_implies)
MK_CONSTANT(iff_fn, name("iff"));
MK_IS_BINARY_APP(is_iff)
MK_CONSTANT(and_fn, name("and"));
MK_IS_BINARY_APP(is_and)
MK_CONSTANT(or_fn, name("or"));
MK_IS_BINARY_APP(is_or)
MK_CONSTANT(not_fn, name("not"));
bool is_not(expr const & e, expr & a) {
if (is_not(e)) {
a = arg(e, 1);
return true;
} else {
return false;
}
}
MK_CONSTANT(forall_fn, name("forall"));
MK_CONSTANT(exists_fn, name("exists"));
MK_CONSTANT(homo_eq_fn, name("eq"));
bool is_homo_eq(expr const & e, expr & lhs, expr & rhs) {
if (is_homo_eq(e)) {
lhs = arg(e, 2);
rhs = arg(e, 3);
return true;
} else {
return false;
}
}
// Axioms
MK_CONSTANT(mp_fn, name("MP"));

45
src/kernel/builtin.h
View file

@ -51,6 +51,9 @@ bool is_false(expr const & e);
/** \brief Return the Lean If-Then-Else operator. It has type: pi (A : Type), bool -> A -> A -> A */
expr mk_if_fn();
bool is_if_fn(expr const & e);
inline bool is_if(expr const & e) { return is_app(e) && is_if_fn(arg(e, 0)); }
bool is_if(expr const & n, expr & c, expr & t, expr & e);
/** \brief Return the term (if A c t e) */
inline expr mk_if(expr const & A, expr const & c, expr const & t, expr const & e) { return mk_app(mk_if_fn(), A, c, t, e); }
inline expr If(expr const & A, expr const & c, expr const & t, expr const & e) { return mk_if(A, c, t, e); }
@ -60,6 +63,9 @@ inline expr bIf(expr const & c, expr const & t, expr const & e) { return mk_bool
/** \brief Return the Lean Implies operator */
expr mk_implies_fn();
bool is_implies_fn(expr const & e);
inline bool is_implies(expr const & e) { return is_app(e) && is_implies_fn(arg(e, 0)); }
bool is_implies(expr const & e, expr & a1, expr & a2);
/** \brief Return the term (e1 => e2) */
inline expr mk_implies(expr const & e1, expr const & e2) { return mk_app(mk_implies_fn(), e1, e2); }
inline expr mk_implies(unsigned num_args, expr const * args) { lean_assert(num_args >= 2); return mk_bin_rop(mk_implies_fn(), False, num_args, args); }
@ -68,6 +74,9 @@ inline expr Implies(std::initializer_list<expr> const & l) { return mk_implies(l
/** \brief Return the Lean Iff operator */
expr mk_iff_fn();
bool is_iff_fn(expr const & e);
inline bool is_iff(expr const & e) { return is_app(e) && is_iff_fn(arg(e, 0)); }
bool is_iff(expr const & e, expr & a1, expr & a2);
/** \brief Return (e1 iff e2) */
inline expr mk_iff(expr const & e1, expr const & e2) { return mk_app(mk_iff_fn(), e1, e2); }
inline expr mk_iff(unsigned num_args, expr const * args) { return mk_bin_rop(mk_iff_fn(), True, num_args, args); }
@ -76,6 +85,9 @@ inline expr Iff(std::initializer_list<expr> const & l) { return mk_iff(l.size(),
/** \brief Return the Lean And operator */
expr mk_and_fn();
bool is_and_fn(expr const & e);
inline bool is_and(expr const & e) { return is_app(e) && is_and_fn(arg(e, 0)); }
bool is_and(expr const & e, expr & a1, expr & a2);
/** \brief Return (e1 and e2) */
inline expr mk_and(expr const & e1, expr const & e2) { return mk_app(mk_and_fn(), e1, e2); }
inline expr mk_and(unsigned num_args, expr const * args) { return mk_bin_rop(mk_and_fn(), True, num_args, args); }
@ -84,6 +96,9 @@ inline expr And(std::initializer_list<expr> const & l) { return mk_and(l.size(),
/** \brief Return the Lean Or operator */
expr mk_or_fn();
bool is_or_fn(expr const & e);
inline bool is_or(expr const & e) { return is_app(e) && is_or_fn(arg(e, 0)); }
bool is_or(expr const & e, expr & a1, expr & a2);
/** \brief Return (e1 Or e2) */
inline expr mk_or(expr const & e1, expr const & e2) { return mk_app(mk_or_fn(), e1, e2); }
inline expr mk_or(unsigned num_args, expr const * args) { return mk_bin_rop(mk_or_fn(), False, num_args, args); }
@ -92,24 +107,34 @@ inline expr Or(std::initializer_list<expr> const & l) { return mk_or(l.size(), l
/** \brief Return the Lean not operator */
expr mk_not_fn();
bool is_not_fn(expr const & e);
inline bool is_not(expr const & e) { return is_app(e) && is_not_fn(arg(e, 0)); }
bool is_not(expr const & e, expr & a1);
/** \brief Return (Not e) */
inline expr mk_not(expr const & e) { return mk_app(mk_not_fn(), e); }
inline expr Not(expr const & e) { return mk_not(e); }
/** \brief Return the Lean forall operator. It has type: <tt>Pi (A : Type), (A -> bool) -> Bool</tt> */
expr mk_forall_fn();
bool is_forall_fn(expr const & e);
inline bool is_forall(expr const & e) { return is_app(e) && is_forall_fn(arg(e, 0)); }
/** \brief Return the term (Forall A P), where A is a type and P : A -> bool */
inline expr mk_forall(expr const & A, expr const & P) { return mk_app(mk_forall_fn(), A, P); }
inline expr Forall(expr const & A, expr const & P) { return mk_forall(A, P); }
/** \brief Return the Lean exists operator. It has type: <tt>Pi (A : Type), (A -> Bool) -> Bool</tt> */
expr mk_exists_fn();
bool is_exists_fn(expr const & e);
inline bool is_exists(expr const & e) { return is_app(e) && is_exists_fn(arg(e, 0)); }
/** \brief Return the term (exists A P), where A is a type and P : A -> bool */
inline expr mk_exists(expr const & A, expr const & P) { return mk_app(mk_exists_fn(), A, P); }
inline expr Exists(expr const & A, expr const & P) { return mk_exists(A, P); }
/** \brief Homogeneous equality. It has type: <tt>Pi (A : Type), A -> A -> Bool</tt> */
expr mk_homo_eq_fn();
bool is_homo_eq_fn(expr const & e);
inline bool is_homo_eq(expr const & e) { return is_app(e) && is_homo_eq_fn(arg(e, 0)); }
bool is_homo_eq(expr const & e, expr & a1, expr & a2);
/** \brief Return the term (homo_eq A l r) */
inline expr mk_homo_eq(expr const & A, expr const & l, expr const & r) { return mk_app(mk_homo_eq_fn(), A, l, r); }
inline expr hEq(expr const & A, expr const & l, expr const & r) { return mk_homo_eq(A, l, r); }
@ -177,5 +202,25 @@ static name Name ## _name = NameObj; \
expr mk_##Name() { \
static thread_local expr r = mk_constant(Name ## _name); \
return r ; \
} \
bool is_ ## Name(expr const & e) { \
return is_constant(e) && const_name(e) == Name ## _name; \
}
#define MK_IS_BUILTIN(Name, Builtin) \
bool Name(expr const & e) { \
expr const & v = Builtin; \
return e == v || (is_constant(e) && const_name(e) == to_value(v).get_name()); \
}
#define MK_IS_BINARY_APP(Name) \
bool Name(expr const & e, expr & a1, expr & a2) { \
if (Name(e)) { \
a1 = arg(e, 1); \
a2 = arg(e, 2); \
return true; \
} else { \
return false; \
} \
}
}

2
src/library/kernel_bindings.cpp
View file

@ -1560,6 +1560,8 @@ static void open_metavar_env(lua_State * L) {
SET_GLOBAL_FUN(instantiate_metavars, "instantiate_metavars");
}
void open_kernel_module(lua_State * L) {
open_level(L);
open_local_context(L);

22
src/library/tactic/boolean.cpp
View file

@ -16,23 +16,8 @@ Author: Leonardo de Moura
#include "library/tactic/tactic.h"
namespace lean {
bool is_app_of(expr const & e, expr const & f) {
return is_app(e) && arg(e, 0) == f;
}
bool is_app_of(expr const & e, expr const & f, expr & arg1, expr & arg2) {
if (is_app_of(e, f)) {
arg1 = arg(e, 1);
arg2 = arg(e, 2);
return true;
} else {
return false;
}
}
tactic conj_tactic(bool all) {
return mk_tactic01([=](environment const &, io_state const &, proof_state const & s) -> optional<proof_state> {
expr andfn = mk_and_fn();
bool found = false;
buffer<std::pair<name, goal>> new_goals_buf;
list<std::pair<name, expr>> proof_info;
@ -41,7 +26,7 @@ tactic conj_tactic(bool all) {
goal const & g = p.second;
expr const & c = g.get_conclusion();
expr c1, c2;
if ((all || !found) && is_app_of(c, andfn, c1, c2)) {
if ((all || !found) && is_and(c, c1, c2)) {
found = true;
name const & n = p.first;
proof_info.emplace_front(n, c);
@ -80,7 +65,7 @@ tactic imp_tactic(name const & H_name, bool all) {
goals new_goals = map_goals(s, [&](name const & g_name, goal const & g) -> goal {
expr const & c = g.get_conclusion();
expr new_h, new_c;
if ((all || !found) && is_app_of(c, impfn, new_h, new_c)) {
if ((all || !found) && is_implies(c, new_h, new_c)) {
found = true;
name new_h_name = g.mk_unique_hypothesis_name(H_name);
proof_info.emplace_front(g_name, new_h_name, c);
@ -113,7 +98,6 @@ tactic imp_tactic(name const & H_name, bool all) {
tactic conj_hyp_tactic(bool all) {
return mk_tactic01([=](environment const &, io_state const &, proof_state const & s) -> optional<proof_state> {
expr andfn = mk_and_fn();
bool found = false;
list<std::pair<name, hypotheses>> proof_info; // goal name -> expanded hypotheses
goals new_goals = map_goals(s, [&](name const & ng, goal const & g) -> goal {
@ -124,7 +108,7 @@ tactic conj_hyp_tactic(bool all) {
name const & H_name = p.first;
expr const & H_prop = p.second;
expr H1, H2;
if ((all || !found) && is_app_of(H_prop, andfn, H1, H2)) {
if ((all || !found) && is_and(H_prop, H1, H2)) {
found = true;
proof_info_data = add_hypothesis(p, proof_info_data);
new_hyp_buf.emplace_back(name(H_name, 1), H1);