From b05c4e09ed9bb406298063f794d87bf666ad2852 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 1 Jul 2017 10:25:34 -0700 Subject: [PATCH] feat(library/init/meta): add `memoize` field to `simp_config` and `dsimp_config` We use `memoize := ff` when implementing `conv.interactive.for` and `conv.interactive.find`. --- library/init/meta/converter/interactive.lean | 4 ++-- library/init/meta/simp_tactic.lean | 2 ++ src/library/tactic/dsimplify.cpp | 18 ++++++++++++------ src/library/tactic/dsimplify.h | 2 ++ src/library/tactic/simplify.cpp | 18 ++++++++++++------ src/library/tactic/simplify.h | 2 ++ .../interactive/info_tactic.lean.expected.out | 8 ++++---- tests/lean/run/conv_tac1.lean | 17 +++++++++++++++++ 8 files changed, 53 insertions(+), 18 deletions(-) diff --git a/library/init/meta/converter/interactive.lean b/library/init/meta/converter/interactive.lean index 2dbb0c958a..416c60115e 100644 --- a/library/init/meta/converter/interactive.lean +++ b/library/init/meta/converter/interactive.lean @@ -76,7 +76,7 @@ do (r, lhs, _) ← tactic.target_lhs_rhs, s ← simp_lemmas.mk_default, -- to be able to use congruence lemmas @[congr] (found, new_lhs, pr) ← tactic.ext_simplify_core ff {zeta := ff, beta := ff, single_pass := tt, eta := ff, - proj := ff, fail_if_unchaged := ff} s + proj := ff, fail_if_unchaged := ff, memoize := ff} s (λ u, return u) (λ found s r p e, do guard (not found), @@ -95,7 +95,7 @@ do (r, lhs, _) ← tactic.target_lhs_rhs, s ← simp_lemmas.mk_default, -- to be able to use congruence lemmas @[congr] (found, new_lhs, pr) ← tactic.ext_simplify_core 1 {zeta := ff, beta := ff, single_pass := tt, eta := ff, - proj := ff, fail_if_unchaged := ff} s + proj := ff, fail_if_unchaged := ff, memoize := ff} s (λ u, return u) (λ i s r p e, do matched ← (tactic.match_pattern_core reducible pat e >> return tt) <|> return ff, diff --git a/library/init/meta/simp_tactic.lean b/library/init/meta/simp_tactic.lean index 61c04b236b..317da792b7 100644 --- a/library/init/meta/simp_tactic.lean +++ b/library/init/meta/simp_tactic.lean @@ -71,6 +71,7 @@ structure dsimp_config := (single_pass : bool := ff) (fail_if_unchaged := tt) (eta := tt) +(memoize := tt) end tactic /-- (Definitional) Simplify the given expression using *only* reflexivity equality lemmas from the given set of lemmas. @@ -197,6 +198,7 @@ structure simp_config := (proj : bool := tt) -- reduce projections (single_pass : bool := ff) (fail_if_unchaged := tt) +(memoize := tt) meta constant simplify_core (c : simp_config) diff --git a/src/library/tactic/dsimplify.cpp b/src/library/tactic/dsimplify.cpp index 9269856fe5..ae6129cbd5 100644 --- a/src/library/tactic/dsimplify.cpp +++ b/src/library/tactic/dsimplify.cpp @@ -30,7 +30,8 @@ dsimp_config::dsimp_config(): m_canonize_instances(true), m_single_pass(false), m_fail_if_unchanged(true), - m_eta(false) { + m_eta(false), + m_memoize(true) { } dsimp_config::dsimp_config(vm_obj const & o) { m_md = to_transparency_mode(cfield(o, 0)); @@ -39,6 +40,7 @@ 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)); } #define lean_dsimp_trace(CTX, N, CODE) lean_trace(N, scope_trace_env _scope1(CTX.env(), CTX); CODE) @@ -151,14 +153,17 @@ expr dsimplify_core_fn::visit(expr const & e) { lean_trace_inc_depth("dsimplify"); lean_dsimp_trace(m_ctx, "dsimplify", tout() << e << "\n";); - auto it = m_cache.find(e); - if (it != m_cache.end()) - return it->second; + if (m_cfg.m_memoize) { + auto it = m_cache.find(e); + if (it != m_cache.end()) + return it->second; + } expr curr_e = e; if (auto p1 = pre(curr_e)) { if (!p1->second) { - m_cache.insert(mk_pair(e, p1->first)); + if (m_cfg.m_memoize) + m_cache.insert(mk_pair(e, p1->first)); return p1->first; } curr_e = p1->first; @@ -205,7 +210,8 @@ expr dsimplify_core_fn::visit(expr const & e) { break; } } - m_cache.insert(mk_pair(e, curr_e)); + if (m_cfg.m_memoize) + m_cache.insert(mk_pair(e, curr_e)); return curr_e; } diff --git a/src/library/tactic/dsimplify.h b/src/library/tactic/dsimplify.h index f5d632e5c3..3457c050e9 100644 --- a/src/library/tactic/dsimplify.h +++ b/src/library/tactic/dsimplify.h @@ -19,6 +19,7 @@ structure dsimp_config := (single_pass : bool := ff) (fail_if_unchaged := tt) (eta := ff) +(memoize := tt) */ struct dsimp_config { transparency_mode m_md; @@ -27,6 +28,7 @@ struct dsimp_config { bool m_single_pass; bool m_fail_if_unchanged; bool m_eta; + bool m_memoize; dsimp_config(); dsimp_config(vm_obj const & o); }; diff --git a/src/library/tactic/simplify.cpp b/src/library/tactic/simplify.cpp index a79cd1c8c2..e3ec0206e9 100644 --- a/src/library/tactic/simplify.cpp +++ b/src/library/tactic/simplify.cpp @@ -73,7 +73,8 @@ simp_config::simp_config(): m_eta(true), m_proj(true), m_single_pass(false), - m_fail_if_unchanged(true) { + m_fail_if_unchanged(true), + m_memoize(true) { } simp_config::simp_config(vm_obj const & obj) { @@ -89,6 +90,7 @@ simp_config::simp_config(vm_obj const & obj) { 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)); } /* ----------------------------------- @@ -640,14 +642,17 @@ simp_result simplify_core_fn::visit(expr const & e, optional const & paren lean_trace_inc_depth("simplify"); lean_simp_trace(m_ctx, "simplify", tout() << m_rel << ": " << e << "\n";); - auto it = m_cache.find(e); - if (it != m_cache.end()) - return it->second; + if (m_cfg.m_memoize) { + auto it = m_cache.find(e); + if (it != m_cache.end()) + return it->second; + } simp_result curr_result(e); if (auto r1 = pre(e, parent)) { if (!r1->second) { - m_cache.insert(mk_pair(e, r1->first)); + if (m_cfg.m_memoize) + m_cache.insert(mk_pair(e, r1->first)); return r1->first; } curr_result = r1->first; @@ -715,7 +720,8 @@ simp_result simplify_core_fn::visit(expr const & e, optional const & paren } } - m_cache.insert(mk_pair(e, curr_result)); + if (m_cfg.m_memoize) + m_cache.insert(mk_pair(e, curr_result)); return curr_result; } diff --git a/src/library/tactic/simplify.h b/src/library/tactic/simplify.h index 9ea176bb29..ba1f0f8ab2 100644 --- a/src/library/tactic/simplify.h +++ b/src/library/tactic/simplify.h @@ -27,6 +27,7 @@ structure simp_config := (proj : bool) (single_pass : bool) (fail_if_unchaged : bool) +(memoize : bool) */ struct simp_config { unsigned m_max_steps; @@ -41,6 +42,7 @@ struct simp_config { bool m_proj; bool m_single_pass; bool m_fail_if_unchanged; + bool m_memoize; simp_config(); simp_config(vm_obj const & o); }; diff --git a/tests/lean/interactive/info_tactic.lean.expected.out b/tests/lean/interactive/info_tactic.lean.expected.out index 2d3caf009a..841336c200 100644 --- a/tests/lean/interactive/info_tactic.lean.expected.out +++ b/tests/lean/interactive/info_tactic.lean.expected.out @@ -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?"],"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 {max_steps := 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_unchaged := tt} → 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?"],"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 {max_steps := 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_unchaged := tt} → 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?"],"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 {max_steps := 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_unchaged := tt} → 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?"],"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 {max_steps := 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_unchaged := tt} → 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?"],"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 {max_steps := 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_unchaged := tt, memoize := tt} → 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?"],"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 {max_steps := 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_unchaged := tt, memoize := tt} → 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?"],"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 {max_steps := 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_unchaged := tt, memoize := tt} → 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?"],"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 {max_steps := 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_unchaged := tt, memoize := tt} → tactic unit"},"response":"ok","seq_num":12} {"record":{"full-id":"tactic.get_env","source":,"tactic_params":[],"type":"tactic environment"},"response":"ok","seq_num":14} diff --git a/tests/lean/run/conv_tac1.lean b/tests/lean/run/conv_tac1.lean index 0f7c6987c3..a093690e67 100644 --- a/tests/lean/run/conv_tac1.lean +++ b/tests/lean/run/conv_tac1.lean @@ -114,3 +114,20 @@ begin simp } end + +example (x : nat) : f x x + f x x + f x x = f x x + x + x + x + x + 1 + 1 := +begin + conv { + -- execute `rw [f]` for 1st and 3rd occurrences of f-applications + for (f _ _) [1, 3] { rw [f] }, + guard_lhs (x + x + 1) + f x x + (x + x + 1) = f x x + x + x + x + x + 1 + 1, + simp + } +end + +example (x : nat) : f x x + f x x = f x x + x + x + 1 := +begin + conv in (f _ _) { rw [f] }, + guard_target (x + x + 1) + f x x = f x x + x + x + 1, + simp +end