feat(frontends/lean/calc_proof_elaborator): add 'elaborator.calc_assistant' option

src/frontends/lean/calc_proof_elaborator.cpp

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include "util/sexpr/option_declarations.h"
 #include "kernel/free_vars.h"
 #include "kernel/instantiate.h"
 #include "library/unifier.h"
@@ -14,7 +15,28 @@ Author: Leonardo de Moura
 #include "frontends/lean/info_manager.h"
 #include "frontends/lean/calc.h"
 
+#ifndef LEAN_DEFAULT_CALC_ASSISTANT
+#define LEAN_DEFAULT_CALC_ASSISTANT true
+#endif
+
 namespace lean {
+static name * g_elaborator_calc_assistant = nullptr;
+
+void initialize_calc_proof_elaborator() {
+    g_elaborator_calc_assistant = new name{"elaborator", "calc_assistant"};
+    register_bool_option(*g_elaborator_calc_assistant,  LEAN_DEFAULT_CALC_ASSISTANT,
+                         "(elaborator) when needed lean automatically adds symmetry, "
+                         "inserts missing arguments, and applies substitutions");
+}
+
+void finalize_calc_proof_elaborator() {
+    delete g_elaborator_calc_assistant;
+}
+
+bool get_elaborator_calc_assistant(options const & o) {
+    return o.get_bool(*g_elaborator_calc_assistant, LEAN_DEFAULT_CALC_ASSISTANT);
+}
+
 static optional<pair<expr, expr>> mk_op(environment const & env, local_context & ctx, name_generator & ngen, type_checker_ptr & tc,
                                         name const & op, unsigned nunivs, unsigned nargs, std::initializer_list<expr> const & explicit_args,
                                         constraint_seq & cs, tag g) {
@@ -95,8 +117,8 @@ static optional<pair<expr, expr>> apply_subst(environment const & env, local_con
       - adding !
       - adding subst
 */
-constraint mk_calc_proof_cnstr(environment const & env, local_context const & _ctx,
-                               expr const & m, expr const & _e,
+constraint mk_calc_proof_cnstr(environment const & env, options const & opts,
+                               local_context const & _ctx, expr const & m, expr const & _e,
                                constraint_seq const & cs, unifier_config const & cfg,
                                info_manager * im, bool relax) {
     justification j         = mk_failed_to_synthesize_jst(env, m);
@@ -112,19 +134,23 @@ constraint mk_calc_proof_cnstr(environment const & env, local_context const & _c
         e_type      = s.instantiate(e_type);
         e_type      = tc->whnf(e_type, new_cs);
         tag g       = e.get_tag();
-        // add '!' is needed
-        while (is_pi(e_type)) {
-            binder_info bi = binding_info(e_type);
-            if (!bi.is_implicit() && !bi.is_inst_implicit()) {
-                if (!has_free_var(binding_body(e_type), 0)) {
-                    // if the rest of the type does not reference argument,
-                    // then we also stop consuming arguments
-                    break;
+        bool calc_assistant = get_elaborator_calc_assistant(opts);
+
+        if (calc_assistant) {
+            // add '!' is needed
+            while (is_pi(e_type)) {
+                binder_info bi = binding_info(e_type);
+                if (!bi.is_implicit() && !bi.is_inst_implicit()) {
+                    if (!has_free_var(binding_body(e_type), 0)) {
+                        // if the rest of the type does not reference argument,
+                        // then we also stop consuming arguments
+                        break;
+                    }
                 }
+                expr imp_arg = ctx.mk_meta(ngen, some_expr(binding_domain(e_type)), g);
+                e            = mk_app(e, imp_arg, g);
+                e_type       = tc->whnf(instantiate(binding_body(e_type), imp_arg), new_cs);
             }
-            expr imp_arg = ctx.mk_meta(ngen, some_expr(binding_domain(e_type)), g);
-            e            = mk_app(e, imp_arg, g);
-            e_type       = tc->whnf(instantiate(binding_body(e_type), imp_arg), new_cs);
         }
 
         auto try_alternative = [&](expr const & e, expr const & e_type, constraint_seq fcs) {
@@ -155,33 +181,37 @@ constraint mk_calc_proof_cnstr(environment const & env, local_context const & _c
             return append(r, postponed);
         };
 
-        std::unique_ptr<exception> saved_ex;
-        try {
+        if (!get_elaborator_calc_assistant(opts)) {
             return try_alternative(e, e_type, new_cs);
-        } catch (exception & ex) {
-            saved_ex.reset(ex.clone());
-        }
+        } else {
+            std::unique_ptr<exception> saved_ex;
+            try {
+                return try_alternative(e, e_type, new_cs);
+            } catch (exception & ex) {
+                saved_ex.reset(ex.clone());
+            }
 
-        constraint_seq symm_cs = new_cs;
-        auto symm = apply_symmetry(env, ctx, ngen, tc, e, e_type, symm_cs, g);
-        if (symm) {
-            try { return try_alternative(symm->first, symm->second, symm_cs); } catch (exception &) {}
-        }
+            constraint_seq symm_cs = new_cs;
+            auto symm = apply_symmetry(env, ctx, ngen, tc, e, e_type, symm_cs, g);
+            if (symm) {
+                try { return try_alternative(symm->first, symm->second, symm_cs); } catch (exception &) {}
+            }
 
-        constraint_seq subst_cs = new_cs;
-        if (auto subst = apply_subst(env, ctx, ngen, tc, e, e_type, meta_type, subst_cs, g)) {
-            try { return try_alternative(subst->first, subst->second, subst_cs); } catch (exception&) {}
-        }
-
-        if (symm) {
-            constraint_seq subst_cs = symm_cs;
-            if (auto subst = apply_subst(env, ctx, ngen, tc, symm->first, symm->second, meta_type, subst_cs, g)) {
+            constraint_seq subst_cs = new_cs;
+            if (auto subst = apply_subst(env, ctx, ngen, tc, e, e_type, meta_type, subst_cs, g)) {
                 try { return try_alternative(subst->first, subst->second, subst_cs); } catch (exception&) {}
             }
-        }
 
-        saved_ex->rethrow();
-        lean_unreachable();
+            if (symm) {
+                constraint_seq subst_cs = symm_cs;
+                if (auto subst = apply_subst(env, ctx, ngen, tc, symm->first, symm->second, meta_type, subst_cs, g)) {
+                    try { return try_alternative(subst->first, subst->second, subst_cs); } catch (exception&) {}
+                }
+            }
+
+            saved_ex->rethrow();
+            lean_unreachable();
+        }
     };
     bool owner = false;
     return mk_choice_cnstr(m, choice_fn, to_delay_factor(cnstr_group::Epilogue), owner, j, relax);

src/frontends/lean/calc_proof_elaborator.h

@@ -16,8 +16,11 @@ namespace lean {
       - adding !
       - adding subst
 */
-constraint mk_calc_proof_cnstr(environment const & env, local_context const & ctx,
-                               expr const & m, expr const & e,
+constraint mk_calc_proof_cnstr(environment const & env, options const & opts,
+                               local_context const & ctx, expr const & m, expr const & e,
                                constraint_seq const & cs, unifier_config const & cfg,
                                info_manager * im, bool relax);
+
+void initialize_calc_proof_elaborator();
+void finalize_calc_proof_elaborator();
 }

src/frontends/lean/elaborator.cpp

@@ -310,7 +310,8 @@ expr elaborator::visit_calc_proof(expr const & e, optional<expr> const & t, cons
     pair<expr, constraint_seq> ecs = visit(get_annotation_arg(e));
     expr m                         = m_full_context.mk_meta(m_ngen, t, e.get_tag());
     register_meta(m);
-    constraint c                   = mk_calc_proof_cnstr(env(), m_context, m, ecs.first, ecs.second, m_unifier_config,
+    constraint c                   = mk_calc_proof_cnstr(env(), ios().get_options(),
+                                                         m_context, m, ecs.first, ecs.second, m_unifier_config,
                                                          im, m_relax_main_opaque);
     cs += c;
     return m;

src/frontends/lean/init_module.cpp

@@ -25,6 +25,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/token_table.h"
 #include "frontends/lean/info_tactic.h"
 #include "frontends/lean/placeholder_elaborator.h"
+#include "frontends/lean/calc_proof_elaborator.h"
 #include "frontends/lean/scanner.h"
 #include "frontends/lean/pp.h"
 #include "frontends/lean/server.h"
@@ -54,10 +55,12 @@ void initialize_frontend_lean_module() {
     initialize_info_tactic();
     initialize_pp();
     initialize_placeholder_elaborator();
+    initialize_calc_proof_elaborator();
     initialize_server();
 }
 void finalize_frontend_lean_module() {
     finalize_server();
+    finalize_calc_proof_elaborator();
     finalize_placeholder_elaborator();
     finalize_pp();
     finalize_info_tactic();

tests/lean/calc_assistant.lean

@@ -0,0 +1,26 @@
+import logic
+open eq.ops
+
+set_option elaborator.calc_assistant false
+
+theorem tst1 (a b c : num) (H₁ : ∀ x, b = x) (H₂ : c = b) : a = c :=
+calc a  = b : H₁  -- error because calc assistant is off
+    ... = c : H₂
+
+theorem tst2 (a b c : num) (H₁ : ∀ x, b = x) (H₂ : c = b) : a = c :=
+calc a  = b : !H₁⁻¹
+    ... = c : H₂   -- error because calc assistant is off
+
+theorem tst3 (a b c : num) (H₁ : ∀ x, b = x) (H₂ : c = b) : a = c :=
+calc a  = b : !H₁⁻¹
+    ... = c : H₂⁻¹
+
+theorem tst4 (a b c : num) (H₁ : ∀ x, b = x) (H₂ : c = b) : a = c :=
+calc a  = b : eq.symm (H₁ a)
+    ... = c : eq.symm H₂
+
+set_option elaborator.calc_assistant true
+
+theorem tst5 (a b c : num) (H₁ : ∀ x, b = x) (H₂ : c = b) : a = c :=
+calc a  = b : H₁
+    ... = c : H₂

tests/lean/calc_assistant.lean.expected.out

@@ -0,0 +1,13 @@
+calc_assistant.lean:7:14: error: type mismatch at term
+  H₁
+has type
+  ∀ (x : num),
+    b = x
+but is expected to have type
+  a = b
+calc_assistant.lean:12:14: error: type mismatch at term
+  H₂
+has type
+  c = b
+but is expected to have type
+  b = c