feat(library/equations_compiler): add option eqn_compiler.zeta

src/library/equations_compiler/compiler.cpp

@@ -236,8 +236,6 @@ expr compile_equations(environment & env, options const & opts, metavar_context
 }
 
 void initialize_compiler() {
-    register_trace_class("eqn_compiler");
-    register_trace_class(name{"debug", "eqn_compiler"});
 }
 void finalize_compiler() {
 }

src/library/equations_compiler/elim_match.cpp

@@ -1208,7 +1208,7 @@ expr mk_nonrec(environment & env, options const & opts, metavar_context & mctx,
     type_context ctx1(env, opts, mctx, lctx, transparency_mode::Semireducible);
     expr fn_type = ctx1.infer(R.m_fn);
     expr fn;
-    std::tie(env, fn) = mk_aux_definition(env, mctx, lctx, header.m_is_private, header.m_is_lemma, header.m_is_noncomputable,
+    std::tie(env, fn) = mk_aux_definition(env, opts, mctx, lctx, header.m_is_private, header.m_is_lemma, header.m_is_noncomputable,
                                           head(header.m_fn_names), fn_type, R.m_fn);
     name fn_name = const_name(get_app_fn(fn));
     unsigned eqn_idx     = 1;

src/library/equations_compiler/structural_rec.cpp

@@ -609,7 +609,7 @@ struct structural_rec_fn {
             return new_fn;
         } else {
             expr r;
-            std::tie(m_env, r) = mk_aux_definition(m_env, m_mctx, m_lctx, m_header.m_is_private, m_header.m_is_lemma,
+            std::tie(m_env, r) = mk_aux_definition(m_env, m_opts, m_mctx, m_lctx, m_header.m_is_private, m_header.m_is_lemma,
                                                    m_header.m_is_noncomputable, head(m_header.m_fn_names), m_fn_type, new_fn);
             return r;
         }

src/library/equations_compiler/util.cpp

@@ -32,9 +32,14 @@ Author: Leonardo de Moura
 #define LEAN_DEFAULT_EQN_COMPILER_LEMMAS true
 #endif
 
+#ifndef LEAN_DEFAULT_EQN_COMPILER_ZETA
+#define LEAN_DEFAULT_EQN_COMPILER_ZETA false
+#endif
+
 namespace lean {
 static name * g_eqn_compiler_dsimp  = nullptr;
 static name * g_eqn_compiler_lemmas = nullptr;
+static name * g_eqn_compiler_zeta   = nullptr;
 
 static bool get_eqn_compiler_dsimp(options const & o) {
     return o.get_bool(*g_eqn_compiler_dsimp, LEAN_DEFAULT_EQN_COMPILER_DSIMP);
@@ -44,6 +49,10 @@ static bool get_eqn_compiler_lemmas(options const & o) {
     return o.get_bool(*g_eqn_compiler_lemmas, LEAN_DEFAULT_EQN_COMPILER_LEMMAS);
 }
 
+static bool get_eqn_compiler_zeta(options const & o) {
+    return o.get_bool(*g_eqn_compiler_zeta, LEAN_DEFAULT_EQN_COMPILER_ZETA);
+}
+
 [[ noreturn ]] void throw_ill_formed_eqns() {
     throw exception("ill-formed match/equations expression");
 }
@@ -236,16 +245,37 @@ static pair<environment, name> mk_def_name(environment const & env, bool is_priv
     }
 }
 
-pair<environment, expr> mk_aux_definition(environment const & env, metavar_context const & mctx, local_context const & lctx,
+static void throw_mk_aux_definition_error(local_context const & lctx, name const & c, expr const & type, expr const & value, exception & ex) {
+    sstream strm;
+    strm << "equation compiler failed to create auxiliary declaration '" << c << "'";
+    if (contains_let_local_decl(lctx, type) || contains_let_local_decl(lctx, value)) {
+        strm << ", auxiliary declaration has references to let-declarations (possible solution: use 'set_option eqn_compiler.zeta true')";
+    }
+    throw nested_exception(strm, ex);
+}
+
+pair<environment, expr> mk_aux_definition(environment const & env, options const & opts, metavar_context const & mctx, local_context const & lctx,
                                           bool is_private, bool is_lemma, bool is_noncomputable,
                                           name const & c, expr const & type, expr const & value) {
+    lean_trace("eqn_compiler", tout() << "declaring auxiliary definition\n" << c << " : " << type << "\n";);
     environment new_env = env;
+    expr new_type       = type;
+    expr new_value      = value;
+    bool zeta           = get_eqn_compiler_zeta(opts);
+    if (zeta) {
+        new_type  = zeta_expand(lctx, new_type);
+        new_value = zeta_expand(lctx, new_value);
+    }
     name new_c;
     std::tie(new_env, new_c) = mk_def_name(env, is_private, c);
     expr r;
-    std::tie(new_env, r) = is_lemma ?
-        mk_aux_lemma(new_env, mctx, lctx, new_c, type, value) :
-        mk_aux_definition(new_env, mctx, lctx, new_c, type, value);
+    try {
+        std::tie(new_env, r) = is_lemma ?
+            mk_aux_lemma(new_env, mctx, lctx, new_c, new_type, new_value) :
+            mk_aux_definition(new_env, mctx, lctx, new_c, new_type, new_value);
+    } catch (exception & ex) {
+        throw_mk_aux_definition_error(lctx, c, new_type, new_value, ex);
+    }
     if (!is_lemma && !is_noncomputable) {
         try {
             declaration d = new_env.get(new_c);
@@ -280,7 +310,17 @@ static environment add_equation_lemma(environment const & env, options const & o
                                    "defeq simplifier error message:\n", ex);
         }
     }
-    std::tie(new_env, r) = mk_aux_definition(new_env, mctx, lctx, new_c, new_type, value);
+    expr new_value = value;
+    bool zeta      = get_eqn_compiler_zeta(opts);
+    if (zeta) {
+        new_type   = zeta_expand(lctx, new_type);
+        new_value  = zeta_expand(lctx, new_value);
+    }
+    try {
+        std::tie(new_env, r) = mk_aux_definition(new_env, mctx, lctx, new_c, new_type, new_value);
+    } catch (exception & ex) {
+        throw_mk_aux_definition_error(lctx, c, new_type, new_value, ex);
+    }
     return new_env;
 }
 
@@ -458,13 +498,18 @@ environment mk_equation_lemma(environment const & env, options const & opts, met
 }
 
 void initialize_eqn_compiler_util() {
+    register_trace_class("eqn_compiler");
+    register_trace_class(name{"debug", "eqn_compiler"});
     g_eqn_compiler_dsimp  = new name{"eqn_compiler", "dsimp"};
     g_eqn_compiler_lemmas = new name{"eqn_compiler", "lemmas"};
+    g_eqn_compiler_zeta   = new name{"eqn_compiler", "zeta"};
     register_bool_option(*g_eqn_compiler_dsimp, LEAN_DEFAULT_EQN_COMPILER_DSIMP,
                          "(equation compiler) use defeq simplifier to cleanup types of "
                          "automatically synthesized equational lemmas");
     register_bool_option(*g_eqn_compiler_lemmas, LEAN_DEFAULT_EQN_COMPILER_LEMMAS,
                          "(equation compiler) generate equation lemmas and induction principle");
+    register_bool_option(*g_eqn_compiler_zeta, LEAN_DEFAULT_EQN_COMPILER_ZETA,
+                         "(equation compiler) apply zeta-expansion (expand references to let-declarations) before creating auxiliary definitions.");
     g_eqn_sanitizer_token = register_defeq_simp_attribute("eqn_sanitizer");
 }
 

src/library/equations_compiler/util.h

@@ -75,7 +75,7 @@ bool is_recursive_eqns(type_context & ctx, expr const & e);
 expr erase_inaccessible_annotations(expr const & e);
 list<expr> erase_inaccessible_annotations(list<expr> const & es);
 
-pair<environment, expr> mk_aux_definition(environment const & env, metavar_context const & mctx, local_context const & lctx,
+pair<environment, expr> mk_aux_definition(environment const & env, options const & opts, metavar_context const & mctx, local_context const & lctx,
                                           bool is_private, bool is_lemma, bool is_noncomputable, name const & n, expr const & type, expr const & value);
 
 environment mk_equation_lemma(environment const & env, options const & opts, metavar_context const & mctx, local_context const & lctx,

src/library/local_context.cpp

@@ -7,6 +7,8 @@ Author: Leonardo de Moura
 #include <limits>
 #include "util/fresh_name.h"
 #include "kernel/for_each_fn.h"
+#include "kernel/find_fn.h"
+#include "kernel/replace_fn.h"
 #include "library/pp_options.h"
 #include "library/local_context.h"
 #include "library/metavar_context.h"
@@ -382,6 +384,29 @@ local_context local_context::instantiate_mvars(metavar_context & mctx) const {
     return r;
 }
 
+bool contains_let_local_decl(local_context const & lctx, expr const & e) {
+    if (!has_local(e)) return false;
+    return static_cast<bool>(find(e, [&](expr const & e, unsigned) {
+                if (!is_local(e)) return false;
+                auto d = lctx.get_local_decl(e);
+                return d && d->get_value();
+            }));
+}
+
+expr zeta_expand(local_context const & lctx, expr const & e) {
+    if (!contains_let_local_decl(lctx, e)) return e;
+    return replace(e, [&](expr const & e, unsigned) {
+            if (!has_local(e)) return some_expr(e);
+            if (is_local(e)) {
+                if (auto d = lctx.get_local_decl(e)) {
+                    if (auto v = d->get_value())
+                        return some_expr(zeta_expand(lctx, *v));
+                }
+            }
+            return none_expr();
+        });
+}
+
 void initialize_local_context() {
     g_local_prefix = new name(name::mk_internal_unique_name());
     g_dummy_type   = new expr(mk_constant(name::mk_internal_unique_name()));

src/library/local_context.h

@@ -179,6 +179,12 @@ public:
     local_context instantiate_mvars(metavar_context & ctx) const;
 };
 
+/** \brief Return true iff `e` contains a local_decl_ref that contains a value */
+bool contains_let_local_decl(local_context const & lctx, expr const & e);
+
+/** \brief Expand all local_decl_refs (that have values) in `e` */
+expr zeta_expand(local_context const & lctx, expr const & e);
+
 void initialize_local_context();
 void finalize_local_context();
 }

tests/lean/aux_decl_zeta.lean

@@ -0,0 +1,24 @@
+set_option new_elaborator true
+
+inductive vec (A : Type) : nat → Type
+| nil  : vec 0
+| cons : Π {n}, A → vec n → vec (n+1)
+
+definition f : bool → Prop
+| x :=
+  let m := 10,
+      n := m in
+  match x with
+  | tt := true
+  | ff := ∀ (x : vec nat 10) (w : vec nat n), x = w
+  end
+
+set_option eqn_compiler.zeta true
+definition f : bool → Prop
+| x :=
+  let m := 10,
+      n := m in
+  match x with
+  | tt := true
+  | ff := ∀ (x : vec nat 10) (w : vec nat n), x = w
+  end

tests/lean/aux_decl_zeta.lean.expected.out

@@ -0,0 +1,10 @@
+aux_decl_zeta.lean:7:0: error: equation compiler failed to create auxiliary declaration 'f._main._match_1', auxiliary declaration has references to let-declarations (possible solution: use 'set_option eqn_compiler.zeta true')
+nested exception message:
+type mismatch at application
+  x = w
+term
+  w
+has type
+  vec ℕ n
+but is expected to have type
+  vec ℕ 10