max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor(library/init/meta/simp_tactic): cleanup simp_intros mess

Browse source
This commit is contained in:
Leonardo de Moura 2017-07-03 13:46:16 -07:00
parent 6b3e28d30b
commit 34c212fa53
3 changed files with 24 additions and 38 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
doc/changes.md
View file

@ -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)
-------------

17
library/init/meta/interactive.lean
View file

@ -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)

44
library/init/meta/simp_tactic.lean
View file

@ -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"),