michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(*): modify '|' binding power, use 'abs a' instead of '|a|', and '(a | b)' instead of 'a | b'

Browse source
This commit is contained in:
Leonardo de Moura 2015-02-25 15:18:21 -08:00
parent c04c610b7b
commit 3c24461e51
13 changed files with 259 additions and 261 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
hott/init/reserved_notation.hlean
View file

@ -81,8 +81,7 @@ reserve infixl `∪`:65
/- other symbols -/
precedence `|`:55
reserve notation | a:55 |
reserve notation `(` a `|` b `)`
reserve infixl `++`:65
reserve infixr `::`:65

88
library/algebra/ordered_group.lean
View file

@ -404,97 +404,95 @@ section
definition abs (a : A) : A := if 0 ≤ a then a else -a
notation `|` a `|` := abs a
theorem abs_of_nonneg (H : a ≥ 0) : abs a = a := if_pos H
theorem abs_of_nonneg (H : a ≥ 0) : |a| = a := if_pos H
theorem abs_of_pos (H : a > 0) : abs a = a := if_pos (le_of_lt H)
theorem abs_of_pos (H : a > 0) : |a| = a := if_pos (le_of_lt H)
theorem abs_of_neg (H : a < 0) : abs a = -a := if_neg (not_le_of_lt H)
theorem abs_of_neg (H : a < 0) : |a| = -a := if_neg (not_le_of_lt H)
theorem abs_zero : abs 0 = 0 := abs_of_nonneg (le.refl _)
theorem abs_zero : |0| = 0 := abs_of_nonneg (le.refl _)
theorem abs_of_nonpos (H : a ≤ 0) : |a| = -a :=
theorem abs_of_nonpos (H : a ≤ 0) : abs a = -a :=
decidable.by_cases
(assume H1 : a = 0, by rewrite [H1, abs_zero, neg_zero])
(assume H1 : a ≠ 0,
have H2 : a < 0, from lt_of_le_of_ne H H1,
abs_of_neg H2)
theorem abs_neg (a : A) : |-a| = |a| :=
theorem abs_neg (a : A) : abs (-a) = abs a :=
or.elim (le.total 0 a)
(assume H1 : 0 ≤ a, by rewrite [abs_of_nonpos (neg_nonpos_of_nonneg H1), neg_neg, abs_of_nonneg H1])
(assume H1 : a ≤ 0, by rewrite [abs_of_nonneg (neg_nonneg_of_nonpos H1), abs_of_nonpos H1])
theorem abs_nonneg (a : A) : | a | ≥ 0 :=
theorem abs_nonneg (a : A) : abs a ≥ 0 :=
or.elim (le.total 0 a)
(assume H : 0 ≤ a, by rewrite (abs_of_nonneg H); exact H)
(assume H : a ≤ 0,
calc
0 ≤ -a : neg_nonneg_of_nonpos H
... = |a| : abs_of_nonpos H)
0 ≤ -a : neg_nonneg_of_nonpos H
... = abs a : abs_of_nonpos H)
theorem abs_abs (a : A) : | |a| | = |a| := abs_of_nonneg !abs_nonneg
theorem abs_abs (a : A) : abs (abs a) = abs a := abs_of_nonneg !abs_nonneg
theorem le_abs_self (a : A) : a ≤ |a| :=
theorem le_abs_self (a : A) : a ≤ abs a :=
or.elim (le.total 0 a)
(assume H : 0 ≤ a, abs_of_nonneg H ▸ !le.refl)
(assume H : a ≤ 0, le.trans H !abs_nonneg)
theorem neg_le_abs_self (a : A) : -a ≤ |a| :=
theorem neg_le_abs_self (a : A) : -a ≤ abs a :=
!abs_neg ▸ !le_abs_self
theorem eq_zero_of_abs_eq_zero (H : |a| = 0) : a = 0 :=
theorem eq_zero_of_abs_eq_zero (H : abs a = 0) : a = 0 :=
have H1 : a ≤ 0, from H ▸ le_abs_self a,
have H2 : -a ≤ 0, from H ▸ abs_neg a ▸ le_abs_self (-a),
le.antisymm H1 (nonneg_of_neg_nonpos H2)
theorem abs_eq_zero_iff_eq_zero (a : A) : |a| = 0 ↔ a = 0 :=
theorem abs_eq_zero_iff_eq_zero (a : A) : abs a = 0 ↔ a = 0 :=
iff.intro eq_zero_of_abs_eq_zero (assume H, congr_arg abs H ⬝ !abs_zero)
theorem abs_pos_of_pos (H : a > 0) : |a| > 0 :=
theorem abs_pos_of_pos (H : a > 0) : abs a > 0 :=
(abs_of_pos H)⁻¹ ▸ H
theorem abs_pos_of_neg (H : a < 0) : |a| > 0 :=
theorem abs_pos_of_neg (H : a < 0) : abs a > 0 :=
!abs_neg ▸ abs_pos_of_pos (neg_pos_of_neg H)
theorem abs_pos_of_ne_zero (H : a ≠ 0) : |a| > 0 :=
theorem abs_pos_of_ne_zero (H : a ≠ 0) : abs a > 0 :=
or.elim (lt_or_gt_of_ne H) abs_pos_of_neg abs_pos_of_pos
theorem abs_sub (a b : A) : |a - b| = |b - a| :=
theorem abs_sub (a b : A) : abs (a - b) = abs (b - a) :=
by rewrite [-neg_sub, abs_neg]
theorem abs.by_cases {P : A → Prop} {a : A} (H1 : P a) (H2 : P (-a)) : P |a| :=
theorem abs.by_cases {P : A → Prop} {a : A} (H1 : P a) (H2 : P (-a)) : P (abs a) :=
or.elim (le.total 0 a)
(assume H : 0 ≤ a, (abs_of_nonneg H)⁻¹ ▸ H1)
(assume H : a ≤ 0, (abs_of_nonpos H)⁻¹ ▸ H2)
theorem abs_le_of_le_of_neg_le (H1 : a ≤ b) (H2 : -a ≤ b) : |a| ≤ b :=
theorem abs_le_of_le_of_neg_le (H1 : a ≤ b) (H2 : -a ≤ b) : abs a ≤ b :=
abs.by_cases H1 H2
theorem abs_lt_of_lt_of_neg_lt (H1 : a < b) (H2 : -a < b) : |a| < b :=
theorem abs_lt_of_lt_of_neg_lt (H1 : a < b) (H2 : -a < b) : abs a < b :=
abs.by_cases H1 H2
-- the triangle inequality
context
private lemma aux1 {a b : A} (H1 : a + b ≥ 0) (H2 : a ≥ 0) : |a + b| ≤ |a| + |b| :=
private lemma aux1 {a b : A} (H1 : a + b ≥ 0) (H2 : a ≥ 0) : abs (a + b) ≤ abs a + abs b :=
decidable.by_cases
(assume H3 : b ≥ 0,
calc
|a + b| ≤ |a + b| : le.refl
... = a + b : abs_of_nonneg H1
... = |a| + b : abs_of_nonneg H2
... = |a| + |b| : abs_of_nonneg H3)
abs (a + b) ≤ abs (a + b) : le.refl
... = a + b : abs_of_nonneg H1
... = abs a + b : abs_of_nonneg H2
... = abs a + abs b : abs_of_nonneg H3)
(assume H3 : ¬ b ≥ 0,
have H4 : b ≤ 0, from le_of_lt (lt_of_not_le H3),
calc
|a + b| = a + b : abs_of_nonneg H1
... = |a| + b : abs_of_nonneg H2
... ≤ |a| + 0 : add_le_add_left H4
... ≤ |a| + -b : add_le_add_left (neg_nonneg_of_nonpos H4)
... = |a| + |b| : abs_of_nonpos H4)
abs (a + b) = a + b : abs_of_nonneg H1
... = abs a + b : abs_of_nonneg H2
... ≤ abs a + 0 : add_le_add_left H4
... ≤ abs a + -b : add_le_add_left (neg_nonneg_of_nonpos H4)
... = abs a + abs b : abs_of_nonpos H4)
private lemma aux2 {a b : A} (H1 : a + b ≥ 0) : |a + b| ≤ |a| + |b| :=
private lemma aux2 {a b : A} (H1 : a + b ≥ 0) : abs (a + b) ≤ abs a + abs b :=
or.elim (le.total b 0)
(assume H2 : b ≤ 0,
have H3 : ¬ a < 0, from
@ -503,27 +501,27 @@ section
not_lt_of_le H1 H5,
aux1 H1 (le_of_not_lt H3))
(assume H2 : 0 ≤ b,
have H3 : |b + a| ≤ |b| + |a|, from aux1 (add.comm a b ▸ H1) H2,
add.comm b a ▸ (add.comm |b| |a|) ▸ H3)
have H3 : abs (b + a) ≤ abs b + abs a, from aux1 (add.comm a b ▸ H1) H2,
add.comm b a ▸ (add.comm (abs b) (abs a)) ▸ H3)
theorem abs_add_le_abs_add_abs (a b : A) : |a + b| ≤ |a| + |b| :=
theorem abs_add_le_abs_add_abs (a b : A) : abs (a + b) ≤ abs a + abs b :=
or.elim (le.total 0 (a + b))
(assume H2 : 0 ≤ a + b, aux2 H2)
(assume H2 : a + b ≤ 0,
have H3 : -a + -b = -(a + b), by rewrite neg_add,
have H4 : -(a + b) ≥ 0, from iff.mp' (neg_nonneg_iff_nonpos (a+b)) H2,
calc
|a + b| = |-a + -b| : by rewrite [-abs_neg, neg_add]
... ≤ |-a| + |-b| : aux2 (H3⁻¹ ▸ H4)
... = |a| + |b| : by rewrite *abs_neg)
abs (a + b) = abs (-a + -b) : by rewrite [-abs_neg, neg_add]
... ≤ abs (-a) + abs (-b) : aux2 (H3⁻¹ ▸ H4)
... = abs a + abs b : by rewrite *abs_neg)
end
theorem abs_sub_abs_le_abs_sub (a b : A) : |a| - |b| ≤ |a - b| :=
have H1 : |a| - |b| + |b| ≤ |a - b| + |b|, from
theorem abs_sub_abs_le_abs_sub (a b : A) : abs a - abs b ≤ abs (a - b) :=
have H1 : abs a - abs b + abs b ≤ abs (a - b) + abs b, from
calc
|a| - |b| + |b| = |a| : sub_add_cancel
... = |a - b + b| : sub_add_cancel
... ≤ |a - b| + |b| : algebra.abs_add_le_abs_add_abs,
abs a - abs b + abs b = abs a : sub_add_cancel
... = abs (a - b + b) : sub_add_cancel
... ≤ abs (a - b) + abs b : algebra.abs_add_le_abs_add_abs,
algebra.le_of_add_le_add_right H1
end

66
library/algebra/ordered_ring.lean
View file

@ -377,83 +377,83 @@ section
-- hopefully, will be quick with the simplifier
theorem sign_mul (a b : A) : sign (a * b) = sign a * sign b := sorry
theorem abs_eq_sign_mul (a : A) : |a| = sign a * a :=
theorem abs_eq_sign_mul (a : A) : abs a = sign a * a :=
lt.by_cases
(assume H1 : 0 < a,
calc
|a| = a : abs_of_pos H1
abs a = a : abs_of_pos H1
... = 1 * a : one_mul
... = sign a * a : {(sign_of_pos H1)⁻¹})
(assume H1 : 0 = a,
calc
|a| = |0| : H1
abs a = abs 0 : H1
... = 0 : abs_zero
... = 0 * a : zero_mul
... = sign 0 * a : sign_zero
... = sign a * a : H1)
(assume H1 : a < 0,
calc
|a| = -a : abs_of_neg H1
abs a = -a : abs_of_neg H1
... = -1 * a : neg_eq_neg_one_mul
... = sign a * a : {(sign_of_neg H1)⁻¹})
theorem eq_sign_mul_abs (a : A) : a = sign a * |a| :=
theorem eq_sign_mul_abs (a : A) : a = sign a * abs a :=
lt.by_cases
(assume H1 : 0 < a,
calc
a = |a| : abs_of_pos H1
... = 1 * |a| : one_mul
... = sign a * |a| : {(sign_of_pos H1)⁻¹})
a = abs a : abs_of_pos H1
... = 1 * abs a : one_mul
... = sign a * abs a : {(sign_of_pos H1)⁻¹})
(assume H1 : 0 = a,
calc
a = 0 : H1
... = 0 * |a| : zero_mul
... = sign 0 * |a| : sign_zero
... = sign a * |a| : H1)
... = 0 * abs a : zero_mul
... = sign 0 * abs a : sign_zero
... = sign a * abs a : H1)
(assume H1 : a < 0,
calc
a = -(-a) : neg_neg
... = -|a| : {(abs_of_neg H1)⁻¹}
... = -1 * |a| : neg_eq_neg_one_mul
... = sign a * |a| : {(sign_of_neg H1)⁻¹})
... = -abs a : {(abs_of_neg H1)⁻¹}
... = -1 * abs a : neg_eq_neg_one_mul
... = sign a * abs a : {(sign_of_neg H1)⁻¹})
theorem abs_dvd_iff_dvd (a b : A) : |a| | b ↔ a | b :=
theorem abs_dvd_iff_dvd (a b : A) : (abs a | b) ↔ (a | b) :=
abs.by_cases !iff.refl !neg_dvd_iff_dvd
theorem dvd_abs_iff (a b : A) : a | |b| ↔ a | b :=
theorem dvd_abs_iff (a b : A) : (a | abs b) ↔ (a | b) :=
abs.by_cases !iff.refl !dvd_neg_iff_dvd
theorem abs_mul (a b : A) : |a * b| = |a| * |b| :=
theorem abs_mul (a b : A) : abs (a * b) = abs a * abs b :=
or.elim (le.total 0 a)
(assume H1 : 0 ≤ a,
or.elim (le.total 0 b)
(assume H2 : 0 ≤ b,
calc
|a * b| = a * b : abs_of_nonneg (mul_nonneg H1 H2)
... = |a| * b : {(abs_of_nonneg H1)⁻¹}
... = |a| * |b| : {(abs_of_nonneg H2)⁻¹})
abs (a * b) = a * b : abs_of_nonneg (mul_nonneg H1 H2)
... = abs a * b : {(abs_of_nonneg H1)⁻¹}
... = abs a * abs b : {(abs_of_nonneg H2)⁻¹})
(assume H2 : b ≤ 0,
calc
|a * b| = -(a * b) : abs_of_nonpos (mul_nonpos_of_nonneg_of_nonpos H1 H2)
... = a * -b : neg_mul_eq_mul_neg
... = |a| * -b : {(abs_of_nonneg H1)⁻¹}
... = |a| * |b| : {(abs_of_nonpos H2)⁻¹}))
abs (a * b) = -(a * b) : abs_of_nonpos (mul_nonpos_of_nonneg_of_nonpos H1 H2)
... = a * -b : neg_mul_eq_mul_neg
... = abs a * -b : {(abs_of_nonneg H1)⁻¹}
... = abs a * abs b : {(abs_of_nonpos H2)⁻¹}))
(assume H1 : a ≤ 0,
or.elim (le.total 0 b)
(assume H2 : 0 ≤ b,
calc
|a * b| = -(a * b) : abs_of_nonpos (mul_nonpos_of_nonpos_of_nonneg H1 H2)
... = -a * b : neg_mul_eq_neg_mul
... = |a| * b : {(abs_of_nonpos H1)⁻¹}
... = |a| * |b| : {(abs_of_nonneg H2)⁻¹})
abs (a * b) = -(a * b) : abs_of_nonpos (mul_nonpos_of_nonpos_of_nonneg H1 H2)
... = -a * b : neg_mul_eq_neg_mul
... = abs a * b : {(abs_of_nonpos H1)⁻¹}
... = abs a * abs b : {(abs_of_nonneg H2)⁻¹})
(assume H2 : b ≤ 0,
calc
|a * b| = a * b : abs_of_nonneg (mul_nonneg_of_nonpos_of_nonpos H1 H2)
... = -a * -b : neg_mul_neg
... = |a| * -b : {(abs_of_nonpos H1)⁻¹}
... = |a| * |b| : {(abs_of_nonpos H2)⁻¹}))
abs (a * b) = a * b : abs_of_nonneg (mul_nonneg_of_nonpos_of_nonpos H1 H2)
... = -a * -b : neg_mul_neg
... = abs a * -b : {(abs_of_nonpos H1)⁻¹}
... = abs a * abs b : {(abs_of_nonpos H2)⁻¹}))
theorem abs_mul_self (a : A) : |a| * |a| = a * a :=
theorem abs_mul_self (a : A) : abs a * abs a = a * a :=
abs.by_cases rfl !neg_mul_neg
end

58
library/algebra/ring.lean
View file

@ -72,28 +72,28 @@ section comm_semiring
include s
definition dvd (a b : A) : Prop := ∃c, b = a * c
infix `|` := dvd
notation ( a | b ) := dvd a b
theorem dvd.intro {a b c : A} (H : a * c = b) : a | b :=
theorem dvd.intro {a b c : A} (H : a * c = b) : (a | b) :=
exists.intro _ H⁻¹
theorem dvd.intro_left {a b c : A} (H : c * a = b) : a | b :=
theorem dvd.intro_left {a b c : A} (H : c * a = b) : (a | b) :=
dvd.intro (!mul.comm ▸ H)
theorem exists_eq_mul_right_of_dvd {a b : A} (H : a | b) : ∃c, b = a * c := H
theorem exists_eq_mul_right_of_dvd {a b : A} (H : (a | b)) : ∃c, b = a * c := H
theorem dvd.elim {P : Prop} {a b : A} (H₁ : a | b) (H₂ : ∀c, b = a * c → P) : P :=
theorem dvd.elim {P : Prop} {a b : A} (H₁ : (a | b)) (H₂ : ∀c, b = a * c → P) : P :=
exists.elim H₁ H₂
theorem exists_eq_mul_left_of_dvd {a b : A} (H : a | b) : ∃c, b = c * a :=
theorem exists_eq_mul_left_of_dvd {a b : A} (H : (a | b)) : ∃c, b = c * a :=
dvd.elim H (take c, assume H1 : b = a * c, exists.intro c (H1 ⬝ !mul.comm))
theorem dvd.elim_left {P : Prop} {a b : A} (H₁ : a | b) (H₂ : ∀c, b = c * a → P) : P :=
theorem dvd.elim_left {P : Prop} {a b : A} (H₁ : (a | b)) (H₂ : ∀c, b = c * a → P) : P :=
exists.elim (exists_eq_mul_left_of_dvd H₁) (take c, assume H₃ : b = c * a, H₂ c H₃)
theorem dvd.refl : a | a := dvd.intro !mul_one
theorem dvd.refl : (a | a) := dvd.intro !mul_one
theorem dvd.trans {a b c : A} (H₁ : a | b) (H₂ : b | c) : a | c :=
theorem dvd.trans {a b c : A} (H₁ : (a | b)) (H₂ : (b | c)) : (a | c) :=
dvd.elim H₁
(take d, assume H₃ : b = a * d,
dvd.elim H₂
@ -101,28 +101,28 @@ section comm_semiring
dvd.intro
(show a * (d * e) = c, by rewrite ⟨-mul.assoc, -H₃, H₄⟩)))
theorem eq_zero_of_zero_dvd {a : A} (H : 0 | a) : a = 0 :=
theorem eq_zero_of_zero_dvd {a : A} (H : (0 | a)) : a = 0 :=
dvd.elim H (take c, assume H' : a = 0 * c, H' ⬝ !zero_mul)
theorem dvd_zero : a | 0 := dvd.intro !mul_zero
theorem dvd_zero : (a | 0) := dvd.intro !mul_zero
theorem one_dvd : 1 | a := dvd.intro !one_mul
theorem one_dvd : (1 | a) := dvd.intro !one_mul
theorem dvd_mul_right : a | a * b := dvd.intro rfl
theorem dvd_mul_right : (a | a * b) := dvd.intro rfl
theorem dvd_mul_left : a | b * a := mul.comm a b ▸ dvd_mul_right a b
theorem dvd_mul_left : (a | b * a) := mul.comm a b ▸ dvd_mul_right a b
theorem dvd_mul_of_dvd_left {a b : A} (H : a | b) (c : A) : a | b * c :=
theorem dvd_mul_of_dvd_left {a b : A} (H : (a | b)) (c : A) : (a | b * c) :=
dvd.elim H
(take d,
assume H₁ : b = a * d,
dvd.intro
(show a * (d * c) = b * c, from by rewrite ⟨-mul.assoc, H₁⟩))
theorem dvd_mul_of_dvd_right {a b : A} (H : a | b) (c : A) : a | c * b :=
theorem dvd_mul_of_dvd_right {a b : A} (H : (a | b)) (c : A) : (a | c * b) :=
!mul.comm ▸ (dvd_mul_of_dvd_left H _)
theorem mul_dvd_mul {a b c d : A} (dvd_ab : a | b) (dvd_cd : c | d) : a * c | b * d :=
theorem mul_dvd_mul {a b c d : A} (dvd_ab : (a | b)) (dvd_cd : (c | d)) : (a * c | b * d) :=
dvd.elim dvd_ab
(take e, assume Haeb : b = a * e,
dvd.elim dvd_cd
@ -131,13 +131,13 @@ section comm_semiring
(show a * c * (e * f) = b * d,
by rewrite [mul.assoc, {c*_}mul.left_comm, -mul.assoc, Haeb, Hcfd])))
theorem dvd_of_mul_right_dvd {a b c : A} (H : a * b | c) : a | c :=
theorem dvd_of_mul_right_dvd {a b c : A} (H : (a * b | c)) : (a | c) :=
dvd.elim H (take d, assume Habdc : c = a * b * d, dvd.intro (!mul.assoc⁻¹ ⬝ Habdc⁻¹))
theorem dvd_of_mul_left_dvd {a b c : A} (H : a * b | c) : b | c :=
theorem dvd_of_mul_left_dvd {a b c : A} (H : (a * b | c)) : (b | c) :=
dvd_of_mul_right_dvd (mul.comm a b ▸ H)
theorem dvd_add {a b c : A} (Hab : a | b) (Hac : a | c) : a | b + c :=
theorem dvd_add {a b c : A} (Hab : (a | b)) (Hac : (a | c)) : (a | b + c) :=
dvd.elim Hab
(take d, assume Hadb : b = a * d,
dvd.elim Hac
@ -239,35 +239,35 @@ section
theorem mul_self_sub_one_eq : a * a - 1 = (a + 1) * (a - 1) :=
mul_one 1 ▸ mul_self_sub_mul_self_eq a 1
theorem dvd_neg_iff_dvd : a | -b ↔ a | b :=
theorem dvd_neg_iff_dvd : (a | -b) ↔ (a | b) :=
iff.intro
(assume H : a | -b,
(assume H : (a | -b),
dvd.elim H
(take c, assume H' : -b = a * c,
dvd.intro
(show a * -c = b,
by rewrite [-neg_mul_eq_mul_neg, -H', neg_neg])))
(assume H : a | b,
(assume H : (a | b),
dvd.elim H
(take c, assume H' : b = a * c,
dvd.intro
(show a * -c = -b,
by rewrite [-neg_mul_eq_mul_neg, -H'])))
theorem neg_dvd_iff_dvd : -a | b ↔ a | b :=
theorem neg_dvd_iff_dvd : (-a | b) ↔ (a | b) :=
iff.intro
(assume H : -a | b,
(assume H : (-a | b),
dvd.elim H
(take c, assume H' : b = -a * c,
dvd.intro
(show a * -c = b, by rewrite [-neg_mul_comm, H'])))
(assume H : a | b,
(assume H : (a | b),
dvd.elim H
(take c, assume H' : b = a * c,
dvd.intro
(show -a * -c = b, by rewrite [neg_mul_neg, H'])))
theorem dvd_sub (H₁ : a | b) (H₂ : a | c) : a | (b - c) :=
theorem dvd_sub (H₁ : (a | b)) (H₂ : (a | c)) : (a | b - c) :=
dvd_add H₁ (iff.elim_right !dvd_neg_iff_dvd H₂)
end
@ -312,14 +312,14 @@ section
-- TODO: c - b * c → c = 0 ∨ b = 1 and variants
theorem dvd_of_mul_dvd_mul_left {a b c : A} (Ha : a ≠ 0) (Hdvd : a * b | a * c) : b | c :=
theorem dvd_of_mul_dvd_mul_left {a b c : A} (Ha : a ≠ 0) (Hdvd : (a * b | a * c)) : (b | c) :=
dvd.elim Hdvd
(take d,
assume H : a * c = a * b * d,
have H1 : b * d = c, from mul.cancel_left Ha (mul.assoc a b d ▸ H⁻¹),
dvd.intro H1)
theorem dvd_of_mul_dvd_mul_right {a b c : A} (Ha : a ≠ 0) (Hdvd : b * a | c * a) : b | c :=
theorem dvd_of_mul_dvd_mul_right {a b c : A} (Ha : a ≠ 0) (Hdvd : (b * a | c * a)) : (b | c) :=
dvd.elim Hdvd
(take d,
assume H : c * a = b * a * d,

50
library/data/int/basic.lean
View file

@ -717,35 +717,35 @@ section port_algebra
theorem ne_zero_of_mul_ne_zero_left : ∀{a b : ℤ}, a * b ≠ 0 → b ≠ 0 :=
@algebra.ne_zero_of_mul_ne_zero_left _ _
definition dvd (a b : ℤ) : Prop := algebra.dvd a b
infix `|` := dvd
theorem dvd.intro : ∀{a b c : ℤ} (H : a * c = b), a | b := @algebra.dvd.intro _ _
theorem dvd.intro_left : ∀{a b c : ℤ} (H : c * a = b), a | b := @algebra.dvd.intro_left _ _
theorem exists_eq_mul_right_of_dvd : ∀{a b : ℤ} (H : a | b), ∃c, b = a * c :=
notation (a | b) := dvd a b
theorem dvd.intro : ∀{a b c : ℤ} (H : a * c = b), (a | b) := @algebra.dvd.intro _ _
theorem dvd.intro_left : ∀{a b c : ℤ} (H : c * a = b), (a | b) := @algebra.dvd.intro_left _ _
theorem exists_eq_mul_right_of_dvd : ∀{a b : ℤ} (H : (a | b)), ∃c, b = a * c :=
@algebra.exists_eq_mul_right_of_dvd _ _
theorem dvd.elim : ∀{P : Prop} {a b : ℤ} (H₁ : a | b) (H₂ : ∀c, b = a * c → P), P :=
theorem dvd.elim : ∀{P : Prop} {a b : ℤ} (H₁ : (a | b)) (H₂ : ∀c, b = a * c → P), P :=
@algebra.dvd.elim _ _
theorem exists_eq_mul_left_of_dvd : ∀{a b : ℤ} (H : a | b), ∃c, b = c * a :=
theorem exists_eq_mul_left_of_dvd : ∀{a b : ℤ} (H : (a | b)), ∃c, b = c * a :=
@algebra.exists_eq_mul_left_of_dvd _ _
theorem dvd.elim_left : ∀{P : Prop} {a b : ℤ} (H₁ : a | b) (H₂ : ∀c, b = c * a → P), P :=
theorem dvd.elim_left : ∀{P : Prop} {a b : ℤ} (H₁ : (a | b)) (H₂ : ∀c, b = c * a → P), P :=
@algebra.dvd.elim_left _ _
theorem dvd.refl : ∀a : ℤ, a | a := algebra.dvd.refl
theorem dvd.trans : ∀{a b c : ℤ} (H₁ : a | b) (H₂ : b | c), a | c := @algebra.dvd.trans _ _
theorem eq_zero_of_zero_dvd : ∀{a : ℤ} (H : 0 | a), a = 0 := @algebra.eq_zero_of_zero_dvd _ _
theorem dvd_zero : ∀a : ℤ, a | 0 := algebra.dvd_zero
theorem one_dvd : ∀a : ℤ, 1 | a := algebra.one_dvd
theorem dvd_mul_right : ∀a b : ℤ, a | a * b := algebra.dvd_mul_right
theorem dvd_mul_left : ∀a b : ℤ, a | b * a := algebra.dvd_mul_left
theorem dvd_mul_of_dvd_left : ∀{a b : ℤ} (H : a | b) (c : ℤ), a | b * c :=
theorem dvd.refl : ∀a : ℤ, (a | a) := algebra.dvd.refl
theorem dvd.trans : ∀{a b c : ℤ} (H₁ : (a | b)) (H₂ : (b | c)), (a | c) := @algebra.dvd.trans _ _
theorem eq_zero_of_zero_dvd : ∀{a : ℤ} (H : (0 | a)), a = 0 := @algebra.eq_zero_of_zero_dvd _ _
theorem dvd_zero : ∀a : ℤ, (a | 0) := algebra.dvd_zero
theorem one_dvd : ∀a : ℤ, (1 | a) := algebra.one_dvd
theorem dvd_mul_right : ∀a b : ℤ, (a | a * b) := algebra.dvd_mul_right
theorem dvd_mul_left : ∀a b : ℤ, (a | b * a) := algebra.dvd_mul_left
theorem dvd_mul_of_dvd_left : ∀{a b : ℤ} (H : (a | b)) (c : ℤ), (a | b * c) :=
@algebra.dvd_mul_of_dvd_left _ _
theorem dvd_mul_of_dvd_right : ∀{a b : ℤ} (H : a | b) (c : ℤ), a | c * b :=
theorem dvd_mul_of_dvd_right : ∀{a b : ℤ} (H : (a | b)) (c : ℤ), (a | c * b) :=
@algebra.dvd_mul_of_dvd_right _ _
theorem mul_dvd_mul : ∀{a b c d : ℤ}, a | b → c | d → a * c | b * d :=
theorem mul_dvd_mul : ∀{a b c d : ℤ}, (a | b) → (c | d) → (a * c | b * d) :=
@algebra.mul_dvd_mul _ _
theorem dvd_of_mul_right_dvd : ∀{a b c : ℤ}, a * b | c → a | c :=
theorem dvd_of_mul_right_dvd : ∀{a b c : ℤ}, (a * b | c) → (a | c) :=
@algebra.dvd_of_mul_right_dvd _ _
theorem dvd_of_mul_left_dvd : ∀{a b c : ℤ}, a * b | c → b | c :=
theorem dvd_of_mul_left_dvd : ∀{a b c : ℤ}, (a * b | c) → (b | c) :=
@algebra.dvd_of_mul_left_dvd _ _
theorem dvd_add : ∀{a b c : ℤ}, a | b → a | c → a | b + c := @algebra.dvd_add _ _
theorem dvd_add : ∀{a b c : ℤ}, (a | b) → (a | c) → (a | b + c) := @algebra.dvd_add _ _
theorem zero_mul : ∀a : ℤ, 0 * a = 0 := algebra.zero_mul
theorem mul_zero : ∀a : ℤ, a * 0 = 0 := algebra.mul_zero
theorem neg_mul_eq_neg_mul : ∀a b : ℤ, -(a * b) = -a * b := algebra.neg_mul_eq_neg_mul
@ -764,9 +764,9 @@ section port_algebra
algebra.mul_self_sub_mul_self_eq
theorem mul_self_sub_one_eq : ∀a : ℤ, a * a - 1 = (a + 1) * (a - 1) :=
algebra.mul_self_sub_one_eq
theorem dvd_neg_iff_dvd : ∀a b : ℤ, a | -b ↔ a | b := algebra.dvd_neg_iff_dvd
theorem neg_dvd_iff_dvd : ∀a b : ℤ, -a | b ↔ a | b := algebra.neg_dvd_iff_dvd
theorem dvd_sub : ∀a b c : ℤ, a | b → a | c → a | (b - c) := algebra.dvd_sub
theorem dvd_neg_iff_dvd : ∀a b : ℤ, (a | -b) ↔ (a | b) := algebra.dvd_neg_iff_dvd
theorem neg_dvd_iff_dvd : ∀a b : ℤ, (-a | b) ↔ (a | b) := algebra.neg_dvd_iff_dvd
theorem dvd_sub : ∀a b c : ℤ, (a | b) → (a | c) → (a | b - c) := algebra.dvd_sub
theorem mul_ne_zero : ∀{a b : ℤ}, a ≠ 0 → b ≠ 0 → a * b ≠ 0 := @algebra.mul_ne_zero _ _
theorem mul.cancel_right : ∀{a b c : ℤ}, a ≠ 0 → b * a = c * a → b = c :=
@algebra.mul.cancel_right _ _
@ -776,9 +776,9 @@ section port_algebra
algebra.mul_self_eq_mul_self_iff
theorem mul_self_eq_one_iff : ∀a : ℤ, a * a = 1 ↔ a = 1 ∨ a = -1 :=
algebra.mul_self_eq_one_iff
theorem dvd_of_mul_dvd_mul_left : ∀{a b c : ℤ}, a ≠ 0 → a * b | a * c → b | c :=
theorem dvd_of_mul_dvd_mul_left : ∀{a b c : ℤ}, a ≠ 0 → (a * b | a * c) → (b | c) :=
@algebra.dvd_of_mul_dvd_mul_left _ _
theorem dvd_of_mul_dvd_mul_right : ∀{a b c : ℤ}, a ≠ 0 → b * a | c * a → b | c :=
theorem dvd_of_mul_dvd_mul_right : ∀{a b c : ℤ}, a ≠ 0 → (b * a | c * a) → (b | c) :=
@algebra.dvd_of_mul_dvd_mul_right _ _
end port_algebra

42
library/data/int/div.lean
View file

@ -100,7 +100,7 @@ calc
... = a - a div b * b : neg_mul_neg
... = a mod b : rfl
theorem mod_abs (a b : ℤ) : a mod |b| = a mod b :=
theorem mod_abs (a b : ℤ) : a mod (abs b) = a mod b :=
abs.by_cases rfl !mod_neg
theorem zero_mod (b : ℤ) : 0 mod b = 0 :=
@ -109,44 +109,44 @@ by rewrite [↑modulo, zero_div, zero_mul, sub_zero]
theorem mod_zero (a : ℤ) : a mod 0 = a :=
by rewrite [↑modulo, mul_zero, sub_zero]
private lemma of_nat_mod_abs (m : ℕ) (b : ℤ) : m mod |b| = (#nat m mod (nat_abs b)) :=
private lemma of_nat_mod_abs (m : ℕ) (b : ℤ) : m mod (abs b) = (#nat m mod (nat_abs b)) :=
calc
m mod |b| = m mod (nat_abs b) : of_nat_nat_abs
... = (#nat m mod (nat_abs b)) : of_nat_mod_of_nat
m mod (abs b) = m mod (nat_abs b) : of_nat_nat_abs
... = (#nat m mod (nat_abs b)) : of_nat_mod_of_nat
private lemma of_nat_mod_abs_lt (m : ℕ) {b : ℤ} (H : b ≠ 0) : m mod |b| < |b| :=
have H1 : |b| > 0, from abs_pos_of_ne_zero H,
private lemma of_nat_mod_abs_lt (m : ℕ) {b : ℤ} (H : b ≠ 0) : m mod (abs b) < (abs b) :=
have H1 : abs b > 0, from abs_pos_of_ne_zero H,
have H2 : (#nat nat_abs b > 0), from lt_of_of_nat_lt_of_nat (!of_nat_nat_abs⁻¹ ▸ H1),
calc
m mod |b| = (#nat m mod (nat_abs b)) : of_nat_mod_abs m b
m mod (abs b) = (#nat m mod (nat_abs b)) : of_nat_mod_abs m b
... < nat_abs b : of_nat_lt_of_nat (nat.mod_lt H2)
... = |b| : of_nat_nat_abs _
... = abs b : of_nat_nat_abs _
theorem mod_nonneg (a : ℤ) {b : ℤ} (H : b ≠ 0) : a mod b ≥ 0 :=
have H1 : |b| > 0, from abs_pos_of_ne_zero H,
have H2 : a mod |b| ≥ 0, from
have H1 : abs b > 0, from abs_pos_of_ne_zero H,
have H2 : a mod (abs b) ≥ 0, from
int.cases_on a
(take m, (of_nat_mod_abs m b)⁻¹ ▸ !of_nat_nonneg)
(take m,
have H3 : 1 + m mod |b| ≤ |b|, from (!add.comm ▸ add_one_le_of_lt (of_nat_mod_abs_lt m H)),
have H3 : 1 + m mod (abs b) ≤ (abs b), from (!add.comm ▸ add_one_le_of_lt (of_nat_mod_abs_lt m H)),
calc
-[ m +1] mod |b| = |b| - 1 - m mod |b| : neg_succ_of_nat_mod _ H1
... = |b| - (1 + m mod |b|) : by rewrite [*sub_eq_add_neg, neg_add, add.assoc]
-[ m +1] mod (abs b) = abs b - 1 - m mod (abs b) : neg_succ_of_nat_mod _ H1
... = abs b - (1 + m mod (abs b)) : by rewrite [*sub_eq_add_neg, neg_add, add.assoc]
... ≥ 0 : iff.mp' !sub_nonneg_iff_le H3),
!mod_abs ▸ H2
theorem mod_lt (a : ℤ) {b : ℤ} (H : b ≠ 0) : a mod b < |b| :=
have H1 : |b| > 0, from abs_pos_of_ne_zero H,
have H2 : a mod |b| < |b|, from
theorem mod_lt (a : ℤ) {b : ℤ} (H : b ≠ 0) : a mod b < (abs b) :=
have H1 : abs b > 0, from abs_pos_of_ne_zero H,
have H2 : a mod (abs b) < abs b, from
int.cases_on a
(take m, of_nat_mod_abs_lt m H)
(take m,
have H3 : |b| ≠ 0, from assume H', H (eq_zero_of_abs_eq_zero H'),
have H4 : 1 + m mod |b| > 0, from add_pos_of_pos_of_nonneg dec_trivial (mod_nonneg _ H3),
have H3 : abs b ≠ 0, from assume H', H (eq_zero_of_abs_eq_zero H'),
have H4 : 1 + m mod (abs b) > 0, from add_pos_of_pos_of_nonneg dec_trivial (mod_nonneg _ H3),
calc
-[ m +1] mod |b| = |b| - 1 - m mod |b| : neg_succ_of_nat_mod _ H1
... = |b| - (1 + m mod |b|) : by rewrite [*sub_eq_add_neg, neg_add, add.assoc]
... < |b| : sub_lt_self _ H4),
-[ m +1] mod (abs b) = abs b - 1 - m mod (abs b) : neg_succ_of_nat_mod _ H1
... = abs b - (1 + m mod (abs b)) : by rewrite [*sub_eq_add_neg, neg_add, add.assoc]
... < abs b : sub_lt_self _ H4),
!mod_abs ▸ H2
/- both div and mod -/

58
library/data/int/order.lean
View file

@ -455,32 +455,32 @@ section port_algebra
theorem eq_zero_of_neg_eq : ∀{a : ℤ}, -a = a → a = 0 := @algebra.eq_zero_of_neg_eq _ _
definition abs : ℤ → ℤ := algebra.abs
notation `|` a `|` := abs a
theorem abs_of_nonneg : ∀{a : ℤ}, a ≥ 0 → |a| = a := @algebra.abs_of_nonneg _ _
theorem abs_of_pos : ∀{a : ℤ}, a > 0 → |a| = a := @algebra.abs_of_pos _ _
theorem abs_of_neg : ∀{a : ℤ}, a < 0 → |a| = -a := @algebra.abs_of_neg _ _
theorem abs_zero : |0| = 0 := algebra.abs_zero
theorem abs_of_nonpos : ∀{a : ℤ}, a ≤ 0 → |a| = -a := @algebra.abs_of_nonpos _ _
theorem abs_neg : ∀a : ℤ, |-a| = |a| := algebra.abs_neg
theorem abs_nonneg : ∀a : ℤ, | a | ≥ 0 := algebra.abs_nonneg
theorem abs_abs : ∀a : ℤ, | |a| | = |a| := algebra.abs_abs
theorem le_abs_self : ∀a : ℤ, a ≤ |a| := algebra.le_abs_self
theorem neg_le_abs_self : ∀a : ℤ, -a ≤ |a| := algebra.neg_le_abs_self
theorem eq_zero_of_abs_eq_zero : ∀{a : ℤ}, |a| = 0 → a = 0 := @algebra.eq_zero_of_abs_eq_zero _ _
theorem abs_eq_zero_iff_eq_zero : ∀a : ℤ, |a| = 0 ↔ a = 0 := algebra.abs_eq_zero_iff_eq_zero
theorem abs_pos_of_pos : ∀{a : ℤ}, a > 0 → |a| > 0 := @algebra.abs_pos_of_pos _ _
theorem abs_pos_of_neg : ∀{a : ℤ}, a < 0 → |a| > 0 := @algebra.abs_pos_of_neg _ _
theorem abs_pos_of_ne_zero : ∀{a : ℤ}, a ≠ 0 → |a| > 0 := @algebra.abs_pos_of_ne_zero _ _
theorem abs_sub : ∀a b : ℤ, |a - b| = |b - a| := algebra.abs_sub
theorem abs.by_cases : ∀{P : ℤ → Prop}, ∀{a : ℤ}, P a → P (-a) → P (|a|) :=
theorem abs_of_nonneg : ∀{a : ℤ}, a ≥ 0 → abs a = a := @algebra.abs_of_nonneg _ _
theorem abs_of_pos : ∀{a : ℤ}, a > 0 → abs a = a := @algebra.abs_of_pos _ _
theorem abs_of_neg : ∀{a : ℤ}, a < 0 → abs a = -a := @algebra.abs_of_neg _ _
theorem abs_zero : abs 0 = 0 := algebra.abs_zero
theorem abs_of_nonpos : ∀{a : ℤ}, a ≤ 0 → abs a = -a := @algebra.abs_of_nonpos _ _
theorem abs_neg : ∀a : ℤ, abs (-a) = abs a := algebra.abs_neg
theorem abs_nonneg : ∀a : ℤ, abs a ≥ 0 := algebra.abs_nonneg
theorem abs_abs : ∀a : ℤ, abs (abs a) = abs a := algebra.abs_abs
theorem le_abs_self : ∀a : ℤ, a ≤ abs a := algebra.le_abs_self
theorem neg_le_abs_self : ∀a : ℤ, -a ≤ abs a := algebra.neg_le_abs_self
theorem eq_zero_of_abs_eq_zero : ∀{a : ℤ}, abs a = 0 → a = 0 := @algebra.eq_zero_of_abs_eq_zero _ _
theorem abs_eq_zero_iff_eq_zero : ∀a : ℤ, abs a = 0 ↔ a = 0 := algebra.abs_eq_zero_iff_eq_zero
theorem abs_pos_of_pos : ∀{a : ℤ}, a > 0 → abs a > 0 := @algebra.abs_pos_of_pos _ _
theorem abs_pos_of_neg : ∀{a : ℤ}, a < 0 → abs a > 0 := @algebra.abs_pos_of_neg _ _
theorem abs_pos_of_ne_zero : ∀{a : ℤ}, a ≠ 0 → abs a > 0 := @algebra.abs_pos_of_ne_zero _ _
theorem abs_sub : ∀a b : ℤ, abs (a - b) = abs (b - a) := algebra.abs_sub
theorem abs.by_cases : ∀{P : ℤ → Prop}, ∀{a : ℤ}, P a → P (-a) → P (abs a) :=
@algebra.abs.by_cases _ _
theorem abs_le_of_le_of_neg_le : ∀{a b : ℤ}, a ≤ b → -a ≤ b → |a| ≤ b :=
theorem abs_le_of_le_of_neg_le : ∀{a b : ℤ}, a ≤ b → -a ≤ b → abs a ≤ b :=
@algebra.abs_le_of_le_of_neg_le _ _
theorem abs_lt_of_lt_of_neg_lt : ∀{a b : ℤ}, a < b → -a < b → |a| < b :=
theorem abs_lt_of_lt_of_neg_lt : ∀{a b : ℤ}, a < b → -a < b → abs a < b :=
@algebra.abs_lt_of_lt_of_neg_lt _ _
theorem abs_add_le_abs_add_abs : ∀a b : ℤ, |a + b| ≤ |a| + |b| :=
theorem abs_add_le_abs_add_abs : ∀a b : ℤ, abs (a + b) ≤ abs a + abs b :=
algebra.abs_add_le_abs_add_abs
theorem abs_sub_abs_le_abs_sub : ∀a b : ℤ, |a| - |b| ≤ |a - b| :=
theorem abs_sub_abs_le_abs_sub : ∀a b : ℤ, abs a - abs b ≤ abs (a - b) :=
algebra.abs_sub_abs_le_abs_sub
theorem mul_le_mul_of_nonneg_left : ∀{a b c : ℤ}, a ≤ b → 0 ≤ c → c * a ≤ c * b :=
@ -549,12 +549,12 @@ section port_algebra
@algebra.neg_of_sign_eq_neg_one _ _
theorem sign_neg : ∀a : ℤ, sign (-a) = -(sign a) := algebra.sign_neg
theorem sign_mul : ∀a b : ℤ, sign (a * b) = sign a * sign b := algebra.sign_mul
theorem abs_eq_sign_mul : ∀a : ℤ, |a| = sign a * a := algebra.abs_eq_sign_mul
theorem eq_sign_mul_abs : ∀a : ℤ, a = sign a * |a| := algebra.eq_sign_mul_abs
theorem abs_dvd_iff_dvd : ∀a b : ℤ, |a| | b ↔ a | b := algebra.abs_dvd_iff_dvd
theorem dvd_abs_iff : ∀a b : ℤ, a | |b| ↔ a | b := algebra.dvd_abs_iff
theorem abs_mul : ∀a b : ℤ, |a * b| = |a| * |b| := algebra.abs_mul
theorem abs_mul_self : ∀a : ℤ, |a| * |a| = a * a := algebra.abs_mul_self
theorem abs_eq_sign_mul : ∀a : ℤ, abs a = sign a * a := algebra.abs_eq_sign_mul
theorem eq_sign_mul_abs : ∀a : ℤ, a = sign a * abs a := algebra.eq_sign_mul_abs
theorem abs_dvd_iff_dvd : ∀a b : ℤ, (abs a | b) ↔ (a | b) := algebra.abs_dvd_iff_dvd
theorem dvd_abs_iff : ∀a b : ℤ, (a | abs b) ↔ (a | b) := algebra.dvd_abs_iff
theorem abs_mul : ∀a b : ℤ, abs (a * b) = abs a * abs b := algebra.abs_mul
theorem abs_mul_self : ∀a : ℤ, abs a * abs a = a * a := algebra.abs_mul_self
end port_algebra
/- more facts specific to int -/
@ -580,7 +580,7 @@ calc
of_nat (nat_abs a) = of_nat (nat_abs (-a)) : nat_abs_neg
... = -a : of_nat_nat_abs_of_nonneg H1
theorem of_nat_nat_abs (b : ℤ) : nat_abs b = |b| :=
theorem of_nat_nat_abs (b : ℤ) : nat_abs b = abs b :=
or.elim (le.total 0 b)
(assume H : b ≥ 0, of_nat_nat_abs_of_nonneg H ⬝ (abs_of_nonneg H)⁻¹)
(assume H : b ≤ 0, of_nat_nat_abs_of_nonpos H ⬝ (abs_of_nonpos H)⁻¹)

41
library/data/nat/basic.lean
View file

@ -316,35 +316,36 @@ section port_algebra
theorem mul.right_comm : ∀a b c : ℕ, (a * b) * c = (a * c) * b := algebra.mul.right_comm
definition dvd (a b : ℕ) : Prop := algebra.dvd a b
infix `|` := dvd
theorem dvd.intro : ∀{a b c : ℕ} (H : a * c = b), a | b := @algebra.dvd.intro _ _
theorem dvd.intro_left : ∀{a b c : ℕ} (H : c * a = b), a | b := @algebra.dvd.intro_left _ _
theorem exists_eq_mul_right_of_dvd : ∀{a b : ℕ} (H : a | b), ∃c, b = a * c :=
notation (a | b) := dvd a b
theorem dvd.intro : ∀{a b c : ℕ} (H : a * c = b), (a | b) := @algebra.dvd.intro _ _
theorem dvd.intro_left : ∀{a b c : ℕ} (H : c * a = b), (a | b) := @algebra.dvd.intro_left _ _
theorem exists_eq_mul_right_of_dvd : ∀{a b : ℕ} (H : (a | b)), ∃c, b = a * c :=
@algebra.exists_eq_mul_right_of_dvd _ _
theorem dvd.elim : ∀{P : Prop} {a b : ℕ} (H₁ : a | b) (H₂ : ∀c, b = a * c → P), P :=
theorem dvd.elim : ∀{P : Prop} {a b : ℕ} (H₁ : (a | b)) (H₂ : ∀c, b = a * c → P), P :=
@algebra.dvd.elim _ _
theorem exists_eq_mul_left_of_dvd : ∀{a b : ℕ} (H : a | b), ∃c, b = c * a :=
theorem exists_eq_mul_left_of_dvd : ∀{a b : ℕ} (H : (a | b)), ∃c, b = c * a :=
@algebra.exists_eq_mul_left_of_dvd _ _
theorem dvd.elim_left : ∀{P : Prop} {a b : ℕ} (H₁ : a | b) (H₂ : ∀c, b = c * a → P), P :=
theorem dvd.elim_left : ∀{P : Prop} {a b : ℕ} (H₁ : (a | b)) (H₂ : ∀c, b = c * a → P), P :=
@algebra.dvd.elim_left _ _
theorem dvd.refl : ∀a : ℕ, a | a := algebra.dvd.refl
theorem dvd.trans : ∀{a b c : ℕ} (H₁ : a | b) (H₂ : b | c), a | c := @algebra.dvd.trans _ _
theorem eq_zero_of_zero_dvd : ∀{a : ℕ} (H : 0 | a), a = 0 := @algebra.eq_zero_of_zero_dvd _ _
theorem dvd_zero : ∀a : ℕ, a | 0 := algebra.dvd_zero
theorem one_dvd : ∀a : ℕ, 1 | a := algebra.one_dvd
theorem dvd_mul_right : ∀a b : ℕ, a | a * b := algebra.dvd_mul_right
theorem dvd_mul_left : ∀a b : ℕ, a | b * a := algebra.dvd_mul_left
theorem dvd_mul_of_dvd_left : ∀{a b : ℕ} (H : a | b) (c : ℕ), a | b * c :=
theorem dvd.refl : ∀a : ℕ, (a | a) := algebra.dvd.refl
theorem dvd.trans : ∀{a b c : ℕ} (H₁ : (a | b)) (H₂ : (b | c)), (a | c) := @algebra.dvd.trans _ _
theorem eq_zero_of_zero_dvd : ∀{a : ℕ} (H : (0 | a)), a = 0 := @algebra.eq_zero_of_zero_dvd _ _
theorem dvd_zero : ∀a : ℕ, (a | 0) := algebra.dvd_zero
theorem one_dvd : ∀a : ℕ, (1 | a) := algebra.one_dvd
theorem dvd_mul_right : ∀a b : ℕ, (a | a * b) := algebra.dvd_mul_right
theorem dvd_mul_left : ∀a b : ℕ, (a | b * a) := algebra.dvd_mul_left
theorem dvd_mul_of_dvd_left : ∀{a b : ℕ} (H : (a | b)) (c : ℕ), (a | b * c) :=
@algebra.dvd_mul_of_dvd_left _ _
theorem dvd_mul_of_dvd_right : ∀{a b : ℕ} (H : a | b) (c : ℕ), a | c * b :=
theorem dvd_mul_of_dvd_right : ∀{a b : ℕ} (H : (a | b)) (c : ℕ), (a | c * b) :=
@algebra.dvd_mul_of_dvd_right _ _
theorem mul_dvd_mul : ∀{a b c d : ℕ}, a | b → c | d → a * c | b * d :=
theorem mul_dvd_mul : ∀{a b c d : ℕ}, (a | b) → (c | d) → (a * c | b * d) :=
@algebra.mul_dvd_mul _ _
theorem dvd_of_mul_right_dvd : ∀{a b c : ℕ}, a * b | c → a | c :=
theorem dvd_of_mul_right_dvd : ∀{a b c : ℕ}, (a * b | c) → (a | c) :=
@algebra.dvd_of_mul_right_dvd _ _
theorem dvd_of_mul_left_dvd : ∀{a b c : ℕ}, a * b | c → b | c :=
theorem dvd_of_mul_left_dvd : ∀{a b c : ℕ}, (a * b | c) → (b | c) :=
@algebra.dvd_of_mul_left_dvd _ _
theorem dvd_add : ∀{a b c : ℕ}, a | b → a | c → a | b + c := @algebra.dvd_add _ _
theorem dvd_add : ∀{a b c : ℕ}, (a | b) → (a | c) → (a | b + c) := @algebra.dvd_add _ _
end port_algebra
end nat

100
library/data/nat/div.lean
View file

@ -324,28 +324,28 @@ calc
/- divides -/
theorem dvd_of_mod_eq_zero {m n : ℕ} (H : n mod m = 0) : m | n :=
theorem dvd_of_mod_eq_zero {m n : ℕ} (H : n mod m = 0) : (m | n) :=
dvd.intro (!mul.comm ▸ div_mul_cancel_of_mod_eq_zero H)
theorem mod_eq_zero_of_dvd {m n : ℕ} (H : m | n) : n mod m = 0 :=
theorem mod_eq_zero_of_dvd {m n : ℕ} (H : (m | n)) : n mod m = 0 :=
dvd.elim H
(take z,
assume H1 : n = m * z,
H1⁻¹ ▸ !mul_mod_right)
theorem dvd_iff_mod_eq_zero (m n : ℕ) : m | n ↔ n mod m = 0 :=
theorem dvd_iff_mod_eq_zero (m n : ℕ) : (m | n) ↔ n mod m = 0 :=
iff.intro mod_eq_zero_of_dvd dvd_of_mod_eq_zero
definition dvd.decidable_rel [instance] : decidable_rel dvd :=
take m n, decidable_of_decidable_of_iff _ (iff.symm !dvd_iff_mod_eq_zero)
theorem div_mul_cancel {m n : ℕ} (H : n | m) : m div n * n = m :=
theorem div_mul_cancel {m n : ℕ} (H : (n | m)) : m div n * n = m :=
div_mul_cancel_of_mod_eq_zero (mod_eq_zero_of_dvd H)
theorem mul_div_cancel' {m n : ℕ} (H : n | m) : n * (m div n) = m :=
theorem mul_div_cancel' {m n : ℕ} (H : (n | m)) : n * (m div n) = m :=
!mul.comm ▸ div_mul_cancel H
theorem eq_mul_of_div_eq {m n k : ℕ} (H1 : m | n) (H2 : n div m = k) : n = m * k :=
theorem eq_mul_of_div_eq {m n k : ℕ} (H1 : (m | n)) (H2 : n div m = k) : n = m * k :=
eq.symm (calc
m * k = m * (n div m) : H2
... = n : mul_div_cancel' H1)
@ -355,7 +355,7 @@ calc
n = n * k div k : mul_div_cancel _ H1
... = m div k : H2
theorem dvd_of_dvd_add_left {m n₁ n₂ : ℕ} (H₁ : m | n₁ + n₂) (H₂ : m | n₁) : m | n₂ :=
theorem dvd_of_dvd_add_left {m n₁ n₂ : ℕ} (H₁ : (m | n₁ + n₂)) (H₂ : (m | n₁)) : (m | n₂) :=
obtain (c₁ : nat) (Hc₁ : n₁ + n₂ = m * c₁), from H₁,
obtain (c₂ : nat) (Hc₂ : n₁ = m * c₂), from H₂,
have aux : m * (c₁ - c₂) = n₂, from calc
@ -365,25 +365,25 @@ have aux : m * (c₁ - c₂) = n₂, from calc
... = n₂ : add_sub_cancel_left,
dvd.intro aux
theorem dvd_of_dvd_add_right {m n1 n2 : ℕ} (H : m | (n1 + n2)) : m | n2 → m | n1 :=
theorem dvd_of_dvd_add_right {m n1 n2 : ℕ} (H : (m | (n1 + n2))) : (m | n2) → (m | n1) :=
dvd_of_dvd_add_left (!add.comm ▸ H)
theorem dvd_sub {m n1 n2 : ℕ} (H1 : m | n1) (H2 : m | n2) : m | (n1 - n2) :=
theorem dvd_sub {m n1 n2 : ℕ} (H1 : (m | n1)) (H2 : (m | n2)) : (m | n1 - n2) :=
by_cases
(assume H3 : n1 ≥ n2,
have H4 : n1 = n1 - n2 + n2, from (sub_add_cancel H3)⁻¹,
show m | n1 - n2, from dvd_of_dvd_add_right (H4 ▸ H1) H2)
show (m | n1 - n2), from dvd_of_dvd_add_right (H4 ▸ H1) H2)
(assume H3 : ¬ (n1 ≥ n2),
have H4 : n1 - n2 = 0, from sub_eq_zero_of_le (le_of_lt (lt_of_not_le H3)),
show m | n1 - n2, from H4⁻¹ ▸ dvd_zero _)
show (m | n1 - n2), from H4⁻¹ ▸ dvd_zero _)
theorem dvd.antisymm {m n : ℕ} : m | n → n | m → m = n :=
theorem dvd.antisymm {m n : ℕ} : (m | n) → (n | m) → m = n :=
by_cases_zero_pos n
(assume H1, assume H2 : 0 | m, eq_zero_of_zero_dvd H2)
(assume H1, assume H2 : (0 | m), eq_zero_of_zero_dvd H2)
(take n,
assume Hpos : n > 0,
assume H1 : m | n,
assume H2 : n | m,
assume H1 : (m | n),
assume H2 : (n | m),
obtain k (Hk : n = m * k), from exists_eq_mul_right_of_dvd H1,
obtain l (Hl : m = n * l), from exists_eq_mul_right_of_dvd H2,
have H3 : n * (l * k) = n, from !mul.assoc ▸ Hl ▸ Hk⁻¹,
@ -391,7 +391,7 @@ by_cases_zero_pos n
have H5 : k = 1, from eq_one_of_mul_eq_one_left H4,
show m = n, from (mul_one m)⁻¹ ⬝ (H5 ▸ Hk⁻¹))
theorem mul_div_assoc (m : ℕ) {n k : ℕ} (H : k | n) : m * n div k = m * (n div k) :=
theorem mul_div_assoc (m : ℕ) {n k : ℕ} (H : (k | n)) : m * n div k = m * (n div k) :=
or.elim (eq_zero_or_pos k)
(assume H1 : k = 0,
calc
@ -407,17 +407,17 @@ or.elim (eq_zero_or_pos k)
... = m * (n div k) * k div k : mul.assoc
... = m * (n div k) : mul_div_cancel _ H1)
theorem dvd_of_mul_dvd_mul_left {m n k : ℕ} (kpos : k > 0) (H : k * m | k * n) : m | n :=
theorem dvd_of_mul_dvd_mul_left {m n k : ℕ} (kpos : k > 0) (H : (k * m | k * n)) : (m | n) :=
dvd.elim H
(take l,
assume H1 : k * n = k * m * l,
have H2 : n = m * l, from eq_of_mul_eq_mul_left kpos (H1 ⬝ !mul.assoc),
dvd.intro H2⁻¹)
theorem dvd_of_mul_dvd_mul_right {m n k : ℕ} (kpos : k > 0) (H : m * k | n * k) : m | n :=
theorem dvd_of_mul_dvd_mul_right {m n k : ℕ} (kpos : k > 0) (H : (m * k | n * k)) : (m | n) :=
dvd_of_mul_dvd_mul_left kpos (!mul.comm ▸ !mul.comm ▸ H)
theorem div_dvd_div {k m n : ℕ} (H1 : k | m) (H2 : m | n) : m div k | n div k :=
theorem div_dvd_div {k m n : ℕ} (H1 : (k | m)) (H2 : (m | n)) : (m div k | n div k) :=
have H3 : m = m div k * k, from (div_mul_cancel H1)⁻¹,
have H4 : n = n div k * k, from (div_mul_cancel (dvd.trans H1 H2))⁻¹,
or.elim (eq_zero_or_pos k)
@ -517,9 +517,9 @@ gcd.induction m n
(take m n,
assume npos : 0 < n,
assume IH : (gcd n (m mod n) | n) ∧ (gcd n (m mod n) | (m mod n)),
have H : gcd n (m mod n) | (m div n * n + m mod n), from
have H : (gcd n (m mod n) | (m div n * n + m mod n)), from
dvd_add (dvd.trans (and.elim_left IH) !dvd_mul_left) (and.elim_right IH),
have H1 : gcd n (m mod n) | m, from eq_div_mul_add_mod⁻¹ ▸ H,
have H1 : (gcd n (m mod n) | m), from eq_div_mul_add_mod⁻¹ ▸ H,
have gcd_eq : gcd n (m mod n) = gcd m n, from !gcd_rec⁻¹,
show (gcd m n | m) ∧ (gcd m n | n), from gcd_eq ▸ (and.intro H1 (and.elim_left IH)))
@ -527,19 +527,19 @@ theorem gcd_dvd_left (m n : ℕ) : (gcd m n | m) := and.elim_left !gcd_dvd
theorem gcd_dvd_right (m n : ℕ) : (gcd m n | n) := and.elim_right !gcd_dvd
theorem dvd_gcd {m n k : ℕ} : k | m → k | n → k | (gcd m n) :=
theorem dvd_gcd {m n k : ℕ} : (k | m) → (k | n) → (k | gcd m n) :=
gcd.induction m n
(take m, assume (h₁ : k | m) (h₂ : k | 0),
show k | gcd m 0, from !gcd_zero_right⁻¹ ▸ h₁)
(take m, assume (h₁ : (k | m)) (h₂ : (k | 0)),
show (k | gcd m 0), from !gcd_zero_right⁻¹ ▸ h₁)
(take m n,
assume npos : n > 0,
assume IH : k | n → k | (m mod n) → k | gcd n (m mod n),
assume H1 : k | m,
assume H2 : k | n,
have H3 : k | m div n * n + m mod n, from eq_div_mul_add_mod ▸ H1,
have H4 : k | m mod n, from nat.dvd_of_dvd_add_left H3 (dvd.trans H2 (by simp)),
assume IH : (k | n) → (k | m mod n) → (k | gcd n (m mod n)),
assume H1 : (k | m),
assume H2 : (k | n),
have H3 : (k | m div n * n + m mod n), from eq_div_mul_add_mod ▸ H1,
have H4 : (k | m mod n), from nat.dvd_of_dvd_add_left H3 (dvd.trans H2 (by simp)),
have gcd_eq : gcd n (m mod n) = gcd m n, from !gcd_rec⁻¹,
show k | gcd m n, from gcd_eq ▸ IH H2 H4)
show (k | gcd m n), from gcd_eq ▸ IH H2 H4)
theorem gcd.comm (m n : ℕ) : gcd m n = gcd n m :=
dvd.antisymm
@ -595,7 +595,7 @@ or.elim (eq_zero_or_pos m)
theorem eq_zero_of_gcd_eq_zero_right {m n : ℕ} (H : gcd m n = 0) : n = 0 :=
eq_zero_of_gcd_eq_zero_left (!gcd.comm ▸ H)
theorem gcd_div {m n k : ℕ} (H1 : k | m) (H2 : k | n) : gcd (m div k) (n div k) = gcd m n div k :=
theorem gcd_div {m n k : ℕ} (H1 : (k | m)) (H2 : (k | n)) : gcd (m div k) (n div k) = gcd m n div k :=
or.elim (eq_zero_or_pos k)
(assume H3 : k = 0,
calc
@ -613,16 +613,16 @@ or.elim (eq_zero_or_pos k)
... = gcd m (n div k * k) : div_mul_cancel H1
... = gcd m n : div_mul_cancel H2))
theorem gcd_dvd_gcd_mul_left (m n k : ℕ) : gcd m n | gcd (k * m) n :=
theorem gcd_dvd_gcd_mul_left (m n k : ℕ) : (gcd m n | gcd (k * m) n) :=
dvd_gcd (dvd.trans !gcd_dvd_left !dvd_mul_left) !gcd_dvd_right
theorem gcd_dvd_gcd_mul_right (m n k : ℕ) : gcd m n | gcd (m * k) n :=
theorem gcd_dvd_gcd_mul_right (m n k : ℕ) : (gcd m n | gcd (m * k) n) :=
!mul.comm ▸ !gcd_dvd_gcd_mul_left
theorem gcd_dvd_gcd_mul_left_right (m n k : ℕ) : gcd m n | gcd m (k * n) :=
theorem gcd_dvd_gcd_mul_left_right (m n k : ℕ) : (gcd m n | gcd m (k * n)) :=
dvd_gcd !gcd_dvd_left (dvd.trans !gcd_dvd_right !dvd_mul_left)
theorem gcd_dvd_gcd_mul_right_right (m n k : ℕ) : gcd m n | gcd m (n * k) :=
theorem gcd_dvd_gcd_mul_right_right (m n k : ℕ) : (gcd m n | gcd m (n * k)) :=
!mul.comm ▸ !gcd_dvd_gcd_mul_left_right
/- lcm -/
@ -661,17 +661,17 @@ calc
... = m * m div m : gcd_self
... = m : H
theorem dvd_lcm_left (m n : ℕ) : m | lcm m n :=
theorem dvd_lcm_left (m n : ℕ) : (m | lcm m n) :=
have H : lcm m n = m * (n div gcd m n), from mul_div_assoc _ !gcd_dvd_right,
dvd.intro H⁻¹
theorem dvd_lcm_right (m n : ℕ) : n | lcm m n :=
theorem dvd_lcm_right (m n : ℕ) : (n | lcm m n) :=
!lcm.comm ▸ !dvd_lcm_left
theorem gcd_mul_lcm (m n : ℕ) : gcd m n * lcm m n = m * n :=
eq.symm (eq_mul_of_div_eq (dvd.trans !gcd_dvd_left !dvd_mul_right) rfl)
theorem lcm_dvd {m n k : ℕ} (H1 : m | k) (H2 : n | k) : lcm m n | k :=
theorem lcm_dvd {m n k : ℕ} (H1 : (m | k)) (H2 : (n | k)) : (lcm m n | k) :=
or.elim (eq_zero_or_pos k)
(assume kzero : k = 0, !kzero⁻¹ ▸ !dvd_zero)
(assume kpos : k > 0,
@ -728,16 +728,16 @@ definition coprime [reducible] (m n : ℕ) : Prop := gcd m n = 1
theorem coprime_swap {m n : ℕ} (H : coprime n m) : coprime m n :=
!gcd.comm ▸ H
theorem dvd_of_coprime_of_dvd_mul_right {m n k : ℕ} (H1 : coprime k n) (H2 : k | m * n) : k | m :=
theorem dvd_of_coprime_of_dvd_mul_right {m n k : ℕ} (H1 : coprime k n) (H2 : (k | m * n)) : (k | m) :=
have H3 : gcd (m * k) (m * n) = m, from
calc
gcd (m * k) (m * n) = m * gcd k n : gcd_mul_left
... = m * 1 : H1
... = m : mul_one,
have H4 : k | gcd (m * k) (m * n), from dvd_gcd !dvd_mul_left H2,
have H4 : (k | gcd (m * k) (m * n)), from dvd_gcd !dvd_mul_left H2,
H3 ▸ H4
theorem dvd_of_coprime_of_dvd_mul_left {m n k : ℕ} (H1 : coprime k m) (H2 : k | m * n) : k | n :=
theorem dvd_of_coprime_of_dvd_mul_left {m n k : ℕ} (H1 : coprime k m) (H2 : (k | m * n)) : (k | n) :=
dvd_of_coprime_of_dvd_mul_right H1 (!mul.comm ▸ H2)
theorem gcd_mul_left_cancel_of_coprime {k : ℕ} (m : ℕ) {n : ℕ} (H : coprime k n) :
@ -788,7 +788,7 @@ theorem coprime_mul_right {k m n : ℕ} (H1 : coprime k m) (H2 : coprime k n) :
coprime_swap (coprime_mul (coprime_swap H1) (coprime_swap H2))
theorem coprime_of_coprime_mul_left {k m n : ℕ} (H : coprime (k * m) n) : coprime m n :=
have H1 : gcd m n | gcd (k * m) n, from !gcd_dvd_gcd_mul_left,
have H1 : (gcd m n | gcd (k * m) n), from !gcd_dvd_gcd_mul_left,
eq_one_of_dvd_one (H ▸ H1)
theorem coprime_of_coprime_mul_right {k m n : ℕ} (H : coprime (m * k) n) : coprime m n :=
@ -800,27 +800,27 @@ coprime_swap (coprime_of_coprime_mul_left (coprime_swap H))
theorem coprime_of_coprime_mul_right_right {k m n : ℕ} (H : coprime m (n * k)) : coprime m n :=
coprime_of_coprime_mul_left_right (!mul.comm ▸ H)
theorem exists_eq_prod_and_dvd_and_dvd {m n k} (H : k | m * n) :
∃ m' n', k = m' * n' ∧ m' | m ∧ n' | n :=
theorem exists_eq_prod_and_dvd_and_dvd {m n k} (H : (k | m * n)) :
∃ m' n', k = m' * n' ∧ (m' | m) ∧ (n' | n) :=
or.elim (eq_zero_or_pos (gcd k m))
(assume H1 : gcd k m = 0,
have H2 : k = 0, from eq_zero_of_gcd_eq_zero_left H1,
have H3 : m = 0, from eq_zero_of_gcd_eq_zero_right H1,
have H4 : k = 0 * n, from H2 ⬝ !zero_mul⁻¹,
have H5 : 0 | m, from H3⁻¹ ▸ !dvd.refl,
have H6 : n | n, from !dvd.refl,
have H5 : (0 | m), from H3⁻¹ ▸ !dvd.refl,
have H6 : (n | n), from !dvd.refl,
exists.intro _ (exists.intro _ (and.intro H4 (and.intro H5 H6))))
(assume H1 : gcd k m > 0,
have H2 : gcd k m | k, from !gcd_dvd_left,
have H3 : k div gcd k m | (m * n) div gcd k m, from div_dvd_div H2 H,
have H2 : (gcd k m | k), from !gcd_dvd_left,
have H3 : (k div gcd k m | (m * n) div gcd k m), from div_dvd_div H2 H,
have H4 : (m * n) div gcd k m = (m div gcd k m) * n, from
calc
m * n div gcd k m = n * m div gcd k m : mul.comm
... = n * (m div gcd k m) : !mul_div_assoc !gcd_dvd_right
... = m div gcd k m * n : mul.comm,
have H5 : k div gcd k m | (m div gcd k m) * n, from H4 ▸ H3,
have H5 : (k div gcd k m | (m div gcd k m) * n), from H4 ▸ H3,
have H6 : coprime (k div gcd k m) (m div gcd k m), from coprime_div_gcd_div_gcd H1,
have H7 : k div gcd k m | n, from dvd_of_coprime_of_dvd_mul_left H6 H5,
have H7 : (k div gcd k m | n), from dvd_of_coprime_of_dvd_mul_left H6 H5,
have H8 : k = gcd k m * (k div gcd k m), from (mul_div_cancel' H2)⁻¹,
exists.intro _ (exists.intro _ (and.intro H8 (and.intro !gcd_dvd_right H7))))

4
library/data/nat/order.lean
View file

@ -411,7 +411,7 @@ ne.symm (ne_of_lt H)
theorem exists_eq_succ_of_pos {n : ℕ} (H : n > 0) : exists l, n = succ l :=
exists_eq_succ_of_lt H
theorem pos_of_dvd_of_pos {m n : ℕ} (H1 : m | n) (H2 : n > 0) : m > 0 :=
theorem pos_of_dvd_of_pos {m n : ℕ} (H1 : (m | n)) (H2 : n > 0) : m > 0 :=
pos_of_ne_zero
(assume H3 : m = 0,
have H4 : n = 0, from eq_zero_of_zero_dvd (H3 ▸ H1),
@ -470,7 +470,7 @@ eq_of_mul_eq_mul_right Hpos (H ⬝ !one_mul⁻¹)
theorem eq_one_of_mul_eq_self_right {n m : ℕ} (Hpos : m > 0) (H : m * n = m) : n = 1 :=
eq_one_of_mul_eq_self_left Hpos (!mul.comm ▸ H)
theorem eq_one_of_dvd_one {n : ℕ} (H : n | 1) : n = 1 :=
theorem eq_one_of_dvd_one {n : ℕ} (H : (n | 1)) : n = 1 :=
dvd.elim H
(take m,
assume H1 : 1 = n * m,

3
library/init/reserved_notation.lean
View file

@ -89,8 +89,7 @@ reserve infixl `∪`:65
/- other symbols -/
precedence `|`:55
reserve notation | a:55 |
reserve notation `(` a `|` b `)`
reserve infixl `++`:65
reserve infixr `::`:65

5
tests/lean/fold.lean
View file

@ -1,5 +1,6 @@
import data.prod data.num
prelude
definition Prop := Type.{0} inductive true : Prop := intro : true inductive false : Prop constant num : Type
inductive prod (A B : Type) := mk : A → B → prod A B infixl `×`:30 := prod
variables a b c : num
context

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

@ -1,7 +1,7 @@
import data.nat
open nat eq.ops
theorem lcm_dvd {m n k : nat} (H1 : m | k) (H2 : n | k) : lcm m n | k :=
theorem lcm_dvd {m n k : nat} (H1 : (m | k)) (H2 : (n | k)) : (lcm m n | k) :=
match eq_zero_or_pos k with
@or.inl _ _ kzero :=
begin