feat(library/init/meta/tactic): intro returns new free_var

library/init/meta/injection_tactic.lean

@@ -18,8 +18,7 @@ private meta_definition mk_intro_name : name → list name → name
 private meta_definition injection_intro : expr → list name → tactic unit
 | (pi n bi b d) ns := do
   Hname ← return (mk_intro_name n ns),
-  intro Hname,
-  H ← get_local Hname,
+  H ← intro Hname,
   Ht ← infer_type H,
   match is_eq Ht with
   | some (lhs, rhs) :=

library/init/meta/tactic.lean

@@ -77,7 +77,7 @@ meta_constant result        : tactic expr
 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 intro         : name → tactic expr
 meta_constant intron        : nat → tactic unit
 meta_constant rename        : name → name → tactic unit
 meta_constant clear         : name → tactic unit
@@ -153,17 +153,17 @@ meta_constant get_assignment : expr → tactic expr
 meta_constant mk_fresh_name : tactic name
 open list nat
 
-meta_definition intros : tactic unit :=
+meta_definition intros : tactic (list expr) :=
 do t ← target,
    match t with
-   | expr.pi   _ _ _ _ := do intro "_", intros
-   | expr.elet _ _ _ _ := do intro "_", intros
-   | _                 := skip
+   | expr.pi   _ _ _ _ := do H ← intro "_", Hs ← intros, return (H :: Hs)
+   | expr.elet _ _ _ _ := do H ← intro "_", Hs ← intros, return (H :: Hs)
+   | _                 := return []
    end
 
-meta_definition intro_lst : list name → tactic unit
-| []      := skip
-| (n::ns) := do intro n, intro_lst ns
+meta_definition intro_lst : list name → tactic (list expr)
+| []      := return []
+| (n::ns) := do H ← intro n, Hs ← intro_lst ns, return (H :: Hs)
 
 meta_definition revert (n : name) : tactic unit :=
 revert_lst [n]

src/library/tactic/intro_tactic.cpp

@@ -9,6 +9,7 @@ Author: Leonardo de Moura
 #include "library/lazy_abstraction.h"
 #include "library/vm/vm_name.h"
 #include "library/vm/vm_nat.h"
+#include "library/vm/vm_expr.h"
 #include "library/tactic/tactic_state.h"
 
 namespace lean {
@@ -94,7 +95,7 @@ vm_obj intro(name const & n, tactic_state const & s) {
         expr new_val         = mk_lambda(n1, binding_domain(type), mk_lazy_abstraction(new_M, mlocal_name(H)));
         mctx.assign(head(s.goals()), new_val);
         list<expr> new_gs(new_M, tail(s.goals()));
-        return mk_tactic_success(set_mctx_goals(s, mctx, new_gs));
+        return mk_tactic_success(to_obj(H), set_mctx_goals(s, mctx, new_gs));
     } else {
         lean_assert(is_let(type));
         name n1              = n == "_" ? let_name(type) : n;
@@ -104,7 +105,7 @@ vm_obj intro(name const & n, tactic_state const & s) {
         expr new_val         = mk_let(n1, let_type(type), let_value(type), mk_lazy_abstraction(new_M, mlocal_name(H)));
         mctx.assign(head(s.goals()), new_val);
         list<expr> new_gs(new_M, tail(s.goals()));
-        return mk_tactic_success(set_mctx_goals(s, mctx, new_gs));
+        return mk_tactic_success(to_obj(H), set_mctx_goals(s, mctx, new_gs));
     }
 }
 

tests/lean/run/nested_begin_end.lean

@@ -1,20 +1,22 @@
-exit
+open tactic
+
 example (p q : Prop) : p ∧ q ↔ q ∧ p :=
-begin
-apply iff.intro,
-  begin
-     intro H,
-     apply and.intro,
-     apply (and.elim_right H),
-     apply (and.elim_left H)
-  end,
-  begin
-    intro H,
-    apply and.intro,
-    apply (and.elim_right H),
-    apply (and.elim_left H)
-  end
-end
+by do
+  iff_intro   ← mk_const ("iff" <.> "intro"),
+  and_intro   ← mk_const ("and" <.> "intro"),
+  apply iff_intro,
+  focus (do
+    H ← intro "H",
+    apply and_intro,
+    mk_app ("and" <.> "right") [H] >>= exact,
+    mk_app ("and" <.> "left")  [H] >>= exact),
+  focus (do
+    H ← intro "H",
+    apply and_intro,
+    mk_app ("and" <.> "right") [H] >>= exact,
+    mk_app ("and" <.> "left")  [H] >>= exact)
+
+exit
 
 example (p q : Prop) : p ∧ q ↔ q ∧ p :=
 begin