feat(library/tactic/backward): finish backward chaining tactic

library/init/meta/tactic.lean

@@ -549,10 +549,10 @@ do max ← get_nat_option ("back_chaining" <.> "max_depth") 8,
    backward_chaining_core reducible tt max leaf_tactic extra_lemmas
 
 meta_definition back_chaining : tactic unit :=
-back_chaining_core failed []
+back_chaining_core assumption []
 
 meta_definition back_chaining_using : list expr → tactic unit :=
-back_chaining_core failed
+back_chaining_core assumption
 
 meta_definition back_chaining_using_hs : tactic unit :=
 local_context >>= back_chaining_core failed

src/library/tactic/backward/backward_chaining.cpp

@@ -5,10 +5,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "util/sexpr/option_declarations.h"
+#include "library/trace.h"
 #include "library/vm/vm_nat.h"
 #include "library/vm/vm_expr.h"
 #include "library/vm/vm_list.h"
 #include "library/tactic/tactic_state.h"
+#include "library/tactic/apply_tactic.h"
 #include "library/tactic/backward/backward_lemmas.h"
 
 #ifndef LEAN_DEFAULT_BACKWARD_CHAINING_MAX_DEPTH
@@ -22,6 +24,8 @@ unsigned get_backward_chaining_max_depth(options const & o) {
     return o.get_unsigned(*g_backward_chaining_max_depth, LEAN_DEFAULT_BACKWARD_CHAINING_MAX_DEPTH);
 }
 
+#define lean_back_trace(code) lean_trace(name({"tactic", "back_chaining"}), scope_trace_env _scope1(m_ctx.env(), m_ctx); code)
+
 struct back_chaining_fn {
     tactic_state         m_initial_state;
     type_context         m_ctx;
@@ -30,6 +34,16 @@ struct back_chaining_fn {
     vm_obj               m_leaf_tactic;
     backward_lemma_index m_lemmas;
 
+    struct choice {
+        tactic_state         m_state;
+        list<backward_lemma> m_lemmas;
+        choice(tactic_state const & s, list<backward_lemma> const & lemmas):
+            m_state(s), m_lemmas(lemmas) {}
+    };
+
+    tactic_state        m_state;
+    buffer<choice>      m_choices;
+
     back_chaining_fn(tactic_state const & s, transparency_mode md, bool use_instances,
                      unsigned max_depth, vm_obj const & leaf_tactic,
                      list<expr> const & extra_lemmas):
@@ -38,20 +52,107 @@ struct back_chaining_fn {
         m_use_instances(use_instances),
         m_max_depth(max_depth),
         m_leaf_tactic(leaf_tactic),
-        m_lemmas(backward_lemma_index(m_ctx)) {
+        m_lemmas(backward_lemma_index(m_ctx)),
+        m_state(m_initial_state) {
+        lean_assert(s.goals());
         for (expr const & extra : extra_lemmas) {
             m_lemmas.insert(m_ctx, extra);
         }
     }
 
+    bool invoke_leaf_tactic() {
+        lean_assert(m_state.goals());
+        tactic_state tmp = set_goals(m_state, to_list(head(m_state.goals())));
+        vm_obj s = to_obj(tmp);
+        vm_obj r = invoke(m_leaf_tactic, 1, &s);
+        if (optional<tactic_state> new_s = is_tactic_success(r)) {
+            m_state = set_goals(*new_s, tail(m_state.goals()));
+            return true;
+        } else {
+            return false;
+        }
+    }
+
+    bool try_lemmas(list<backward_lemma> const & lemmas) {
+        m_ctx.set_mctx(m_state.mctx());
+        list<backward_lemma> it = lemmas;
+        while (it) {
+            backward_lemma const & blemma = head(it);
+            expr lemma = blemma.to_expr(m_ctx);
+            lean_back_trace(tout() << "[" << m_choices.size() << "] trying lemma " << lemma << "\n";);
+            if (optional<tactic_state> new_state = apply(m_ctx, false, m_use_instances, lemma, m_state)) {
+                lean_back_trace(tout() << "succeed\n";);
+                if (tail(it)) {
+                    m_choices.emplace_back(m_state, tail(it));
+                }
+                m_state = *new_state;
+                return true;
+            }
+            it = tail(it);
+        }
+        return false;
+    }
+
+    bool backtrack() {
+        while (!m_choices.empty()) {
+            lean_back_trace(tout() << "[" << m_choices.size() << "] backtracking\n";);
+            list<backward_lemma> lemmas = m_choices.back().m_lemmas;
+            m_state = m_choices.back().m_state;
+            m_choices.pop_back();
+            if (try_lemmas(lemmas)) {
+                return true;
+            }
+        }
+        return false;
+    }
+
+    bool run() {
+        while (true) {
+          loop_entry:
+            lean_back_trace(tout() << "current state:\n" << m_state.pp() << "\n";);
+            if (!m_state.goals())
+                return true;
+            if (m_choices.size() >= m_max_depth) {
+                lean_back_trace(tout() << "maximum depth reached\n" << m_state.pp() << "\n";);
+                if (!backtrack())
+                    return false;
+                goto loop_entry;
+            }
+            metavar_decl g = *m_state.get_main_goal_decl();
+            expr target    = m_ctx.whnf(g.get_type());
+            list<backward_lemma> lemmas = m_lemmas.find(head_index(target));
+            if (!lemmas) {
+                if (!invoke_leaf_tactic()) {
+                    if (!backtrack())
+                        return false;
+                    goto loop_entry;
+                }
+            } else {
+                if (!try_lemmas(lemmas)) {
+                    if (!backtrack())
+                        return false;
+                    goto loop_entry;
+                }
+            }
+        }
+    }
+
     vm_obj operator()() {
-        // TODO(Leo):
-        return mk_tactic_exception("back_chaining entry point", m_initial_state);
+        list<expr> goals = m_initial_state.goals();
+        m_state = set_goals(m_initial_state, to_list(head(goals)));
+        if (run()) {
+            tactic_state final_state = set_goals(m_state, tail(goals));
+            return mk_tactic_success(final_state);
+        } else {
+            return mk_tactic_exception("back_chaining failed, use command 'set_option trace.back_chaining true' to obtain more details", m_initial_state);
+        }
     }
 };
 
 vm_obj back_chaining(transparency_mode md, bool use_instances, unsigned max_depth,
                      vm_obj const & leaf_tactic, list<expr> const & extra_lemmas, tactic_state const & s) {
+    optional<metavar_decl> g = s.get_main_goal_decl();
+    if (!g) return mk_no_goals_exception(s);
     return back_chaining_fn(s, md, use_instances, max_depth, leaf_tactic, extra_lemmas)();
 }
 

src/library/tactic/gexpr.cpp

@@ -7,13 +7,13 @@ Author: Leonardo de Moura
 #include "library/tactic/gexpr.h"
 
 namespace lean {
-expr gexpr::to_expr(environment const & env, metavar_context & mctx) const {
+expr gexpr::to_expr(type_context & ctx) const {
     if (m_univ_poly) {
-        declaration const & fdecl = env.get(const_name(m_expr));
+        declaration const & fdecl = ctx.env().get(const_name(m_expr));
         buffer<level> ls_buffer;
         unsigned num_univ_ps = fdecl.get_num_univ_params();
         for (unsigned i = 0; i < num_univ_ps; i++)
-            ls_buffer.push_back(mctx.mk_univ_metavar_decl());
+            ls_buffer.push_back(ctx.mk_univ_metavar_decl());
         levels ls = to_list(ls_buffer.begin(), ls_buffer.end());
         return mk_constant(const_name(m_expr), ls);
     } else {

src/library/tactic/gexpr.h

@@ -6,7 +6,7 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include "kernel/expr.h"
-#include "library/metavar_context.h"
+#include "library/type_context.h"
 #include "library/io_state_stream.h"
 
 namespace lean {
@@ -33,7 +33,7 @@ public:
     /** \brief Convert generalized expression into a regular expression.
         If it is universe polymorphic, we accomplish that by creating
         meta-variables using \c mctx. */
-    expr to_expr(environment const & env, metavar_context & mctx) const;
+    expr to_expr(type_context & ctx) const;
 
     /** \brief Return "bare" expression (without adding fresh metavariables if universe polymorphic) */
     expr to_bare_expr() const { return m_expr; }

src/library/type_context.h

@@ -205,6 +205,7 @@ public:
     local_context const & lctx() const { return m_lctx; }
     metavar_context const & mctx() const { return m_mctx; }
     expr mk_metavar_decl(local_context const & ctx, expr const & type) { return m_mctx.mk_metavar_decl(ctx, type); }
+    level mk_univ_metavar_decl() { return m_mctx.mk_univ_metavar_decl(); }
 
     metavar_context const & get_mctx() const { return m_mctx; }
     /* note: mctx must be a descendent of m_mctx */

tests/lean/run/back_chaining1.lean

@@ -1,6 +1,4 @@
-exit
 -- Backward chaining with tagged rules
-set_option blast.strategy "backward"
 constants {P Q R S T U : Prop} (Hpq : P → Q) (Hqr : Q → R) (Hrs : R → S) (Hst : S → T)
 constants (Huq : U → Q) (Hur : U → R) (Hus : U → S) (Hut : U → T)
 attribute Hpq [intro]
@@ -13,7 +11,9 @@ attribute Hur [intro]
 attribute Hus [intro]
 attribute Hut [intro]
 
-definition lemma1 (p : P) : Q := by blast
-definition lemma2 (p : P) : R := by blast
-definition lemma3 (p : P) : S := by blast
-definition lemma4 (p : P) : T := by blast
+open tactic
+
+definition lemma1 (p : P) : Q := by back_chaining
+definition lemma2 (p : P) : R := by back_chaining
+definition lemma3 (p : P) : S := by back_chaining
+definition lemma4 (p : P) : T := by back_chaining

tests/lean/run/back_chaining2.lean

@@ -1,6 +1,4 @@
-exit
 -- Backward chaining with hypotheses
-set_option blast.strategy "backward"
 constants {P Q R S T U : Prop}
 constants (Huq : U → Q) (Hur : U → R) (Hus : U → S) (Hut : U → T)
 attribute Huq [intro]
@@ -8,7 +6,9 @@ attribute Hur [intro]
 attribute Hus [intro]
 attribute Hut [intro]
 
-definition lemma1 : (P → Q) → P → Q := by blast
-definition lemma2 : (P → Q) → (Q → R) → P → R := by blast
-definition lemma3 : (P → Q) → (Q → R) → (R → S) → P → S := by blast
-definition lemma4 : (P → Q) → (Q → R) → (R → S) → (S → T) → P → T := by blast
+open tactic
+
+definition lemma1 : (P → Q) → P → Q := by intros >> back_chaining_using_hs
+definition lemma2 : (P → Q) → (Q → R) → P → R := by intros >> back_chaining_using_hs
+definition lemma3 : (P → Q) → (Q → R) → (R → S) → P → S := by intros >> back_chaining_using_hs
+definition lemma4 : (P → Q) → (Q → R) → (R → S) → (S → T) → P → T := by intros >> back_chaining_using_hs

tests/lean/run/back_chaining3.lean

@@ -0,0 +1,22 @@
+namespace ex
+open tactic
+
+constant typ : Type₁
+
+constant subtype : typ → typ → Prop
+
+constant subtype_refl : ∀ T, subtype T T
+
+constant subtype_trans : ∀ S T U, subtype S T → subtype T U → subtype S U
+
+attribute subtype_refl subtype_trans [intro]
+
+lemma L1 : ∀ T1 T2 T3 T4, subtype T1 T2 → subtype T2 T3 → subtype T3 T4 → subtype T1 T4 :=
+by intros >> back_chaining_using_hs
+
+set_option back_chaining.max_depth 10
+
+lemma L2 : ∀ T1 T2 T3 T4 T5 T6 (H1 :subtype T1 T2) (H2 : subtype T2 T3) (H3 : subtype T3 T4) (H3 : subtype T4 T5) (H4 : subtype T5 T6), subtype T1 T6 :=
+by intros >> back_chaining_using_hs
+
+end ex

tests/lean/run/blast21.lean

@@ -1,22 +0,0 @@
-exit
-
-namespace ex
-set_option blast.strategy "backward"
-
-constant typ : Type₁
-
-constant subtype : typ → typ → Prop
-
-constant subtype_refl : ∀ T, subtype T T
-
-constant subtype_trans : ∀ S T U, subtype S T → subtype T U → subtype S U
-
-attribute subtype_refl subtype_trans [intro]
-
-lemma L1 : ∀ T1 T2 T3 T4 T5 T6, subtype T1 T2 → subtype T2 T3 → subtype T3 T4 → subtype T4 T5 → subtype T5 T6 → subtype T1 T6 :=
-by blast
-
-reveal L1
-print L1
-
-end ex