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

fix(library/tactic/simplify): missing projection reduction, add proj := tt to simp

Browse source
This commit is contained in:
Leonardo de Moura 2017-03-27 17:23:09 -07:00
parent 161879b1bf
commit eea46610ea
6 changed files with 87 additions and 24 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -195,6 +195,7 @@ structure simp_config :=
(use_axioms : bool := tt)
(zeta : bool := tt)
(beta : bool := tt)
(proj : bool := tt) -- reduce projections
meta constant simplify_core
(c : simp_config)

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

@ -69,7 +69,8 @@ simp_config::simp_config():
m_canonize_proofs(false),
m_use_axioms(false),
m_zeta(false),
m_beta(false) {
m_beta(false),
m_proj(true) {
}
simp_config::simp_config(vm_obj const & obj) {
@ -81,6 +82,7 @@ simp_config::simp_config(vm_obj const & obj) {
m_use_axioms = to_bool(cfield(obj, 5));
m_zeta = to_bool(cfield(obj, 6));
m_beta = to_bool(cfield(obj, 7));
m_proj = to_bool(cfield(obj, 8));
}
/* -----------------------------------
@ -681,7 +683,8 @@ simp_result simplify_core_fn::rewrite(expr const & e, simp_lemma const & sl) {
simp_result it_r = rewrite_core(it, sl);
if (it_r.get_new() == it)
return simp_result(e);
expr new_e = head_beta_reduce(mk_rev_app(it_r.get_new(), extra_args));
expr new_e = mk_rev_app(it_r.get_new(), extra_args);
new_e = reduce(new_e);
if (!it_r.has_proof())
return simp_result(new_e);
expr pr = it_r.get_proof();
@ -792,27 +795,54 @@ simp_result simplify_core_fn::visit_fn(expr const & e) {
return congr_funs(r_f, args);
}
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;
}
}
} while (p);
return e;
}
simp_result simplify_core_fn::reduce(simp_result r) {
r.update(reduce(r.get_new()));
return r;
}
simp_result simplify_core_fn::visit_app(expr const & _e) {
lean_assert(is_app(_e));
expr e = _e;
if (m_cfg.m_beta)
e = head_beta_reduce(e);
e = should_defeq_canonize() ? defeq_canonize_args_step(e) : e;
expr e = reduce(_e);
e = should_defeq_canonize() ? defeq_canonize_args_step(e) : e;
// (1) Try user-defined congruences
simp_result r_user = try_user_congrs(e);
if (r_user.has_proof()) {
if (m_rel == get_eq_name()) {
return join(r_user, visit_fn(r_user.get_new()));
return reduce(join(r_user, visit_fn(r_user.get_new())));
} else {
return r_user;
return reduce(r_user);
}
}
if (m_rel == get_eq_name()) {
// (2) Synthesize congruence lemma
optional<simp_result> r_args = try_auto_eq_congr(e);
if (r_args) return join(*r_args, visit_fn(r_args->get_new()));
if (r_args) {
return reduce(join(*r_args, visit_fn(r_args->get_new())));
}
// (3) Fall back on generic binary congruence
expr const & f = app_fn(e);
@ -821,11 +851,11 @@ simp_result simplify_core_fn::visit_app(expr const & _e) {
simp_result r_f = visit(f, some_expr(e));
if (is_dependent_fn(f)) {
if (r_f.has_proof()) return congr_fun(r_f, arg);
else return mk_app(r_f.get_new(), arg);
if (r_f.has_proof()) return reduce(congr_fun(r_f, arg));
else return reduce(mk_app(r_f.get_new(), arg));
} else {
simp_result r_arg = visit(arg, some_expr(e));
return congr_fun_arg(r_f, r_arg);
return reduce(congr_fun_arg(r_f, r_arg));
}
}
@ -1089,11 +1119,8 @@ static optional<pair<simp_result, bool>> no_ext_result() {
return optional<pair<simp_result, bool>>();
}
optional<pair<simp_result, bool>> simplify_fn::pre(expr const & e, optional<expr> const &) {
if (auto r = m_ctx.reduce_projection(e))
return to_ext_result(simp_result(*r));
else
return no_ext_result();
optional<pair<simp_result, bool>> simplify_fn::pre(expr const &, optional<expr> const &) {
return no_ext_result();
}
optional<pair<simp_result, bool>> simplify_fn::post(expr const & e, optional<expr> const &) {

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

@ -23,6 +23,7 @@ structure simp_config :=
(use_axioms : bool)
(zeta : bool)
(beta : bool)
(proj : bool)
*/
struct simp_config {
unsigned m_max_steps;
@ -33,6 +34,7 @@ struct simp_config {
bool m_use_axioms;
bool m_zeta;
bool m_beta;
bool m_proj;
/* The following option should be removed as soon as we
refactor the inductive compiler. */
bool m_use_matcher{true};
@ -126,6 +128,10 @@ protected:
simp_result simplify(expr const & e);
/* Apply conversion rules: beta, projection */
expr reduce(expr e);
simp_result reduce(simp_result r);
bool match(tmp_type_context & ctx, simp_lemma const & sl, expr const & t);
public:

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

@ -1,6 +1,6 @@
{"msgs":[{"caption":"","file_name":"f","pos_col":2,"pos_line":3,"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 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` simplifies the non dependent hypothesis `h : T`. The tactic fails if the target or another hypothesis depends on `h`.\n\n- `simp with attr` simplifies the main goal target using the lemmas tagged with the attribute `[attr]`.","source":,"state":"⊢ false","tactic_params":["[expr, ...]?","(with id*)?","(without id*)?","(at id*)?","tactic.simp_config?"],"text":"simp","type":"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 tactic.simp_config {max_steps := tactic.simp_config.max_steps._default, contextual := tactic.simp_config.contextual._default, lift_eq := tactic.simp_config.lift_eq._default, canonize_instances := tactic.simp_config.canonize_instances._default, canonize_proofs := tactic.simp_config.canonize_proofs._default, use_axioms := tactic.simp_config.use_axioms._default, zeta := tactic.simp_config.zeta._default, beta := tactic.simp_config.beta._default} → tactic unit"},"response":"ok","seq_num":4}
{"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 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` simplifies the non dependent hypothesis `h : T`. The tactic fails if the target or another hypothesis depends on `h`.\n\n- `simp with attr` simplifies the main goal target using the lemmas tagged with the attribute `[attr]`.","source":,"tactic_param_idx":0,"tactic_params":["[expr, ...]?","(with id*)?","(without id*)?","(at id*)?","tactic.simp_config?"],"text":"simp","type":"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 tactic.simp_config {max_steps := tactic.simp_config.max_steps._default, contextual := tactic.simp_config.contextual._default, lift_eq := tactic.simp_config.lift_eq._default, canonize_instances := tactic.simp_config.canonize_instances._default, canonize_proofs := tactic.simp_config.canonize_proofs._default, use_axioms := tactic.simp_config.use_axioms._default, zeta := tactic.simp_config.zeta._default, beta := tactic.simp_config.beta._default} → 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 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` simplifies the non dependent hypothesis `h : T`. The tactic fails if the target or another hypothesis depends on `h`.\n\n- `simp with attr` simplifies the main goal target using the lemmas tagged with the attribute `[attr]`.","source":,"tactic_param_idx":0,"tactic_params":["[expr, ...]?","(with id*)?","(without id*)?","(at id*)?","tactic.simp_config?"],"text":"simp","type":"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 tactic.simp_config {max_steps := tactic.simp_config.max_steps._default, contextual := tactic.simp_config.contextual._default, lift_eq := tactic.simp_config.lift_eq._default, canonize_instances := tactic.simp_config.canonize_instances._default, canonize_proofs := tactic.simp_config.canonize_proofs._default, use_axioms := tactic.simp_config.use_axioms._default, zeta := tactic.simp_config.zeta._default, beta := tactic.simp_config.beta._default} → 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 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` simplifies the non dependent hypothesis `h : T`. The tactic fails if the target or another hypothesis depends on `h`.\n\n- `simp with attr` simplifies the main goal target using the lemmas tagged with the attribute `[attr]`.","source":,"tactic_param_idx":1,"tactic_params":["[expr, ...]?","(with id*)?","(without id*)?","(at id*)?","tactic.simp_config?"],"text":"simp","type":"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 tactic.simp_config {max_steps := tactic.simp_config.max_steps._default, contextual := tactic.simp_config.contextual._default, lift_eq := tactic.simp_config.lift_eq._default, canonize_instances := tactic.simp_config.canonize_instances._default, canonize_proofs := tactic.simp_config.canonize_proofs._default, use_axioms := tactic.simp_config.use_axioms._default, zeta := tactic.simp_config.zeta._default, beta := tactic.simp_config.beta._default} → 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 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` simplifies the non dependent hypothesis `h : T`. The tactic fails if the target or another hypothesis depends on `h`.\n\n- `simp with attr` simplifies the main goal target using the lemmas tagged with the attribute `[attr]`.","source":,"state":"⊢ false","tactic_params":["[expr, ...]?","(with id*)?","(without id*)?","(at id*)?","tactic.simp_config?"],"text":"simp","type":"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 tactic.simp_config {max_steps := tactic.simp_config.max_steps._default, contextual := tactic.simp_config.contextual._default, lift_eq := tactic.simp_config.lift_eq._default, canonize_instances := tactic.simp_config.canonize_instances._default, canonize_proofs := tactic.simp_config.canonize_proofs._default, use_axioms := tactic.simp_config.use_axioms._default, zeta := tactic.simp_config.zeta._default, beta := tactic.simp_config.beta._default, proj := tactic.simp_config.proj._default} → tactic unit"},"response":"ok","seq_num":4}
{"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 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` simplifies the non dependent hypothesis `h : T`. The tactic fails if the target or another hypothesis depends on `h`.\n\n- `simp with attr` simplifies the main goal target using the lemmas tagged with the attribute `[attr]`.","source":,"tactic_param_idx":0,"tactic_params":["[expr, ...]?","(with id*)?","(without id*)?","(at id*)?","tactic.simp_config?"],"text":"simp","type":"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 tactic.simp_config {max_steps := tactic.simp_config.max_steps._default, contextual := tactic.simp_config.contextual._default, lift_eq := tactic.simp_config.lift_eq._default, canonize_instances := tactic.simp_config.canonize_instances._default, canonize_proofs := tactic.simp_config.canonize_proofs._default, use_axioms := tactic.simp_config.use_axioms._default, zeta := tactic.simp_config.zeta._default, beta := tactic.simp_config.beta._default, proj := tactic.simp_config.proj._default} → 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 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` simplifies the non dependent hypothesis `h : T`. The tactic fails if the target or another hypothesis depends on `h`.\n\n- `simp with attr` simplifies the main goal target using the lemmas tagged with the attribute `[attr]`.","source":,"tactic_param_idx":0,"tactic_params":["[expr, ...]?","(with id*)?","(without id*)?","(at id*)?","tactic.simp_config?"],"text":"simp","type":"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 tactic.simp_config {max_steps := tactic.simp_config.max_steps._default, contextual := tactic.simp_config.contextual._default, lift_eq := tactic.simp_config.lift_eq._default, canonize_instances := tactic.simp_config.canonize_instances._default, canonize_proofs := tactic.simp_config.canonize_proofs._default, use_axioms := tactic.simp_config.use_axioms._default, zeta := tactic.simp_config.zeta._default, beta := tactic.simp_config.beta._default, proj := tactic.simp_config.proj._default} → 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 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` simplifies the non dependent hypothesis `h : T`. The tactic fails if the target or another hypothesis depends on `h`.\n\n- `simp with attr` simplifies the main goal target using the lemmas tagged with the attribute `[attr]`.","source":,"tactic_param_idx":1,"tactic_params":["[expr, ...]?","(with id*)?","(without id*)?","(at id*)?","tactic.simp_config?"],"text":"simp","type":"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 tactic.simp_config {max_steps := tactic.simp_config.max_steps._default, contextual := tactic.simp_config.contextual._default, lift_eq := tactic.simp_config.lift_eq._default, canonize_instances := tactic.simp_config.canonize_instances._default, canonize_proofs := tactic.simp_config.canonize_proofs._default, use_axioms := tactic.simp_config.use_axioms._default, zeta := tactic.simp_config.zeta._default, beta := tactic.simp_config.beta._default, proj := tactic.simp_config.proj._default} → tactic unit"},"response":"ok","seq_num":10}

31
tests/lean/run/simp_proj.lean Normal file
View file

@ -0,0 +1,31 @@
def f (a : nat) := (a, 0)
example (a b : nat) (h : a = b) : (f a).1 = b :=
begin
simp [f],
guard_target a = b,
exact h
end
example (a b : nat) (h : a = b) : (f a).1 = b :=
begin
simp [f] {proj := ff},
guard_target (a, 0)^.1 = b,
exact h
end
def g (a : nat) := (λ x, x) a
example (a b : nat) (h : a = b) : g a = b :=
begin
simp [g],
guard_target a = b,
exact h
end
example (a b : nat) (h : a = b) : g a = b :=
begin
simp [g] {beta := ff},
guard_target (λ x, x) a = b,
exact h
end

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

@ -30,9 +30,7 @@ instance semigroup_morphism_to_map { α β : Type u } { s : semigroup α } { t:
mul := λ p q, (p^.fst * q^.fst, p^.snd * q^.snd),
mul_assoc := begin
intros,
simp [@mul.equations._eqn_1 (α × β)],
dsimp,
simp
simp [@mul.equations._eqn_1 (α × β)]
end
}