From eea46610eac0f012c8e62fc99343a9c72ec80b38 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 27 Mar 2017 17:23:09 -0700 Subject: [PATCH] fix(library/tactic/simplify): missing projection reduction, add `proj := tt` to simp --- library/init/meta/simp_tactic.lean | 1 + src/library/tactic/simplify.cpp | 61 +++++++++++++------ src/library/tactic/simplify.h | 6 ++ .../interactive/info_tactic.lean.expected.out | 8 +-- tests/lean/run/simp_proj.lean | 31 ++++++++++ tests/lean/run/u_eq_max_u_v.lean | 4 +- 6 files changed, 87 insertions(+), 24 deletions(-) create mode 100644 tests/lean/run/simp_proj.lean diff --git a/library/init/meta/simp_tactic.lean b/library/init/meta/simp_tactic.lean index 442222de61..5de76f0507 100644 --- a/library/init/meta/simp_tactic.lean +++ b/library/init/meta/simp_tactic.lean @@ -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) diff --git a/src/library/tactic/simplify.cpp b/src/library/tactic/simplify.cpp index 9537089411..51a95e93cb 100644 --- a/src/library/tactic/simplify.cpp +++ b/src/library/tactic/simplify.cpp @@ -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 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> no_ext_result() { return optional>(); } -optional> simplify_fn::pre(expr const & e, optional const &) { - if (auto r = m_ctx.reduce_projection(e)) - return to_ext_result(simp_result(*r)); - else - return no_ext_result(); +optional> simplify_fn::pre(expr const &, optional const &) { + return no_ext_result(); } optional> simplify_fn::post(expr const & e, optional const &) { diff --git a/src/library/tactic/simplify.h b/src/library/tactic/simplify.h index 425e45764e..3ada915fa2 100644 --- a/src/library/tactic/simplify.h +++ b/src/library/tactic/simplify.h @@ -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: diff --git a/tests/lean/interactive/info_tactic.lean.expected.out b/tests/lean/interactive/info_tactic.lean.expected.out index def6e8494e..9dd97a2a0f 100644 --- a/tests/lean/interactive/info_tactic.lean.expected.out +++ b/tests/lean/interactive/info_tactic.lean.expected.out @@ -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} diff --git a/tests/lean/run/simp_proj.lean b/tests/lean/run/simp_proj.lean new file mode 100644 index 0000000000..a6ae0af56b --- /dev/null +++ b/tests/lean/run/simp_proj.lean @@ -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 diff --git a/tests/lean/run/u_eq_max_u_v.lean b/tests/lean/run/u_eq_max_u_v.lean index d6863b8a5c..7cb20d7105 100644 --- a/tests/lean/run/u_eq_max_u_v.lean +++ b/tests/lean/run/u_eq_max_u_v.lean @@ -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 }