refactor(library/tactic/simplify): add simplify subclasses, and use new simplifier at nested
This commit is contained in:
Leonardo de Moura
parent
fa01e062ef
commit
4d52de6f33
12 changed files with 412 additions and 50 deletions
|
|
@ -143,13 +143,13 @@ cases_true_false (λ x, x = false ∨ x = true)
|
|||
(or.inl rfl)
|
||||
a
|
||||
|
||||
theorem eq.of_iff {a b : Prop} (h : a ↔ b) : a = b :=
|
||||
theorem iff.to_eq {a b : Prop} (h : a ↔ b) : a = b :=
|
||||
iff.elim (assume h1 h2, propext (iff.intro h1 h2)) h
|
||||
|
||||
theorem iff_eq_eq {a b : Prop} : (a ↔ b) = (a = b) :=
|
||||
propext (iff.intro
|
||||
(assume h, eq.of_iff h)
|
||||
(assume h, iff.of_eq h))
|
||||
(assume h, iff.to_eq h)
|
||||
(assume h, h^.to_iff))
|
||||
|
||||
lemma eq_false {a : Prop} : (a = false) = (¬ a) :=
|
||||
have (a ↔ false) = (¬ a), from propext (iff_false a),
|
||||
|
|
|
|||
16
library/init/congr.lean
Normal file
16
library/init/congr.lean
Normal file
|
|
@ -0,0 +1,16 @@
|
|||
/-
|
||||
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Author: Leonardo de Moura
|
||||
|
||||
Additional congruence lemmas.
|
||||
-/
|
||||
prelude
|
||||
import init.quot
|
||||
universe variables u v
|
||||
|
||||
lemma forall_congr_eq {A : Type u} {p q : A → Prop} (h : ∀ a, p a = q a) : (∀ a, p a) = ∀ a, q a :=
|
||||
propext (forall_congr (λ a, (h a)^.to_iff))
|
||||
|
||||
lemma imp_congr_eq {a b c d : Prop} (h₁ : a = c) (h₂ : b = d) : (a → b) = (c → d) :=
|
||||
propext (imp_congr h₁^.to_iff h₂^.to_iff)
|
||||
|
|
@ -281,7 +281,7 @@ iff.intro (iff.elim_right h) (iff.elim_left h)
|
|||
lemma iff.comm : (a ↔ b) ↔ (b ↔ a) :=
|
||||
iff.intro iff.symm iff.symm
|
||||
|
||||
lemma iff.of_eq {a b : Prop} (h : a = b) : a ↔ b :=
|
||||
lemma eq.to_iff {a b : Prop} (h : a = b) : a ↔ b :=
|
||||
eq.rec_on h iff.rfl
|
||||
|
||||
lemma not_iff_not_of_iff (h₁ : a ↔ b) : ¬a ↔ ¬b :=
|
||||
|
|
@ -646,7 +646,7 @@ section
|
|||
else is_false (iff.mp (not_iff_not_of_iff h) hp)
|
||||
|
||||
def decidable_of_decidable_of_eq (hp : decidable p) (h : p = q) : decidable q :=
|
||||
decidable_of_decidable_of_iff hp (iff.of_eq h)
|
||||
decidable_of_decidable_of_iff hp h^.to_iff
|
||||
|
||||
protected def or.by_cases [decidable p] [decidable q] {A : Type u}
|
||||
(h : p ∨ q) (h₁ : p → A) (h₂ : q → A) : A :=
|
||||
|
|
|
|||
|
|
@ -16,11 +16,7 @@ is_associative.mk (λ x y z, propext (@or.assoc x y z))
|
|||
-- Basic congruence theorems over equality (using propext)
|
||||
attribute [congr]
|
||||
theorem imp_congr_ctx_eq {P₁ P₂ Q₁ Q₂ : Prop} (H₁ : P₁ = P₂) (H₂ : P₂ → (Q₁ = Q₂)) : (P₁ → Q₁) = (P₂ → Q₂) :=
|
||||
propext (imp_congr_ctx (iff.of_eq H₁) (assume p₂, iff.of_eq (H₂ p₂)))
|
||||
|
||||
attribute [congr]
|
||||
theorem forall_congr_eq {A : Type u} (P Q : A → Prop) (H : ∀ a, P a = Q a) : ((∀ a, P a) = (∀ a, Q a)) :=
|
||||
propext (forall_congr (assume a, iff.of_eq (H a)))
|
||||
propext (imp_congr_ctx H₁^.to_iff (assume p₂, (H₂ p₂)^.to_iff))
|
||||
|
||||
-- Congruence theorems for flattening
|
||||
namespace simplifier
|
||||
|
|
|
|||
|
|
@ -78,6 +78,8 @@ name const * g_false_rec = nullptr;
|
|||
name const * g_field = nullptr;
|
||||
name const * g_fin = nullptr;
|
||||
name const * g_fin_mk = nullptr;
|
||||
name const * g_forall_congr = nullptr;
|
||||
name const * g_forall_congr_eq = nullptr;
|
||||
name const * g_funext = nullptr;
|
||||
name const * g_ge = nullptr;
|
||||
name const * g_get_line = nullptr;
|
||||
|
|
@ -116,6 +118,8 @@ name const * g_iff_refl = nullptr;
|
|||
name const * g_iff_symm = nullptr;
|
||||
name const * g_iff_trans = nullptr;
|
||||
name const * g_iff_true_intro = nullptr;
|
||||
name const * g_imp_congr = nullptr;
|
||||
name const * g_imp_congr_eq = nullptr;
|
||||
name const * g_implies = nullptr;
|
||||
name const * g_implies_of_if_neg = nullptr;
|
||||
name const * g_implies_of_if_pos = nullptr;
|
||||
|
|
@ -460,6 +464,8 @@ void initialize_constants() {
|
|||
g_field = new name{"field"};
|
||||
g_fin = new name{"fin"};
|
||||
g_fin_mk = new name{"fin", "mk"};
|
||||
g_forall_congr = new name{"forall_congr"};
|
||||
g_forall_congr_eq = new name{"forall_congr_eq"};
|
||||
g_funext = new name{"funext"};
|
||||
g_ge = new name{"ge"};
|
||||
g_get_line = new name{"get_line"};
|
||||
|
|
@ -498,6 +504,8 @@ void initialize_constants() {
|
|||
g_iff_symm = new name{"iff", "symm"};
|
||||
g_iff_trans = new name{"iff", "trans"};
|
||||
g_iff_true_intro = new name{"iff_true_intro"};
|
||||
g_imp_congr = new name{"imp_congr"};
|
||||
g_imp_congr_eq = new name{"imp_congr_eq"};
|
||||
g_implies = new name{"implies"};
|
||||
g_implies_of_if_neg = new name{"implies_of_if_neg"};
|
||||
g_implies_of_if_pos = new name{"implies_of_if_pos"};
|
||||
|
|
@ -843,6 +851,8 @@ void finalize_constants() {
|
|||
delete g_field;
|
||||
delete g_fin;
|
||||
delete g_fin_mk;
|
||||
delete g_forall_congr;
|
||||
delete g_forall_congr_eq;
|
||||
delete g_funext;
|
||||
delete g_ge;
|
||||
delete g_get_line;
|
||||
|
|
@ -881,6 +891,8 @@ void finalize_constants() {
|
|||
delete g_iff_symm;
|
||||
delete g_iff_trans;
|
||||
delete g_iff_true_intro;
|
||||
delete g_imp_congr;
|
||||
delete g_imp_congr_eq;
|
||||
delete g_implies;
|
||||
delete g_implies_of_if_neg;
|
||||
delete g_implies_of_if_pos;
|
||||
|
|
@ -1225,6 +1237,8 @@ name const & get_false_rec_name() { return *g_false_rec; }
|
|||
name const & get_field_name() { return *g_field; }
|
||||
name const & get_fin_name() { return *g_fin; }
|
||||
name const & get_fin_mk_name() { return *g_fin_mk; }
|
||||
name const & get_forall_congr_name() { return *g_forall_congr; }
|
||||
name const & get_forall_congr_eq_name() { return *g_forall_congr_eq; }
|
||||
name const & get_funext_name() { return *g_funext; }
|
||||
name const & get_ge_name() { return *g_ge; }
|
||||
name const & get_get_line_name() { return *g_get_line; }
|
||||
|
|
@ -1263,6 +1277,8 @@ name const & get_iff_refl_name() { return *g_iff_refl; }
|
|||
name const & get_iff_symm_name() { return *g_iff_symm; }
|
||||
name const & get_iff_trans_name() { return *g_iff_trans; }
|
||||
name const & get_iff_true_intro_name() { return *g_iff_true_intro; }
|
||||
name const & get_imp_congr_name() { return *g_imp_congr; }
|
||||
name const & get_imp_congr_eq_name() { return *g_imp_congr_eq; }
|
||||
name const & get_implies_name() { return *g_implies; }
|
||||
name const & get_implies_of_if_neg_name() { return *g_implies_of_if_neg; }
|
||||
name const & get_implies_of_if_pos_name() { return *g_implies_of_if_pos; }
|
||||
|
|
|
|||
|
|
@ -80,6 +80,8 @@ name const & get_false_rec_name();
|
|||
name const & get_field_name();
|
||||
name const & get_fin_name();
|
||||
name const & get_fin_mk_name();
|
||||
name const & get_forall_congr_name();
|
||||
name const & get_forall_congr_eq_name();
|
||||
name const & get_funext_name();
|
||||
name const & get_ge_name();
|
||||
name const & get_get_line_name();
|
||||
|
|
@ -118,6 +120,8 @@ name const & get_iff_refl_name();
|
|||
name const & get_iff_symm_name();
|
||||
name const & get_iff_trans_name();
|
||||
name const & get_iff_true_intro_name();
|
||||
name const & get_imp_congr_name();
|
||||
name const & get_imp_congr_eq_name();
|
||||
name const & get_implies_name();
|
||||
name const & get_implies_of_if_neg_name();
|
||||
name const & get_implies_of_if_pos_name();
|
||||
|
|
|
|||
|
|
@ -73,6 +73,8 @@ false.rec
|
|||
field
|
||||
fin
|
||||
fin.mk
|
||||
forall_congr
|
||||
forall_congr_eq
|
||||
funext
|
||||
ge
|
||||
get_line
|
||||
|
|
@ -111,6 +113,8 @@ iff.refl
|
|||
iff.symm
|
||||
iff.trans
|
||||
iff_true_intro
|
||||
imp_congr
|
||||
imp_congr_eq
|
||||
implies
|
||||
implies_of_if_neg
|
||||
implies_of_if_pos
|
||||
|
|
|
|||
|
|
@ -1251,35 +1251,31 @@ class add_nested_inductive_decl_fn {
|
|||
return simp_result(h_a, pr);
|
||||
}
|
||||
|
||||
options get_simp_options(options opts) {
|
||||
opts = remove_all_with_prefix(get_simplify_prefix_name(), m_tctx.get_options());
|
||||
opts = opts.update(get_simplify_max_steps_name(), 100000);
|
||||
opts = opts.update(get_simplify_contextual_name(), false);
|
||||
opts = opts.update(get_simplify_rewrite_name(), true);
|
||||
opts = opts.update(get_simplify_lift_eq_name(), false);
|
||||
opts = opts.update(get_simplify_canonize_instances_fixed_point_name(), false);
|
||||
opts = opts.update(get_simplify_canonize_proofs_fixed_point_name(), false);
|
||||
return opts;
|
||||
}
|
||||
|
||||
expr prove_by_simp(local_context const & lctx, expr const & thm, list<expr> Hs, bool use_sizeof) {
|
||||
type_context tctx(m_env, get_simp_options(m_tctx.get_options()), lctx, transparency_mode::Semireducible);
|
||||
type_context tctx_whnf(m_env, get_simp_options(m_tctx.get_options()), lctx, transparency_mode::None);
|
||||
|
||||
type_context tctx(m_env, m_tctx.get_options(), lctx, transparency_mode::Semireducible);
|
||||
type_context tctx_whnf(m_env, m_tctx.get_options(), lctx, transparency_mode::None);
|
||||
simp_lemmas all_lemmas = use_sizeof ? join(m_sizeof_lemmas, m_lemmas) : m_lemmas;
|
||||
for (expr const & H : Hs) {
|
||||
expr H_type = tctx_whnf.infer(H);
|
||||
all_lemmas = add(tctx_whnf, all_lemmas, mlocal_name(H), H_type, H, LEAN_DEFAULT_PRIORITY);
|
||||
}
|
||||
|
||||
lean_trace(name({"inductive_compiler", "nested", "simp", "start"}), tout() << thm << "\n";);
|
||||
auto thm_pr = prove_eq_by_simp(tctx, tctx_whnf, all_lemmas, thm);
|
||||
unsigned max_steps = 1000000;
|
||||
bool contextual = false;
|
||||
bool lift_eq = false;
|
||||
bool canonize_instances = false;
|
||||
bool canonize_proofs = false;
|
||||
bool use_axioms = false;
|
||||
simplify_fn simplifier(tctx, all_lemmas, max_steps, contextual, lift_eq,
|
||||
canonize_instances, canonize_proofs, use_axioms);
|
||||
auto thm_pr = simplifier.prove_by_simp(get_eq_name(), thm);
|
||||
if (!thm_pr) {
|
||||
formatter_factory const & fmtf = get_global_ios().get_formatter_factory();
|
||||
lean_trace(name({"inductive_compiler", "nested", "simp", "failure"}),
|
||||
tout() << "\n-------------------\n"
|
||||
<< lctx.pp(fmtf(m_env, m_tctx.get_options(), m_tctx)) << "\n";);
|
||||
throw exception("simplifier failed to prove goal; trace 'inductive_compiler.nested.simp.failure' for more information");
|
||||
throw exception("simplifier failed to prove goal; trace 'inductive_compiler.nested.simp.failure' "
|
||||
"for more information");
|
||||
}
|
||||
return *thm_pr;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -30,6 +30,7 @@ Author: Daniel Selsam, Leonardo de Moura
|
|||
#include "library/congr_lemma.h"
|
||||
#include "library/fun_info.h"
|
||||
#include "library/vm/vm_expr.h"
|
||||
#include "library/vm/vm_option.h"
|
||||
#include "library/vm/vm_list.h"
|
||||
#include "library/vm/vm_name.h"
|
||||
#include "library/tactic/tactic_state.h"
|
||||
|
|
@ -39,7 +40,7 @@ Author: Daniel Selsam, Leonardo de Moura
|
|||
#include "library/tactic/simplify.h"
|
||||
|
||||
#ifndef LEAN_DEFAULT_SIMPLIFY_MAX_STEPS
|
||||
#define LEAN_DEFAULT_SIMPLIFY_MAX_STEPS 10000
|
||||
#define LEAN_DEFAULT_SIMPLIFY_MAX_STEPS 1000000
|
||||
#endif
|
||||
#ifndef LEAN_DEFAULT_SIMPLIFY_CONTEXTUAL
|
||||
#define LEAN_DEFAULT_SIMPLIFY_CONTEXTUAL true
|
||||
|
|
@ -60,6 +61,10 @@ Author: Daniel Selsam, Leonardo de Moura
|
|||
namespace lean {
|
||||
#define lean_simp_trace(CTX, N, CODE) lean_trace(N, scope_trace_env _scope1(CTX.env(), CTX); CODE)
|
||||
|
||||
/* -----------------------------------
|
||||
Core simplification procedure.
|
||||
------------------------------------ */
|
||||
|
||||
simp_result simplify_core_fn::join(simp_result const & r1, simp_result const & r2) {
|
||||
return ::lean::join(m_ctx, m_rel, r1, r2);
|
||||
}
|
||||
|
|
@ -239,7 +244,8 @@ simp_result simplify_core_fn::try_user_congr(expr const & e, simp_lemma const &
|
|||
expr m_type = tmp_ctx.instantiate_mvars(tmp_ctx.infer(m));
|
||||
|
||||
while (is_pi(m_type)) {
|
||||
expr d = instantiate_rev(binding_domain(m_type), local_factory.as_buffer().size(), local_factory.as_buffer().data());
|
||||
expr d = instantiate_rev(binding_domain(m_type), local_factory.as_buffer().size(),
|
||||
local_factory.as_buffer().data());
|
||||
expr l = local_factory.push_local(binding_name(m_type), d, binding_info(m_type));
|
||||
lean_assert(!has_metavar(l));
|
||||
m_type = binding_body(m_type);
|
||||
|
|
@ -463,6 +469,64 @@ simp_result simplify_core_fn::congr_funs(simp_result const & r_f, buffer<expr> c
|
|||
return simp_result(e, pf);
|
||||
}
|
||||
|
||||
simp_result simplify_core_fn::rewrite(expr const & e) {
|
||||
simp_lemmas_for const * sr = m_slss.find(m_rel);
|
||||
if (!sr) return simp_result(e);
|
||||
|
||||
list<simp_lemma> const * srs = sr->find(e);
|
||||
if (!srs) {
|
||||
lean_trace_d(name({"debug", "simplify", "try_rewrite"}), tout() << "no simp lemmas for: " << e << "\n";);
|
||||
return simp_result(e);
|
||||
}
|
||||
|
||||
for (simp_lemma const & lemma : *srs) {
|
||||
simp_result r = rewrite(e, lemma);
|
||||
if (!is_eqp(r.get_new(), e)) {
|
||||
lean_trace_d(name({"simplify", "rewrite"}), tout() << "[" << lemma.get_id() << "]: " << e
|
||||
<< " ==> " << r.get_new() << "\n";);
|
||||
return r;
|
||||
}
|
||||
}
|
||||
|
||||
return simp_result(e);
|
||||
}
|
||||
|
||||
simp_result simplify_core_fn::rewrite(expr const & e, simp_lemma const & sl) {
|
||||
tmp_type_context tmp_ctx(m_ctx, sl.get_num_umeta(), sl.get_num_emeta());
|
||||
if (!tmp_ctx.is_def_eq(e, sl.get_lhs())) {
|
||||
lean_trace_d(name({"debug", "simplify", "rewrite"}), tout() << "fail to unify: " << sl.get_id() << "\n";);
|
||||
return simp_result(e);
|
||||
}
|
||||
|
||||
if (!instantiate_emetas(tmp_ctx, sl.get_num_emeta(), sl.get_emetas(), sl.get_instances())) {
|
||||
lean_trace_d(name({"debug", "simplify", "rewrite"}), tout() << "fail to instantiate emetas: " <<
|
||||
sl.get_id() << "\n";);
|
||||
return simp_result(e);
|
||||
}
|
||||
|
||||
for (unsigned i = 0; i < sl.get_num_umeta(); i++) {
|
||||
if (!tmp_ctx.is_uassigned(i))
|
||||
return simp_result(e);
|
||||
}
|
||||
|
||||
expr new_lhs = tmp_ctx.instantiate_mvars(sl.get_lhs());
|
||||
expr new_rhs = tmp_ctx.instantiate_mvars(sl.get_rhs());
|
||||
if (sl.is_permutation()) {
|
||||
if (!is_lt(new_rhs, new_lhs, false)) {
|
||||
lean_simp_trace(tmp_ctx, name({"simplify", "perm"}),
|
||||
tout() << "perm rejected: " << new_rhs << " !< " << new_lhs << "\n";);
|
||||
return simp_result(e);
|
||||
}
|
||||
}
|
||||
|
||||
if (sl.is_refl()) {
|
||||
return simp_result(new_rhs);
|
||||
} else {
|
||||
expr pf = tmp_ctx.instantiate_mvars(sl.get_proof());
|
||||
return simp_result(new_rhs, pf);
|
||||
}
|
||||
}
|
||||
|
||||
simp_result simplify_core_fn::visit(expr const & e, optional<expr> const & parent) {
|
||||
check_system("simplify");
|
||||
inc_num_steps();
|
||||
|
|
@ -635,6 +699,238 @@ simp_result simplify_core_fn::operator()(name const & rel, expr const & e) {
|
|||
}
|
||||
}
|
||||
|
||||
optional<expr> simplify_core_fn::prove_by_simp(name const & rel, expr const & e) {
|
||||
lean_assert(rel == get_eq_name() || rel == get_iff_name());
|
||||
simp_result r = operator()(rel, e);
|
||||
name const & mpr = rel == get_eq_name() ? get_eq_mpr_name() : get_iff_mpr_name();
|
||||
|
||||
name rrel;
|
||||
expr lhs, rhs;
|
||||
if (is_relation(m_ctx.env(), r.get_new(), rrel, lhs, rhs) &&
|
||||
is_refl_relation(m_ctx.env(), rrel) &&
|
||||
m_ctx.is_def_eq(lhs, rhs)) {
|
||||
if (r.has_proof()) {
|
||||
return some_expr(mk_app(m_ctx, mpr, r.get_proof(), mk_refl(m_ctx, rrel, lhs)));
|
||||
} else {
|
||||
return some_expr(mk_refl(m_ctx, rrel, lhs));
|
||||
}
|
||||
} else if (is_true(r.get_new())) {
|
||||
if (r.has_proof()) {
|
||||
return some_expr(mk_app(m_ctx, mpr, r.get_proof(), mk_true_intro()));
|
||||
} else {
|
||||
return some_expr(mk_true_intro());
|
||||
}
|
||||
}
|
||||
return none_expr();
|
||||
}
|
||||
|
||||
/* -----------------------------------
|
||||
simplify_ext_core_fn
|
||||
------------------------------------ */
|
||||
|
||||
simplify_ext_core_fn::simplify_ext_core_fn(type_context & ctx, simp_lemmas const & slss,
|
||||
unsigned max_steps, bool contextual, bool lift_eq,
|
||||
bool canonize_instances, bool canonize_proofs,
|
||||
bool use_axioms):
|
||||
simplify_core_fn(ctx, slss, max_steps, contextual, lift_eq, canonize_instances, canonize_proofs),
|
||||
m_use_axioms (use_axioms) {
|
||||
}
|
||||
|
||||
simp_result simplify_ext_core_fn::visit_lambda(expr const & e) {
|
||||
if (m_rel != get_eq_name() || !m_use_axioms) return simp_result(e);
|
||||
type_context::tmp_locals locals(m_ctx);
|
||||
expr it = e;
|
||||
while (is_lambda(it)) {
|
||||
expr d = instantiate_rev(binding_domain(it), locals.size(), locals.as_buffer().data());
|
||||
expr l = locals.push_local(binding_name(it), d, binding_info(it));
|
||||
it = binding_body(it);
|
||||
}
|
||||
it = instantiate_rev(it, locals.size(), locals.as_buffer().data());
|
||||
|
||||
simp_result r = visit(it, some_expr(e));
|
||||
expr new_body = r.get_new();
|
||||
|
||||
if (new_body == it)
|
||||
return simp_result(e);
|
||||
|
||||
if (!r.has_proof())
|
||||
return simp_result(locals.mk_lambda(new_body));
|
||||
|
||||
// TODO(Leo): create funext proof
|
||||
return simp_result(e);
|
||||
}
|
||||
|
||||
simp_result simplify_ext_core_fn::forall_congr(expr const & e) {
|
||||
lean_assert(m_rel == get_eq_name() || m_rel == get_iff_name());
|
||||
buffer<expr> pis;
|
||||
type_context::tmp_locals locals(m_ctx);
|
||||
expr it = e;
|
||||
while (is_pi(it)) {
|
||||
expr d = instantiate_rev(binding_domain(it), locals.as_buffer().size(), locals.as_buffer().data());
|
||||
if (m_ctx.is_prop(d))
|
||||
break;
|
||||
pis.push_back(it);
|
||||
locals.push_local(binding_name(it), d, binding_info(it));
|
||||
it = binding_body(it);
|
||||
}
|
||||
buffer<expr> const & ls = locals.as_buffer();
|
||||
lean_assert(pis.size() == ls.size());
|
||||
expr body = instantiate_rev(it, ls.size(), ls.data());
|
||||
simp_result body_r = visit(body, some_expr(e));
|
||||
expr new_body = body_r.get_new();
|
||||
expr abst_new_body = abstract_locals(new_body, ls.size(), ls.data());
|
||||
name lemma_name = m_rel == get_eq_name() ? get_forall_congr_eq_name() : get_forall_congr_name();
|
||||
if (body_r.has_proof()) {
|
||||
expr pr = body_r.get_proof();
|
||||
expr Pr = abstract_locals(pr, ls.size(), ls.data());
|
||||
unsigned i = pis.size();
|
||||
expr Q = abst_new_body;
|
||||
expr R = abst_new_body;
|
||||
while (i > 0) {
|
||||
--i;
|
||||
expr pi = pis[i];
|
||||
expr A = binding_domain(pi);
|
||||
level A_lvl = get_level(m_ctx, m_ctx.infer(ls[i]));
|
||||
expr P = mk_lambda(binding_name(pi), A, binding_body(pi));
|
||||
expr Q = mk_lambda(binding_name(pi), A, R);
|
||||
expr H = mk_lambda(binding_name(pi), A, Pr);
|
||||
Pr = mk_app(mk_constant(lemma_name, {A_lvl}), A, P, Q, H);
|
||||
R = update_binding(pi, A, R);
|
||||
}
|
||||
lean_assert(closed(Pr));
|
||||
return simp_result(R, Pr);
|
||||
} else if (new_body == body) {
|
||||
return simp_result(e);
|
||||
} else {
|
||||
expr R = abst_new_body;
|
||||
unsigned i = pis.size();
|
||||
while (i > 0) {
|
||||
--i;
|
||||
R = update_binding(pis[i], binding_domain(pis[i]), R);
|
||||
}
|
||||
return simp_result(R);
|
||||
}
|
||||
return simp_result(e);
|
||||
}
|
||||
|
||||
simp_result simplify_ext_core_fn::imp_congr(expr const & e) {
|
||||
// TODO(Leo)
|
||||
return simp_result(e);
|
||||
}
|
||||
|
||||
simp_result simplify_ext_core_fn::visit_pi(expr const & e) {
|
||||
if ((m_rel == get_eq_name() && m_use_axioms) || m_rel == get_iff_name()) {
|
||||
if (m_ctx.is_prop(e)) {
|
||||
if (!m_ctx.is_prop(binding_domain(e)))
|
||||
return forall_congr(e);
|
||||
else if (is_arrow(e))
|
||||
return imp_congr(e);
|
||||
}
|
||||
}
|
||||
return simplify_core_fn::visit_pi(e);
|
||||
}
|
||||
|
||||
simp_result simplify_ext_core_fn::visit_let(expr const & e) {
|
||||
/* TODO(Leo): we need to implement efficient code for checking whether the abstraction of
|
||||
a let-body is type correct or not */
|
||||
return simp_result(e);
|
||||
}
|
||||
|
||||
static optional<pair<simp_result, bool>> to_ext_result(simp_result const & r) {
|
||||
return optional<pair<simp_result, bool>>(r, true);
|
||||
}
|
||||
|
||||
static optional<pair<simp_result, bool>> no_ext_result() {
|
||||
return optional<pair<simp_result, bool>>();
|
||||
}
|
||||
|
||||
optional<pair<simp_result, bool>> simplify_fn::pre(expr const & e, optional<expr> const &) {
|
||||
if (auto r = m_ctx.reduce_projection(e))
|
||||
return to_ext_result(simp_result(*r));
|
||||
else
|
||||
return no_ext_result();
|
||||
}
|
||||
|
||||
optional<pair<simp_result, bool>> simplify_fn::post(expr const & e, optional<expr> const &) {
|
||||
simp_result r = rewrite(e);
|
||||
if (r.get_new() != e)
|
||||
return to_ext_result(r);
|
||||
else
|
||||
return no_ext_result();
|
||||
}
|
||||
|
||||
class vm_simplify_fn : public simplify_ext_core_fn {
|
||||
vm_obj m_a;
|
||||
vm_obj m_prove;
|
||||
vm_obj m_pre;
|
||||
vm_obj m_post;
|
||||
tactic_state m_s;
|
||||
|
||||
optional<pair<simp_result, bool>> invoke_fn(vm_obj const & fn, expr const & e, optional<expr> const & parent) {
|
||||
m_s = set_mctx_lctx(m_s, m_ctx.mctx(), m_ctx.lctx());
|
||||
vm_obj r = invoke(fn, m_a, to_obj(m_rel), to_obj(m_slss), to_obj(parent), to_obj(e), to_obj(m_s));
|
||||
/* r : tactic_state (A × expr × option expr × bool) */
|
||||
if (optional<tactic_state> new_s = is_tactic_success(r)) {
|
||||
m_s = *new_s;
|
||||
m_ctx.set_mctx(m_s.mctx());
|
||||
vm_obj t = cfield(r, 0);
|
||||
/* t : A × expr × option expr × bool */
|
||||
m_a = cfield(t, 0);
|
||||
vm_obj t1 = cfield(t, 1);
|
||||
expr new_e = to_expr(cfield(t1, 0));
|
||||
vm_obj t2 = cfield(t1, 1);
|
||||
optional<expr> new_pr;
|
||||
vm_obj vpr = cfield(t2, 0);
|
||||
if (!is_none(vpr))
|
||||
new_pr = to_expr(get_some_value(vpr));
|
||||
bool flag = to_bool(cfield(t2, 1));
|
||||
return optional<pair<simp_result, bool>>(simp_result(new_e, new_pr), flag);
|
||||
} else {
|
||||
return no_ext_result();
|
||||
}
|
||||
}
|
||||
|
||||
virtual optional<pair<simp_result, bool>> pre(expr const & e, optional<expr> const & parent) override {
|
||||
return invoke_fn(m_pre, e, parent);
|
||||
}
|
||||
|
||||
virtual optional<pair<simp_result, bool>> post(expr const & e, optional<expr> const & parent) override {
|
||||
return invoke_fn(m_post, e, parent);
|
||||
}
|
||||
|
||||
virtual optional<expr> prove(expr const & e) override {
|
||||
tactic_state s = mk_tactic_state_for(m_ctx.env(), m_ctx.get_options(), m_ctx.lctx(), e);
|
||||
vm_obj r_obj = invoke(m_prove, m_a, to_obj(s));
|
||||
optional<tactic_state> s_new = is_tactic_success(r_obj);
|
||||
if (!s_new || s_new->goals()) return none_expr();
|
||||
metavar_context mctx = s_new->mctx();
|
||||
expr result = mctx.instantiate_mvars(s_new->main());
|
||||
if (has_expr_metavar(result)) return none_expr();
|
||||
m_a = cfield(r_obj, 0);
|
||||
m_ctx.set_mctx(mctx);
|
||||
return some_expr(result);
|
||||
}
|
||||
|
||||
public:
|
||||
vm_simplify_fn(type_context & ctx, simp_lemmas const & slss,
|
||||
unsigned max_steps, bool contextual, bool lift_eq,
|
||||
bool canonize_instances, bool canonize_proofs, bool use_axioms,
|
||||
vm_obj const & prove, vm_obj const & pre, vm_obj const & post):
|
||||
simplify_ext_core_fn(ctx, slss, max_steps, contextual, lift_eq,
|
||||
canonize_instances, canonize_proofs, use_axioms),
|
||||
m_prove(prove), m_pre(pre), m_post(post),
|
||||
m_s(mk_tactic_state_for(ctx.env(), ctx.get_options(), ctx.mctx(), ctx.lctx(), mk_true())) {}
|
||||
};
|
||||
|
||||
void initialize_new_simplify() {
|
||||
}
|
||||
|
||||
void finalize_new_simplify() {
|
||||
}
|
||||
|
||||
/* LEGACY */
|
||||
|
||||
|
||||
|
||||
static name * g_simplify_prefix = nullptr;
|
||||
name get_simplify_prefix_name() { return *g_simplify_prefix; }
|
||||
|
|
@ -672,7 +968,8 @@ static bool get_simplify_lift_eq(options const & o) {
|
|||
}
|
||||
|
||||
static bool get_simplify_canonize_instances_fixed_point(options const & o) {
|
||||
return o.get_bool(*g_simplify_canonize_instances_fixed_point, LEAN_DEFAULT_SIMPLIFY_DEFEQ_CANONIZE_INSTANCES_FIXED_POINT);
|
||||
return o.get_bool(*g_simplify_canonize_instances_fixed_point,
|
||||
LEAN_DEFAULT_SIMPLIFY_DEFEQ_CANONIZE_INSTANCES_FIXED_POINT);
|
||||
}
|
||||
|
||||
static bool get_simplify_canonize_proofs_fixed_point(options const & o) {
|
||||
|
|
@ -739,7 +1036,8 @@ class simplifier {
|
|||
return m_canonize_instances_fixed_point || m_canonize_proofs_fixed_point;
|
||||
}
|
||||
|
||||
bool instantiate_emetas(tmp_type_context & tmp_tctx, unsigned num_emeta, list<expr> const & emetas, list<bool> const & instances);
|
||||
bool instantiate_emetas(tmp_type_context & tmp_tctx, unsigned num_emeta,
|
||||
list<expr> const & emetas, list<bool> const & instances);
|
||||
|
||||
/* Simp_Results */
|
||||
simp_result lift_from_eq(expr const & old_e, simp_result const & r_eq);
|
||||
|
|
@ -796,7 +1094,8 @@ class simplifier {
|
|||
for (simp_lemma const & lemma : *srs) {
|
||||
simp_result r = rewrite_binary(e, lemma);
|
||||
if (!is_eqp(r.get_new(), e)) {
|
||||
lean_trace_d(name({"simplifier", "rewrite"}), tout() << "[" << lemma.get_id() << "]: " << e << " ==> " << r.get_new() << "\n";);
|
||||
lean_trace_d(name({"simplifier", "rewrite"}), tout() << "[" << lemma.get_id() << "]: " << e <<
|
||||
" ==> " << r.get_new() << "\n";);
|
||||
return r;
|
||||
}
|
||||
}
|
||||
|
|
@ -810,7 +1109,8 @@ class simplifier {
|
|||
return simp_result(e);
|
||||
}
|
||||
if (!instantiate_emetas(tmp_tctx, sl.get_num_emeta(), sl.get_emetas(), sl.get_instances())) {
|
||||
lean_trace_d(name({"debug", "simplifier", "try_rewrite"}), tout() << "fail to instantiate emetas: " << sl.get_id() << "\n";);
|
||||
lean_trace_d(name({"debug", "simplifier", "try_rewrite"}), tout() << "fail to instantiate emetas: " <<
|
||||
sl.get_id() << "\n";);
|
||||
return simp_result(e);
|
||||
}
|
||||
|
||||
|
|
@ -913,7 +1213,8 @@ class simplifier {
|
|||
if (m_rewrite) {
|
||||
simp_result r_rewrite = simplify_rewrite_binary(r.get_new());
|
||||
if (r_rewrite.get_new() != r.get_new()) {
|
||||
lean_trace_d(name({"simplifier", "rewrite"}), tout() << r.get_new() << " ==> " << r_rewrite.get_new() << "\n";);
|
||||
lean_trace_d(name({"simplifier", "rewrite"}), tout() << r.get_new() << " ==> " <<
|
||||
r_rewrite.get_new() << "\n";);
|
||||
return join(r, r_rewrite);
|
||||
}
|
||||
}
|
||||
|
|
@ -1486,6 +1787,9 @@ expr simplifier::remove_unnecessary_casts(expr const & e) {
|
|||
return mk_app(f, args);
|
||||
}
|
||||
|
||||
simp_result simplify(type_context & tctx, name const & rel, simp_lemmas const & simp_lemmas,
|
||||
vm_obj const & prove_fn, expr const & e);
|
||||
|
||||
vm_obj simp_lemmas_simplify_core(vm_obj const & lemmas, vm_obj const & prove_fn, vm_obj const & rel_name, vm_obj const & e, vm_obj const & s0) {
|
||||
tactic_state const & s = to_tactic_state(s0);
|
||||
try {
|
||||
|
|
|
|||
|
|
@ -54,7 +54,8 @@ protected:
|
|||
void inc_num_steps();
|
||||
bool is_dependent_fn(expr const & f);
|
||||
bool should_defeq_canonize() const { return m_canonize_instances || m_canonize_proofs; }
|
||||
bool instantiate_emetas(tmp_type_context & tmp_tctx, unsigned num_emeta, list<expr> const & emetas, list<bool> const & instances);
|
||||
bool instantiate_emetas(tmp_type_context & tmp_tctx, unsigned num_emeta,
|
||||
list<expr> const & emetas, list<bool> const & instances);
|
||||
simp_result lift_from_eq(simp_result const & r_eq);
|
||||
simp_lemmas add_to_slss(simp_lemmas const & slss, buffer<expr> const & ls);
|
||||
expr remove_unnecessary_casts(expr const & e);
|
||||
|
|
@ -72,6 +73,12 @@ protected:
|
|||
simp_result congr_arg(expr const & f, simp_result const & r_arg);
|
||||
simp_result congr_funs(simp_result const & r_f, buffer<expr> const & args);
|
||||
|
||||
/* Rewriting
|
||||
Remark: the rewriting methods are implemented on this base class once and for all,
|
||||
but used in subclasses.*/
|
||||
simp_result rewrite(expr const & e);
|
||||
simp_result rewrite(expr const & e, simp_lemma const & sl);
|
||||
|
||||
/* Visitors */
|
||||
virtual optional<pair<simp_result, bool>> pre(expr const & e, optional<expr> const & parent);
|
||||
virtual optional<pair<simp_result, bool>> post(expr const & e, optional<expr> const & parent);
|
||||
|
|
@ -94,24 +101,38 @@ public:
|
|||
|
||||
environment const & env() const;
|
||||
simp_result operator()(name const & rel, expr const & e);
|
||||
|
||||
optional<expr> prove_by_simp(name const & rel, expr const & e);
|
||||
};
|
||||
|
||||
simp_result simplify(type_context & tctx, name const & rel, simp_lemmas const & simp_lemmas, vm_obj const & prove_fn, expr const & e);
|
||||
simp_result simplify(type_context & tctx, name const & rel, simp_lemmas const & simp_lemmas, expr const & e);
|
||||
/* Extend simplify_core_fn functionality by assuming function
|
||||
extensionality and propositional extensionality. */
|
||||
class simplify_ext_core_fn : public simplify_core_fn {
|
||||
protected:
|
||||
bool m_use_axioms;
|
||||
simp_result forall_congr(expr const & e);
|
||||
simp_result imp_congr(expr const & e);
|
||||
virtual simp_result visit_lambda(expr const & e) override;
|
||||
virtual simp_result visit_pi(expr const & e) override;
|
||||
virtual simp_result visit_let(expr const & e) override;
|
||||
public:
|
||||
simplify_ext_core_fn(type_context & ctx, simp_lemmas const & slss,
|
||||
unsigned max_steps, bool contextual, bool lift_eq,
|
||||
bool canonize_instances, bool canonize_proofs, bool use_axioms);
|
||||
};
|
||||
|
||||
simp_result simplify(type_context & tctx, type_context & tctx_whnf, name const & rel, simp_lemmas const & simp_lemmas, vm_obj const & prove_fn, expr const & e);
|
||||
simp_result simplify(type_context & tctx, type_context & tctx_whnf, name const & rel, simp_lemmas const & simp_lemmas, expr const & e);
|
||||
|
||||
optional<expr> prove_eq_by_simp(type_context & tctx, type_context & tctx_whnf, simp_lemmas const & simp_lemmas, expr const & e);
|
||||
|
||||
name get_simplify_prefix_name();
|
||||
name get_simplify_max_steps_name();
|
||||
name get_simplify_contextual_name();
|
||||
name get_simplify_rewrite_name();
|
||||
name get_simplify_lift_eq_name();
|
||||
name get_simplify_canonize_instances_fixed_point_name();
|
||||
name get_simplify_canonize_proofs_fixed_point_name();
|
||||
name get_simplify_canonize_subsingletons_name();
|
||||
/* Default (bottom-up) simplifier: reduce projections, and apply simplification lemmas */
|
||||
class simplify_fn : public simplify_ext_core_fn {
|
||||
protected:
|
||||
virtual optional<pair<simp_result, bool>> pre(expr const & e, optional<expr> const & parent) override;
|
||||
virtual optional<pair<simp_result, bool>> post(expr const & e, optional<expr> const & parent) override;
|
||||
public:
|
||||
simplify_fn(type_context & ctx, simp_lemmas const & slss,
|
||||
unsigned max_steps, bool contextual, bool lift_eq,
|
||||
bool canonize_instances, bool canonize_proofs, bool use_axioms):
|
||||
simplify_ext_core_fn(ctx, slss, max_steps, contextual, lift_eq,
|
||||
canonize_instances, canonize_proofs, use_axioms) {}
|
||||
};
|
||||
|
||||
void initialize_simplify();
|
||||
void finalize_simplify();
|
||||
|
|
|
|||
|
|
@ -60,6 +60,10 @@ vm_obj to_obj(expr const & e) {
|
|||
return mk_vm_external(new (get_vm_allocator().allocate(sizeof(vm_expr))) vm_expr(e));
|
||||
}
|
||||
|
||||
vm_obj to_obj(optional<expr> const & e) {
|
||||
return e ? mk_vm_some(to_obj(*e)) : mk_vm_none();
|
||||
}
|
||||
|
||||
binder_info to_binder_info(vm_obj const & o) {
|
||||
lean_assert(is_simple(o));
|
||||
/*
|
||||
|
|
|
|||
|
|
@ -15,6 +15,7 @@ macro_definition const & to_macro_definition(vm_obj const & o);
|
|||
vm_obj to_obj(macro_definition const & d);
|
||||
expr const & to_expr(vm_obj const & o);
|
||||
vm_obj to_obj(expr const & e);
|
||||
vm_obj to_obj(optional<expr> const & e);
|
||||
void initialize_vm_expr();
|
||||
void finalize_vm_expr();
|
||||
void initialize_vm_expr_builtin_idxs();
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue