feat(frontends/lean): improve 'begin...end' blocks

2016-09-27 13:30:17 -07:00 · 2016-09-27 13:30:17 -07:00 · c6ec659bf5
commit c6ec659bf5
parent 6207dd0346
13 changed files with 435 additions and 30 deletions
--- a/library/init/meta/interactive.lean
+++ b/library/init/meta/interactive.lean
@ -4,26 +4,172 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.meta.tactic
+import init.meta.tactic init.meta.rewrite_tactic

 namespace tactic
 namespace interactive
+namespace types
+/- The parser treats constants in the tactic.interactice namespace specially.
+   The following argument types have special parser support when interactive tactics
+   are used inside `begin ... end` blocks.

-meta def intro (h : name) : tactic unit :=
-tactic.intro h >> skip
+   - ident : make sure the next token is an identifier, and
+             produce the quoted name `t, where t is the next identifier.

-meta def apply (q : pexpr) : tactic unit :=
+   - opt_ident : parse (identifier)?
+
+   - using_ident
+
+   - raw_ident_list : parse identifier* and produce a list of quoted identifiers.
+
+         Example:
+           a b c
+         produces
+           [`a, `b, `c]
+
+   - with_ident_list : parse
+                 (`with` identifier+)?
+                 and produce a list of quoted identifiers
+   - comma_tk : parse the token `,` and produce the unit ()
+
+   - location : parse
+             (`at` identifier+)?
+             and produce a list of quoted identifiers
+
+   - qexpr : parse an expression e and produce the quoted expression `e
+
+   - qexpr_list : parse
+           `[` (expr (`,` expr)*)? `]`
+
+            and produce a list of quoted expressions.
+
+   - qexpr0 : parse an expression e using 0 as the right-binding-power,
+              and produce the quoted expression `e
+
+   - qexpr_list_or_qexpr0 : parse
+           `[` (expr (`,` expr)*)? `]`
+            or
+            expr
+
+            and produce a list of quoted expressions
+
+  - itactic: parse a nested "interactive" tactic -/
+def ident : Type := name
+def opt_ident : Type := option ident
+def using_ident : Type := option ident
+def raw_ident_list : Type := list ident
+def with_ident_list : Type := list ident
+def location : Type := list ident
+@[reducible] meta def qexpr : Type := pexpr
+@[reducible] meta def qexpr0 : Type := pexpr
+meta def qexpr_list : Type := list qexpr
+meta def qexpr_list_or_qexpr0 : Type := list qexpr
+meta def itactic : Type := tactic unit
+end types
+
+open types expr
+
+meta def intro : opt_ident → tactic unit
+| none     := intro1 >> skip
+| (some h) := tactic.intro h >> skip
+
+meta def intros : raw_ident_list → tactic unit
+| [] := tactic.intros >> skip
+| hs := intro_lst hs >> skip
+
+meta def apply (q : qexpr0) : tactic unit :=
 to_expr q >>= tactic.apply

-meta def refine : pexpr → tactic unit :=
+meta def refine : qexpr0 → tactic unit :=
 tactic.refine

 meta def assumption : tactic unit :=
 tactic.assumption

-meta def exact (e : pexpr) : tactic unit :=
+meta def change (q : qexpr0) : tactic unit :=
+to_expr_strict q >>= tactic.change
+
+meta def exact (q : qexpr0) : tactic unit :=
 do tgt : expr ← target,
-   to_expr_strict `((%%e : %%tgt)) >>= exact
+   to_expr_strict `((%%q : %%tgt)) >>= tactic.exact
+
+private meta def get_locals : list name → tactic (list expr)
+| []      := return []
+| (n::ns) := do h ← get_local n, hs ← get_locals ns, return (h::hs)
+
+meta def revert (ids : raw_ident_list) : tactic unit :=
+do hs ← get_locals ids, revert_lst hs, skip
+
+/- Return (some a) iff p is of the form (- a) -/
+private meta def is_neg (p : pexpr) : option pexpr :=
+/- Remark: we use the low-level to_raw_expr and of_raw_expr to be able to
+   pattern match pre-terms. This is a low-level trick (aka hack). -/
+match pexpr.to_raw_expr p with
+| (app (const c []) arg) := if c = `neg then some (pexpr.of_raw_expr arg) else none
+| _                      := none
+end
+
+private meta def to_symm_expr_list : list pexpr → tactic (list (bool × expr))
+| []      := return []
+| (p::ps) :=
+  match is_neg p with
+  | some a :=  do r ← to_expr a, rs ← to_symm_expr_list ps, return ((tt, r) :: rs)
+  | none   :=  do r ← to_expr p, rs ← to_symm_expr_list ps, return ((ff, r) :: rs)
+  end
+
+private meta def rw_goal : list (bool × expr) → tactic unit
+| []              := return ()
+| ((symm, e)::es) := rewrite_core reducible tt occurrences.all symm e >> rw_goal es
+
+private meta def rw_hyp : list (bool × expr) → name → tactic unit
+| []              hname := return ()
+| ((symm, e)::es) hname :=
+  do h ← get_local hname,
+     rewrite_at_core reducible tt occurrences.all symm e h,
+     rw_hyp es hname
+
+private meta def rw_hyps : list (bool × expr) → list name → tactic unit
+| es  []      := return ()
+| es  (h::hs) := rw_hyp es h >> rw_hyps es hs
+
+meta def rewrite (hs : qexpr_list_or_qexpr0) (loc : location) : tactic unit :=
+do hlist ← to_symm_expr_list hs,
+   match loc with
+   | [] := rw_goal hlist >> try reflexivity
+   | hs := rw_hyps hlist hs >> try reflexivity
+   end
+
+meta def rw : qexpr_list_or_qexpr0 → location → tactic unit :=
+rewrite
+
+private meta def get_type_name (e : expr) : tactic name :=
+do e_type ← infer_type e >>= whnf,
+   (const I ls) ← return $ get_app_fn e_type | failed,
+   return I
+
+meta def induction (p : qexpr0) (rec_name : using_ident) (ids : with_ident_list) : tactic unit :=
+do e ← to_expr p,
+   match rec_name with
+   | some n := induction_core semireducible e n ids
+   | none   := do I ← get_type_name e, induction_core semireducible e (I <.> "rec") ids
+   end
+
+meta def cases (p : qexpr0) (ids : with_ident_list) : tactic unit :=
+do e ← to_expr p,
+   cases_core semireducible e ids
+
+meta def generalize (p : qexpr) (x : ident) : tactic unit :=
+do e ← to_expr p,
+   tactic.generalize e x
+
+meta def trivial : tactic unit :=
+tactic.triv <|> tactic.reflexivity <|> tactic.contradiction
+
+meta def contradiction : tactic unit :=
+tactic.contradiction
+
+meta def repeat : itactic → tactic unit :=
+tactic.repeat

 end interactive
 end tactic
--- a/library/init/meta/pexpr.lean
+++ b/library/init/meta/pexpr.lean
@ -9,8 +9,12 @@ universe variables u

 /- Quoted expressions. They can be converted into expressions by using a tactic. -/
 meta constant pexpr : Type
-protected meta constant pexpr.of_expr : expr → pexpr
-protected meta constant pexpr.subst   : pexpr → pexpr → pexpr
+protected meta constant pexpr.of_expr  : expr → pexpr
+protected meta constant pexpr.subst    : pexpr → pexpr → pexpr
+
+/- Low level primitives for accessing internal representation. -/
+protected meta constant pexpr.to_raw_expr : pexpr → expr
+protected meta constant pexpr.of_raw_expr : expr → pexpr

 meta constant pexpr.to_string : pexpr → string
 meta instance : has_to_string pexpr :=
--- a/src/emacs/lean-syntax.el
+++ b/src/emacs/lean-syntax.el
@ -16,7 +16,7 @@
    "alias" "help" "precedence" "reserve" "declare_trace" "add_key_equivalence"
    "match" "infix" "infixl" "infixr" "notation" "postfix" "prefix" "instance"
    "eval" "vm_eval" "check" "end" "reveal" "this" "suppose"
-    "using_well_founded" "namespace" "section" "fields"
+    "using" "using_well_founded" "namespace" "section" "fields"
    "attribute" "local" "set_option" "extends" "include" "omit" "classes" "class"
    "instances" "coercions" "attributes" "raw" "replacing"
    "calc" "have" "show" "suffices" "by" "in" "at" "do" "let" "forall" "Pi" "fun"
--- a/src/frontends/lean/begin_end_block.cpp
+++ b/src/frontends/lean/begin_end_block.cpp
@ -68,32 +68,141 @@ static optional<name> is_tactic_interactive(parser & p) {
        return optional<name>();
 }

-static expr parse_auto_quoted_expr(parser & p, unsigned rbp) {
+static expr mk_lean_list(buffer<expr> const & es) {
+    expr r = mk_constant(get_list_nil_name());
+    unsigned i = es.size();
+    while (i > 0) {
+        --i;
+        r = mk_app(mk_constant(get_list_cons_name()), es[i], r);
+    }
+    return r;
+}
+
+static expr mk_lean_none() {
+    return mk_constant(get_option_none_name());
+}
+
+static expr mk_lean_some(expr const & e) {
+    return mk_app(mk_constant(get_option_some_name()), e);
+}
+
+static expr parse_quoted_ident(parser & p, name const & decl_name) {
+    if (!p.curr_is_identifier())
+        throw parser_error(sstream() << "invalid tactic '" << decl_name  << "', identifier expected", p.pos());
+    auto pos = p.pos();
+    name id  = p.get_name_val();
+    p.next();
+    return p.save_pos(quote_name(id), pos);
+}
+
+static expr parse_optional_quoted_ident(parser & p, name const & decl_name) {
+    auto pos = p.pos();
+    if (p.curr_is_identifier())
+        return p.save_pos(mk_lean_some(parse_quoted_ident(p, decl_name)), pos);
+    else
+        return p.save_pos(mk_lean_none(), pos);
+}
+
+
+static expr parse_using_id(parser & p, name const & decl_name) {
+    auto pos = p.pos();
+    if (p.curr_is_token(get_using_tk())) {
+        p.next();
+        return p.save_pos(mk_lean_some(parse_quoted_ident(p, decl_name)), pos);
+    } else {
+        return p.save_pos(mk_lean_none(), pos);
+    }
+}
+
+static expr parse_qexpr(parser & p, unsigned rbp) {
    auto pos = p.pos();
    parser::quote_scope scope(p, true);
    expr e = p.parse_expr(rbp);
    return p.save_pos(mk_quote(e), pos);
 }

+static expr parse_qexpr_list(parser & p) {
+    buffer<expr> result;
+    auto pos = p.pos();
+    p.check_token_next(get_lbracket_tk(), "invalid tactic argument, '[' expected");
+    while (!p.curr_is_token(get_rbracket_tk())) {
+        result.push_back(parse_qexpr(p, 0));
+        if (!p.curr_is_token(get_comma_tk())) break;
+        p.next();
+    }
+    p.check_token_next(get_rbracket_tk(), "invalid tactic argument, ']' expected");
+    return p.rec_save_pos(mk_lean_list(result), pos);
+}
+
+static expr parse_qexpr_list_or_qexpr0(parser & p) {
+    if (p.curr_is_token(get_lbracket_tk())) {
+        return parse_qexpr_list(p);
+    } else {
+        auto pos = p.pos();
+        buffer<expr> args;
+        args.push_back(parse_qexpr(p, 0));
+        return p.rec_save_pos(mk_lean_list(args), pos);
+    }
+}
+
+static expr parse_raw_id_list(parser & p) {
+    auto pos = p.pos();
+    buffer<expr> result;
+    while (p.curr_is_identifier()) {
+        auto id_pos = p.pos();
+        name id = p.get_name_val();
+        p.next();
+        result.push_back(p.save_pos(quote_name(id), id_pos));
+    }
+    return p.rec_save_pos(mk_lean_list(result), pos);
+}
+
+static expr parse_with_id_list(parser & p) {
+    if (p.curr_is_token(get_with_tk())) {
+        p.next();
+        return parse_raw_id_list(p);
+    } else {
+        return p.save_pos(mk_constant(get_list_nil_name()), p.pos());
+    }
+}
+
+static expr parse_location(parser & p) {
+    if (p.curr_is_token(get_at_tk())) {
+        p.next();
+        return parse_raw_id_list(p);
+    } else {
+        return p.save_pos(mk_constant(get_list_nil_name()), p.pos());
+    }
+}
+
 static expr parse_tactic_interactive(parser & p, name const & decl_name) {
    auto pos = p.pos();
    p.next();
    expr type = p.env().get(decl_name).get_type();
-    unsigned arity = get_arity(type);
    buffer<expr> args;
    while (is_pi(type)) {
        if (is_explicit(binding_info(type))) {
            expr arg_type = binding_domain(type);
-            if (is_constant(arg_type, get_pexpr_name())) {
-                /* auto quote expressions */
-                expr arg = parse_auto_quoted_expr(p, arity == 1 ? 0 : get_max_prec());
-                args.push_back(arg);
-            } else if (is_constant(arg_type, get_name_name())) {
-                if (!p.curr_is_identifier())
-                    throw parser_error(sstream() << "invalid tactic '" << decl_name  << "', identifier expected", p.pos());
-                name id = p.get_name_val();
-                p.next();
-                args.push_back(quote_name(id));
+            if (is_constant(arg_type, get_tactic_interactive_types_qexpr_name())) {
+                args.push_back(parse_qexpr(p, get_max_prec()));
+            } else if (is_constant(arg_type, get_tactic_interactive_types_qexpr0_name())) {
+                args.push_back(parse_qexpr(p, 0));
+            } else if (is_constant(arg_type, get_tactic_interactive_types_qexpr_list_name())) {
+                args.push_back(parse_qexpr_list(p));
+            } else if (is_constant(arg_type, get_tactic_interactive_types_qexpr_list_or_qexpr0_name())) {
+                args.push_back(parse_qexpr_list_or_qexpr0(p));
+            } else if (is_constant(arg_type, get_tactic_interactive_types_ident_name())) {
+                args.push_back(parse_quoted_ident(p, decl_name));
+            } else if (is_constant(arg_type, get_tactic_interactive_types_opt_ident_name())) {
+                args.push_back(parse_optional_quoted_ident(p, decl_name));
+            } else if (is_constant(arg_type, get_tactic_interactive_types_raw_ident_list_name())) {
+                args.push_back(parse_raw_id_list(p));
+            } else if (is_constant(arg_type, get_tactic_interactive_types_with_ident_list_name())) {
+                args.push_back(parse_with_id_list(p));
+            } else if (is_constant(arg_type, get_tactic_interactive_types_using_ident_name())) {
+                args.push_back(parse_using_id(p, decl_name));
+            } else if (is_constant(arg_type, get_tactic_interactive_types_location_name())) {
+                args.push_back(parse_location(p));
            } else {
                args.push_back(p.parse_expr(get_max_prec()));
            }
--- a/src/frontends/lean/token_table.cpp
+++ b/src/frontends/lean/token_table.cpp
@ -89,7 +89,7 @@ void init_token_table(token_table & t) {
         {"⊢", 0}, {"⟨", g_max_prec}, {"⟩", 0}, {"^", 0}, {"↑", 0}, {"▸", 0},
         {"//", 0}, {"|", 0}, {"!", g_max_prec}, {"?", 0},  {"with", 0}, {"...", 0}, {",", 0},
         {".", 0}, {":", 0}, {"::", 0}, {"calc", 0}, {"as", 0}, {":=", 0}, {"--", 0}, {"#", 0},
-         {"(*", 0}, {"/-", 0}, {"begin", g_max_prec}, {"abstract", g_max_prec},
+         {"(*", 0}, {"/-", 0}, {"begin", g_max_prec}, {"abstract", g_max_prec}, {"using", 0},
         {"@@", g_max_prec}, {"@", g_max_prec},
         {"sorry", g_max_prec}, {"+", g_plus_prec}, {"->", g_arrow_prec}, {"<-", 0},
         {"?(", g_max_prec}, {"⌞", g_max_prec}, {"⌟", 0}, {"match", 0},
--- a/src/frontends/lean/tokens.cpp
+++ b/src/frontends/lean/tokens.cpp
@ -39,6 +39,7 @@ static name const * g_turnstile_tk = nullptr;
 static name const * g_membership_tk = nullptr;
 static name const * g_explicit_tk = nullptr;
 static name const * g_partial_explicit_tk = nullptr;
+static name const * g_at_tk = nullptr;
 static name const * g_max_tk = nullptr;
 static name const * g_imax_tk = nullptr;
 static name const * g_import_tk = nullptr;
@ -117,6 +118,7 @@ static name const * g_this_tk = nullptr;
 static name const * g_noncomputable_tk = nullptr;
 static name const * g_theory_tk = nullptr;
 static name const * g_key_equivalences_tk = nullptr;
+static name const * g_using_tk = nullptr;
 static name const * g_using_well_founded_tk = nullptr;
 void initialize_tokens() {
    g_aliases_tk = new name{"aliases"};
@ -155,6 +157,7 @@ void initialize_tokens() {
    g_membership_tk = new name{"∈"};
    g_explicit_tk = new name{"@"};
    g_partial_explicit_tk = new name{"@@"};
+    g_at_tk = new name{"at"};
    g_max_tk = new name{"max"};
    g_imax_tk = new name{"imax"};
    g_import_tk = new name{"import"};
@ -233,6 +236,7 @@ void initialize_tokens() {
    g_noncomputable_tk = new name{"noncomputable"};
    g_theory_tk = new name{"theory"};
    g_key_equivalences_tk = new name{"key_equivalences"};
+    g_using_tk = new name{"using"};
    g_using_well_founded_tk = new name{"using_well_founded"};
 }
 void finalize_tokens() {
@ -272,6 +276,7 @@ void finalize_tokens() {
    delete g_membership_tk;
    delete g_explicit_tk;
    delete g_partial_explicit_tk;
+    delete g_at_tk;
    delete g_max_tk;
    delete g_imax_tk;
    delete g_import_tk;
@ -350,6 +355,7 @@ void finalize_tokens() {
    delete g_noncomputable_tk;
    delete g_theory_tk;
    delete g_key_equivalences_tk;
+    delete g_using_tk;
    delete g_using_well_founded_tk;
 }
 name const & get_aliases_tk() { return *g_aliases_tk; }
@ -388,6 +394,7 @@ name const & get_turnstile_tk() { return *g_turnstile_tk; }
 name const & get_membership_tk() { return *g_membership_tk; }
 name const & get_explicit_tk() { return *g_explicit_tk; }
 name const & get_partial_explicit_tk() { return *g_partial_explicit_tk; }
+name const & get_at_tk() { return *g_at_tk; }
 name const & get_max_tk() { return *g_max_tk; }
 name const & get_imax_tk() { return *g_imax_tk; }
 name const & get_import_tk() { return *g_import_tk; }
@ -466,5 +473,6 @@ name const & get_this_tk() { return *g_this_tk; }
 name const & get_noncomputable_tk() { return *g_noncomputable_tk; }
 name const & get_theory_tk() { return *g_theory_tk; }
 name const & get_key_equivalences_tk() { return *g_key_equivalences_tk; }
+name const & get_using_tk() { return *g_using_tk; }
 name const & get_using_well_founded_tk() { return *g_using_well_founded_tk; }
 }
--- a/src/frontends/lean/tokens.h
+++ b/src/frontends/lean/tokens.h
@ -41,6 +41,7 @@ name const & get_turnstile_tk();
 name const & get_membership_tk();
 name const & get_explicit_tk();
 name const & get_partial_explicit_tk();
+name const & get_at_tk();
 name const & get_max_tk();
 name const & get_imax_tk();
 name const & get_import_tk();
@ -119,5 +120,6 @@ name const & get_this_tk();
 name const & get_noncomputable_tk();
 name const & get_theory_tk();
 name const & get_key_equivalences_tk();
+name const & get_using_tk();
 name const & get_using_well_founded_tk();
 }
--- a/src/frontends/lean/tokens.txt
+++ b/src/frontends/lean/tokens.txt
@ -34,6 +34,7 @@ turnstile    ⊢
 membership   ∈
 explicit     @
 partial_explicit @@
+at           at
 max          max
 imax         imax
 import       import
@ -112,4 +113,5 @@ this         this
 noncomputable noncomputable
 theory       theory
 key_equivalences key_equivalences
+using        using
 using_well_founded using_well_founded
--- a/src/library/constants.cpp
+++ b/src/library/constants.cpp
@ -339,11 +339,24 @@ name const * g_sum_inl = nullptr;
 name const * g_sum_inr = nullptr;
 name const * g_tactic = nullptr;
 name const * g_tactic_constructor = nullptr;
-name const * g_tactic_interactive = nullptr;
 name const * g_tactic_step = nullptr;
 name const * g_tactic_to_expr = nullptr;
 name const * g_tactic_skip = nullptr;
 name const * g_tactic_try = nullptr;
+name const * g_tactic_interactive = nullptr;
+name const * g_tactic_interactive_types_ident = nullptr;
+name const * g_tactic_interactive_types_opt_ident = nullptr;
+name const * g_tactic_interactive_types_using_ident = nullptr;
+name const * g_tactic_interactive_types_ident_list = nullptr;
+name const * g_tactic_interactive_types_raw_ident_list = nullptr;
+name const * g_tactic_interactive_types_with_ident_list = nullptr;
+name const * g_tactic_interactive_types_location = nullptr;
+name const * g_tactic_interactive_types_comma_tk = nullptr;
+name const * g_tactic_interactive_types_qexpr = nullptr;
+name const * g_tactic_interactive_types_qexpr0 = nullptr;
+name const * g_tactic_interactive_types_qexpr_list = nullptr;
+name const * g_tactic_interactive_types_qexpr_list_or_qexpr0 = nullptr;
+name const * g_tactic_interactive_types_itactic = nullptr;
 name const * g_to_string = nullptr;
 name const * g_to_int = nullptr;
 name const * g_to_real = nullptr;
@ -703,11 +716,24 @@ void initialize_constants() {
    g_sum_inr = new name{"sum", "inr"};
    g_tactic = new name{"tactic"};
    g_tactic_constructor = new name{"tactic", "constructor"};
-    g_tactic_interactive = new name{"tactic", "interactive"};
    g_tactic_step = new name{"tactic", "step"};
    g_tactic_to_expr = new name{"tactic", "to_expr"};
    g_tactic_skip = new name{"tactic", "skip"};
    g_tactic_try = new name{"tactic", "try"};
+    g_tactic_interactive = new name{"tactic", "interactive"};
+    g_tactic_interactive_types_ident = new name{"tactic", "interactive", "types", "ident"};
+    g_tactic_interactive_types_opt_ident = new name{"tactic", "interactive", "types", "opt_ident"};
+    g_tactic_interactive_types_using_ident = new name{"tactic", "interactive", "types", "using_ident"};
+    g_tactic_interactive_types_ident_list = new name{"tactic", "interactive", "types", "ident_list"};
+    g_tactic_interactive_types_raw_ident_list = new name{"tactic", "interactive", "types", "raw_ident_list"};
+    g_tactic_interactive_types_with_ident_list = new name{"tactic", "interactive", "types", "with_ident_list"};
+    g_tactic_interactive_types_location = new name{"tactic", "interactive", "types", "location"};
+    g_tactic_interactive_types_comma_tk = new name{"tactic", "interactive", "types", "comma_tk"};
+    g_tactic_interactive_types_qexpr = new name{"tactic", "interactive", "types", "qexpr"};
+    g_tactic_interactive_types_qexpr0 = new name{"tactic", "interactive", "types", "qexpr0"};
+    g_tactic_interactive_types_qexpr_list = new name{"tactic", "interactive", "types", "qexpr_list"};
+    g_tactic_interactive_types_qexpr_list_or_qexpr0 = new name{"tactic", "interactive", "types", "qexpr_list_or_qexpr0"};
+    g_tactic_interactive_types_itactic = new name{"tactic", "interactive", "types", "itactic"};
    g_to_string = new name{"to_string"};
    g_to_int = new name{"to_int"};
    g_to_real = new name{"to_real"};
@ -1068,11 +1094,24 @@ void finalize_constants() {
    delete g_sum_inr;
    delete g_tactic;
    delete g_tactic_constructor;
-    delete g_tactic_interactive;
    delete g_tactic_step;
    delete g_tactic_to_expr;
    delete g_tactic_skip;
    delete g_tactic_try;
+    delete g_tactic_interactive;
+    delete g_tactic_interactive_types_ident;
+    delete g_tactic_interactive_types_opt_ident;
+    delete g_tactic_interactive_types_using_ident;
+    delete g_tactic_interactive_types_ident_list;
+    delete g_tactic_interactive_types_raw_ident_list;
+    delete g_tactic_interactive_types_with_ident_list;
+    delete g_tactic_interactive_types_location;
+    delete g_tactic_interactive_types_comma_tk;
+    delete g_tactic_interactive_types_qexpr;
+    delete g_tactic_interactive_types_qexpr0;
+    delete g_tactic_interactive_types_qexpr_list;
+    delete g_tactic_interactive_types_qexpr_list_or_qexpr0;
+    delete g_tactic_interactive_types_itactic;
    delete g_to_string;
    delete g_to_int;
    delete g_to_real;
@ -1432,11 +1471,24 @@ name const & get_sum_inl_name() { return *g_sum_inl; }
 name const & get_sum_inr_name() { return *g_sum_inr; }
 name const & get_tactic_name() { return *g_tactic; }
 name const & get_tactic_constructor_name() { return *g_tactic_constructor; }
-name const & get_tactic_interactive_name() { return *g_tactic_interactive; }
 name const & get_tactic_step_name() { return *g_tactic_step; }
 name const & get_tactic_to_expr_name() { return *g_tactic_to_expr; }
 name const & get_tactic_skip_name() { return *g_tactic_skip; }
 name const & get_tactic_try_name() { return *g_tactic_try; }
+name const & get_tactic_interactive_name() { return *g_tactic_interactive; }
+name const & get_tactic_interactive_types_ident_name() { return *g_tactic_interactive_types_ident; }
+name const & get_tactic_interactive_types_opt_ident_name() { return *g_tactic_interactive_types_opt_ident; }
+name const & get_tactic_interactive_types_using_ident_name() { return *g_tactic_interactive_types_using_ident; }
+name const & get_tactic_interactive_types_ident_list_name() { return *g_tactic_interactive_types_ident_list; }
+name const & get_tactic_interactive_types_raw_ident_list_name() { return *g_tactic_interactive_types_raw_ident_list; }
+name const & get_tactic_interactive_types_with_ident_list_name() { return *g_tactic_interactive_types_with_ident_list; }
+name const & get_tactic_interactive_types_location_name() { return *g_tactic_interactive_types_location; }
+name const & get_tactic_interactive_types_comma_tk_name() { return *g_tactic_interactive_types_comma_tk; }
+name const & get_tactic_interactive_types_qexpr_name() { return *g_tactic_interactive_types_qexpr; }
+name const & get_tactic_interactive_types_qexpr0_name() { return *g_tactic_interactive_types_qexpr0; }
+name const & get_tactic_interactive_types_qexpr_list_name() { return *g_tactic_interactive_types_qexpr_list; }
+name const & get_tactic_interactive_types_qexpr_list_or_qexpr0_name() { return *g_tactic_interactive_types_qexpr_list_or_qexpr0; }
+name const & get_tactic_interactive_types_itactic_name() { return *g_tactic_interactive_types_itactic; }
 name const & get_to_string_name() { return *g_to_string; }
 name const & get_to_int_name() { return *g_to_int; }
 name const & get_to_real_name() { return *g_to_real; }
--- a/src/library/constants.h
+++ b/src/library/constants.h
@ -341,11 +341,24 @@ name const & get_sum_inl_name();
 name const & get_sum_inr_name();
 name const & get_tactic_name();
 name const & get_tactic_constructor_name();
-name const & get_tactic_interactive_name();
 name const & get_tactic_step_name();
 name const & get_tactic_to_expr_name();
 name const & get_tactic_skip_name();
 name const & get_tactic_try_name();
+name const & get_tactic_interactive_name();
+name const & get_tactic_interactive_types_ident_name();
+name const & get_tactic_interactive_types_opt_ident_name();
+name const & get_tactic_interactive_types_using_ident_name();
+name const & get_tactic_interactive_types_ident_list_name();
+name const & get_tactic_interactive_types_raw_ident_list_name();
+name const & get_tactic_interactive_types_with_ident_list_name();
+name const & get_tactic_interactive_types_location_name();
+name const & get_tactic_interactive_types_comma_tk_name();
+name const & get_tactic_interactive_types_qexpr_name();
+name const & get_tactic_interactive_types_qexpr0_name();
+name const & get_tactic_interactive_types_qexpr_list_name();
+name const & get_tactic_interactive_types_qexpr_list_or_qexpr0_name();
+name const & get_tactic_interactive_types_itactic_name();
 name const & get_to_string_name();
 name const & get_to_int_name();
 name const & get_to_real_name();
--- a/src/library/constants.txt
+++ b/src/library/constants.txt
@ -334,11 +334,24 @@ sum.inl
 sum.inr
 tactic
 tactic.constructor
-tactic.interactive
 tactic.step
 tactic.to_expr
 tactic.skip
 tactic.try
+tactic.interactive
+tactic.interactive.types.ident
+tactic.interactive.types.opt_ident
+tactic.interactive.types.using_ident
+tactic.interactive.types.ident_list
+tactic.interactive.types.raw_ident_list
+tactic.interactive.types.with_ident_list
+tactic.interactive.types.location
+tactic.interactive.types.comma_tk
+tactic.interactive.types.qexpr
+tactic.interactive.types.qexpr0
+tactic.interactive.types.qexpr_list
+tactic.interactive.types.qexpr_list_or_qexpr0
+tactic.interactive.types.itactic
 to_string
 to_int
 to_real
--- a/src/library/vm/vm_pexpr.cpp
+++ b/src/library/vm/vm_pexpr.cpp
@ -30,10 +30,20 @@ vm_obj pexpr_to_string(vm_obj const & e) {
    return expr_to_string(e);
 }

+vm_obj pexpr_to_raw_expr(vm_obj const & e) {
+    return e;
+}
+
+vm_obj pexpr_of_raw_expr(vm_obj const & e) {
+    return e;
+}
+
 void initialize_vm_pexpr() {
    DECLARE_VM_BUILTIN(name({"pexpr", "subst"}),        pexpr_subst);
    DECLARE_VM_BUILTIN(name({"pexpr", "of_expr"}),      pexpr_of_expr);
    DECLARE_VM_BUILTIN(name({"pexpr", "to_string"}),    pexpr_to_string);
+    DECLARE_VM_BUILTIN(name({"pexpr", "of_raw_expr"}),  pexpr_of_raw_expr);
+    DECLARE_VM_BUILTIN(name({"pexpr", "to_raw_expr"}),  pexpr_to_raw_expr);
 }

 void finalize_vm_pexpr() {
--- a/tests/lean/run/auto_quote1.lean
+++ b/tests/lean/run/auto_quote1.lean
@ -1,6 +1,6 @@
 example (a b c : nat) : a = b → b = c → c = a :=
 begin
-  tactic.intros,
+  intros,
  apply eq.symm,
  apply eq.trans,
  assumption,
@ -14,3 +14,49 @@ begin
  refine eq.symm (eq.trans h1 _),
  exact h2
 end
+
+example (a b c : nat) : a = b → b = c → c = a :=
+begin
+  intros h1 h2, -- we can optionally provide the names
+  refine eq.symm (eq.trans h1 _),
+  exact h2
+end
+
+example (a b c : nat) : a = b → b = c → c = a :=
+begin
+  intro h1,
+  intro, -- optional argument
+  refine eq.symm (eq.trans h1 _),
+  assumption
+end
+
+constant add_comm {a b : nat} : a + b = b + a
+constant add_assoc {a b c : nat} : (a + b) + c = a + (b + c)
+constant zero_add (a : nat) : 0 + a = a
+
+example (a b c : nat) : b = 0 → 0 + a + b + c = c + a :=
+begin
+  intro h,
+  rewrite h, -- single rewrite
+  rewrite [zero_add, @add_comm a 0, zero_add, add_comm] -- sequence of rewrites
+end
+
+example (a b c : nat) : 0 = b → 0 + a + b + c = c + a :=
+begin
+  intro h,
+  rewrite -h, -- single rewrite using symmetry
+  rw [zero_add, @add_comm a 0, zero_add, add_comm] -- rw is shorthand for rewrite
+end
+
+open nat
+
+example : ∀ n m : ℕ, n + m = m + n :=
+begin
+  intros n m,
+  induction m with m' ih,
+  { -- Remark: Used change here to make sure nat.zero is replaced with polymorphic zero.
+    -- dsimp tactic should fix that in the future.
+    change n + 0 = 0 + n, rw zero_add n },
+  { change succ (n + m') = succ m' + n,
+    rw [succ_add, ih] }
+end