From 7fe0fff91dc27cd0a25f82f52267e67aaad4d334 Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Mon, 29 May 2017 14:31:20 -0400 Subject: [PATCH] feat(library/init/meta/interactive): add 'only' option for simp, dimph, dimp_intros, and dsimp --- library/init/meta/interactive.lean | 40 ++++++++++--------- library/init/meta/simp_tactic.lean | 4 +- library/init/meta/smt/interactive.lean | 16 ++++---- .../{simp_wildcard.lean => simp_options.lean} | 17 ++++++++ 4 files changed, 48 insertions(+), 29 deletions(-) rename tests/lean/{simp_wildcard.lean => simp_options.lean} (59%) diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean index 9b37ae90b1..11788b2f9a 100644 --- a/library/init/meta/interactive.lean +++ b/library/init/meta/interactive.lean @@ -53,8 +53,11 @@ meta def location := (tk "at" *> (tk "*" *> pure loc.wildcard <|> (loc.ns <$> id meta def qexpr_list := list_of (qexpr 0) meta def opt_qexpr_list := qexpr_list <|> return [] meta def qexpr_list_or_texpr := qexpr_list <|> list.ret <$> texpr +meta def only_flag : parser bool := (tk "only" *> return tt) <|> return ff end types +precedence only:0 + /-- Use `desc` as the interactive description of `p`. -/ meta def with_desc {α : Type} (desc : format) (p : parser α) : parser α := p @@ -654,8 +657,8 @@ private meta def simp_lemmas.append_pexprs : simp_lemmas → list pexpr → tact | s [] := return s | s (l::ls) := do new_s ← simp_lemmas.add_pexpr s l, simp_lemmas.append_pexprs new_s ls -private meta def mk_simp_set (attr_names : list name) (hs : list pexpr) (ex : list name) : tactic simp_lemmas := -do s₀ ← join_user_simp_lemmas attr_names, +private meta def mk_simp_set (no_dflt : bool) (attr_names : list name) (hs : list pexpr) (ex : list name) : tactic simp_lemmas := +do s₀ ← join_user_simp_lemmas no_dflt attr_names, s₁ ← simp_lemmas.append_pexprs s₀ hs, -- add equational lemmas, if any ex ← ex.mfor (λ n, list.cons n <$> get_eqn_lemmas_for tt n), @@ -680,8 +683,8 @@ private meta def simp_hyps (cfg : simp_config) : simp_lemmas → list name → t | s [] := skip | s (h::hs) := simp_hyp cfg s h >> simp_hyps s hs -private meta def simp_core (cfg : simp_config) (ctx : list expr) (hs : list pexpr) (attr_names : list name) (ids : list name) (locat : loc) : tactic unit := -do s ← mk_simp_set attr_names hs ids, +private meta def simp_core (cfg : simp_config) (no_dflt : bool) (ctx : list expr) (hs : list pexpr) (attr_names : list name) (ids : list name) (locat : loc) : tactic unit := +do s ← mk_simp_set no_dflt attr_names hs ids, s ← s.append ctx, match locat : _ → tactic unit with | loc.wildcard := @@ -712,52 +715,51 @@ It has many variants. - `simp with attr` simplifies the main goal target using the lemmas tagged with the attribute `[attr]`. -/ -meta def simp (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) (locat : parse location) +meta def simp (no_dflt : parse only_flag) (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) (locat : parse location) (cfg : simp_config := {}) : tactic unit := -simp_core cfg [] hs attr_names ids locat +simp_core cfg no_dflt [] hs attr_names ids locat /-- Similar to the `simp` tactic, but adds all applicable hypotheses as simplification rules. -/ -meta def simp_using_hs (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) +meta def simp_using_hs (no_dflt : parse only_flag) (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) (cfg : simp_config := {}) : tactic unit := do ctx ← collect_ctx_simps, - simp_core cfg ctx hs attr_names ids (loc.ns []) + simp_core cfg no_dflt ctx hs attr_names ids (loc.ns []) -meta def simph (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) +meta def simph (no_dflt : parse only_flag) (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) (cfg : simp_config := {}) : tactic unit := -simp_using_hs hs attr_names ids cfg +simp_using_hs no_dflt hs attr_names ids cfg -meta def simp_intros (ids : parse ident_*) (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) +meta def simp_intros (ids : parse ident_*) (no_dflt : parse only_flag) (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (wo_ids : parse without_ident_list) (cfg : simp_config := {}) : tactic unit := -do s ← mk_simp_set attr_names hs wo_ids, +do s ← mk_simp_set no_dflt attr_names hs wo_ids, match ids with | [] := simp_intros_using s cfg | ns := simp_intro_lst_using ns s cfg end, try triv >> try (reflexivity reducible) -meta def simph_intros (ids : parse ident_*) (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) +meta def simph_intros (ids : parse ident_*) (no_dflt : parse only_flag) (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (wo_ids : parse without_ident_list) (cfg : simp_config := {}) : tactic unit := -do s ← mk_simp_set attr_names hs wo_ids, +do s ← mk_simp_set no_dflt attr_names hs wo_ids, match ids with | [] := simph_intros_using s cfg | ns := simph_intro_lst_using ns s cfg end, try triv >> try (reflexivity reducible) - private meta def dsimp_hyps (s : simp_lemmas) : list name → tactic unit | [] := skip | (h::hs) := get_local h >>= dsimp_at_core s -meta def dsimp (es : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) : parse location → tactic unit -| (loc.ns []) := do s ← mk_simp_set attr_names es ids, tactic.dsimp_core s -| (loc.ns hs) := do s ← mk_simp_set attr_names es ids, dsimp_hyps s hs +meta def dsimp (no_dflt : parse only_flag) (es : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) : parse location → tactic unit +| (loc.ns []) := do s ← mk_simp_set no_dflt attr_names es ids, tactic.dsimp_core s +| (loc.ns hs) := do s ← mk_simp_set no_dflt attr_names es ids, dsimp_hyps s hs | (loc.wildcard) := do ls ← local_context, n ← revert_lst ls, - s ← mk_simp_set attr_names es ids, + s ← mk_simp_set no_dflt attr_names es ids, tactic.dsimp_core s, intron n diff --git a/library/init/meta/simp_tactic.lean b/library/init/meta/simp_tactic.lean index 20e15c64de..2e490ef6dd 100644 --- a/library/init/meta/simp_tactic.lean +++ b/library/init/meta/simp_tactic.lean @@ -409,8 +409,8 @@ meta def join_user_simp_lemmas_core : simp_lemmas → list name → tactic simp_ | S [] := return S | S (attr_name::R) := do S' ← get_user_simp_lemmas attr_name, join_user_simp_lemmas_core (S.join S') R -meta def join_user_simp_lemmas : list name → tactic simp_lemmas -| [] := simp_lemmas.mk_default +meta def join_user_simp_lemmas (no_dflt : bool) : list name → tactic simp_lemmas +| [] := if no_dflt then pure simp_lemmas.mk else simp_lemmas.mk_default | attr_names := join_user_simp_lemmas_core simp_lemmas.mk attr_names /- Normalize numerical expression, returns a pair (n, pr) where n is the resultant numeral, diff --git a/library/init/meta/smt/interactive.lean b/library/init/meta/smt/interactive.lean index 187f6ccc87..aeceddf63e 100644 --- a/library/init/meta/smt/interactive.lean +++ b/library/init/meta/smt/interactive.lean @@ -228,18 +228,18 @@ slift (tactic.interactive.induction p rec_name ids revert) open tactic /-- Simplify the target type of the main goal. -/ -meta def simp (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) (cfg : simp_config := {}) : smt_tactic unit := -tactic.interactive.simp hs attr_names ids (loc.ns []) cfg +meta def simp (no_dflt : parse only_flag) (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) (cfg : simp_config := {}) : smt_tactic unit := +tactic.interactive.simp no_dflt hs attr_names ids (loc.ns []) cfg /-- Simplify the target type of the main goal using simplification lemmas and the current set of hypotheses. -/ -meta def simp_using_hs (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) (cfg : simp_config := {}) : smt_tactic unit := -tactic.interactive.simp_using_hs hs attr_names ids cfg +meta def simp_using_hs (no_dflt : parse only_flag) (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) (cfg : simp_config := {}) : smt_tactic unit := +tactic.interactive.simp_using_hs no_dflt hs attr_names ids cfg -meta def simph (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) (cfg : simp_config := {}) : smt_tactic unit := -simp_using_hs hs attr_names ids cfg +meta def simph (no_dflt : parse only_flag) (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) (cfg : simp_config := {}) : smt_tactic unit := +simp_using_hs no_dflt hs attr_names ids cfg -meta def dsimp (es : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) : smt_tactic unit := -tactic.interactive.dsimp es attr_names ids (loc.ns []) +meta def dsimp (no_dflt : parse only_flag) (es : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) : smt_tactic unit := +tactic.interactive.dsimp no_dflt es attr_names ids (loc.ns []) meta def rsimp : smt_tactic unit := do ccs ← to_cc_state, _root_.rsimp.rsimplify_goal ccs diff --git a/tests/lean/simp_wildcard.lean b/tests/lean/simp_options.lean similarity index 59% rename from tests/lean/simp_wildcard.lean rename to tests/lean/simp_options.lean index 4dacae05b9..c8ad53fff7 100644 --- a/tests/lean/simp_wildcard.lean +++ b/tests/lean/simp_options.lean @@ -25,3 +25,20 @@ begin rw [a₁, a₂], split; reflexivity end + +constants (f : ℕ → ℕ) (a b c : ℕ) (fab : f a = f b) (fbc : f b = f c) +constants (p : ℕ → Prop) (pfa : p (f a)) (pfb : p (f b)) (pfc :p (f c)) + +attribute [simp] fbc + +example : p (f a) := +by simp [fab]; exact pfc + +example : p (f a) := +by simp only [fab]; exact pfb + +example (h : p (f a)) : p (f c) := +by simp [fab] at h; assumption + +example (h : p (f a)) : p (f b) := +by simp only [fab] at h; assumption