feat(library/init/meta/simp_tactic): add option for reducing [reducible] definitions at dsimp, and to_unfold : list name similar to the one in the simp tactic
This complete addresses the two pending items at 16711fcdba
This commit is contained in:
Leonardo de Moura
parent
9a41f0f899
commit
6b3e28d30b
23 changed files with 138 additions and 100 deletions
|
|
@ -34,7 +34,7 @@ master branch (aka work in progress branch)
|
|||
tries to discharge the subgoal by reducing it to `true`.
|
||||
Example: `simp {discharger := assumption}`.
|
||||
|
||||
* `simp` can be used to unfold projection applications when the argument is a type class instance.
|
||||
* `simp` and `dsimp` can be used to unfold projection applications when the argument is a type class instance.
|
||||
Example: `simp [has_add.add]` will replace `@has_add.add nat nat.has_add a b` with `nat.add a b`
|
||||
|
||||
* `dsimp` has several new configuration options to control reduction (e.g., `iota`, `beta`, `zeta`, ...).
|
||||
|
|
@ -62,6 +62,8 @@ For more details, see discussion [here](https://github.com/leanprover/lean/pull/
|
|||
* `dsimp` does not unfold reducible definitions by default anymore.
|
||||
Example: `function.comp` applications will not be unfolded by default.
|
||||
We should use `dsimp [f]` if we want to reduce a reducible definition `f`.
|
||||
Another option is to use the new configuration parameter `unfold_reducible`.
|
||||
Example `dsimp {unfold_reducible := tt}`
|
||||
|
||||
* All `dunfold` and `unfold` tactics fail if they did not unfold anything.
|
||||
We can simulate the v3.2.0 using `unfold f {fail_if_unchaged := ff}` or `try {unfold f}`.
|
||||
|
|
@ -73,6 +75,18 @@ For more details, see discussion [here](https://github.com/leanprover/lean/pull/
|
|||
and it is shorthand for `unfold f {single_pass := tt}`.
|
||||
Remark: in v3.2.0, `unfold` was just an alias for the `dunfold` tactic.
|
||||
|
||||
*API name changes*
|
||||
|
||||
* `tactic.dsimp` and `tactic.dsimp_core` => `tactic.dsimp_target`
|
||||
* `tactic.dsimp_at_core` and `tactic.dsimp_at` => `tactic.dsimp_hyp`
|
||||
* `tactic.delta_expr` => `tactic.delta`
|
||||
* `tactic.delta` => `tactic.delta_target`
|
||||
* `tactic.delta_at` => `tactic.delta_hyp`
|
||||
* `tactic.simplify_goal` => `tactic.simp_target`
|
||||
* `tactic.unfold_projection` => `tactic.unfold_proj`
|
||||
* `tactic.unfold_projections_core` => `tactic.unfold_projs`
|
||||
* `tactic.unfold_projections` => `tactic.unfold_projs_target`
|
||||
* `tactic.unfold_projections_at` => `tactic.unfold_projs_hyp`
|
||||
|
||||
v3.2.0 (18 June 2017)
|
||||
-------------
|
||||
|
|
|
|||
|
|
@ -67,13 +67,13 @@ reflexivity
|
|||
meta def whnf : conv unit :=
|
||||
lhs >>= tactic.whnf >>= change
|
||||
|
||||
meta def dsimp (s : option simp_lemmas := none) (cfg : dsimp_config := {}) : conv unit :=
|
||||
meta def dsimp (s : option simp_lemmas := none) (u : list name := []) (cfg : dsimp_config := {}) : conv unit :=
|
||||
do s ← match s with
|
||||
| some s := return s
|
||||
| none := simp_lemmas.mk_default
|
||||
end,
|
||||
l ← lhs,
|
||||
s.dsimplify l cfg >>= change
|
||||
s.dsimplify u l cfg >>= change
|
||||
|
||||
private meta def congr_aux : list congr_arg_kind → list expr → tactic (list expr × list expr)
|
||||
| [] [] := return ([], [])
|
||||
|
|
|
|||
|
|
@ -42,7 +42,7 @@ conv.whnf
|
|||
meta def dsimp (no_dflt : parse only_flag) (es : parse opt_qexpr_list) (attr_names : parse with_ident_list)
|
||||
(ids : parse without_ident_list) (cfg : tactic.dsimp_config := {}) : conv unit :=
|
||||
do (s, u) ← tactic.mk_simp_set no_dflt attr_names es ids,
|
||||
conv.dsimp (some s) cfg
|
||||
conv.dsimp (some s) u cfg
|
||||
|
||||
meta def trace_lhs : conv unit :=
|
||||
lhs >>= tactic.trace
|
||||
|
|
|
|||
|
|
@ -813,18 +813,18 @@ do (s, u) ← mk_simp_set no_dflt attr_names hs wo_ids,
|
|||
end,
|
||||
try triv >> try (reflexivity reducible)
|
||||
|
||||
private meta def dsimp_hyps (s : simp_lemmas) (hs : list name) (cfg : dsimp_config := {}) : tactic unit :=
|
||||
hs.mfor' (λ h_name, do h ← get_local h_name, dsimp_at_core s h cfg)
|
||||
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)
|
||||
|
||||
meta def dsimp (no_dflt : parse only_flag) (es : parse opt_qexpr_list) (attr_names : parse with_ident_list)
|
||||
(ids : parse without_ident_list) (l : parse location) (cfg : dsimp_config := {}) : tactic unit :=
|
||||
match l with
|
||||
| (loc.ns []) := do (s, u) ← mk_simp_set no_dflt attr_names es ids, tactic.dsimp_core s cfg
|
||||
| (loc.ns hs) := do (s, u) ← mk_simp_set no_dflt attr_names es ids, dsimp_hyps s hs cfg
|
||||
| (loc.ns []) := do (s, u) ← mk_simp_set no_dflt attr_names es ids, dsimp_target s u cfg
|
||||
| (loc.ns hs) := do (s, u) ← mk_simp_set no_dflt attr_names es ids, dsimp_hyps s u hs cfg
|
||||
| (loc.wildcard) := do ls ← local_context,
|
||||
n ← revert_lst ls,
|
||||
(s, u) ← mk_simp_set no_dflt attr_names es ids,
|
||||
tactic.dsimp_core s cfg,
|
||||
dsimp_target s u cfg,
|
||||
intron n
|
||||
end
|
||||
|
||||
|
|
@ -904,28 +904,28 @@ end
|
|||
|
||||
private meta def delta_hyps : list name → list name → tactic unit
|
||||
| cs [] := skip
|
||||
| cs (h::hs) := get_local h >>= delta_at cs >> delta_hyps cs hs
|
||||
| cs (h::hs) := get_local h >>= delta_hyp cs >> delta_hyps cs hs
|
||||
|
||||
meta def delta : parse ident* → parse location → tactic unit
|
||||
| cs (loc.ns []) := do new_cs ← to_qualified_names cs, tactic.delta new_cs
|
||||
| cs (loc.ns []) := do new_cs ← to_qualified_names cs, delta_target new_cs
|
||||
| cs (loc.ns hs) := do new_cs ← to_qualified_names cs, delta_hyps new_cs hs
|
||||
| cs (loc.wildcard) := do ls ← tactic.local_context,
|
||||
n ← revert_lst ls,
|
||||
new_cs ← to_qualified_names cs,
|
||||
tactic.delta new_cs,
|
||||
delta_target new_cs,
|
||||
intron n
|
||||
|
||||
private meta def unfold_projections_hyps : list name → tactic unit
|
||||
private meta def unfold_projs_hyps : list name → tactic unit
|
||||
| [] := skip
|
||||
| (h::hs) := get_local h >>= unfold_projections_at >> unfold_projections_hyps hs
|
||||
| (h::hs) := get_local h >>= unfold_projs_hyp >> unfold_projs_hyps hs
|
||||
|
||||
/--
|
||||
This tactic unfolds all structure projections.
|
||||
-/
|
||||
meta def unfold_projections : parse location → tactic unit
|
||||
| (loc.ns []) := tactic.unfold_projections
|
||||
| (loc.ns hs) := unfold_projections_hyps hs
|
||||
| (loc.wildcard) := do ls ← local_context, unfold_projections_hyps (ls.map expr.local_pp_name)
|
||||
meta def unfold_projs : parse location → tactic unit
|
||||
| (loc.ns []) := tactic.unfold_projs_target
|
||||
| (loc.ns hs) := unfold_projs_hyps hs
|
||||
| (loc.wildcard) := do ls ← local_context, unfold_projs_hyps (ls.map expr.local_pp_name)
|
||||
|
||||
end interactive
|
||||
|
||||
|
|
|
|||
|
|
@ -73,12 +73,15 @@ structure dsimp_config :=
|
|||
(beta : bool := tt)
|
||||
(proj : bool := tt) -- reduce projections
|
||||
(iota : bool := tt)
|
||||
(unfold_reducible := ff) -- if tt, reducible definitions will be unfolded (delta-reduced)
|
||||
(memoize := tt)
|
||||
end tactic
|
||||
|
||||
/-- (Definitional) Simplify the given expression using *only* reflexivity equality lemmas from the given set of lemmas.
|
||||
The resulting expression is definitionally equal to the input. -/
|
||||
meta constant simp_lemmas.dsimplify (s : simp_lemmas) (e : expr) (cfg : tactic.dsimp_config := {}) : tactic expr
|
||||
The resulting expression is definitionally equal to the input.
|
||||
|
||||
The list `u` contains defintions to be delta-reduced, and projections to be reduced.-/
|
||||
meta constant simp_lemmas.dsimplify (s : simp_lemmas) (u : list name := []) (e : expr) (cfg : tactic.dsimp_config := {}) : tactic expr
|
||||
|
||||
namespace tactic
|
||||
/- Remark: the configuration parameters `cfg.md` and `cfg.eta` are ignored by this tactic. -/
|
||||
|
|
@ -110,18 +113,15 @@ meta def dsimplify
|
|||
(λ u e, do r ← post e, return (u, r)) e,
|
||||
return new_e
|
||||
|
||||
meta def dsimp_core (s : simp_lemmas) (cfg : dsimp_config := {}) : tactic unit :=
|
||||
do t ← target, s.dsimplify t cfg >>= unsafe_change
|
||||
meta def get_simp_lemmas_or_default : option simp_lemmas → tactic simp_lemmas
|
||||
| none := simp_lemmas.mk_default
|
||||
| (some s) := return s
|
||||
|
||||
meta def dsimp (cfg : dsimp_config := {}) : tactic unit :=
|
||||
do s ← simp_lemmas.mk_default, dsimp_core s cfg
|
||||
|
||||
meta def dsimp_at_core (s : simp_lemmas) (h : expr) (cfg : dsimp_config := {}) : tactic unit :=
|
||||
revert_and_transform (λ e, s.dsimplify e cfg) h
|
||||
|
||||
meta def dsimp_at (h : expr) (cfg : dsimp_config := {}) : tactic unit :=
|
||||
do s ← simp_lemmas.mk_default, dsimp_at_core s h cfg
|
||||
meta def dsimp_target (s : option simp_lemmas := none) (u : list name := []) (cfg : dsimp_config := {}) : tactic unit :=
|
||||
do s ← get_simp_lemmas_or_default s, t ← target, s.dsimplify u t cfg >>= unsafe_change
|
||||
|
||||
meta def dsimp_hyp (h : expr) (s : option simp_lemmas := none) (u : list name := []) (cfg : dsimp_config := {}) : tactic unit :=
|
||||
do s ← get_simp_lemmas_or_default s, revert_and_transform (λ e, s.dsimplify u e cfg) h
|
||||
|
||||
/- Remark: we use transparency.instances by default to make sure that we
|
||||
can unfold projections of type classes. Example:
|
||||
|
|
@ -130,8 +130,6 @@ do s ← simp_lemmas.mk_default, dsimp_at_core s h cfg
|
|||
-/
|
||||
|
||||
/-- If `e` is a projection application, try to unfold it, otherwise fail. -/
|
||||
meta constant unfold_projection (e : expr) (md := transparency.instances) : tactic expr
|
||||
|
||||
meta constant dunfold_expr (e : expr) (md := transparency.instances) : tactic expr
|
||||
|
||||
structure dunfold_config extends dsimp_config :=
|
||||
|
|
@ -157,7 +155,7 @@ cs.any (λ c,
|
|||
f.is_constant && f.const_name.is_internal && (f.const_name.get_prefix = c))
|
||||
|
||||
/-- Delta reduce the given constant names -/
|
||||
meta def delta_expr (cs : list name) (e : expr) (cfg : delta_config) : tactic expr :=
|
||||
meta def delta (cs : list name) (e : expr) (cfg : delta_config := {}) : tactic expr :=
|
||||
let unfold (u : unit) (e : expr) : tactic (unit × expr × bool) := do
|
||||
guard (is_delta_target e cs),
|
||||
(expr.const f_name f_lvls) ← return e.get_app_fn,
|
||||
|
|
@ -169,24 +167,29 @@ let unfold (u : unit) (e : expr) : tactic (unit × expr × bool) := do
|
|||
in do (c, new_e) ← dsimplify_core () (λ c e, failed) unfold e {max_steps := cfg.max_steps, canonize_instances := cfg.visit_instances},
|
||||
return new_e
|
||||
|
||||
meta def delta (cs : list name) : tactic unit :=
|
||||
do t ← target, delta_expr cs t {} >>= unsafe_change
|
||||
meta def delta_target (cs : list name) (cfg : delta_config := {}) : tactic unit :=
|
||||
do t ← target, delta cs t cfg >>= unsafe_change
|
||||
|
||||
meta def delta_at (cs : list name) : expr → tactic unit :=
|
||||
revert_and_transform (λ e, delta_expr cs e {})
|
||||
meta def delta_hyp (cs : list name) (h : expr) (cfg : delta_config := {}) :tactic unit :=
|
||||
revert_and_transform (λ e, delta cs e cfg) h
|
||||
|
||||
meta def unfold_projections_core (e : expr) (md := transparency.instances) (max_steps : nat := simp.default_max_steps) : tactic expr :=
|
||||
structure unfold_proj_config extends dsimp_config :=
|
||||
(md := transparency.instances)
|
||||
|
||||
meta constant unfold_proj (e : expr) (md := transparency.instances) : tactic expr
|
||||
|
||||
meta def unfold_projs (e : expr) (cfg : unfold_proj_config := {}) : tactic expr :=
|
||||
let unfold (changed : bool) (e : expr) : tactic (bool × expr × bool) := do
|
||||
new_e ← unfold_projection e md,
|
||||
new_e ← unfold_proj e cfg.md,
|
||||
return (tt, new_e, tt)
|
||||
in do (tt, new_e) ← dsimplify_core ff (λ c e, failed) unfold e {max_steps := max_steps, md := md} | fail "no projections to unfold",
|
||||
in do (tt, new_e) ← dsimplify_core ff (λ c e, failed) unfold e cfg.to_dsimp_config | fail "no projections to unfold",
|
||||
return new_e
|
||||
|
||||
meta def unfold_projections (md := transparency.instances) (max_steps : nat := simp.default_max_steps) : tactic unit :=
|
||||
do t ← target, unfold_projections_core t md max_steps >>= unsafe_change
|
||||
meta def unfold_projs_target (cfg : unfold_proj_config := {}) : tactic unit :=
|
||||
do t ← target, unfold_projs t cfg >>= unsafe_change
|
||||
|
||||
meta def unfold_projections_at (h : expr) (md := transparency.instances) (max_steps : nat := simp.default_max_steps) : tactic unit :=
|
||||
revert_and_transform (λ e, unfold_projections_core e md max_steps) h
|
||||
meta def unfold_projs_hyp (h : expr) (cfg : unfold_proj_config := {}) : tactic unit :=
|
||||
revert_and_transform (λ e, unfold_projs e cfg) h
|
||||
|
||||
structure simp_config :=
|
||||
(max_steps : nat := simp.default_max_steps)
|
||||
|
|
@ -215,7 +218,7 @@ structure simp_config :=
|
|||
meta constant simplify (s : simp_lemmas) (to_unfold : list name) (e : expr) (cfg : simp_config := {}) (r : name := `eq)
|
||||
(discharger : tactic unit := failed) : tactic (expr × expr)
|
||||
|
||||
meta def simplify_goal (S : simp_lemmas) (to_unfold : list name := []) (cfg : simp_config := {}) (discharger : tactic unit := failed) : tactic unit :=
|
||||
meta def simp_target (S : simp_lemmas) (to_unfold : list name := []) (cfg : simp_config := {}) (discharger : tactic unit := failed) : tactic unit :=
|
||||
do t ← target,
|
||||
(new_t, pr) ← simplify S to_unfold t cfg `eq discharger,
|
||||
replace_target new_t pr
|
||||
|
|
@ -274,7 +277,7 @@ meta def intro1_aux : bool → list name → tactic expr
|
|||
| _ _ := failed
|
||||
|
||||
meta def simp_intro_aux (cfg : simp_config) (updt : bool) : simp_lemmas → bool → list name → tactic simp_lemmas
|
||||
| S tt [] := try (simplify_goal S [] cfg) >> return S
|
||||
| S tt [] := try (simp_target S [] cfg) >> return S
|
||||
| S use_ns ns := do
|
||||
t ← target,
|
||||
if t.is_napp_of `not 1 then
|
||||
|
|
@ -301,7 +304,7 @@ meta def simp_intro_aux (cfg : simp_config) (updt : bool) : simp_lemmas → bool
|
|||
new_t ← whnf t reducible,
|
||||
if new_t.is_pi then unsafe_change new_t >> simp_intro_aux S use_ns ns
|
||||
else
|
||||
try (simplify_goal S [] cfg) >>
|
||||
try (simp_target S [] cfg) >>
|
||||
mcond (expr.is_pi <$> target)
|
||||
(simp_intro_aux S use_ns ns)
|
||||
(if use_ns ∧ ¬ns.empty then failed else return S)
|
||||
|
|
@ -423,7 +426,6 @@ do
|
|||
let s := remove_deps s t,
|
||||
return $ ctx.filter (λ h, s.contains h.local_uniq_name)
|
||||
|
||||
|
||||
section simp_all
|
||||
|
||||
meta structure simp_all_entry :=
|
||||
|
|
@ -471,7 +473,7 @@ private meta def loop (cfg : simp_config) (discharger : tactic unit) (to_unfold
|
|||
if m then loop r [] s ff
|
||||
else do
|
||||
add_new_hyps r,
|
||||
target_changed ← (simplify_goal s to_unfold cfg discharger >> return tt) <|> return ff,
|
||||
target_changed ← (simp_target s to_unfold cfg discharger >> return tt) <|> return ff,
|
||||
guard (cfg.fail_if_unchanged = ff ∨ target_changed ∨ r.any (λ e, e.pr ≠ none)) <|> fail "simp_all tactic failed to simplify",
|
||||
clear_old_hyps r
|
||||
| (e::es) r s m := do
|
||||
|
|
|
|||
|
|
@ -79,7 +79,7 @@ private meta def unfold_sizeof_loop : tactic unit :=
|
|||
do
|
||||
dunfold [``sizeof, ``has_sizeof.sizeof] {fail_if_unchanged := ff},
|
||||
S ← target >>= collect_sizeof_lemmas,
|
||||
(simplify_goal S >> unfold_sizeof_loop)
|
||||
(simp_target S >> unfold_sizeof_loop)
|
||||
<|>
|
||||
try `[simp]
|
||||
|
||||
|
|
|
|||
|
|
@ -12,8 +12,10 @@ Author: Leonardo de Moura
|
|||
#include "library/fun_info.h"
|
||||
#include "library/util.h"
|
||||
#include "library/trace.h"
|
||||
#include "library/reducible.h"
|
||||
#include "library/vm/vm.h"
|
||||
#include "library/vm/vm_nat.h"
|
||||
#include "library/vm/vm_list.h"
|
||||
#include "library/vm/vm_expr.h"
|
||||
#include "library/tactic/dsimplify.h"
|
||||
#include "library/tactic/simp_lemmas.h"
|
||||
|
|
@ -58,6 +60,26 @@ expr reduce_beta_eta_proj_iota(type_context & ctx, expr e, bool beta, bool eta,
|
|||
return e;
|
||||
}
|
||||
|
||||
optional<expr> unfold_step(type_context & ctx, expr const & e, name_set const & to_unfold, bool unfold_reducible) {
|
||||
if (!unfold_reducible && to_unfold.empty())
|
||||
return none_expr();
|
||||
if (!is_app(e) && !is_constant(e))
|
||||
return none_expr();
|
||||
expr const & fn = get_app_fn(e);
|
||||
if (!is_constant(fn))
|
||||
return none_expr();
|
||||
name const & fn_name = const_name(fn);
|
||||
if (!to_unfold.contains(const_name(fn)) && (!unfold_reducible || !is_reducible(ctx.env(), fn_name)))
|
||||
return none_expr();
|
||||
type_context::transparency_scope scope(ctx, transparency_mode::Instances);
|
||||
optional<expr> new_e;
|
||||
if (is_projection(ctx.env(), const_name(fn))) {
|
||||
return ctx.reduce_projection(e);
|
||||
} else {
|
||||
return unfold_term(ctx.env(), e);
|
||||
}
|
||||
}
|
||||
|
||||
dsimp_config::dsimp_config():
|
||||
m_md(transparency_mode::Reducible),
|
||||
m_max_steps(LEAN_DEFAULT_DSIMPLIFY_MAX_STEPS),
|
||||
|
|
@ -69,6 +91,7 @@ dsimp_config::dsimp_config():
|
|||
m_beta(true),
|
||||
m_proj(true),
|
||||
m_iota(true),
|
||||
m_unfold_reducible(false),
|
||||
m_memoize(true) {
|
||||
}
|
||||
dsimp_config::dsimp_config(vm_obj const & o) {
|
||||
|
|
@ -82,7 +105,8 @@ dsimp_config::dsimp_config(vm_obj const & o) {
|
|||
m_beta = to_bool(cfield(o, 7));
|
||||
m_proj = to_bool(cfield(o, 8));
|
||||
m_iota = to_bool(cfield(o, 9));
|
||||
m_memoize = to_bool(cfield(o, 10));
|
||||
m_unfold_reducible = to_bool(cfield(o, 10));
|
||||
m_memoize = to_bool(cfield(o, 11));
|
||||
}
|
||||
|
||||
#define lean_dsimp_trace(CTX, N, CODE) lean_trace(N, scope_trace_env _scope1(CTX.env(), CTX); CODE)
|
||||
|
|
@ -294,6 +318,8 @@ optional<pair<expr, bool>> dsimplify_fn::pre(expr const & e) {
|
|||
}
|
||||
|
||||
optional<pair<expr, bool>> dsimplify_fn::post(expr const & e) {
|
||||
if (auto r = unfold_step(m_ctx, e, m_to_unfold, m_cfg.m_unfold_reducible))
|
||||
return optional<pair<expr, bool>>(*r, true);
|
||||
expr curr_e;
|
||||
{
|
||||
type_context::transparency_scope s(m_ctx, m_cfg.m_md);
|
||||
|
|
@ -332,9 +358,11 @@ optional<pair<expr, bool>> dsimplify_fn::post(expr const & e) {
|
|||
return optional<pair<expr, bool>>(curr_e, true);
|
||||
}
|
||||
|
||||
dsimplify_fn::dsimplify_fn(type_context & ctx, defeq_canonizer::state & dcs, simp_lemmas_for const & lemmas, dsimp_config const & cfg):
|
||||
dsimplify_fn::dsimplify_fn(type_context & ctx, defeq_canonizer::state & dcs, simp_lemmas_for const & lemmas,
|
||||
list<name> const & to_unfold, dsimp_config const & cfg):
|
||||
dsimplify_core_fn(ctx, dcs, cfg),
|
||||
m_simp_lemmas(lemmas) {
|
||||
m_simp_lemmas(lemmas),
|
||||
m_to_unfold(to_name_set(to_unfold)) {
|
||||
}
|
||||
|
||||
class tactic_dsimplify_fn : public dsimplify_core_fn {
|
||||
|
|
@ -404,16 +432,17 @@ vm_obj tactic_dsimplify_core(vm_obj const &, vm_obj const & a,
|
|||
}
|
||||
}
|
||||
|
||||
vm_obj simp_lemmas_dsimplify(vm_obj const & lemmas, vm_obj const & e, vm_obj const & _cfg, vm_obj const & _s) {
|
||||
vm_obj simp_lemmas_dsimplify(vm_obj const & lemmas, vm_obj const & u, vm_obj const & e, vm_obj const & _cfg, vm_obj const & _s) {
|
||||
tactic_state const & s = tactic::to_state(_s);
|
||||
dsimp_config cfg(_cfg);
|
||||
try {
|
||||
type_context ctx = mk_type_context_for(s, cfg.m_md);
|
||||
defeq_can_state dcs = s.dcs();
|
||||
type_context ctx = mk_type_context_for(s, cfg.m_md);
|
||||
defeq_can_state dcs = s.dcs();
|
||||
list<name> to_unfold = to_list_name(u);
|
||||
simp_lemmas_for dlemmas;
|
||||
if (auto * dls = to_simp_lemmas(lemmas).find(get_eq_name()))
|
||||
dlemmas = *dls;
|
||||
dsimplify_fn F(ctx, dcs, dlemmas, cfg);
|
||||
dsimplify_fn F(ctx, dcs, dlemmas, to_unfold, cfg);
|
||||
expr new_e = F(to_expr(e));
|
||||
if (cfg.m_fail_if_unchanged && to_expr(e) == new_e) {
|
||||
return tactic::mk_exception("dsimplify tactic failed to simplify", s);
|
||||
|
|
|
|||
|
|
@ -21,8 +21,9 @@ structure dsimp_config :=
|
|||
(eta : bool := ff)
|
||||
(zeta : bool := ff)
|
||||
(beta : bool := tt)
|
||||
(proj : bool := tt) -- reduce projections
|
||||
(proj : bool := tt)
|
||||
(iota : bool := tt)
|
||||
(unfold_reducible := ff)
|
||||
(memoize := tt)
|
||||
*/
|
||||
struct dsimp_config {
|
||||
|
|
@ -36,6 +37,7 @@ struct dsimp_config {
|
|||
bool m_beta;
|
||||
bool m_proj;
|
||||
bool m_iota;
|
||||
bool m_unfold_reducible;
|
||||
bool m_memoize;
|
||||
dsimp_config();
|
||||
dsimp_config(vm_obj const & o);
|
||||
|
|
@ -69,15 +71,17 @@ public:
|
|||
|
||||
class dsimplify_fn : public dsimplify_core_fn {
|
||||
simp_lemmas_for m_simp_lemmas;
|
||||
name_set m_to_unfold;
|
||||
expr reduce(expr const & e);
|
||||
virtual optional<pair<expr, bool>> pre(expr const & e) override;
|
||||
virtual optional<pair<expr, bool>> post(expr const & e) override;
|
||||
public:
|
||||
dsimplify_fn(type_context & ctx, defeq_canonizer::state & s,
|
||||
simp_lemmas_for const & lemmas, dsimp_config const & cfg);
|
||||
simp_lemmas_for const & lemmas, list<name> const & to_unfold, dsimp_config const & cfg);
|
||||
};
|
||||
|
||||
expr reduce_beta_eta_proj_iota(type_context & ctx, expr e, bool beta, bool eta, bool proj, bool iota);
|
||||
optional<expr> unfold_step(type_context & ctx, expr const & e, name_set const & to_unfold, bool unfold_reducible);
|
||||
|
||||
void initialize_dsimplify();
|
||||
void finalize_dsimplify();
|
||||
|
|
|
|||
|
|
@ -41,5 +41,4 @@ simp_result join(type_context & tctx, name const & rel, simp_result const & r1,
|
|||
|
||||
simp_result finalize_eq(abstract_type_context & tctx, simp_result const & r);
|
||||
simp_result join_eq(abstract_type_context & tctx, simp_result const & r1, simp_result const & r2);
|
||||
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1050,31 +1050,9 @@ optional<pair<simp_result, bool>> simplify_fn::pre(expr const &, optional<expr>
|
|||
return no_ext_result();
|
||||
}
|
||||
|
||||
static optional<simp_result> to_opt_simp_result(optional<expr> const & e) {
|
||||
if (!e) return optional<simp_result>();
|
||||
return optional<simp_result>(*e);
|
||||
}
|
||||
|
||||
optional<simp_result> simplify_fn::unfold_step(expr const & e) {
|
||||
if (m_to_unfold.empty())
|
||||
return optional<simp_result>();
|
||||
if (!is_app(e) && !is_constant(e))
|
||||
return optional<simp_result>();
|
||||
expr const & fn = get_app_fn(e);
|
||||
if (!is_constant(fn) || !m_to_unfold.contains(const_name(fn)))
|
||||
return optional<simp_result>();
|
||||
type_context::transparency_scope scope(m_ctx, transparency_mode::Instances);
|
||||
optional<expr> new_e;
|
||||
if (is_projection(m_ctx.env(), const_name(fn))) {
|
||||
return to_opt_simp_result(m_ctx.reduce_projection(e));
|
||||
} else {
|
||||
return to_opt_simp_result(unfold_term(m_ctx.env(), e));
|
||||
}
|
||||
}
|
||||
|
||||
optional<pair<simp_result, bool>> simplify_fn::post(expr const & e, optional<expr> const &) {
|
||||
if (auto r = unfold_step(e))
|
||||
return to_ext_result(*r);
|
||||
if (auto r = unfold_step(m_ctx, e, m_to_unfold, false))
|
||||
return to_ext_result(simp_result(*r));
|
||||
simp_result r = rewrite(e);
|
||||
if (r.get_new() != e) {
|
||||
return to_ext_result(r);
|
||||
|
|
|
|||
|
|
@ -171,7 +171,6 @@ public:
|
|||
class simplify_fn : public simplify_ext_core_fn {
|
||||
protected:
|
||||
name_set m_to_unfold;
|
||||
optional<simp_result> unfold_step(expr const & e);
|
||||
virtual optional<pair<simp_result, bool>> pre(expr const & e, optional<expr> const & parent) override;
|
||||
virtual optional<pair<simp_result, bool>> post(expr const & e, optional<expr> const & parent) override;
|
||||
virtual optional<expr> prove(expr const & e) override;
|
||||
|
|
|
|||
|
|
@ -256,7 +256,7 @@ static expr dsimp(type_context & ctx, transparency_mode md, expr const & e) {
|
|||
cfg.m_canonize_instances = false;
|
||||
cfg.m_max_steps = 1000000; /* TODO(Leo): add parameter? */
|
||||
cfg.m_eta = true;
|
||||
return dsimplify_fn(ctx, dcs, simp_lemmas_for(), cfg)(e);
|
||||
return dsimplify_fn(ctx, dcs, simp_lemmas_for(), list<name>(), cfg)(e);
|
||||
}
|
||||
|
||||
struct mk_hinst_lemma_fn {
|
||||
|
|
|
|||
|
|
@ -207,7 +207,7 @@ static dsimplify_fn mk_dsimp(type_context & ctx, defeq_can_state & dcs, smt_pre_
|
|||
simp_lemmas_for eq_lemmas;
|
||||
if (auto r = cfg.m_simp_lemmas.find(get_eq_name()))
|
||||
eq_lemmas = *r;
|
||||
return dsimplify_fn(ctx, dcs, eq_lemmas, dcfg);
|
||||
return dsimplify_fn(ctx, dcs, eq_lemmas, list<name>(), dcfg);
|
||||
}
|
||||
|
||||
static simplify_fn mk_simp(type_context & ctx, defeq_can_state & dcs, smt_pre_config const & cfg) {
|
||||
|
|
|
|||
|
|
@ -165,7 +165,7 @@ vm_obj tactic_dunfold_expr(vm_obj const & _e, vm_obj const & m, vm_obj const & _
|
|||
}
|
||||
|
||||
void initialize_unfold_tactic() {
|
||||
DECLARE_VM_BUILTIN(name({"tactic", "unfold_projection"}), tactic_unfold_projection);
|
||||
DECLARE_VM_BUILTIN(name({"tactic", "unfold_proj"}), tactic_unfold_projection);
|
||||
DECLARE_VM_BUILTIN(name({"tactic", "dunfold_core"}), tactic_dunfold_core);
|
||||
DECLARE_VM_BUILTIN(name({"tactic", "dunfold_expr"}), tactic_dunfold_expr);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -6,10 +6,9 @@ rfl
|
|||
|
||||
example (a b : nat) : a = b → succ (succ a) = succ (b + 1) :=
|
||||
by do intro `Heq,
|
||||
t ← target,
|
||||
trace_state,
|
||||
s ← simp_lemmas.mk_default,
|
||||
t' ← s^.dsimplify t,
|
||||
t' ← target >>= s^.dsimplify,
|
||||
change t',
|
||||
trace "---- after change ----",
|
||||
trace_state,
|
||||
|
|
|
|||
|
|
@ -8,7 +8,7 @@ example (a b : nat) : a = b → succ (succ a) = succ (b + 1) :=
|
|||
by do intro `Heq,
|
||||
get_local `a >>= subst,
|
||||
trace_state,
|
||||
dsimp,
|
||||
dsimp_target,
|
||||
trace "---- after dsimp ----",
|
||||
trace_state,
|
||||
t ← target,
|
||||
|
|
|
|||
|
|
@ -9,6 +9,6 @@ example (n m : nat) (H : succ (succ n) = succ m) : true :=
|
|||
by do H ← get_local `H,
|
||||
t ← infer_type H,
|
||||
s ← simp_lemmas.mk_default,
|
||||
t' ← s^.dsimplify t,
|
||||
t' ← s^.dsimplify [] t,
|
||||
trace t',
|
||||
exact (expr.const `trivial [])
|
||||
|
|
|
|||
|
|
@ -10,7 +10,7 @@ axiom foo3 (n : nat) : n ≥ 0
|
|||
example (a b : nat) (H : f a (foo1 a) = f a (foo2 a)) : true :=
|
||||
by do
|
||||
s ← simp_lemmas.mk_default,
|
||||
e ← get_local `H >>= infer_type, s^.dsimplify e {fail_if_unchanged := ff} >>= trace,
|
||||
e ← get_local `H >>= infer_type, s^.dsimplify [] e {fail_if_unchanged := ff} >>= trace,
|
||||
constructor
|
||||
|
||||
constant x1 : nat -- update the environment to force defeq_canonize cache to be reset
|
||||
|
|
@ -18,7 +18,7 @@ constant x1 : nat -- update the environment to force defeq_canonize cache to be
|
|||
example (a b : nat) (H : f a (foo1 a) = f a (foo2 a)) : true :=
|
||||
by do
|
||||
s ← simp_lemmas.mk_default,
|
||||
e ← get_local `H >>= infer_type, s^.dsimplify e {fail_if_unchanged := ff} >>= trace,
|
||||
e ← get_local `H >>= infer_type, s^.dsimplify [] e {fail_if_unchanged := ff} >>= trace,
|
||||
constructor
|
||||
|
||||
constant x2 : nat -- update the environment to force defeq_canonize cache to be reset
|
||||
|
|
|
|||
|
|
@ -16,10 +16,10 @@ set_option pp.all true
|
|||
example (a b : nat) (H : (λ x : nat, @has_add.add nat (nat_has_add3 x) a b) = (λ x : nat, @has_add.add nat nat_has_add2 a x)) : true :=
|
||||
by do
|
||||
s ← simp_lemmas.mk_default,
|
||||
e ← get_local `H >>= infer_type, s^.dsimplify e {fail_if_unchanged := ff} >>= trace,
|
||||
e ← get_local `H >>= infer_type, s^.dsimplify [] e {fail_if_unchanged := ff} >>= trace,
|
||||
trace "---------",
|
||||
-- The following should work
|
||||
e ← get_local `H >>= infer_type,
|
||||
e ← s^.dsimplify e {fail_if_unchanged := ff},
|
||||
s^.dsimplify e {fail_if_unchanged := ff} >>= trace,
|
||||
e ← s^.dsimplify [] e {fail_if_unchanged := ff},
|
||||
s^.dsimplify [] e {fail_if_unchanged := ff} >>= trace,
|
||||
constructor
|
||||
|
|
|
|||
|
|
@ -2,6 +2,6 @@ open tactic
|
|||
|
||||
example (a b : nat) : ((a + 1, b).1) = a + 1 :=
|
||||
by do
|
||||
dsimp,
|
||||
dsimp_target,
|
||||
trace_state,
|
||||
reflexivity
|
||||
|
|
|
|||
|
|
@ -25,7 +25,7 @@ by do
|
|||
w ← get_local `w,
|
||||
cases w [`n', `hw, `tw],
|
||||
trace_state,
|
||||
dsimp,
|
||||
dsimp_target,
|
||||
trace_state,
|
||||
Heq1 ← intro1,
|
||||
Heq2 ← intro1,
|
||||
|
|
|
|||
14
tests/lean/run/dsimp_proj.lean
Normal file
14
tests/lean/run/dsimp_proj.lean
Normal file
|
|
@ -0,0 +1,14 @@
|
|||
example (a b : nat) : a + b = b + a :=
|
||||
begin
|
||||
dsimp [has_add.add],
|
||||
guard_target nat.add a b = nat.add b a,
|
||||
apply add_comm
|
||||
end
|
||||
|
||||
example (f g : nat → nat) : (f ∘ g) = (λ x, f (g x)) :=
|
||||
begin
|
||||
fail_if_success {dsimp},
|
||||
dsimp {unfold_reducible := tt},
|
||||
guard_target (λ x, f (g x)) = (λ x, f (g x)),
|
||||
refl
|
||||
end
|
||||
|
|
@ -2,6 +2,6 @@ open tactic
|
|||
|
||||
example {α : Type} (f : α → α → α) (a b : α) (H₁ : a = b) (H₂ : f b a = a) :
|
||||
let c := a in f c c = c :=
|
||||
by do dsimp,
|
||||
by do dsimp_target,
|
||||
e ← get_local `H₁, rewrite_target e {occs := occurrences.pos [1]},
|
||||
get_local `H₂ >>= exact
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue