From bb9e3ddae2396b574b8ab62976bd4db9520d525d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 5 Jul 2017 11:42:55 -0700 Subject: [PATCH] =?UTF-8?q?feat(library/init/meta/interactive):=20`rw=20[-?= =?UTF-8?q?h]`=20=3D=3D>=20`rw=20[=E2=86=90=20h]`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit @Armael: this change may affect your project. The file `doc/changes.md` explains the motivation for the change. --- doc/changes.md | 3 ++ library/data/bitvec.lean | 2 +- library/data/hash_map.lean | 30 +++++------ library/data/stream.lean | 16 +++--- library/init/algebra/field.lean | 54 +++++++++---------- library/init/algebra/functions.lean | 10 ++-- library/init/algebra/group.lean | 10 ++-- library/init/algebra/norm_num.lean | 32 +++++------ library/init/algebra/ordered_field.lean | 12 ++--- library/init/algebra/ordered_group.lean | 4 +- library/init/algebra/ordered_ring.lean | 14 ++--- library/init/algebra/ring.lean | 6 +-- library/init/data/array/basic.lean | 2 +- library/init/data/array/lemmas.lean | 8 +-- library/init/data/int/basic.lean | 4 +- library/init/data/int/bitwise.lean | 34 ++++++------ library/init/data/int/comp_lemmas.lean | 6 +-- library/init/data/int/lemmas.lean | 52 +++++++++--------- library/init/data/int/order.lean | 34 ++++++------ library/init/data/list/instances.lean | 10 ++-- library/init/data/list/lemmas.lean | 20 +++---- library/init/data/nat/bitwise.lean | 12 ++--- library/init/data/nat/lemmas.lean | 46 ++++++++-------- library/init/meta/interactive.lean | 2 +- tests/lean/interactive/goal_info_rw.lean | 4 +- .../goal_info_rw.lean.expected.out | 8 +-- tests/lean/nested_match.lean | 2 +- tests/lean/run/auto_quote1.lean | 4 +- tests/lean/run/bin_tree.lean | 6 +-- tests/lean/run/conv_tac1.lean | 2 +- tests/lean/run/doc_string4.lean | 4 +- tests/lean/run/term_app2.lean | 2 +- 32 files changed, 229 insertions(+), 226 deletions(-) diff --git a/doc/changes.md b/doc/changes.md index 461ff3147e..34466a6796 100644 --- a/doc/changes.md +++ b/doc/changes.md @@ -81,6 +81,9 @@ For more details, see discussion [here](https://github.com/leanprover/lean/pull/ Moreover, `simp [*, -h]` if `h` is a hypothesis, we are adding all hypotheses but `h` as additional simplification lemmas. +* Changed notation `rw [-h]` to `rw [← h]` to avoid confusion with the new `simp [-h]` notation. + The ASCII version `rw [<- h]` is also supported. + *API name changes* * `tactic.dsimp` and `tactic.dsimp_core` => `tactic.dsimp_target` diff --git a/library/data/bitvec.lean b/library/data/bitvec.lean index 0b19b54b88..082d7f0317 100644 --- a/library/data/bitvec.lean +++ b/library/data/bitvec.lean @@ -43,7 +43,7 @@ section shift begin by_cases (i ≤ n), { have h₁ := sub_le n i, - rw [min_eq_right h], rw [min_eq_left h₁, -nat.add_sub_assoc h, add_comm, nat.add_sub_cancel] }, + rw [min_eq_right h], rw [min_eq_left h₁, ← nat.add_sub_assoc h, add_comm, nat.add_sub_cancel] }, { have h₁ := le_of_not_ge h, rw [min_eq_left h₁, sub_eq_zero_of_le h₁, min_zero_left, add_zero] } end $ diff --git a/library/data/hash_map.lean b/library/data/hash_map.lean index a5bea0c2b1..637ce1b44d 100644 --- a/library/data/hash_map.lean +++ b/library/data/hash_map.lean @@ -48,7 +48,7 @@ begin (λm, let ⟨i, il, im⟩ := IH.1 m in ⟨i, nat.le_succ_of_le il, im⟩), λ⟨i, le, m⟩, or.elim (lt_or_eq_of_le (nat.le_of_succ_le_succ le)) (λl, or.inr (IH.2 ⟨i, l, m⟩)) - (λe, or.inl $ by rwa -(show i = ⟨j, h⟩, from fin.eq_of_veq e))⟩ + (λe, or.inl $ by rwa [← show i = ⟨j, h⟩, from fin.eq_of_veq e])⟩ end def foldl {δ : Type w} (d : δ) (f : δ → Π a, β a → δ) : δ := @@ -88,7 +88,7 @@ theorem find_aux_iff (a : α) (b : β a) : Π (l : list Σ a, β a), (l.map sigm | (⟨a',b'⟩::t) nd := by simp[find_aux]; exact if h : a' = a then by rw dif_pos h; exact match a', b', h with ._, b', rfl := - ⟨λe, by injection e with e; rw -e; exact or.inl rfl, + ⟨λe, by injection e with e; rw ← e; exact or.inl rfl, λo, or.elim o (λe, by injection e with _ e; rw eq_of_heq e) (λm, have a' ∉ t.map sigma.fst, from list.not_mem_of_nodup_cons nd, @@ -164,7 +164,7 @@ have h1 : list.length (array.to_list bkts) - 1 - i < list.length (list.reverse ( have _, from nat.sub_eq_sub_min, 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, + 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, rw array.to_list_reverse, exact v, @@ -200,7 +200,7 @@ end theorem valid.as_list_length {n} {bkts : bucket_array α β n} {sz : nat} (v : valid bkts sz) : bkts.as_list.length = sz := have ∀l sz, valid_aux (λ (a : α), (mk_idx n (hash_fn a)).val) l sz → ∀t, (l.foldr (λbkt r, r ++ bkt) t).length = sz + t.length, by {intros, induction a, simp[list.foldr], simp[list.foldr, ih_1]}, -by have h := this _ _ v []; rwa -array.foldl_eq at h +by have h := this _ _ v []; rwa [← array.foldl_eq] at h theorem valid.mk (n : ℕ+) : @valid n (mk_array n.1 []) 0 := let bkts : bucket_array α β n := mk_array n.1 [] in @@ -212,7 +212,7 @@ show valid_aux (λa, (mk_idx n (hash_fn a)).1) (array.iterate_aux bkts (λ_ v l, theorem valid.find_aux_iff {n} {bkts : bucket_array α β n} {sz : nat} (v : valid bkts sz) (a : α) (b : β a) : find_aux a (bkts.read hash_fn a) = some b ↔ sigma.mk a b ∈ bkts.as_list := iff.trans (find_aux_iff _ _ _ (v.nodup _ _)) - $ iff.trans (by exact ⟨λm, ⟨_, m⟩, λ⟨⟨i, h⟩, m⟩, by rwa -(v.eq' _ m) at m⟩) + $ iff.trans (by exact ⟨λm, ⟨_, m⟩, λ⟨⟨i, h⟩, m⟩, by rwa [← v.eq' _ m] at m⟩) (iff.symm (bkts.mem_as_list _)) theorem valid.contains_aux_iff {n} {bkts : bucket_array α β n} {sz : nat} (v : valid bkts sz) (a : α) : @@ -262,7 +262,7 @@ section have bn : bidx ≠ ⟨i, h⟩, from λhh, ne_of_gt hl $ fin.veq_of_eq $ eq.symm hh, have he : array.read bkts ⟨i, h⟩ = array.read bkts' ⟨i, h⟩, from (show _ = ite (bidx = ⟨i, h⟩) (f _) _, by rw if_neg bn), - by simp[array.iterate_aux]; rw -he; exact + by simp[array.iterate_aux]; rw [← he]; exact let ⟨u', w', hb, hb'⟩ := append_of_modify_aux i (le_of_lt h) hl in ⟨u', w' ++ array.read bkts ⟨i, h⟩, by simp[hb], by simp[hb']⟩ | or.inr e := @@ -271,9 +271,9 @@ section show ite (bidx = bidx) _ _ = _, by rw if_pos rfl, begin simp[array.iterate_aux, -add_comm], - rw -(show bidx = ⟨bidx.1, h⟩, from fin.eq_of_veq rfl), + 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 _), + rw [← valid.modify_aux1 _ _ (le_refl _)], rw [this, hfl, hl], simp end @@ -299,7 +299,7 @@ section have bn : bidx ≠ ⟨i, h⟩, from λhh, ne_of_gt hl $ fin.veq_of_eq $ eq.symm hh, have he : array.read bkts ⟨i, h⟩ = array.read bkts' ⟨i, h⟩, from (show _ = ite (bidx = ⟨i, h⟩) (f _) _, by rw if_neg bn), - by simp[array.iterate_aux]; rw -he; exact λvv, + by simp[array.iterate_aux]; rw [← he]; exact λvv, let ⟨s, v, nd, al, e⟩ := _root_.hash_map.valid_aux.unfold_cons vv in let ⟨hsz, v'⟩ := valid.modify_aux2 i (le_of_lt h) hl v in by rw [e, calc (s + (array.read bkts ⟨i, h⟩).length) + v2.length - v1.length @@ -313,8 +313,8 @@ section show ite (bidx = bidx) _ _ = _, by rw if_pos rfl, begin simp[array.iterate_aux, -add_comm], - rw [-(show bidx = ⟨bidx.1, h⟩, from fin.eq_of_veq rfl), - -valid.modify_aux1 _ _ (le_refl _), + rw [← show bidx = ⟨bidx.1, h⟩, from fin.eq_of_veq rfl, + ← valid.modify_aux1 _ _ (le_refl _), this, hfl, hl], exact λvv, let ⟨s, v, nd, al, e⟩ := _root_.hash_map.valid_aux.unfold_cons vv in @@ -520,7 +520,7 @@ end, list.disjoint_of_nodup_append nd' (list.mem_map sigma.fst m1) this, if h : mk_idx n' (hash_fn c.1) = i then by simp[h] at im; exact or.elim im - (λe, nc $ list.mem_append_left _ (by rwa -(show a = c.fst, from congr_arg sigma.fst e))) + (λe, nc $ list.mem_append_left _ (by rwa [← show a = c.fst, from congr_arg sigma.fst e])) this else by simp[h] at im; exact this im end @@ -624,10 +624,10 @@ match (by apply_instance : decidable (contains_aux a bkt)) with from h.trans $ (list.mem_reverse _ _).trans this, have h : bkts'' = bkts'.as_list.foldl _ _, from bkts'.foldl_eq _ _, begin - rw -list.foldr_reverse at h, rw h, + rw [← list.foldr_reverse] at h, rw h, generalize bkts'.as_list.reverse l, intro l, induction l with a l IH, { simp, rw[mk_as_list hash_fn n'], simp }, - { cases a with a'' b'', simp, rw -IH, exact + { cases a with a'' b'', simp, rw [← IH], exact let B := l.foldr (λ y (x : bucket_array α β n'), reinsert_aux hash_fn x y.1 y.2) (mk_array n'.1 []), ⟨u, w, hl, hfl⟩ := show ∃ u' w', B.as_list = _ ∧ @@ -680,7 +680,7 @@ match (by apply_instance : decidable (contains_aux a bkt)) with append_of_modify u' [⟨a, b⟩] [] _ hl' hfl', v.as_list_nodup _ with | ._, ._, ⟨u, w, rfl, rfl⟩, nd' := by simp; simp at nd'; exact ⟨λhm, ⟨λe, match a', e, b', hm with ._, rfl, b', hm := by { - rw -list.mem_append_iff at hm; + rw [← list.mem_append_iff] at hm; have hm := list.mem_map sigma.fst hm; rw list.map_append at hm; exact list.not_mem_of_nodup_cons (list.nodup_head nd') hm } diff --git a/library/data/stream.lean b/library/data/stream.lean index 4a39389c46..ceb615ba51 100644 --- a/library/data/stream.lean +++ b/library/data/stream.lean @@ -118,10 +118,10 @@ lemma head_map (s : stream α) : head (map f s) = f (head s) := rfl lemma map_eq (s : stream α) : map f s = f (head s) :: map f (tail s) := -by rw [-stream.eta (map f s), tail_map, head_map] +by rw [← stream.eta (map f s), tail_map, head_map] lemma map_cons (a : α) (s : stream α) : map f (a :: s) = f a :: map f s := -begin rw [-stream.eta (map f (a :: s)), map_eq], reflexivity end +begin rw [← stream.eta (map f (a :: s)), map_eq], reflexivity end lemma map_id (s : stream α) : map id s = s := rfl @@ -153,7 +153,7 @@ lemma tail_zip (s₁ : stream α) (s₂ : stream β) : tail (zip f s₁ s₂) = rfl lemma zip_eq (s₁ : stream α) (s₂ : stream β) : zip f s₁ s₂ = f (head s₁) (head s₂) :: zip f (tail s₁) (tail s₂) := -begin rw [-stream.eta (zip f s₁ s₂)], reflexivity end +begin rw [← stream.eta (zip f s₁ s₂)], reflexivity end end zip @@ -170,7 +170,7 @@ begin end lemma tail_const (a : α) : tail (const a) = const a := -suffices tail (a :: const a) = const a, by rwa -const_eq at this, +suffices tail (a :: const a) = const a, by rwa [← const_eq] at this, rfl lemma map_const (f : α → β) (a : α) : map f (const a) = const (f a) := @@ -201,7 +201,7 @@ end lemma iterate_eq (f : α → α) (a : α) : iterate f a = a :: iterate f (f a) := begin - rw [-stream.eta (iterate f a)], + rw [← stream.eta (iterate f a)], rw tail_iterate, reflexivity end @@ -234,7 +234,7 @@ assume hh ht₁ ht₂, eq_of_bisim (λ s₁ s₂, head s₁ = head s₂ ∧ s₁ = tail s₁ ∧ s₂ = tail s₂) (λ s₁ s₂ ⟨h₁, h₂, h₃⟩, begin - constructor, exact h₁, rw [-h₂, -h₃], repeat {constructor, repeat {assumption}} + constructor, exact h₁, rw [← h₂, ← h₃], repeat {constructor, repeat {assumption}} end) (and.intro hh (and.intro ht₁ ht₂)) @@ -484,7 +484,7 @@ begin induction n with n ih, { have aux := h 1, unfold approx at aux, injection aux }, { have h₁ : some (nth (succ n) s₁) = some (nth (succ n) s₂), - { rw [-nth_approx, -nth_approx, h (succ (succ n))] }, + { rw [← nth_approx, ← nth_approx, h (succ (succ n))] }, injection h₁ } end @@ -572,7 +572,7 @@ lemma nth_inits : ∀ (n : nat) (s : stream α), nth n (inits s) = approx (succ begin intro n, induction n with n' ih, {intros, reflexivity}, - {intros, rw [nth_succ, approx_succ, -ih, tail_inits, inits_tail, cons_nth_inits_core]} + {intros, rw [nth_succ, approx_succ, ← ih, tail_inits, inits_tail, cons_nth_inits_core]} end lemma inits_eq (s : stream α) : inits s = [head s] :: map (list.cons (head s)) (inits (tail s)) := diff --git a/library/init/algebra/field.lean b/library/init/algebra/field.lean index 61fa81e376..9306ec2bad 100644 --- a/library/init/algebra/field.lean +++ b/library/init/algebra/field.lean @@ -73,7 +73,7 @@ by simp lemma one_div_ne_zero {a : α} (h : a ≠ 0) : 1 / a ≠ 0 := assume : 1 / a = 0, -have 0 = (1:α), from eq.symm (by rw [-(mul_one_div_cancel h), this, mul_zero]), +have 0 = (1:α), from eq.symm (by rw [← mul_one_div_cancel h, this, mul_zero]), absurd this zero_ne_one lemma one_inv_eq : 1⁻¹ = (1:α) := @@ -92,7 +92,7 @@ by simp -- domain, but let's not define that class for now. lemma division_ring.mul_ne_zero {a b : α} (ha : a ≠ 0) (hb : b ≠ 0) : a * b ≠ 0 := assume : a * b = 0, -have a * 1 = 0, by rw [-(mul_one_div_cancel hb), -mul_assoc, this, zero_mul], +have a * 1 = 0, by rw [← mul_one_div_cancel hb, ← mul_assoc, this, zero_mul], have a = 0, by rwa mul_one at this, absurd this ha @@ -114,11 +114,11 @@ have a ≠ 0, from assume : a = 0, have 0 = (1:α), by rwa [this, mul_zero] at h, absurd this zero_ne_one, -by rw [-h, mul_div_assoc, div_self this, mul_one] +by rw [← h, mul_div_assoc, div_self this, mul_one] lemma division_ring.one_div_mul_one_div {a b : α} (ha : a ≠ 0) (hb : b ≠ 0) : (1 / a) * (1 / b) = 1 / (b * a) := have (b * a) * ((1 / a) * (1 / b)) = 1, - by rw [mul_assoc, -(mul_assoc a), mul_one_div_cancel ha, one_mul, mul_one_div_cancel hb], + by rw [mul_assoc, ← mul_assoc a, mul_one_div_cancel ha, one_mul, mul_one_div_cancel hb], eq_one_div_of_mul_eq_one this lemma one_div_neg_one_eq_neg_one : (1:α) / (-1) = -1 := @@ -139,13 +139,13 @@ calc lemma div_neg_eq_neg_div {a : α} (b : α) (ha : a ≠ 0) : b / (- a) = - (b / a) := calc - b / (- a) = b * (1 / (- a)) : by rw [-inv_eq_one_div, division_def] + b / (- a) = b * (1 / (- a)) : by rw [← inv_eq_one_div, division_def] ... = b * -(1 / a) : by rw (division_ring.one_div_neg_eq_neg_one_div ha) ... = -(b * (1 / a)) : by rw neg_mul_eq_mul_neg ... = - (b * a⁻¹) : by rw inv_eq_one_div lemma neg_div (a b : α) : (-b) / a = - (b / a) := -by rw [neg_eq_neg_one_mul, mul_div_assoc, -neg_eq_neg_one_mul] +by rw [neg_eq_neg_one_mul, mul_div_assoc, ← neg_eq_neg_one_mul] lemma division_ring.neg_div_neg_eq (a : α) {b : α} (hb : b ≠ 0) : (-a) / (-b) = a / b := by rw [(div_neg_eq_neg_div _ hb), neg_div, neg_neg] @@ -154,7 +154,7 @@ lemma division_ring.one_div_one_div {a : α} (h : a ≠ 0) : 1 / (1 / a) = a := eq.symm (eq_one_div_of_mul_eq_one_left (mul_one_div_cancel h)) lemma division_ring.eq_of_one_div_eq_one_div {a b : α} (ha : a ≠ 0) (hb : b ≠ 0) (h : 1 / a = 1 / b) : a = b := -by rw [-(division_ring.one_div_one_div ha), h, (division_ring.one_div_one_div hb)] +by rw [← division_ring.one_div_one_div ha, h, (division_ring.one_div_one_div hb)] lemma mul_inv_eq {a b : α} (ha : a ≠ 0) (hb : b ≠ 0) : (b * a)⁻¹ = a⁻¹ * b⁻¹ := eq.symm $ calc @@ -172,7 +172,7 @@ lemma div_add_div_same (a b c : α) : a / c + b / c = (a + b) / c := eq.symm $ right_distrib a b (c⁻¹) lemma div_sub_div_same (a b c : α) : (a / c) - (b / c) = (a - b) / c := -by rw [sub_eq_add_neg, -neg_div, div_add_div_same, sub_eq_add_neg] +by rw [sub_eq_add_neg, ← neg_div, div_add_div_same, sub_eq_add_neg] lemma one_div_mul_add_mul_one_div_eq_one_div_add_one_div {a b : α} (ha : a ≠ 0) (hb : b ≠ 0) : (1 / a) * (a + b) * (1 / b) = 1 / a + 1 / b := @@ -198,7 +198,7 @@ iff.mp $ div_eq_one_iff_eq a Hb lemma eq_div_iff_mul_eq (a b : α) {c : α} (hc : c ≠ 0) : a = b / c ↔ a * c = b := iff.intro (assume : a = b / c, by rw [this, (div_mul_cancel _ hc)]) - (assume : a * c = b, by rw [-this, mul_div_cancel _ hc]) + (assume : a * c = b, by rw [← this, mul_div_cancel _ hc]) lemma eq_div_of_mul_eq (a b : α) {c : α} (hc : c ≠ 0) : a * c = b → a = b / c := iff.mpr $ eq_div_iff_mul_eq a b hc @@ -227,7 +227,7 @@ by rw [(division_ring.one_div_mul_one_div ha hb), mul_comm b] lemma field.div_mul_right {a b : α} (hb : b ≠ 0) (h : a * b ≠ 0) : a / (a * b) = 1 / b := have a ≠ 0, from ne_zero_of_mul_ne_zero_right h, eq.symm (calc - 1 / b = a * ((1 / a) * (1 / b)) : by rw [-mul_assoc, mul_one_div_cancel this, one_mul] + 1 / b = a * ((1 / a) * (1 / b)) : by rw [← mul_assoc, mul_one_div_cancel this, one_mul] ... = a * (1 / (b * a)) : by rw (division_ring.one_div_mul_one_div this hb) ... = a * (a * b)⁻¹ : by rw [inv_eq_one_div, mul_comm a b]) @@ -243,8 +243,8 @@ by rw [mul_comm, (div_mul_cancel _ hb)] lemma one_div_add_one_div {a b : α} (ha : a ≠ 0) (hb : b ≠ 0) : 1 / a + 1 / b = (a + b) / (a * b) := have a * b ≠ 0, from (division_ring.mul_ne_zero ha hb), -by rw [add_comm, -(field.div_mul_left ha this), -(field.div_mul_right hb this), - division_def, division_def, division_def, -right_distrib] +by rw [add_comm, ← field.div_mul_left ha this, ← field.div_mul_right hb this, + division_def, division_def, division_def, ← right_distrib] lemma field.div_mul_div (a : α) {b : α} (c : α) {d : α} (hb : b ≠ 0) (hd : d ≠ 0) : (a / b) * (c / d) = (a * c) / (b * d) := @@ -252,7 +252,7 @@ begin simp [division_def], rw [mul_inv_eq hd hb, mul_comm d⁻¹] end lemma mul_div_mul_left (a : α) {b c : α} (hb : b ≠ 0) (hc : c ≠ 0) : (c * a) / (c * b) = a / b := -by rw [-(field.div_mul_div _ _ hc hb), div_self hc, one_mul] +by rw [← field.div_mul_div _ _ hc hb, div_self hc, one_mul] lemma mul_div_mul_right (a : α) {b c : α} (hb : b ≠ 0) (hc : c ≠ 0) : (a * c) / (b * c) = a / b := @@ -263,25 +263,25 @@ by simp [division_def] lemma field.div_mul_eq_mul_div_comm (a b : α) {c : α} (hc : c ≠ 0) : (b / c) * a = b * (a / c) := -by rw [div_mul_eq_mul_div, -(one_mul c), -(field.div_mul_div _ _ (ne.symm zero_ne_one) hc), +by rw [div_mul_eq_mul_div, ← one_mul c, ← field.div_mul_div _ _ (ne.symm zero_ne_one) hc, div_one, one_mul] lemma div_add_div (a : α) {b : α} (c : α) {d : α} (hb : b ≠ 0) (hd : d ≠ 0) : (a / b) + (c / d) = ((a * d) + (b * c)) / (b * d) := -by rw [-(mul_div_mul_right _ hb hd), -(mul_div_mul_left _ hd hb), div_add_div_same] +by rw [← mul_div_mul_right _ hb hd, ← mul_div_mul_left _ hd hb, div_add_div_same] lemma div_sub_div (a : α) {b : α} (c : α) {d : α} (hb : b ≠ 0) (hd : d ≠ 0) : (a / b) - (c / d) = ((a * d) - (b * c)) / (b * d) := begin simp [sub_eq_add_neg], - rw [neg_eq_neg_one_mul, -mul_div_assoc, div_add_div _ _ hb hd, - -mul_assoc, mul_comm b, mul_assoc, -neg_eq_neg_one_mul] + rw [neg_eq_neg_one_mul, ← mul_div_assoc, div_add_div _ _ hb hd, + ← mul_assoc, mul_comm b, mul_assoc, ← neg_eq_neg_one_mul] end lemma mul_eq_mul_of_div_eq_div (a : α) {b : α} (c : α) {d : α} (hb : b ≠ 0) (hd : d ≠ 0) (h : a / b = c / d) : a * d = c * b := -by rw [-(mul_one (a*d)), mul_assoc, (mul_comm d), -mul_assoc, -(div_self hb), - -(field.div_mul_eq_mul_div_comm _ _ hb), h, div_mul_eq_mul_div, div_mul_cancel _ hd] +by rw [← mul_one (a*d), mul_assoc, mul_comm d, ← mul_assoc, ← div_self hb, + ← field.div_mul_eq_mul_div_comm _ _ hb, h, div_mul_eq_mul_div, div_mul_cancel _ hd] lemma field.one_div_div {a b : α} (ha : a ≠ 0) (hb : b ≠ 0) : 1 / (a / b) = b / a := have (a / b) * (b / a) = 1, from calc @@ -292,7 +292,7 @@ eq.symm (eq_one_div_of_mul_eq_one this) lemma field.div_div_eq_mul_div (a : α) {b c : α} (hb : b ≠ 0) (hc : c ≠ 0) : a / (b / c) = (a * c) / b := -by rw [div_eq_mul_one_div, field.one_div_div hb hc, -mul_div_assoc] +by rw [div_eq_mul_one_div, field.one_div_div hb hc, ← mul_div_assoc] lemma field.div_div_eq_div_mul (a : α) {b c : α} (hb : b ≠ 0) (hc : c ≠ 0) : (a / b) / c = a / (b * c) := @@ -305,13 +305,13 @@ by rw [field.div_div_eq_mul_div _ hc hd, div_mul_eq_mul_div, lemma field.div_mul_eq_div_mul_one_div (a : α) {b c : α} (hb : b ≠ 0) (hc : c ≠ 0) : a / (b * c) = (a / b) * (1 / c) := -by rw [-(field.div_div_eq_div_mul _ hb hc), -div_eq_mul_one_div] +by rw [← field.div_div_eq_div_mul _ hb hc, ← div_eq_mul_one_div] lemma eq_of_mul_eq_mul_of_nonzero_left {a b c : α} (h : a ≠ 0) (h₂ : a * b = a * c) : b = c := -by rw [-one_mul b, -div_self h, div_mul_eq_mul_div, h₂, mul_div_cancel_left _ h] +by rw [← one_mul b, ← div_self h, div_mul_eq_mul_div, h₂, mul_div_cancel_left _ h] lemma eq_of_mul_eq_mul_of_nonzero_right {a b c : α} (h : c ≠ 0) (h2 : a * c = b * c) : a = b := -by rw [-mul_one a, -div_self h, -mul_div_assoc, h2, mul_div_cancel _ h] +by rw [← mul_one a, ← div_self h, ← mul_div_assoc, h2, mul_div_cancel _ h] end field @@ -332,7 +332,7 @@ lemma discrete_field.eq_zero_or_eq_zero_of_mul_eq_zero decidable.by_cases (assume : a = 0, or.inl this) (assume : a ≠ 0, - or.inr (by rw [-(one_mul b), -(inv_mul_cancel this), mul_assoc, h, mul_zero])) + or.inr (by rw [← one_mul b, ← inv_mul_cancel this, mul_assoc, h, mul_zero])) instance discrete_field.to_integral_domain [s : discrete_field α] : integral_domain α := {s with @@ -386,7 +386,7 @@ decidable.by_cases lemma eq_of_one_div_eq_one_div {a b : α} (h : 1 / a = 1 / b) : a = b := decidable.by_cases (assume ha : a = 0, - have hb : b = 0, from eq_zero_of_one_div_eq_zero (by rw [-h, ha, div_zero]), + have hb : b = 0, from eq_zero_of_one_div_eq_zero (by rw [← h, ha, div_zero]), hb.symm ▸ ha) (assume ha : a ≠ 0, have hb : b ≠ 0, from ne_zero_of_one_div_ne_zero (h ▸ (one_div_ne_zero ha)), @@ -442,7 +442,7 @@ decidable.by_cases (assume hb : b ≠ 0, field.one_div_div ha hb)) lemma div_div_eq_mul_div (a b c : α) : a / (b / c) = (a * c) / b := -by rw [div_eq_mul_one_div, one_div_div, -mul_div_assoc] +by rw [div_eq_mul_one_div, one_div_div, ← mul_div_assoc] lemma div_div_eq_div_mul (a b c : α) : (a / b) / c = a / (b * c) := by rw [div_eq_mul_one_div, div_mul_div, mul_one] @@ -454,6 +454,6 @@ lemma div_helper {a : α} (b : α) (h : a ≠ 0) : (1 / (a * b)) * a = 1 / b := by rw [div_mul_eq_mul_div, one_mul, div_mul_right _ h] lemma div_mul_eq_div_mul_one_div (a b c : α) : a / (b * c) = (a / b) * (1 / c) := -by rw [-div_div_eq_div_mul, -div_eq_mul_one_div] +by rw [← div_div_eq_div_mul, ← div_eq_mul_one_div] end discrete_field diff --git a/library/init/algebra/functions.lean b/library/init/algebra/functions.lean index 99a86ccf3c..0875bfad39 100644 --- a/library/init/algebra/functions.lean +++ b/library/init/algebra/functions.lean @@ -216,7 +216,7 @@ lemma abs_pos_of_neg {a : α} (h : a < 0) : abs a > 0 := abs_neg a ▸ abs_pos_of_pos (neg_pos_of_neg h) lemma abs_sub (a b : α) : abs (a - b) = abs (b - a) := -by rw [-neg_sub, abs_neg] +by rw [← neg_sub, abs_neg] lemma ne_zero_of_abs_ne_zero {a : α} (h : abs a ≠ 0) : a ≠ 0 := assume ha, h (eq.symm ha ▸ abs_zero) @@ -321,9 +321,9 @@ or.elim (le_total 0 (a + b)) (assume h2 : a + b ≤ 0, have h3 : -a + -b = -(a + b), by rw neg_add, have h4 : -(a + b) ≥ 0, from neg_nonneg_of_nonpos h2, - have h5 : -a + -b ≥ 0, begin rw -h3 at h4, exact h4 end, + have h5 : -a + -b ≥ 0, begin rw [← h3] at h4, exact h4 end, calc - abs (a + b) = abs (-a + -b) : by rw [-abs_neg, neg_add] + abs (a + b) = abs (-a + -b) : by rw [← abs_neg, neg_add] ... ≤ abs (-a) + abs (-b) : aux2 h5 ... = abs a + abs b : by rw [abs_neg, abs_neg]) @@ -457,7 +457,7 @@ begin apply sub_le_sub_left, repeat {rw mul_assoc}, apply mul_le_mul_of_nonneg_left, - rw -abs_mul, + rw [← abs_mul], apply le_abs_self, apply le_of_lt, apply add_pos, @@ -477,7 +477,7 @@ decidable.by_cases have h₁ : abs b ≠ 0, from assume h₂, h (eq_zero_of_abs_eq_zero h₂), eq_div_of_mul_eq _ _ h₁ - (show abs (a / b) * abs b = abs a, by rw [-abs_mul, div_mul_cancel _ h])) + (show abs (a / b) * abs b = abs a, by rw [← abs_mul, div_mul_cancel _ h])) lemma abs_one_div (a : α) : abs (1 / a) = 1 / abs a := by rw [abs_div, abs_of_nonneg (zero_le_one : 1 ≥ (0 : α))] diff --git a/library/init/algebra/group.lean b/library/init/algebra/group.lean index 260696a495..818bcac476 100644 --- a/library/init/algebra/group.lean +++ b/library/init/algebra/group.lean @@ -79,13 +79,13 @@ group.mul_left_inv def inv_mul_self := @mul_left_inv @[simp] lemma inv_mul_cancel_left [group α] (a b : α) : a⁻¹ * (a * b) = b := -by rw [-mul_assoc, mul_left_inv, one_mul] +by rw [← mul_assoc, mul_left_inv, one_mul] @[simp] lemma inv_mul_cancel_right [group α] (a b : α) : a * b⁻¹ * b = a := by simp @[simp] lemma inv_eq_of_mul_eq_one [group α] {a b : α} (h : a * b = 1) : a⁻¹ = b := -by rw [-mul_one a⁻¹, -h, -mul_assoc, mul_left_inv, one_mul] +by rw [← mul_one a⁻¹, ←h, ←mul_assoc, mul_left_inv, one_mul] @[simp] lemma one_inv [group α] : 1⁻¹ = (1 : α) := inv_eq_of_mul_eq_one (one_mul 1) @@ -118,13 +118,13 @@ instance group.to_right_cancel_semigroup [s : group α] : right_cancel_semigroup { s with mul_right_cancel := @group.mul_right_cancel α s } lemma mul_inv_cancel_left [group α] (a b : α) : a * (a⁻¹ * b) = b := -by rw [-mul_assoc, mul_right_inv, one_mul] +by rw [← mul_assoc, mul_right_inv, one_mul] lemma mul_inv_cancel_right [group α] (a b : α) : a * b * b⁻¹ = a := by rw [mul_assoc, mul_right_inv, mul_one] @[simp] lemma mul_inv_rev [group α] (a b : α) : (a * b)⁻¹ = b⁻¹ * a⁻¹ := -inv_eq_of_mul_eq_one begin rw [mul_assoc, -mul_assoc b, mul_right_inv, one_mul, mul_right_inv] end +inv_eq_of_mul_eq_one begin rw [mul_assoc, ← mul_assoc b, mul_right_inv, one_mul, mul_right_inv] end lemma eq_inv_of_eq_inv [group α] {a b : α} (h : a = b⁻¹) : b = a⁻¹ := by simp [h] @@ -332,7 +332,7 @@ lemma add_sub_cancel [add_group α] (a b : α) : a + b - b = a := add_neg_cancel_right a b lemma add_sub_assoc [add_group α] (a b c : α) : a + b - c = a + (b - c) := -by rw [sub_eq_add_neg, add_assoc, -sub_eq_add_neg] +by rw [sub_eq_add_neg, add_assoc, ←sub_eq_add_neg] lemma eq_of_sub_eq_zero [add_group α] {a b : α} (h : a - b = 0) : a = b := have 0 + b = b, by rw zero_add, diff --git a/library/init/algebra/norm_num.lean b/library/init/algebra/norm_num.lean index c5ef8cc22f..77a951df04 100644 --- a/library/init/algebra/norm_num.lean +++ b/library/init/algebra/norm_num.lean @@ -36,7 +36,7 @@ lemma mul_bit0 [distrib α] (a b : α) : a * (bit0 b) = bit0 (a * b) := by simp lemma mul_bit0_helper [distrib α] (a b t : α) (h : a * b = t) : a * (bit0 b) = bit0 t := -begin rw [-h], simp end +begin rw [← h], simp end lemma mul_bit1 [semiring α] (a b : α) : a * (bit1 b) = bit0 (a * b) + a := by simp @@ -71,7 +71,7 @@ lemma neg_add_pos_helper2 [add_comm_group α] (a b c : α) (h : a + c = b) : -a begin apply neg_add_eq_of_eq_add, rw h end lemma pos_add_neg_helper [add_comm_group α] (a b c : α) (h : b + a = c) : a + b = c := -by rw [-h, add_comm a b] +by rw [← h, add_comm a b] lemma subst_into_subtr [add_group α] (l r t : α) (h : l + -r = t) : l - r = t := by simp [h] @@ -92,23 +92,23 @@ lemma div_add_helper [field α] (n d b c val : α) (hd : d ≠ 0) (h : n + b * d (h2 : c * d = val) : n / d + b = c := begin apply eq_of_mul_eq_mul_of_nonzero_right hd, - rw [h2, -h, right_distrib, div_mul_cancel _ hd] + rw [h2, ← h, right_distrib, div_mul_cancel _ hd] end lemma add_div_helper [field α] (n d b c val : α) (hd : d ≠ 0) (h : d * b + n = val) (h2 : d * c = val) : b + n / d = c := begin apply eq_of_mul_eq_mul_of_nonzero_left hd, - rw [h2, -h, left_distrib, mul_div_cancel' _ hd] + rw [h2, ← h, left_distrib, mul_div_cancel' _ hd] end lemma div_mul_helper [field α] (n d c v : α) (hd : d ≠ 0) (h : (n * c) / d = v) : (n / d) * c = v := -by rw [-h, field.div_mul_eq_mul_div_comm _ _ hd, mul_div_assoc] +by rw [← h, field.div_mul_eq_mul_div_comm _ _ hd, mul_div_assoc] lemma mul_div_helper [field α] (a n d v : α) (hd : d ≠ 0) (h : (a * n) / d = v) : a * (n / d) = v := -by rw [-h, mul_div_assoc] +by rw [← h, mul_div_assoc] lemma nonzero_of_div_helper [field α] (a b : α) (ha : a ≠ 0) (hb : b ≠ 0) : a / b ≠ 0 := begin @@ -153,14 +153,14 @@ by usimp lemma bit0_add_bit0_helper [add_comm_semigroup α] (a b t : α) (h : a + b = t) : bit0 a + bit0 b = bit0 t := -begin rw -h, usimp end +begin rw [← h], usimp end lemma bit1_add_bit0 [add_comm_semigroup α] [has_one α] (a b : α) : bit1 a + bit0 b = bit1 (a + b) := by usimp lemma bit1_add_bit0_helper [add_comm_semigroup α] [has_one α] (a b t : α) (h : a + b = t) : bit1 a + bit0 b = bit1 t := -begin rw -h, usimp end +begin rw [← h], usimp end lemma bit0_add_bit1 [add_comm_semigroup α] [has_one α] (a b : α) : bit0 a + bit1 b = bit1 (a + b) := @@ -168,7 +168,7 @@ by usimp lemma bit0_add_bit1_helper [add_comm_semigroup α] [has_one α] (a b t : α) (h : a + b = t) : bit0 a + bit1 b = bit1 t := -begin rw -h, usimp end +begin rw [← h], usimp end lemma bit1_add_bit1 [add_comm_semigroup α] [has_one α] (a b : α) : bit1 a + bit1 b = bit0 (add1 (a + b)) := @@ -176,7 +176,7 @@ by usimp lemma bit1_add_bit1_helper [add_comm_semigroup α] [has_one α] (a b t s : α) (h : (a + b) = t) (h2 : add1 t = s) : bit1 a + bit1 b = bit0 s := -begin rw -h at h2, rw -h2, usimp end +begin rw [← h] at h2, rw [← h2], usimp end lemma bin_add_zero [add_monoid α] (a : α) : a + 0 = a := by simp @@ -195,14 +195,14 @@ rfl lemma bit1_add_one_helper [has_add α] [has_one α] (a t : α) (h : add1 (bit1 a) = t) : bit1 a + 1 = t := -by rw -h +by rw [← h] lemma one_add_bit1 [add_comm_semigroup α] [has_one α] (a : α) : 1 + bit1 a = add1 (bit1 a) := begin unfold bit0 bit1 add1, simp end lemma one_add_bit1_helper [add_comm_semigroup α] [has_one α] (a t : α) (h : add1 (bit1 a) = t) : 1 + bit1 a = t := -begin rw -h, usimp end +begin rw [← h], usimp end lemma add1_bit0 [has_add α] [has_one α] (a : α) : add1 (bit0 a) = bit1 a := rfl @@ -213,7 +213,7 @@ by usimp lemma add1_bit1_helper [add_comm_semigroup α] [has_one α] (a t : α) (h : add1 a = t) : add1 (bit1 a) = bit0 t := -begin rw -h, usimp end +begin rw [← h], usimp end lemma add1_one [has_add α] [has_one α] : add1 (1 : α) = bit0 1 := rfl @@ -226,7 +226,7 @@ rfl lemma subst_into_sum [has_add α] (l r tl tr t : α) (prl : l = tl) (prr : r = tr) (prt : tl + tr = t) : l + r = t := -by rw [-prt, prr, prl] +by rw [← prt, prr, prl] lemma neg_zero_helper [add_group α] (a : α) (h : a = 0) : - a = 0 := begin rw h, simp end @@ -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 [*], 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 [*], rw [-hced, nat.add_sub_cancel] +simp *, rw [← hced, nat.add_sub_cancel] end end norm_num diff --git a/library/init/algebra/ordered_field.lean b/library/init/algebra/ordered_field.lean index df40f8aaf4..a6b95a4d98 100644 --- a/library/init/algebra/ordered_field.lean +++ b/library/init/algebra/ordered_field.lean @@ -287,7 +287,7 @@ by rw [add_sub_cancel] lemma add_midpoint {a b : α} (h : a < b) : a + (b - a) / 2 < b := begin - rw [-div_sub_div_same, sub_eq_add_neg, add_comm (b/2), -add_assoc, -sub_eq_add_neg], + rw [← div_sub_div_same, sub_eq_add_neg, add_comm (b/2), ← add_assoc, ← sub_eq_add_neg], apply add_lt_of_lt_sub_right, rw [sub_self_div_two, sub_self_div_two], apply div_lt_div_of_lt_of_pos h two_pos @@ -315,7 +315,7 @@ add_pos two_pos two_pos lemma mul_le_mul_of_mul_div_le {a b c d : α} (h : a * (b / c) ≤ d) (hc : c > 0) : b * a ≤ d * c := begin - rw [-mul_div_assoc] at h, rw [mul_comm b], + rw [← mul_div_assoc] at h, rw [mul_comm b], apply le_mul_of_div_le hc h end @@ -350,7 +350,7 @@ begin have h3 : (a + a) / 2 > ((b + b) + (a - b)) / 2, exact div_lt_div_of_lt_of_pos h2 two_pos, rw [one_add_one_eq_two, sub_eq_add_neg], - rw [add_self_div_two, -div_add_div_same, add_self_div_two, sub_eq_add_neg] at h3, + rw [add_self_div_two, ← div_add_div_same, add_self_div_two, sub_eq_add_neg] at h3, exact h3}, exact div_pos_of_pos_of_pos (sub_pos_of_lt h) two_pos end @@ -459,7 +459,7 @@ le_of_not_gt lemma one_div_le_of_one_div_le_of_pos {a b : α} (ha : a > 0) (h : 1 / a ≤ b) : 1 / b ≤ a := begin - rw -(one_div_one_div a), + rw [← one_div_one_div a], apply one_div_le_one_div_of_le, apply one_div_pos_of_pos, repeat {assumption} @@ -467,7 +467,7 @@ end lemma one_div_le_of_one_div_le_of_neg {a b : α} (ha : b < 0) (h : 1 / a ≤ b) : 1 / b ≤ a := begin - rw -(one_div_one_div a), + rw [← one_div_one_div a], apply one_div_le_one_div_of_le_of_neg, repeat {assumption} end @@ -491,7 +491,7 @@ one_div_le_one_div_of_le_of_neg h1 h2 lemma div_lt_div_of_pos_of_lt_of_pos {a b c : α} (hb : 0 < b) (h : b < a) (hc : 0 < c) : c / a < c / b := begin apply lt_of_sub_neg, - rw [div_eq_mul_one_div, div_eq_mul_one_div c b, -mul_sub_left_distrib], + rw [div_eq_mul_one_div, div_eq_mul_one_div c b, ← mul_sub_left_distrib], apply mul_neg_of_pos_of_neg, exact hc, apply sub_neg_of_lt, diff --git a/library/init/algebra/ordered_group.lean b/library/init/algebra/ordered_group.lean index 49763175e7..343ba77136 100644 --- a/library/init/algebra/ordered_group.lean +++ b/library/init/algebra/ordered_group.lean @@ -347,7 +347,7 @@ end lemma add_le_of_le_sub_left {a b c : α} (h : b ≤ c - a) : a + b ≤ c := begin have h := add_le_add_left h a, - rwa [-add_sub_assoc, add_comm a c, add_sub_cancel] at h + rwa [← add_sub_assoc, add_comm a c, add_sub_cancel] at h end lemma le_sub_left_of_add_le {a b c : α} (h : a + b ≤ c) : b ≤ c - a := @@ -470,7 +470,7 @@ end lemma add_lt_of_lt_sub_left {a b c : α} (h : b < c - a) : a + b < c := begin have h := add_lt_add_left h a, - rwa [-add_sub_assoc, add_comm a c, add_sub_cancel] at h + rwa [← add_sub_assoc, add_comm a c, add_sub_cancel] at h end lemma lt_sub_left_of_add_lt {a b c : α} (h : a + b < c) : b < c - a := diff --git a/library/init/algebra/ordered_ring.lean b/library/init/algebra/ordered_ring.lean index 8ea58dd681..727c2b9e5a 100644 --- a/library/init/algebra/ordered_ring.lean +++ b/library/init/algebra/ordered_ring.lean @@ -227,13 +227,13 @@ variable [ordered_ring α] lemma mul_le_mul_of_nonpos_left {a b c : α} (h : b ≤ a) (hc : c ≤ 0) : c * a ≤ c * b := have -c ≥ 0, from neg_nonneg_of_nonpos hc, have -c * b ≤ -c * a, from mul_le_mul_of_nonneg_left h this, -have -(c * b) ≤ -(c * a), by rwa [-neg_mul_eq_neg_mul, -neg_mul_eq_neg_mul] at this, +have -(c * b) ≤ -(c * a), by rwa [← neg_mul_eq_neg_mul, ← neg_mul_eq_neg_mul] at this, le_of_neg_le_neg this lemma mul_le_mul_of_nonpos_right {a b c : α} (h : b ≤ a) (hc : c ≤ 0) : a * c ≤ b * c := have -c ≥ 0, from neg_nonneg_of_nonpos hc, have b * -c ≤ a * -c, from mul_le_mul_of_nonneg_right h this, -have -(b * c) ≤ -(a * c), by rwa [-neg_mul_eq_mul_neg, -neg_mul_eq_mul_neg] at this, +have -(b * c) ≤ -(a * c), by rwa [← neg_mul_eq_mul_neg, ← neg_mul_eq_mul_neg] at this, le_of_neg_le_neg this lemma mul_nonneg_of_nonpos_of_nonpos {a b : α} (ha : a ≤ 0) (hb : b ≤ 0) : 0 ≤ a * b := @@ -243,13 +243,13 @@ by rwa zero_mul at this lemma mul_lt_mul_of_neg_left {a b c : α} (h : b < a) (hc : c < 0) : c * a < c * b := have -c > 0, from neg_pos_of_neg hc, have -c * b < -c * a, from mul_lt_mul_of_pos_left h this, -have -(c * b) < -(c * a), by rwa [-neg_mul_eq_neg_mul, -neg_mul_eq_neg_mul] at this, +have -(c * b) < -(c * a), by rwa [← neg_mul_eq_neg_mul, ← neg_mul_eq_neg_mul] at this, lt_of_neg_lt_neg this lemma mul_lt_mul_of_neg_right {a b c : α} (h : b < a) (hc : c < 0) : a * c < b * c := have -c > 0, from neg_pos_of_neg hc, have b * -c < a * -c, from mul_lt_mul_of_pos_right h this, -have -(b * c) < -(a * c), by rwa [-neg_mul_eq_mul_neg, -neg_mul_eq_mul_neg] at this, +have -(b * c) < -(a * c), by rwa [← neg_mul_eq_mul_neg, ← neg_mul_eq_mul_neg] at this, lt_of_neg_lt_neg this lemma mul_pos_of_neg_of_neg {a b : α} (ha : a < 0) (hb : b < 0) : 0 < a * b := @@ -289,14 +289,14 @@ match lt_trichotomy 0 a with | or.inl hlt₁ := match lt_trichotomy 0 b with | or.inl hlt₂ := or.inl ⟨hlt₁, hlt₂⟩ - | or.inr (or.inl heq₂) := begin rw [-heq₂, mul_zero] at hab, exact absurd hab (lt_irrefl _) end + | or.inr (or.inl heq₂) := begin rw [← heq₂, mul_zero] at hab, exact absurd hab (lt_irrefl _) end | or.inr (or.inr hgt₂) := absurd hab (lt_asymm (mul_neg_of_pos_of_neg hlt₁ hgt₂)) end -| or.inr (or.inl heq₁) := begin rw [-heq₁, zero_mul] at hab, exact absurd hab (lt_irrefl _) end +| or.inr (or.inl heq₁) := begin rw [← heq₁, zero_mul] at hab, exact absurd hab (lt_irrefl _) end | or.inr (or.inr hgt₁) := match lt_trichotomy 0 b with | or.inl hlt₂ := absurd hab (lt_asymm (mul_neg_of_neg_of_pos hgt₁ hlt₂)) - | or.inr (or.inl heq₂) := begin rw [-heq₂, mul_zero] at hab, exact absurd hab (lt_irrefl _) end + | or.inr (or.inl heq₂) := begin rw [← heq₂, mul_zero] at hab, exact absurd hab (lt_irrefl _) end | or.inr (or.inr hgt₂) := or.inr ⟨hgt₁, hgt₂⟩ end end diff --git a/library/init/algebra/ring.lean b/library/init/algebra/ring.lean index 122826d495..687eb709a7 100644 --- a/library/init/algebra/ring.lean +++ b/library/init/algebra/ring.lean @@ -179,11 +179,11 @@ instance ring.to_semiring [s : ring α] : semiring α := lemma neg_mul_eq_neg_mul [s : ring α] (a b : α) : -(a * b) = -a * b := neg_eq_of_add_eq_zero - begin rw [-right_distrib, add_right_neg, zero_mul] end + begin rw [← right_distrib, add_right_neg, zero_mul] end lemma neg_mul_eq_mul_neg [s : ring α] (a b : α) : -(a * b) = a * -b := neg_eq_of_add_eq_zero - begin rw [-left_distrib, add_right_neg, mul_zero] end + begin rw [← left_distrib, add_right_neg, mul_zero] end @[simp] lemma neg_mul_eq_neg_mul_symm [s : ring α] (a b : α) : - a * b = - (a * b) := eq.symm (neg_mul_eq_neg_mul a b) @@ -316,7 +316,7 @@ section integral_domain iff.intro (assume : a * a = b * b, have (a - b) * (a + b) = 0, - by rewrite [mul_comm, -mul_self_sub_mul_self_eq, this, sub_self], + by rewrite [mul_comm, ← mul_self_sub_mul_self_eq, this, sub_self], have a - b = 0 ∨ a + b = 0, from eq_zero_or_eq_zero_of_mul_eq_zero this, or.elim this (assume : a - b = 0, or.inl (eq_of_sub_eq_zero this)) diff --git a/library/init/data/array/basic.lean b/library/init/data/array/basic.lean index 7687f64da1..2ffbc7afb0 100644 --- a/library/init/data/array/basic.lean +++ b/library/init/data/array/basic.lean @@ -59,7 +59,7 @@ lt_of_le_of_lt (nat.sub_le _ _) this theorem write_ind (a : array α n) (i : fin n) (v : α) (C : fin n → α → Sort w) (Hi : C i v) (Hj : ∀j, i ≠ j → C j (a.read j)) (j) : C j ((a.write i v).read j) := show C j (if i = j then v else read a j), from -if h : i = j then by rwa [if_pos h, -h] +if h : i = j then by rwa [if_pos h, ← h] else by rw [if_neg h]; exact Hj j h def foreach_aux (f : fin n → α → α) : Π (i : nat), i ≤ n → array α n → array α n diff --git a/library/init/data/array/lemmas.lean b/library/init/data/array/lemmas.lean index 1fc117fa65..4528a35f87 100644 --- a/library/init/data/array/lemmas.lean +++ b/library/init/data/array/lemmas.lean @@ -25,7 +25,7 @@ theorem rev_list_reverse (a : array α n) : a.rev_list.reverse = a.to_list := rev_list_reverse_core a _ _ _ theorem to_list_reverse (a : array α n) : a.to_list.reverse = a.rev_list := -by rw [-rev_list_reverse, list.reverse_reverse] +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; simp [*, iterate_aux] @@ -34,7 +34,7 @@ theorem rev_list_length (a : array α n) : a.rev_list.length = n := rev_list_length_aux a _ _ theorem to_list_length (a : array α n) : a.to_list.length = n := -by rw[-rev_list_reverse, list.length_reverse, rev_list_length] +by rw[← rev_list_reverse, list.length_reverse, rev_list_length] theorem to_list_nth_core (a : array α n) (i : ℕ) (ih : i < n) : Π (j) {jh t h'}, (∀k tl, j + k = i → list.nth_le t k tl = a.read ⟨i, ih⟩) → (a.rev_iterate_aux (λ _ v l, v :: l) j jh t).nth_le i h' = a.read ⟨i, ih⟩ @@ -55,7 +55,7 @@ theorem mem_iff_rev_list_mem_core (a : array α n) (v : α) : Π i (h : i ≤ n) | (i+1) h := let IH := mem_iff_rev_list_mem_core i (le_of_lt h) in ⟨λ⟨j, ji1, e⟩, or.elim (lt_or_eq_of_le $ nat.le_of_succ_le_succ ji1) (λji, list.mem_cons_of_mem _ $ IH.1 ⟨j, ji, e⟩) - (λje, by simp[iterate_aux]; apply or.inl; have H : j = ⟨i, h⟩ := fin.eq_of_veq je; rwa [-H, e]), + (λje, by simp[iterate_aux]; apply or.inl; have H : j = ⟨i, h⟩ := fin.eq_of_veq je; rwa [← H, e]), λm, begin simp[iterate_aux, list.mem] at m, cases m with e m', @@ -70,7 +70,7 @@ iff.trans (mem_iff_rev_list_mem_core a v _ _) theorem mem_iff_list_mem (a : array α n) (v : α) : v ∈ a ↔ v ∈ a.to_list := -by rw -rev_list_reverse; simp[mem_iff_rev_list_mem] +by rw [← rev_list_reverse]; simp[mem_iff_rev_list_mem] @[simp] def to_list_to_array (a : array α n) : a.to_list.to_array == a := have array.mk (λ (v : fin n), list.nth_le (to_list a) (v.val) (eq.rec_on (eq.symm (to_list_length a)) (v.is_lt))) = a, from diff --git a/library/init/data/int/basic.lean b/library/init/data/int/basic.lean index fdd29a98b0..7031f49448 100644 --- a/library/init/data/int/basic.lean +++ b/library/init/data/int/basic.lean @@ -437,7 +437,7 @@ show of_nat (n - m) = of_nat n + neg_of_nat m, from match m, h with end lemma neg_succ_of_nat_coe' (n : ℕ) : -[1+ n] = -↑n - 1 := -by rw [sub_eq_add_neg, -neg_add]; refl +by rw [sub_eq_add_neg, ← neg_add]; refl protected lemma coe_nat_sub {n m : ℕ} : n ≤ m → (↑(m - n) : ℤ) = ↑m - ↑n := of_nat_sub @@ -452,7 +452,7 @@ def to_nat : ℤ → ℕ | -[1+ n] := 0 theorem to_nat_sub (m n : ℕ) : to_nat (m - n) = m - n := -by rw -int.sub_nat_nat_eq_coe; exact sub_nat_nat_elim m n +by rw [← int.sub_nat_nat_eq_coe]; exact sub_nat_nat_elim m n (λm n i, to_nat i = m - n) (λi n, by rw [nat.add_sub_cancel_left]; refl) (λi n, by rw [add_assoc, nat.sub_eq_zero_of_le (nat.le_add_right _ _)]; refl) diff --git a/library/init/data/int/bitwise.lean b/library/init/data/int/bitwise.lean index 01ba9b4a99..efa79863b1 100644 --- a/library/init/data/int/bitwise.lean +++ b/library/init/data/int/bitwise.lean @@ -69,7 +69,7 @@ namespace int (bit_val _ _).trans $ (add_comm _ _).trans $ bodd_add_div2 _ def bit_cases_on {C : ℤ → Sort u} (n) (h : ∀ b n, C (bit b n)) : C n := - by rw -bit_decomp n; apply h + by rw [← bit_decomp n]; apply h @[simp] lemma bit_zero : bit ff 0 = 0 := rfl @@ -174,7 +174,7 @@ namespace int bitwise f (bit a m) (bit b n) = bit (f a b) (bitwise f m n) := begin cases m with m m; cases n with n n; - repeat { rw -int.coe_nat_eq <|> rw bit_coe_nat <|> rw bit_neg_succ }; + repeat { rw [← int.coe_nat_eq] <|> rw bit_coe_nat <|> rw bit_neg_succ }; unfold bitwise nat_bitwise bnot; [ ginduction f ff ff with h, ginduction f ff tt with h, @@ -187,16 +187,16 @@ namespace int end @[simp] lemma lor_bit (a m b n) : lor (bit a m) (bit b n) = bit (a || b) (lor m n) := - by rw [-bitwise_or, bitwise_bit] + by rw [← bitwise_or, bitwise_bit] @[simp] lemma land_bit (a m b n) : land (bit a m) (bit b n) = bit (a && b) (land m n) := - by rw [-bitwise_and, bitwise_bit] + by rw [← bitwise_and, bitwise_bit] @[simp] lemma ldiff_bit (a m b n) : ldiff (bit a m) (bit b n) = bit (a && bnot b) (ldiff m n) := - by rw [-bitwise_diff, bitwise_bit] + by rw [← bitwise_diff, bitwise_bit] @[simp] lemma lxor_bit (a m b n) : lxor (bit a m) (bit b n) = bit (bxor a b) (lxor m n) := - by rw [-bitwise_xor, bitwise_bit] + by rw [← bitwise_xor, bitwise_bit] @[simp] lemma lnot_bit (b) : ∀ n, lnot (bit b n) = bit (bnot b) (lnot n) | (n : ℕ) := by simp [lnot] @@ -214,16 +214,16 @@ namespace int end @[simp] lemma test_bit_lor (m n k) : test_bit (lor m n) k = test_bit m k || test_bit n k := - by rw [-bitwise_or, test_bit_bitwise] + by rw [← bitwise_or, test_bit_bitwise] @[simp] lemma test_bit_land (m n k) : test_bit (land m n) k = test_bit m k && test_bit n k := - by rw [-bitwise_and, test_bit_bitwise] + by rw [← bitwise_and, test_bit_bitwise] @[simp] lemma test_bit_ldiff (m n k) : test_bit (ldiff m n) k = test_bit m k && bnot (test_bit n k) := - by rw [-bitwise_diff, test_bit_bitwise] + by rw [← bitwise_diff, test_bit_bitwise] @[simp] lemma test_bit_lxor (m n k) : test_bit (lxor m n) k = bxor (test_bit m k) (test_bit n k) := - by rw [-bitwise_xor, test_bit_bitwise] + by rw [← bitwise_xor, test_bit_bitwise] @[simp] lemma test_bit_lnot : ∀ n k, test_bit (lnot n) k = bnot (test_bit n k) | (n : ℕ) k := by simp [lnot, test_bit] @@ -235,21 +235,21 @@ namespace int | (m : ℕ) n -[1+k] := sub_nat_nat_elim n k.succ (λ n k i, shiftl ↑m i = nat.shiftr (nat.shiftl m n) k) (λ i n, congr_arg coe $ - by rw [-nat.shiftl_sub, nat.add_sub_cancel_left]; apply nat.le_add_right) + by rw [← nat.shiftl_sub, nat.add_sub_cancel_left]; apply nat.le_add_right) (λ i n, congr_arg coe $ - by rw [add_assoc, nat.shiftr_add, -nat.shiftl_sub, nat.sub_self]; refl) + by rw [add_assoc, nat.shiftr_add, ← nat.shiftl_sub, nat.sub_self]; refl) | -[1+ m] n -[1+k] := sub_nat_nat_elim n k.succ (λ n k i, shiftl -[1+ m] i = -[1+ nat.shiftr (nat.shiftl' tt m n) k]) (λ i n, congr_arg neg_succ_of_nat $ - by rw [-nat.shiftl'_sub, nat.add_sub_cancel_left]; apply nat.le_add_right) + by rw [← nat.shiftl'_sub, nat.add_sub_cancel_left]; apply nat.le_add_right) (λ i n, congr_arg neg_succ_of_nat $ - by rw [add_assoc, nat.shiftr_add, -nat.shiftl'_sub, nat.sub_self]; refl) + by rw [add_assoc, nat.shiftr_add, ← nat.shiftl'_sub, nat.sub_self]; refl) lemma shiftl_sub (m : ℤ) (n : ℕ) (k : ℤ) : shiftl m (n - k) = shiftr (shiftl m n) k := shiftl_add _ _ _ @[simp] lemma shiftl_neg (m n : ℤ) : shiftl m (-n) = shiftr m n := rfl - @[simp] lemma shiftr_neg (m n : ℤ) : shiftr m (-n) = shiftl m n := by rw [-shiftl_neg, neg_neg] + @[simp] lemma shiftr_neg (m n : ℤ) : shiftr m (-n) = shiftl m n := by rw [← shiftl_neg, neg_neg] @[simp] lemma shiftl_coe_nat (m n : ℕ) : shiftl m n = nat.shiftl m n := rfl @[simp] lemma shiftr_coe_nat (m n : ℕ) : shiftr m n = nat.shiftr m n := by cases n; refl @@ -259,9 +259,9 @@ namespace int lemma shiftr_add : ∀ (m : ℤ) (n k : ℕ), shiftr m (n + k) = shiftr (shiftr m n) k | (m : ℕ) n k := by rw [shiftr_coe_nat, shiftr_coe_nat, - -int.coe_nat_add, shiftr_coe_nat, nat.shiftr_add] + ← int.coe_nat_add, shiftr_coe_nat, nat.shiftr_add] | -[1+ m] n k := by rw [shiftr_neg_succ, shiftr_neg_succ, - -int.coe_nat_add, shiftr_neg_succ, nat.shiftr_add] + ← int.coe_nat_add, shiftr_neg_succ, nat.shiftr_add] lemma shiftl_eq_mul_pow : ∀ (m : ℤ) (n : ℕ), shiftl m n = m * 2 ^ n | (m : ℕ) n := congr_arg coe (nat.shiftl_eq_mul_pow _ _) diff --git a/library/init/data/int/comp_lemmas.lean b/library/init/data/int/comp_lemmas.lean index c9a339cc45..e1ac0f9d4f 100644 --- a/library/init/data/int/comp_lemmas.lean +++ b/library/init/data/int/comp_lemmas.lean @@ -28,7 +28,7 @@ ne.symm (int.neg_ne_zero_of_ne (ne.symm h)) protected lemma neg_ne_of_pos {a b : ℤ} : a > 0 → b > 0 → -a ≠ b := λ h₁ h₂ h, begin - rw [-h] at h₂, + rw [← h] at h₂, exact absurd (le_of_lt h₁) (not_le_of_gt (neg_of_neg_pos h₂)) end @@ -108,13 +108,13 @@ protected lemma nat_abs_bit0 : ∀ (a : int), nat_abs (bit0 a) = bit0 (nat_abs a | (neg_succ_of_nat n) := int.nat_abs_add_neg (neg_succ_of_nat_lt_zero n) (neg_succ_of_nat_lt_zero n) protected lemma nat_abs_bit0_step {a : int} {n : nat} (h : nat_abs a = n) : nat_abs (bit0 a) = bit0 n := -begin rw [-h], apply int.nat_abs_bit0 end +begin rw [← h], apply int.nat_abs_bit0 end protected lemma nat_abs_bit1_nonneg {a : int} (h : a ≥ 0) : nat_abs (bit1 a) = bit1 (nat_abs a) := show nat_abs (bit0 a + 1) = bit0 (nat_abs a) + nat_abs 1, from by rw [int.nat_abs_add_nonneg (int.bit0_nonneg h) (le_of_lt (zero_lt_one)), int.nat_abs_bit0] protected lemma nat_abs_bit1_nonneg_step {a : int} {n : nat} (h₁ : a ≥ 0) (h₂ : nat_abs a = n) : nat_abs (bit1 a) = bit1 n := -begin rw [-h₂], apply int.nat_abs_bit1_nonneg h₁ end +begin rw [← h₂], apply int.nat_abs_bit1_nonneg h₁ end end int diff --git a/library/init/data/int/lemmas.lean b/library/init/data/int/lemmas.lean index 8dd7642d5d..0174aa2b68 100644 --- a/library/init/data/int/lemmas.lean +++ b/library/init/data/int/lemmas.lean @@ -43,7 +43,7 @@ match a, b, eq_coe_of_zero_le Ha, eq_coe_of_zero_le Hb with end protected theorem div_nonpos {a b : ℤ} (Ha : a ≥ 0) (Hb : b ≤ 0) : a / b ≤ 0 := -nonpos_of_neg_nonneg $ by rw -int.div_neg; exact int.div_nonneg Ha (neg_nonneg_of_nonpos Hb) +nonpos_of_neg_nonneg $ by rw [← int.div_neg]; exact int.div_nonneg Ha (neg_nonneg_of_nonpos Hb) theorem div_neg' {a b : ℤ} (Ha : a < 0) (Hb : b > 0) : a / b < 0 := match a, b, eq_neg_succ_of_lt_zero Ha, eq_succ_of_zero_lt Hb with @@ -74,7 +74,7 @@ end theorem div_eq_zero_of_lt_abs {a b : ℤ} (H1 : 0 ≤ a) (H2 : a < abs b) : a / b = 0 := match b, abs b, abs_eq_nat_abs b, H2 with | (n : ℕ), ._, rfl, H2 := div_eq_zero_of_lt H1 H2 -| -[1+ n], ._, rfl, H2 := neg_inj $ by rw -int.div_neg; exact div_eq_zero_of_lt H1 H2 +| -[1+ n], ._, rfl, H2 := neg_inj $ by rw [← int.div_neg]; exact div_eq_zero_of_lt H1 H2 end protected theorem add_mul_div_right (a b : ℤ) {c : ℤ} (H : c ≠ 0) : @@ -85,16 +85,16 @@ have ∀ {k n : ℕ} {a : ℤ}, (a + n * k.succ) / k.succ = a / k.succ + n, from | -[1+ m] := show ((n * k.succ:ℕ) - m.succ : ℤ) / k.succ = n - (m / k.succ + 1 : ℕ), begin cases lt_or_ge m (n*k.succ) with h h, - { rw [-int.coe_nat_sub h, - -int.coe_nat_sub ((nat.div_lt_iff_lt_mul _ _ k.succ_pos).2 h)], + { rw [← int.coe_nat_sub h, + ← int.coe_nat_sub ((nat.div_lt_iff_lt_mul _ _ k.succ_pos).2 h)], apply congr_arg of_nat, rw [mul_comm, nat.mul_sub_div], rwa mul_comm }, { change (↑(n * nat.succ k) - (m + 1) : ℤ) / ↑(nat.succ k) = ↑n - ((m / nat.succ k : ℕ) + 1), - rw [-sub_sub, -sub_sub, -neg_sub (m:ℤ), -neg_sub _ (n:ℤ), - -int.coe_nat_sub h, - -int.coe_nat_sub ((nat.le_div_iff_mul_le _ _ k.succ_pos).2 h), - -neg_succ_of_nat_coe', -neg_succ_of_nat_coe'], + rw [← sub_sub, ← sub_sub, ← neg_sub (m:ℤ), ← neg_sub _ (n:ℤ), + ← int.coe_nat_sub h, + ← int.coe_nat_sub ((nat.le_div_iff_mul_le _ _ k.succ_pos).2 h), + ← neg_succ_of_nat_coe', ← neg_succ_of_nat_coe'], { apply congr_arg neg_succ_of_nat, rw [mul_comm, nat.sub_mul_div], rwa mul_comm } } end @@ -104,10 +104,10 @@ have ∀ {a b c : ℤ}, c > 0 → (a + b * c) / c = a / c + b, from | ._, ⟨k, rfl⟩, (n : ℕ) := this | ._, ⟨k, rfl⟩, -[1+ n] := show (a - n.succ * k.succ) / k.succ = (a / k.succ) - n.succ, from - eq_sub_of_add_eq $ by rw [-this, sub_add_cancel] + eq_sub_of_add_eq $ by rw [← this, sub_add_cancel] end, match lt_trichotomy c 0 with -| or.inl hlt := neg_inj $ by rw [-int.div_neg, neg_add, -int.div_neg, -neg_mul_neg]; +| or.inl hlt := neg_inj $ by rw [← int.div_neg, neg_add, ← int.div_neg, ← neg_mul_neg]; apply this (neg_pos_of_neg hlt) | or.inr (or.inl heq) := absurd heq H | or.inr (or.inr hgt) := this hgt @@ -172,11 +172,11 @@ match a, b, eq_succ_of_zero_lt H with end theorem mod_lt (a : ℤ) {b : ℤ} (H : b ≠ 0) : a % b < abs b := -by rw -mod_abs; exact mod_lt_of_pos _ (abs_pos_of_ne_zero H) +by rw [← mod_abs]; exact mod_lt_of_pos _ (abs_pos_of_ne_zero H) lemma mod_add_div_aux (m n : ℕ) : (n - (m % n + 1) - (n * (m / n) + n) : ℤ) = -[1+ m] := begin - rw [-sub_sub, neg_succ_of_nat_coe, sub_sub (n:ℤ)], + rw [← sub_sub, neg_succ_of_nat_coe, sub_sub (n:ℤ)], apply eq_neg_of_eq_neg, rw [neg_sub, sub_sub_self, add_right_comm], exact @congr_arg ℕ ℤ _ _ (λi, (i + 1 : ℤ)) (nat.mod_add_div _ _).symm @@ -218,7 +218,7 @@ by rw [add_comm, mod_add_mod, add_comm] theorem add_mod_eq_add_mod_right {m n k : ℤ} (i : ℤ) (H : m % n = k % n) : (m + i) % n = (k + i) % n := -by rw [-mod_add_mod, -mod_add_mod k, H] +by rw [← mod_add_mod, ← mod_add_mod k, H] theorem add_mod_eq_add_mod_left {m n k : ℤ} (i : ℤ) (H : m % n = k % n) : (i + m) % n = (i + k) % n := @@ -235,7 +235,7 @@ theorem mod_eq_mod_of_add_mod_eq_add_mod_left {m n k i : ℤ} : by rw [add_comm, add_comm i]; apply mod_eq_mod_of_add_mod_eq_add_mod_right @[simp] theorem mul_mod_left (a b : ℤ) : (a * b) % b = 0 := -by rw [-zero_add (a * b), add_mul_mod_self, zero_mod] +by rw [← zero_add (a * b), add_mul_mod_self, zero_mod] @[simp] theorem mul_mod_right (a b : ℤ) : (a * b) % a = 0 := by rw [mul_comm, mul_mod_left] @@ -250,7 +250,7 @@ suffices ∀ (m k : ℕ) (b : ℤ), (m.succ * b / (m.succ * k) : ℤ) = b / k, f match a, eq_succ_of_zero_lt H, c, eq_coe_or_neg c with | ._, ⟨m, rfl⟩, ._, ⟨k, or.inl rfl⟩ := this _ _ _ | ._, ⟨m, rfl⟩, ._, ⟨k, or.inr rfl⟩ := - by rw [-neg_mul_eq_mul_neg, int.div_neg, int.div_neg]; + by rw [← neg_mul_eq_mul_neg, int.div_neg, int.div_neg]; apply congr_arg has_neg.neg; apply this end, λ m k b, match b, k with @@ -260,7 +260,7 @@ end, show (m.succ * n + m) / (m.succ * k.succ) = n / k.succ, begin apply nat.div_eq_of_lt_le, { refine le_trans _ (nat.le_add_right _ _), - rw -nat.mul_div_mul _ _ m.succ_pos, + rw [← nat.mul_div_mul _ _ m.succ_pos], apply nat.div_mul_le_self }, { change m.succ * n.succ ≤ _, rw [mul_left_comm], @@ -279,7 +279,7 @@ by rw [mod_def, mod_def, mul_div_mul_of_pos _ _ H, mul_sub_left_distrib, mul_ass theorem lt_div_add_one_mul_self (a : ℤ) {b : ℤ} (H : b > 0) : a < (a / b + 1) * b := by rw [add_mul, one_mul, mul_comm]; apply lt_add_of_sub_left_lt; - rw [-mod_def]; apply mod_lt_of_pos _ H + rw [← mod_def]; apply mod_lt_of_pos _ H theorem abs_div_le_abs : ∀ (a b : ℤ), abs (a / b) ≤ abs a := suffices ∀ (a : ℤ) (n : ℕ), abs (a / n) ≤ abs a, from @@ -299,7 +299,7 @@ by have := le_trans (le_abs_self _) (abs_div_le_abs a b); rwa [abs_of_nonneg Ha] at this theorem mul_div_cancel_of_mod_eq_zero {a b : ℤ} (H : a % b = 0) : b * (a / b) = a := -by have := mod_add_div a b; rwa [H, zero_add] at this +by have := mod_add_div a b; rwa [H, zero_add] at this theorem div_mul_cancel_of_mod_eq_zero {a b : ℤ} (H : a % b = 0) : a / b * b = a := by rw [mul_comm, mul_div_cancel_of_mod_eq_zero H] @@ -315,16 +315,16 @@ dvd.elim h $ λa ae, (λm0, by rw[m0, int.coe_nat_zero, zero_mul] at ae; rw [int.coe_nat_inj ae]; apply dvd_zero) (λm0l, let ⟨k, ke⟩ := int.eq_coe_of_zero_le $ nonneg_of_mul_nonneg_left - (by rw -ae; apply int.coe_zero_le : 0 ≤ (m:ℤ) * a) + (by rw [← ae]; apply int.coe_zero_le : 0 ≤ (m:ℤ) * a) (int.coe_nat_le_coe_nat_of_le m0l) in - by rw [ke, -int.coe_nat_mul] at ae; exact dvd.intro _ (int.coe_nat_inj ae).symm) + by rw [ke, ← int.coe_nat_mul] at ae; exact dvd.intro _ (int.coe_nat_inj ae).symm) lemma coe_nat_dvd_coe_nat_iff (m n : ℕ) : (↑m : ℤ) ∣ ↑n ↔ m ∣ n := ⟨dvd_of_coe_nat_dvd_coe_nat, coe_nat_dvd_coe_nat_of_dvd⟩ theorem dvd_antisymm {a b : ℤ} (H1 : a ≥ 0) (H2 : b ≥ 0) : a ∣ b → b ∣ a → a = b := begin - rw [-abs_of_nonneg H1, -abs_of_nonneg H2, abs_eq_nat_abs, abs_eq_nat_abs], + rw [← abs_of_nonneg H1, ← abs_of_nonneg H2, abs_eq_nat_abs, abs_eq_nat_abs], rw [coe_nat_dvd_coe_nat_iff, coe_nat_dvd_coe_nat_iff, int.coe_nat_eq_coe_nat_iff], apply nat.dvd_antisymm end @@ -358,7 +358,7 @@ theorem div_dvd_div : ∀ {a b c : ℤ} (H1 : a ∣ b) (H2 : b ∣ c), b / a ∣ protected theorem div_eq_iff_eq_mul_right {a b : ℤ} (c : ℤ) (H : b ≠ 0) (H' : b ∣ a) : a / b = c ↔ a = b * c := -⟨λ H1, by rw [-H1, int.mul_div_cancel' H'], +⟨λ H1, by rw [← H1, int.mul_div_cancel' H'], λ H1, by rw [H1, int.mul_div_cancel_left _ H]⟩ protected theorem div_eq_iff_eq_mul_left {a b : ℤ} (c : ℤ) (H : b ≠ 0) (H' : b ∣ a) : @@ -367,7 +367,7 @@ by rw mul_comm; exact int.div_eq_iff_eq_mul_right _ H H' protected theorem eq_mul_of_div_eq_right {a b c : ℤ} (H1 : b ∣ a) (H2 : a / b = c) : a = b * c := -by rw [-H2, int.mul_div_cancel' H1] +by rw [← H2, int.mul_div_cancel' H1] protected theorem div_eq_of_eq_mul_right {a b c : ℤ} (H1 : b ≠ 0) (H2 : a = b * c) : a / b = c := @@ -413,7 +413,7 @@ eq_one_of_mul_eq_one_right H (by rw [mul_comm, H']) /- / and ordering -/ protected theorem div_mul_le (a : ℤ) {b : ℤ} (H : b ≠ 0) : a / b * b ≤ a := -le_of_sub_nonneg $ by rw [mul_comm, -mod_def]; apply mod_nonneg _ H +le_of_sub_nonneg $ by rw [mul_comm, ← mod_def]; apply mod_nonneg _ H protected theorem div_le_of_le_mul {a b c : ℤ} (H : c > 0) (H' : a ≤ b * c) : a / c ≤ b := le_of_mul_le_mul_right (le_trans (int.div_mul_le _ (ne_of_gt H)) H') H @@ -445,7 +445,7 @@ protected theorem div_lt_iff_lt_mul {a b c : ℤ} (H : c > 0) : a / c < b ↔ a protected theorem le_mul_of_div_le {a b c : ℤ} (H1 : b ≥ 0) (H2 : b ∣ a) (H3 : a / b ≤ c) : a ≤ c * b := -by rw -int.div_mul_cancel H2; exact mul_le_mul_of_nonneg_right H3 H1 +by rw [← int.div_mul_cancel H2]; exact mul_le_mul_of_nonneg_right H3 H1 protected theorem lt_div_of_mul_lt {a b c : ℤ} (H1 : b ≥ 0) (H2 : b ∣ c) (H3 : a * b < c) : a < c / b := @@ -462,7 +462,7 @@ theorem div_eq_div_of_mul_eq_mul {a b c d : ℤ} (H1 : b ∣ a) (H2 : d ∣ c) ( (H4 : d ≠ 0) (H5 : a * d = b * c) : a / b = c / d := int.div_eq_of_eq_mul_right H3 $ -by rw -int.mul_div_assoc _ H2; exact +by rw [← int.mul_div_assoc _ H2]; exact (int.div_eq_of_eq_mul_left H4 H5.symm).symm end int diff --git a/library/init/data/int/order.lean b/library/init/data/int/order.lean index eb32c921f2..3419409b77 100644 --- a/library/init/data/int/order.lean +++ b/library/init/data/int/order.lean @@ -39,13 +39,13 @@ lemma le.intro_sub {a b : ℤ} {n : ℕ} (h : b - a = n) : a ≤ b := show nonneg (b - a), by rw h; trivial lemma le.intro {a b : ℤ} {n : ℕ} (h : a + n = b) : a ≤ b := -le.intro_sub (by rw -h; simp) +le.intro_sub (by rw [← h]; simp) lemma le.dest_sub {a b : ℤ} (h : a ≤ b) : ∃ n : ℕ, b - a = n := nonneg.elim h lemma le.dest {a b : ℤ} (h : a ≤ b) : ∃ n : ℕ, a + n = b := match (le.dest_sub h) with -| ⟨n, h₁⟩ := exists.intro n begin rw [-h₁, add_comm], simp end +| ⟨n, h₁⟩ := exists.intro n begin rw [← h₁, add_comm], simp end end lemma le.elim {a b : ℤ} (h : a ≤ b) {P : Prop} (h' : ∀ n : ℕ, a + ↑n = b → P) : P := @@ -60,7 +60,7 @@ or.imp_right lemma coe_nat_le_coe_nat_of_le {m n : ℕ} (h : m ≤ n) : (↑m : ℤ) ≤ ↑n := match nat.le.dest h with -| ⟨k, (hk : m + k = n)⟩ := le.intro (begin rw [-hk], reflexivity end) +| ⟨k, (hk : m + k = n)⟩ := le.intro (begin rw [← hk], reflexivity end) end lemma le_of_coe_nat_le_coe_nat {m n : ℕ} (h : (↑m : ℤ) ≤ ↑n) : m ≤ n := @@ -89,13 +89,13 @@ h ▸ lt_add_succ a n lemma lt.dest {a b : ℤ} (h : a < b) : ∃ n : ℕ, a + ↑(nat.succ n) = b := le.elim h (assume n, assume hn : a + 1 + n = b, - exists.intro n begin rw [-hn, add_assoc, add_comm (1 : int)], reflexivity end) + exists.intro n begin rw [← hn, add_assoc, add_comm (1 : int)], reflexivity end) lemma lt.elim {a b : ℤ} (h : a < b) {P : Prop} (h' : ∀ n : ℕ, a + ↑(nat.succ n) = b → P) : P := exists.elim (lt.dest h) h' lemma coe_nat_lt_coe_nat_iff (n m : ℕ) : (↑n : ℤ) < ↑m ↔ n < m := -begin rw [lt_iff_add_one_le, -int.coe_nat_succ, coe_nat_le_coe_nat_iff], reflexivity end +begin rw [lt_iff_add_one_le, ← int.coe_nat_succ, coe_nat_le_coe_nat_iff], reflexivity end lemma lt_of_coe_nat_lt_coe_nat {m n : ℕ} (h : (↑m : ℤ) < ↑n) : m < n := (coe_nat_lt_coe_nat_iff _ _).mp h @@ -111,16 +111,16 @@ le.intro (add_zero a) protected lemma le_trans {a b c : ℤ} (h₁ : a ≤ b) (h₂ : b ≤ c) : a ≤ c := le.elim h₁ (assume n, assume hn : a + n = b, le.elim h₂ (assume m, assume hm : b + m = c, -begin apply le.intro, rw [-hm, -hn, add_assoc], reflexivity end)) +begin apply le.intro, rw [← hm, ← hn, add_assoc], reflexivity end)) protected lemma le_antisymm {a b : ℤ} (h₁ : a ≤ b) (h₂ : b ≤ a) : a = b := le.elim h₁ (assume n, assume hn : a + n = b, le.elim h₂ (assume m, assume hm : b + m = a, - have a + ↑(n + m) = a + 0, by rw [int.coe_nat_add, -add_assoc, hn, hm, add_zero a], + have a + ↑(n + m) = a + 0, by rw [int.coe_nat_add, ← add_assoc, hn, hm, add_zero a], have (↑(n + m) : ℤ) = 0, from add_left_cancel this, have n + m = 0, from int.coe_nat_inj this, have n = 0, from nat.eq_zero_of_add_eq_zero_right this, - show a = b, begin rw [-hn, this, int.coe_nat_zero, add_zero a] end)) + show a = b, begin rw [← hn, this, int.coe_nat_zero, add_zero a] end)) protected lemma lt_irrefl (a : ℤ) : ¬ a < a := assume : a < a, @@ -141,7 +141,7 @@ iff.intro (assume ⟨aleb, aneb⟩, le.elim aleb (assume n, assume hn : a + n = b, have n ≠ 0, - from (assume : n = 0, aneb begin rw [-hn, this, int.coe_nat_zero, add_zero] end), + from (assume : n = 0, aneb begin rw [← hn, this, int.coe_nat_zero, add_zero] end), have n = nat.succ (nat.pred n), from eq.symm (nat.succ_pred_eq_of_pos (nat.pos_of_ne_zero this)), lt.intro (begin rewrite this at hn, exact hn end))) @@ -154,7 +154,7 @@ iff.intro (assume : a ≠ b, le.elim h (assume n, assume hn : a + n = b, have n ≠ 0, from - (assume : n = 0, ‹a ≠ b› begin rw [-hn, this, int.coe_nat_zero, add_zero] end), + (assume : n = 0, ‹a ≠ b› begin rw [← hn, this, int.coe_nat_zero, add_zero] end), have n = nat.succ (nat.pred n), from eq.symm (nat.succ_pred_eq_of_pos (nat.pos_of_ne_zero this)), or.inl (lt.intro (begin rewrite this at hn, exact hn end))))) @@ -179,14 +179,14 @@ iff.mpr (int.lt_iff_le_and_ne _ _) protected lemma mul_nonneg {a b : ℤ} (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a * b := le.elim ha (assume n, assume hn, le.elim hb (assume m, assume hm, - le.intro (show 0 + ↑n * ↑m = a * b, begin rw [-hn, -hm], repeat {rw zero_add} end))) + le.intro (show 0 + ↑n * ↑m = a * b, begin rw [← hn, ← hm], repeat {rw zero_add} end))) protected lemma mul_pos {a b : ℤ} (ha : 0 < a) (hb : 0 < b) : 0 < a * b := lt.elim ha (assume n, assume hn, lt.elim hb (assume m, assume hm, lt.intro (show 0 + ↑(nat.succ (nat.succ n * m + n)) = a * b, - begin rw [-hn, -hm], repeat {rw int.coe_nat_zero}, simp, - rw [-int.coe_nat_mul], simp [nat.mul_succ, nat.succ_add] end))) + begin rw [← hn, ← hm], repeat {rw int.coe_nat_zero}, simp, + rw [← int.coe_nat_mul], simp [nat.mul_succ, nat.succ_add] end))) protected lemma zero_lt_one : (0 : ℤ) < 1 := trivial @@ -199,7 +199,7 @@ protected lemma lt_of_lt_of_le {a b c : ℤ} (hab : a < b) (hbc : b ≤ c) : a < have hac : a ≤ c, from int.le_trans (le_of_lt hab) hbc, iff.mpr (int.lt_iff_le_and_ne _ _) - (and.intro hac (assume heq, int.not_le_of_gt begin rw -heq, assumption end hbc)) + (and.intro hac (assume heq, int.not_le_of_gt (by rwa [← heq]) hbc)) protected lemma lt_of_le_of_lt {a b c : ℤ} (hab : a ≤ b) (hbc : b < c) : a < c := have hac : a ≤ c, from int.le_trans hab (le_of_lt hbc), @@ -263,7 +263,7 @@ theorem nat_abs_of_nonneg {a : ℤ} (H : a ≥ 0) : (nat_abs a : ℤ) = a := match a, eq_coe_of_zero_le H with ._, ⟨n, rfl⟩ := rfl end theorem of_nat_nat_abs_of_nonpos {a : ℤ} (H : a ≤ 0) : (nat_abs a : ℤ) = -a := -by rw [-nat_abs_neg, nat_abs_of_nonneg (neg_nonneg_of_nonpos H)] +by rw [← nat_abs_neg, nat_abs_of_nonneg (neg_nonneg_of_nonpos H)] theorem abs_eq_nat_abs : ∀ a : ℤ, abs a = nat_abs a | (n : ℕ) := abs_of_nonneg $ coe_zero_le _ @@ -355,6 +355,6 @@ let ⟨b, Hb⟩ := Hbdd in ⟨-b, λ z h, Hb _ (lt_neg_of_lt_neg h)⟩, have Hinh' : ∃ z : ℤ, P (-z), from let ⟨elt, Helt⟩ := Hinh in ⟨-elt, by rw [neg_neg]; exact Helt⟩, let ⟨lb, Plb, al⟩ := exists_least_of_bdd Hbdd' Hinh' in -⟨-lb, Plb, λ z h, by rw [-neg_neg z]; exact al _ (neg_lt_of_neg_lt h)⟩ +⟨-lb, Plb, λ z h, by rw [← neg_neg z]; exact al _ (neg_lt_of_neg_lt h)⟩ -end int \ No newline at end of file +end int diff --git a/library/init/data/list/instances.lean b/library/init/data/list/instances.lean index fe47146b5f..5b269354de 100644 --- a/library/init/data/list/instances.lean +++ b/library/init/data/list/instances.lean @@ -100,8 +100,8 @@ instance decidable_prefix [decidable_eq α] : ∀ (l₁ l₂ : list α), decidab | (a::l₁) [] := is_false $ λ⟨t, te⟩, list.no_confusion te | (a::l₁) (b::l₂) := if h : a = b then - decidable_of_decidable_of_iff (decidable_prefix l₁ l₂) $ by rw -h; exact - ⟨λ⟨t, te⟩, ⟨t, by rw -te; refl⟩, + decidable_of_decidable_of_iff (decidable_prefix l₁ l₂) $ by rw [← h]; exact + ⟨λ⟨t, te⟩, ⟨t, by rw [← te]; refl⟩, λ⟨t, te⟩, list.no_confusion te (λ_ te, ⟨t, te⟩)⟩ else is_false $ λ⟨t, te⟩, list.no_confusion te $ λh', absurd h' h @@ -114,7 +114,7 @@ instance decidable_suffix [decidable_eq α] : ∀ (l₁ l₂ : list α), decidab | l₁ l₂ := let len1 := length l₁, len2 := length l₂ in if hl : len1 ≤ len2 then if he : drop (len2 - len1) l₂ = l₁ then is_true $ - ⟨take (len2 - len1) l₂, by rw [-he, take_append_drop]⟩ + ⟨take (len2 - len1) l₂, by rw [← he, take_append_drop]⟩ else is_false $ suffices length l₁ ≤ length l₂ → l₁ <:+ l₂ → drop (length l₂ - length l₁) l₂ = l₁, from λsuf, he (this hl suf), @@ -122,7 +122,7 @@ instance decidable_suffix [decidable_eq α] : ∀ (l₁ l₂ : list α), decidab append_right_inj (eq.trans (take_append_drop (length l₂ - length l₁) l₂) te.symm) $ by simp; exact nat.sub_sub_self hl else is_false $ λ⟨t, te⟩, hl $ - show length l₁ ≤ length l₂, by rw [-te, length_append]; apply nat.le_add_left + show length l₁ ≤ length l₂, by rw [← te, length_append]; apply nat.le_add_left instance decidable_infix [decidable_eq α] : ∀ (l₁ l₂ : list α), decidable (l₁ <:+: l₂) | [] l₂ := is_true ⟨[], l₂, rfl⟩ @@ -138,7 +138,7 @@ instance decidable_sublist [decidable_eq α] : ∀ (l₁ l₂ : list α), decida | (a::l₁) (b::l₂) := if h : a = b then decidable_of_decidable_of_iff (decidable_sublist l₁ l₂) $ - by rw -h; exact ⟨cons_sublist_cons _, sublist_of_cons_sublist_cons⟩ + by rw [← h]; exact ⟨cons_sublist_cons _, sublist_of_cons_sublist_cons⟩ else decidable_of_decidable_of_iff (decidable_sublist (a::l₁) l₂) ⟨sublist_cons_of_sublist _, λs, match a, l₁, s, h with | a, l₁, sublist.cons ._ ._ ._ s', h := s' diff --git a/library/init/data/list/lemmas.lean b/library/init/data/list/lemmas.lean index c8ce3f5eb4..f179ebd805 100644 --- a/library/init/data/list/lemmas.lean +++ b/library/init/data/list/lemmas.lean @@ -130,7 +130,7 @@ lemma append_inj_right {s₁ s₂ t₁ t₂ : list α} (h : s₁ ++ t₁ = s₂ lemma append_right_inj {s₁ s₂ t₁ t₂ : list α} (h : s₁ ++ t₁ = s₂ ++ t₂) (hl : length t₁ = length t₂) : s₁ = s₂ ∧ t₁ = t₂ := append_inj h $ @nat.add_right_cancel _ (length t₁) _ $ -let hap := congr_arg length h in by simp at hap; rwa -hl at hap +let hap := congr_arg length h in by simp at hap; rwa [← hl] at hap /- nth -/ @@ -152,8 +152,8 @@ theorem ext : Π {l₁ l₂ : list α}, (∀n, nth l₁ n = nth l₂ n) → l₁ 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₁ - then by rw [nth_le_nth, nth_le_nth, h n h₁ (by rwa -hl)] - else let h₁ := le_of_not_gt h₁ in by rw [nth_ge_len _ _ h₁, nth_ge_len _ _ (by rwa -hl)] + then by rw [nth_le_nth, nth_le_nth, h n h₁ (by rwa [← hl])] + else let h₁ := le_of_not_gt h₁ in by rw [nth_ge_len _ _ h₁, nth_ge_len _ _ (by rwa [← hl])] /- map -/ @@ -252,7 +252,7 @@ lemma nth_le_reverse_aux2 : Π (l r : list α) (i : nat) (h1) (h2), have heq := calc length (a :: l) - 1 - (i + 1) = length l - (1 + i) : by rw add_comm; refl ... = length l - 1 - i : by rw nat.sub_sub, - rw -heq at aux, + rw [← heq] at aux, apply aux end @@ -446,7 +446,7 @@ begin end lemma mem_map_iff {f : α → β} {b : β} {l : list α} : b ∈ map f l ↔ ∃ a, a ∈ l ∧ f a = b := -⟨exists_of_mem_map, λ ⟨a, la, h⟩, by rw -h; exact mem_map f la⟩ +⟨exists_of_mem_map, λ ⟨a, la, h⟩, by rw [← h]; exact mem_map f la⟩ lemma mem_join_iff {a : α} : ∀ {L : list (list α)}, a ∈ join L ↔ ∃ l, l ∈ L ∧ a ∈ l | [] := ⟨false.elim, λ⟨_, h, _⟩, false.elim h⟩ @@ -600,7 +600,7 @@ lemma eq_nil_of_sublist_nil {l : list α} (s : l <+ []) : l = [] := eq_nil_of_subset_nil $ subset_of_sublist s lemma eq_nil_of_map_eq_nil {f : α → β} {l :list α} (h : map f l = nil) : l = nil := -eq_nil_of_length_eq_zero (begin rw -(length_map f l), simp [h] end) +eq_nil_of_length_eq_zero (begin rw [← length_map f l], simp [h] end) lemma eq_of_map_const {b₁ b₂ : β} {l : list α} (h : b₁ ∈ map (function.const α b₂) l) : b₁ = b₂ := let ⟨a, _, e⟩ := exists_of_mem_map h in e.symm @@ -667,7 +667,7 @@ lemma infix_of_suffix {l₁ l₂ : list α} : l₁ <:+ l₂ → l₁ <:+: l₂ : lemma infix_refl (l : list α) : l <:+: l := infix_of_prefix $ prefix_refl l lemma sublist_of_infix {l₁ l₂ : list α} : l₁ <:+: l₂ → l₁ <+ l₂ := -λ⟨s, t, h⟩, by rw -h; exact (sublist_append_right _ _).trans (sublist_append_left _ _) +λ⟨s, t, h⟩, by rw [← h]; exact (sublist_append_right _ _).trans (sublist_append_left _ _) lemma length_le_of_infix {l₁ l₂ : list α} (s : l₁ <:+: l₂) : length l₁ ≤ length l₂ := length_le_of_sublist $ sublist_of_infix s @@ -682,7 +682,7 @@ lemma eq_nil_of_suffix_nil {l : list α} (s : l <:+ []) : l = [] := eq_nil_of_infix_nil $ infix_of_suffix s lemma infix_iff_prefix_suffix (l₁ l₂ : list α) : l₁ <:+: l₂ ↔ ∃ t, l₁ <+: t ∧ t <:+ l₂ := -⟨λ⟨s, t, e⟩, ⟨l₁ ++ t, ⟨_, rfl⟩, by rw [-e, append_assoc]; exact ⟨_, rfl⟩⟩, +⟨λ⟨s, t, e⟩, ⟨l₁ ++ t, ⟨_, rfl⟩, by rw [← e, append_assoc]; exact ⟨_, rfl⟩⟩, λ⟨._, ⟨t, rfl⟩, ⟨s, e⟩⟩, ⟨s, t, by rw append_assoc; exact e⟩⟩ @[simp] lemma mem_inits : ∀ (s t : list α), s ∈ inits t ↔ s <+: t @@ -690,7 +690,7 @@ lemma infix_iff_prefix_suffix (l₁ l₂ : list α) : l₁ <:+: l₂ ↔ ∃ t, | s (a::t) := by simp; exact ⟨λo, match s, o with | ._, or.inl rfl := ⟨_, rfl⟩ | s, or.inr mm := let ⟨r, hr, hs⟩ := exists_of_mem_map mm, ⟨s, ht⟩ := (mem_inits _ _).1 hr in - by rw [-hs, -ht]; exact ⟨s, rfl⟩ + by rw [← hs, ← ht]; exact ⟨s, rfl⟩ end, λmi, match s, mi with | [], ⟨._, rfl⟩ := or.inl rfl | (b::s), ⟨r, hr⟩ := list.no_confusion hr $ λba st, or.inr $ @@ -718,7 +718,7 @@ by simp [sublists_aux]; rw [sublists_aux_eq_foldl l, sublists_aux_eq_foldl l (λ lemma sublists_aux_cons_cons (l : list α) (a : α) : sublists_aux (a::l) cons = [a] :: foldr (λys r, ys :: (a :: ys) :: r) [] (sublists_aux l cons) := -by rw -sublists_aux_eq_foldl; refl +by rw [← sublists_aux_eq_foldl]; refl @[simp] lemma mem_sublists (s t : list α) : s ∈ sublists t ↔ s <+ t := by simp [sublists]; exact diff --git a/library/init/data/nat/bitwise.lean b/library/init/data/nat/bitwise.lean index d81dcde176..a7dbe49cc3 100644 --- a/library/init/data/nat/bitwise.lean +++ b/library/init/data/nat/bitwise.lean @@ -50,7 +50,7 @@ namespace nat simp [bnot] at this, rw [show ∀ b, ff && b = ff, by intros; cases b; refl, show ∀ b, bxor b ff = b, by intros; cases b; refl] at this, - rw -this, + rw [← this], cases mod_two_eq_zero_or_one n; rw a; refl end @@ -89,7 +89,7 @@ namespace nat (bit_val _ _).trans $ (add_comm _ _).trans $ bodd_add_div2 _ def bit_cases_on {C : nat → Sort u} (n) (h : ∀ b n, C (bit b n)) : C n := - by rw -bit_decomp n; apply h + by rw [← bit_decomp n]; apply h @[simp] lemma bit_zero : bit ff 0 = 0 := rfl @@ -164,7 +164,7 @@ namespace nat lemma test_bit_succ (m b n) : test_bit (bit b n) (succ m) = test_bit n m := have bodd (shiftr (shiftr (bit b n) 1) m) = bodd (shiftr n m), by dsimp [shiftr]; rw div2_bit, - by rw [-shiftr_add, add_comm] at this; exact this + by rw [← shiftr_add, add_comm] at this; exact this def binary_rec {C : nat → Sort u} (z : C 0) (f : ∀ b n, C n → C (bit b n)) : Π n, C n | n := if n0 : n = 0 then by rw n0; exact z else let n' := div2 n in @@ -175,7 +175,7 @@ namespace nat (lt_of_le_of_ne (zero_le _) (ne.symm n0)), rwa mul_one at this end, - by rw [-show bit (bodd n) n' = n, from bit_decomp n]; exact + by rw [← show bit (bodd n) n' = n, from bit_decomp n]; exact f (bodd n) n' (binary_rec n') def size : ℕ → ℕ := binary_rec 0 (λ_ _, succ) @@ -210,7 +210,7 @@ namespace nat have n0 := div2_bit b n, rw h' at bf n0, simp at bf n0, - rw [-bf, -n0, binary_rec_zero], + rw [← bf, ← n0, binary_rec_zero], intros, exact h.symm }, {simp [dif_neg h'], generalize (binary_rec._main._pack._proof_2 (bit b n)) e, @@ -257,7 +257,7 @@ namespace nat all_goals { apply bit_cases_on m, intros a m, rw [binary_rec_eq, binary_rec_zero], - rw [-bitwise_bit_aux h, ftf], refl } }, + rw [← bitwise_bit_aux h, ftf], refl } }, { exact bitwise_bit_aux h } end diff --git a/library/init/data/nat/lemmas.lean b/library/init/data/nat/lemmas.lean index 84e61e8fa8..5c78ec0da9 100644 --- a/library/init/data/nat/lemmas.lean +++ b/library/init/data/nat/lemmas.lean @@ -382,7 +382,7 @@ iff.intro nat.lt_or_eq_of_le nat.le_of_lt_or_eq lemma mul_le_mul_left {n m : ℕ} (k : ℕ) (h : n ≤ m) : k * n ≤ k * m := match le.dest h with | ⟨l, hl⟩ := - have k * n + k * l = k * m, by rw [-left_distrib, hl], + have k * n + k * l = k * m, by rw [← left_distrib, hl], le.intro this end @@ -716,7 +716,7 @@ by rw [nat.add_sub_add_left, nat.zero_sub] theorem add_le_to_le_sub (x : ℕ) {y k : ℕ} (h : k ≤ y) : x + k ≤ y ↔ x ≤ y - k := -by rw [-nat.add_sub_cancel x k, nat.sub_le_sub_right_iff _ _ _ h, nat.add_sub_cancel] +by rw [← nat.add_sub_cancel x k, nat.sub_le_sub_right_iff _ _ _ h, nat.add_sub_cancel] lemma sub_lt_of_pos_le (a b : ℕ) (h₀ : 0 < a) (h₁ : a ≤ b) : b - a < b := @@ -757,11 +757,11 @@ by rw [nat.mul_sub_left_distrib, right_distrib, right_distrib, mul_comm b a, add nat.add_sub_add_left] theorem succ_mul_succ_eq (a b : nat) : succ a * succ b = a*b + a + b + 1 := -begin rw [-add_one_eq_succ, -add_one_eq_succ], simp [right_distrib, left_distrib] end +begin rw [← add_one_eq_succ, ← add_one_eq_succ], simp [right_distrib, left_distrib] end theorem sub_eq_zero_of_le {n m : ℕ} (h : n ≤ m) : n - m = 0 := exists.elim (nat.le.dest h) - (assume k, assume hk : n + k = m, by rw [-hk, sub_self_add]) + (assume k, assume hk : n + k = m, by rw [← hk, sub_self_add]) protected theorem le_of_sub_eq_zero : ∀{n m : ℕ}, n - m = 0 → n ≤ m | n 0 H := begin rw [nat.sub_zero] at H, simp [H] end @@ -775,12 +775,12 @@ protected theorem sub_eq_zero_iff_le {n m : ℕ} : n - m = 0 ↔ n ≤ m := theorem succ_sub {m n : ℕ} (h : m ≥ n) : succ m - n = succ (m - n) := exists.elim (nat.le.dest h) (assume k, assume hk : n + k = m, - by rw [-hk, nat.add_sub_cancel_left, -add_succ, nat.add_sub_cancel_left]) + by rw [← hk, nat.add_sub_cancel_left, ← add_succ, nat.add_sub_cancel_left]) theorem add_sub_of_le {n m : ℕ} (h : n ≤ m) : n + (m - n) = m := exists.elim (nat.le.dest h) (assume k, assume hk : n + k = m, - by rw [-hk, nat.add_sub_cancel_left]) + by rw [← hk, nat.add_sub_cancel_left]) protected theorem sub_add_cancel {n m : ℕ} (h : n ≥ m) : n - m + m = n := by rw [add_comm, add_sub_of_le h] @@ -792,7 +792,7 @@ lt_of_add_lt_add_right this protected theorem add_sub_assoc {m k : ℕ} (h : k ≤ m) (n : ℕ) : n + m - k = n + (m - k) := exists.elim (nat.le.dest h) (assume l, assume hl : k + l = m, - by rw [-hl, nat.add_sub_cancel_left, add_comm k, -add_assoc, nat.add_sub_cancel]) + by rw [← hl, nat.add_sub_cancel_left, add_comm k, ← add_assoc, nat.add_sub_cancel]) protected lemma sub_eq_iff_eq_add {a b c : ℕ} (ab : b ≤ a) : a - b = c ↔ a = c + b := ⟨assume c_eq, begin rw [c_eq.symm, nat.sub_add_cancel ab] end, @@ -923,7 +923,7 @@ begin have h₁ : succ x % y = (succ x - y) % y, {exact mod_eq_sub_mod (le_of_not_gt h₁)}, have this : succ x - y ≤ x, {exact le_of_lt_succ (sub_lt (succ_pos x) h)}, have h₂ : (succ x - y) % y < y, {exact ih _ this}, - rwa -h₁ at h₂}} + rwa [← h₁] at h₂}} end lemma mod_le (x y : ℕ) : x % y ≤ x := @@ -940,13 +940,13 @@ by rw [mod_eq_sub_mod (nat.le_add_left _ _), nat.add_sub_cancel] by rw [add_comm, add_mod_right] @[simp] theorem add_mul_mod_self_left (x y z : ℕ) : (x + y * z) % y = x % y := -by {induction z with z ih, simp, rw[mul_succ, -add_assoc, add_mod_right, ih]} +by {induction z with z ih, simp, rw[mul_succ, ← add_assoc, add_mod_right, ih]} @[simp] theorem add_mul_mod_self_right (x y z : ℕ) : (x + y * z) % z = x % z := by rw [mul_comm, add_mul_mod_self_left] @[simp] theorem mul_mod_right (m n : ℕ) : (m * n) % m = 0 := -by rw [-(zero_add (m*n)), add_mul_mod_self_left, zero_mod] +by rw [← zero_add (m*n), add_mul_mod_self_left, zero_mod] @[simp] theorem mul_mod_left (m n : ℕ) : (m * n) % n = 0 := by rw [mul_comm, mul_mod_right] @@ -970,7 +970,7 @@ else x.strong_induction_on $ λn IH, (λyn, by rw [ mod_eq_sub_mod yn, mod_eq_sub_mod (mul_le_mul_left z yn), - -nat.mul_sub_left_distrib]; + ← nat.mul_sub_left_distrib]; exact IH _ (sub_lt (lt_of_lt_of_le y0 yn) y0)) (λyn, by rw [mod_eq_of_lt yn, mod_eq_of_lt (mul_lt_mul_of_pos_left yn z0)]) @@ -1015,7 +1015,7 @@ begin { apply @nat.le_of_add_le_add_right (n*k), rw [nat.sub_add_cancel h₂], simp [mul_succ] at h₁, simp [h₁] }, - rw [mul_succ, -nat.sub_sub, -mod_eq_sub_mod h₄, ih_1 h₂] } + rw [mul_succ, ← nat.sub_sub, ← mod_eq_sub_mod h₄, ih_1 h₂] } end /- div & mod -/ @@ -1035,7 +1035,7 @@ begin apply lt_of_lt_of_le h.left h.right }, rw [div_def, mod_def, if_pos h, if_pos h], simp [left_distrib, IH _ h'], - rw [-nat.add_sub_assoc h.right, nat.add_sub_cancel_left] }, + rw [← nat.add_sub_assoc h.right, nat.add_sub_cancel_left] }, -- ¬ (0 < k ∧ k ≤ m) { rw [div_def, mod_def, if_neg h', if_neg h'], simp }, end @@ -1090,7 +1090,7 @@ begin rw [nat.sub_add_cancel h₂, add_comm], rw [mul_succ] at h₁, apply h₁ }, - rw [sub_succ, -ih_1 h₂], + rw [sub_succ, ← ih_1 h₂], rw [@div_eq_sub_div (x - n*p) _ h₀ h₃], simp [add_one_eq_succ, pred_succ, mul_succ, nat.sub_sub] } } end @@ -1135,7 +1135,7 @@ begin { simp [zero_mul, zero_le_iff_true] }, { have Hlt : y - k < y, { apply sub_lt_of_pos_le ; assumption }, - rw [ -add_one_eq_succ + rw [ ← add_one_eq_succ , nat.add_le_add_iff_le_right , IH (y - k) Hlt x , add_one_eq_succ @@ -1172,7 +1172,7 @@ protected theorem div_self {n : ℕ} (H : n > 0) : n / n = 1 := let t := add_div_right 0 H in by rwa [zero_add, nat.zero_div] at t theorem add_mul_div_left (x z : ℕ) {y : ℕ} (H : y > 0) : (x + y * z) / y = x / y + z := -by {induction z with z ih, simp, rw [mul_succ, -add_assoc, add_div_right _ H, ih]} +by {induction z with z ih, simp, rw [mul_succ, ← add_assoc, add_div_right _ H, ih]} theorem add_mul_div_right (x y : ℕ) {z : ℕ} (H : z > 0) : (x + y * z) / z = x / z + y := by rw [mul_comm, add_mul_div_left _ _ H] @@ -1222,7 +1222,7 @@ begin cases eq_zero_or_pos n with n0 npos, {rw [n0, zero_mul, nat.div_zero, nat.zero_div]}, apply le_antisymm, { apply (le_div_iff_mul_le _ _ (mul_pos npos kpos)).2, - rw [mul_comm n k, -mul_assoc], + rw [mul_comm n k, ← mul_assoc], apply (le_div_iff_mul_le _ _ npos).1, apply (le_div_iff_mul_le _ _ kpos).1, refl }, @@ -1234,14 +1234,14 @@ begin end protected theorem mul_div_mul {m : ℕ} (n k : ℕ) (H : m > 0) : m * n / (m * k) = n / k := -by rw [-nat.div_div_eq_div_mul, nat.mul_div_cancel_left _ H] +by rw [← nat.div_div_eq_div_mul, nat.mul_div_cancel_left _ H] /- dvd -/ protected theorem dvd_add_iff_right {k m n : ℕ} (h : k ∣ m) : k ∣ n ↔ k ∣ m + n := ⟨dvd_add h, dvd.elim h $ λd hd, match m, hd with | ._, rfl := λh₂, dvd.elim h₂ $ λe he, ⟨e - d, - by rw [nat.mul_sub_left_distrib, -he, nat.add_sub_cancel_left]⟩ + by rw [nat.mul_sub_left_distrib, ← he, nat.add_sub_cancel_left]⟩ end⟩ protected theorem dvd_add_iff_left {k m n : ℕ} (h : k ∣ n) : k ∣ m ↔ k ∣ m + n := @@ -1293,7 +1293,7 @@ protected theorem mul_div_assoc (m : ℕ) {n k : ℕ} (H : k ∣ n) : m * n / k or.elim (eq_zero_or_pos k) (λh, by rw [h, nat.div_zero, nat.div_zero, mul_zero]) (λh, have m * n / k = m * (n / k * k) / k, by rw nat.div_mul_cancel H, - by rw[this, -mul_assoc, nat.mul_div_cancel _ h]) + by rw[this, ← mul_assoc, nat.mul_div_cancel _ h]) theorem dvd_of_mul_dvd_mul_left {m n k : ℕ} (kpos : k > 0) (H : k * m ∣ k * n) : m ∣ n := dvd.elim H (λl H1, by rw mul_assoc at H1; exact ⟨_, eq_of_mul_eq_mul_left kpos H1⟩) @@ -1312,7 +1312,7 @@ theorem pow_le_pow_of_le_left {x y : ℕ} (H : x ≤ y) : ∀ i, x^i ≤ y^i theorem pow_le_pow_of_le_right {x : ℕ} (H : x > 0) {i} : ∀ {j}, i ≤ j → x^i ≤ x^j | 0 h := by rw eq_zero_of_le_zero h; apply le_refl | (succ j) h := (lt_or_eq_of_le h).elim - (λhl, by rw [pow_succ, -mul_one (x^i)]; exact + (λhl, by rw [pow_succ, ← mul_one (x^i)]; exact mul_le_mul (pow_le_pow_of_le_right $ le_of_lt_succ hl) H (zero_le _) (zero_le _)) (λe, by rw e; refl) @@ -1320,7 +1320,7 @@ lemma pos_pow_of_pos {b : ℕ} (n : ℕ) (h : 0 < b) : 0 < b^n := pow_le_pow_of_le_right h (zero_le _) lemma zero_pow {n : ℕ} (h : 0 < n) : 0^n = 0 := -by rw [-succ_pred_eq_of_pos h, pow_succ, mul_zero] +by rw [← succ_pred_eq_of_pos h, pow_succ, mul_zero] theorem pow_lt_pow_of_lt_left {x y : ℕ} (H : x < y) {i} (h : i > 0) : x^i < y^i := begin @@ -1334,7 +1334,7 @@ theorem pow_lt_pow_of_lt_right {x : ℕ} (H : x > 1) {i j} (h : i < j) : x^i < x begin have xpos := lt_of_succ_lt H, refine lt_of_lt_of_le _ (pow_le_pow_of_le_right xpos h), - rw [-mul_one (x^i), pow_succ], + rw [← mul_one (x^i), pow_succ], exact nat.mul_lt_mul_of_pos_left H (pos_pow_of_pos _ xpos) end diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean index 307c736b5f..6526cb089d 100644 --- a/library/init/meta/interactive.lean +++ b/library/init/meta/interactive.lean @@ -334,7 +334,7 @@ private meta def rw_hyps (cfg : rewrite_cfg) (rs : list rw_rule) (hs : list name hs.mfor' (rw_hyp cfg rs) meta def rw_rule_p (ep : parser pexpr) : parser rw_rule := -rw_rule.mk <$> cur_pos <*> (option.is_some <$> (tk "-")?) <*> ep +rw_rule.mk <$> cur_pos <*> (option.is_some <$> (tk "←" <|> tk "<-")?) <*> ep meta structure rw_rules_t := (rules : list rw_rule) diff --git a/tests/lean/interactive/goal_info_rw.lean b/tests/lean/interactive/goal_info_rw.lean index 0c0de6b09d..f6b0afc9ef 100644 --- a/tests/lean/interactive/goal_info_rw.lean +++ b/tests/lean/interactive/goal_info_rw.lean @@ -1,9 +1,9 @@ example (p q r : Prop) (h₁ : p = q) (h₂ : q = r) : p = r := by rw [h₁, --^ "command": "info" - -h₂, + ←h₂, --^ "command": "info" - -h₁ + ←h₁ --^ "command": "info" --^ "command": "info" ] diff --git a/tests/lean/interactive/goal_info_rw.lean.expected.out b/tests/lean/interactive/goal_info_rw.lean.expected.out index c300640b7b..f5cb69e520 100644 --- a/tests/lean/interactive/goal_info_rw.lean.expected.out +++ b/tests/lean/interactive/goal_info_rw.lean.expected.out @@ -1,6 +1,6 @@ {"message":"file invalidated","response":"ok","seq_num":0} -{"record":{"source":,"state":"p q r : Prop,\nh₁ : p = q,\nh₂ : q = r\n⊢ q = r","tactic_param_idx":0,"tactic_params":["([ (-? expr), ... ] | -? expr)","(at (* | id*))?","tactic.rewrite_cfg?"],"text":"rw","type":"interactive.parse tactic.interactive.rw_rules → interactive.parse interactive.types.location → opt_param tactic.rewrite_cfg {to_apply_cfg := {md := reducible, approx := tt, new_goals := tactic.new_goals.non_dep_first, instances := tt, auto_param := tt, opt_param := tt}, symm := ff, occs := occurrences.all} → tactic unit"},"response":"ok","seq_num":3} -{"record":{"source":,"state":"p q r : Prop,\nh₁ : p = q,\nh₂ : q = r\n⊢ q = r","tactic_param_idx":0,"tactic_params":["([ (-? expr), ... ] | -? expr)","(at (* | id*))?","tactic.rewrite_cfg?"],"text":"rw","type":"interactive.parse tactic.interactive.rw_rules → interactive.parse interactive.types.location → opt_param tactic.rewrite_cfg {to_apply_cfg := {md := reducible, approx := tt, new_goals := tactic.new_goals.non_dep_first, instances := tt, auto_param := tt, opt_param := tt}, symm := ff, occs := occurrences.all} → tactic unit"},"response":"ok","seq_num":5} +{"record":{"source":,"state":"p q r : Prop,\nh₁ : p = q,\nh₂ : q = r\n⊢ q = r","tactic_param_idx":0,"tactic_params":["([ ((← | <-)? expr), ... ] | (← | <-)? expr)","(at (* | id*))?","tactic.rewrite_cfg?"],"text":"rw","type":"interactive.parse tactic.interactive.rw_rules → interactive.parse interactive.types.location → opt_param tactic.rewrite_cfg {to_apply_cfg := {md := reducible, approx := tt, new_goals := tactic.new_goals.non_dep_first, instances := tt, auto_param := tt, opt_param := tt}, symm := ff, occs := occurrences.all} → tactic unit"},"response":"ok","seq_num":3} +{"record":{"source":,"state":"p q r : Prop,\nh₁ : p = q,\nh₂ : q = r\n⊢ q = r","tactic_param_idx":0,"tactic_params":["([ ((← | <-)? expr), ... ] | (← | <-)? expr)","(at (* | id*))?","tactic.rewrite_cfg?"],"text":"rw","type":"interactive.parse tactic.interactive.rw_rules → interactive.parse interactive.types.location → opt_param tactic.rewrite_cfg {to_apply_cfg := {md := reducible, approx := tt, new_goals := tactic.new_goals.non_dep_first, instances := tt, auto_param := tt, opt_param := tt}, symm := ff, occs := occurrences.all} → tactic unit"},"response":"ok","seq_num":5} {"record":{"full-id":"h₁","state":"p q r : Prop,\nh₁ : p = q,\nh₂ : q = r\n⊢ q = q","type":"p = q"},"response":"ok","seq_num":7} -{"record":{"source":,"state":"no goals","tactic_param_idx":0,"tactic_params":["([ (-? expr), ... ] | -? expr)","(at (* | id*))?","tactic.rewrite_cfg?"],"text":"rw","type":"interactive.parse tactic.interactive.rw_rules → interactive.parse interactive.types.location → opt_param tactic.rewrite_cfg {to_apply_cfg := {md := reducible, approx := tt, new_goals := tactic.new_goals.non_dep_first, instances := tt, auto_param := tt, opt_param := tt}, symm := ff, occs := occurrences.all} → tactic unit"},"response":"ok","seq_num":8} -{"record":{"source":,"state":"no goals","tactic_param_idx":0,"tactic_params":["([ (-? expr), ... ] | -? expr)","(at (* | id*))?","tactic.rewrite_cfg?"],"text":"rw","type":"interactive.parse tactic.interactive.rw_rules → interactive.parse interactive.types.location → opt_param tactic.rewrite_cfg {to_apply_cfg := {md := reducible, approx := tt, new_goals := tactic.new_goals.non_dep_first, instances := tt, auto_param := tt, opt_param := tt}, symm := ff, occs := occurrences.all} → tactic unit"},"response":"ok","seq_num":10} +{"record":{"source":,"state":"no goals","tactic_param_idx":0,"tactic_params":["([ ((← | <-)? expr), ... ] | (← | <-)? expr)","(at (* | id*))?","tactic.rewrite_cfg?"],"text":"rw","type":"interactive.parse tactic.interactive.rw_rules → interactive.parse interactive.types.location → opt_param tactic.rewrite_cfg {to_apply_cfg := {md := reducible, approx := tt, new_goals := tactic.new_goals.non_dep_first, instances := tt, auto_param := tt, opt_param := tt}, symm := ff, occs := occurrences.all} → tactic unit"},"response":"ok","seq_num":8} +{"record":{"source":,"state":"no goals","tactic_param_idx":0,"tactic_params":["([ ((← | <-)? expr), ... ] | (← | <-)? expr)","(at (* | id*))?","tactic.rewrite_cfg?"],"text":"rw","type":"interactive.parse tactic.interactive.rw_rules → interactive.parse interactive.types.location → opt_param tactic.rewrite_cfg {to_apply_cfg := {md := reducible, approx := tt, new_goals := tactic.new_goals.non_dep_first, instances := tt, auto_param := tt, opt_param := tt}, symm := ff, occs := occurrences.all} → tactic unit"},"response":"ok","seq_num":10} diff --git a/tests/lean/nested_match.lean b/tests/lean/nested_match.lean index 815d2d8125..fe951a969d 100644 --- a/tests/lean/nested_match.lean +++ b/tests/lean/nested_match.lean @@ -12,7 +12,7 @@ def g : ℕ → ℕ (match n, rfl : ∀ m, m = n → ℕ with | 0, h := 0 | (m+1), h := - have m < n, begin rw [-h], apply nat.lt_succ_self end, + have m < n, begin rw [←h], apply nat.lt_succ_self end, g m end) + 1 diff --git a/tests/lean/run/auto_quote1.lean b/tests/lean/run/auto_quote1.lean index b61fe4358b..1600871c3e 100644 --- a/tests/lean/run/auto_quote1.lean +++ b/tests/lean/run/auto_quote1.lean @@ -42,7 +42,7 @@ end example (a b c : nat) : 0 = b → 0 + a + b + c = c + a := begin intro h, - rewrite -h, -- single rewrite using symmetry + rewrite [<- h], -- single rewrite using symmetry rw [zadd, @addc a 0, zadd, addc] -- rw is shorthand for rewrite end @@ -62,7 +62,7 @@ end example (a b c : nat) : 0 = b → 0 + a + b + c = c + a := by do tactic.intro `h, - `[rewrite -h, rw zadd, rw @addc a 0, rw zadd, rw addc] + `[rewrite ←h, rw zadd, rw @addc a 0, rw zadd, rw addc] example : ∀ n m : ℕ, n + m = m + n := begin diff --git a/tests/lean/run/bin_tree.lean b/tests/lean/run/bin_tree.lean index a3b75d664b..82bf22027f 100644 --- a/tests/lean/run/bin_tree.lean +++ b/tests/lean/run/bin_tree.lean @@ -18,8 +18,8 @@ def trees_of_size : Π s, list {bt : bin_tree // size bt = s} | 0 := [⟨leaf, rfl⟩] | (n+1) := do ⟨(s1, s2), (h : s1 + s2 = n)⟩ ← pairs_with_sum n, - ⟨t1, sz1⟩ ← have s1 < n+1, by apply nat.lt_succ_of_le; rw -h; apply nat.le_add_right, + ⟨t1, sz1⟩ ← have s1 < n+1, by apply nat.lt_succ_of_le; rw ←h; apply nat.le_add_right, trees_of_size s1, - ⟨t2, sz2⟩ ← have s2 < n+1, by apply nat.lt_succ_of_le; rw -h; apply nat.le_add_left, + ⟨t2, sz2⟩ ← have s2 < n+1, by apply nat.lt_succ_of_le; rw ←h; apply nat.le_add_left, trees_of_size s2, - return ⟨branch t1 t2, by rw [-h, -sz1, -sz2]; refl⟩ + return ⟨branch t1 t2, by rw [←h, ←sz1, ←sz2]; refl⟩ diff --git a/tests/lean/run/conv_tac1.lean b/tests/lean/run/conv_tac1.lean index a093690e67..d25e2cc667 100644 --- a/tests/lean/run/conv_tac1.lean +++ b/tests/lean/run/conv_tac1.lean @@ -79,7 +79,7 @@ end example (x : nat) (f : nat → nat) (h₁ : x = 0) (h₂ : ∀ x, f x = x + x) : f x = x := begin - conv { to_rhs, rw [h₁, -add_zero 0, -h₁], }, + conv { to_rhs, rw [h₁, <- add_zero 0, <- h₁], }, exact h₂ x end diff --git a/tests/lean/run/doc_string4.lean b/tests/lean/run/doc_string4.lean index 8f643043af..043598de06 100644 --- a/tests/lean/run/doc_string4.lean +++ b/tests/lean/run/doc_string4.lean @@ -82,7 +82,7 @@ begin induction a with n x a₁ a₂ ih₁ ih₂, repeat {reflexivity}, {unfold asimp_const aval, - rewrite [-ih₁, -ih₂], + rewrite [←ih₁, ←ih₂], cases (asimp_const a₁), repeat {cases (asimp_const a₂), repeat {reflexivity}}} end @@ -126,7 +126,7 @@ lemma aval_asimp_const₃ : ∀ (a : aexp) (s : state), aval (asimp_const a) s = have h₁ := aval_asimp_const₃ a₁ s, have h₂ := aval_asimp_const₃ a₂ s, unfold asimp_const aval, - rewrite [-h₁, -h₂], + rewrite [←h₁, ←h₂], cases (asimp_const a₁); cases (asimp_const a₂); repeat {reflexivity} end diff --git a/tests/lean/run/term_app2.lean b/tests/lean/run/term_app2.lean index 488cee002c..6a8db61e9e 100644 --- a/tests/lean/run/term_app2.lean +++ b/tests/lean/run/term_app2.lean @@ -10,7 +10,7 @@ lemma nat.lt_one_add_of_lt {a b : nat} : a < b → a < 1 + b := begin intro h, have aux := lt.trans h (nat.lt_succ_self _), - rwa [-nat.add_one_eq_succ, add_comm] at aux + rwa [<- nat.add_one_eq_succ, add_comm] at aux end namespace list