refactor(library/tactic): refine interface between tactic and proof-term modes

Some constraints were being lost with the previous interface.
This is why we had a workaround in fintype.lean.

We can also remove some hacks we have used in the past.

hott/algebra/category/functor.hlean

@@ -74,7 +74,7 @@ namespace functor
         apply (apd10' c'),
         apply concat, rotate_left 1, esimp,
         exact (pi_transport_constant (eq_of_homotopy pF) H₁ c),
-        reflexivity
+        esimp
       end))))
 
   definition functor_eq {F₁ F₂ : C ⇒ D} : Π(p : to_fun_ob F₁ ∼ to_fun_ob F₂),

library/data/fintype.lean

@@ -136,13 +136,7 @@ match h₁ with
   match check_pred (λ a, ¬ p a) e with
   | tt := λ h : check_pred (λ a, ¬ p a) e = tt, inr (λ ex : (∃ x, p x),
           obtain x px, from ex,
-          begin
+          absurd px (all_of_check_pred_eq_tt h (c x)))
-            -- TODO(Leo): remove the following hack. This hack is needed to workaround a problem in
-            -- the method elaborator::elaborate_nested
-            apply absurd px,
-            apply all_of_check_pred_eq_tt h,
-            apply c x,
-          end)
   | ff := λ h : check_pred (λ a, ¬ p a) e = ff, inl (
           assert aux₁ : ∃ x, ¬¬p x, from ex_of_check_pred_eq_ff h,
           obtain x nnpx, from aux₁, exists.intro x (not_not_elim nnpx))

src/frontends/lean/elaborator.cpp

@@ -1640,13 +1640,13 @@ 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, optional<expr> const & expected_type,
-                      bool report_unassigned) {
+                      substitution const & subst, 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(), expected_type, e,
-                                                   relax, use_tactic_hints, report_unassigned);
+                                                   relax, use_tactic_hints, subst, report_unassigned);
         };
         return optional<tactic>(expr_to_tactic(env(), fn, pre_tac, pip()));
     } catch (expr_to_tactic_exception & ex) {
@@ -2067,9 +2067,9 @@ 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, optional<expr> const & expected_type,
+elaborate_result elaborator::elaborate_nested(list<expr> const & ctx, optional<expr> const & expected_type,
-                                                     expr const & n, bool relax, bool use_tactic_hints,
+                                              expr const & n, bool relax, bool use_tactic_hints,
-                                                     bool report_unassigned) {
+                                              substitution const & subst, bool report_unassigned) {
     if (infom()) {
         if (auto ps = get_info_tactic_proof_state()) {
             save_proof_state_info(*ps, n);
@@ -2089,21 +2089,24 @@ pair<expr, constraints> elaborator::elaborate_nested(list<expr> const & ctx, opt
     flet<bool> set_use_hints(m_use_tactic_hints, use_tactic_hints);
     constraint_seq cs;
     expr r  = visit(e, cs);
-    auto p  = solve(cs).pull();
+
+    buffer<constraint> tmp;
+    cs.linearize(tmp);
+    auto p  = unify(env(), tmp.size(), tmp.data(), m_ngen.mk_child(), subst, m_unifier_config).pull();
     lean_assert(p);
-    substitution s  = p->first.first;
+    substitution new_subst = p->first.first;
-    constraints rcs = p->first.second;
+    constraints rcs        = p->first.second;
-    r = s.instantiate_all(r);
+    r = new_subst.instantiate_all(r);
-    r = solve_unassigned_mvars(s, r);
+    r = solve_unassigned_mvars(new_subst, r);
-    rcs = map(rcs, [&](constraint const & c) { return instantiate_metavars(c, s); });
+    rcs = map(rcs, [&](constraint const & c) { return instantiate_metavars(c, new_subst); });
-    copy_info_to_manager(s);
+    copy_info_to_manager(new_subst);
     if (report_unassigned)
-        display_unassigned_mvars(r, s);
+        display_unassigned_mvars(r, new_subst);
     if (expected_type) {
         justification j;
-        rcs = append(rcs, cls.mk_constraints(s, j, relax));
+        rcs = append(rcs, cls.mk_constraints(new_subst, j, relax));
     }
-    return mk_pair(r, rcs);
+    return elaborate_result(r, new_subst, rcs);
 }
 
 static name * g_tmp_prefix = nullptr;

src/frontends/lean/elaborator.h

@@ -12,8 +12,9 @@ Author: Leonardo de Moura
 #include "kernel/type_checker.h"
 #include "library/expr_lt.h"
 #include "library/unifier.h"
-#include "library/tactic/tactic.h"
 #include "library/local_context.h"
+#include "library/tactic/tactic.h"
+#include "library/tactic/elaborate.h"
 #include "frontends/lean/elaborator_context.h"
 #include "frontends/lean/coercion_elaborator.h"
 #include "frontends/lean/util.h"
@@ -165,8 +166,8 @@ 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 & ctx, optional<expr> const & expected_type, expr const & e,
+    elaborate_result elaborate_nested(list<expr> const & ctx, optional<expr> const & expected_type, expr const & e,
-                                             bool relax, bool use_tactic_hints, bool report_unassigned);
+                                      bool relax, bool use_tactic_hints, substitution const &, bool report_unassigned);
 
     expr const & get_equation_fn(expr const & eq) const;
     expr visit_equations(expr const & eqns, constraint_seq & cs);

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, none_expr(), false);
+            fn(goal(), name_generator("dummy"), dummy, none_expr(), substitution(), false);
             return ps;
         });
 }

src/library/tactic/apply_tactic.cpp

@@ -234,13 +234,13 @@ tactic apply_tactic_core(elaborate_fn const & elab, expr const & e, add_meta_kin
             }
             goal const & g      = head(gs);
             name_generator ngen = s.get_ngen();
-            expr       new_e;
+            expr       new_e; substitution new_subst; constraints cs_;
+            auto ecs = elab(g, ngen.mk_child(), e, none_expr(), s.get_subst(), false);
+            std::tie(new_e, new_subst, cs_) = ecs;
             buffer<constraint> cs;
-            auto ecs = elab(g, ngen.mk_child(), e, none_expr(), false);
+            to_buffer(cs_, cs);
-            new_e    = ecs.first;
-            to_buffer(ecs.second, cs);
             to_buffer(s.get_postponed(), cs);
-            proof_state new_s(s, ngen, constraints());
+            proof_state new_s(s, new_subst, ngen, constraints());
             return apply_tactic_core(env, ios, new_s, new_e, cs, add_meta, k);
         });
 }

src/library/tactic/check_expr_tactic.cpp

@@ -21,7 +21,7 @@ tactic check_expr_tactic(elaborate_fn const & elab, expr const & e,
             }
             goal const & g      = head(gs);
             name_generator ngen = s.get_ngen();
-            expr new_e = elab(g, ngen.mk_child(), e, none_expr(), false).first;
+            expr new_e = std::get<0>(elab(g, ngen.mk_child(), e, none_expr(), s.get_subst(), false));
             auto tc = mk_type_checker(env, ngen.mk_child(), s.relax_main_opaque());
             expr new_t = tc->infer(new_e).first;
             auto out = regular(env, ios);

src/library/tactic/elaborate.cpp

@@ -44,13 +44,14 @@ optional<expr> elaborate_with_respect_to(environment const & env, io_state const
     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);
+    auto esc   = elab(head(gs), ngen.mk_child(), e, elab_expected_type, subst, report_unassigned);
-    expr new_e = ecs.first;
+    expr new_e; substitution new_subst; constraints cs_;
+    std::tie(new_e, new_subst, cs_) = esc;
     buffer<constraint> cs;
-    to_buffer(ecs.second, cs);
+    to_buffer(cs_, cs);
     if (cs.empty() && (!expected_type || enforce_type_during_elaboration)) {
         // easy case: no constraints to be solved
-        s = proof_state(s, ngen);
+        s = proof_state(s, new_subst, ngen);
         return some_expr(new_e);
     } else {
         to_buffer(s.get_postponed(), cs);
@@ -75,7 +76,7 @@ optional<expr> elaborate_with_respect_to(environment const & env, io_state const
             d_cs.second.linearize(cs);
         }
         unifier_config cfg(ios.get_options());
-        unify_result_seq rseq = unify(env, cs.size(), cs.data(), ngen.mk_child(), subst, cfg);
+        unify_result_seq rseq = unify(env, cs.size(), cs.data(), ngen.mk_child(), new_subst, cfg);
         if (auto p = rseq.pull()) {
             substitution new_subst     = p->first.first;
             constraints  new_postponed = p->first.second;

src/library/tactic/elaborate.h

@@ -17,10 +17,16 @@ bool solve_constraints(environment const & env, io_state const & ios, proof_stat
     2- name generator
     3- expression to be elaborated
     4- expected type
-    5- a flag indicating whether the elaborator should report unassigned/unsolved placeholders
+    5- substitution associated with the proof state
+    6- a flag indicating whether the elaborator should report unassigned/unsolved placeholders
+    The results are
+    1- elaborated expression
+    2- updated substitution
+    3- postponed constraints
 */
-typedef std::function<pair<expr, constraints>(goal const &, name_generator const &, expr const &,
+typedef std::tuple<expr, substitution, constraints> elaborate_result;
-                                              optional<expr> const &, bool)> elaborate_fn;
+typedef std::function<elaborate_result(goal const &, name_generator const &, expr const &,
+                                       optional<expr> const &, substitution 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

src/library/tactic/let_tactic.cpp

@@ -7,6 +7,7 @@ Author: Leonardo de Moura
 #include "kernel/abstract.h"
 #include "library/constants.h"
 #include "library/reducible.h"
+#include "library/unifier.h"
 #include "library/tactic/tactic.h"
 #include "library/tactic/elaborate.h"
 #include "library/tactic/expr_to_tactic.h"
@@ -28,10 +29,11 @@ tactic let_tactic(elaborate_fn const & elab, name const & id, expr const & e) {
             goal const & g         = head(gs);
             name_generator ngen    = s.get_ngen();
             bool report_unassigned = true;
-            auto ecs = elab(g, ngen.mk_child(), e, none_expr(), report_unassigned);
+            elaborate_result esc = elab(g, ngen.mk_child(), e, none_expr(), new_s.get_subst(), report_unassigned);
-            if (ecs.second)
+            expr new_e; substitution new_subst; constraints cs;
+            std::tie(new_e, new_subst, cs) = esc;
+            if (cs)
                 throw_tactic_exception_if_enabled(s, "invalid 'let' tactic, fail to resolve generated constraints");
-            expr new_e      = ecs.first;
             auto tc         = mk_type_checker(env, ngen.mk_child(), s.relax_main_opaque());
             expr new_e_type = tc->infer(new_e).first;
             expr new_local  = mk_local(ngen.next(), id, new_e_type, binder_info());
@@ -43,7 +45,6 @@ tactic let_tactic(elaborate_fn const & elab, name const & id, expr const & e) {
             expr new_meta_core = mk_app(new_mvar, hyps);
             expr new_meta      = mk_app(new_meta_core, new_local);
             goal new_goal(new_meta, g.get_type());
-            substitution new_subst = new_s.get_subst();
             assign(new_subst, g, mk_app(new_meta_core, new_e));
             return some_proof_state(proof_state(s, cons(new_goal, tail(gs)), new_subst, ngen));
         });

src/library/tactic/proof_state.h

@@ -40,10 +40,17 @@ public:
         proof_state(s, gs, s.m_subst, ngen) {}
     proof_state(proof_state const & s, goals const & gs):
         proof_state(s, gs, s.m_subst) {}
+    proof_state(proof_state const & s, substitution const & subst, name_generator const & ngen,
+                constraints const & postponed):
+        proof_state(s.m_goals, subst, ngen, postponed, s.relax_main_opaque(), s.report_failure()) {}
     proof_state(proof_state const & s, name_generator const & ngen, constraints const & postponed):
-        proof_state(s.m_goals, s.m_subst, ngen, postponed, s.relax_main_opaque(), s.report_failure()) {}
+        proof_state(s, s.m_goals, s.m_subst, ngen, postponed) {}
+    proof_state(proof_state const & s, substitution const & subst, name_generator const & ngen):
+        proof_state(s, s.m_goals, subst, ngen, s.m_postponed) {}
     proof_state(proof_state const & s, name_generator const & ngen):
         proof_state(s, ngen, s.m_postponed) {}
+    proof_state(proof_state const & s, substitution const & subst):
+        proof_state(s, subst, s.m_ngen) {}
 
     proof_state update_report_failure(bool f) const {
         return m_report_failure == f ? *this : proof_state(m_goals, m_subst, m_ngen, m_postponed, m_relax_main_opaque, f);

src/library/tactic/rewrite_tactic.cpp

@@ -677,11 +677,31 @@ class rewrite_fn {
         return process_reduce_step(info.get_names(), info.get_location());
     }
 
+    optional<pair<expr, constraints>> elaborate_core(expr const & e, bool fail_if_cnstrs) {
+        expr new_expr; substitution new_subst; constraints cs;
+        std::tie(new_expr, new_subst, cs) = m_elab(m_g, m_ngen.mk_child(), e, none_expr(), m_ps.get_subst(), false);
+        if (fail_if_cnstrs && cs)
+            return optional<pair<expr, constraints>>();
+        m_ps = proof_state(m_ps, new_subst);
+        return optional<pair<expr, constraints>>(new_expr, cs);
+    }
+
+    optional<expr> elaborate_if_no_cnstr(expr const & e) {
+        if (auto r = elaborate_core(e, true))
+            return some_expr(r->first);
+        else
+            return none_expr();
+    }
+
+    pair<expr, constraints> elaborate(expr const & e) {
+        return *elaborate_core(e, false);
+    }
+
     optional<expr> fold(expr const & type, expr const & e, occurrence const & occ) {
-        auto ecs       = m_elab(m_g, m_ngen.mk_child(), e, none_expr(), false);
+        auto oe = elaborate_if_no_cnstr(e);
-        expr new_e     = ecs.first;
+        if (!oe)
-        if (ecs.second)
+            return none_expr();
-            return none_expr(); // contain constraints...
+        expr new_e     = *oe;
         optional<expr> unfolded_e = unfold_app(m_env, new_e);
         if (!unfolded_e)
             return none_expr();
@@ -750,7 +770,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, none_expr(), false);
+        auto ecs       = elaborate(e);
         expr new_e     = ecs.first;
         buffer<constraint> cs;
         to_buffer(ecs.second, cs);
@@ -1074,7 +1094,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, none_expr(), false);
+            auto rcs          = elaborate(rule);
             rule              = rcs.first;
             buffer<constraint> cs;
             to_buffer(rcs.second, cs);
@@ -1376,11 +1396,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), none_expr(), false).first;
+                expr pattern     = elaborate(get_rewrite_pattern(elem)).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, none_expr(), false).first;
+                rule     = elaborate(rule).first;
                 new_elem = mk_macro(macro_def(elem), 1, &rule);
             }
             return process_rewrite_step(new_elem, elem);
@@ -1504,8 +1524,8 @@ tactic mk_simple_rewrite_tactic(buffer<expr> const & rw_elems) {
     auto fn = [=](environment const & env, io_state const & ios, proof_state const & s) {
         // dummy elaborator
         auto elab = [](goal const &, name_generator const &, expr const & H,
-                       optional<expr> const &, bool) -> pair<expr, constraints> {
+                       optional<expr> const &, substitution const & s, bool) -> elaborate_result {
-            return mk_pair(H, constraints());
+            return elaborate_result(H, s, constraints());
         };
         return rewrite_fn(env, ios, elab, s)(rw_elems);
     };