feat(library/tactic): add zeta option, refactor simplify config option, allow users to change simplify_config in interactive mode
This commit is contained in:
Leonardo de Moura
parent
2928273a1e
commit
0d22410e2e
15 changed files with 155 additions and 133 deletions
|
|
@ -41,7 +41,7 @@ protected lemma add_left_comm : ∀ (n m k : ℕ), n + (m + k) = m + (n + k) :=
|
|||
left_comm nat.add nat.add_comm nat.add_assoc
|
||||
|
||||
protected lemma add_left_cancel : ∀ {n m k : ℕ}, n + m = n + k → m = k
|
||||
| 0 m k := by ctx_simp [nat.zero_add]
|
||||
| 0 m k := by simp [nat.zero_add] {contextual := tt}
|
||||
| (succ n) m k := λ h,
|
||||
have n+m = n+k, begin simp [succ_add] at h, injection h, assumption end,
|
||||
add_left_cancel this
|
||||
|
|
@ -64,7 +64,7 @@ protected lemma zero_ne_one : 0 ≠ (1 : ℕ) :=
|
|||
assume h, nat.no_confusion h
|
||||
|
||||
lemma eq_zero_of_add_eq_zero_right : ∀ {n m : ℕ}, n + m = 0 → n = 0
|
||||
| 0 m := by ctx_simp [nat.zero_add]
|
||||
| 0 m := by simp [nat.zero_add] {contextual := tt}
|
||||
| (n+1) m := λ h,
|
||||
begin
|
||||
exfalso,
|
||||
|
|
|
|||
|
|
@ -481,25 +481,21 @@ It has many variants.
|
|||
|
||||
- `simp with attr` simplifies the main goal target using the lemmas tagged with the attribute `[attr]`.
|
||||
-/
|
||||
meta def simp (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) (loc : parse location) : tactic unit :=
|
||||
simp_core {} [] hs attr_names ids loc
|
||||
|
||||
/--
|
||||
Similar to the `simp` tactic, but uses contextual simplification. For example, when simplifying `t = s → p`,
|
||||
the equation `t = s` is automatically added to the set of simplification rules when simplifying `p`.
|
||||
-/
|
||||
meta def ctx_simp (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) (loc : parse location) : tactic unit :=
|
||||
simp_core {contextual := tt} [] hs attr_names ids loc
|
||||
meta def simp (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) (loc : parse location)
|
||||
(cfg : simplify_config := {}) : tactic unit :=
|
||||
simp_core cfg [] hs attr_names ids loc
|
||||
|
||||
/--
|
||||
Similar to the `simp` tactic, but adds all applicable hypotheses as simplification rules.
|
||||
-/
|
||||
meta def simp_using_hs (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) : tactic unit :=
|
||||
meta def simp_using_hs (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list)
|
||||
(cfg : simplify_config := {}) : tactic unit :=
|
||||
do ctx ← collect_ctx_simps,
|
||||
simp_core {} ctx hs attr_names ids []
|
||||
simp_core cfg ctx hs attr_names ids []
|
||||
|
||||
meta def simph (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) : tactic unit :=
|
||||
simp_using_hs hs attr_names ids
|
||||
meta def simph (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list)
|
||||
(cfg : simplify_config := {}) : tactic unit :=
|
||||
simp_using_hs hs attr_names ids cfg
|
||||
|
||||
private meta def dsimp_hyps (s : simp_lemmas) : list name → tactic unit
|
||||
| [] := skip
|
||||
|
|
@ -579,12 +575,12 @@ private meta def dunfold_hyps_occs : name → occurrences → list name → tact
|
|||
| c occs [] := skip
|
||||
| c occs (h::hs) := get_local h >>= dunfold_core_at occs [c] >> dunfold_hyps_occs c occs hs
|
||||
|
||||
meta def dunfold_occs : parse ident → list nat → parse location → tactic unit
|
||||
| c ps [] := do new_c ← to_qualified_name c, tactic.dunfold_occs_of ps new_c
|
||||
| c ps hs := do new_c ← to_qualified_name c, dunfold_hyps_occs new_c (occurrences.pos ps) hs
|
||||
meta def dunfold_occs : parse ident → parse location → list nat → tactic unit
|
||||
| c [] ps := do new_c ← to_qualified_name c, tactic.dunfold_occs_of ps new_c
|
||||
| c hs ps := do new_c ← to_qualified_name c, dunfold_hyps_occs new_c (occurrences.pos ps) hs
|
||||
|
||||
/- TODO(Leo): add support for non-refl lemmas -/
|
||||
meta def unfold_occs : parse ident → list nat → parse location → tactic unit :=
|
||||
meta def unfold_occs : parse ident → parse location → list nat → tactic unit :=
|
||||
dunfold_occs
|
||||
|
||||
private meta def delta_hyps : list name → list name → tactic unit
|
||||
|
|
|
|||
|
|
@ -192,6 +192,7 @@ structure simplify_config :=
|
|||
(canonize_instances : bool := tt)
|
||||
(canonize_proofs : bool := ff)
|
||||
(use_axioms : bool := tt)
|
||||
(zeta : bool := tt)
|
||||
|
||||
meta constant simplify_core
|
||||
(c : simplify_config)
|
||||
|
|
|
|||
|
|
@ -229,16 +229,18 @@ smt_tactic.all_goals t
|
|||
meta def induction (p : parse texpr) (rec_name : parse using_ident) (ids : parse with_ident_list) : smt_tactic unit :=
|
||||
slift (tactic.interactive.induction p rec_name ids)
|
||||
|
||||
/-- Simplify the target type of the main goal. -/
|
||||
meta def simp (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) : smt_tactic unit :=
|
||||
tactic.interactive.simp hs attr_names ids []
|
||||
open tactic
|
||||
|
||||
meta def ctx_simp (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) : smt_tactic unit :=
|
||||
tactic.interactive.ctx_simp hs attr_names ids []
|
||||
/-- Simplify the target type of the main goal. -/
|
||||
meta def simp (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) (cfg : simplify_config := {}) : smt_tactic unit :=
|
||||
tactic.interactive.simp hs attr_names ids [] cfg
|
||||
|
||||
/-- Simplify the target type of the main goal using simplification lemmas and the current set of hypotheses. -/
|
||||
meta def simp_using_hs (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) : smt_tactic unit :=
|
||||
tactic.interactive.simp_using_hs hs attr_names ids
|
||||
meta def simp_using_hs (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) (cfg : simplify_config := {}) : smt_tactic unit :=
|
||||
tactic.interactive.simp_using_hs hs attr_names ids cfg
|
||||
|
||||
meta def simph (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) (cfg : simplify_config := {}) : smt_tactic unit :=
|
||||
simp_using_hs hs attr_names ids cfg
|
||||
|
||||
meta def dsimp (es : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) : smt_tactic unit :=
|
||||
tactic.interactive.dsimp es attr_names ids []
|
||||
|
|
|
|||
|
|
@ -173,11 +173,14 @@ static expr parse_auto_quote_tactic(parser & p, name const & decl_name, name con
|
|||
} else if (is_constant(arg_type, irtactic)) {
|
||||
args.push_back(parse_nested_auto_quote_tactic(p, tac_class, use_rstep, report_error));
|
||||
} else {
|
||||
args.push_back(p.parse_expr(get_max_prec()));
|
||||
break;
|
||||
}
|
||||
}
|
||||
type = binding_body(type);
|
||||
}
|
||||
while (p.curr_lbp() >= get_max_prec()) {
|
||||
args.push_back(p.parse_expr(get_max_prec()));
|
||||
}
|
||||
expr r = p.mk_app(p.save_pos(mk_constant(decl_name), pos), args, pos);
|
||||
return mk_tactic_step(p, r, pos, tac_class, use_rstep, report_error);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -17,7 +17,7 @@ Author: Leonardo de Moura
|
|||
namespace lean {
|
||||
// User-level maximum precedence
|
||||
unsigned get_max_prec();
|
||||
// Internal maximum precedence used for @@, @ and ! operators
|
||||
// Internal maximum precedence used for @@ and @ operators
|
||||
unsigned get_Max_prec();
|
||||
unsigned get_arrow_prec();
|
||||
class token_info {
|
||||
|
|
|
|||
|
|
@ -1260,16 +1260,17 @@ class add_nested_inductive_decl_fn {
|
|||
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";);
|
||||
unsigned max_steps = 1000000;
|
||||
bool contextual = false;
|
||||
bool lift_eq = false;
|
||||
bool canonize_instances = false;
|
||||
bool canonize_proofs = false;
|
||||
bool use_axioms = false;
|
||||
simplify_config cfg;
|
||||
cfg.m_max_steps = 1000000;
|
||||
cfg.m_contextual = false;
|
||||
cfg.m_lift_eq = false;
|
||||
cfg.m_canonize_instances = false;
|
||||
cfg.m_canonize_proofs = false;
|
||||
cfg.m_use_axioms = false;
|
||||
cfg.m_zeta = false;
|
||||
cfg.m_use_matcher = false;
|
||||
defeq_can_state dcs;
|
||||
simplify_fn simplifier(tctx, dcs, all_lemmas, max_steps, contextual, lift_eq,
|
||||
canonize_instances, canonize_proofs, use_axioms);
|
||||
simplifier.set_use_matcher(false); // hack
|
||||
simplify_fn simplifier(tctx, dcs, all_lemmas, cfg);
|
||||
auto thm_pr = simplifier.prove_by_simp(get_eq_name(), thm);
|
||||
if (!thm_pr) {
|
||||
formatter_factory const & fmtf = get_global_ios().get_formatter_factory();
|
||||
|
|
|
|||
|
|
@ -55,17 +55,31 @@ Author: Daniel Selsam, Leonardo de Moura
|
|||
#ifndef LEAN_DEFAULT_SIMPLIFY_LIFT_EQ
|
||||
#define LEAN_DEFAULT_SIMPLIFY_LIFT_EQ true
|
||||
#endif
|
||||
#ifndef LEAN_DEFAULT_SIMPLIFY_DEFEQ_CANONIZE_INSTANCES_FIXED_POINT
|
||||
#define LEAN_DEFAULT_SIMPLIFY_DEFEQ_CANONIZE_INSTANCES_FIXED_POINT false
|
||||
#endif
|
||||
#ifndef LEAN_DEFAULT_SIMPLIFY_DEFEQ_CANONIZE_PROOFS_FIXED_POINT
|
||||
#define LEAN_DEFAULT_SIMPLIFY_DEFEQ_CANONIZE_PROOFS_FIXED_POINT false
|
||||
#endif
|
||||
|
||||
namespace lean {
|
||||
#define lean_simp_trace(CTX, N, CODE) lean_trace(N, scope_trace_env _scope1(CTX.env(), CTX); CODE)
|
||||
#define lean_simp_trace_d(CTX, N, CODE) lean_trace_d(N, scope_trace_env _scope1(CTX.env(), CTX); CODE)
|
||||
|
||||
simplify_config::simplify_config():
|
||||
m_max_steps(LEAN_DEFAULT_SIMPLIFY_MAX_STEPS),
|
||||
m_contextual(LEAN_DEFAULT_SIMPLIFY_CONTEXTUAL),
|
||||
m_lift_eq(LEAN_DEFAULT_SIMPLIFY_LIFT_EQ),
|
||||
m_canonize_instances(true),
|
||||
m_canonize_proofs(false),
|
||||
m_use_axioms(false),
|
||||
m_zeta(false) {
|
||||
}
|
||||
|
||||
simplify_config::simplify_config(vm_obj const & obj) {
|
||||
m_max_steps = force_to_unsigned(cfield(obj, 0));
|
||||
m_contextual = to_bool(cfield(obj, 1));
|
||||
m_lift_eq = to_bool(cfield(obj, 2));
|
||||
m_canonize_instances = to_bool(cfield(obj, 3));
|
||||
m_canonize_proofs = to_bool(cfield(obj, 4));
|
||||
m_use_axioms = to_bool(cfield(obj, 5));
|
||||
m_zeta = to_bool(cfield(obj, 6));
|
||||
}
|
||||
|
||||
/* -----------------------------------
|
||||
Core simplification procedure.
|
||||
------------------------------------ */
|
||||
|
|
@ -76,7 +90,7 @@ simp_result simplify_core_fn::join(simp_result const & r1, simp_result const & r
|
|||
|
||||
void simplify_core_fn::inc_num_steps() {
|
||||
m_num_steps++;
|
||||
if (m_num_steps > m_max_steps)
|
||||
if (m_num_steps > m_cfg.m_max_steps)
|
||||
throw exception("simplify failed, maximum number of steps exceeded");
|
||||
}
|
||||
|
||||
|
|
@ -200,7 +214,8 @@ expr simplify_core_fn::defeq_canonize_args_step(expr const & e) {
|
|||
for (param_info const & pinfo : info.get_params_info()) {
|
||||
lean_assert(i < args.size());
|
||||
expr new_a;
|
||||
if ((m_canonize_instances && pinfo.is_inst_implicit()) || (m_canonize_proofs && pinfo.is_prop())) {
|
||||
if ((m_cfg.m_canonize_instances && pinfo.is_inst_implicit()) ||
|
||||
(m_cfg.m_canonize_proofs && pinfo.is_prop())) {
|
||||
new_a = m_defeq_canonizer.canonize(args[i], m_need_restart);
|
||||
lean_simp_trace(m_ctx, name({"simplify", "canonize"}),
|
||||
tout() << "\n" << args[i] << "\n==>\n" << new_a << "\n";);
|
||||
|
|
@ -265,11 +280,11 @@ simp_result simplify_core_fn::try_user_congr(expr const & e, simp_lemma const &
|
|||
lean_verify(is_simp_relation(tmp_ctx.env(), m_type, h_rel, h_lhs, h_rhs) && is_constant(h_rel));
|
||||
{
|
||||
relations.push_back(const_name(h_rel));
|
||||
flet<simp_lemmas> set_slss(m_slss, m_contextual ? add_to_slss(m_slss, local_factory.as_buffer()) : m_slss);
|
||||
flet<simp_lemmas> set_slss(m_slss, m_cfg.m_contextual ? add_to_slss(m_slss, local_factory.as_buffer()) : m_slss);
|
||||
|
||||
h_lhs = tmp_ctx.instantiate_mvars(h_lhs);
|
||||
|
||||
if (m_contextual || m_rel != const_name(h_rel)) {
|
||||
if (m_cfg.m_contextual || m_rel != const_name(h_rel)) {
|
||||
flet<name> set_name(m_rel, const_name(h_rel));
|
||||
freset<simplify_cache> reset_cache(m_cache);
|
||||
congr_hyp_results.emplace_back(visit(h_lhs, some_expr(e)));
|
||||
|
|
@ -561,7 +576,7 @@ struct match_fn {
|
|||
};
|
||||
|
||||
bool simplify_core_fn::match(tmp_type_context & ctx, simp_lemma const & sl, expr const & t) {
|
||||
if (m_use_matcher)
|
||||
if (m_cfg.m_use_matcher)
|
||||
return match_fn(ctx, sl.get_id())(sl.get_lhs(), t);
|
||||
else
|
||||
return ctx.is_def_eq(t, sl.get_lhs());
|
||||
|
|
@ -743,7 +758,7 @@ simp_result simplify_core_fn::visit(expr const & e, optional<expr> const & paren
|
|||
}
|
||||
}
|
||||
|
||||
if (m_lift_eq && m_rel != get_eq_name()) {
|
||||
if (m_cfg.m_lift_eq && m_rel != get_eq_name()) {
|
||||
simp_result eq_result;
|
||||
{
|
||||
flet<name> use_eq(m_rel, get_eq_name());
|
||||
|
|
@ -819,7 +834,10 @@ simp_result simplify_core_fn::visit_pi(expr const & e) {
|
|||
}
|
||||
|
||||
simp_result simplify_core_fn::visit_let(expr const & e) {
|
||||
return simp_result(e);
|
||||
if (m_cfg.m_zeta)
|
||||
return visit(instantiate(let_body(e), let_value(e)), none_expr());
|
||||
else
|
||||
return simp_result(e);
|
||||
}
|
||||
|
||||
simp_result simplify_core_fn::visit_macro(expr const & e) {
|
||||
|
|
@ -835,10 +853,8 @@ optional<pair<simp_result, bool>> simplify_core_fn::post(expr const &, optional<
|
|||
}
|
||||
|
||||
simplify_core_fn::simplify_core_fn(type_context & ctx, defeq_canonizer::state & dcs, simp_lemmas const & slss,
|
||||
unsigned max_steps, bool contextual, bool lift_eq,
|
||||
bool canonize_instances, bool canonize_proofs):
|
||||
m_ctx(ctx), m_defeq_canonizer(m_ctx, dcs), m_slss(slss), m_max_steps(max_steps), m_contextual(contextual),
|
||||
m_lift_eq(lift_eq), m_canonize_instances(canonize_instances), m_canonize_proofs(canonize_proofs) {
|
||||
simplify_config const & cfg):
|
||||
m_ctx(ctx), m_defeq_canonizer(m_ctx, dcs), m_slss(slss), m_cfg(cfg) {
|
||||
}
|
||||
|
||||
simp_result simplify_core_fn::simplify(expr const & e) {
|
||||
|
|
@ -899,15 +915,12 @@ optional<expr> simplify_core_fn::prove_by_simp(name const & rel, expr const & e)
|
|||
------------------------------------ */
|
||||
|
||||
simplify_ext_core_fn::simplify_ext_core_fn(type_context & ctx, defeq_can_state & dcs, 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, dcs, slss, max_steps, contextual, lift_eq, canonize_instances, canonize_proofs),
|
||||
m_use_axioms (use_axioms) {
|
||||
simplify_config const & cfg):
|
||||
simplify_core_fn(ctx, dcs, slss, cfg) {
|
||||
}
|
||||
|
||||
simp_result simplify_ext_core_fn::visit_lambda(expr const & e) {
|
||||
if (m_rel != get_eq_name() || !m_use_axioms) return simp_result(e);
|
||||
if (m_rel != get_eq_name() || !m_cfg.m_use_axioms) return simp_result(e);
|
||||
type_context::tmp_locals locals(m_ctx);
|
||||
expr it = e;
|
||||
while (is_lambda(it)) {
|
||||
|
|
@ -997,7 +1010,7 @@ simp_result simplify_ext_core_fn::imp_congr(expr const & e) {
|
|||
expr const & a = binding_domain(e);
|
||||
expr const & b = binding_body(e);
|
||||
simp_result r_a = visit(a, some_expr(e));
|
||||
if (m_contextual) {
|
||||
if (m_cfg.m_contextual) {
|
||||
type_context::tmp_locals locals(m_ctx);
|
||||
expr h = locals.push_local("_h", r_a.get_new());
|
||||
flet<simp_lemmas> set_slss(m_slss, add_to_slss(m_slss, locals.as_buffer()));
|
||||
|
|
@ -1031,7 +1044,7 @@ simp_result simplify_ext_core_fn::imp_congr(expr const & 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_rel == get_eq_name() && m_cfg.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);
|
||||
|
|
@ -1043,9 +1056,9 @@ simp_result simplify_ext_core_fn::visit_pi(expr const & 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
|
||||
/* TODO(Leo): when m_zeta is false, we need to implement efficient code for checking whether the abstraction of
|
||||
a let-body is type correct or not */
|
||||
return simp_result(e);
|
||||
return simplify_core_fn::visit_let(e);
|
||||
}
|
||||
|
||||
static optional<pair<simp_result, bool>> to_ext_result(simp_result const & r) {
|
||||
|
|
@ -1067,7 +1080,7 @@ optional<pair<simp_result, bool>> simplify_fn::post(expr const & e, optional<exp
|
|||
simp_result r = rewrite(e);
|
||||
if (r.get_new() != e) {
|
||||
return to_ext_result(r);
|
||||
} else if (!m_use_axioms) {
|
||||
} else if (!m_cfg.m_use_axioms) {
|
||||
return no_ext_result();
|
||||
} else {
|
||||
r = propext_rewrite(e);
|
||||
|
|
@ -1136,13 +1149,9 @@ class vm_simplify_fn : public simplify_ext_core_fn {
|
|||
}
|
||||
|
||||
public:
|
||||
vm_simplify_fn(type_context & ctx, defeq_can_state & dcs, 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,
|
||||
tactic_state const & s):
|
||||
simplify_ext_core_fn(ctx, dcs, slss, max_steps, contextual, lift_eq,
|
||||
canonize_instances, canonize_proofs, use_axioms),
|
||||
vm_simplify_fn(type_context & ctx, defeq_can_state & dcs, simp_lemmas const & slss, simplify_config const & cfg,
|
||||
vm_obj const & prove, vm_obj const & pre, vm_obj const & post, tactic_state const & s):
|
||||
simplify_ext_core_fn(ctx, dcs, slss, cfg),
|
||||
m_prove(prove), m_pre(pre), m_post(post),
|
||||
m_s(s) {}
|
||||
|
||||
|
|
@ -1153,25 +1162,6 @@ public:
|
|||
}
|
||||
};
|
||||
|
||||
/*
|
||||
structure simplify_config :=
|
||||
(max_steps : nat)
|
||||
(contextual : bool)
|
||||
(lift_eq : bool)
|
||||
(canonize_instances : bool)
|
||||
(canonize_proofs : bool)
|
||||
(use_axioms : bool)
|
||||
*/
|
||||
void get_simplify_config(vm_obj const & obj, unsigned & max_steps, bool & contextual, bool & lift_eq,
|
||||
bool & canonize_instances, bool & canonize_proofs, bool & use_axioms) {
|
||||
max_steps = force_to_unsigned(cfield(obj, 0), std::numeric_limits<unsigned>::max());
|
||||
contextual = to_bool(cfield(obj, 1));
|
||||
lift_eq = to_bool(cfield(obj, 2));
|
||||
canonize_instances = to_bool(cfield(obj, 3));
|
||||
canonize_proofs = to_bool(cfield(obj, 4));
|
||||
use_axioms = to_bool(cfield(obj, 5));
|
||||
}
|
||||
|
||||
/*
|
||||
meta constant simplify_core
|
||||
(c : simplify_config)
|
||||
|
|
@ -1182,12 +1172,10 @@ meta constant simplify_core
|
|||
vm_obj tactic_simplify_core(vm_obj const & c, vm_obj const & slss, vm_obj const & rel, vm_obj const & e, vm_obj const & _s) {
|
||||
tactic_state const & s = tactic::to_state(_s);
|
||||
try {
|
||||
unsigned max_steps; bool contextual, lift_eq, canonize_instances, canonize_proofs, use_axioms;
|
||||
get_simplify_config(c, max_steps, contextual, lift_eq, canonize_instances, canonize_proofs, use_axioms);
|
||||
simplify_config cfg(c);
|
||||
type_context ctx = mk_type_context_for(s, transparency_mode::Reducible);
|
||||
defeq_can_state dcs = s.dcs();
|
||||
simplify_fn simp(ctx, dcs, to_simp_lemmas(slss), max_steps, contextual, lift_eq,
|
||||
canonize_instances, canonize_proofs, use_axioms);
|
||||
simplify_fn simp(ctx, dcs, to_simp_lemmas(slss), cfg);
|
||||
simp_result result = simp(to_name(rel), to_expr(e));
|
||||
if (result.get_new() != to_expr(e)) {
|
||||
result = finalize(ctx, to_name(rel), result);
|
||||
|
|
@ -1205,12 +1193,10 @@ static vm_obj ext_simplify_core(vm_obj const & a, vm_obj const & c, simp_lemmas
|
|||
vm_obj const & pre, vm_obj const & post, name const & r, expr const & e,
|
||||
tactic_state const & s) {
|
||||
try {
|
||||
unsigned max_steps; bool contextual, lift_eq, canonize_instances, canonize_proofs, use_axioms;
|
||||
get_simplify_config(c, max_steps, contextual, lift_eq, canonize_instances, canonize_proofs, use_axioms);
|
||||
simplify_config cfg(c);
|
||||
type_context ctx = mk_type_context_for(s, transparency_mode::Reducible);
|
||||
defeq_can_state dcs = s.dcs();
|
||||
vm_simplify_fn simp(ctx, dcs, slss, max_steps, contextual, lift_eq, canonize_instances, canonize_proofs,
|
||||
use_axioms, prove, pre, post, s);
|
||||
vm_simplify_fn simp(ctx, dcs, slss, cfg, prove, pre, post, s);
|
||||
pair<vm_obj, simp_result> p = simp(a, r, e);
|
||||
if (p.second.get_new() != e) {
|
||||
vm_obj const & a = p.first;
|
||||
|
|
|
|||
|
|
@ -12,6 +12,32 @@ Author: Daniel Selsam, Leonardo de Moura
|
|||
#include "library/tactic/simp_result.h"
|
||||
|
||||
namespace lean {
|
||||
|
||||
/*
|
||||
structure simplify_config :=
|
||||
(max_steps : nat)
|
||||
(contextual : bool)
|
||||
(lift_eq : bool)
|
||||
(canonize_instances : bool)
|
||||
(canonize_proofs : bool)
|
||||
(use_axioms : bool)
|
||||
(zeta : bool)
|
||||
*/
|
||||
struct simplify_config {
|
||||
unsigned m_max_steps;
|
||||
bool m_contextual;
|
||||
bool m_lift_eq;
|
||||
bool m_canonize_instances;
|
||||
bool m_canonize_proofs;
|
||||
bool m_use_axioms;
|
||||
bool m_zeta;
|
||||
/* The following option should be removed as soon as we
|
||||
refactor the inductive compiler. */
|
||||
bool m_use_matcher{true};
|
||||
simplify_config();
|
||||
simplify_config(vm_obj const & o);
|
||||
};
|
||||
|
||||
/* Core simplification procedure. It performs the following tasks:
|
||||
1- Manages the cache;
|
||||
2- Applies congruence lemmas;
|
||||
|
|
@ -46,19 +72,14 @@ protected:
|
|||
bool m_need_restart{false};
|
||||
|
||||
/* Options */
|
||||
unsigned m_max_steps;
|
||||
bool m_contextual;
|
||||
bool m_lift_eq;
|
||||
bool m_canonize_instances;
|
||||
bool m_canonize_proofs;
|
||||
/* The following option should be removed as soon as we
|
||||
refactor the inductive compiler. */
|
||||
bool m_use_matcher{true};
|
||||
simplify_config m_cfg;
|
||||
|
||||
simp_result join(simp_result const & r1, simp_result const & r2);
|
||||
void inc_num_steps();
|
||||
bool is_dependent_fn(expr const & f);
|
||||
bool should_defeq_canonize() const { return m_canonize_instances || m_canonize_proofs; }
|
||||
bool should_defeq_canonize() const {
|
||||
return m_cfg.m_canonize_instances || m_cfg.m_canonize_proofs;
|
||||
}
|
||||
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);
|
||||
|
|
@ -107,14 +128,11 @@ protected:
|
|||
|
||||
public:
|
||||
simplify_core_fn(type_context & ctx, defeq_canonizer::state & dcs, simp_lemmas const & slss,
|
||||
unsigned max_steps, bool contextual, bool lift_eq,
|
||||
bool canonize_instances, bool canonize_proofs);
|
||||
simplify_config const & cfg);
|
||||
|
||||
environment const & env() const;
|
||||
simp_result operator()(name const & rel, expr const & e);
|
||||
|
||||
void set_use_matcher(bool flag) { m_use_matcher = flag; }
|
||||
|
||||
optional<expr> prove_by_simp(name const & rel, expr const & e);
|
||||
};
|
||||
|
||||
|
|
@ -122,7 +140,6 @@ public:
|
|||
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;
|
||||
|
|
@ -130,8 +147,7 @@ protected:
|
|||
virtual simp_result visit_let(expr const & e) override;
|
||||
public:
|
||||
simplify_ext_core_fn(type_context & ctx, defeq_canonizer::state & dcs, simp_lemmas const & slss,
|
||||
unsigned max_steps, bool contextual, bool lift_eq,
|
||||
bool canonize_instances, bool canonize_proofs, bool use_axioms);
|
||||
simplify_config const & cfg);
|
||||
};
|
||||
|
||||
/* Default (bottom-up) simplifier: reduce projections, apply simplification lemmas,
|
||||
|
|
@ -143,10 +159,8 @@ protected:
|
|||
virtual optional<expr> prove(expr const & e) override;
|
||||
public:
|
||||
simplify_fn(type_context & ctx, defeq_canonizer::state & dcs, 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, dcs, slss, max_steps, contextual, lift_eq,
|
||||
canonize_instances, canonize_proofs, use_axioms) {}
|
||||
simplify_config const & cfg):
|
||||
simplify_ext_core_fn(ctx, dcs, slss, cfg) {}
|
||||
};
|
||||
|
||||
void initialize_simplify();
|
||||
|
|
|
|||
|
|
@ -209,15 +209,15 @@ static dsimplify_fn mk_dsimp(type_context & ctx, defeq_can_state & dcs, smt_pre_
|
|||
}
|
||||
|
||||
static simplify_fn mk_simp(type_context & ctx, defeq_can_state & dcs, smt_pre_config const & cfg) {
|
||||
unsigned max_steps = cfg.m_max_steps;
|
||||
bool contextual = false;
|
||||
bool lift_eq = true;
|
||||
bool canonize_instances = true;
|
||||
bool canonize_proofs = false;
|
||||
bool use_axioms = true;
|
||||
return simplify_fn(ctx, dcs, cfg.m_simp_lemmas, max_steps,
|
||||
contextual, lift_eq, canonize_instances,
|
||||
canonize_proofs, use_axioms);
|
||||
simplify_config scfg;
|
||||
scfg.m_max_steps = cfg.m_max_steps;
|
||||
scfg.m_contextual = false;
|
||||
scfg.m_lift_eq = true;
|
||||
scfg.m_canonize_instances = true;
|
||||
scfg.m_canonize_proofs = false;
|
||||
scfg.m_use_axioms = true;
|
||||
scfg.m_zeta = cfg.m_zeta;
|
||||
return simplify_fn(ctx, dcs, cfg.m_simp_lemmas, scfg);
|
||||
}
|
||||
|
||||
static simp_result preprocess(type_context & ctx, defeq_can_state & dcs, smt_pre_config const & cfg, expr const & e) {
|
||||
|
|
|
|||
|
|
@ -63,6 +63,6 @@ begin
|
|||
induction n with n',
|
||||
{intro, reflexivity},
|
||||
{intro,
|
||||
simp [test], dsimp, simp [ih_1],
|
||||
simp [test] {zeta := ff}, dsimp, simp [ih_1],
|
||||
simp [nat.bit1_eq_succ_bit0, test]}
|
||||
end
|
||||
|
|
|
|||
|
|
@ -2,4 +2,4 @@ example (p q : Prop) (h : p) : q ∨ p :=
|
|||
by simp [h]
|
||||
|
||||
example (p q : Prop) : p → q ∨ p :=
|
||||
by ctx_simp
|
||||
by simp {contextual := tt}
|
||||
|
|
|
|||
|
|
@ -45,4 +45,4 @@ begin
|
|||
end
|
||||
open tactic
|
||||
example (a b : nat) : a = b → h 0 a = b :=
|
||||
by ctx_simp without bla
|
||||
by simp without bla {contextual := tt}
|
||||
|
|
|
|||
|
|
@ -7,5 +7,5 @@ sorry
|
|||
|
||||
print [congr] default
|
||||
|
||||
example (A : Type) (a b c : A) : (a = b) → (a = c) → a = b := by ctx_simp
|
||||
example (A : Type) (a b c : A) : (a = c) → (a = b) → a = b := by ctx_simp
|
||||
example (A : Type) (a b c : A) : (a = b) → (a = c) → a = b := by simp {contextual := tt}
|
||||
example (A : Type) (a b c : A) : (a = c) → (a = b) → a = b := by simp {contextual := tt}
|
||||
|
|
|
|||
|
|
@ -3,6 +3,7 @@ declare_trace mini_crush
|
|||
namespace mini_crush
|
||||
open smt_tactic tactic
|
||||
|
||||
/- Collect relevant functions -/
|
||||
meta def is_auto_construction : name → bool
|
||||
| (name.mk_string "brec_on" p) := tt
|
||||
| (name.mk_string "cases_on" p) := tt
|
||||
|
|
@ -36,6 +37,24 @@ do ctx ← local_context,
|
|||
s₁ ← mfoldl (λ s e, infer_type e >>= collect_revelant_fns_aux s) mk_name_set ctx,
|
||||
target >>= collect_revelant_fns_aux s₁
|
||||
|
||||
/- repeat simp & intro -/
|
||||
|
||||
meta def simph_and_intro_aux : simp_lemmas → tactic unit
|
||||
| S := do
|
||||
t ← target,
|
||||
|
||||
|
||||
return ()
|
||||
|
||||
meta def simph_and_intro : tactic unit :=
|
||||
do S ← simp_lemmas.mk_default,
|
||||
S ← collect_ctx_simps >>= S^.append,
|
||||
simph_and_intro_aux S
|
||||
|
||||
|
||||
meta def collect_ctx_simps : tactic (list expr) :=
|
||||
|
||||
|
||||
meta def size (e : expr) : nat :=
|
||||
e^.fold 1 (λ e _ n, n+1)
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue