fix(frontends/lean/builtin_exprs): bug in 'using' expressions

src/frontends/lean/builtin_exprs.cpp

@@ -303,10 +303,14 @@ static expr parse_using_expr(parser & p, expr const & prop, pos_info const & usi
         expr l      = p.parse_id();
         if (!is_local(l))
             throw parser_error("invalid 'using' declaration for 'have', local expected", id_pos);
-        expr new_l = l;
-        binder_info bi = local_info(l);
-        if (!bi.is_contextual())
-            new_l = update_local(l, bi.update_contextual(true));
+        expr new_l;
+        binder_info bi = local_info(l).update_contextual(true);
+        if (p.is_local_variable_parameter(local_pp_name(l))) {
+            expr new_type = p.save_pos(mk_as_is(mlocal_type(l)), id_pos);
+            new_l = p.save_pos(mk_local(mlocal_name(l), local_pp_name(l), new_type, bi), id_pos);
+        } else {
+            new_l = p.save_pos(update_local(l, bi), id_pos);
+        }
         p.add_local(new_l);
         locals.push_back(l);
         new_locals.push_back(new_l);

src/frontends/lean/local_decls.h

@@ -32,6 +32,11 @@ public:
         m_map.insert(k, mk_pair(v, m_counter));
         m_entries = cons(mk_pair(k, v), m_entries);
         m_counter++;
+        lean_assert(m_counter == length(m_entries)+1);
+    }
+    unsigned size() const {
+        lean_assert(m_counter > 0);
+        return m_counter - 1;
     }
     void update(name const & k, V const & v) {
         if (auto it = m_map.find(k)) {

src/frontends/lean/parser.cpp

@@ -110,6 +110,7 @@ parser::parser(environment const & env, io_state const & ios,
     m_scanner(strm, strm_name, s ? s->m_line : 1),
     m_theorem_queue(*this, num_threads > 1 ? num_threads - 1 : 0),
     m_snapshot_vector(sv), m_info_manager(im), m_cache(nullptr), m_index(nullptr) {
+    m_local_decls_size_at_beg_cmd = 0;
     m_profile    = ios.get_options().get_bool("profile", false);
     if (num_threads > 1 && m_profile)
         throw exception("option --profile cannot be used when theorems are compiled in parallel");
@@ -1599,6 +1600,7 @@ void parser::parse_command() {
     m_cmd_token = get_token_info().token();
     if (auto it = cmds().find(cmd_name)) {
         next();
+        m_local_decls_size_at_beg_cmd = m_local_decls.size();
         m_env = it->get_fn()(*this);
     } else {
         auto p = pos();

src/frontends/lean/parser.h

@@ -144,6 +144,9 @@ class parser {
     // profiling
     bool                   m_profile;
 
+    // auxiliary field used to record the size of m_local_decls before a command is executed.
+    unsigned               m_local_decls_size_at_beg_cmd;
+
     void display_warning_pos(unsigned line, unsigned pos);
     void display_error_pos(unsigned line, unsigned pos);
     void display_error_pos(pos_info p);
@@ -436,6 +439,11 @@ public:
     bool is_local_level_variable(name const & n) const { return m_level_variables.contains(n); }
     bool is_local_variable(name const & n) const { return m_variables.contains(n); }
     bool is_local_variable(expr const & e) const { return is_local_variable(local_pp_name(e)); }
+    /** \brief Return true iff n is the name of a variable or parameter. */
+    bool is_local_variable_parameter(name const & n) const {
+        unsigned idx = m_local_decls.find_idx(n);
+        return 0 < idx && idx <= m_local_decls_size_at_beg_cmd;
+    }
     /** \brief Update binder information for the section parameter n, return true if success, and false if n is not a section parameter. */
     bool update_local_binder_info(name const & n, binder_info const & bi);
     void include_variable(name const & n) { m_include_vars.insert(n); }

tests/lean/run/using_bug2.lean

@@ -0,0 +1,12 @@
+variable {A : Type}
+variable {f : A → A → A}
+variable {finv : A → A}
+premise  (h : ∀ x y : A, finv (f x y) = y)
+
+theorem foo₁ : ∀ x y z : A, f x y = f x z → y = z :=
+λ x y z, assume e, using h, from sorry
+
+theorem foo₂ : ∀ x y z : A, f x y = f x z → y = z :=
+λ x y z, assume e,
+assert s₁ : finv (f x y) = finv (f x z), by rewrite e,
+show y = z, using h, by rewrite *h at s₁; exact s₁