diff --git a/doc/changes.md b/doc/changes.md index ce2b8f9d59..be3acda49f 100644 --- a/doc/changes.md +++ b/doc/changes.md @@ -27,6 +27,11 @@ master branch (aka work in progress branch) - `conv in (_ = _) { to_lhs, whnf }` replace the left-hand-side of the equality in target with its weak-head-normal-form. - `conv at h in (0 + _) { rw [zero_add] }` +* `simp` tactics in interactive mode have a new configuration parameter (`discharger : tactic unit`) + a tactic for discharging subgoals created by the simplifier. If the tactic fails, the simplifier + tries to discharge the subgoal by reducing it to `true`. + Example: `simp {discharger := assumption}`. + *Changes* * We now have two type classes for converting to string: `has_to_string` and `has_repr`. diff --git a/library/init/meta/converter/interactive.lean b/library/init/meta/converter/interactive.lean index 5962303648..244b1d81e7 100644 --- a/library/init/meta/converter/interactive.lean +++ b/library/init/meta/converter/interactive.lean @@ -109,10 +109,11 @@ do (r, lhs, _) ← tactic.target_lhs_rhs, update_lhs new_lhs pr meta def simp (no_dflt : parse only_flag) (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) - (ids : parse without_ident_list) (cfg : tactic.simp_config := {}) : conv unit := + (ids : parse without_ident_list) (cfg : tactic.simp_config_ext := {}) + : conv unit := do s ← tactic.mk_simp_set no_dflt attr_names hs ids, (r, lhs, rhs) ← tactic.target_lhs_rhs, - (new_lhs, pr) ← tactic.simplify s lhs cfg r, + (new_lhs, pr) ← tactic.simplify s lhs cfg.to_simp_config r cfg.discharger, update_lhs new_lhs pr, return () diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean index 7dd1c432e4..5e96cbb52d 100644 --- a/library/init/meta/interactive.lean +++ b/library/init/meta/interactive.lean @@ -653,6 +653,9 @@ do tactic.injections_with hs, try assumption end interactive +meta structure simp_config_ext extends simp_config := +(discharger : tactic unit := failed) + section mk_simp_set open expr @@ -704,34 +707,37 @@ end mk_simp_set namespace interactive open interactive interactive.types expr -private meta def simp_goal (cfg : simp_config) : simp_lemmas → tactic unit +private meta def simp_goal (cfg : simp_config) (discharger : tactic unit) : simp_lemmas → tactic unit | s := do - (new_target, pr) ← target >>= λ t, simplify s t cfg `eq, + (new_target, pr) ← target >>= λ t, simplify s t cfg `eq discharger, replace_target new_target pr -private meta def simp_hyp (cfg : simp_config) (s : simp_lemmas) (h_name : name) : tactic unit := +private meta def simp_hyp (cfg : simp_config) (discharger : tactic unit) (s : simp_lemmas) (h_name : name) : tactic unit := do h ← get_local h_name, h_type ← infer_type h, - (h_new_type, pr) ← simplify s h_type cfg `eq, + (h_new_type, pr) ← simplify s h_type cfg `eq discharger, replace_hyp h h_new_type pr, return () -private meta def simp_hyps (cfg : simp_config) : simp_lemmas → list name → tactic unit +private meta def simp_hyps (cfg : simp_config) (discharger : tactic unit) : simp_lemmas → list name → tactic unit | s [] := skip -| s (h::hs) := simp_hyp cfg s h >> simp_hyps s hs +| s (h::hs) := simp_hyp cfg discharger s h >> simp_hyps s hs -private meta def simp_core (cfg : simp_config) (no_dflt : bool) (ctx : list expr) (hs : list pexpr) (attr_names : list name) (ids : list name) (locat : loc) : tactic unit := +private meta def simp_core (cfg : simp_config) (discharger : tactic unit) + (no_dflt : bool) (ctx : list expr) (hs : list pexpr) (attr_names : list name) (ids : list name) + (locat : loc) : tactic unit := do s ← mk_simp_set no_dflt attr_names hs ids, s ← s.append ctx, match locat : _ → tactic unit with | loc.wildcard := + -- TODO(Leo): fix do ls ← local_context, let loc_names := ls.map expr.local_pp_name, revert_lst ls, simp_intro_aux cfg ff s ff loc_names, return () - | (loc.ns []) := simp_goal cfg s - | (loc.ns hs) := simp_hyps cfg s hs + | (loc.ns []) := simp_goal cfg discharger s + | (loc.ns hs) := simp_hyps cfg discharger s hs end, try tactic.triv, try (tactic.reflexivity reducible) @@ -756,9 +762,10 @@ It has many variants. - `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]`. -/ -meta def simp (no_dflt : parse only_flag) (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) (locat : parse location) - (cfg : simp_config := {}) : tactic unit := -simp_core cfg no_dflt [] hs attr_names ids locat +meta def simp (no_dflt : parse only_flag) (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) + (ids : parse without_ident_list) (locat : parse location) + (cfg : simp_config_ext := {}) : tactic unit := +simp_core cfg.to_simp_config cfg.discharger no_dflt [] hs attr_names ids locat /-- Simplify the whole context, and use simplified hypotheses to simplify other hypotheses. -/ meta def simp_all (no_dflt : parse only_flag) (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) @@ -774,12 +781,12 @@ do s ← mk_simp_set no_dflt attr_names hs ids, Similar to the `simp` tactic, but adds all applicable hypotheses as simplification rules. -/ meta def simp_using_hs (no_dflt : parse only_flag) (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) - (cfg : simp_config := {}) : tactic unit := + (cfg : simp_config_ext := {}) : tactic unit := do ctx ← collect_ctx_simps, - simp_core cfg no_dflt ctx hs attr_names ids (loc.ns []) + simp_core cfg.to_simp_config cfg.discharger no_dflt ctx hs attr_names ids (loc.ns []) meta def simph (no_dflt : parse only_flag) (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) - (cfg : simp_config := {}) : tactic unit := + (cfg : simp_config_ext := {}) : tactic unit := simp_using_hs no_dflt hs attr_names ids cfg meta def simp_intros (ids : parse ident_*) (no_dflt : parse only_flag) (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) diff --git a/library/init/meta/simp_tactic.lean b/library/init/meta/simp_tactic.lean index 26951cc94a..2cf2bb0eb0 100644 --- a/library/init/meta/simp_tactic.lean +++ b/library/init/meta/simp_tactic.lean @@ -199,7 +199,12 @@ structure simp_config := (fail_if_unchaged := tt) (memoize := tt) -meta constant simplify (s : simp_lemmas) (e : expr) (cfg : simp_config := {}) (r : name := `eq) : tactic (expr × expr) +/-- + `simplify s e cfg r prove` simplify `e` using `s` using bottom-up traversal. + `discharger` is a tactic for dischaging new subgoals created by the simplifier. + If it fails, the simplifier tries to discharge the subgoal by simplifying it to `true`. -/ +meta constant simplify (s : simp_lemmas) (e : expr) (cfg : simp_config := {}) (r : name := `eq) + (discharger : tactic unit := failed) : tactic (expr × expr) meta def simplify_goal (S : simp_lemmas) (cfg : simp_config := {}) : tactic unit := do t ← target, @@ -227,7 +232,7 @@ meta constant ext_simplify_core (s : simp_lemmas) /- Tactic for dischaging hypothesis in conditional rewriting rules. The argument 'α' is the current user state. -/ - (prove : α → tactic α) + (discharger : α → tactic α) /- (pre a S r s p e) is invoked before visiting the children of subterm 'e', 'r' is the simplification relation being used, 's' is the updated set of lemmas if 'contextual' is tt, 'p' is the "parent" expression (if there is one). diff --git a/library/init/meta/smt/interactive.lean b/library/init/meta/smt/interactive.lean index c1fbaebef2..32b06a8245 100644 --- a/library/init/meta/smt/interactive.lean +++ b/library/init/meta/smt/interactive.lean @@ -252,14 +252,17 @@ slift (tactic.interactive.induction p rec_name ids revert) open tactic /-- Simplify the target type of the main goal. -/ -meta def simp (no_dflt : parse only_flag) (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) (cfg : simp_config := {}) : smt_tactic unit := +meta def simp (no_dflt : parse only_flag) (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) + (cfg : simp_config_ext := {}) : smt_tactic unit := tactic.interactive.simp no_dflt hs attr_names ids (loc.ns []) cfg /-- Simplify the target type of the main goal using simplification lemmas and the current set of hypotheses. -/ -meta def simp_using_hs (no_dflt : parse only_flag) (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) (cfg : simp_config := {}) : smt_tactic unit := +meta def simp_using_hs (no_dflt : parse only_flag) (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) + (ids : parse without_ident_list) (cfg : simp_config_ext := {}) : smt_tactic unit := tactic.interactive.simp_using_hs no_dflt hs attr_names ids cfg -meta def simph (no_dflt : parse only_flag) (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) (cfg : simp_config := {}) : smt_tactic unit := +meta def simph (no_dflt : parse only_flag) (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) + (ids : parse without_ident_list) (cfg : simp_config_ext := {}) : smt_tactic unit := simp_using_hs no_dflt hs attr_names ids cfg meta def dsimp (no_dflt : parse only_flag) (es : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) : smt_tactic unit := diff --git a/src/library/tactic/simplify.cpp b/src/library/tactic/simplify.cpp index 2562343f6b..9c75a302c4 100644 --- a/src/library/tactic/simplify.cpp +++ b/src/library/tactic/simplify.cpp @@ -1156,20 +1156,55 @@ public: } }; +class tactic_simplify_fn : public simplify_fn { + tactic_state m_s; + vm_obj m_prove; + + optional prove_core(expr const & e) { + auto s = mk_tactic_state_for(m_ctx.env(), m_ctx.get_options(), m_s.decl_name(), m_ctx.lctx(), e); + vm_obj r_obj = invoke(m_prove, to_obj(s)); + optional s_new = tactic::is_success(r_obj); + if (!s_new || s_new->goals()) return none_expr(); + metavar_context mctx = s_new->mctx(); + expr result = mctx.instantiate_mvars(s_new->main()); + if (has_expr_metavar(result)) return none_expr(); + m_ctx.set_mctx(mctx); + return some_expr(result); + } + + virtual optional prove(expr const & e) override { + if (auto r = prove_core(e)) + return r; + else + return simplify_fn::prove(e); + } + +public: + tactic_simplify_fn(type_context & ctx, defeq_canonizer::state & dcs, simp_lemmas const & slss, + simp_config const & cfg, tactic_state const & s, vm_obj const & prove): + simplify_fn(ctx, dcs, slss, cfg), + m_s(s), + m_prove(prove) { + } +}; + /* meta constant simplify (s : simp_lemmas) (e : expr) (c : simp_config) - (r : name) : tactic (expr × expr) + (r : name) + (prove : tactic unit) + : tactic (expr × expr) */ -vm_obj tactic_simplify(vm_obj const & slss, vm_obj const & e, vm_obj const & c, vm_obj const & rel, vm_obj const & _s) { +vm_obj tactic_simplify(vm_obj const & slss, vm_obj const & e, vm_obj const & c, vm_obj const & rel, + vm_obj const & prove, vm_obj const & _s) { tactic_state const & s = tactic::to_state(_s); try { simp_config cfg(c); type_context ctx = mk_type_context_for(s, transparency_mode::Reducible); defeq_can_state dcs = s.dcs(); - simplify_fn simp(ctx, dcs, to_simp_lemmas(slss), cfg); + tactic_simplify_fn simp(ctx, dcs, to_simp_lemmas(slss), cfg, s, prove); simp_result result = simp(to_name(rel), to_expr(e)); if (!cfg.m_fail_if_unchanged || result.get_new() != to_expr(e)) { result = finalize(ctx, to_name(rel), result); diff --git a/tests/lean/interactive/info_tactic.lean.expected.out b/tests/lean/interactive/info_tactic.lean.expected.out index 3b60cce30c..de561fb772 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 := 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_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 := 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_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 := 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_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 := 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_unchaged := tt, memoize := 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_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_unchaged := 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_unchaged := 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_unchaged := 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_unchaged := 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} diff --git a/tests/lean/run/simp_subgoals.lean b/tests/lean/run/simp_subgoals.lean new file mode 100644 index 0000000000..5770461efa --- /dev/null +++ b/tests/lean/run/simp_subgoals.lean @@ -0,0 +1,22 @@ +axiom DivS (x : nat) : x ≠ 0 → x / x = 1 + +open tactic + +example (x : nat) (h : x ≠ 0) : x / x = 1 := +begin + simp[DivS, h] +end + +example (x : nat) (h : x ≠ 0) : x / x = 1 := +begin + fail_if_success {simp [DivS]}, + simp [DivS] {discharger := assumption} +end + +constant f : nat → nat → nat +axiom flemma : ∀ a b, b ≠ 0 → a ≠ 0 → f a b = 0 + +example (x : nat) (h : x ≠ 0) : f 1 x = 0 := +begin + simp [flemma] {discharger := trace "subgoal" >> trace_state >> (assumption <|> comp_val)} +end