diff --git a/doc/changes.md b/doc/changes.md index b77103a208..017845ce31 100644 --- a/doc/changes.md +++ b/doc/changes.md @@ -87,6 +87,7 @@ For more details, see discussion [here](https://github.com/leanprover/lean/pull/ * `tactic.unfold_projections_core` => `tactic.unfold_projs` * `tactic.unfold_projections` => `tactic.unfold_projs_target` * `tactic.unfold_projections_at` => `tactic.unfold_projs_hyp` +* `tactic.simp_intros_using`, `tactic.simph_intros_using`, `tactic.simp_intro_lst_using`, `tactic.simph_intro_lst_using` => `tactic.simp_intros` v3.2.0 (18 June 2017) ------------- diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean index 8a5ff9b6cd..f04601d452 100644 --- a/library/init/meta/interactive.lean +++ b/library/init/meta/interactive.lean @@ -794,24 +794,15 @@ meta def simph (no_dflt : parse only_flag) (hs : parse opt_qexpr_list) (attr_nam simp_using_hs no_dflt hs attr_names ids cfg 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 := + (wo_ids : parse without_ident_list) (cfg : simp_intros_config := {}) : tactic unit := do (s, u) ← mk_simp_set no_dflt attr_names hs wo_ids, when (¬u.empty) (fail (sformat! "simp_intros tactic does not support {u}")), - match ids with - | [] := simp_intros_using s cfg - | ns := simp_intro_lst_using ns s cfg - end, + tactic.simp_intros s u ids cfg, try triv >> try (reflexivity reducible) 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, u) ← mk_simp_set no_dflt attr_names hs wo_ids, - when (¬u.empty) (fail (sformat! "simph_intros tactic does not support {u}")), - match ids with - | [] := simph_intros_using s cfg - | ns := simph_intro_lst_using ns s cfg - end, - try triv >> try (reflexivity reducible) + (wo_ids : parse without_ident_list) (cfg : simp_intros_config := {}) : tactic unit := +simp_intros ids no_dflt hs attr_names wo_ids {cfg with use_hyps := tt} private meta def dsimp_hyps (s : simp_lemmas) (u : list name) (hs : list name) (cfg : dsimp_config := {}) : tactic unit := hs.mfor' (λ h_name, do h ← get_local h_name, dsimp_hyp h s u cfg) diff --git a/library/init/meta/simp_tactic.lean b/library/init/meta/simp_tactic.lean index 9f4e8e0105..faa4ef11a7 100644 --- a/library/init/meta/simp_tactic.lean +++ b/library/init/meta/simp_tactic.lean @@ -271,59 +271,53 @@ private meta def collect_simps : list expr → tactic (list expr) meta def collect_ctx_simps : tactic (list expr) := local_context >>= collect_simps +section simp_intros + meta def intro1_aux : bool → list name → tactic expr | ff _ := intro1 | tt (n::ns) := intro n | _ _ := failed -meta def simp_intro_aux (cfg : simp_config) (updt : bool) : simp_lemmas → bool → list name → tactic simp_lemmas -| S tt [] := try (simp_target S [] cfg) >> return S +structure simp_intros_config extends simp_config := +(use_hyps := ff) + +meta def simp_intros_aux (cfg : simp_config) (use_hyps : bool) (to_unfold : list name) : simp_lemmas → bool → list name → tactic simp_lemmas +| S tt [] := try (simp_target S to_unfold cfg) >> return S | S use_ns ns := do t ← target, if t.is_napp_of `not 1 then - intro1_aux use_ns ns >> simp_intro_aux S use_ns ns.tail + intro1_aux use_ns ns >> simp_intros_aux S use_ns ns.tail else if t.is_arrow then do { d ← return t.binding_domain, - (new_d, h_d_eq_new_d) ← simplify S [] d cfg, + (new_d, h_d_eq_new_d) ← simplify S to_unfold d cfg, h_d ← intro1_aux use_ns ns, h_new_d ← mk_eq_mp h_d_eq_new_d h_d, assertv_core h_d.local_pp_name new_d h_new_d, clear h_d, h_new ← intro1, - new_S ← if updt then mcond (is_prop new_d) (S.add h_new) (return S) + new_S ← if use_hyps then mcond (is_prop new_d) (S.add h_new) (return S) else return S, - simp_intro_aux new_S use_ns ns.tail + simp_intros_aux new_S use_ns ns.tail } <|> -- failed to simplify... we just introduce and continue - (intro1_aux use_ns ns >> simp_intro_aux S use_ns ns.tail) + (intro1_aux use_ns ns >> simp_intros_aux S use_ns ns.tail) else if t.is_pi || t.is_let then - intro1_aux use_ns ns >> simp_intro_aux S use_ns ns.tail + intro1_aux use_ns ns >> simp_intros_aux S use_ns ns.tail else do new_t ← whnf t reducible, - if new_t.is_pi then unsafe_change new_t >> simp_intro_aux S use_ns ns + if new_t.is_pi then unsafe_change new_t >> simp_intros_aux S use_ns ns else - try (simp_target S [] cfg) >> + try (simp_target S to_unfold cfg) >> mcond (expr.is_pi <$> target) - (simp_intro_aux S use_ns ns) + (simp_intros_aux S use_ns ns) (if use_ns ∧ ¬ns.empty then failed else return S) -meta def simp_intros_using (s : simp_lemmas) (cfg : simp_config := {}) : tactic unit := -step $ simp_intro_aux cfg ff s ff [] +meta def simp_intros (s : simp_lemmas) (to_unfold : list name := []) (ids : list name := []) (cfg : simp_intros_config := {}) : tactic unit := +step $ simp_intros_aux cfg.to_simp_config cfg.use_hyps to_unfold s (bnot ids.empty) ids -meta def simph_intros_using (s : simp_lemmas) (cfg : simp_config := {}) : tactic unit := -step $ -do s ← collect_ctx_simps >>= s.append, - simp_intro_aux cfg tt s ff [] - -meta def simp_intro_lst_using (ns : list name) (s : simp_lemmas) (cfg : simp_config := {}) : tactic unit := -step $ simp_intro_aux cfg ff s tt ns - -meta def simph_intro_lst_using (ns : list name) (s : simp_lemmas) (cfg : simp_config := {}) : tactic unit := -step $ -do s ← collect_ctx_simps >>= s.append, - simp_intro_aux cfg tt s tt ns +end simp_intros meta def simp_at (h : expr) (extra_lemmas : list expr := []) (cfg : simp_config := {}) : tactic expr := do when (expr.is_local_constant h = ff) (fail "tactic simp_at failed, the given expression is not a hypothesis"),