From 692701c5ef18ca7e02e25900ef7efa87d1fff5b3 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 8 Dec 2016 14:38:25 -0800 Subject: [PATCH] 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 | 3 ++- library/init/data/nat/lemmas.lean | 4 ++-- library/init/meta/interactive.lean | 8 ++++---- library/init/meta/relation_tactics.lean | 13 ++++++++----- library/init/meta/rewrite_tactic.lean | 2 +- library/init/meta/simp_tactic.lean | 4 ++-- tests/lean/run/cheap_try_refl.lean | 23 +++++++++++++++++++++++ 7 files changed, 42 insertions(+), 15 deletions(-) create mode 100644 tests/lean/run/cheap_try_refl.lean diff --git a/library/init/data/char/lemmas.lean b/library/init/data/char/lemmas.lean index 78cc8eddd8..818cd5201b 100644 --- a/library/init/data/char/lemmas.lean +++ b/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₂ := diff --git a/library/init/data/nat/lemmas.lean b/library/init/data/nat/lemmas.lean index 82cd1fa625..69eebad9a5 100644 --- a/library/init/data/nat/lemmas.lean +++ b/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] diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean index 4bfe6aaee6..db630888cf 100644 --- a/library/init/meta/interactive.lean +++ b/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 diff --git a/library/init/meta/relation_tactics.lean b/library/init/meta/relation_tactics.lean index 93107a9454..ab2ee779ea 100644 --- a/library/init/meta/relation_tactics.lean +++ b/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 diff --git a/library/init/meta/rewrite_tactic.lean b/library/init/meta/rewrite_tactic.lean index adc8f53ce7..6ed1b7e103 100644 --- a/library/init/meta/rewrite_tactic.lean +++ b/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, diff --git a/library/init/meta/simp_tactic.lean b/library/init/meta/simp_tactic.lean index 8c6d936d71..1bb33ac4bc 100644 --- a/library/init/meta/simp_tactic.lean +++ b/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, diff --git a/tests/lean/run/cheap_try_refl.lean b/tests/lean/run/cheap_try_refl.lean new file mode 100644 index 0000000000..5b55480fb2 --- /dev/null +++ b/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