feat/refactor(library/*): various additions and improvements
This commit is contained in:
Jeremy Avigad
parent
cdecc309b3
commit
ffa648a090
7 changed files with 99 additions and 47 deletions
|
|
@ -11,7 +11,7 @@ of "linear_ordered_comm_ring". This development is modeled after Isabelle's libr
|
|||
import algebra.ordered_group algebra.ring
|
||||
open eq eq.ops
|
||||
|
||||
namespace algebra
|
||||
namespace algebra
|
||||
|
||||
variable {A : Type}
|
||||
|
||||
|
|
@ -349,7 +349,7 @@ section
|
|||
(assume H : a ≤ 0, mul_nonneg_of_nonpos_of_nonpos H H)
|
||||
|
||||
theorem zero_le_one : 0 ≤ (1:A) := one_mul 1 ▸ mul_self_nonneg 1
|
||||
theorem zero_lt_one : 0 < (1:A) := linear_ordered_ring.zero_lt_one A
|
||||
theorem zero_lt_one : 0 < (1:A) := linear_ordered_ring.zero_lt_one A
|
||||
|
||||
theorem pos_and_pos_or_neg_and_neg_of_mul_pos {a b : A} (Hab : a * b > 0) :
|
||||
(a > 0 ∧ b > 0) ∨ (a < 0 ∧ b < 0) :=
|
||||
|
|
@ -555,7 +555,7 @@ section
|
|||
... = -1 * abs a : by rewrite neg_eq_neg_one_mul
|
||||
... = sign a * abs a : by rewrite (sign_of_neg H1))
|
||||
|
||||
theorem abs_dvd_iff_dvd (a b : A) : abs a ∣ b ↔ a ∣ b :=
|
||||
theorem abs_dvd_iff (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 ∣ abs b ↔ a ∣ b :=
|
||||
|
|
|
|||
|
|
@ -308,13 +308,13 @@ section
|
|||
assume H : a * b = 0,
|
||||
or.elim (eq_zero_or_eq_zero_of_mul_eq_zero H) (assume H3, H1 H3) (assume H4, H2 H4)
|
||||
|
||||
theorem mul.cancel_right {a b c : A} (Ha : a ≠ 0) (H : b * a = c * a) : b = c :=
|
||||
theorem eq_of_mul_eq_mul_right {a b c : A} (Ha : a ≠ 0) (H : b * a = c * a) : b = c :=
|
||||
have H1 : b * a - c * a = 0, from iff.mp !eq_iff_sub_eq_zero H,
|
||||
have H2 : (b - c) * a = 0, using H1, by rewrite [mul_sub_right_distrib, H1],
|
||||
have H3 : b - c = 0, from or_resolve_left (eq_zero_or_eq_zero_of_mul_eq_zero H2) Ha,
|
||||
iff.elim_right !eq_iff_sub_eq_zero H3
|
||||
|
||||
theorem mul.cancel_left {a b c : A} (Ha : a ≠ 0) (H : a * b = a * c) : b = c :=
|
||||
theorem eq_of_mul_eq_mul_left {a b c : A} (Ha : a ≠ 0) (H : a * b = a * c) : b = c :=
|
||||
have H1 : a * b - a * c = 0, from iff.mp !eq_iff_sub_eq_zero H,
|
||||
have H2 : a * (b - c) = 0, using H1, by rewrite [mul_sub_left_distrib, H1],
|
||||
have H3 : b - c = 0, from or_resolve_right (eq_zero_or_eq_zero_of_mul_eq_zero H2) Ha,
|
||||
|
|
@ -345,7 +345,7 @@ section
|
|||
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⁻¹),
|
||||
have H1 : b * d = c, from eq_of_mul_eq_mul_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) :=
|
||||
|
|
@ -353,7 +353,7 @@ section
|
|||
(take d,
|
||||
assume H : c * a = b * a * d,
|
||||
have H1 : b * d * a = c * a, from by rewrite [mul.right_comm, -H],
|
||||
have H2 : b * d = c, from mul.cancel_right Ha H1,
|
||||
have H2 : b * d = c, from eq_of_mul_eq_mul_right Ha H1,
|
||||
dvd.intro H2)
|
||||
end
|
||||
|
||||
|
|
|
|||
|
|
@ -458,7 +458,7 @@ H⁻¹ ▸ H1⁻¹ ▸ H2⁻¹ ▸ H3
|
|||
|
||||
section
|
||||
local attribute nat_abs [reducible]
|
||||
theorem mul_nat_abs (a b : ℤ) : nat_abs (a * b) = #nat (nat_abs a) * (nat_abs b) :=
|
||||
theorem nat_abs_mul (a b : ℤ) : nat_abs (a * b) = #nat (nat_abs a) * (nat_abs b) :=
|
||||
int.cases_on a
|
||||
(take m,
|
||||
int.cases_on b
|
||||
|
|
@ -592,7 +592,7 @@ show false, from succ_ne_zero 0 ((of_nat.inj H)⁻¹)
|
|||
theorem eq_zero_or_eq_zero_of_mul_eq_zero {a b : ℤ} (H : a * b = 0) : a = 0 ∨ b = 0 :=
|
||||
have H2 : (nat_abs a) * (nat_abs b) = nat.zero, from
|
||||
calc
|
||||
(nat_abs a) * (nat_abs b) = (nat_abs (a * b)) : (mul_nat_abs a b)⁻¹
|
||||
(nat_abs a) * (nat_abs b) = (nat_abs (a * b)) : (nat_abs_mul a b)⁻¹
|
||||
... = (nat_abs 0) : {H}
|
||||
... = nat.zero : nat_abs_of_nat nat.zero,
|
||||
have H3 : (nat_abs a) = nat.zero ∨ (nat_abs b) = nat.zero,
|
||||
|
|
|
|||
|
|
@ -444,6 +444,36 @@ theorem mul_div_cancel_of_mod_eq_zero {a b : ℤ} (H : a mod b = 0) : b * (a div
|
|||
|
||||
/- dvd -/
|
||||
|
||||
theorem dvd_of_of_nat_dvd_of_nat {m n : ℕ} : of_nat m ∣ of_nat n → (#nat m ∣ n) :=
|
||||
nat.by_cases_zero_pos n
|
||||
(assume H, nat.dvd_zero m)
|
||||
(take n',
|
||||
assume H1 : (#nat n' > 0),
|
||||
have H2 : of_nat n' > 0, from of_nat_pos H1,
|
||||
assume H3 : of_nat m ∣ of_nat n',
|
||||
dvd.elim H3
|
||||
(take c,
|
||||
assume H4 : of_nat n' = of_nat m * c,
|
||||
have H5 : c > 0, from pos_of_mul_pos_left (H4 ▸ H2) !of_nat_nonneg,
|
||||
obtain k (H6 : c = of_nat k), from exists_eq_of_nat (le_of_lt H5),
|
||||
have H7 : n' = (#nat m * k), from (!iff.mp !of_nat_eq_of_nat (H6 ▸ H4)),
|
||||
nat.dvd.intro H7⁻¹))
|
||||
|
||||
theorem of_nat_dvd_of_nat_of_dvd {m n : ℕ} (H : #nat m ∣ n) : of_nat m ∣ of_nat n :=
|
||||
nat.dvd.elim H
|
||||
(take k, assume H1 : #nat n = m * k,
|
||||
dvd.intro (!iff.mp' !of_nat_eq_of_nat H1⁻¹))
|
||||
|
||||
theorem of_nat_dvd_of_nat (m n : ℕ) : of_nat m ∣ of_nat n ↔ (#nat m ∣ n) :=
|
||||
iff.intro dvd_of_of_nat_dvd_of_nat of_nat_dvd_of_nat_of_dvd
|
||||
|
||||
theorem dvd.antisymm {a b : ℤ} (H1 : a ≥ 0) (H2 : b ≥ 0) : a ∣ b → b ∣ a → a = b :=
|
||||
begin
|
||||
rewrite [-abs_of_nonneg H1, -abs_of_nonneg H2, -*of_nat_nat_abs],
|
||||
rewrite [*of_nat_dvd_of_nat, *of_nat_eq_of_nat],
|
||||
apply nat.dvd.antisymm
|
||||
end
|
||||
|
||||
theorem dvd_of_mod_eq_zero {a b : ℤ} (H : b mod a = 0) : a ∣ b :=
|
||||
dvd.intro (!mul.comm ▸ div_mul_cancel_of_mod_eq_zero H)
|
||||
|
||||
|
|
@ -469,6 +499,16 @@ decidable.by_cases
|
|||
obtain d (H' : b = d * c), from exists_eq_mul_left_of_dvd H,
|
||||
by rewrite [H', -mul.assoc, *(!mul_div_cancel cnz)])
|
||||
|
||||
theorem div_dvd_div {a b c : ℤ} (H1 : a ∣ b) (H2 : b ∣ c) : b div a ∣ c div a :=
|
||||
have H3 : b = b div a * a, from (div_mul_cancel H1)⁻¹,
|
||||
have H4 : c = c div a * a, from (div_mul_cancel (dvd.trans H1 H2))⁻¹,
|
||||
decidable.by_cases
|
||||
(assume H5 : a = 0,
|
||||
have H6: c div a = 0, from (congr_arg _ H5 ⬝ !div_zero),
|
||||
H6⁻¹ ▸ !dvd_zero)
|
||||
(assume H5 : a ≠ 0,
|
||||
dvd_of_mul_dvd_mul_right H5 (H3 ▸ H4 ▸ H2))
|
||||
|
||||
theorem div_eq_iff_eq_mul_right {a b : ℤ} (c : ℤ) (H : b ≠ 0) (H' : b ∣ a) :
|
||||
a div b = c ↔ a = b * c :=
|
||||
iff.intro
|
||||
|
|
|
|||
|
|
@ -145,10 +145,6 @@ theorem lt.irrefl (a : ℤ) : ¬ a < a :=
|
|||
theorem ne_of_lt {a b : ℤ} (H : a < b) : a ≠ b :=
|
||||
(assume H2 : a = b, absurd (H2 ▸ H) (lt.irrefl b))
|
||||
|
||||
theorem succ_le_of_lt {a b : ℤ} (H : a < b) : a + 1 ≤ b := H
|
||||
|
||||
theorem lt_of_le_succ {a b : ℤ} (H : a + 1 ≤ b) : a < b := H
|
||||
|
||||
theorem le_of_lt {a b : ℤ} (H : a < b) : a ≤ b :=
|
||||
obtain (n : ℕ) (Hn : a + succ n = b), from lt.elim H,
|
||||
le.intro Hn
|
||||
|
|
@ -191,7 +187,7 @@ have H2 : c + a + n = c + b, from
|
|||
le.intro H2
|
||||
|
||||
theorem add_lt_add_left {a b : ℤ} (H : a < b) (c : ℤ) : c + a < c + b :=
|
||||
let H' := le_of_lt H in
|
||||
let H' := le_of_lt H in
|
||||
(iff.mp' (lt_iff_le_and_ne _ _)) (and.intro (add_le_add_left H' _)
|
||||
(take Heq, let Heq' := add_left_cancel Heq in
|
||||
!lt.irrefl (Heq' ▸ H)))
|
||||
|
|
@ -228,8 +224,8 @@ theorem zero_lt_one : (0 : ℤ) < 1 := trivial
|
|||
|
||||
theorem not_le_of_gt {a b : ℤ} (H : a < b) : ¬ b ≤ a :=
|
||||
assume Hba,
|
||||
let Heq := le.antisymm (le_of_lt H) Hba in
|
||||
!lt.irrefl (Heq ▸ H)
|
||||
let Heq := le.antisymm (le_of_lt H) Hba in
|
||||
!lt.irrefl (Heq ▸ H)
|
||||
|
||||
theorem lt_of_lt_of_le {a b c : ℤ} (Hab : a < b) (Hbc : b ≤ c) : a < c :=
|
||||
let Hab' := le_of_lt Hab in
|
||||
|
|
@ -327,6 +323,9 @@ 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)⁻¹)
|
||||
|
||||
theorem nat_abs_abs (a : ℤ) : nat_abs (abs a) = nat_abs a :=
|
||||
abs.by_cases rfl !nat_abs_neg
|
||||
|
||||
theorem lt_of_add_one_le {a b : ℤ} (H : a + 1 ≤ b) : a < b :=
|
||||
obtain n (H1 : a + 1 + n = b), from le.elim H,
|
||||
have H2 : a + succ n = b, by rewrite [-H1, add.assoc, add.comm 1],
|
||||
|
|
@ -364,4 +363,32 @@ int.cases_on a
|
|||
(take m H, absurd (of_nat_nonneg m : 0 ≤ m) (not_le_of_gt H))
|
||||
(take m H, exists.intro m rfl)
|
||||
|
||||
theorem eq_one_of_mul_eq_one_right {a b : ℤ} (H : a ≥ 0) (H' : a * b = 1) : a = 1 :=
|
||||
have H2 : a * b > 0, by rewrite H'; apply trivial,
|
||||
have H3 : b > 0, from pos_of_mul_pos_left H2 H,
|
||||
have H4 : a > 0, from pos_of_mul_pos_right H2 (le_of_lt H3),
|
||||
or.elim (le_or_gt a 1)
|
||||
(assume H5 : a ≤ 1,
|
||||
show a = 1, from le.antisymm H5 (add_one_le_of_lt H4))
|
||||
(assume H5 : a > 1,
|
||||
assert H6 : a * b ≥ 2 * 1,
|
||||
from mul_le_mul (add_one_le_of_lt H5) (add_one_le_of_lt H3) trivial H,
|
||||
have H7 : false, by rewrite [H' at H6]; apply H6,
|
||||
false.elim H7)
|
||||
|
||||
theorem eq_one_of_mul_eq_one_left {a b : ℤ} (H : b ≥ 0) (H' : a * b = 1) : b = 1 :=
|
||||
eq_one_of_mul_eq_one_right H (!mul.comm ▸ H')
|
||||
|
||||
theorem eq_one_of_mul_eq_self_left {a b : ℤ} (Hpos : a ≠ 0) (H : b * a = a) : b = 1 :=
|
||||
eq_of_mul_eq_mul_right Hpos (H ⬝ (one_mul a)⁻¹)
|
||||
|
||||
theorem eq_one_of_mul_eq_self_right {a b : ℤ} (Hpos : b ≠ 0) (H : b * a = b) : a = 1 :=
|
||||
eq_one_of_mul_eq_self_left Hpos (!mul.comm ▸ H)
|
||||
|
||||
theorem eq_one_of_dvd_one {a : ℤ} (H : a ≥ 0) (H' : a ∣ 1) : a = 1 :=
|
||||
dvd.elim H'
|
||||
(take b,
|
||||
assume H1 : 1 = a * b,
|
||||
eq_one_of_mul_eq_one_right H H1⁻¹)
|
||||
|
||||
end int
|
||||
|
|
|
|||
|
|
@ -64,7 +64,7 @@ nat.cases_on n
|
|||
... = gcd (succ n₁) 0 : zero_mod
|
||||
... = (succ n₁) : gcd_zero_right)
|
||||
|
||||
theorem gcd_rec_of_pos (m : ℕ) {n : ℕ} (H : n > 0) : gcd m n = gcd n (m mod n) :=
|
||||
theorem gcd_of_pos (m : ℕ) {n : ℕ} (H : n > 0) : gcd m n = gcd n (m mod n) :=
|
||||
gcd_def m n ⬝ if_neg (ne_zero_of_pos H)
|
||||
|
||||
theorem gcd_rec (m n : ℕ) : gcd m n = gcd n (m mod n) :=
|
||||
|
|
@ -73,7 +73,7 @@ by_cases_zero_pos n
|
|||
gcd m 0 = m : gcd_zero_right
|
||||
... = gcd 0 m : gcd_zero_left
|
||||
... = gcd 0 (m mod 0) : mod_zero)
|
||||
(take n, assume H : 0 < n, gcd_rec_of_pos m H)
|
||||
(take n, assume H : 0 < n, gcd_of_pos m H)
|
||||
|
||||
theorem gcd.induction {P : ℕ → ℕ → Prop}
|
||||
(m n : ℕ)
|
||||
|
|
@ -265,26 +265,15 @@ or.elim (eq_zero_or_pos k)
|
|||
have qpos : q > 0, from pos_of_mul_pos_left (kn ▸ kpos),
|
||||
have H3 : p * q * (m * n * gcd p q) = p * q * (gcd m n * k), from
|
||||
calc
|
||||
p * q * (m * n * gcd p q) = p * (q * (m * n * gcd p q)) : mul.assoc
|
||||
... = p * (q * (m * (n * gcd p q))) : mul.assoc
|
||||
... = p * (m * (q * (n * gcd p q))) : mul.left_comm
|
||||
... = p * m * (q * (n * gcd p q)) : mul.assoc
|
||||
... = p * m * (q * n * gcd p q) : mul.assoc
|
||||
... = m * p * (q * n * gcd p q) : mul.comm
|
||||
... = k * (q * n * gcd p q) : km
|
||||
... = k * (n * q * gcd p q) : mul.comm
|
||||
... = k * (k * gcd p q) : kn
|
||||
... = k * gcd (k * p) (k * q) : gcd_mul_left
|
||||
... = k * gcd (n * q * p) (k * q) : kn
|
||||
... = k * gcd (n * q * p) (m * p * q) : km
|
||||
... = k * gcd (n * (q * p)) (m * p * q) : mul.assoc
|
||||
... = k * gcd (n * (q * p)) (m * (p * q)) : mul.assoc
|
||||
... = k * gcd (n * (p * q)) (m * (p * q)) : mul.comm
|
||||
... = k * (gcd n m * (p * q)) : gcd_mul_right
|
||||
... = gcd n m * (p * q) * k : mul.comm
|
||||
... = p * q * gcd n m * k : mul.comm
|
||||
... = p * q * (gcd n m * k) : mul.assoc
|
||||
... = p * q * (gcd m n * k) : gcd.comm,
|
||||
p * q * (m * n * gcd p q)
|
||||
= m * p * (n * q * gcd p q) : by rewrite [*mul.assoc, *mul.left_comm q,
|
||||
mul.left_comm p]
|
||||
... = k * (k * gcd p q) : by rewrite [-kn, -km]
|
||||
... = k * gcd (k * p) (k * q) : by rewrite gcd_mul_left
|
||||
... = k * gcd (n * q * p) (m * p * q) : by rewrite [-kn, -km]
|
||||
... = k * (gcd n m * (p * q)) : by rewrite [*mul.assoc, mul.comm q, gcd_mul_right]
|
||||
... = p * q * (gcd m n * k) : by rewrite [mul.comm, mul.comm (gcd n m), gcd.comm,
|
||||
*mul.assoc],
|
||||
have H4 : m * n * gcd p q = gcd m n * k,
|
||||
from !eq_of_mul_eq_mul_left (mul_pos ppos qpos) H3,
|
||||
have H5 : gcd m n * (lcm m n * gcd p q) = gcd m n * k,
|
||||
|
|
@ -293,7 +282,7 @@ or.elim (eq_zero_or_pos k)
|
|||
from !eq_of_mul_eq_mul_left gcd_pos H5,
|
||||
dvd.intro H6)
|
||||
|
||||
theorem lcm_assoc (m n k : ℕ) : lcm (lcm m n) k = lcm m (lcm n k) :=
|
||||
theorem lcm.assoc (m n k : ℕ) : lcm (lcm m n) k = lcm m (lcm n k) :=
|
||||
dvd.antisymm
|
||||
(lcm_dvd
|
||||
(lcm_dvd !dvd_lcm_left (dvd.trans !dvd_lcm_left !dvd_lcm_right))
|
||||
|
|
@ -325,13 +314,9 @@ theorem gcd_mul_left_cancel_of_coprime {k : ℕ} (m : ℕ) {n : ℕ} (H : coprim
|
|||
gcd (k * m) n = gcd m n :=
|
||||
have H1 : coprime (gcd (k * m) n) k, from
|
||||
calc
|
||||
gcd (gcd (k * m) n) k = gcd k (gcd (k * m) n) : gcd.comm
|
||||
... = gcd (gcd k (k * m)) n : gcd.assoc
|
||||
... = gcd (gcd (k * 1) (k * m)) n : mul_one
|
||||
... = gcd (k * gcd 1 m) n : gcd_mul_left
|
||||
... = gcd (k * 1) n : gcd_one_left
|
||||
... = gcd k n : mul_one
|
||||
... = 1 : H,
|
||||
gcd (gcd (k * m) n) k
|
||||
= gcd (k * gcd 1 m) n : by rewrite [-gcd_mul_left, mul_one, gcd.comm, gcd.assoc]
|
||||
... = 1 : by rewrite [gcd_one_left, mul_one, ↑coprime at H, H],
|
||||
dvd.antisymm
|
||||
(dvd_gcd (dvd_of_coprime_of_dvd_mul_left H1 !gcd_dvd_left) !gcd_dvd_right)
|
||||
(dvd_gcd (dvd.trans !gcd_dvd_left !dvd_mul_left) !gcd_dvd_right)
|
||||
|
|
|
|||
|
|
@ -64,7 +64,7 @@ decidable.by_cases
|
|||
... = (num b * denom b) * (num c * denom a) :
|
||||
by rewrite [*mul.assoc, *mul.left_comm (denom a),
|
||||
*mul.left_comm (denom b), mul.comm (denom a)],
|
||||
mul.cancel_left H3 H4)
|
||||
eq_of_mul_eq_mul_left H3 H4)
|
||||
|
||||
theorem equiv.is_equivalence : equivalence equiv :=
|
||||
mk_equivalence equiv equiv.refl @equiv.symm @equiv.trans
|
||||
|
|
|
|||
Loading…
Reference in a new issue