From 7f53cb96011e60fff1baeab75598284333129b74 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 28 Jan 2014 01:15:28 -0800
Subject: [PATCH] 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     |  6 +++++-
 tests/lean/add_assoc.lean              | 17 +++++++++++++++++
 tests/lean/add_assoc.lean.expected.out | 23 +++++++++++++++++++++++
 3 files changed, 45 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/add_assoc.lean
 create mode 100644 tests/lean/add_assoc.lean.expected.out

diff --git a/src/frontends/lean/parser_cmds.cpp b/src/frontends/lean/parser_cmds.cpp
index 4718408fc..81923a201 100644
--- a/src/frontends/lean/parser_cmds.cpp
+++ b/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);
     }
 }
 
diff --git a/tests/lean/add_assoc.lean b/tests/lean/add_assoc.lean
new file mode 100644
index 000000000..d0f715eaa
--- /dev/null
+++ b/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
\ No newline at end of file
diff --git a/tests/lean/add_assoc.lean.expected.out b/tests/lean/add_assoc.lean.expected.out
new file mode 100644
index 000000000..01ea01498
--- /dev/null
+++ b/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)