From 23af5ab217c46f42af48cce4c861d03be413b971 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 26 Jul 2014 10:36:21 -0700
Subject: [PATCH] fix(library/unifier): eager whnf application

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/library/unifier.cpp      | 11 +++++++++--
 tests/lean/run/nat_bug5.lean |  2 +-
 tests/lean/run/nat_bug6.lean | 19 +++++++++++++++++++
 3 files changed, 29 insertions(+), 3 deletions(-)
 create mode 100644 tests/lean/run/nat_bug6.lean

diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp
index b5bb77c19..7b857932d 100644
--- a/src/library/unifier.cpp
+++ b/src/library/unifier.cpp
@@ -1262,8 +1262,15 @@ struct unifier_fn {
         lean_assert(!is_meta(rhs));
         buffer<expr> margs;
         expr m     = get_app_args(lhs, margs);
-        for (expr & marg : margs)
-            marg = m_tc->whnf(marg);
+        for (expr & marg : margs) {
+            // Make sure that if marg is reducible to a local constant, then it is replaced with it.
+            // We need that because of the optimization based on is_easy_flex_rigid_arg
+            if (!is_local(marg)) {
+                expr new_marg = m_tc->whnf(marg);
+                if (is_local(new_marg))
+                    marg = new_marg;
+            }
+        }
         buffer<constraints> alts;
         switch (rhs.kind()) {
         case expr_kind::Var: case expr_kind::Meta:
diff --git a/tests/lean/run/nat_bug5.lean b/tests/lean/run/nat_bug5.lean
index 342946442..4927a318f 100644
--- a/tests/lean/run/nat_bug5.lean
+++ b/tests/lean/run/nat_bug5.lean
@@ -17,7 +17,7 @@ axiom mul_succ_right (n m : nat) : n * succ m = n * m + n
 axiom add_assoc (n m k : nat) : (n + m) + k = n + (m + k)
 axiom add_right_comm (n m k : nat) : n + m + k = n + k + m
 axiom induction_on {P : nat → Prop} (a : nat) (H1 : P zero) (H2 : ∀ (n : nat) (IH : P n), P (succ n)) : P a
-
+set_option unifier.max_steps 50000
 theorem mul_add_distr_left (n m k : nat) : (n + m) * k = n * k + m * k
 := induction_on k
     (calc
diff --git a/tests/lean/run/nat_bug6.lean b/tests/lean/run/nat_bug6.lean
new file mode 100644
index 000000000..5c035cda5
--- /dev/null
+++ b/tests/lean/run/nat_bug6.lean
@@ -0,0 +1,19 @@
+import logic num
+using eq_proofs
+
+inductive nat : Type :=
+| zero : nat
+| succ : nat → nat
+
+definition add (x y : nat) : nat := nat_rec x (λn r, succ r) y
+infixl `+`:65 := add
+definition mul (n m : nat) := nat_rec zero (fun m x, x + n) m
+infixl `*`:75 := mul
+
+axiom mul_zero_right (n : nat) : n * zero = zero
+
+variable P : nat → Prop
+
+print "==========================="
+theorem tst (n : nat) (H : P (n * zero)) : P zero
+:= subst (mul_zero_right _) H
\ No newline at end of file