feat(frontends/lean/parser): add_rewrite take the 'using' command into account

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/frontends/lean/parser_cmds.cpp

@@ -857,7 +857,11 @@ void parser_imp::parse_add_rewrite() {
     name rsid;
     parse_ids_and_rsid(th_names, rsid);
     for (auto id : th_names) {
-        add_rewrite_rules(m_env, rsid, id);
+        auto it = m_using_decls.find(id);
+        if (it != m_using_decls.end())
+            add_rewrite_rules(m_env, rsid, it->second);
+        else
+            add_rewrite_rules(m_env, rsid, id);
     }
 }
 

tests/lean/add_assoc.lean

@@ -0,0 +1,17 @@
+import tactic
+using Nat
+
+rewrite_set basic
+add_rewrite add_zerol add_succl eq_id : basic
+
+theorem add_assoc (a b c : Nat) : a + (b + c) = (a + b) + c
+:= induction_on a
+    (have 0 + (b + c) = (0 + b) + c : by simp basic)
+    (λ (n : Nat) (iH : n + (b + c) = (n + b) + c),
+        have (n + 1) + (b + c) = ((n + 1) + b) + c : by simp basic)
+
+check add_zerol
+check add_succl
+check @eq_id
+
+print environment 1

tests/lean/add_assoc.lean.expected.out

@@ -0,0 +1,23 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Imported 'tactic'
+  Using: Nat
+  Proved: add_assoc
+Nat::add_zerol : ∀ a : ℕ, 0 + a = a
+Nat::add_succl : ∀ a b : ℕ, a + 1 + b = a + b + 1
+@eq_id : ∀ (A : TypeU) (a : A), a = a ↔ ⊤
+theorem add_assoc (a b c : ℕ) : a + (b + c) = a + b + c :=
+    Nat::induction_on
+        a
+        (let have_expr : 0 + (b + c) = 0 + b + c :=
+                 eqt_elim (trans (congr (congr2 eq (Nat::add_zerol (b + c)))
+                                        (congr1 c (congr2 Nat::add (Nat::add_zerol b))))
+                                 (eq_id (b + c)))
+         in have_expr)
+        (λ (n : ℕ) (iH : n + (b + c) = n + b + c),
+           let have_expr : n + 1 + (b + c) = n + 1 + b + c :=
+                   eqt_elim (trans (congr (congr2 eq (trans (Nat::add_succl n (b + c)) (congr1 1 (congr2 Nat::add iH))))
+                                          (trans (congr1 c (congr2 Nat::add (Nat::add_succl n b)))
+                                                 (Nat::add_succl (n + b) c)))
+                                   (eq_id (n + b + c + 1)))
+           in have_expr)