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

feat(library/init/meta): allow users to specify tactic for discharging subgoals in the simp tactic family

Browse source 
@dselsam @Armael: this feature may be useful for you.
The doc/changes.md describes many other new features.
This commit is contained in:
Leonardo de Moura 2017-07-01 15:20:40 -07:00
parent 7c35fae9e3
commit 4604d7fd5a
8 changed files with 107 additions and 29 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
doc/changes.md
View file

@ -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`.

5
library/init/meta/converter/interactive.lean
View file

@ -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 ()

37
library/init/meta/interactive.lean
View file

@ -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)

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

@ -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).

9
library/init/meta/smt/interactive.lean
View file

@ -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 :=

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

@ -1156,20 +1156,55 @@ public:
}
};
class tactic_simplify_fn : public simplify_fn {
tactic_state m_s;
vm_obj m_prove;
optional<expr> 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<tactic_state> 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<expr> 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);

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

@ -1,7 +1,7 @@
{"msgs":[{"caption":"","file_name":"f","pos_col":2,"pos_line":5,"severity":"error","text":"simplify tactic failed to simplify\nstate:\n⊢ false"}],"response":"all_messages"}
{"message":"file invalidated","response":"ok","seq_num":0}
{"record":{"doc":"This tactic uses lemmas and hypotheses to simplify the main goal target or non-dependent hypotheses.\nIt has many variants.\n\n- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.\n\n- `simp [h_1, ..., h_n]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and the given `h_i`s.\n The `h_i`'s are terms. If a `h_i` is a definition `f`, then the equational lemmas associated with `f` are used.\n This is a convenient way to \"unfold\" `f`.\n\n- `simp only [h_1, ..., h_n]` is like `simp [h_1, ..., h_n]` but does not use `[simp]` lemmas\n\n- `simp without id_1 ... id_n` simplifies the main goal target using the lemmas tagged with the attribute `[simp]`,\n but removes the ones named `id_i`s.\n\n- `simp at h_1 ... h_n` simplifies the non dependent hypotheses `h_1 : T_1` ... `h_n : T : n`. The tactic fails if the target or another hypothesis depends on one of them.\n\n- `simp at *` simplifies all the hypotheses and the goal.\n\n- `simp with attr_1 ... attr_n` simplifies the main goal target using the lemmas tagged with any of the attributes `[attr_1]`, ..., `[attr_n]` or `[simp]`.","source":,"state":"⊢ false","tactic_params":["only?","[expr, ...]?","(with id*)?","(without id*)?","(at (* | id*))?","simp_config?"],"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}

22
tests/lean/run/simp_subgoals.lean Normal file
View file

@ -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