feat(frontends/lean): add version of 'exact' tactic (sexact) that enforces goal type during term elaboration

hott/init/tactic.hlean

@@ -62,6 +62,8 @@ opaque definition clear      (e : expr)   : tactic := builtin
 opaque definition revert     (e : expr)   : tactic := builtin
 opaque definition unfold     (e : expr)   : tactic := builtin
 opaque definition exact      (e : expr)   : tactic := builtin
+-- rexact is similar to exact, but the goal type is enforced during elaboration
+opaque definition sexact     (e : expr)   : tactic := builtin
 opaque definition trace      (s : string) : tactic := builtin
 
 inductive expr_list : Type :=

library/init/tactic.lean

@@ -61,6 +61,8 @@ opaque definition clear      (e : expr)   : tactic := builtin
 opaque definition revert     (e : expr)   : tactic := builtin
 opaque definition unfold     (e : expr)   : tactic := builtin
 opaque definition exact      (e : expr)   : tactic := builtin
+-- rexact is similar to exact, but the goal type is enforced during elaboration
+opaque definition sexact     (e : expr)   : tactic := builtin
 opaque definition trace      (s : string) : tactic := builtin
 
 inductive expr_list : Type :=

src/frontends/lean/builtin_exprs.cpp

@@ -213,13 +213,17 @@ static expr parse_begin_end_core(parser & p, pos_info const & pos, name const &
             } else {
                 throw parser_error("invalid 'have' tactic, 'by', 'begin', 'proof', or 'from' expected", p.pos());
             }
-        } else if (p.curr_is_token(get_show_tk()) || p.curr_is_token(get_match_tk()) ||
+        } else if (p.curr_is_token(get_show_tk())) {
-                   p.curr_is_token(get_assume_tk()) || p.curr_is_token(get_take_tk()) ||
-                   p.curr_is_token(get_fun_tk())) {
             auto pos = p.pos();
             expr t = p.parse_expr();
             t      = p.mk_app(get_exact_tac_fn(), t, pos);
             add_tac(t, pos);
+        } else if (p.curr_is_token(get_match_tk()) || p.curr_is_token(get_assume_tk()) ||
+                   p.curr_is_token(get_take_tk())  || p.curr_is_token(get_fun_tk())) {
+            auto pos = p.pos();
+            expr t = p.parse_expr();
+            t      = p.mk_app(get_sexact_tac_fn(), t, pos);
+            add_tac(t, pos);
         } else {
             auto pos = p.pos();
             expr t   = p.parse_tactic();

src/frontends/lean/elaborator.cpp

@@ -1464,12 +1464,14 @@ optional<expr> elaborator::get_pre_tactic_for(expr const & mvar) {
 optional<tactic> elaborator::pre_tactic_to_tactic(expr const & pre_tac) {
     try {
         bool relax = m_relax_main_opaque;
-        auto fn = [=](goal const & g, name_generator const & ngen, expr const & e, bool report_unassigned) {
+        auto fn = [=](goal const & g, name_generator const & ngen, expr const & e, optional<expr> const & expected_type,
+                      bool report_unassigned) {
             elaborator aux_elaborator(m_ctx, ngen);
             // Disable tactic hints when processing expressions nested in tactics.
             // We must do it otherwise, it is easy to make the system loop.
             bool use_tactic_hints = false;
-            return aux_elaborator.elaborate_nested(g.to_context(), e, relax, use_tactic_hints, report_unassigned);
+            return aux_elaborator.elaborate_nested(g.to_context(), expected_type, e,
+                                                   relax, use_tactic_hints, report_unassigned);
         };
         return optional<tactic>(expr_to_tactic(env(), fn, pre_tac, pip()));
     } catch (expr_to_tactic_exception & ex) {
@@ -1870,14 +1872,18 @@ static expr translate(environment const & env, list<expr> const & ctx, expr cons
 }
 
 /** \brief Elaborate expression \c e in context \c ctx. */
-pair<expr, constraints> elaborator::elaborate_nested(list<expr> const & ctx, expr const & n,
+pair<expr, constraints> elaborator::elaborate_nested(list<expr> const & ctx, optional<expr> const & expected_type,
-                                                     bool relax, bool use_tactic_hints, bool report_unassigned) {
+                                                     expr const & n, bool relax, bool use_tactic_hints,
+                                                     bool report_unassigned) {
     if (infom()) {
         if (auto ps = get_info_tactic_proof_state()) {
             save_proof_state_info(*ps, n);
         }
     }
     expr e = translate(env(), ctx, n);
+    if (expected_type)
+        e = copy_tag(e, mk_typed_expr(mk_as_is(*expected_type), e));
+    m_context.set_ctx(ctx);
     m_context.set_ctx(ctx);
     m_full_context.set_ctx(ctx);
     flet<bool> set_relax(m_relax_main_opaque, relax);

src/frontends/lean/elaborator.h

@@ -157,7 +157,7 @@ class elaborator : public coercion_info_manager {
     void check_sort_assignments(substitution const & s);
     expr apply(substitution & s, expr const & e, name_set & univ_params, buffer<name> & new_params);
     std::tuple<expr, level_param_names> apply(substitution & s, expr const & e);
-    pair<expr, constraints> elaborate_nested(list<expr> const & g, expr const & e,
+    pair<expr, constraints> elaborate_nested(list<expr> const & ctx, optional<expr> const & expected_type, expr const & e,
                                              bool relax, bool use_tactic_hints, bool report_unassigned);
 
     expr const & get_equation_fn(expr const & eq) const;

src/frontends/lean/info_tactic.cpp

@@ -36,7 +36,7 @@ tactic mk_info_tactic(elaborate_fn const & fn, expr const & e) {
             // create dummy variable just to communicate position to the elaborator
             expr dummy = mk_sort(mk_level_zero(), e.get_tag());
             scoped_info_tactic_proof_state scope(ps);
-            fn(goal(), name_generator("dummy"), dummy, false);
+            fn(goal(), name_generator("dummy"), dummy, none_expr(), false);
             return ps;
         });
 }

src/library/constants.cpp

@@ -94,6 +94,7 @@ name const * g_tactic_now = nullptr;
 name const * g_tactic_opt_expr_list = nullptr;
 name const * g_tactic_or_else = nullptr;
 name const * g_tactic_par = nullptr;
+name const * g_tactic_sexact = nullptr;
 name const * g_tactic_state = nullptr;
 name const * g_tactic_rename = nullptr;
 name const * g_tactic_repeat = nullptr;
@@ -204,6 +205,7 @@ void initialize_constants() {
     g_tactic_opt_expr_list = new name{"tactic", "opt_expr_list"};
     g_tactic_or_else = new name{"tactic", "or_else"};
     g_tactic_par = new name{"tactic", "par"};
+    g_tactic_sexact = new name{"tactic", "sexact"};
     g_tactic_state = new name{"tactic", "state"};
     g_tactic_rename = new name{"tactic", "rename"};
     g_tactic_repeat = new name{"tactic", "repeat"};
@@ -315,6 +317,7 @@ void finalize_constants() {
     delete g_tactic_opt_expr_list;
     delete g_tactic_or_else;
     delete g_tactic_par;
+    delete g_tactic_sexact;
     delete g_tactic_state;
     delete g_tactic_rename;
     delete g_tactic_repeat;
@@ -425,6 +428,7 @@ name const & get_tactic_now_name() { return *g_tactic_now; }
 name const & get_tactic_opt_expr_list_name() { return *g_tactic_opt_expr_list; }
 name const & get_tactic_or_else_name() { return *g_tactic_or_else; }
 name const & get_tactic_par_name() { return *g_tactic_par; }
+name const & get_tactic_sexact_name() { return *g_tactic_sexact; }
 name const & get_tactic_state_name() { return *g_tactic_state; }
 name const & get_tactic_rename_name() { return *g_tactic_rename; }
 name const & get_tactic_repeat_name() { return *g_tactic_repeat; }

src/library/constants.h

@@ -96,6 +96,7 @@ name const & get_tactic_now_name();
 name const & get_tactic_opt_expr_list_name();
 name const & get_tactic_or_else_name();
 name const & get_tactic_par_name();
+name const & get_tactic_sexact_name();
 name const & get_tactic_state_name();
 name const & get_tactic_rename_name();
 name const & get_tactic_repeat_name();

src/library/constants.txt

@@ -89,6 +89,7 @@ tactic.now
 tactic.opt_expr_list
 tactic.or_else
 tactic.par
+tactic.sexact
 tactic.state
 tactic.rename
 tactic.repeat

src/library/tactic/apply_tactic.cpp

@@ -210,7 +210,7 @@ tactic apply_tactic_core(elaborate_fn const & elab, expr const & e, subgoals_act
             name_generator ngen = s.get_ngen();
             expr       new_e;
             buffer<constraint> cs;
-            auto ecs = elab(g, ngen.mk_child(), e, false);
+            auto ecs = elab(g, ngen.mk_child(), e, none_expr(), false);
             new_e    = ecs.first;
             to_buffer(ecs.second, cs);
             to_buffer(s.get_postponed(), cs);

src/library/tactic/elaborate.cpp

@@ -31,18 +31,24 @@ bool solve_constraints(environment const & env, io_state const & ios, proof_stat
 }
 
 optional<expr> elaborate_with_respect_to(environment const & env, io_state const & ios, elaborate_fn const & elab,
-                                         proof_state & s, expr const & e, optional<expr> const & expected_type,
+                                         proof_state & s, expr const & e, optional<expr> const & _expected_type,
-                                         bool report_unassigned) {
+                                         bool report_unassigned, bool enforce_type_during_elaboration) {
     name_generator ngen = s.get_ngen();
     substitution subst  = s.get_subst();
     goals const & gs    = s.get_goals();
+    optional<expr> expected_type = _expected_type;
+    if (expected_type)
+        expected_type = subst.instantiate(*expected_type);
     if (empty(gs))
         return none_expr();
-    auto ecs   = elab(head(gs), ngen.mk_child(), e, report_unassigned);
+    optional<expr> elab_expected_type;
+    if (enforce_type_during_elaboration)
+        elab_expected_type = expected_type;
+    auto ecs   = elab(head(gs), ngen.mk_child(), e, elab_expected_type, report_unassigned);
     expr new_e = ecs.first;
     buffer<constraint> cs;
     to_buffer(ecs.second, cs);
-    if (cs.empty() && !expected_type) {
+    if (cs.empty() && (!expected_type || enforce_type_during_elaboration)) {
         // easy case: no constraints to be solved
         s = proof_state(s, ngen);
         return some_expr(new_e);
@@ -51,7 +57,7 @@ optional<expr> elaborate_with_respect_to(environment const & env, io_state const
         if (expected_type) {
             auto tc      = mk_type_checker(env, ngen.mk_child());
             auto e_t_cs  = tc->infer(new_e);
-            expr t       = subst.instantiate(*expected_type);
+            expr t       = *expected_type;
             e_t_cs.second.linearize(cs);
             auto d_cs    = tc->is_def_eq(e_t_cs.first, t);
             if (!d_cs.first) {

src/library/tactic/elaborate.h

@@ -16,9 +16,11 @@ bool solve_constraints(environment const & env, io_state const & ios, proof_stat
     1- goal that will provide the context where the expression will be elaborated
     2- name generator
     3- expression to be elaborated
-    4- a flag indicating whether the elaborator should report unassigned/unsolved placeholders
+    4- expected type
+    5- a flag indicating whether the elaborator should report unassigned/unsolved placeholders
 */
-typedef std::function<pair<expr, constraints>(goal const &, name_generator const &, expr const &, bool)> elaborate_fn;
+typedef std::function<pair<expr, constraints>(goal const &, name_generator const &, expr const &,
+                                              optional<expr> const &, bool)> elaborate_fn;
 
 /** \brief Try to elaborate expression \c e using the elaboration function \c elab. The elaboration is performed
     with respect to (local context of) the first goal in \c s. The constraints generated during elaboration
@@ -31,6 +33,7 @@ typedef std::function<pair<expr, constraints>(goal const &, name_generator const
     is not modified.
 */
 optional<expr> elaborate_with_respect_to(environment const & env, io_state const & ios, elaborate_fn const & elab,
-                                         proof_state & s, expr const & e, optional<expr> const & expected_type = optional<expr>(),
+                                         proof_state & s, expr const & e,
-                                         bool report_unassigned = false);
+                                         optional<expr> const & expected_type = optional<expr>(),
+                                         bool report_unassigned = false, bool enforce_type_during_elaboration = false);
 }

src/library/tactic/exact_tactic.cpp

@@ -11,7 +11,7 @@ Author: Leonardo de Moura
 #include "library/tactic/expr_to_tactic.h"
 
 namespace lean {
-tactic exact_tactic(elaborate_fn const & elab, expr const & e) {
+tactic exact_tactic(elaborate_fn const & elab, expr const & e, bool enforce_type_during_elaboration) {
     return tactic01([=](environment const & env, io_state const & ios, proof_state const & s) {
             proof_state new_s = s;
             goals const & gs  = new_s.get_goals();
@@ -21,7 +21,8 @@ tactic exact_tactic(elaborate_fn const & elab, expr const & e) {
             }
             expr t            = head(gs).get_type();
             bool report_unassigned = false;
-            if (auto new_e = elaborate_with_respect_to(env, ios, elab, new_s, e, some_expr(t), report_unassigned)) {
+            if (auto new_e = elaborate_with_respect_to(env, ios, elab, new_s, e, some_expr(t),
+                                                       report_unassigned, enforce_type_during_elaboration)) {
                 goals const & gs   = new_s.get_goals();
                 goal const & g     = head(gs);
                 expr new_p         = g.abstract(*new_e);
@@ -35,14 +36,23 @@ tactic exact_tactic(elaborate_fn const & elab, expr const & e) {
 }
 
 static expr * g_exact_tac_fn      = nullptr;
-expr const & get_exact_tac_fn() { return *g_exact_tac_fn; }
+static expr * g_sexact_tac_fn      = nullptr;
+expr const & get_exact_tac_fn()  { return *g_exact_tac_fn; }
+expr const & get_sexact_tac_fn() { return *g_sexact_tac_fn; }
 void initialize_exact_tactic() {
     name const & exact_tac_name = get_tactic_exact_name();
+    name const & sexact_tac_name = get_tactic_sexact_name();
     g_exact_tac_fn      = new expr(Const(exact_tac_name));
+    g_sexact_tac_fn     = new expr(Const(sexact_tac_name));
     register_tac(exact_tac_name,
                  [](type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
                      check_tactic_expr(app_arg(e), "invalid 'exact' tactic, invalid argument");
-                     return exact_tactic(fn, get_tactic_expr_expr(app_arg(e)));
+                     return exact_tactic(fn, get_tactic_expr_expr(app_arg(e)), false);
+                 });
+    register_tac(sexact_tac_name,
+                 [](type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
+                     check_tactic_expr(app_arg(e), "invalid 'exact' tactic, invalid argument");
+                     return exact_tactic(fn, get_tactic_expr_expr(app_arg(e)), true);
                  });
 }
 void finalize_exact_tactic() {

src/library/tactic/exact_tactic.h

@@ -9,8 +9,8 @@ Author: Leonardo de Moura
 
 namespace lean {
 expr const & get_exact_tac_fn();
+expr const & get_sexact_tac_fn();
 /** \brief Solve first goal iff it is definitionally equal to type of \c e */
-tactic exact_tactic(expr const & e);
 void initialize_exact_tactic();
 void finalize_exact_tactic();
 }

src/library/tactic/rewrite_tactic.cpp

@@ -579,7 +579,7 @@ class rewrite_fn {
     }
 
     optional<expr> fold(expr const & type, expr const & e, occurrence const & occ) {
-        auto ecs       = m_elab(m_g, m_ngen.mk_child(), e, false);
+        auto ecs       = m_elab(m_g, m_ngen.mk_child(), e, none_expr(), false);
         expr new_e     = ecs.first;
         if (ecs.second)
             return none_expr(); // contain constraints...
@@ -651,7 +651,7 @@ class rewrite_fn {
     }
 
     optional<expr> unify_with(expr const & t, expr const & e) {
-        auto ecs       = m_elab(m_g, m_ngen.mk_child(), e, false);
+        auto ecs       = m_elab(m_g, m_ngen.mk_child(), e, none_expr(), false);
         expr new_e     = ecs.first;
         buffer<constraint> cs;
         to_buffer(ecs.second, cs);
@@ -832,7 +832,7 @@ class rewrite_fn {
     unify_result unify_target(expr const & t, expr const & orig_elem, bool is_goal) {
         try {
             expr rule         = get_rewrite_rule(orig_elem);
-            auto rcs          = m_elab(m_g, m_ngen.mk_child(), rule, false);
+            auto rcs          = m_elab(m_g, m_ngen.mk_child(), rule, none_expr(), false);
             rule              = rcs.first;
             buffer<constraint> cs;
             to_buffer(rcs.second, cs);
@@ -1096,11 +1096,11 @@ class rewrite_fn {
             expr rule = get_rewrite_rule(elem);
             expr new_elem;
             if (has_rewrite_pattern(elem)) {
-                expr pattern     = m_elab(m_g, m_ngen.mk_child(), get_rewrite_pattern(elem), false).first;
+                expr pattern     = m_elab(m_g, m_ngen.mk_child(), get_rewrite_pattern(elem), none_expr(), false).first;
                 expr new_args[2] = { rule, pattern };
                 new_elem         = mk_macro(macro_def(elem), 2, new_args);
             } else {
-                rule     = m_elab(m_g, m_ngen.mk_child(), rule, false).first;
+                rule     = m_elab(m_g, m_ngen.mk_child(), rule, none_expr(), false).first;
                 new_elem = mk_macro(macro_def(elem), 1, &rule);
             }
             return process_rewrite_step(new_elem, elem);

tests/lean/run/match_tac2.lean

@@ -0,0 +1,12 @@
+example (a b c : Prop) : a ∧ b ↔ b ∧ a :=
+begin
+  apply iff.intro,
+  {intro H,
+   match H with
+   |  and.intro H₁ H₂ := by apply and.intro; assumption
+   end},
+  {intro H,
+   match H with
+   | and.intro H₁ H₂ := by apply and.intro; assumption
+   end},
+end

tests/lean/run/match_tac3.lean

@@ -0,0 +1,13 @@
+import data.nat
+open nat
+
+theorem tst (a b : nat) (H : a = 0) : a + b = b :=
+begin
+  revert H,
+  match a with
+  | zero  := λ H, by rewrite zero_add
+  | (n+1) := λ H, nat.no_confusion H
+  end
+end
+
+print definition tst