feat(library/equations_compiler): prove equational lemmas for auxiliary definition

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; }

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();

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

src/library/equations_compiler/util.cpp

@@ -565,6 +565,20 @@ static expr prove_eqn_lemma_core(type_context & ctx, buffer<expr> const & Hs, ex
 }
 
 static expr prove_eqn_lemma(type_context & ctx, buffer<expr> const & Hs, expr const & lhs, expr const & rhs) {
+    if (auto new_lhs = unfold_app(ctx.env(), lhs)) {
+        buffer<expr> 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);
 }

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<expr> 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, "

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

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