feat(library/init/meta): use cheap "reflexivity" after simp and rewrite

The idea is to make sure lean doesn't timeout (at reflexivity) when we apply simp or
rewrite in goals such as

    (x y : nat) |- x + y + 10000000000 = x + y + 200000000000000

This commit also addresses an issue raised at #1218

library/init/data/char/lemmas.lean

@@ -24,7 +24,8 @@ end
 lemma of_nat_eq_of_ge {n : nat} : n ≥ char_sz → of_nat n = of_nat 0 :=
 begin
   intro h,
-  rw [of_nat_eq_fin_of_ge h]
+  rw [of_nat_eq_fin_of_ge h],
+  reflexivity
 end
 
 lemma of_nat_ne_of_ne {n₁ n₂ : nat} (h₁ : n₁ ≠ n₂) (h₂ : n₁ < char_sz) (h₃ : n₂ < char_sz) : of_nat n₁ ≠ of_nat n₂ :=

library/init/data/nat/lemmas.lean

@@ -112,7 +112,7 @@ protected lemma left_distrib : ∀ (n m k : ℕ), n * (m + k) = n * m + n * k
   begin simp [succ_mul, left_distrib n m k], sort_add end
 
 protected lemma mul_comm : ∀ (n m : ℕ), n * m = m * n
-| n 0        := by rw nat.zero_mul
+| n 0        := by rw [nat.zero_mul, nat.mul_zero]
 | n (succ m) := by simp [mul_succ, succ_mul, mul_comm n m]
 
 protected lemma mul_assoc : ∀ (n m k : ℕ), (n * m) * k = n * (m * k)
@@ -121,7 +121,7 @@ protected lemma mul_assoc : ∀ (n m k : ℕ), (n * m) * k = n * (m * k)
 
 protected lemma mul_one : ∀ (n : ℕ), n * 1 = n
 | 0        := rfl
-| (succ n) := by simp [succ_mul, mul_one n]
+| (succ n) := by simp [succ_mul, mul_one n, add_one_eq_succ]
 
 protected lemma one_mul (n : ℕ) : 1 * n = n :=
 by rw [nat.mul_comm, nat.mul_one]

library/init/meta/interactive.lean

@@ -180,8 +180,8 @@ private meta def rw_hyps : transparency → list (bool × expr) → list name
 private meta def rw_core (m : transparency) (hs : qexpr_list_or_qexpr0) (loc : location) : tactic unit :=
 do hlist ← to_symm_expr_list hs,
    match loc with
-   | [] := rw_goal m hlist >> try reflexivity
-   | hs := rw_hyps m hlist hs >> try reflexivity
+   | [] := rw_goal m hlist >> try (reflexivity_core reducible)
+   | hs := rw_hyps m hlist hs >> try (reflexivity_core reducible)
    end
 
 meta def rewrite : qexpr_list_or_qexpr0 → location → tactic unit :=
@@ -350,7 +350,7 @@ do s ← mk_simp_set attr_names hs ids,
    | [] := simp_goal cfg s
    | _  := simp_hyps cfg s loc
    end,
-   try tactic.triv, try tactic.reflexivity
+   try tactic.triv, try (tactic.reflexivity_core reducible)
 
 meta def simp (hs : opt_qexpr_list) (attr_names : with_ident_list) (ids : without_ident_list) (loc : location) : tactic unit :=
 simp_core default_simplify_config hs attr_names ids loc
@@ -376,7 +376,7 @@ meta def transitivity : tactic unit :=
 tactic.transitivity
 
 meta def subst (q : qexpr0) : tactic unit :=
-to_expr q >>= tactic.subst >> try reflexivity
+to_expr q >>= tactic.subst >> try (reflexivity_core reducible)
 
 meta def clear : raw_ident_list → tactic unit :=
 tactic.clear_lst

library/init/meta/relation_tactics.lean

@@ -9,23 +9,26 @@ import init.meta.tactic init.function
 namespace tactic
 open expr
 
-private meta def relation_tactic (op_for : environment → name → option name) (tac_name : string) : tactic unit :=
+private meta def relation_tactic (t : transparency) (op_for : environment → name → option name) (tac_name : string) : tactic unit :=
 do tgt ← target,
    env ← get_env,
    r   ← return $ get_app_fn tgt,
    match (op_for env (const_name r)) with
-   | (some refl) := mk_const refl >>= apply
+   | (some refl) := mk_const refl >>= apply_core t ff tt
    | none        := fail $ tac_name ++ " tactic failed, target is not a relation application with the expected property."
    end
 
+meta def reflexivity_core (t : transparency) : tactic unit :=
+relation_tactic t environment.refl_for "reflexivity"
+
 meta def reflexivity : tactic unit :=
-relation_tactic environment.refl_for "reflexivity"
+reflexivity_core semireducible
 
 meta def symmetry : tactic unit :=
-relation_tactic environment.symm_for "symmetry"
+relation_tactic semireducible environment.symm_for "symmetry"
 
 meta def transitivity : tactic unit :=
-relation_tactic environment.trans_for "transitivity"
+relation_tactic semireducible environment.trans_for "transitivity"
 
 meta def relation_lhs_rhs : expr → tactic (name × expr × expr) :=
 λ e, do

library/init/meta/rewrite_tactic.lean

@@ -14,7 +14,7 @@ meta constant rewrite_at_core : transparency → bool → occurrences → bool
 meta def rewrite (th_name : name) : tactic unit :=
 do th ← mk_const th_name,
    rewrite_core reducible tt occurrences.all ff th,
-   try reflexivity
+   try (reflexivity_core reducible)
 
 meta def rewrite_at (th_name : name) (H_name : name) : tactic unit :=
 do th ← mk_const th_name,

library/init/meta/simp_tactic.lean

@@ -210,13 +210,13 @@ do (new_target, heq) ← target >>= simplify cfg extra_lemmas,
    mk_app `eq.mpr [heq, ht] >>= exact
 
 meta def simp : tactic unit :=
-simplify_goal default_simplify_config [] >> try triv >> try reflexivity
+simplify_goal default_simplify_config [] >> try triv >> try (reflexivity_core reducible)
 
 meta def simp_using (hs : list expr) : tactic unit :=
 simplify_goal default_simplify_config hs >> try triv
 
 meta def ctx_simp : tactic unit :=
-simplify_goal {default_simplify_config with contextual := tt} [] >> try triv >> try reflexivity
+simplify_goal {default_simplify_config with contextual := tt} [] >> try triv >> try (reflexivity_core reducible)
 
 meta def dsimp : tactic unit :=
 do S ← simp_lemmas.mk_default,

tests/lean/run/cheap_try_refl.lean

@@ -0,0 +1,23 @@
+example (h : false) : 10000000 = 20000000 :=
+begin
+  try {simp},
+  contradiction
+end
+
+example (h : false) (x : nat) : x + 10000000 = x + 20000000 :=
+begin
+  try {simp},
+  contradiction
+end
+
+example (h : false) (x y : nat) : x + y + 10000000 = x + y + 20000000 :=
+begin
+  try {simp},
+  contradiction
+end
+
+example (h : false) : "hello" = "world" :=
+begin
+  try {simp},
+  contradiction
+end