feat(frontends/lean): insert ! in calculational proofs when needed

This is part of #268

src/frontends/lean/CMakeLists.txt

@@ -8,7 +8,7 @@ theorem_queue.cpp structure_cmd.cpp info_manager.cpp no_info.cpp
 extra_info.cpp local_context.cpp choice_iterator.cpp
 placeholder_elaborator.cpp coercion_elaborator.cpp info_tactic.cpp
 proof_qed_elaborator.cpp init_module.cpp elaborator_context.cpp
-elaborator_exception.cpp)
+calc_proof_elaborator.cpp elaborator_exception.cpp)
 
 
 target_link_libraries(lean_frontend ${LEAN_LIBS})

src/frontends/lean/calc.cpp

@@ -155,6 +155,16 @@ void register_calc_cmds(cmd_table & r) {
     add_cmd(r, cmd_info("calc_trans",     "set the transitivity rule for a pair of operators, this command is relevant for the calculational proof '{...}' notation", calc_trans_cmd));
 }
 
+static expr mk_calc_annotation_core(expr const & e) { return mk_annotation(*g_calc_name, e); }
+static expr mk_calc_annotation(expr const & pr) {
+    if (is_by(pr) || is_begin_end_annotation(pr) || is_sorry(pr)) {
+        return pr;
+    } else {
+        return mk_calc_annotation_core(pr);
+    }
+}
+bool is_calc_annotation(expr const & e) { return is_annotation(e, *g_calc_name); }
+
 typedef std::tuple<name, expr, expr>  calc_pred;
 typedef pair<calc_pred, expr>         calc_step;
 inline name const & pred_op(calc_pred const & p) { return std::get<0>(p); }
@@ -198,16 +208,6 @@ static expr mk_op_fn(parser & p, name const & op, unsigned num_placeholders, pos
     return r;
 }
 
-static expr mk_calc_annotation(expr const & pr) {
-    if (is_by(pr) || is_begin_end_annotation(pr) || is_sorry(pr)) {
-        return pr;
-    } else {
-        // TODO(Leo): replace with custom annotation for calc
-        // that will influence the elaborator
-        return mk_proof_qed_annotation(pr);
-    }
-}
-
 static void parse_calc_proof(parser & p, buffer<calc_pred> const & preds, std::vector<calc_step> & steps) {
     steps.clear();
     auto pos = p.pos();
@@ -310,6 +310,7 @@ void initialize_calc() {
     g_calc_name = new name("calc");
     g_key       = new std::string("calc");
     calc_ext::initialize();
+    register_annotation(*g_calc_name);
 }
 
 void finalize_calc() {

src/frontends/lean/calc.h

@@ -10,6 +10,7 @@ namespace lean {
 class parser;
 void register_calc_cmds(cmd_table & r);
 expr parse_calc(parser & p);
+bool is_calc_annotation(expr const & e);
 void initialize_calc();
 void finalize_calc();
 }

src/frontends/lean/calc_proof_elaborator.cpp

@@ -0,0 +1,82 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "kernel/free_vars.h"
+#include "kernel/instantiate.h"
+#include "library/unifier.h"
+#include "library/reducible.h"
+#include "library/metavar_closure.h"
+#include "frontends/lean/util.h"
+#include "frontends/lean/local_context.h"
+#include "frontends/lean/info_manager.h"
+
+namespace lean {
+/** \brief Create a "choice" constraint that postpones the resolution of a calc proof step.
+
+    By delaying it, we can perform quick fixes such as:
+      - adding symmetry
+      - adding !
+      - adding subst
+*/
+constraint mk_calc_proof_cnstr(environment const & env, 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);
+    auto choice_fn = [=](expr const & meta, expr const & meta_type, substitution const & s,
+                         name_generator const & _ngen) {
+        local_context ctx = _ctx;
+        expr e            = _e;
+        name_generator ngen(_ngen);
+        type_checker_ptr tc(mk_type_checker(env, ngen.mk_child(), relax));
+        constraint_seq new_cs = cs;
+        expr e_type = tc->infer(e, new_cs);
+        e_type      = tc->whnf(e_type, new_cs);
+        tag g       = e.get_tag();
+        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);
+        }
+
+        justification new_j            = mk_type_mismatch_jst(e, e_type, meta_type);
+        if (!tc->is_def_eq(e_type, meta_type, new_j, new_cs))
+            throw unifier_exception(new_j, s);
+        buffer<constraint> cs_buffer;
+        new_cs.linearize(cs_buffer);
+        metavar_closure cls(meta);
+        cls.add(meta_type);
+        cls.mk_constraints(s, j, relax, cs_buffer);
+        cs_buffer.push_back(mk_eq_cnstr(meta, e, j, relax));
+
+        unifier_config new_cfg(cfg);
+        new_cfg.m_discard    = false;
+        unify_result_seq seq = unify(env, cs_buffer.size(), cs_buffer.data(), ngen, substitution(), new_cfg);
+        auto p = seq.pull();
+        lean_assert(p);
+        substitution new_s     = p->first.first;
+        constraints  postponed = map(p->first.second,
+                                     [&](constraint const & c) {
+                                         // we erase internal justifications
+                                         return update_justification(c, j);
+                                     });
+        if (im)
+            im->instantiate(new_s);
+        constraints r = cls.mk_constraints(new_s, j, relax);
+        return append(r, postponed);
+    };
+    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

@@ -0,0 +1,23 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "library/unifier.h"
+#include "frontends/lean/info_manager.h"
+
+namespace lean {
+/** \brief Create a "choice" constraint that postpones the resolution of a calc proof step.
+
+    By delaying it, we can perform quick fixes such as:
+      - adding symmetry
+      - adding !
+      - adding subst
+*/
+constraint mk_calc_proof_cnstr(environment const & env, local_context const & ctx,
+                               expr const & m, expr const & e,
+                               constraint_seq const & cs, unifier_config const & cfg,
+                               info_manager * im, bool relax);
+}

src/frontends/lean/elaborator.cpp

@@ -43,10 +43,12 @@ Author: Leonardo de Moura
 #include "frontends/lean/choice_iterator.h"
 #include "frontends/lean/placeholder_elaborator.h"
 #include "frontends/lean/proof_qed_elaborator.h"
+#include "frontends/lean/calc_proof_elaborator.h"
 #include "frontends/lean/info_tactic.h"
 #include "frontends/lean/pp_options.h"
 #include "frontends/lean/begin_end_ext.h"
 #include "frontends/lean/elaborator_exception.h"
+#include "frontends/lean/calc.h"
 
 namespace lean {
 /** \brief 'Choice' expressions <tt>(choice e_1 ... e_n)</tt> are mapped into a metavariable \c ?m
@@ -265,6 +267,8 @@ expr elaborator::visit_expecting_type_of(expr const & e, expr const & t, constra
         return visit_choice(e, some_expr(t), cs);
     } else if (is_by(e)) {
         return visit_by(e, some_expr(t), cs);
+    } else if (is_calc_annotation(e)) {
+        return visit_calc_proof(e, some_expr(t), cs);
     } else if (is_proof_qed_annotation(e)) {
         return visit_proof_qed(e, some_expr(t), cs);
     } else {
@@ -298,6 +302,20 @@ expr elaborator::visit_by(expr const & e, optional<expr> const & t, constraint_s
     return m;
 }
 
+expr elaborator::visit_calc_proof(expr const & e, optional<expr> const & t, constraint_seq & cs) {
+    lean_assert(is_calc_annotation(e));
+    info_manager * im = nullptr;
+    if (infom())
+        im = &m_pre_info_data;
+    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,
+                                                         im, m_relax_main_opaque);
+    cs += c;
+    return m;
+}
+
 expr elaborator::visit_proof_qed(expr const & e, optional<expr> const & t, constraint_seq & cs) {
     lean_assert(is_proof_qed_annotation(e));
     info_manager * im = nullptr;
@@ -801,6 +819,8 @@ expr elaborator::visit_core(expr const & e, constraint_seq & cs) {
         return visit_let_value(e, cs);
     } else if (is_by(e)) {
         return visit_by(e, none_expr(), cs);
+    } else if (is_calc_annotation(e)) {
+        return visit_calc_proof(e, none_expr(), cs);
     } else if (is_proof_qed_annotation(e)) {
         return visit_proof_qed(e, none_expr(), cs);
     } else if (is_no_info(e)) {

src/frontends/lean/elaborator.h

@@ -103,6 +103,7 @@ class elaborator : public coercion_info_manager {
     expr visit_choice(expr const & e, optional<expr> const & t, constraint_seq & cs);
     expr visit_by(expr const & e, optional<expr> const & t, constraint_seq & cs);
     expr visit_proof_qed(expr const & e, optional<expr> const & t, constraint_seq & cs);
+    expr visit_calc_proof(expr const & e, optional<expr> const & t, constraint_seq & cs);
     expr add_implict_args(expr e, constraint_seq & cs, bool relax);
     pair<expr, expr> ensure_fun(expr f, constraint_seq & cs);
     bool has_coercions_from(expr const & a_type);

tests/lean/run/imp_bang.lean

@@ -0,0 +1,14 @@
+import algebra.category.basic
+open eq eq.ops category functor natural_transformation
+
+variables {obC obD : Type} {C : category obC} {D : category obD} {F G H : C ⇒ D}
+
+protected definition compose2 (η : G ⟹ H) (θ : F ⟹ G) : F ⟹ H :=
+natural_transformation.mk
+  (λ a, η a ∘ θ a)
+  (λ a b f, calc
+    H f ∘ (η a ∘ θ a) = (H f ∘ η a) ∘ θ a : assoc
+                  ... = (η b ∘ G f) ∘ θ a : {naturality η f}
+                  ... = η b ∘ (G f ∘ θ a) : symm !assoc
+                  ... = η b ∘ (θ b ∘ F f) : {naturality θ f}
+                  ... = (η b ∘ θ b) ∘ F f : assoc)