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

feat(library/tactic/dsimplify): new configuration options for dsimp

Browse source 
TODO for `dsimp`:
- Add an option for reducing [reducible] definitions
- Add (to_unfold : list name) similar to the one in the `simp` tactic
This commit is contained in:
Leonardo de Moura 2017-07-02 17:58:47 -07:00
parent df091f5c34
commit 16711fcdba
20 changed files with 223 additions and 85 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
doc/changes.md
View file

@ -34,7 +34,10 @@ 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. Example: `simp [has_add.add]`.
* `simp` 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`, ...).
*Changes*
@ -56,6 +59,10 @@ For more details, see discussion [here](https://github.com/leanprover/lean/pull/
* All `dsimp` tactics fail if they did not change anything.
We can simulate the v3.2.0 using `dsimp {fail_if_unchaged := ff}` or `try dsimp`.
* `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`.
* 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}`.

2
library/data/hash_map.lean
View file

@ -445,7 +445,7 @@ structure hash_map (α : Type u) [decidable_eq α] (β : α → Type v) :=
def mk_hash_map {α : Type u} [decidable_eq α] {β : α → Type v} (hash_fn : α → nat) (nbuckets := 8) : hash_map α β :=
let n := if nbuckets = 0 then 8 else nbuckets in
let nz : n > 0 := by abstract {dsimp, cases nbuckets, {simp, tactic.comp_val}, simp [if_pos, nat.succ_ne_zero], apply nat.zero_lt_succ} in
let nz : n > 0 := by abstract { cases nbuckets, {simp, tactic.comp_val}, simp [if_pos, nat.succ_ne_zero], apply nat.zero_lt_succ} in
{ hash_fn := hash_fn,
size := 0,
nbuckets := ⟨n, nz⟩,

2
library/init/data/list/instances.lean
View file

@ -36,7 +36,7 @@ instance : monad list :=
id_map := begin
intros _ xs, induction xs with x xs ih,
{ refl },
{ dsimp at ih, dsimp, simph }
{ dsimp [function.comp] at ih, dsimp [function.comp], simph }
end,
pure_bind := by simp_intros,
bind_assoc := begin

16
library/init/data/nat/bitwise.lean
View file

@ -203,13 +203,15 @@ namespace nat
binary_rec z f (bit b n) = f b n (binary_rec z f n) :=
begin
rw [binary_rec.equations._eqn_1],
cases (by apply_instance : decidable (bit b n = 0)) with b0 b0; dsimp [dite],
{ generalize (binary_rec._main._pack._proof_2 (bit b n)) e,
rw [bodd_bit, div2_bit], intro e, refl },
{ generalize (binary_rec._main._pack._proof_1 (bit b n) b0) e,
have bf := bodd_bit b n, have n0 := div2_bit b n,
rw b0 at bf n0, simp at bf n0, rw [-bf, -n0, binary_rec_zero],
exact λe, h.symm },
cases (by apply_instance : decidable (bit b n = 0)) with b0 b0,
{rw [dif_neg],
generalize (binary_rec._main._pack._proof_2 (bit b n)) e,
rw [bodd_bit, div2_bit], intro e, refl, assumption},
{rw [dif_pos],
generalize (binary_rec._main._pack._proof_1 (bit b n) b0) e,
have bf := bodd_bit b n, have n0 := div2_bit b n,
rw b0 at bf n0, simp at bf n0, rw [-bf, -n0, binary_rec_zero],
exact λe, h.symm }
end
lemma bitwise_bit_aux {f : bool → bool → bool} (h : f ff ff = ff) :

2
library/init/data/set.lean
View file

@ -90,7 +90,7 @@ instance : functor set :=
end,
map_comp := begin
intros, apply funext, intro c,
dsimp [image, set_of],
dsimp [image, set_of, function.comp],
exact propext ⟨λ ⟨a, ⟨h₁, h₂⟩⟩, ⟨g a, ⟨⟨a, ⟨h₁, rfl⟩⟩, h₂⟩⟩,
λ ⟨b, ⟨⟨a, ⟨h₁, h₂⟩⟩, h₃⟩⟩, ⟨a, ⟨h₁, h₂.symm ▸ h₃⟩⟩⟩
end}

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

@ -69,6 +69,10 @@ structure dsimp_config :=
(single_pass : bool := ff)
(fail_if_unchanged := tt)
(eta := tt)
(zeta : bool := tt)
(beta : bool := tt)
(proj : bool := tt) -- reduce projections
(iota : bool := tt)
(memoize := tt)
end tactic
@ -195,6 +199,7 @@ structure simp_config :=
(beta : bool := tt)
(eta : bool := tt)
(proj : bool := tt) -- reduce projections
(iota : bool := tt)
(single_pass : bool := ff)
(fail_if_unchanged := tt)
(memoize := tt)

2
library/init/native/result.lean
View file

@ -49,7 +49,7 @@ section resultT
{pure := @resultT.pure M m E, bind := @resultT.and_then M m E,
id_map := begin
intros, cases x,
dsimp [resultT.and_then],
dsimp [resultT.and_then, function.comp],
have h : @resultT.and_then._match_1 _ m E α _ resultT.pure = pure,
{ apply funext, intro x,
cases x; simp [resultT.and_then, resultT.pure, resultT.and_then] },

99
src/library/tactic/dsimplify.cpp
View file

@ -24,6 +24,40 @@ Author: Leonardo de Moura
#endif
namespace lean {
expr reduce_beta_eta_proj_iota(type_context & ctx, expr e, bool beta, bool eta, bool proj, bool iota) {
bool p;
do {
p = false;
if (beta) {
expr new_e = head_beta_reduce(e);
if (!is_eqp(new_e, e)) {
e = new_e;
p = true;
}
}
if (proj) {
if (auto v = ctx.reduce_projection(e)) {
e = *v;
p = true;
}
}
if (eta) {
expr new_e = try_eta(e);
if (!is_eqp(new_e, e)) {
e = new_e;
p = true;
}
}
if (iota) {
if (auto v = ctx.reduce_recursor(e)) {
e = *v;
p = true;
}
}
} while (p);
return e;
}
dsimp_config::dsimp_config():
m_md(transparency_mode::Reducible),
m_max_steps(LEAN_DEFAULT_DSIMPLIFY_MAX_STEPS),
@ -31,6 +65,10 @@ dsimp_config::dsimp_config():
m_single_pass(false),
m_fail_if_unchanged(true),
m_eta(false),
m_zeta(false),
m_beta(true),
m_proj(true),
m_iota(true),
m_memoize(true) {
}
dsimp_config::dsimp_config(vm_obj const & o) {
@ -40,7 +78,11 @@ dsimp_config::dsimp_config(vm_obj const & o) {
m_single_pass = to_bool(cfield(o, 3));
m_fail_if_unchanged = to_bool(cfield(o, 4));
m_eta = to_bool(cfield(o, 5));
m_memoize = to_bool(cfield(o, 6));
m_zeta = to_bool(cfield(o, 6));
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));
}
#define lean_dsimp_trace(CTX, N, CODE) lean_trace(N, scope_trace_env _scope1(CTX.env(), CTX); CODE)
@ -82,25 +124,29 @@ expr dsimplify_core_fn::visit_binding(expr const & e) {
}
expr dsimplify_core_fn::visit_let(expr const & e) {
type_context::tmp_locals locals(m_ctx);
expr b = e;
bool modified = false;
while (is_let(b)) {
expr t = instantiate_rev(let_type(b), locals.size(), locals.data());
expr v = instantiate_rev(let_value(b), locals.size(), locals.data());
expr new_t = visit(t);
expr new_v = visit(v);
if (!is_eqp(t, new_t) || !is_eqp(v, new_v)) modified = true;
locals.push_let(let_name(b), new_t, new_v);
b = let_body(b);
if (m_cfg.m_zeta) {
return visit(instantiate(let_body(e), let_value(e)));
} else {
type_context::tmp_locals locals(m_ctx);
expr b = e;
bool modified = false;
while (is_let(b)) {
expr t = instantiate_rev(let_type(b), locals.size(), locals.data());
expr v = instantiate_rev(let_value(b), locals.size(), locals.data());
expr new_t = visit(t);
expr new_v = visit(v);
if (!is_eqp(t, new_t) || !is_eqp(v, new_v)) modified = true;
locals.push_let(let_name(b), new_t, new_v);
b = let_body(b);
}
b = instantiate_rev(b, locals.size(), locals.data());
expr new_b = visit(b);
if (!is_eqp(b, new_b)) modified = true;
if (modified)
return locals.mk_lambda(new_b);
else
return e;
}
b = instantiate_rev(b, locals.size(), locals.data());
expr new_b = visit(b);
if (!is_eqp(b, new_b)) modified = true;
if (modified)
return locals.mk_lambda(new_b);
else
return e;
}
expr dsimplify_core_fn::visit_app(expr const & e) {
@ -232,18 +278,15 @@ metavar_context const & dsimplify_core_fn::mctx() const {
return m_ctx.mctx();
}
expr dsimplify_fn::whnf(expr const & e) {
expr new_e = m_ctx.whnf(e);
if (m_cfg.m_eta)
new_e = try_eta(new_e);
return new_e;
expr dsimplify_fn::reduce(expr const & e) {
return reduce_beta_eta_proj_iota(m_ctx, e, m_cfg.m_beta, m_cfg.m_eta, m_cfg.m_proj, m_cfg.m_iota);
}
optional<pair<expr, bool>> dsimplify_fn::pre(expr const & e) {
type_context::transparency_scope s(m_ctx, m_cfg.m_md);
expr new_e = whnf(e);
expr new_e = reduce(e);
if (new_e != e) {
lean_dsimp_trace(m_ctx, "dsimplify", tout() << "whnf\n" << e << "\n==>\n" << new_e << "\n";);
lean_dsimp_trace(m_ctx, "dsimplify", tout() << "reduce\n" << e << "\n==>\n" << new_e << "\n";);
return optional<pair<expr, bool>>(new_e, true);
} else {
return optional<pair<expr, bool>>();
@ -254,9 +297,9 @@ optional<pair<expr, bool>> dsimplify_fn::post(expr const & e) {
expr curr_e;
{
type_context::transparency_scope s(m_ctx, m_cfg.m_md);
curr_e = whnf(e);
curr_e = reduce(e);
if (curr_e != e) {
lean_dsimp_trace(m_ctx, "dsimplify", tout() << "whnf\n" << e << "\n==>\n" << curr_e << "\n";);
lean_dsimp_trace(m_ctx, "dsimplify", tout() << "reduce\n" << e << "\n==>\n" << curr_e << "\n";);
}
}
while (true) {

16
src/library/tactic/dsimplify.h
View file

@ -17,8 +17,12 @@ structure dsimp_config :=
(canonize_instances : bool := tt)
(canonize_proofs : bool := ff)
(single_pass : bool := ff)
(fail_if_unchaged := tt)
(eta := ff)
(fail_if_unchaged : bool := tt)
(eta : bool := ff)
(zeta : bool := ff)
(beta : bool := tt)
(proj : bool := tt) -- reduce projections
(iota : bool := tt)
(memoize := tt)
*/
struct dsimp_config {
@ -28,6 +32,10 @@ struct dsimp_config {
bool m_single_pass;
bool m_fail_if_unchanged;
bool m_eta;
bool m_zeta;
bool m_beta;
bool m_proj;
bool m_iota;
bool m_memoize;
dsimp_config();
dsimp_config(vm_obj const & o);
@ -61,7 +69,7 @@ public:
class dsimplify_fn : public dsimplify_core_fn {
simp_lemmas_for m_simp_lemmas;
expr whnf(expr const & e);
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:
@ -69,6 +77,8 @@ public:
simp_lemmas_for const & lemmas, dsimp_config const & cfg);
};
expr reduce_beta_eta_proj_iota(type_context & ctx, expr e, bool beta, bool eta, bool proj, bool iota);
void initialize_dsimplify();
void finalize_dsimplify();
}

35
src/library/tactic/simplify.cpp
View file

@ -44,6 +44,7 @@ Author: Daniel Selsam, Leonardo de Moura
#include "library/tactic/app_builder_tactics.h"
#include "library/tactic/simp_lemmas.h"
#include "library/tactic/simplify.h"
#include "library/tactic/dsimplify.h"
#ifndef LEAN_DEFAULT_SIMPLIFY_MAX_STEPS
#define LEAN_DEFAULT_SIMPLIFY_MAX_STEPS 1000000
@ -73,6 +74,7 @@ simp_config::simp_config():
m_beta(false),
m_eta(true),
m_proj(true),
m_iota(true),
m_single_pass(false),
m_fail_if_unchanged(true),
m_memoize(true) {
@ -89,9 +91,10 @@ simp_config::simp_config(vm_obj const & obj) {
m_beta = to_bool(cfield(obj, 7));
m_eta = to_bool(cfield(obj, 8));
m_proj = to_bool(cfield(obj, 9));
m_single_pass = to_bool(cfield(obj, 10));
m_fail_if_unchanged = to_bool(cfield(obj, 11));
m_memoize = to_bool(cfield(obj, 12));
m_iota = to_bool(cfield(obj, 10));
m_single_pass = to_bool(cfield(obj, 11));
m_fail_if_unchanged = to_bool(cfield(obj, 12));
m_memoize = to_bool(cfield(obj, 13));
}
/* -----------------------------------
@ -736,31 +739,7 @@ simp_result simplify_core_fn::visit_fn(expr const & e) {
}
expr simplify_core_fn::reduce(expr e) {
bool p;
do {
p = false;
if (m_cfg.m_beta) {
expr new_e = head_beta_reduce(e);
if (!is_eqp(new_e, e)) {
e = new_e;
p = true;
}
}
if (m_cfg.m_proj) {
if (auto v = m_ctx.reduce_projection(e)) {
e = *v;
p = true;
}
}
if (m_cfg.m_eta) {
expr new_e = try_eta(e);
if (!is_eqp(new_e, e)) {
e = new_e;
p = true;
}
}
} while (p);
return e;
return reduce_beta_eta_proj_iota(m_ctx, e, m_cfg.m_beta, m_cfg.m_eta, m_cfg.m_proj, m_cfg.m_iota);
}
simp_result simplify_core_fn::reduce(simp_result r) {

2
src/library/tactic/simplify.h
View file

@ -25,6 +25,7 @@ structure simp_config :=
(beta : bool)
(eta : bool)
(proj : bool)
(iota : bool)
(single_pass : bool)
(fail_if_unchaged : bool)
(memoize : bool)
@ -40,6 +41,7 @@ struct simp_config {
bool m_beta;
bool m_eta;
bool m_proj;
bool m_iota;
bool m_single_pass;
bool m_fail_if_unchanged;
bool m_memoize;

1
src/library/tactic/unfold_tactic.cpp
View file

@ -96,6 +96,7 @@ public:
unfold_core_fn(type_context & ctx, defeq_canonizer::state & dcs, list<name> const & cs, dsimp_config const & cfg):
dsimplify_core_fn(ctx, dcs, cfg),
m_cs(to_name_set(cs)) {
m_cfg.m_zeta = false;
}
};

10
src/library/type_context.cpp
View file

@ -794,6 +794,16 @@ bool type_context::use_zeta() const {
return m_zeta;
}
optional<expr> type_context::reduce_recursor(expr const & e) {
if (auto r = norm_ext(e))
return r;
if (auto r = reduce_aux_recursor(e))
return r;
if (auto r = reduce_large_elim_recursor(e))
return r;
return none_expr();
}
/*
Apply beta-reduction, zeta-reduction (i.e., unfold let local-decls), iota-reduction,
unfold macros, expand let-expressions, expand assigned meta-variables.

1
src/library/type_context.h
View file

@ -406,6 +406,7 @@ public:
optional<expr> reduce_large_elim_recursor(expr const & e);
optional<expr> reduce_projection(expr const & e);
optional<expr> norm_ext(expr const & e) { return env().norm_ext()(e, *this); }
optional<expr> reduce_recursor(expr const & e);
/** Similar to whnf, but ignores transparency annotations, and use
the given predicate to decide whether a constant should be unfolded or not.

8
tests/lean/1467.lean
View file

@ -4,7 +4,7 @@ axiom H_f_g : ∀ n, f (g n) = n
example (m : ℕ) : h m = h m :=
begin
let n : ℕ := g m,
have H : f n = m := begin dsimp, rw H_f_g end,
have H : f n = m := begin rw H_f_g end,
subst H, -- Error here
end
@ -14,14 +14,14 @@ example (m : ℕ) : h m = h m :=
begin
let n : ℕ, -- add metavar
exact g m,
have H : f n = m := begin dsimp, rw H_f_g end,
have H : f n = m := begin rw H_f_g end,
subst H, -- Error here
end
example (m : ℕ) : h m = h m :=
begin
let n : ℕ := g m,
have H : f n = m := begin dsimp, rw H_f_g end,
have H : f n = m := begin rw H_f_g end,
subst m, -- Error here
end
@ -31,7 +31,7 @@ example (m : ℕ) : h m = h m :=
begin
let n : ℕ, -- add metavar
exact g m,
have H : f n = m := begin dsimp, rw H_f_g end,
have H : f n = m := begin rw H_f_g end,
subst m, -- Error here
end

4
tests/lean/hinst_lemmas1.lean.expected.out
View file

@ -1,3 +1 @@
{[foo1, patterns: {{?x_1 < ?x_2, ?x_0 < ?x_1}}],
[foo2, patterns: {{?x_1 < ?x_2, ?x_1 > ?x_0}}],
[foo3, patterns: {{?x_0 < ?x_1, ?x_1 < ?x_2 + ?x_2}}]}
{[foo2, patterns: {{?x_1 < ?x_2, ?x_1 > ?x_0}}], [foo3, patterns: {{?x_1 > ?x_0, ?x_1 < ?x_2 + ?x_2}}]}

8
tests/lean/interactive/info_tactic.lean.expected.out
View file

@ -1,7 +1,7 @@
{"msgs":[{"caption":"","file_name":"f","pos_col":2,"pos_line":5,"severity":"error","text":"simplify tactic failed to simplify\nstate:\n⊢ false"}],"response":"all_messages"}
{"message":"file invalidated","response":"ok","seq_num":0}
{"record":{"doc":"This tactic uses lemmas and hypotheses to simplify the main goal target or non-dependent hypotheses.\nIt has many variants.\n\n- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.\n\n- `simp [h_1, ..., h_n]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and the given `h_i`s.\n The `h_i`'s are terms. If a `h_i` is a definition `f`, then the equational lemmas associated with `f` are used.\n This is a convenient way to \"unfold\" `f`.\n\n- `simp only [h_1, ..., h_n]` is like `simp [h_1, ..., h_n]` but does not use `[simp]` lemmas\n\n- `simp without id_1 ... id_n` simplifies the main goal target using the lemmas tagged with the attribute `[simp]`,\n but removes the ones named `id_i`s.\n\n- `simp at h_1 ... h_n` simplifies the non dependent hypotheses `h_1 : T_1` ... `h_n : T : n`. The tactic fails if the target or another hypothesis depends on one of them.\n\n- `simp at *` simplifies all the hypotheses and the goal.\n\n- `simp with attr_1 ... attr_n` simplifies the main goal target using the lemmas tagged with any of the attributes `[attr_1]`, ..., `[attr_n]` or `[simp]`.","source":,"state":"⊢ false","tactic_params":["only?","[expr, ...]?","(with id*)?","(without id*)?","(at (* | id*))?","simp_config_ext?"],"text":"simp","type":"interactive.parse interactive.types.only_flag → interactive.parse interactive.types.opt_qexpr_list → interactive.parse interactive.types.with_ident_list → interactive.parse interactive.types.without_ident_list → interactive.parse interactive.types.location → opt_param simp_config_ext {to_simp_config := {max_steps := simp.default_max_steps, contextual := ff, lift_eq := tt, canonize_instances := tt, canonize_proofs := ff, use_axioms := tt, zeta := tt, beta := tt, eta := tt, proj := tt, single_pass := ff, fail_if_unchanged := tt, memoize := tt}, discharger := failed unit} → tactic unit"},"response":"ok","seq_num":6}
{"record":{"doc":"This tactic uses lemmas and hypotheses to simplify the main goal target or non-dependent hypotheses.\nIt has many variants.\n\n- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.\n\n- `simp [h_1, ..., h_n]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and the given `h_i`s.\n The `h_i`'s are terms. If a `h_i` is a definition `f`, then the equational lemmas associated with `f` are used.\n This is a convenient way to \"unfold\" `f`.\n\n- `simp only [h_1, ..., h_n]` is like `simp [h_1, ..., h_n]` but does not use `[simp]` lemmas\n\n- `simp without id_1 ... id_n` simplifies the main goal target using the lemmas tagged with the attribute `[simp]`,\n but removes the ones named `id_i`s.\n\n- `simp at h_1 ... h_n` simplifies the non dependent hypotheses `h_1 : T_1` ... `h_n : T : n`. The tactic fails if the target or another hypothesis depends on one of them.\n\n- `simp at *` simplifies all the hypotheses and the goal.\n\n- `simp with attr_1 ... attr_n` simplifies the main goal target using the lemmas tagged with any of the attributes `[attr_1]`, ..., `[attr_n]` or `[simp]`.","source":,"tactic_param_idx":0,"tactic_params":["only?","[expr, ...]?","(with id*)?","(without id*)?","(at (* | id*))?","simp_config_ext?"],"text":"simp","type":"interactive.parse interactive.types.only_flag → interactive.parse interactive.types.opt_qexpr_list → interactive.parse interactive.types.with_ident_list → interactive.parse interactive.types.without_ident_list → interactive.parse interactive.types.location → opt_param simp_config_ext {to_simp_config := {max_steps := simp.default_max_steps, contextual := ff, lift_eq := tt, canonize_instances := tt, canonize_proofs := ff, use_axioms := tt, zeta := tt, beta := tt, eta := tt, proj := tt, single_pass := ff, fail_if_unchanged := tt, memoize := tt}, discharger := failed unit} → tactic unit"},"response":"ok","seq_num":8}
{"record":{"doc":"This tactic uses lemmas and hypotheses to simplify the main goal target or non-dependent hypotheses.\nIt has many variants.\n\n- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.\n\n- `simp [h_1, ..., h_n]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and the given `h_i`s.\n The `h_i`'s are terms. If a `h_i` is a definition `f`, then the equational lemmas associated with `f` are used.\n This is a convenient way to \"unfold\" `f`.\n\n- `simp only [h_1, ..., h_n]` is like `simp [h_1, ..., h_n]` but does not use `[simp]` lemmas\n\n- `simp without id_1 ... id_n` simplifies the main goal target using the lemmas tagged with the attribute `[simp]`,\n but removes the ones named `id_i`s.\n\n- `simp at h_1 ... h_n` simplifies the non dependent hypotheses `h_1 : T_1` ... `h_n : T : n`. The tactic fails if the target or another hypothesis depends on one of them.\n\n- `simp at *` simplifies all the hypotheses and the goal.\n\n- `simp with attr_1 ... attr_n` simplifies the main goal target using the lemmas tagged with any of the attributes `[attr_1]`, ..., `[attr_n]` or `[simp]`.","source":,"tactic_param_idx":1,"tactic_params":["only?","[expr, ...]?","(with id*)?","(without id*)?","(at (* | id*))?","simp_config_ext?"],"text":"simp","type":"interactive.parse interactive.types.only_flag → interactive.parse interactive.types.opt_qexpr_list → interactive.parse interactive.types.with_ident_list → interactive.parse interactive.types.without_ident_list → interactive.parse interactive.types.location → opt_param simp_config_ext {to_simp_config := {max_steps := simp.default_max_steps, contextual := ff, lift_eq := tt, canonize_instances := tt, canonize_proofs := ff, use_axioms := tt, zeta := tt, beta := tt, eta := tt, proj := tt, single_pass := ff, fail_if_unchanged := tt, memoize := tt}, discharger := failed unit} → tactic unit"},"response":"ok","seq_num":10}
{"record":{"doc":"This tactic uses lemmas and hypotheses to simplify the main goal target or non-dependent hypotheses.\nIt has many variants.\n\n- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.\n\n- `simp [h_1, ..., h_n]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and the given `h_i`s.\n The `h_i`'s are terms. If a `h_i` is a definition `f`, then the equational lemmas associated with `f` are used.\n This is a convenient way to \"unfold\" `f`.\n\n- `simp only [h_1, ..., h_n]` is like `simp [h_1, ..., h_n]` but does not use `[simp]` lemmas\n\n- `simp without id_1 ... id_n` simplifies the main goal target using the lemmas tagged with the attribute `[simp]`,\n but removes the ones named `id_i`s.\n\n- `simp at h_1 ... h_n` simplifies the non dependent hypotheses `h_1 : T_1` ... `h_n : T : n`. The tactic fails if the target or another hypothesis depends on one of them.\n\n- `simp at *` simplifies all the hypotheses and the goal.\n\n- `simp with attr_1 ... attr_n` simplifies the main goal target using the lemmas tagged with any of the attributes `[attr_1]`, ..., `[attr_n]` or `[simp]`.","source":,"tactic_param_idx":2,"tactic_params":["only?","[expr, ...]?","(with id*)?","(without id*)?","(at (* | id*))?","simp_config_ext?"],"text":"simp","type":"interactive.parse interactive.types.only_flag → interactive.parse interactive.types.opt_qexpr_list → interactive.parse interactive.types.with_ident_list → interactive.parse interactive.types.without_ident_list → interactive.parse interactive.types.location → opt_param simp_config_ext {to_simp_config := {max_steps := simp.default_max_steps, contextual := ff, lift_eq := tt, canonize_instances := tt, canonize_proofs := ff, use_axioms := tt, zeta := tt, beta := tt, eta := tt, proj := tt, single_pass := ff, fail_if_unchanged := tt, memoize := tt}, discharger := failed unit} → tactic unit"},"response":"ok","seq_num":12}
{"record":{"doc":"This tactic uses lemmas and hypotheses to simplify the main goal target or non-dependent hypotheses.\nIt has many variants.\n\n- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.\n\n- `simp [h_1, ..., h_n]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and the given `h_i`s.\n The `h_i`'s are terms. If a `h_i` is a definition `f`, then the equational lemmas associated with `f` are used.\n This is a convenient way to \"unfold\" `f`.\n\n- `simp only [h_1, ..., h_n]` is like `simp [h_1, ..., h_n]` but does not use `[simp]` lemmas\n\n- `simp without id_1 ... id_n` simplifies the main goal target using the lemmas tagged with the attribute `[simp]`,\n but removes the ones named `id_i`s.\n\n- `simp at h_1 ... h_n` simplifies the non dependent hypotheses `h_1 : T_1` ... `h_n : T : n`. The tactic fails if the target or another hypothesis depends on one of them.\n\n- `simp at *` simplifies all the hypotheses and the goal.\n\n- `simp with attr_1 ... attr_n` simplifies the main goal target using the lemmas tagged with any of the attributes `[attr_1]`, ..., `[attr_n]` or `[simp]`.","source":,"state":"⊢ false","tactic_params":["only?","[expr, ...]?","(with id*)?","(without id*)?","(at (* | id*))?","simp_config_ext?"],"text":"simp","type":"interactive.parse interactive.types.only_flag → interactive.parse interactive.types.opt_qexpr_list → interactive.parse interactive.types.with_ident_list → interactive.parse interactive.types.without_ident_list → interactive.parse interactive.types.location → opt_param simp_config_ext {to_simp_config := {max_steps := simp.default_max_steps, contextual := ff, lift_eq := tt, canonize_instances := tt, canonize_proofs := ff, use_axioms := tt, zeta := tt, beta := tt, eta := tt, proj := tt, iota := tt, single_pass := ff, fail_if_unchanged := tt, memoize := tt}, discharger := failed unit} → tactic unit"},"response":"ok","seq_num":6}
{"record":{"doc":"This tactic uses lemmas and hypotheses to simplify the main goal target or non-dependent hypotheses.\nIt has many variants.\n\n- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.\n\n- `simp [h_1, ..., h_n]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and the given `h_i`s.\n The `h_i`'s are terms. If a `h_i` is a definition `f`, then the equational lemmas associated with `f` are used.\n This is a convenient way to \"unfold\" `f`.\n\n- `simp only [h_1, ..., h_n]` is like `simp [h_1, ..., h_n]` but does not use `[simp]` lemmas\n\n- `simp without id_1 ... id_n` simplifies the main goal target using the lemmas tagged with the attribute `[simp]`,\n but removes the ones named `id_i`s.\n\n- `simp at h_1 ... h_n` simplifies the non dependent hypotheses `h_1 : T_1` ... `h_n : T : n`. The tactic fails if the target or another hypothesis depends on one of them.\n\n- `simp at *` simplifies all the hypotheses and the goal.\n\n- `simp with attr_1 ... attr_n` simplifies the main goal target using the lemmas tagged with any of the attributes `[attr_1]`, ..., `[attr_n]` or `[simp]`.","source":,"tactic_param_idx":0,"tactic_params":["only?","[expr, ...]?","(with id*)?","(without id*)?","(at (* | id*))?","simp_config_ext?"],"text":"simp","type":"interactive.parse interactive.types.only_flag → interactive.parse interactive.types.opt_qexpr_list → interactive.parse interactive.types.with_ident_list → interactive.parse interactive.types.without_ident_list → interactive.parse interactive.types.location → opt_param simp_config_ext {to_simp_config := {max_steps := simp.default_max_steps, contextual := ff, lift_eq := tt, canonize_instances := tt, canonize_proofs := ff, use_axioms := tt, zeta := tt, beta := tt, eta := tt, proj := tt, iota := tt, single_pass := ff, fail_if_unchanged := tt, memoize := tt}, discharger := failed unit} → tactic unit"},"response":"ok","seq_num":8}
{"record":{"doc":"This tactic uses lemmas and hypotheses to simplify the main goal target or non-dependent hypotheses.\nIt has many variants.\n\n- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.\n\n- `simp [h_1, ..., h_n]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and the given `h_i`s.\n The `h_i`'s are terms. If a `h_i` is a definition `f`, then the equational lemmas associated with `f` are used.\n This is a convenient way to \"unfold\" `f`.\n\n- `simp only [h_1, ..., h_n]` is like `simp [h_1, ..., h_n]` but does not use `[simp]` lemmas\n\n- `simp without id_1 ... id_n` simplifies the main goal target using the lemmas tagged with the attribute `[simp]`,\n but removes the ones named `id_i`s.\n\n- `simp at h_1 ... h_n` simplifies the non dependent hypotheses `h_1 : T_1` ... `h_n : T : n`. The tactic fails if the target or another hypothesis depends on one of them.\n\n- `simp at *` simplifies all the hypotheses and the goal.\n\n- `simp with attr_1 ... attr_n` simplifies the main goal target using the lemmas tagged with any of the attributes `[attr_1]`, ..., `[attr_n]` or `[simp]`.","source":,"tactic_param_idx":1,"tactic_params":["only?","[expr, ...]?","(with id*)?","(without id*)?","(at (* | id*))?","simp_config_ext?"],"text":"simp","type":"interactive.parse interactive.types.only_flag → interactive.parse interactive.types.opt_qexpr_list → interactive.parse interactive.types.with_ident_list → interactive.parse interactive.types.without_ident_list → interactive.parse interactive.types.location → opt_param simp_config_ext {to_simp_config := {max_steps := simp.default_max_steps, contextual := ff, lift_eq := tt, canonize_instances := tt, canonize_proofs := ff, use_axioms := tt, zeta := tt, beta := tt, eta := tt, proj := tt, iota := tt, single_pass := ff, fail_if_unchanged := tt, memoize := tt}, discharger := failed unit} → tactic unit"},"response":"ok","seq_num":10}
{"record":{"doc":"This tactic uses lemmas and hypotheses to simplify the main goal target or non-dependent hypotheses.\nIt has many variants.\n\n- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.\n\n- `simp [h_1, ..., h_n]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and the given `h_i`s.\n The `h_i`'s are terms. If a `h_i` is a definition `f`, then the equational lemmas associated with `f` are used.\n This is a convenient way to \"unfold\" `f`.\n\n- `simp only [h_1, ..., h_n]` is like `simp [h_1, ..., h_n]` but does not use `[simp]` lemmas\n\n- `simp without id_1 ... id_n` simplifies the main goal target using the lemmas tagged with the attribute `[simp]`,\n but removes the ones named `id_i`s.\n\n- `simp at h_1 ... h_n` simplifies the non dependent hypotheses `h_1 : T_1` ... `h_n : T : n`. The tactic fails if the target or another hypothesis depends on one of them.\n\n- `simp at *` simplifies all the hypotheses and the goal.\n\n- `simp with attr_1 ... attr_n` simplifies the main goal target using the lemmas tagged with any of the attributes `[attr_1]`, ..., `[attr_n]` or `[simp]`.","source":,"tactic_param_idx":2,"tactic_params":["only?","[expr, ...]?","(with id*)?","(without id*)?","(at (* | id*))?","simp_config_ext?"],"text":"simp","type":"interactive.parse interactive.types.only_flag → interactive.parse interactive.types.opt_qexpr_list → interactive.parse interactive.types.with_ident_list → interactive.parse interactive.types.without_ident_list → interactive.parse interactive.types.location → opt_param simp_config_ext {to_simp_config := {max_steps := simp.default_max_steps, contextual := ff, lift_eq := tt, canonize_instances := tt, canonize_proofs := ff, use_axioms := tt, zeta := tt, beta := tt, eta := tt, proj := tt, iota := tt, single_pass := ff, fail_if_unchanged := tt, memoize := tt}, discharger := failed unit} → tactic unit"},"response":"ok","seq_num":12}
{"record":{"full-id":"tactic.get_env","source":,"tactic_params":[],"type":"tactic environment"},"response":"ok","seq_num":14}

80
tests/lean/run/dsimp_options.lean Normal file
View file

@ -0,0 +1,80 @@
example (b c : nat) : c = @bool.cases_on (λ _, nat) tt b c :=
begin
fail_if_success {dsimp {iota := ff}},
dsimp {iota := tt},
guard_target c = c,
reflexivity
end
example (b c : nat) : c = @bool.cases_on (λ _, nat) tt b c :=
begin
dsimp, -- iota is tt by default
guard_target c = c,
reflexivity
end
example (b c : nat) : c = (λ x : nat, x) c :=
begin
fail_if_success {dsimp {beta := ff}},
dsimp {beta := tt},
guard_target c = c,
reflexivity
end
example (b c : nat) : c = (λ x : nat, x) c :=
begin
dsimp, -- beta is tt by default
guard_target c = c,
reflexivity
end
example (b c : nat) : c = (b, c).2 :=
begin
fail_if_success {dsimp {proj := ff}},
dsimp {proj := tt},
guard_target c = c,
reflexivity
end
example (b c : nat) : c = (b, c).2 :=
begin
dsimp, -- projection reduction is true by default IF argument is a constructor
guard_target c = c,
reflexivity
end
example (f g : nat → nat) : f ∘ g = λ x, f (g x) :=
begin
fail_if_success {dsimp}, -- reducible definition (e.g., function.comp) are not unfolded by default
dsimp [(∘)],
guard_target (λ x, f (g x)) = λ x, f (g x),
reflexivity
end
example (f g : nat → nat) : f ∘ g = λ x, f (g x) :=
begin
dsimp [function.comp],
guard_target (λ x, f (g x)) = λ x, f (g x),
reflexivity
end
example (a : nat) : (let x := a in x) = a :=
begin
fail_if_success{dsimp {zeta := ff}},
dsimp {zeta := tt},
guard_target a = a,
reflexivity
end
example (a : nat) : (let x := a in x) = a :=
begin
dsimp, -- zeta is tt by default
guard_target a = a,
reflexivity
end
example (a b : nat) : a + b = b + a :=
begin
fail_if_success{dsimp}, -- will not unfold has_add.add applications
apply add_comm
end

4
tests/lean/run/u_eq_max_u_v.lean
View file

@ -23,7 +23,7 @@ attribute [simp] semigroup_morphism.multiplicative
( f: semigroup_morphism s t ) ( g: semigroup_morphism t u ) : semigroup_morphism s u :=
{
map := λ x, g (f x),
multiplicative := begin blast, simp end
multiplicative := begin intros, simp [coe_fn] end
}
@[reducible] definition semigroup_product { α β : Type u } ( s : semigroup α ) ( t: semigroup β ) : semigroup (α × β) := {
@ -45,7 +45,7 @@ definition semigroup_morphism_product
-- cf https://groups.google.com/d/msg/lean-user/bVs5FdjClp4/tfHiVjLIBAAJ
intros,
unfold has_mul.mul,
dsimp,
dsimp [coe_fn],
simp
end
}

2
tests/lean/run/using_smt1.lean
View file

@ -12,7 +12,7 @@ lemma ex3 (p q r : Prop) : p → q → ¬p → r :=
by using_smt intros
lemma ex4 (a b c : nat) : a > nat.zero → 0 < a :=
by using_smt intros
by simp [(>)]; using_smt intros
lemma ex5 (a b c d : nat) : a ≠ d → a = b ∧ b = c → a = c :=
by using_smt intros