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

fix(library/simplifier): include flag indicating if the proof generated by simplifier is a homogenous or heterogenous equality, use flag to fix bug in the simp_tactic

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-01-29 12:01:01 -08:00
parent f0a2d3627e
commit 069e5edf6b
11 changed files with 88 additions and 57 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/builtin/heq.lean
View file

@ -13,6 +13,9 @@ theorem to_heq {A : TypeU} {a b : A} (H : a = b) : a == b
theorem hrefl {A : TypeU} (a : A) : a == a
:= to_heq (refl a)
theorem heqt_elim {a : Bool} (H : a == true) : a
:= eqt_elim (to_eq H)
axiom hsymm {A B : TypeU} {a : A} {b : B} : a == b → b == a
axiom htrans {A B C : TypeU} {a : A} {b : B} {c : C} : a == b → b == c → a == c

BIN
src/builtin/obj/heq.olean
View file

Binary file not shown.

1
src/library/heq_decls.cpp
View file

@ -11,6 +11,7 @@ MK_CONSTANT(heq_eq_fn, name("heq_eq"));
MK_CONSTANT(to_eq_fn, name("to_eq"));
MK_CONSTANT(to_heq_fn, name("to_heq"));
MK_CONSTANT(hrefl_fn, name("hrefl"));
MK_CONSTANT(heqt_elim_fn, name("heqt_elim"));
MK_CONSTANT(hsymm_fn, name("hsymm"));
MK_CONSTANT(htrans_fn, name("htrans"));
MK_CONSTANT(hcongr_fn, name("hcongr"));

3
src/library/heq_decls.h
View file

@ -21,6 +21,9 @@ inline expr mk_to_heq_th(expr const & e1, expr const & e2, expr const & e3, expr
expr mk_hrefl_fn();
bool is_hrefl_fn(expr const & e);
inline expr mk_hrefl_th(expr const & e1, expr const & e2) { return mk_app({mk_hrefl_fn(), e1, e2}); }
expr mk_heqt_elim_fn();
bool is_heqt_elim_fn(expr const & e);
inline expr mk_heqt_elim_th(expr const & e1, expr const & e2) { return mk_app({mk_heqt_elim_fn(), e1, e2}); }
expr mk_hsymm_fn();
bool is_hsymm_fn(expr const & e);
inline expr mk_hsymm_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_hsymm_fn(), e1, e2, e3, e4, e5}); }

57
src/library/simplifier/simplifier.cpp
View file

@ -121,20 +121,6 @@ static name g_unique = name::mk_internal_unique_name();
class simplifier_cell::imp {
friend class simplifier_cell;
friend class simplifier;
struct result {
expr m_expr; // the result of a simplification step
optional<expr> m_proof; // a proof that the result is equal to the input (when m_proofs_enabled)
bool m_heq_proof; // true if the proof has type lhs == rhs (i.e., it is a heterogeneous equality)
result() {}
explicit result(expr const & out, bool heq_proof = false):
m_expr(out), m_heq_proof(heq_proof) {}
result(expr const & out, expr const & pr, bool heq_proof = false):
m_expr(out), m_proof(pr), m_heq_proof(heq_proof) {}
result(expr const & out, optional<expr> const & pr, bool heq_proof = false):
m_expr(out), m_proof(pr), m_heq_proof(heq_proof) {}
bool is_heq_proof() const { return m_heq_proof; }
result update_expr(expr const & new_e) const { return result(new_e, m_proof, m_heq_proof); }
};
typedef std::vector<rewrite_rule_set> rule_sets;
typedef expr_map<result> cache;
@ -931,6 +917,8 @@ class simplifier_cell::imp {
if (!d_res.m_proof) {
// No proof available. So d should be definitionally equal to True
d_proof = mk_trivial();
} else if (d_res.m_heq_proof) {
d_proof = mk_heqt_elim_th(d, *d_res.m_proof);
} else {
d_proof = mk_eqt_elim_th(d, *d_res.m_proof);
}
@ -1502,7 +1490,7 @@ public:
m_next_idx = 0;
}
expr_pair operator()(expr const & e, context const & ctx, optional<ro_metavar_env> const & menv) {
result operator()(expr const & e, context const & ctx, optional<ro_metavar_env> const & menv) {
set_ctx(ctx);
if (m_menv.update(menv))
m_cache.clear();
@ -1510,7 +1498,10 @@ public:
m_depth = 0;
try {
auto r = simplify(e);
return mk_pair(r.m_expr, get_proof(r));
if (m_proofs_enabled && !r.get_proof())
return r.update_proof(get_proof(r));
else
return r;
} catch (stack_space_exception & ex) {
throw simplifier_stack_space_exception();
}
@ -1522,7 +1513,7 @@ simplifier_cell::simplifier_cell(ro_environment const & env, options const & o,
m_ptr(new imp(env, o, num_rs, rs, monitor)) {
}
expr_pair simplifier_cell::operator()(expr const & e, context const & ctx, optional<ro_metavar_env> const & menv) {
simplifier_cell::result simplifier_cell::operator()(expr const & e, context const & ctx, optional<ro_metavar_env> const & menv) {
return m_ptr->operator()(e, ctx, menv);
}
void simplifier_cell::clear() { return m_ptr->m_cache.clear(); }
@ -1547,17 +1538,17 @@ ro_simplifier::ro_simplifier(weak_ref const & r) {
m_ptr = r.lock();
}
expr_pair simplify(expr const & e, ro_environment const & env, context const & ctx, options const & opts,
unsigned num_rs, rewrite_rule_set const * rs,
optional<ro_metavar_env> const & menv,
std::shared_ptr<simplifier_monitor> const & monitor) {
simplifier::result simplify(expr const & e, ro_environment const & env, context const & ctx, options const & opts,
unsigned num_rs, rewrite_rule_set const * rs,
optional<ro_metavar_env> const & menv,
std::shared_ptr<simplifier_monitor> const & monitor) {
return simplifier(env, opts, num_rs, rs, monitor)(e, ctx, menv);
}
expr_pair simplify(expr const & e, ro_environment const & env, context const & ctx, options const & opts,
unsigned num_ns, name const * ns,
optional<ro_metavar_env> const & menv,
std::shared_ptr<simplifier_monitor> const & monitor) {
simplifier::result simplify(expr const & e, ro_environment const & env, context const & ctx, options const & opts,
unsigned num_ns, name const * ns,
optional<ro_metavar_env> const & menv,
std::shared_ptr<simplifier_monitor> const & monitor) {
buffer<rewrite_rule_set> rules;
for (unsigned i = 0; i < num_ns; i++)
rules.push_back(get_rewrite_rule_set(env, ns[i]));
@ -1736,16 +1727,17 @@ static int mk_simplifier(lua_State * L) {
static int simplifier_apply(lua_State * L) {
int nargs = lua_gettop(L);
expr_pair r;
simplifier::result r;
if (nargs == 2)
r = to_simplifier(L, 1)(to_expr(L, 2), context(), none_ro_menv());
else if (nargs == 3)
r = to_simplifier(L, 1)(to_expr(L, 2), to_context(L, 3), none_ro_menv());
else
r = to_simplifier(L, 1)(to_expr(L, 2), to_context(L, 3), some_ro_menv(to_metavar_env(L, 4)));
push_expr(L, r.first);
push_expr(L, r.second);
return 2;
push_expr(L, r.get_expr());
push_optional_expr(L, r.get_proof());
lua_pushboolean(L, r.is_heq_proof());
return 3;
}
static int simplifier_clear(lua_State * L) { to_simplifier(L, 1)->clear(); return 0; }
@ -1790,9 +1782,10 @@ static int simplify_core(lua_State * L, ro_shared_environment const & env) {
if (nargs >= 5)
ctx = to_context(L, 5);
auto r = simplify(e, env, ctx, opts, rules.size(), rules.data());
push_expr(L, r.first);
push_expr(L, r.second);
return 2;
push_expr(L, r.get_expr());
push_optional_expr(L, r.get_proof());
lua_pushboolean(L, r.is_heq_proof());
return 3;
}
static int simplify(lua_State * L) {

43
src/library/simplifier/simplifier.h
View file

@ -21,10 +21,30 @@ class simplifier_cell {
class imp;
std::unique_ptr<imp> m_ptr;
public:
/**
\brief Simplification result
*/
class result {
friend class imp;
expr m_expr; // new expression
optional<expr> m_proof; // a proof that the m_expr is equal to the input (when m_proofs_enabled)
bool m_heq_proof; // true if the proof has type lhs == rhs (i.e., it is a heterogeneous equality)
explicit result(expr const & out, bool heq_proof = false):m_expr(out), m_heq_proof(heq_proof) {}
result(expr const & out, expr const & pr, bool heq_proof = false):m_expr(out), m_proof(pr), m_heq_proof(heq_proof) {}
result(expr const & out, optional<expr> const & pr, bool heq_proof = false):
m_expr(out), m_proof(pr), m_heq_proof(heq_proof) {}
result update_expr(expr const & new_e) const { return result(new_e, m_proof, m_heq_proof); }
result update_proof(expr const & new_pr) const { return result(m_expr, new_pr, m_heq_proof); }
public:
result() {}
expr get_expr() const { return m_expr; }
optional<expr> get_proof() const { return m_proof; }
bool is_heq_proof() const { return m_heq_proof; }
};
simplifier_cell(ro_environment const & env, options const & o, unsigned num_rs, rewrite_rule_set const * rs,
std::shared_ptr<simplifier_monitor> const & monitor);
expr_pair operator()(expr const & e, context const & ctx, optional<ro_metavar_env> const & menv);
result operator()(expr const & e, context const & ctx, optional<ro_metavar_env> const & menv);
void clear();
unsigned get_depth() const;
@ -38,11 +58,12 @@ class simplifier {
friend class ro_simplifier;
std::shared_ptr<simplifier_cell> m_ptr;
public:
typedef simplifier_cell::result result;
simplifier(ro_environment const & env, options const & o, unsigned num_rs, rewrite_rule_set const * rs,
std::shared_ptr<simplifier_monitor> const & monitor);
simplifier_cell * operator->() const { return m_ptr.get(); }
simplifier_cell & operator*() const { return *(m_ptr.get()); }
expr_pair operator()(expr const & e, context const & ctx, optional<ro_metavar_env> const & menv) {
result operator()(expr const & e, context const & ctx, optional<ro_metavar_env> const & menv) {
return (*m_ptr)(e, ctx, menv);
}
};
@ -116,13 +137,13 @@ public:
virtual void rethrow() const;
};
expr_pair simplify(expr const & e, ro_environment const & env, context const & ctx, options const & pts,
unsigned num_rs, rewrite_rule_set const * rs,
optional<ro_metavar_env> const & menv = none_ro_menv(),
std::shared_ptr<simplifier_monitor> const & monitor = std::shared_ptr<simplifier_monitor>());
expr_pair simplify(expr const & e, ro_environment const & env, context const & ctx, options const & opts,
unsigned num_ns, name const * ns,
optional<ro_metavar_env> const & menv = none_ro_menv(),
std::shared_ptr<simplifier_monitor> const & monitor = std::shared_ptr<simplifier_monitor>());
simplifier::result simplify(expr const & e, ro_environment const & env, context const & ctx, options const & pts,
unsigned num_rs, rewrite_rule_set const * rs,
optional<ro_metavar_env> const & menv = none_ro_menv(),
std::shared_ptr<simplifier_monitor> const & monitor = std::shared_ptr<simplifier_monitor>());
simplifier::result simplify(expr const & e, ro_environment const & env, context const & ctx, options const & opts,
unsigned num_ns, name const * ns,
optional<ro_metavar_env> const & menv = none_ro_menv(),
std::shared_ptr<simplifier_monitor> const & monitor = std::shared_ptr<simplifier_monitor>());
void open_simplifier(lua_State * L);
}

18
src/library/tactic/simplify_tactic.cpp
View file

@ -9,6 +9,7 @@ Author: Leonardo de Moura
#include "util/sexpr/option_declarations.h"
#include "kernel/type_checker.h"
#include "kernel/kernel.h"
#include "library/heq_decls.h"
#include "library/simplifier/simplifier.h"
#include "library/tactic/tactic.h"
@ -51,12 +52,21 @@ static optional<proof_state> simplify_tactic(ro_environment const & env, io_stat
rule_sets.push_back(get_rewrite_rule_set(env, ns[i]));
}
expr conclusion = g.get_conclusion();
auto r = simplify(conclusion, env, context(), opts, rule_sets.size(), rule_sets.data(), some_ro_menv(menv));
expr new_conclusion = r.first;
expr eq_proof = r.second;
expr conclusion = g.get_conclusion();
auto r = simplify(conclusion, env, context(), opts, rule_sets.size(), rule_sets.data(), some_ro_menv(menv));
expr new_conclusion = r.get_expr();
if (new_conclusion == g.get_conclusion())
return optional<proof_state>(s);
expr eq_proof;
if (!r.get_proof()) {
// TODO(Leo): we should create a "by simplifier" proof
// For now, we just fail
return none_proof_state();
} else {
eq_proof = *r.get_proof();
}
if (r.is_heq_proof())
eq_proof = mk_to_eq_th(Bool, conclusion, new_conclusion, eq_proof);
bool solved = is_true(new_conclusion);
goals rest_gs = tail(s.get_goals());
goals new_gs;

2
tests/lean/errmsg1.lean.expected.out
View file

@ -8,6 +8,6 @@ errmsg1.lean:4:10: error: invalid expression, it still contains metavariables af
errmsg1.lean:5:11: error: failed to synthesize metavar M::0, it could not be synthesized by type inference and its type is not a proposition
λ (A : Type) (x : A), ?M::0
errmsg1.lean:6:3: error: unsolved metavar M::0
errmsg1.lean:8:0: error: invalid definition, type still contains metavariables after elaboration
errmsg1.lean:8:0: error: failed to synthesize metavar M::1, it could not be synthesized by type inference and its type is not a proposition
∀ x : ?M::1, @eq ?M::1 x x
errmsg1.lean:8:22: error: unsolved metavar M::1

8
tests/lean/simp.lean.expected.out
View file

@ -8,7 +8,7 @@
Assumed: b
Axfg : ∀ x : ℕ, g x x = x
Axf1 : ∀ x : ℕ, f (f x) = x
a trans (congr2 (g a) (Axf1 a)) (Axfg a)
g a a congr2 (g a) (Axf1 a)
a trans (congr2 (g a) (Axf1 a)) (Axfg a)
a trans (congr2 (g a) (Axf1 a)) (Axfg a)
a trans (congr2 (g a) (Axf1 a)) (Axfg a) false
g a a congr2 (g a) (Axf1 a) false
a trans (congr2 (g a) (Axf1 a)) (Axfg a) false
a trans (congr2 (g a) (Axf1 a)) (Axfg a) false

8
tests/lean/simp3.lean.expected.out
View file

@ -30,7 +30,7 @@ trans (congr (congr2 (λ x : ℕ, eq ((λ x : ℕ, x + 10) x))
(congr2 (λ x : ℕ, x + 10) (if_a_a (a > 0) b)))
(eq_id (b + 10))
a * a + (a * b + (b * a + b * b))
⊤ → ⊥ refl (⊤ → ⊥)
⊤ → ⊤ refl (⊤ → ⊤)
⊥ → ⊥ refl (⊥ → ⊥)
⊥ refl ⊥
⊤ → ⊥ refl (⊤ → ⊥) false
⊤ → ⊤ refl (⊤ → ⊤) false
⊥ → ⊥ refl (⊥ → ⊥) false
⊥ refl ⊥ false

2
tests/lean/simp6.lean.expected.out
View file

@ -2,4 +2,4 @@
Set: pp::unicode
Assumed: a
Assumed: b
⊤ trans (congr2 (eq (a + b)) (Nat::add_comm b a)) (eq_id (a + b))
⊤ trans (congr2 (eq (a + b)) (Nat::add_comm b a)) (eq_id (a + b)) false