feat(library/tactic/apply_tactic): improve apply_tactic

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/kernel/type_checker.cpp

@@ -491,6 +491,19 @@ bool type_checker::is_proposition(expr const & e, context const & ctx) {
 bool type_checker::is_proposition(expr const & e, context const & ctx, metavar_env const & menv) {
     return is_proposition(e, ctx, some_menv(menv));
 }
+bool type_checker::is_flex_proposition(expr e, context ctx, optional<metavar_env> const & menv) {
+    while (is_pi(e)) {
+        ctx = extend(ctx, abst_name(e), abst_domain(e));
+        e   = abst_body(e);
+    }
+    return is_proposition(e, ctx, menv);
+}
+bool type_checker::is_flex_proposition(expr const & e, context const & ctx, metavar_env const & menv) {
+    return is_flex_proposition(e, ctx, some_menv(menv));
+}
+bool type_checker::is_flex_proposition(expr const & e, context const & ctx) {
+    return is_flex_proposition(e, ctx, none_menv());
+}
 void type_checker::clear() { m_ptr->clear(); }
 normalizer & type_checker::get_normalizer() { return m_ptr->get_normalizer(); }
 expr  type_check(expr const & e, ro_environment const & env, context const & ctx) {

src/kernel/type_checker.h

@@ -77,10 +77,16 @@ public:
     /** \brief Return true iff \c t1 is convertible to \c t2 in the context \c ctx. */
     bool is_convertible(expr const & t1, expr const & t2, context const & ctx = context());
 
+    /** \brief Return true iff \c e is a proposition (i.e., it has type Bool) */
     bool is_proposition(expr const & e, context const & ctx, optional<metavar_env> const & menv);
     bool is_proposition(expr const & e, context const & ctx, metavar_env const & menv);
     bool is_proposition(expr const & e, context const & ctx = context());
 
+    /** \brief Return true iff \c e is a proposition or is a Pi s.t. the range is a flex_proposition */
+    bool is_flex_proposition(expr e, context ctx, optional<metavar_env> const & menv);
+    bool is_flex_proposition(expr const & e, context const & ctx, metavar_env const & menv);
+    bool is_flex_proposition(expr const & e, context const & ctx = context());
+
     /** \brief Reset internal caches */
     void clear();
 

src/library/tactic/apply_tactic.cpp

@@ -9,6 +9,7 @@ Author: Leonardo de Moura
 #include "kernel/environment.h"
 #include "kernel/instantiate.h"
 #include "kernel/type_checker.h"
+#include "kernel/abstract.h"
 #include "library/fo_unify.h"
 #include "library/kernel_bindings.h"
 #include "library/tactic/goal.h"
@@ -43,9 +44,11 @@ static optional<proof_state> apply_tactic(ro_environment const & env, proof_stat
     // The proof is based on an application of th.
     // There are two kinds of arguments:
     //    1) regular arguments computed using unification.
-    //    2) propostions that generate new subgoals.
+    //    2) propositions that generate new subgoals.
+    typedef std::pair<name, hypotheses> proposition_arg;
     // We use a pair to simulate this "union" type.
-    typedef list<std::pair<optional<expr>, name>> arg_list;
+    typedef list<std::pair<optional<expr>,
+                           optional<proposition_arg>>> arg_list;
     // We may solve more than one goal.
     // We store the solved goals using a list of pairs
     // name, args. Where the 'name' is the name of the solved goal.
@@ -66,21 +69,32 @@ static optional<proof_state> apply_tactic(ro_environment const & env, proof_stat
                 for (auto const & mvar : mvars) {
                     expr mvar_sol = apply(*subst, mvar);
                     if (mvar_sol != mvar) {
-                        l = cons(mk_pair(some_expr(mvar_sol), name()), l);
+                        l = cons(mk_pair(some_expr(mvar_sol), optional<proposition_arg>()), l);
                         th_type_c = instantiate(abst_body(th_type_c), mvar_sol, new_menv);
                     } else {
-                        if (checker.is_proposition(abst_domain(th_type_c), context(), new_menv)) {
+                        expr arg_type = abst_domain(th_type_c);
+                        if (checker.is_flex_proposition(arg_type, context(), new_menv)) {
                             name new_gname(gname, new_goal_idx);
                             new_goal_idx++;
-                            l = cons(mk_pair(none_expr(), new_gname), l);
+                            hypotheses hs = g.get_hypotheses();
-                            new_goals_buf.emplace_back(new_gname, update(g, abst_domain(th_type_c)));
+                            update_hypotheses_fn add_hypothesis(hs);
-                            th_type_c = instantiate(abst_body(th_type_c), mk_constant(new_gname, abst_domain(th_type_c)), new_menv);
+                            hypotheses extra_hs;
+                            while (is_pi(arg_type)) {
+                                expr d   = abst_domain(arg_type);
+                                name n   = arg_to_hypothesis_name(env, context(), abst_name(arg_type), d);
+                                n   = add_hypothesis(n, d);
+                                extra_hs.emplace_front(n, d);
+                                arg_type = instantiate(abst_body(arg_type), mk_constant(n, d), new_menv);
+                            }
+                            l = cons(mk_pair(none_expr(), some(proposition_arg(new_gname, extra_hs))), l);
+                            new_goals_buf.emplace_back(new_gname, goal(add_hypothesis.get_hypotheses(), arg_type));
+                            th_type_c = instantiate(abst_body(th_type_c), mk_constant(new_gname, arg_type), new_menv);
                         } else {
                             // we have to create a new metavar in menv
                             // since we do not have a substitution for mvar, and
                             // it is not a proposition
-                            expr new_m = new_menv->mk_metavar(context(), some_expr(abst_domain(th_type_c)));
+                            expr new_m = new_menv->mk_metavar(context(), some_expr(arg_type));
-                            l = cons(mk_pair(some_expr(new_m), name()), l);
+                            l = cons(mk_pair(some_expr(new_m), optional<proposition_arg>()), l);
                             th_type_c = instantiate(abst_body(th_type_c), 1, &new_m, new_menv);
                         }
                     }
@@ -108,8 +122,12 @@ static optional<proof_state> apply_tactic(ro_environment const & env, proof_stat
                             // TODO(Leo): decide if we instantiate the metavars in the end or not.
                             args.push_back(*arg);
                         } else {
-                            name const & subgoal_name = p2.second;
+                            proposition_arg const & parg = *(p2.second);
-                            args.push_back(find(m, subgoal_name));
+                            name const & subgoal_name = parg.first;
+                            expr pr = find(m, subgoal_name);
+                            for (auto p : parg.second)
+                                pr = Fun(p.first, p.second, pr);
+                            args.push_back(pr);
                             new_m.erase(subgoal_name);
                         }
                     }

src/library/tactic/goal.cpp

@@ -18,6 +18,33 @@ Author: Leonardo de Moura
 
 namespace lean {
 
+name mk_unique_hypothesis_name(hypotheses const & hs, name const & suggestion) {
+    name n = suggestion;
+    unsigned i = 0;
+    // TODO(Leo): investigate if this method is a performance bottleneck
+    while (true) {
+        bool ok = true;
+        for (auto const & p : hs) {
+            if (is_prefix_of(n, p.first)) {
+                ok = false;
+                break;
+            }
+        }
+        if (ok) {
+            return n;
+        } else {
+            i++;
+            n = name(suggestion, i);
+        }
+    }
+}
+
+name update_hypotheses_fn::operator()(name const & suggestion, expr const & t) {
+    name n = mk_unique_hypothesis_name(m_hypotheses, suggestion);
+    m_hypotheses.emplace_front(n, t);
+    return n;
+}
+
 goal::goal(hypotheses const & hs, expr const & c):m_hypotheses(hs), m_conclusion(c) {}
 
 format goal::pp(formatter const & fmt, options const & opts) const {
@@ -43,24 +70,7 @@ format goal::pp(formatter const & fmt, options const & opts) const {
 }
 
 name goal::mk_unique_hypothesis_name(name const & suggestion) const {
-    name n = suggestion;
+    return ::lean::mk_unique_hypothesis_name(m_hypotheses, suggestion);
-    unsigned i = 0;
-    // TODO(Leo): investigate if this method is a performance bottleneck
-    while (true) {
-        bool ok = true;
-        for (auto const & p : m_hypotheses) {
-            if (is_prefix_of(n, p.first)) {
-                ok = false;
-                break;
-            }
-        }
-        if (ok) {
-            return n;
-        } else {
-            i++;
-            n = name(suggestion, i);
-        }
-    }
 }
 
 goal_proof_fn::goal_proof_fn(std::vector<expr> && consts):

src/library/tactic/goal.h

@@ -28,6 +28,20 @@ public:
 
 typedef std::pair<name, expr> hypothesis;
 typedef list<hypothesis>      hypotheses;
+
+class update_hypotheses_fn {
+    hypotheses m_hypotheses;
+public:
+    update_hypotheses_fn(hypotheses const & hs):m_hypotheses(hs) {}
+    hypotheses const & get_hypotheses() const { return m_hypotheses; }
+    /**
+        \brief Add a new hypothesis, the name \c n is a suggestion.
+        The method checks if the given name collides with an existing name.
+        It returns the actual name used.
+    */
+    name operator()(name const & n, expr const & t);
+};
+
 class goal {
     hypotheses m_hypotheses;
     expr       m_conclusion;

src/library/tactic/proof_state.cpp

@@ -88,16 +88,19 @@ void proof_state::get_goal_names(name_set & r) const {
     }
 }
 
+name arg_to_hypothesis_name(ro_environment const & env, context const & ctx, name const & n, expr const & d) {
+    if (is_default_arrow_var_name(n) && is_proposition(d, env, ctx))
+        return name("H");
+    else
+        return n;
+}
+
 static name g_main("main");
 
 proof_state to_proof_state(ro_environment const & env, context ctx, expr t) {
     list<std::pair<name, expr>> extra_binders;
     while (is_pi(t)) {
-        name vname;
+        name vname = arg_to_hypothesis_name(env, ctx, abst_name(t), abst_domain(t));
-        if (is_default_arrow_var_name(abst_name(t)) && is_proposition(abst_domain(t), env, ctx))
-            vname = name("H");
-        else
-            vname = abst_name(t);
         extra_binders.emplace_front(vname, abst_domain(t));
         ctx = extend(ctx, vname, abst_domain(t));
         t   = abst_body(t);

src/library/tactic/proof_state.h

@@ -120,6 +120,12 @@ goals map_goals(proof_state const & s, F && f) {
 
 io_state_stream const & operator<<(io_state_stream const & out, proof_state & s);
 
+/**
+    \brief Return a name based on \c n that is suitable to be used as a hypothesis name
+    It basically renames \c n to 'H' if \c d is a proposition and \c n is the default arrow binder name.
+*/
+name arg_to_hypothesis_name(ro_environment const & env, context const & ctx, name const & n, expr const & d);
+
 UDATA_DEFS_CORE(goals)
 UDATA_DEFS(proof_state)
 void open_proof_state(lua_State * L);

tests/lean/apply_tac2.lean

@@ -0,0 +1,7 @@
+Check @Discharge
+Theorem T (a b : Bool) : a => b => b => a.
+   apply Discharge.
+   apply Discharge.
+   apply Discharge.
+   assumption.
+   done.

tests/lean/apply_tac2.lean.expected.out

@@ -0,0 +1,4 @@
+  Set: pp::colors
+  Set: pp::unicode
+@Discharge : Π (a b : Bool), (a → b) → (a ⇒ b)
+  Proved: T