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

feat(library/init/meta/interactive): simp without foo ==> simp [-foo]

Browse source 
This commit also adds "exception" validation.
A bad "exception" was being silently ignored.
We can also exclude hypotheses. Example: `simp [*, -h]`
This commit is contained in:
Leonardo de Moura 2017-07-03 16:51:56 -07:00
parent 76799db032
commit e24f3341d4
12 changed files with 143 additions and 58 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
doc/changes.md
View file

@ -77,6 +77,10 @@ For more details, see discussion [here](https://github.com/leanprover/lean/pull/
* Deleted `simph` and `simp_using_hs` tactics. We should use `simp [*]` instead.
* Use `simp [-h]` and `dsimp [-h]` instead of `simp without h` and `dsimp without h`.
Moreover, `simp [*, -h]` if `h` is a hypothesis, we are adding all hypotheses but `h`
as additional simplification lemmas.
*API name changes*
* `tactic.dsimp` and `tactic.dsimp_core` => `tactic.dsimp_target`

6
library/data/hash_map.lean
View file

@ -270,7 +270,7 @@ section
have array.read bkts' bidx = f L, from
show ite (bidx = bidx) _ _ = _, by rw if_pos rfl,
begin
simp[array.iterate_aux] without add_comm,
simp[array.iterate_aux, -add_comm],
rw -(show bidx = ⟨bidx.1, h⟩, from fin.eq_of_veq rfl),
refine ⟨array.iterate_aux bkts (λ_ bkt r, r ++ bkt) bidx.1 (le_of_lt h) [] ++ u, w, _⟩,
rw -valid.modify_aux1 _ _ (le_refl _),
@ -312,7 +312,7 @@ section
have array.read bkts' bidx = f L, from
show ite (bidx = bidx) _ _ = _, by rw if_pos rfl,
begin
simp[array.iterate_aux] without add_comm,
simp[array.iterate_aux, -add_comm],
rw [-(show bidx = ⟨bidx.1, h⟩, from fin.eq_of_veq rfl),
-valid.modify_aux1 _ _ (le_refl _),
this, hfl, hl],
@ -365,7 +365,7 @@ theorem valid.replace_aux (a : α) (b : β a) : Π (l : list (Σ a, β a)), a
| [] Hc := false.elim Hc
| (⟨a', b'⟩::t) Hc := begin
simp at Hc,
simp [replace_aux] without and.comm,
simp [replace_aux, -and.comm],
exact match (by apply_instance : decidable (a' = a)) with
| is_true e := match a', b', e with ._, b', rfl := ⟨[], t, b', rfl, rfl, by simp⟩ end
| is_false ne :=

2
library/init/data/list/lemmas.lean
View file

@ -110,7 +110,7 @@ by induction l; intros; contradiction
lemma length_remove_nth : ∀ (l : list α) (i : ℕ), i < length l → length (remove_nth l i) = length l - 1
| [] _ h := rfl
| (x::xs) 0 h := by simp [remove_nth] without add_comm
| (x::xs) 0 h := by simp [remove_nth, -add_comm]
| (x::xs) (i+1) h := have i < length xs, from lt_of_succ_lt_succ h,
by dsimp [remove_nth]; rw [length_remove_nth xs i this, nat.sub_add_cancel (lt_of_le_of_lt (nat.zero_le _) this)]; refl

2
library/init/data/nat/lemmas.lean
View file

@ -1163,7 +1163,7 @@ by rw [div_eq_sub_div H (nat.le_add_left _ _), nat.add_sub_cancel]
by rw [add_comm, add_div_right x H]
@[simp] theorem mul_div_right (n : ℕ) {m : ℕ} (H : m > 0) : m * n / m = n :=
by {induction n; simp [*, mul_succ] without mul_comm}
by {induction n; simp [*, mul_succ, -mul_comm]}
@[simp] theorem mul_div_left (m : ℕ) {n : ℕ} (H : n > 0) : m * n / n = m :=
by rw [mul_comm, mul_div_right _ H]

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

@ -40,8 +40,8 @@ meta def whnf : conv unit :=
conv.whnf
meta def dsimp (no_dflt : parse only_flag) (es : parse tactic.simp_arg_list) (attr_names : parse with_ident_list)
(ids : parse without_ident_list) (cfg : tactic.dsimp_config := {}) : conv unit :=
do (s, u) ← tactic.mk_simp_set no_dflt attr_names es ids,
(cfg : tactic.dsimp_config := {}) : conv unit :=
do (s, u) ← tactic.mk_simp_set no_dflt attr_names es,
conv.dsimp (some s) u cfg
meta def trace_lhs : conv unit :=
@ -109,9 +109,9 @@ do (r, lhs, _) ← tactic.target_lhs_rhs,
update_lhs new_lhs pr
meta def simp (no_dflt : parse only_flag) (hs : parse tactic.simp_arg_list) (attr_names : parse with_ident_list)
(ids : parse without_ident_list) (cfg : tactic.simp_config_ext := {})
(cfg : tactic.simp_config_ext := {})
: conv unit :=
do (s, u) ← tactic.mk_simp_set no_dflt attr_names hs ids,
do (s, u) ← tactic.mk_simp_set no_dflt attr_names hs,
(r, lhs, rhs) ← tactic.target_lhs_rhs,
(new_lhs, pr) ← tactic.simplify s u lhs cfg.to_simp_config r cfg.discharger,
update_lhs new_lhs pr,

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

@ -661,27 +661,46 @@ open expr interactive.types
meta inductive simp_arg_type : Type
| all_hyps : simp_arg_type
| except : name → simp_arg_type
| expr : pexpr → simp_arg_type
meta instance : has_reflect simp_arg_type
| simp_arg_type.all_hyps := `(_)
| (simp_arg_type.expr _) := `(_)
| simp_arg_type.all_hyps := `(_)
| (simp_arg_type.except _) := `(_)
| (simp_arg_type.expr _) := `(_)
meta def simp_arg : parser simp_arg_type :=
(tk "*" *> return simp_arg_type.all_hyps) <|> (simp_arg_type.expr <$> texpr)
(tk "*" *> return simp_arg_type.all_hyps) <|> (tk "-" *> simp_arg_type.except <$> ident) <|> (simp_arg_type.expr <$> texpr)
meta def simp_arg_list : parser (list simp_arg_type) :=
list_of simp_arg <|> return []
meta def decode_simp_arg_list (hs : list simp_arg_type) : list pexpr × bool :=
let r : list pexpr × bool := hs.foldl
(λ ⟨es, all⟩ h,
match h with
| simp_arg_type.all_hyps := (es, tt)
| simp_arg_type.expr e := (e::es, all)
end)
([], ff) in
(r.1.reverse, r.2)
private meta def resolve_exception_ids (all_hyps : bool) : list name → list name → list name → tactic (list name × list name)
| [] gex hex := return (gex.reverse, hex.reverse)
| (id::ids) gex hex := do
p ← resolve_name id,
let e := p.erase_annotations.get_app_fn.erase_annotations,
match e with
| const n _ := resolve_exception_ids ids (n::gex) hex
| local_const n _ _ _ := when (not all_hyps) (fail $ sformat! "invalid local exception {id}, '*' was not used") >>
resolve_exception_ids ids gex (n::hex)
| _ := fail $ sformat! "invalid exception {id}, unknown identifier"
end
/- Return (hs, gex, hex, all) -/
meta def decode_simp_arg_list (hs : list simp_arg_type) : tactic $ list pexpr × list name × list name × bool :=
do
let (hs, ex, all) := hs.foldl
(λ r h,
match r, h with
| (es, ex, all), simp_arg_type.all_hyps := (es, ex, tt)
| (es, ex, all), simp_arg_type.except id := (es, id::ex, all)
| (es, ex, all), simp_arg_type.expr e := (e::es, ex, all)
end)
([], [], ff),
(gex, hex) ← resolve_exception_ids all ex [] [],
return (hs.reverse, gex, hex, all)
private meta def add_simps : simp_lemmas → list name → tactic simp_lemmas
| s [] := return s
@ -721,14 +740,18 @@ private meta def simp_lemmas.append_pexprs : simp_lemmas → list name → list
| s u [] := return (s, u)
| s u (l::ls) := do (s, u) ← simp_lemmas.add_pexpr s u l, simp_lemmas.append_pexprs s u ls
meta def mk_simp_set (no_dflt : bool) (attr_names : list name) (hs : list simp_arg_type) (ex : list name) : tactic (simp_lemmas × list name) :=
do let (hs, add_hyps) := decode_simp_arg_list hs,
meta def mk_simp_set (no_dflt : bool) (attr_names : list name) (hs : list simp_arg_type) : tactic (simp_lemmas × list name) :=
do (hs, gex, hex, add_hyps) ← decode_simp_arg_list hs,
s ← join_user_simp_lemmas no_dflt attr_names,
(s, u) ← simp_lemmas.append_pexprs s [] hs,
s ← if add_hyps then collect_ctx_simps >>= s.append else return s,
s ← if add_hyps then do
ctx ← collect_ctx_simps,
let ctx := ctx.filter (λ h, h.local_uniq_name ∉ hex), -- remove local exceptions
s.append ctx
else return s,
-- add equational lemmas, if any
ex ← ex.mfor (λ n, list.cons n <$> get_eqn_lemmas_for tt n),
return (simp_lemmas.erase s $ ex.join, u)
gex ← gex.mfor (λ n, list.cons n <$> get_eqn_lemmas_for tt n),
return (simp_lemmas.erase s $ gex.join, u)
end mk_simp_set
@ -740,9 +763,9 @@ private meta def simp_hyps (cfg : simp_config) (discharger : tactic unit) (s : s
| (h::hs) := do h ← get_local h, simp_hyp s u h cfg discharger, simp_hyps hs
meta def simp_core (cfg : simp_config) (discharger : tactic unit)
(no_dflt : bool) (hs : list simp_arg_type) (attr_names : list name) (ids : list name)
(no_dflt : bool) (hs : list simp_arg_type) (attr_names : list name)
(locat : loc) : tactic unit :=
do (s, u) ← mk_simp_set no_dflt attr_names hs ids,
do (s, u) ← mk_simp_set no_dflt attr_names hs,
match locat : _ → tactic unit with
| loc.wildcard :=
do hs ← non_dep_prop_hyps,
@ -772,9 +795,11 @@ It has many variants.
The `h_i`'s are terms. If a `h_i` is a definition `f`, then the equational lemmas associated with `f` are used.
This is a convenient way to "unfold" `f`.
- `simp [*]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and all hypotheses.
- `simp only [h_1, ..., h_n]` is like `simp [h_1, ..., h_n]` but does not use `[simp]` lemmas
- `simp without id_1 ... id_n` simplifies the main goal target using the lemmas tagged with the attribute `[simp]`,
- `simp [-id_1, ... -id_n]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]`,
but removes the ones named `id_i`s.
- `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.
@ -784,20 +809,23 @@ 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 simp_arg_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
(locat : parse location) (cfg : simp_config_ext := {}) : tactic unit :=
simp_core cfg.to_simp_config cfg.discharger no_dflt hs attr_names locat
/-- Just construct the simp set and trace it -/
meta def trace_simp_set (no_dflt : parse only_flag) (hs : parse simp_arg_list) (attr_names : parse with_ident_list) : tactic unit :=
do (s, _) ← mk_simp_set no_dflt attr_names hs,
s.pp >>= trace
/-- Simplify the whole context, and use simplified hypotheses to simplify other hypotheses. -/
meta def simp_all (no_dflt : parse only_flag) (hs : parse simp_arg_list) (attr_names : parse with_ident_list)
(ids : parse without_ident_list) (cfg : simp_config_ext := {}) : tactic unit :=
do (s, u) ← mk_simp_set no_dflt attr_names hs ids,
meta def simp_all (no_dflt : parse only_flag) (hs : parse simp_arg_list) (attr_names : parse with_ident_list) (cfg : simp_config_ext := {}) : tactic unit :=
do (s, u) ← mk_simp_set no_dflt attr_names hs,
tactic.simp_all s u cfg.to_simp_config cfg.discharger,
try tactic.triv, try (tactic.reflexivity reducible)
meta def simp_intros (ids : parse ident_*) (no_dflt : parse only_flag) (hs : parse simp_arg_list) (attr_names : parse with_ident_list)
(wo_ids : parse without_ident_list) (cfg : simp_intros_config := {}) : tactic unit :=
do (s, u) ← mk_simp_set no_dflt attr_names hs wo_ids,
(cfg : simp_intros_config := {}) : tactic unit :=
do (s, u) ← mk_simp_set no_dflt attr_names hs,
when (¬u.empty) (fail (sformat! "simp_intros tactic does not support {u}")),
tactic.simp_intros s u ids cfg,
try triv >> try (reflexivity reducible)
@ -808,16 +836,13 @@ hs.mfor' (λ h_name, do h ← get_local h_name, dsimp_hyp h s u cfg)
private meta def to_simp_arg_list (es : list pexpr) : list simp_arg_type :=
es.map simp_arg_type.expr
meta def dsimp (no_dflt : parse only_flag) (es : parse opt_qexpr_list) (attr_names : parse with_ident_list)
(ids : parse without_ident_list) (l : parse location) (cfg : dsimp_config := {}) : tactic unit :=
meta def dsimp (no_dflt : parse only_flag) (es : parse simp_arg_list) (attr_names : parse with_ident_list)
(l : parse location) (cfg : dsimp_config := {}) : tactic unit :=
do (s, u) ← mk_simp_set no_dflt attr_names es,
match l with
| (loc.ns []) := do (s, u) ← mk_simp_set no_dflt attr_names (to_simp_arg_list es) ids, dsimp_target s u cfg
| (loc.ns hs) := do (s, u) ← mk_simp_set no_dflt attr_names (to_simp_arg_list es) ids, dsimp_hyps s u hs cfg
| (loc.wildcard) := do ls ← local_context,
n ← revert_lst ls,
(s, u) ← mk_simp_set no_dflt attr_names (to_simp_arg_list es) ids,
dsimp_target s u cfg,
intron n
| (loc.ns []) := dsimp_target s u cfg
| (loc.ns hs) := dsimp_hyps s u hs cfg
| (loc.wildcard) := do ls ← local_context, n ← revert_lst ls, dsimp_target s u cfg, intron n
end
/--
@ -942,7 +967,7 @@ open interactive interactive.types expr
meta def unfold (cs : parse ident*) (locat : parse location) (cfg : unfold_config := {}) : tactic unit :=
do es ← ids_to_simp_arg_list "unfold" cs,
let no_dflt := tt,
simp_core cfg.to_simp_config failed no_dflt es [] [] locat
simp_core cfg.to_simp_config failed no_dflt es [] locat
meta def unfold1 (cs : parse ident*) (locat : parse location) (cfg : unfold_config := {single_pass := tt}) : tactic unit :=
unfold cs locat cfg

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

@ -252,12 +252,12 @@ 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 simp_arg_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list)
meta def simp (no_dflt : parse only_flag) (hs : parse simp_arg_list) (attr_names : parse with_ident_list)
(cfg : simp_config_ext := {}) : smt_tactic unit :=
tactic.interactive.simp no_dflt hs attr_names ids (loc.ns []) cfg
tactic.interactive.simp no_dflt hs attr_names (loc.ns []) 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 :=
tactic.interactive.dsimp no_dflt es attr_names ids (loc.ns [])
meta def dsimp (no_dflt : parse only_flag) (es : parse simp_arg_list) (attr_names : parse with_ident_list) : smt_tactic unit :=
tactic.interactive.dsimp no_dflt es attr_names (loc.ns [])
meta def rsimp : smt_tactic unit :=
do ccs ← to_cc_state, _root_.rsimp.rsimplify_goal ccs

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_ext?"],"text":"simp","type":"interactive.parse interactive.types.only_flag → interactive.parse simp_arg_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, iota := tt, single_pass := ff, fail_if_unchanged := 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 simp_arg_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, iota := tt, single_pass := ff, fail_if_unchanged := 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 simp_arg_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, iota := tt, single_pass := ff, fail_if_unchanged := 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 simp_arg_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, iota := tt, single_pass := ff, fail_if_unchanged := tt, memoize := tt}, discharger := failed unit} → 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 [*]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and all hypotheses.\n\n- `simp only [h_1, ..., h_n]` is like `simp [h_1, ..., h_n]` but does not use `[simp]` lemmas\n\n- `simp [-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?","[(* | (- id | expr)), ...]?","(with id*)?","(at (* | id*))?","simp_config_ext?"],"text":"simp","type":"interactive.parse interactive.types.only_flag → interactive.parse simp_arg_list → interactive.parse interactive.types.with_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, iota := tt, single_pass := ff, fail_if_unchanged := 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 [*]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and all hypotheses.\n\n- `simp only [h_1, ..., h_n]` is like `simp [h_1, ..., h_n]` but does not use `[simp]` lemmas\n\n- `simp [-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?","[(* | (- id | expr)), ...]?","(with id*)?","(at (* | id*))?","simp_config_ext?"],"text":"simp","type":"interactive.parse interactive.types.only_flag → interactive.parse simp_arg_list → interactive.parse interactive.types.with_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, iota := tt, single_pass := ff, fail_if_unchanged := 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 [*]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and all hypotheses.\n\n- `simp only [h_1, ..., h_n]` is like `simp [h_1, ..., h_n]` but does not use `[simp]` lemmas\n\n- `simp [-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?","[(* | (- id | expr)), ...]?","(with id*)?","(at (* | id*))?","simp_config_ext?"],"text":"simp","type":"interactive.parse interactive.types.only_flag → interactive.parse simp_arg_list → interactive.parse interactive.types.with_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, iota := tt, single_pass := ff, fail_if_unchanged := 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 [*]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and all hypotheses.\n\n- `simp only [h_1, ..., h_n]` is like `simp [h_1, ..., h_n]` but does not use `[simp]` lemmas\n\n- `simp [-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?","[(* | (- id | expr)), ...]?","(with id*)?","(at (* | id*))?","simp_config_ext?"],"text":"simp","type":"interactive.parse interactive.types.only_flag → interactive.parse simp_arg_list → interactive.parse interactive.types.with_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, iota := tt, single_pass := ff, fail_if_unchanged := 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}

2
tests/lean/run/dsimp_test.lean
View file

@ -52,7 +52,7 @@ end
example (a b c : nat) : g (f 1, f 2) = 41 :=
begin
dsimp [f] without gax,
dsimp [f, -gax],
guard_target g (20 + 0, 20 + 1) = 41,
dsimp [g],
guard_target 20 + 0 + (20 + 1) = 41,

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

@ -41,8 +41,8 @@ attribute [simp] boo bla
example (a b : nat) : a = b → h 0 a = b :=
begin
intro h,
simp [h] without bla -- should fail if bla is used
simp [h, -bla] -- should fail if bla is used
end
open tactic
example (a b : nat) : a = b → h 0 a = b :=
by simp without bla {contextual := tt}
by simp [-bla] {contextual := tt}

34
tests/lean/simp_except.lean Normal file
View file

@ -0,0 +1,34 @@
constant f : nat → nat
namespace foo
axiom fax : ∀ x, f x = x
end foo
attribute [simp] foo.fax
example (a : nat) : f a = a :=
by simp -- works
example (a : nat) : f a = a :=
by simp [-fax] -- Error: unknown identifier 'fax'
example (a : nat) : f a = a :=
by simp [-foo.fax] -- Error: simplify failed to simplify
section
open foo
example (a : nat) : f a = a :=
by simp [-fax] -- Error: simplify failed to simplify
end
example (a : nat) (h : a = 0) : a = 0 :=
by simp [-h] -- Error: invalid local exception h, '*' was not used
example (a : nat) (h : a = 0) : a = 0 :=
by simp [*, -h] -- Error: simplify failed to simplify
example (a : nat) (h : a = 0) : a = 0 :=
by simp [*] -- works
example (a b : nat) (h : b = 0) (h₁ : a = b) (h₂ : b = a) : b = 0 :=
by simp [*, -h₁, -h₂] -- we can prevent loops by removing "bad" hypotheses

22
tests/lean/simp_except.lean.expected.out Normal file
View file

@ -0,0 +1,22 @@
simp_except.lean:13:3: error: unknown identifier 'fax'
state:
a : ℕ
⊢ f a = a
simp_except.lean:16:3: error: simplify tactic failed to simplify
state:
a : ℕ
⊢ f a = a
simp_except.lean:21:3: error: simplify tactic failed to simplify
state:
a : ℕ
⊢ f a = a
simp_except.lean:25:3: error: invalid local exception h, '*' was not used
state:
a : ℕ,
h : a = 0
⊢ a = 0
simp_except.lean:28:3: error: simplify tactic failed to simplify
state:
a : ℕ,
h : a = 0
⊢ a = 0