fix(frontends/lean): improve begin-end construct

src/frontends/lean/builtin_exprs.cpp

@@ -137,11 +137,12 @@ static expr parse_by(parser & p, unsigned, expr const *, pos_info const & pos) {
 static expr parse_begin_end_core(parser & p, pos_info const & pos) {
     if (!p.has_tactic_decls())
         throw parser_error("invalid 'begin-end' expression, tactic module has not been imported", pos);
-    optional<expr> pre_tac = get_begin_end_pre_tactic(p.env());
+    environment env = open_tactic_namespace(p);
+    parser::local_scope scope2(p, env);
+    parser::undef_id_to_local_scope scope1(p);
+    optional<expr> pre_tac = get_begin_end_pre_tactic(env);
     buffer<expr> tacs;
     bool first = true;
-    parser::undef_id_to_local_scope scope(p);
-    environment env = open_tactic_namespace(p);
     while (!p.curr_is_token(get_end_tk())) {
         if (first) {
             first = false;
@@ -159,7 +160,7 @@ static expr parse_begin_end_core(parser & p, pos_info const & pos) {
                           p.curr_is_token(get_assume_tk()) || p.curr_is_token(get_take_tk()) ||
                           p.curr_is_token(get_fun_tk()));
         auto pos = p.pos();
-        expr tac = p.parse_scoped_expr(0, nullptr, env);
+        expr tac = p.parse_expr();
         if (use_exact)
             tac = p.mk_app(get_exact_tac_fn(), tac, pos);
         if (pre_tac)

src/frontends/lean/parser.cpp

@@ -68,7 +68,12 @@ bool get_parser_parallel_import(options const & opts) {
 
 parser::local_scope::local_scope(parser & p):
     m_p(p), m_env(p.env()) {
-    p.push_local_scope();
+    m_p.push_local_scope();
+}
+parser::local_scope::local_scope(parser & p, environment const & env):
+    m_p(p), m_env(p.env()) {
+    m_p.m_env = env;
+    m_p.push_local_scope();
 }
 parser::local_scope::~local_scope() {
     m_p.pop_local_scope();

src/frontends/lean/parser.h

@@ -348,7 +348,9 @@ public:
     }
     expr parse_scoped_expr(buffer<expr> const & ps, unsigned rbp = 0) { return parse_scoped_expr(ps.size(), ps.data(), rbp); }
 
-    struct local_scope { parser & m_p; environment m_env; local_scope(parser & p); ~local_scope(); };
+    struct local_scope { parser & m_p; environment m_env;
+        local_scope(parser & p); local_scope(parser & p, environment const & env); ~local_scope();
+    };
     bool has_locals() const { return !m_local_decls.empty() || !m_local_level_decls.empty(); }
     void add_local_level(name const & n, level const & l, bool is_variable = false);
     void add_local_expr(name const & n, expr const & p, bool is_variable = false);

tests/lean/run/vector.lean

@@ -0,0 +1,36 @@
+import logic data.nat.basic
+open nat
+
+inductive vector (A : Type) : nat → Type :=
+vnil  : vector A zero,
+vcons : Π {n : nat}, A → vector A n → vector A (succ n)
+
+namespace vector
+  definition no_confusion_type {A : Type} {n : nat} (P : Type) (v₁ v₂ : vector A n) : Type :=
+  cases_on v₁
+    (cases_on v₂
+      (P → P)
+      (λ n₂ h₂ t₂, P))
+    (λ n₁ h₁ t₁, cases_on v₂
+      P
+      (λ n₂ h₂ t₂, (Π (H : n₁ = n₂), h₁ = h₂ → eq.rec_on H t₁ = t₂ → P) → P))
+
+  definition no_confusion {A : Type} {n : nat} {P : Type} {v₁ v₂ : vector A n} : v₁ = v₂ → no_confusion_type P v₁ v₂ :=
+  assume H₁₂ : v₁ = v₂,
+    have aux : v₁ = v₁ → no_confusion_type P v₁ v₁, from
+      take H₁₁, cases_on v₁
+        (assume h : P, h)
+        (take n₁ h₁ t₁, assume h : (Π (H : n₁ = n₁), h₁ = h₁ → t₁ = t₁ → P),
+          h rfl rfl rfl),
+    eq.rec aux H₁₂ H₁₂
+
+  theorem vcons.inj₁ {A : Type} {n : nat} (a₁ a₂ : A) (v₁ v₂ : vector A n) : vcons a₁ v₁ = vcons a₂ v₂ → a₁ = a₂ :=
+  begin
+     intro h, apply (no_confusion h), intros, assumption
+  end
+
+  theorem vcons.inj₂ {A : Type} {n : nat} (a₁ a₂ : A) (v₁ v₂ : vector A n) : vcons a₁ v₁ = vcons a₂ v₂ → v₁ = v₂ :=
+  begin
+    intro h, apply (no_confusion h), intros, eassumption
+  end
+end vector