feat(library/tactic): add 'subst' tactic

library/init/meta/tactic.lean

@@ -64,6 +64,7 @@ meta_constant format_result : tactic format
 /- Return target type of the main goal. Fail if tactic_state does not have any goal left. -/
 meta_constant target        : tactic expr
 meta_constant intro         : name → tactic unit
+meta_constant intron        : nat → tactic unit
 meta_constant assumption    : tactic unit
 meta_constant rename        : name → name → tactic unit
 meta_constant clear         : name → tactic unit
@@ -98,6 +99,7 @@ meta_constant mk_app        : name → list expr → tactic expr
    returns the application
      @ite.{1} (a > b) (nat.decidable_gt a b) nat a b -/
 meta_constant mk_mapp       : name → list (option expr) → tactic expr
+meta_constant subst         : name → tactic unit
 open list nat
 
 meta_definition intros : tactic unit :=

src/library/lazy_abstraction.cpp

@@ -216,6 +216,15 @@ expr mk_lazy_abstraction(expr const & e, name const & n) {
     return mk_lazy_abstraction(e, ns);
 }
 
+expr mk_lazy_abstraction_with_locals(expr const & e, buffer<expr> const & ls) {
+    lean_assert(is_metavar(e));
+    lean_assert(std::all_of(ls.begin(), ls.end(), is_local));
+    buffer<name> ns;
+    for (expr const & l : ls)
+        ns.push_back(mlocal_name(l));
+    return mk_lazy_abstraction_core(e, ns, ls);
+}
+
 void initialize_lazy_abstraction() {
     g_lazy_abstraction_macro = new name("lazy_abstraction");
 }

src/library/lazy_abstraction.h

@@ -15,6 +15,11 @@ expr const & get_lazy_abstraction_expr(expr const & e);
 void get_lazy_abstraction_info(expr const & e, buffer<name> & ns, buffer<expr> & es);
 expr push_lazy_abstraction(expr const & e);
 
+/* Create e{ls[0] := ls[0], ..., ls[n-1] := ls[n-1]}
+   \pre is_metavar(e)
+   \pre for all x in ls, is_local(x) */
+expr mk_lazy_abstraction_with_locals(expr const & e, buffer<expr> const & ls);
+
 void initialize_lazy_abstraction();
 void finalize_lazy_abstraction();
 }

src/library/tactic/CMakeLists.txt

@@ -1,3 +1,3 @@
 add_library(tactic OBJECT tactic_state.cpp intro_tactic.cpp assumption_tactic.cpp
   revert_tactic.cpp rename_tactic.cpp clear_tactic.cpp
-  app_builder_tactics.cpp elaborate.cpp init_module.cpp)
+  app_builder_tactics.cpp subst_tactic.cpp elaborate.cpp init_module.cpp)

src/library/tactic/clear_tactic.cpp

@@ -8,12 +8,12 @@ Author: Leonardo de Moura
 #include "library/tactic/tactic_state.h"
 
 namespace lean {
-vm_obj clear(name const & n, tactic_state const & s) {
+vm_obj clear(name const & n, tactic_state const & s, bool internal_name) {
     optional<metavar_decl> g   = s.get_main_goal_decl();
     if (!g) return mk_no_goals_exception(s);
     metavar_context mctx       = s.mctx();
     local_context lctx         = g->get_context();
-    optional<local_decl> d     = lctx.get_local_decl_from_user_name(n);
+    optional<local_decl> d     = internal_name ? lctx.get_local_decl(n) : lctx.get_local_decl_from_user_name(n);
     if (!d)
         return mk_tactic_exception(sstream() << "clear tactic failed, unknown '" << n << "' hypothesis", s);
     expr l = d->mk_ref();
@@ -29,7 +29,8 @@ vm_obj clear(name const & n, tactic_state const & s) {
 }
 
 vm_obj tactic_clear(vm_obj const & n, vm_obj const & s) {
-    return clear(to_name(n), to_tactic_state(s));
+    bool internal_name = false;
+    return clear(to_name(n), to_tactic_state(s), internal_name);
 }
 
 void initialize_clear_tactic() {

src/library/tactic/clear_tactic.h

@@ -5,7 +5,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
+#include "library/tactic/tactic_state.h"
 namespace lean {
+vm_obj clear(name const & n, tactic_state const & s, bool internal_name);
+inline vm_obj clear_internal(name const & n, tactic_state const & s) { return clear(n, s, true); }
 void initialize_clear_tactic();
 void finalize_clear_tactic();
 }

src/library/tactic/init_module.cpp

@@ -11,6 +11,7 @@ Author: Leonardo de Moura
 #include "library/tactic/rename_tactic.h"
 #include "library/tactic/clear_tactic.h"
 #include "library/tactic/app_builder_tactics.h"
+#include "library/tactic/subst_tactic.h"
 #include "library/tactic/elaborate.h"
 
 namespace lean {
@@ -22,10 +23,12 @@ void initialize_tactic_module() {
     initialize_rename_tactic();
     initialize_clear_tactic();
     initialize_app_builder_tactics();
+    initialize_subst_tactic();
     initialize_elaborate();
 }
 void finalize_tactic_module() {
     finalize_elaborate();
+    finalize_subst_tactic();
     finalize_app_builder_tactics();
     finalize_clear_tactic();
     finalize_rename_tactic();

src/library/tactic/intro_tactic.cpp

@@ -7,9 +7,59 @@ Author: Leonardo de Moura
 #include "kernel/instantiate.h"
 #include "library/lazy_abstraction.h"
 #include "library/vm/vm_name.h"
+#include "library/vm/vm_nat.h"
 #include "library/tactic/tactic_state.h"
 
 namespace lean {
+optional<tactic_state> intron(unsigned n, tactic_state const & s, buffer<name> & new_Hs) {
+    if (n == 0) return some_tactic_state(s);
+    optional<metavar_decl> g = s.get_main_goal_decl();
+    if (!g) return none_tactic_state();
+    metavar_context mctx = s.mctx();
+    type_context ctx     = mk_type_context_for(s, mctx);
+    expr type            = g->get_type();
+    type_context::tmp_locals new_locals(ctx);
+    for (unsigned i = 0; i < n; i++) {
+        if (!is_pi(type) && !is_lambda(type)) {
+            type = ctx.whnf(type);
+            if (!is_pi(type))
+                return none_tactic_state();
+        }
+        lean_assert(is_pi(type) || is_lambda(type));
+        if (is_pi(type)) {
+            expr H  = new_locals.push_local(binding_name(type), binding_domain(type), binding_info(type));
+            type    = instantiate(binding_body(type), H);
+            new_Hs.push_back(mlocal_name(H));
+
+        } else {
+            expr H  = new_locals.push_let(let_name(type), let_type(type), let_value(type));
+            type    = instantiate(let_body(type), H);
+            new_Hs.push_back(mlocal_name(H));
+        }
+    }
+    local_context lctx = ctx.lctx();
+    expr new_M   = mctx.mk_metavar_decl(lctx, type);
+    expr new_val = new_locals.mk_lambda(mk_lazy_abstraction(new_M, new_Hs));
+    mctx.assign(head(s.goals()), new_val);
+    list<expr> new_gs(new_M, tail(s.goals()));
+    return some_tactic_state(set_mctx_goals(s, mctx, new_gs));
+}
+
+optional<tactic_state> intron(unsigned n, tactic_state const & s) {
+    buffer<name> tmp;
+    return intron(n, s, tmp);
+}
+
+vm_obj tactic_intron(vm_obj const & num, vm_obj const & s) {
+    optional<metavar_decl> g = to_tactic_state(s).get_main_goal_decl();
+    if (!g) return mk_no_goals_exception(to_tactic_state(s));
+    buffer<name> new_Hs;
+    if (auto new_s = intron(force_to_unsigned(num, 0), to_tactic_state(s), new_Hs))
+        return mk_tactic_success(*new_s);
+    else
+        return mk_tactic_exception("intron tactic failed, insufficient binders", to_tactic_state(s));
+}
+
 vm_obj intro(name const & n, tactic_state const & s) {
     optional<metavar_decl> g = s.get_main_goal_decl();
     if (!g) return mk_no_goals_exception(s);
@@ -50,6 +100,7 @@ vm_obj tactic_intro(vm_obj const & n, vm_obj const & s) {
 
 void initialize_intro_tactic() {
     DECLARE_VM_BUILTIN(name({"tactic", "intro"}),   tactic_intro);
+    DECLARE_VM_BUILTIN(name({"tactic", "intron"}),  tactic_intron);
 }
 
 void finalize_intro_tactic() {

src/library/tactic/intro_tactic.h

@@ -5,7 +5,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
+#include "library/tactic/tactic_state.h"
 namespace lean {
+optional<tactic_state> intron(unsigned n, tactic_state const & s, buffer<name> & new_Hs);
+optional<tactic_state> intron(unsigned n, tactic_state const & s);
 void initialize_intro_tactic();
 void finalize_intro_tactic();
 }

src/library/tactic/subst_tactic.cpp

@@ -0,0 +1,134 @@
+/*
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include <algorithm>
+#include "kernel/abstract.h"
+#include "kernel/instantiate.h"
+#include "library/util.h"
+#include "library/locals.h"
+#include "library/vm/vm.h"
+#include "library/vm/vm_name.h"
+#include "library/tactic/tactic_state.h"
+#include "library/tactic/revert_tactic.h"
+#include "library/tactic/intro_tactic.h"
+#include "library/tactic/clear_tactic.h"
+#include "library/tactic/app_builder_tactics.h"
+
+namespace lean {
+/* n is the internal name of a hypothesis that represents an equality */
+vm_obj tactic_subst_core(name const & n, bool symm, tactic_state const & s) {
+    try {
+        metavar_decl g             = *s.get_main_goal_decl();
+        local_context lctx         = g.get_context();
+        local_decl d               = *lctx.get_local_decl(n);
+        expr lhs, rhs;
+        is_eq(d.get_type(), lhs, rhs);
+        buffer<expr> to_revert;
+        if (symm)
+            std::swap(lhs, rhs);
+        to_revert.push_back(lhs);
+        to_revert.push_back(d.mk_ref());
+        tactic_state s1 = revert(to_revert, s);
+        lean_assert(to_revert.size() >= 2);
+        buffer<name> lhsH;
+        optional<tactic_state> s2 = intron(2, s1, lhsH);
+        if (!s2) return mk_tactic_exception("subst tactic failed, unexpected failure during intro", s);
+        lctx                 = s2->get_main_goal_decl()->get_context();
+        expr type            = s2->get_main_goal_decl()->get_type();
+        lhs                  = lctx.get_local_decl(lhsH[0])->mk_ref();
+        expr H               = lctx.get_local_decl(lhsH[1])->mk_ref();
+        bool depH            = depends_on(type, H);
+        expr new_type        = instantiate(abstract_local(type, lhs), rhs);
+        metavar_context mctx = s2->mctx();
+        type_context ctx     = mk_type_context_for(*s2, mctx);
+        app_builder builder  = mk_app_builder_for(ctx);
+        expr motive;
+        if (depH) {
+            new_type = instantiate(abstract_local(new_type, H), builder.mk_eq_refl(rhs));
+            if (symm) {
+                motive = ctx.mk_lambda({lhs, H}, type);
+            } else {
+                motive = mk_lambda("H", builder.mk_eq(rhs, lhs), type);
+                motive = ctx.mk_lambda(lhs, motive);
+            }
+        } else {
+            motive   = ctx.mk_lambda(lhs, type);
+        }
+        expr major   = symm ? H : builder.mk_eq_symm(H);
+        expr new_M   = mctx.mk_metavar_decl(lctx, new_type);
+        expr minor   = new_M;
+        expr new_val = depH ? builder.mk_eq_drec(motive, minor, major) : builder.mk_eq_rec(motive, minor, major);
+        mctx.assign(head(s2->goals()), new_val);
+        list<expr> new_gs(new_M, tail(s.goals()));
+        tactic_state s3 = set_mctx_goals(*s2, mctx, new_gs);
+        vm_obj o4    = clear_internal(lhsH[1], s3);
+        optional<tactic_state> s4 = is_tactic_success(o4);
+        if (!s4) return o4;
+        vm_obj o5    = clear_internal(lhsH[0], *s4);
+        optional<tactic_state> s5 = is_tactic_success(o5);
+        if (!s5) return o5;
+        optional<tactic_state> s6 = intron(to_revert.size() - 2, *s5);
+        if (!s6) return mk_tactic_exception("subst tactic failed, unexpected failure during intro", s);
+        return mk_tactic_success(*s6);
+    } catch (exception & ex) {
+        return mk_tactic_exception(ex, s);
+    }
+}
+
+vm_obj tactic_subst(name const & n, tactic_state const & s) {
+    optional<metavar_decl> g   = s.get_main_goal_decl();
+    if (!g) return mk_no_goals_exception(s);
+    local_context lctx         = g->get_context();
+    optional<local_decl> d     = lctx.get_local_decl_from_user_name(n);
+    if (!d)
+        return mk_tactic_exception(sstream() << "subst tactic failed, unknown '" << n << "' hypothesis", s);
+    expr const & type = d->get_type();
+    expr lhs, rhs;
+    if (is_eq(type, lhs, rhs)) {
+        if (is_local(rhs) && !depends_on(rhs, lhs)) {
+            return tactic_subst_core(d->get_name(), true, s);
+        } else if (is_local(lhs) && !depends_on(lhs, rhs)) {
+            return tactic_subst_core(d->get_name(), false, s);
+        } else {
+            return mk_tactic_exception(sstream() << "subst tactic failed, hypothesis '"
+                                       << n << "' is not of the form (x = t) or (t = x)", s);
+        }
+    } else {
+        bool found = false;
+        vm_obj r;
+        lctx.for_each_after(*d, [&](local_decl const & d2) {
+                if (found) return;
+                expr lhs, rhs;
+                if (is_eq(d2.get_type(), lhs, rhs)) {
+                    if (is_local(lhs) && mlocal_name(lhs) == d->get_name() && !depends_on(rhs, lhs)) {
+                        found = true;
+                        r     = tactic_subst_core(d2.get_name(), false, s);
+                    } else if (is_local(rhs) && mlocal_name(rhs) == d->get_name() && !depends_on(lhs, rhs)) {
+                        found = true;
+                        r     = tactic_subst_core(d2.get_name(), true, s);
+                    }
+                }
+            });
+        if (found) {
+            return r;
+        } else {
+            return mk_tactic_exception(sstream() << "subst tactic failed, hypothesis '"
+                                       << n << "' is not a variable nor an equation of the form (x = t) or (t = x)", s);
+        }
+    }
+}
+
+vm_obj tactic_subst(vm_obj const & n, vm_obj const & s) {
+    return tactic_subst(to_name(n), to_tactic_state(s));
+}
+
+void initialize_subst_tactic() {
+    DECLARE_VM_BUILTIN(name({"tactic", "subst"}), tactic_subst);
+}
+
+void finalize_subst_tactic() {
+}
+}

src/library/tactic/subst_tactic.h

@@ -0,0 +1,11 @@
+/*
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+namespace lean {
+void initialize_subst_tactic();
+void finalize_subst_tactic();
+}

src/library/type_context.cpp

@@ -369,6 +369,21 @@ expr type_context::mk_pi(buffer<expr> const & locals, expr const & e) {
     return mk_binding(true, locals.size(), locals.data(), e);
 }
 
+expr type_context::mk_lambda(expr const & local, expr const & e) {
+    return mk_binding(false, 1, &local, e);
+}
+
+expr type_context::mk_pi(expr const & local, expr const & e) {
+    return mk_binding(true, 1, &local, e);
+}
+
+expr type_context::mk_lambda(std::initializer_list<expr> const & locals, expr const & e) {
+    return mk_binding(false, locals.size(), locals.begin(), e);
+}
+
+expr type_context::mk_pi(std::initializer_list<expr> const & locals, expr const & e) {
+    return mk_binding(true, locals.size(), locals.begin(), e);
+}
 
 /* ---------------------
    Normalization

src/library/type_context.h

@@ -216,6 +216,10 @@ public:
 
     expr mk_lambda(buffer<expr> const & locals, expr const & e);
     expr mk_pi(buffer<expr> const & locals, expr const & e);
+    expr mk_lambda(expr const & local, expr const & e);
+    expr mk_pi(expr const & local, expr const & e);
+    expr mk_lambda(std::initializer_list<expr> const & locals, expr const & e);
+    expr mk_pi(std::initializer_list<expr> const & locals, expr const & e);
 
     /* Add a let-decl (aka local definition) to the local context */
     expr push_let(name const & ppn, expr const & type, expr const & value) {

tests/lean/run/subst_tac1.lean

@@ -0,0 +1,17 @@
+constant p : nat → Prop
+open tactic
+set_option pp.all true
+
+definition ex (a b c : nat) (H : p c) : a = b → p a → p b :=
+by do intro "H1", intro "H2",
+      subst "a",
+      trace_state,
+      assumption
+
+print ex
+
+example (a b c : nat) (H : p c) : a = b → p a → p b :=
+by do intros,
+      subst "b",
+      trace_state,
+      assumption