fix(library/unifier): eager whnf application

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

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:

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

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