From fa863496da300cb5087ad641dac2a1eb24d0d92f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 20 May 2017 16:38:32 -0700 Subject: [PATCH] feat(library/equations_compiler): prove equational lemmas for auxiliary definition --- src/library/constants.cpp | 4 ++ src/library/constants.h | 1 + src/library/constants.txt | 1 + src/library/equations_compiler/util.cpp | 14 +++++ src/library/equations_compiler/wf_rec.cpp | 63 ++++++++++++++++++++++- tests/lean/run/check_constants.lean | 1 + tmp/even_odd.lean | 4 -- 7 files changed, 83 insertions(+), 5 deletions(-) diff --git a/src/library/constants.cpp b/src/library/constants.cpp index 9e95e0aa37..d8a995e0a7 100644 --- a/src/library/constants.cpp +++ b/src/library/constants.cpp @@ -371,6 +371,7 @@ name const * g_vm_monitor = nullptr; name const * g_weak_order = nullptr; name const * g_well_founded = nullptr; name const * g_well_founded_fix = nullptr; +name const * g_well_founded_fix_eq = nullptr; name const * g_xor = nullptr; name const * g_zero_le_one = nullptr; name const * g_zero_lt_one = nullptr; @@ -744,6 +745,7 @@ void initialize_constants() { g_weak_order = new name{"weak_order"}; g_well_founded = new name{"well_founded"}; g_well_founded_fix = new name{"well_founded", "fix"}; + g_well_founded_fix_eq = new name{"well_founded", "fix_eq"}; g_xor = new name{"xor"}; g_zero_le_one = new name{"zero_le_one"}; g_zero_lt_one = new name{"zero_lt_one"}; @@ -1118,6 +1120,7 @@ void finalize_constants() { delete g_weak_order; delete g_well_founded; delete g_well_founded_fix; + delete g_well_founded_fix_eq; delete g_xor; delete g_zero_le_one; delete g_zero_lt_one; @@ -1491,6 +1494,7 @@ name const & get_vm_monitor_name() { return *g_vm_monitor; } name const & get_weak_order_name() { return *g_weak_order; } name const & get_well_founded_name() { return *g_well_founded; } name const & get_well_founded_fix_name() { return *g_well_founded_fix; } +name const & get_well_founded_fix_eq_name() { return *g_well_founded_fix_eq; } name const & get_xor_name() { return *g_xor; } name const & get_zero_le_one_name() { return *g_zero_le_one; } name const & get_zero_lt_one_name() { return *g_zero_lt_one; } diff --git a/src/library/constants.h b/src/library/constants.h index b0037bdb9b..5ce924eb42 100644 --- a/src/library/constants.h +++ b/src/library/constants.h @@ -373,6 +373,7 @@ name const & get_vm_monitor_name(); name const & get_weak_order_name(); name const & get_well_founded_name(); name const & get_well_founded_fix_name(); +name const & get_well_founded_fix_eq_name(); name const & get_xor_name(); name const & get_zero_le_one_name(); name const & get_zero_lt_one_name(); diff --git a/src/library/constants.txt b/src/library/constants.txt index 3629fd2826..1fa3c12eea 100644 --- a/src/library/constants.txt +++ b/src/library/constants.txt @@ -366,6 +366,7 @@ vm_monitor weak_order well_founded well_founded.fix +well_founded.fix_eq xor zero_le_one zero_lt_one diff --git a/src/library/equations_compiler/util.cpp b/src/library/equations_compiler/util.cpp index 85cf9b572d..2b9127218c 100644 --- a/src/library/equations_compiler/util.cpp +++ b/src/library/equations_compiler/util.cpp @@ -565,6 +565,20 @@ static expr prove_eqn_lemma_core(type_context & ctx, buffer const & Hs, ex } static expr prove_eqn_lemma(type_context & ctx, buffer const & Hs, expr const & lhs, expr const & rhs) { + if (auto new_lhs = unfold_app(ctx.env(), lhs)) { + buffer args; + expr fn = get_app_args(*new_lhs, args); + if (is_constant(fn, get_well_founded_fix_name()) && + args.size() == 6) { + expr H1 = mk_app(mk_constant(get_well_founded_fix_eq_name(), const_levels(fn)), args.size(), args.data()); + expr H1_type = ctx.relaxed_whnf(ctx.infer(H1)); + expr lhs_dummy, new_lhs; + lean_verify(is_eq(H1_type, lhs_dummy, new_lhs)); + expr H2 = prove_eqn_lemma_core(ctx, Hs, new_lhs, rhs, true); + expr body = mk_eq_trans(ctx, H1, H2); + return ctx.mk_lambda(Hs, body); + } + } expr body = prove_eqn_lemma_core(ctx, Hs, lhs, rhs, true); return ctx.mk_lambda(Hs, body); } diff --git a/src/library/equations_compiler/wf_rec.cpp b/src/library/equations_compiler/wf_rec.cpp index 53db2a5fdf..43eb323f1b 100644 --- a/src/library/equations_compiler/wf_rec.cpp +++ b/src/library/equations_compiler/wf_rec.cpp @@ -19,8 +19,8 @@ Author: Leonardo de Moura namespace lean { #define trace_wf(Code) lean_trace(name({"eqn_compiler", "wf_rec"}), type_context ctx = mk_type_context(); scope_trace_env _scope1(m_env, ctx); Code) - #define trace_debug_wf(Code) lean_trace(name({"debug", "eqn_compiler", "wf_rec"}), type_context ctx = mk_type_context(); scope_trace_env _scope1(m_env, ctx); Code) +#define trace_debug_wf_aux(Code) lean_trace(name({"debug", "eqn_compiler", "wf_rec"}), scope_trace_env _scope1(m_env, ctx); Code) struct wf_rec_fn { environment m_env; @@ -211,6 +211,62 @@ struct wf_rec_fn { return r; } + struct mk_lemma_rhs_fn : public replace_visitor_with_tc { + expr m_fn; + expr m_F; + + mk_lemma_rhs_fn(type_context & ctx, expr const & fn, expr const & F): + replace_visitor_with_tc(ctx), m_fn(fn), m_F(F) {} + + virtual expr visit_local(expr const & e) override { + if (e == m_F) { + throw exception("equation compiler failed when generation equational lemmas"); + } else { + return e; + } + } + + virtual expr visit_app(expr const & e) override { + if (is_app(app_fn(e)) && app_fn(app_fn(e)) == m_F) { + return mk_app(m_fn, visit(app_arg(app_fn(e)))); + } else { + return replace_visitor_with_tc::visit_app(e); + } + } + }; + + expr mk_lemma_rhs(type_context & ctx, expr const & fn, expr rhs) { + rhs = ctx.relaxed_whnf(rhs); + lean_assert(is_lambda(rhs)); + type_context::tmp_locals locals(ctx); + expr F = locals.push_local_from_binding(rhs); + rhs = instantiate(binding_body(rhs), F); + return mk_lemma_rhs_fn(ctx, fn, F)(rhs); + } + + void mk_lemmas(expr const & fn, list const & lemmas) { + name const & fn_name = const_name(get_app_fn(fn)); + unsigned eqn_idx = 1; + type_context ctx = mk_type_context(); + for (expr type : lemmas) { + type_context::tmp_locals locals(ctx); + type = ctx.relaxed_whnf(type); + while (is_pi(type)) { + expr local = locals.push_local_from_binding(type); + type = instantiate(binding_body(type), local); + } + lean_assert(is_eq(type)); + expr lhs = app_arg(app_fn(type)); + expr rhs = app_arg(type); + expr new_lhs = mk_app(fn, app_arg(lhs)); + expr new_rhs = mk_lemma_rhs(ctx, fn, rhs); + trace_debug_wf_aux(tout() << "aux equation [" << eqn_idx << "]:\n" << new_lhs << "\n=\n" << new_rhs << "\n";); + m_env = mk_equation_lemma(m_env, m_opts, m_mctx, ctx.lctx(), fn_name, + eqn_idx, m_header.m_is_private, locals.as_buffer(), new_lhs, new_rhs); + eqn_idx++; + } + } + expr operator()(expr eqns) { m_ref = eqns; m_header = get_equations_header(eqns); @@ -246,6 +302,11 @@ struct wf_rec_fn { expr fn = mk_fix_aux_function(get_equations_header(eqns), r.m_fn); trace_debug_wf(tout() << "after mk_fix\n" << fn << " :\n " << mk_type_context().infer(fn) << "\n";); + if (m_header.m_aux_lemmas) { + lean_assert(!m_header.m_is_meta); + mk_lemmas(fn, r.m_lemmas); + } + // TODO(Leo): throw exception("support for well-founded recursion has not been implemented yet, " diff --git a/tests/lean/run/check_constants.lean b/tests/lean/run/check_constants.lean index 971bcfbcb4..6be547d034 100644 --- a/tests/lean/run/check_constants.lean +++ b/tests/lean/run/check_constants.lean @@ -371,6 +371,7 @@ run_cmd script_check_id `vm_monitor run_cmd script_check_id `weak_order run_cmd script_check_id `well_founded run_cmd script_check_id `well_founded.fix +run_cmd script_check_id `well_founded.fix_eq run_cmd script_check_id `xor run_cmd script_check_id `zero_le_one run_cmd script_check_id `zero_lt_one diff --git a/tmp/even_odd.lean b/tmp/even_odd.lean index 758323d582..9652cd0279 100644 --- a/tmp/even_odd.lean +++ b/tmp/even_odd.lean @@ -1,13 +1,10 @@ import data.vector open nat universes u v -set_option pp.all true set_option trace.eqn_compiler.wf_rec true set_option trace.debug.eqn_compiler.wf_rec true set_option trace.debug.eqn_compiler.mutual true -set_option trace.eqn_compiler.elim_match true - mutual def even, odd with even : nat → bool @@ -17,7 +14,6 @@ with odd : nat → bool | 0 := ff | (a+1) := even a - mutual def f, g {α β : Type u} (f : α → β) (p : α × β) with f : Π n : nat, vector (α × β) n | 0 := vector.nil