diff --git a/doc/changes.md b/doc/changes.md index 5c62f3545c..1e9d7f9cbc 100644 --- a/doc/changes.md +++ b/doc/changes.md @@ -75,6 +75,8 @@ For more details, see discussion [here](https://github.com/leanprover/lean/pull/ and it is shorthand for `unfold f {single_pass := tt}`. Remark: in v3.2.0, `unfold` was just an alias for the `dunfold` tactic. +* Deleted `simph` and `simp_using_hs` tactics. We should use `simp [*]` instead. + *API name changes* * `tactic.dsimp` and `tactic.dsimp_core` => `tactic.dsimp_target` diff --git a/library/data/hash_map.lean b/library/data/hash_map.lean index aed3a17cf4..3bfece4f56 100644 --- a/library/data/hash_map.lean +++ b/library/data/hash_map.lean @@ -160,9 +160,9 @@ theorem valid.nodup {n} {bkts : bucket_array α β n} {sz : nat} : valid bkts sz theorem valid.eq {n} {bkts : bucket_array α β n} {sz : nat} (v : valid bkts sz) {i h a b} (el : sigma.mk a b ∈ array.read bkts ⟨i, h⟩) : (mk_idx n (hash_fn a)).1 = i := have h1 : list.length (array.to_list bkts) - 1 - i < list.length (list.reverse (array.to_list bkts)), - by simph[array.to_list_length, nat.sub_one_sub_lt], + by simp [*, array.to_list_length, nat.sub_one_sub_lt], have _, from nat.sub_eq_sub_min, -have sigma.mk a b ∈ list.nth_le (array.to_list bkts) i (by simph[array.to_list_length]), by {rw array.to_list_nth, exact el}, +have sigma.mk a b ∈ list.nth_le (array.to_list bkts) i (by simp [*, array.to_list_length]), by {rw array.to_list_nth, exact el}, begin rw -list.nth_le_reverse at this, have v : valid_aux (λa, (mk_idx n (hash_fn a)).1) (array.to_list bkts).reverse sz, diff --git a/library/data/list/comb.lean b/library/data/list/comb.lean index 6f78acdf4d..230c5fa52a 100644 --- a/library/data/list/comb.lean +++ b/library/data/list/comb.lean @@ -91,7 +91,7 @@ theorem foldr_append (f : α → β → β) : | b (a::l₁) l₂ := by simp [foldr_append] theorem foldl_reverse (f : α → β → α) (a : α) (l : list β) : foldl f a (reverse l) = foldr (λx y, f y x) a l := -by induction l; simph [foldl, foldr] +by induction l; simp [*, foldl, foldr] theorem foldr_reverse (f : α → β → β) (a : β) (l : list α) : foldr f a (reverse l) = foldl (λx y, f y x) a l := let t := foldl_reverse (λx y, f y x) a (reverse l) in diff --git a/library/data/vector.lean b/library/data/vector.lean index 7a1eefc0e3..538393c4d1 100644 --- a/library/data/vector.lean +++ b/library/data/vector.lean @@ -54,7 +54,7 @@ def to_list (v : vector α n) : list α := v.1 def nth : Π (v : vector α n), fin n → α | ⟨ l, h ⟩ i := l.nth_le i.1 (by rw h; exact i.2) def append {n m : nat} : vector α n → vector α m → vector α (n + m) -| ⟨ l₁, h₁ ⟩ ⟨ l₂, h₂ ⟩ := ⟨ l₁ ++ l₂, by simp_using_hs ⟩ +| ⟨ l₁, h₁ ⟩ ⟨ l₂, h₂ ⟩ := ⟨ l₁ ++ l₂, by simp [*] ⟩ @[elab_as_eliminator] def elim {α} {C : Π {n}, vector α n → Sort u} (H : ∀l : list α, C ⟨l, rfl⟩) {n : nat} : Π (v : vector α n), C v @@ -63,7 +63,7 @@ def append {n m : nat} : vector α n → vector α m → vector α (n + m) /- map -/ def map (f : α → β) : vector α n → vector β n -| ⟨ l, h ⟩ := ⟨ list.map f l, by simp_using_hs ⟩ +| ⟨ l, h ⟩ := ⟨ list.map f l, by simp [*] ⟩ @[simp] lemma map_nil (f : α → β) : map f nil = nil := rfl @@ -71,16 +71,16 @@ lemma map_cons (f : α → β) (a : α) : Π (v : vector α n), map f (a::v) = f | ⟨l,h⟩ := rfl def map₂ (f : α → β → φ) : vector α n → vector β n → vector φ n -| ⟨ x, _ ⟩ ⟨ y, _ ⟩ := ⟨ list.map₂ f x y, by simp_using_hs ⟩ +| ⟨ x, _ ⟩ ⟨ y, _ ⟩ := ⟨ list.map₂ f x y, by simp [*] ⟩ def repeat (a : α) (n : ℕ) : vector α n := ⟨ list.repeat a n, list.length_repeat a n ⟩ def dropn (i : ℕ) : vector α n → vector α (n - i) -| ⟨l, p⟩ := ⟨ list.dropn i l, by simp_using_hs ⟩ +| ⟨l, p⟩ := ⟨ list.dropn i l, by simp [*] ⟩ def taken (i : ℕ) : vector α n → vector α (min i n) -| ⟨l, p⟩ := ⟨ list.taken i l, by simp_using_hs ⟩ +| ⟨l, p⟩ := ⟨ list.taken i l, by simp [*] ⟩ def remove_nth (i : fin n) : vector α n → vector α (n - 1) | ⟨l, p⟩ := ⟨ list.remove_nth l i.1, by rw[l.length_remove_nth i.1]; rw p; exact i.2 ⟩ @@ -96,13 +96,13 @@ section accum def map_accumr (f : α → σ → σ × β) : vector α n → σ → σ × vector β n | ⟨ x, px ⟩ c := let res := list.map_accumr f x c in - ⟨ res.1, res.2, by simp_using_hs ⟩ + ⟨ res.1, res.2, by simp [*] ⟩ def map_accumr₂ {α β σ φ : Type} (f : α → β → σ → σ × φ) : vector α n → vector β n → σ → σ × vector φ n | ⟨ x, px ⟩ ⟨ y, py ⟩ c := let res := list.map_accumr₂ f x y c in - ⟨ res.1, res.2, by simp_using_hs ⟩ + ⟨ res.1, res.2, by simp [*] ⟩ end accum diff --git a/library/init/algebra/functions.lean b/library/init/algebra/functions.lean index 2402ee38c1..be86f90b81 100644 --- a/library/init/algebra/functions.lean +++ b/library/init/algebra/functions.lean @@ -19,7 +19,7 @@ variables {α : Type u} [decidable_linear_order α] private meta def min_tac_step : tactic unit := solve1 $ intros >> `[unfold min max] ->> try `[simp_using_hs [if_pos, if_neg]] +>> try `[simp [*, if_pos, if_neg]] >> try `[apply le_refl] >> try `[apply le_of_not_le, assumption] diff --git a/library/init/algebra/norm_num.lean b/library/init/algebra/norm_num.lean index 85d2689048..c5ef8cc22f 100644 --- a/library/init/algebra/norm_num.lean +++ b/library/init/algebra/norm_num.lean @@ -256,13 +256,13 @@ begin intro ha, apply h, apply neg_inj, rwa neg_zero end lemma sub_nat_zero_helper {a b c d: ℕ} (hac : a = c) (hbd : b = d) (hcd : c < d) : a - b = 0 := begin - simp_using_hs, apply nat.sub_eq_zero_of_le, apply le_of_lt, assumption + simp [*], apply nat.sub_eq_zero_of_le, apply le_of_lt, assumption end lemma sub_nat_pos_helper {a b c d e : ℕ} (hac : a = c) (hbd : b = d) (hced : e + d = c) : a - b = e := begin -simp_using_hs, rw [-hced, nat.add_sub_cancel] +simp [*], rw [-hced, nat.add_sub_cancel] end end norm_num diff --git a/library/init/data/array/lemmas.lean b/library/init/data/array/lemmas.lean index d66689e25c..1fc117fa65 100644 --- a/library/init/data/array/lemmas.lean +++ b/library/init/data/array/lemmas.lean @@ -28,7 +28,7 @@ theorem to_list_reverse (a : array α n) : a.to_list.reverse = a.rev_list := by rw [-rev_list_reverse, list.reverse_reverse] theorem rev_list_length_aux (a : array α n) (i h) : (a.iterate_aux (λ _ v l, v :: l) i h []).length = i := -by induction i; simph[iterate_aux] +by induction i; simp [*, iterate_aux] theorem rev_list_length (a : array α n) : a.rev_list.length = n := rev_list_length_aux a _ _ @@ -43,7 +43,7 @@ theorem to_list_nth_core (a : array α n) (i : ℕ) (ih : i < n) : Π (j) {jh t show list.nth_le (a.read ⟨j, jh⟩ :: t) k tl = a.read ⟨i, ih⟩, from match k, hjk, tl with | 0, e, tl := match i, e, ih with ._, rfl, _ := rfl end - | k'+1, _, tl := by simp[list.nth_le]; exact al _ _ (by simph) + | k'+1, _, tl := by simp[list.nth_le]; exact al _ _ (by simp [*]) end theorem to_list_nth (a : array α n) (i : ℕ) (h h') : list.nth_le a.to_list i h' = a.read ⟨i, h⟩ := diff --git a/library/init/data/array/slice.lean b/library/init/data/array/slice.lean index 402bce67d1..a22e18c625 100644 --- a/library/init/data/array/slice.lean +++ b/library/init/data/array/slice.lean @@ -27,7 +27,7 @@ calc n - (n - m) = (n - m) + m - (n - m) : by rw nat.sub_add_cancel; assumption ... = m : nat.add_sub_cancel_left _ _ def taken_right (a : array α n) (m : nat) (h : m ≤ n) : array α m := -cast (by simph [sub_sub_cancel]) $ a.dropn (n - m) (nat.sub_le _ _) +cast (by simp [*, sub_sub_cancel]) $ a.dropn (n - m) (nat.sub_le _ _) def reverse (a : array α n) : array α n := ⟨ λ ⟨ i, hi ⟩, a.read ⟨ n - (i + 1), diff --git a/library/init/data/list/instances.lean b/library/init/data/list/instances.lean index 80de070766..91153bae85 100644 --- a/library/init/data/list/instances.lean +++ b/library/init/data/list/instances.lean @@ -25,7 +25,7 @@ private lemma append_bind : list.bind (xs ++ ys) f = list.bind xs f ++ list.bind begin induction xs, { refl }, - { simph [cons_bind] } + { simp [*, cons_bind] } end end @@ -36,13 +36,13 @@ instance : monad list := id_map := begin intros _ xs, induction xs with x xs ih, { refl }, - { dsimp [function.comp] at ih, dsimp [function.comp], simph } + { dsimp [function.comp] at ih, dsimp [function.comp], simp [*] } end, pure_bind := by simp_intros, bind_assoc := begin intros _ _ _ xs _ _, induction xs, { refl }, - { simph } + { simp [*] } end} instance : alternative list := diff --git a/library/init/data/list/lemmas.lean b/library/init/data/list/lemmas.lean index fdbced6524..5116ec571c 100644 --- a/library/init/data/list/lemmas.lean +++ b/library/init/data/list/lemmas.lean @@ -22,10 +22,10 @@ rfl rfl @[simp] lemma append_nil (t : list α) : t ++ [] = t := -by induction t; simph +by induction t; simp [*] @[simp] lemma append_assoc (s t u : list α) : s ++ t ++ u = s ++ (t ++ u) := -by induction s; simph +by induction s; simp [*] lemma append_ne_nil_of_ne_nil_left (s t : list α) : s ≠ [] → s ++ t ≠ [] := by induction s; intros; contradiction @@ -42,7 +42,7 @@ by {revert a, induction s with b s H, exact λ_, rfl, intros, simp [foldr], rw H /- concat -/ @[simp] lemma concat_eq_append (a : α) (l : list α) : concat l a = l ++ [a] := -by induction l; simph [concat] +by induction l; simp [*, concat] /- head & tail -/ @@ -79,13 +79,13 @@ lemma length_cons (a : α) (l : list α) : length (a :: l) = length l + 1 := rfl @[simp] lemma length_append (s t : list α) : length (s ++ t) = length s + length t := -by induction s; simph +by induction s; simp [*] lemma length_concat (a : α) (l : list α) : length (concat l a) = succ (length l) := by simp [succ_eq_add_one] @[simp] lemma length_repeat (a : α) (n : ℕ) : length (repeat a n) = n := -by induction n; simph; refl +by induction n; simp [*]; refl lemma eq_nil_of_length_eq_zero {l : list α} : length l = 0 → l = [] := by {induction l; intros, refl, contradiction} @@ -97,7 +97,7 @@ by induction l; intros; contradiction @[simp] lemma length_taken : ∀ (i : ℕ) (l : list α), length (taken i l) = min i (length l) | 0 l := by simp | (succ n) [] := by simp -| (succ n) (a::l) := begin simph [nat.min_succ_succ, add_one_eq_succ] end +| (succ n) (a::l) := begin simp [*, nat.min_succ_succ, add_one_eq_succ] end -- TODO(Leo): cleanup proof after arith dec proc @[simp] lemma length_dropn : ∀ (i : ℕ) (l : list α), length (dropn i l) = length l - i @@ -148,7 +148,7 @@ theorem ext : Π {l₁ l₂ : list α}, (∀n, nth l₁ n = nth l₂ n) → l₁ | [] [] h := rfl | (a::l₁) [] h := by have h0 := h 0; contradiction | [] (a'::l₂) h := by have h0 := h 0; contradiction -| (a::l₁) (a'::l₂) h := by have h0 : some a = some a' := h 0; injection h0 with aa; simph[ext $ λn, h (n+1)] +| (a::l₁) (a'::l₂) h := by have h0 : some a = some a' := h 0; injection h0 with aa; simp [*, ext (λn, h (n+1))] theorem ext_le {l₁ l₂ : list α} (hl : length l₁ = length l₂) (h : ∀n h₁ h₂, nth_le l₁ n h₁ = nth_le l₂ n h₂) : l₁ = l₂ := ext $ λn, if h₁ : n < length l₁ @@ -163,46 +163,46 @@ lemma map_cons (f : α → β) (a l) : map f (a::l) = f a :: map f l := rfl @[simp] lemma map_append (f : α → β) : ∀ l₁ l₂, map f (l₁ ++ l₂) = (map f l₁) ++ (map f l₂) := -by intro l₁; induction l₁; intros; simph +by intro l₁; induction l₁; intros; simp [*] lemma map_singleton (f : α → β) (a : α) : map f [a] = [f a] := rfl lemma map_concat (f : α → β) (a : α) (l : list α) : map f (concat l a) = concat (map f l) (f a) := -by induction l; simph +by induction l; simp [*] @[simp] lemma map_id (l : list α) : map id l = l := -by induction l; simph +by induction l; simp [*] lemma map_id' {f : α → α} (h : ∀ x, f x = x) (l : list α) : map f l = l := -by induction l; simph +by induction l; simp [*] @[simp] lemma map_map (g : β → γ) (f : α → β) (l : list α) : map g (map f l) = map (g ∘ f) l := -by induction l; simph +by induction l; simp [*] @[simp] lemma length_map (f : α → β) (l : list α) : length (map f l) = length l := -by induction l; simph +by induction l; simp [*] @[simp] lemma foldl_map (g : β → γ) (f : α → γ → α) (a : α) (l : list β) : foldl f a (map g l) = foldl (λx y, f x (g y)) a l := -by revert a; induction l; intros; simph[foldl] +by revert a; induction l; intros; simp [*, foldl] @[simp] lemma foldr_map (g : β → γ) (f : γ → α → α) (a : α) (l : list β) : foldr f a (map g l) = foldr (f ∘ g) a l := -by revert a; induction l; intros; simph[foldr] +by revert a; induction l; intros; simp [*, foldr] theorem foldl_hom (f : α → β) (g : α → γ → α) (g' : β → γ → β) (a : α) (h : ∀a x, f (g a x) = g' (f a) x) (l : list γ) : f (foldl g a l) = foldl g' (f a) l := -by revert a; induction l; intros; simph[foldl] +by revert a; induction l; intros; simp [*, foldl] theorem foldr_hom (f : α → β) (g : γ → α → α) (g' : γ → β → β) (a : α) (h : ∀x a, f (g x a) = g' x (f a)) (l : list γ) : f (foldr g a l) = foldr g' (f a) l := -by revert a; induction l; intros; simph[foldr] +by revert a; induction l; intros; simp [*, foldr] /- map₂ -/ attribute [simp] map₂ @[simp] lemma length_map₂ (f : α → β → γ) (l₁) : ∀ l₂, length (map₂ f l₁ l₂) = min (length l₁) (length l₂) := -by {induction l₁; intro l₂; cases l₂; simph [add_one_eq_succ, min_succ_succ]} +by {induction l₁; intro l₂; cases l₂; simp [*, add_one_eq_succ, min_succ_succ]} /- reverse -/ @@ -220,19 +220,19 @@ aux l nil rfl @[simp] lemma reverse_append (s t : list α) : reverse (s ++ t) = (reverse t) ++ (reverse s) := -by induction s; simph +by induction s; simp [*] @[simp] lemma reverse_reverse (l : list α) : reverse (reverse l) = l := -by induction l; simph +by induction l; simp [*] lemma concat_eq_reverse_cons (a : α) (l : list α) : concat l a = reverse (a :: reverse l) := -by induction l; simph +by induction l; simp [*] @[simp] lemma length_reverse (l : list α) : length (reverse l) = length l := -by induction l; simph +by induction l; simp [*] @[simp] lemma map_reverse (f : α → β) (l : list α) : map f (reverse l) = reverse (map f l) := -by induction l; simph +by induction l; simp [*] lemma nth_le_reverse_aux1 : Π (l r : list α) (i h1 h2), nth_le (reverse_core l r) (i + length l) h1 = nth_le r i h2 | [] r i := λh1 h2, rfl @@ -265,18 +265,18 @@ nth_le_reverse_aux2 _ _ _ _ _ attribute [simp] last @[simp] lemma last_cons {a : α} {l : list α} : ∀ (h₁ : a :: l ≠ nil) (h₂ : l ≠ nil), last (a :: l) h₁ = last l h₂ := -by {induction l; intros, contradiction, simph, reflexivity} +by {induction l; intros, contradiction, simp [*], reflexivity} @[simp] lemma last_append {a : α} (l : list α) (h : l ++ [a] ≠ []) : last (l ++ [a]) h = a := begin induction l with hd tl ih; rsimp, have haux : tl ++ [a] ≠ [], {apply append_ne_nil_of_ne_nil_right, contradiction}, - simph + simp [*] end lemma last_concat {a : α} (l : list α) (h : concat l a ≠ []) : last (concat l a) h = a := -by simph +by simp [*] /- nth -/ @@ -408,7 +408,7 @@ lemma ne_and_not_mem_of_not_mem_cons {a y : α} {l : list α} : a ∉ y::l → a assume p, and.intro (ne_of_not_mem_cons p) (not_mem_of_not_mem_cons p) @[simp] lemma mem_reverse (a : α) (l : list α) : a ∈ reverse l ↔ a ∈ l := -by induction l; simph; rw mem_append_eq +by induction l; simp [*]; rw mem_append_eq @[simp] lemma bex_nil_iff_false (p : α → Prop) : (∃ x ∈ @nil α, p x) ↔ false := iff_false_intro $ λ⟨x, hx, px⟩, hx @@ -431,7 +431,7 @@ begin induction l with b l' ih, {simp at h, contradiction }, {simp, simp at h, cases h with h h, - {simph}, + {simp [*]}, {exact or.inr (ih h)}} end @@ -442,7 +442,7 @@ begin {cases (eq_or_mem_of_mem_cons h) with h h, {existsi c, simp [h]}, {cases ih h with a ha, cases ha with ha₁ ha₂, - existsi a, simph }} + existsi a, simp [*] }} end lemma mem_map_iff {f : α → β} {b : β} {l : list α} : b ∈ map f l ↔ ∃ a, a ∈ l ∧ f a = b := diff --git a/library/init/data/nat/lemmas.lean b/library/init/data/nat/lemmas.lean index dcf1124608..b8a11e1206 100644 --- a/library/init/data/nat/lemmas.lean +++ b/library/init/data/nat/lemmas.lean @@ -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; simph[mul_succ] without mul_comm} +by {induction n; simp [*, mul_succ] without mul_comm} @[simp] theorem mul_div_left (m : ℕ) {n : ℕ} (H : n > 0) : m * n / n = m := by rw [mul_comm, mul_div_right _ H] diff --git a/library/init/meta/converter/interactive.lean b/library/init/meta/converter/interactive.lean index 27f8e9ffb2..245aac42f9 100644 --- a/library/init/meta/converter/interactive.lean +++ b/library/init/meta/converter/interactive.lean @@ -39,7 +39,7 @@ conv.skip meta def whnf : conv unit := conv.whnf -meta def dsimp (no_dflt : parse only_flag) (es : parse opt_qexpr_list) (attr_names : parse with_ident_list) +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, conv.dsimp (some s) u cfg @@ -108,7 +108,7 @@ do (r, lhs, _) ← tactic.target_lhs_rhs, r lhs, update_lhs new_lhs pr -meta def simp (no_dflt : parse only_flag) (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) +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 := {}) : conv unit := do (s, u) ← tactic.mk_simp_set no_dflt attr_names hs ids, diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean index 083ab0e3ad..1fc19f0689 100644 --- a/library/init/meta/interactive.lean +++ b/library/init/meta/interactive.lean @@ -657,7 +657,31 @@ meta structure simp_config_ext extends simp_config := (discharger : tactic unit := failed) section mk_simp_set -open expr +open expr interactive.types + +meta inductive simp_arg_type : Type +| all_hyps : simp_arg_type +| expr : pexpr → simp_arg_type + +meta instance : has_reflect simp_arg_type +| simp_arg_type.all_hyps := `(_) +| (simp_arg_type.expr _) := `(_) + +meta def simp_arg : parser simp_arg_type := +(tk "*" *> return simp_arg_type.all_hyps) <|> (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 add_simps : simp_lemmas → list name → tactic simp_lemmas | s [] := return s @@ -697,9 +721,11 @@ 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 pexpr) (ex : list name) : tactic (simp_lemmas × list name) := -do s ← join_user_simp_lemmas no_dflt attr_names, +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, + 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, -- 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) @@ -714,10 +740,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) (ctx : list expr) (hs : list pexpr) (attr_names : list name) (ids : list name) + (no_dflt : bool) (hs : list simp_arg_type) (attr_names : list name) (ids : list name) (locat : loc) : tactic unit := do (s, u) ← mk_simp_set no_dflt attr_names hs ids, - s ← s.append ctx, match locat : _ → tactic unit with | loc.wildcard := do hs ← non_dep_prop_hyps, @@ -758,52 +783,39 @@ 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) +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 +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) +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, tactic.simp_all s u cfg.to_simp_config cfg.discharger, try tactic.triv, try (tactic.reflexivity reducible) -/-- -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_ext := {}) : tactic unit := -do ctx ← collect_ctx_simps, - 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_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) +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, when (¬u.empty) (fail (sformat! "simp_intros tactic does not support {u}")), tactic.simp_intros s u ids cfg, try triv >> try (reflexivity reducible) -meta def simph_intros (ids : parse ident_*) (no_dflt : parse only_flag) (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) - (wo_ids : parse without_ident_list) (cfg : simp_intros_config := {}) : tactic unit := -simp_intros ids no_dflt hs attr_names wo_ids {cfg with use_hyps := tt} - private meta def dsimp_hyps (s : simp_lemmas) (u : list name) (hs : list name) (cfg : dsimp_config := {}) : tactic unit := 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 := match l with -| (loc.ns []) := do (s, u) ← mk_simp_set no_dflt attr_names es ids, dsimp_target s u cfg -| (loc.ns hs) := do (s, u) ← mk_simp_set no_dflt attr_names es ids, dsimp_hyps s u hs cfg +| (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 es ids, + (s, u) ← mk_simp_set no_dflt attr_names (to_simp_arg_list es) ids, dsimp_target s u cfg, intron n end @@ -909,14 +921,14 @@ meta def unfold_projs : parse location → tactic unit end interactive -meta def ids_to_pexprs (tac_name : name) (cs : list name) : tactic (list pexpr) := +meta def ids_to_simp_arg_list (tac_name : name) (cs : list name) : tactic (list simp_arg_type) := cs.mmap $ λ c, do n ← resolve_name c, hs ← get_eqn_lemmas_for ff n.const_name, env ← get_env, let p := env.is_projection n.const_name, when (hs.empty ∧ p.is_none) (fail (sformat! "{tac_name} tactic failed, {c} does not have equational lemmas nor is a projection")), - return (expr.const c []) + return $ simp_arg_type.expr (expr.const c []) structure unfold_config extends simp_config := (zeta := ff) @@ -928,9 +940,9 @@ namespace interactive open interactive interactive.types expr meta def unfold (cs : parse ident*) (locat : parse location) (cfg : unfold_config := {}) : tactic unit := -do es ← ids_to_pexprs "unfold" cs, +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 diff --git a/library/init/meta/smt/interactive.lean b/library/init/meta/smt/interactive.lean index 32b06a8245..6ef5f81b79 100644 --- a/library/init/meta/smt/interactive.lean +++ b/library/init/meta/smt/interactive.lean @@ -252,19 +252,10 @@ 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) +meta def simp (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 := {}) : 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_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_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 := tactic.interactive.dsimp no_dflt es attr_names ids (loc.ns []) diff --git a/tests/lean/interactive/info_tactic.lean.expected.out b/tests/lean/interactive/info_tactic.lean.expected.out index 0db9b09f16..eb843ed003 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_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, 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 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, 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 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, 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 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, 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 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":{"full-id":"tactic.get_env","source":,"tactic_params":[],"type":"tactic environment"},"response":"ok","seq_num":14} diff --git a/tests/lean/run/cpdt.lean b/tests/lean/run/cpdt.lean index 086c8b7f50..38f55ace1a 100644 --- a/tests/lean/run/cpdt.lean +++ b/tests/lean/run/cpdt.lean @@ -37,7 +37,7 @@ def reassoc : exp → exp attribute [simp] mul_add times reassoc eeval theorem eeval_times (k e) : eeval (times k e) = k * eeval e := -by induction e; simph +by induction e; simp [*] theorem reassoc_correct (e) : eeval (reassoc e) = eeval e := -by induction e; simph; cases (reassoc e2); rsimp +by induction e; simp [*]; cases (reassoc e2); rsimp diff --git a/tests/lean/run/even_odd.lean b/tests/lean/run/even_odd.lean index b95672dfe5..fb70ceaa13 100644 --- a/tests/lean/run/even_odd.lean +++ b/tests/lean/run/even_odd.lean @@ -16,5 +16,5 @@ lemma even_eq_not_odd : ∀ a, even a = bnot (odd a) := begin intro a, induction a, simp [even, odd], - simph [even, odd] + simp [*, even, odd] end diff --git a/tests/lean/run/even_odd2.lean b/tests/lean/run/even_odd2.lean index c5f5ecb9cd..de89ba850e 100644 --- a/tests/lean/run/even_odd2.lean +++ b/tests/lean/run/even_odd2.lean @@ -17,5 +17,5 @@ lemma even_eq_not_odd : ∀ a, even a = bnot (odd a) := begin intro a, induction a, simp [even, odd], - simph [even, odd] + simp [*, even, odd] end diff --git a/tests/lean/run/quote_bas.lean b/tests/lean/run/quote_bas.lean index 9c42f2764f..5f822f2a4b 100644 --- a/tests/lean/run/quote_bas.lean +++ b/tests/lean/run/quote_bas.lean @@ -46,7 +46,7 @@ begin induction e, reflexivity, reflexivity, - simp_using_hs + simp [*] end @[simp] lemma eval_map_var_sum_assoc {A : Type u} {B : Type v} {C : Type w} (v : Env A) (v' : Env B) (v'' : Env C) (e : Expr (sum (sum A B) C)) : @@ -55,7 +55,7 @@ begin induction e, reflexivity, { cases v_1 with v₁, cases v₁, all_goals {simp} }, - { simp_using_hs } + { simp [*] } end class Quote {V : inout Type u} (l : inout Env V) (n : Value) {V' : inout Type v} (r : inout Env V') := diff --git a/tests/lean/run/simp_match_reducibility_issue.lean b/tests/lean/run/simp_match_reducibility_issue.lean index 1ea1c8256d..adfcc060fb 100644 --- a/tests/lean/run/simp_match_reducibility_issue.lean +++ b/tests/lean/run/simp_match_reducibility_issue.lean @@ -10,7 +10,7 @@ namespace vector def nil : vector α 0 := ⟨[], rfl⟩ def append {m n : ℕ} : vector α m → vector α n → vector α (m + n) - | ⟨v, _⟩ ⟨w, _⟩ := ⟨v ++ w, by abstract {simph}⟩ + | ⟨v, _⟩ ⟨w, _⟩ := ⟨v ++ w, by abstract {simp [*]}⟩ end vector diff --git a/tests/lean/run/simp_proj.lean b/tests/lean/run/simp_proj.lean index 915ac6fde6..78780d475a 100644 --- a/tests/lean/run/simp_proj.lean +++ b/tests/lean/run/simp_proj.lean @@ -53,7 +53,7 @@ end example (a b : nat) : a + b = b + a := begin - simph only [has_add.add], + simp only [*, has_add.add], guard_target nat.add a b = nat.add b a, apply nat.add_comm end diff --git a/tests/lean/run/soundness.lean b/tests/lean/run/soundness.lean index 55608e3a02..97246406ed 100644 --- a/tests/lean/run/soundness.lean +++ b/tests/lean/run/soundness.lean @@ -123,41 +123,41 @@ namespace PropF (λ t : is_true (TrueQ v A), have Satisfies v (A::Γ), from Satisfies_cons s t, have TrueQ v B = tt, from Soundness_general H this, - by simph) + by simp[*]) (λ f : ¬ is_true (TrueQ v A), - have TrueQ v A = ff, by simp at f; simph, - have bnot (TrueQ v A) = tt, by simph, - by simph) + have TrueQ v A = ff, by simp at f; simp[*], + have bnot (TrueQ v A) = tt, by simp[*], + by simp[*]) | ._ ._ (ImpE Γ A B H₁ H₂) s := have aux : TrueQ v A = tt, from Soundness_general H₂ s, have bnot (TrueQ v A) || TrueQ v B = tt, from Soundness_general H₁ s, - by simp [aux] at this; simph + by simp [aux] at this; simp[*] | ._ ._ (BotC Γ A H) s := by_contradiction (λ n : TrueQ v A ≠ tt, - have TrueQ v A = ff, by {simp at n; simph}, - have TrueQ v (~A) = tt, begin change (bnot (TrueQ v A) || ff = tt), simph end, + have TrueQ v A = ff, by {simp at n; simp[*]}, + have TrueQ v (~A) = tt, begin change (bnot (TrueQ v A) || ff = tt), simp[*] end, have Satisfies v ((~A)::Γ), from Satisfies_cons s this, have TrueQ v ⊥ = tt, from Soundness_general H this, absurd this ff_ne_tt) | .(A ∧ B) ._ (AndI Γ A B H₁ H₂) s := have TrueQ v A = tt, from Soundness_general H₁ s, have TrueQ v B = tt, from Soundness_general H₂ s, - by simph + by simp[*] | ._ ._ (AndE₁ Γ A B H) s := have TrueQ v (A ∧ B) = tt, from Soundness_general H s, - by simp [TrueQ] at this; simph [is_true] + by simp [TrueQ] at this; simp [*, is_true] | ._ ._ (AndE₂ Γ A B H) s := have TrueQ v (A ∧ B) = tt, from Soundness_general H s, - by simp at this; simph + by simp at this; simp[*] | .(A ∨ B) ._ (OrI₁ Γ A B H) s := have TrueQ v A = tt, from Soundness_general H s, - by simph + by simp[*] | .(A ∨ B) ._ (OrI₂ Γ A B H) s := have TrueQ v B = tt, from Soundness_general H s, - by simph + by simp[*] | ._ ._ (OrE Γ A B C H₁ H₂ H₃) s := have TrueQ v A || TrueQ v B = tt, from Soundness_general H₁ s, - have or (TrueQ v A = tt) (TrueQ v B = tt), by simp at this; simph, + have or (TrueQ v A = tt) (TrueQ v B = tt), by simp at this; simp[*], or.elim this (λ At, have Satisfies v (A::Γ), from Satisfies_cons s At,