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

feat(library/init/meta/interactive): rw [-h] ==> rw [← h]

Browse source 
@Armael: this change may affect your project.

The file `doc/changes.md` explains the motivation for the change.
This commit is contained in:
Leonardo de Moura 2017-07-05 11:42:55 -07:00
parent a76e839e5a
commit bb9e3ddae2
32 changed files with 229 additions and 226 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
doc/changes.md
View file

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

2
library/data/bitvec.lean
View file

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

30
library/data/hash_map.lean
View file

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

16
library/data/stream.lean
View file

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

54
library/init/algebra/field.lean
View file

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

10
library/init/algebra/functions.lean
View file

@ -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 : α))]

10
library/init/algebra/group.lean
View file

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

32
library/init/algebra/norm_num.lean
View file

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

12
library/init/algebra/ordered_field.lean
View file

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

4
library/init/algebra/ordered_group.lean
View file

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

14
library/init/algebra/ordered_ring.lean
View file

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

6
library/init/algebra/ring.lean
View file

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

2
library/init/data/array/basic.lean
View file

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

8
library/init/data/array/lemmas.lean
View file

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

4
library/init/data/int/basic.lean
View file

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

34
library/init/data/int/bitwise.lean
View file

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

6
library/init/data/int/comp_lemmas.lean
View file

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

52
library/init/data/int/lemmas.lean
View file

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

34
library/init/data/int/order.lean
View file

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

10
library/init/data/list/instances.lean
View file

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

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

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

12
library/init/data/nat/bitwise.lean
View file

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

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

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

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

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

4
tests/lean/interactive/goal_info_rw.lean
View file

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

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

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

2
tests/lean/nested_match.lean
View file

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

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

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

6
tests/lean/run/bin_tree.lean
View file

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

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

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

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

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

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

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