feat(library/algebra):refactor field and ordered_field more appropriately
This commit is contained in:
Rob Lewis
Leonardo de Moura
parent
b79f600fbc
commit
abcc56a2a7
4 changed files with 299 additions and 149 deletions
|
|
@ -21,7 +21,7 @@ variable {A : Type}
|
|||
structure division_ring [class] (A : Type) extends ring A, has_inv A, zero_ne_one_class A :=
|
||||
(mul_inv_cancel : ∀{a}, a ≠ zero → mul a (inv a) = one)
|
||||
(inv_mul_cancel : ∀{a}, a ≠ zero → mul (inv a) a = one)
|
||||
(inv_zero : inv zero = zero)
|
||||
--(inv_zero : inv zero = zero)
|
||||
|
||||
section division_ring
|
||||
variables [s : division_ring A] {a b c : A}
|
||||
|
|
@ -41,18 +41,20 @@ section division_ring
|
|||
|
||||
theorem inv_eq_one_div : a⁻¹ = 1 / a := !one_mul⁻¹
|
||||
|
||||
theorem inv_zero : 0⁻¹ = 0 := !division_ring.inv_zero
|
||||
-- the following are only theorems if we assume inv_zero here
|
||||
/- theorem inv_zero : 0⁻¹ = 0 := !division_ring.inv_zero
|
||||
|
||||
theorem one_div_zero : 1 / 0 = 0 :=
|
||||
calc
|
||||
1 / 0 = 1 * 0⁻¹ : refl
|
||||
... = 1 * 0 : division_ring.inv_zero A
|
||||
... = 0 : mul_zero
|
||||
-/
|
||||
|
||||
theorem div_eq_mul_one_div : a / b = a * (1 / b) :=
|
||||
by rewrite [↑divide, one_mul]
|
||||
|
||||
theorem div_zero : a / 0 = 0 := by rewrite [div_eq_mul_one_div, one_div_zero, mul_zero]
|
||||
-- theorem div_zero : a / 0 = 0 := by rewrite [div_eq_mul_one_div, one_div_zero, mul_zero]
|
||||
|
||||
theorem mul_one_div_cancel (H : a ≠ 0) : a * (1 / a) = 1 :=
|
||||
by rewrite [-inv_eq_one_div, (mul_inv_cancel H)]
|
||||
|
|
@ -71,8 +73,8 @@ section division_ring
|
|||
have C1 : 0 = 1, from symm (by rewrite [-(mul_one_div_cancel H), H2, mul_zero]),
|
||||
absurd C1 zero_ne_one
|
||||
|
||||
theorem ne_zero_of_one_div_ne_zero (H : 1 / a ≠ 0) : a ≠ 0 :=
|
||||
assume Ha : a = 0, absurd (Ha⁻¹ ▸ one_div_zero) H
|
||||
-- theorem ne_zero_of_one_div_ne_zero (H : 1 / a ≠ 0) : a ≠ 0 :=
|
||||
-- assume Ha : a = 0, absurd (Ha⁻¹ ▸ one_div_zero) H
|
||||
|
||||
-- the analogue in group is called inv_one
|
||||
theorem inv_one_is_one : 1⁻¹ = 1 :=
|
||||
|
|
@ -89,24 +91,10 @@ section division_ring
|
|||
have C1 : a = 0, by rewrite [-mul_one, -(mul_one_div_cancel Hb), -mul.assoc, H, zero_mul],
|
||||
absurd C1 Ha
|
||||
|
||||
-- this belongs in ring?
|
||||
theorem mul_ne_zero_imp_ne_zero (H : a * b ≠ 0) : a ≠ 0 ∧ b ≠ 0 :=
|
||||
have Ha : a ≠ 0, from
|
||||
(assume Ha1 : a = 0,
|
||||
have H1 : a * b = 0, by rewrite [Ha1, zero_mul],
|
||||
absurd H1 H),
|
||||
have Hb : b ≠ 0, from
|
||||
(assume Hb1 : b = 0,
|
||||
have H1 : a * b = 0, by rewrite [Hb1, mul_zero],
|
||||
absurd H1 H),
|
||||
and.intro Ha Hb
|
||||
|
||||
theorem mul_ne_zero_comm (H : a * b ≠ 0) : b * a ≠ 0 :=
|
||||
have H2 : a ≠ 0 ∧ b ≠ 0, from mul_ne_zero_imp_ne_zero H,
|
||||
mul_ne_zero' (and.right H2) (and.left H2)
|
||||
|
||||
-- theorem inv_zero_imp_zero (H : a⁻¹ = 0) : a = 0 :=
|
||||
-- classical?
|
||||
|
||||
-- make "left" and "right" versions?
|
||||
theorem eq_one_div_of_mul_eq_one (H : a * b = 1) : b = 1 / a :=
|
||||
|
|
@ -137,7 +125,6 @@ section division_ring
|
|||
... = b * 1 : mul_one_div_cancel H2
|
||||
... = b : mul_one)
|
||||
|
||||
-- with 1 / 0 = 0, this should be provable without Ha and Hb. Needs decidable =?
|
||||
theorem one_div_mul_one_div (Ha : a ≠ 0) (Hb : b ≠ 0) : (1 / a) * (1 / b) = 1 / (b * a) :=
|
||||
have H : (b * a) * ((1 / a) * (1 / b)) = 1, by
|
||||
rewrite [mul.assoc, -(mul.assoc a), (mul_one_div_cancel Ha), one_mul, (mul_one_div_cancel Hb)],
|
||||
|
|
@ -147,15 +134,6 @@ section division_ring
|
|||
have H : (-1) * (-1) = 1, by rewrite [-neg_eq_neg_one_mul, neg_neg],
|
||||
symm (eq_one_div_of_mul_eq_one H)
|
||||
|
||||
-- this should be in ring
|
||||
theorem mul_neg_one_eq_neg : a * (-1) = -a :=
|
||||
have H : a + a * -1 = 0, from calc
|
||||
a + a * -1 = a * 1 + a * -1 : mul_one
|
||||
... = a * (1 + -1) : left_distrib
|
||||
... = a * 0 : add.right_inv
|
||||
... = 0 : mul_zero,
|
||||
symm (neg_eq_of_add_eq_zero H)
|
||||
|
||||
theorem one_div_neg_eq_neg_one_div (H : a ≠ 0) : 1 / (- a) = - (1 / a) :=
|
||||
have H1 : -1 ≠ 0, from
|
||||
(assume H2 : -1 = 0, absurd (symm (calc
|
||||
|
|
@ -175,7 +153,6 @@ section division_ring
|
|||
... = -(b * (1 / a)) : neg_mul_eq_mul_neg
|
||||
... = - (b * a⁻¹) : inv_eq_one_div
|
||||
|
||||
-- can lose Ha
|
||||
theorem neg_div (Ha : a ≠ 0) : (-b) / a = - (b / a) :=
|
||||
by rewrite [neg_eq_neg_one_mul, mul_div_assoc, -neg_eq_neg_one_mul]
|
||||
|
||||
|
|
@ -235,7 +212,7 @@ section division_ring
|
|||
have H : (a + b / c) * c = a * c + b, by rewrite [right_distrib, (div_mul_cancel Hc)],
|
||||
(iff.elim_right (eq_div_iff_mul_eq Hc)) H
|
||||
|
||||
theorem mul_mul_div (Hc : c ≠ 0) : a = a * c * (1 / c) :=
|
||||
theorem mul_mul_div (Hc : c ≠ 0) : a = a * c * (1 / c) :=
|
||||
calc
|
||||
a = a * 1 : mul_one
|
||||
... = a * (c * (1 / c)) : mul_one_div_cancel Hc
|
||||
|
|
@ -333,13 +310,18 @@ section field
|
|||
end field
|
||||
|
||||
structure discrete_field [class] (A : Type) extends field A :=
|
||||
(decidable_equality : ∀x y : A, decidable (x = y))
|
||||
(decidable_equality : ∀x y : A, decidable (x = y))
|
||||
(inv_zero : inv zero = zero)
|
||||
|
||||
section discrete_field
|
||||
variable [s : discrete_field A]
|
||||
include s
|
||||
variables {a b c d : A}
|
||||
|
||||
-- many of the theorems in discrete_field are the same as theorems in field or division ring,
|
||||
-- but with fewer hypotheses since 0⁻¹ = 0 and equality is decidable.
|
||||
-- they are named with '. Is there a better convention?
|
||||
|
||||
-- name clash with order
|
||||
definition decidable_eq' [instance] (a b : A) : decidable (a = b) :=
|
||||
@discrete_field.decidable_equality A s a b
|
||||
|
|
@ -356,6 +338,19 @@ section discrete_field
|
|||
⦃ integral_domain, s,
|
||||
eq_zero_or_eq_zero_of_mul_eq_zero := discrete_field.eq_zero_or_eq_zero_of_mul_eq_zero⦄
|
||||
|
||||
theorem inv_zero : 0⁻¹ = 0 := !discrete_field.inv_zero
|
||||
|
||||
theorem one_div_zero : 1 / 0 = 0 :=
|
||||
calc
|
||||
1 / 0 = 1 * 0⁻¹ : refl
|
||||
... = 1 * 0 : discrete_field.inv_zero A
|
||||
... = 0 : mul_zero
|
||||
|
||||
theorem div_zero : a / 0 = 0 := by rewrite [div_eq_mul_one_div, one_div_zero, mul_zero]
|
||||
|
||||
theorem ne_zero_of_one_div_ne_zero (H : 1 / a ≠ 0) : a ≠ 0 :=
|
||||
assume Ha : a = 0, absurd (Ha⁻¹ ▸ one_div_zero) H
|
||||
|
||||
theorem inv_zero_imp_zero (H : 1 / a = 0) : a = 0 :=
|
||||
decidable.by_cases
|
||||
(assume Ha, Ha)
|
||||
|
|
@ -374,17 +369,17 @@ section discrete_field
|
|||
|
||||
theorem one_div_neg_eq_neg_one_div' : 1 / (- a) = - (1 / a) :=
|
||||
decidable.by_cases
|
||||
(assume Ha : a = 0, by rewrite [Ha, neg_zero, div_zero, -neg_zero, -(@div_zero A s 1)])
|
||||
(assume Ha : a = 0, by rewrite [Ha, neg_zero, 2 div_zero, neg_zero])
|
||||
(assume Ha : a ≠ 0, one_div_neg_eq_neg_one_div Ha)
|
||||
|
||||
theorem neg_div' : (-b) / a = - (b / a) :=
|
||||
decidable.by_cases
|
||||
(assume Ha : a = 0, by rewrite [Ha, div_zero, -neg_zero, -(@div_zero A s b)])
|
||||
(assume Ha : a = 0, by rewrite [Ha, 2 div_zero, neg_zero])
|
||||
(assume Ha : a ≠ 0, neg_div Ha)
|
||||
|
||||
theorem neg_div_neg_eq_div' : (-a) / (-b) = a / b :=
|
||||
decidable.by_cases
|
||||
(assume Hb : b = 0, by rewrite [Hb, neg_zero, div_zero, -(@div_zero A s a)])
|
||||
(assume Hb : b = 0, by rewrite [Hb, neg_zero, 2 div_zero])
|
||||
(assume Hb : b ≠ 0, neg_div_neg_eq_div Hb)
|
||||
|
||||
theorem div_div' : 1 / (1 / a) = a :=
|
||||
|
|
@ -403,10 +398,10 @@ section discrete_field
|
|||
|
||||
theorem mul_inv' : (b * a)⁻¹ = a⁻¹ * b⁻¹ :=
|
||||
decidable.by_cases
|
||||
(assume Ha : a = 0, by rewrite [Ha, mul_zero, inv_zero, -(zero_mul b⁻¹), -inv_zero])
|
||||
(assume Ha : a = 0, by rewrite [Ha, mul_zero, 2 inv_zero, zero_mul])
|
||||
(assume Ha : a ≠ 0,
|
||||
decidable.by_cases
|
||||
(assume Hb : b = 0, by rewrite [Hb, zero_mul, inv_zero, -(mul_zero a⁻¹), -inv_zero])
|
||||
(assume Hb : b = 0, by rewrite [Hb, zero_mul, 2 inv_zero, mul_zero])
|
||||
(assume Hb : b ≠ 0, mul_inv Ha Hb))
|
||||
|
||||
-- the following are specifically for fields
|
||||
|
|
@ -415,7 +410,7 @@ section discrete_field
|
|||
|
||||
theorem div_mul_right' (Ha : a ≠ 0) : a / (a * b) = 1 / b :=
|
||||
decidable.by_cases
|
||||
(assume Hb : b = 0, by rewrite [Hb, mul_zero, div_zero, -(@div_zero A s 1)])
|
||||
(assume Hb : b = 0, by rewrite [Hb, mul_zero, 2 div_zero])
|
||||
(assume Hb : b ≠ 0, div_mul_right Hb (mul_ne_zero Ha Hb))
|
||||
|
||||
theorem div_mul_left' (Hb : b ≠ 0) : b / (a * b) = 1 / a :=
|
||||
|
|
@ -431,7 +426,7 @@ section discrete_field
|
|||
|
||||
theorem mul_div_mul_left' (Hc : c ≠ 0) : (c * a) / (c * b) = a / b :=
|
||||
decidable.by_cases
|
||||
(assume Hb : b = 0, by rewrite [Hb, mul_zero, div_zero, -(@div_zero A s a)])
|
||||
(assume Hb : b = 0, by rewrite [Hb, mul_zero, 2 div_zero])
|
||||
(assume Hb : b ≠ 0, mul_div_mul_left Hb Hc)
|
||||
|
||||
theorem mul_div_mul_right' (Hc : c ≠ 0) : (a * c) / (b * c) = a / b :=
|
||||
|
|
@ -445,10 +440,10 @@ section discrete_field
|
|||
|
||||
theorem one_div_div' : 1 / (a / b) = b / a :=
|
||||
decidable.by_cases
|
||||
(assume Ha : a = 0, by rewrite [Ha, zero_div, div_zero, -(@div_zero A s b)])
|
||||
(assume Ha : a = 0, by rewrite [Ha, zero_div, 2 div_zero])
|
||||
(assume Ha : a ≠ 0,
|
||||
decidable.by_cases
|
||||
(assume Hb : b = 0, by rewrite [Hb, 2 div_zero, -(@zero_div A s a)])
|
||||
(assume Hb : b = 0, by rewrite [Hb, 2 div_zero, zero_div])
|
||||
(assume Hb : b ≠ 0, one_div_div Ha Hb))
|
||||
|
||||
theorem div_div_eq_mul_div' : a / (b / c) = (a * c) / b :=
|
||||
|
|
|
|||
|
|
@ -17,20 +17,9 @@ structure linear_ordered_field [class] (A : Type) extends linear_ordered_ring A,
|
|||
section linear_ordered_field
|
||||
|
||||
variable {A : Type}
|
||||
variables [s : linear_ordered_field A] {a b c : A}
|
||||
variables [s : linear_ordered_field A] {a b c d : A}
|
||||
include s
|
||||
|
||||
-- ordered ring theorem?
|
||||
-- split H3 into its own lemma
|
||||
theorem gt_of_mul_lt_mul_neg_left (H : c * a < c * b) (Hc : c ≤ 0) : a > b :=
|
||||
have nhc : -c ≥ 0, from neg_nonneg_of_nonpos Hc,
|
||||
have H2 : -(c * b) < -(c * a), from iff.mp' (neg_lt_neg_iff_lt _ _) H,
|
||||
have H3 : (-c) * b < (-c) * a, from calc
|
||||
(-c) * b = - (c * b) : neg_mul_eq_neg_mul
|
||||
... < -(c * a) : H2
|
||||
... = (-c) * a : neg_mul_eq_neg_mul,
|
||||
lt_of_mul_lt_mul_left H3 nhc
|
||||
|
||||
-- helpers for following
|
||||
theorem mul_zero_lt_mul_inv_of_pos (H : 0 < a) : a * 0 < a * (1 / a) :=
|
||||
calc
|
||||
|
|
@ -48,24 +37,10 @@ section linear_ordered_field
|
|||
|
||||
theorem div_pos_of_pos (H : 0 < a) : 0 < 1 / a :=
|
||||
lt_of_mul_lt_mul_left (mul_zero_lt_mul_inv_of_pos H) (le_of_lt H)
|
||||
|
||||
theorem pos_of_div_pos (H : 0 < 1 / a) : 0 < a :=
|
||||
have H1 : 0 < 1 / (1 / a), from div_pos_of_pos H,
|
||||
have H2 : 1 / a ≠ 0, from
|
||||
(assume H3 : 1 / a = 0,
|
||||
have H4 : 1 / (1 / a) = 0, from H3⁻¹ ▸ div_zero,
|
||||
absurd H4 (ne.symm (ne_of_lt H1))),
|
||||
(div_div (ne_zero_of_one_div_ne_zero H2)) ▸ H1
|
||||
|
||||
|
||||
theorem div_neg_of_neg (H : a < 0) : 1 / a < 0 :=
|
||||
gt_of_mul_lt_mul_neg_left (mul_zero_lt_mul_inv_of_neg H) (le_of_lt H)
|
||||
|
||||
theorem neg_of_div_neg (H : 1 / a < 0) : a < 0 :=
|
||||
have H1 : 0 < - (1 / a), from neg_pos_of_neg H,
|
||||
have Ha : a ≠ 0, from ne_zero_of_one_div_ne_zero (ne_of_lt H),
|
||||
have H2 : 0 < 1 / (-a), from (one_div_neg_eq_neg_one_div Ha)⁻¹ ▸ H1,
|
||||
have H3 : 0 < -a, from pos_of_div_pos H2,
|
||||
neg_of_neg_pos H3
|
||||
|
||||
theorem le_mul_of_ge_one_right (Hb : b ≥ 0) (H : a ≥ 1) : b ≤ b * a :=
|
||||
mul_one _ ▸ (mul_le_mul_of_nonneg_left H Hb)
|
||||
|
|
@ -113,74 +88,6 @@ section linear_ordered_field
|
|||
theorem one_lt_div_of_lt (Hb : b > 0) (H : b < a) : 1 < a / b :=
|
||||
(iff.mp' (one_lt_div_iff_lt Hb)) H
|
||||
|
||||
-- why is mul_le_mul under ordered_ring namespace?
|
||||
theorem le_of_div_le (H : 0 < a) (Hl : 1 / a ≤ 1 / b) : b ≤ a :=
|
||||
have Hb : 0 < b, from pos_of_div_pos (calc
|
||||
0 < 1 / a : div_pos_of_pos H
|
||||
... ≤ 1 / b : Hl),
|
||||
have H' : 1 ≤ a / b, from (calc
|
||||
1 = a / a : div_self (ne.symm (ne_of_lt H))
|
||||
... = a * (1 / a) : div_eq_mul_one_div
|
||||
... ≤ a * (1 / b) : ordered_ring.mul_le_mul_of_nonneg_left Hl (le_of_lt H)
|
||||
... = a / b : div_eq_mul_one_div
|
||||
), le_of_one_le_div Hb H'
|
||||
|
||||
|
||||
theorem lt_of_div_lt (H : 0 < a) (Hl : 1 / a < 1 / b) : b < a :=
|
||||
have Hb : 0 < b, from pos_of_div_pos (calc
|
||||
0 < 1 / a : div_pos_of_pos H
|
||||
... < 1 / b : Hl),
|
||||
have H : 1 < a / b, from (calc
|
||||
1 = a / a : div_self (ne.symm (ne_of_lt H))
|
||||
... = a * (1 / a) : div_eq_mul_one_div
|
||||
... < a * (1 / b) : mul_lt_mul_of_pos_left Hl H
|
||||
... = a / b : div_eq_mul_one_div),
|
||||
lt_of_one_lt_div Hb H
|
||||
|
||||
theorem le_of_div_le_neg (H : b < 0) (Hl : 1 / a ≤ 1 / b) : b ≤ a :=
|
||||
have Ha : a ≠ 0, from ne_of_lt (neg_of_div_neg (calc
|
||||
1 / a ≤ 1 / b : Hl
|
||||
... < 0 : div_neg_of_neg H)),
|
||||
have H' : -b > 0, from neg_pos_of_neg H,
|
||||
have Hl' : - (1 / b) ≤ - (1 / a), from neg_le_neg Hl,
|
||||
have Hl'' : 1 / - b ≤ 1 / - a, from calc
|
||||
1 / -b = - (1 / b) : one_div_neg_eq_neg_one_div (ne_of_lt H)
|
||||
... ≤ - (1 / a) : Hl'
|
||||
... = 1 / -a : one_div_neg_eq_neg_one_div Ha,
|
||||
le_of_neg_le_neg (le_of_div_le H' Hl'')
|
||||
|
||||
theorem lt_of_div_lt_neg (H : b < 0) (Hl : 1 / a < 1 / b) : b < a :=
|
||||
have H1 : b ≤ a, from le_of_div_le_neg H (le_of_lt Hl),
|
||||
have Hn : b ≠ a, from
|
||||
(assume Hn' : b = a,
|
||||
have Hl' : 1 / a = 1 / b, from Hn' ▸ refl _,
|
||||
absurd Hl' (ne_of_lt Hl)),
|
||||
lt_of_le_of_ne H1 Hn
|
||||
|
||||
theorem div_lt_div_of_lt (Ha : 0 < a) (H : a < b) : 1 / b < 1 / a :=
|
||||
lt_of_not_le
|
||||
(assume H',
|
||||
absurd H (not_lt_of_le (le_of_div_le Ha H')))
|
||||
|
||||
theorem div_le_div_of_le (Ha : 0 < a) (H : a ≤ b) : 1 / b ≤ 1 / a :=
|
||||
le_of_not_lt
|
||||
(assume H',
|
||||
absurd H (not_le_of_lt (lt_of_div_lt Ha H')))
|
||||
|
||||
theorem div_lt_div_of_lt_neg (Hb : b < 0) (H : a < b) : 1 / b < 1 / a :=
|
||||
lt_of_not_le
|
||||
(assume H',
|
||||
absurd H (not_lt_of_le (le_of_div_le_neg Hb H')))
|
||||
|
||||
theorem div_le_div_of_le_neg (Hb : b < 0) (H : a ≤ b) : 1 / b ≤ 1 / a :=
|
||||
le_of_not_lt
|
||||
(assume H',
|
||||
absurd H (not_le_of_lt (lt_of_div_lt_neg Hb H')))
|
||||
|
||||
-- belongs in ordered ring?
|
||||
theorem zero_gt_neg_one : -1 < 0 :=
|
||||
neg_zero ▸ (neg_lt_neg zero_lt_one)
|
||||
|
||||
theorem exists_lt : ∃ x, x < a :=
|
||||
have H : a - 1 < a, from add_lt_of_le_of_neg (le.refl _) zero_gt_neg_one,
|
||||
exists.intro _ H
|
||||
|
|
@ -189,18 +96,6 @@ section linear_ordered_field
|
|||
have H : a + 1 > a, from lt_add_of_le_of_pos (le.refl _) zero_lt_one,
|
||||
exists.intro _ H
|
||||
|
||||
theorem one_lt_div (H1 : 0 < a) (H2 : a < 1) : 1 < 1 / a :=
|
||||
one_div_one ▸ div_lt_div_of_lt H1 H2
|
||||
|
||||
theorem one_le_div (H1 : 0 < a) (H2 : a ≤ 1) : 1 ≤ 1 / a :=
|
||||
one_div_one ▸ div_le_div_of_le H1 H2
|
||||
|
||||
theorem neg_one_lt_div_neg (H1 : a < 0) (H2 : -1 < a) : 1 / a < -1 :=
|
||||
one_div_neg_one_eq_neg_one ▸ div_lt_div_of_lt_neg H1 H2
|
||||
|
||||
theorem neg_one_le_div_neg (H1 : a < 0) (H2 : -1 ≤ a) : 1 / a ≤ -1 :=
|
||||
one_div_neg_one_eq_neg_one ▸ div_le_div_of_le_neg H1 H2
|
||||
|
||||
|
||||
-- the following theorems amount to four iffs, for <, ≤, ≥, >.
|
||||
|
||||
|
|
@ -240,10 +135,132 @@ section linear_ordered_field
|
|||
... > b * (1 / c) : mul_lt_mul_of_neg_right H (div_neg_of_neg Hc)
|
||||
... = b / c : div_eq_mul_one_div
|
||||
|
||||
-- following these in the isabelle file, there are 8 biconditionals for the above with - signs
|
||||
-- skipping for now
|
||||
|
||||
theorem mul_sub_mul_div_mul_neg (Hc : c ≠ 0) (Hd : d ≠ 0) (H : a / c < b / d) :
|
||||
(a * d - b * c) / (c * d) < 0 :=
|
||||
have H1 : a / c - b / d < 0, from calc
|
||||
a / c - b / d < b / d - b / d : sub_lt_sub_right H
|
||||
... = 0 : sub_self,
|
||||
calc
|
||||
0 > a / c - b / d : H1
|
||||
... = (a * d - c * b) / (c * d) : div_sub_div Hc Hd
|
||||
... = (a * d - b * c) / (c * d) : mul.comm
|
||||
|
||||
theorem mul_sub_mul_div_mul_nonpos (Hc : c ≠ 0) (Hd : d ≠ 0) (H : a / c ≤ b / d) :
|
||||
(a * d - b * c) / (c * d) ≤ 0 :=
|
||||
have H1 : a / c - b / d ≤ 0, from calc
|
||||
a / c - b / d ≤ b / d - b / d : sub_le_sub_right H
|
||||
... = 0 : sub_self,
|
||||
calc
|
||||
0 ≥ a / c - b / d : H1
|
||||
... = (a * d - c * b) / (c * d) : div_sub_div Hc Hd
|
||||
... = (a * d - b * c) / (c * d) : mul.comm
|
||||
|
||||
theorem div_lt_div_of_mul_sub_mul_div_neg (Hc : c ≠ 0) (Hd : d ≠ 0)
|
||||
(H : (a * d - b * c) / (c * d) < 0) : a / c < b / d :=
|
||||
have H1 : (a * d - c * b) / (c * d) < 0, from !mul.comm ▸ H,
|
||||
have H2 : a / c - b / d < 0, from (div_sub_div Hc Hd)⁻¹ ▸ H1,
|
||||
have H3 [visible] : a / c - b / d + b / d < 0 + b / d, from add_lt_add_right H2 _,
|
||||
begin rewrite [zero_add at H3, neg_add_cancel_right at H3], exact H3 end
|
||||
|
||||
theorem div_le_div_of_mul_sub_mul_div_nonpos (Hc : c ≠ 0) (Hd : d ≠ 0)
|
||||
(H : (a * d - b * c) / (c * d) ≤ 0) : a / c ≤ b / d :=
|
||||
have H1 : (a * d - c * b) / (c * d) ≤ 0, from !mul.comm ▸ H,
|
||||
have H2 : a / c - b / d ≤ 0, from (div_sub_div Hc Hd)⁻¹ ▸ H1,
|
||||
have H3 [visible] : a / c - b / d + b / d ≤ 0 + b / d, from add_le_add_right H2 _,
|
||||
begin rewrite [zero_add at H3, neg_add_cancel_right at H3], exact H3 end
|
||||
|
||||
theorem pos_div_of_pos_of_pos (Ha : 0 < a) (Hb : 0 < b) : 0 < a / b :=
|
||||
begin
|
||||
rewrite div_eq_mul_one_div,
|
||||
apply mul_pos,
|
||||
exact Ha,
|
||||
apply div_pos_of_pos,
|
||||
exact Hb
|
||||
end
|
||||
|
||||
theorem nonneg_div_of_nonneg_of_pos (Ha : 0 ≤ a) (Hb : 0 < b) : 0 ≤ a / b :=
|
||||
begin
|
||||
rewrite div_eq_mul_one_div,
|
||||
apply mul_nonneg,
|
||||
exact Ha,
|
||||
apply le_of_lt,
|
||||
apply div_pos_of_pos,
|
||||
exact Hb
|
||||
end
|
||||
|
||||
theorem neg_div_of_neg_of_pos (Ha : a < 0) (Hb : 0 < b) : a / b < 0:=
|
||||
begin
|
||||
rewrite div_eq_mul_one_div,
|
||||
apply mul_neg_of_neg_of_pos,
|
||||
exact Ha,
|
||||
apply div_pos_of_pos,
|
||||
exact Hb
|
||||
end
|
||||
|
||||
theorem nonpos_div_of_nonpos_of_pos (Ha : a ≤ 0) (Hb : 0 < b) : a / b ≤ 0 :=
|
||||
begin
|
||||
rewrite div_eq_mul_one_div,
|
||||
apply mul_nonpos_of_nonpos_of_nonneg,
|
||||
exact Ha,
|
||||
apply le_of_lt,
|
||||
apply div_pos_of_pos,
|
||||
exact Hb
|
||||
end
|
||||
|
||||
theorem neg_div_of_pos_of_neg (Ha : 0 < a) (Hb : b < 0) : a / b < 0 :=
|
||||
begin
|
||||
rewrite div_eq_mul_one_div,
|
||||
apply mul_neg_of_pos_of_neg,
|
||||
exact Ha,
|
||||
apply div_neg_of_neg,
|
||||
exact Hb
|
||||
end
|
||||
|
||||
theorem nonpos_div_of_nonneg_of_neg (Ha : 0 ≤ a) (Hb : b < 0) : a / b ≤ 0 :=
|
||||
begin
|
||||
rewrite div_eq_mul_one_div,
|
||||
apply mul_nonpos_of_nonneg_of_nonpos,
|
||||
exact Ha,
|
||||
apply le_of_lt,
|
||||
apply div_neg_of_neg,
|
||||
exact Hb
|
||||
end
|
||||
|
||||
theorem pos_div_of_neg_of_neg (Ha : a < 0) (Hb : b < 0) : 0 < a / b :=
|
||||
begin
|
||||
rewrite div_eq_mul_one_div,
|
||||
apply mul_pos_of_neg_of_neg,
|
||||
exact Ha,
|
||||
apply div_neg_of_neg,
|
||||
exact Hb
|
||||
end
|
||||
|
||||
|
||||
theorem nonneg_div_of_nonpos_of_neg (Ha : a ≤ 0) (Hb : b < 0) : 0 ≤ a / b :=
|
||||
begin
|
||||
rewrite div_eq_mul_one_div,
|
||||
apply mul_nonneg_of_nonpos_of_nonpos,
|
||||
exact Ha,
|
||||
apply le_of_lt,
|
||||
apply div_neg_of_neg,
|
||||
exact Hb
|
||||
end
|
||||
|
||||
theorem div_lt_div_of_lt_of_pos (H : a < b) (Hc : 0 < c) : a / c < b / c :=
|
||||
div_eq_mul_one_div⁻¹ ▸ div_eq_mul_one_div⁻¹ ▸ mul_lt_mul_of_pos_right H (div_pos_of_pos Hc)
|
||||
|
||||
theorem div_lt_div_of_lt_of_neg (H : b < a) (Hc : c < 0) : a / c < b / c :=
|
||||
div_eq_mul_one_div⁻¹ ▸ div_eq_mul_one_div⁻¹ ▸ mul_lt_mul_of_neg_right H (div_neg_of_neg Hc)
|
||||
|
||||
|
||||
end linear_ordered_field
|
||||
|
||||
structure discrete_linear_ordered_field [class] (A : Type) extends linear_ordered_field A,
|
||||
decidable_linear_ordered_comm_ring A
|
||||
decidable_linear_ordered_comm_ring A :=
|
||||
(inv_zero : inv zero = zero)
|
||||
|
||||
section discrete_linear_ordered_field
|
||||
|
||||
|
|
@ -266,7 +283,111 @@ section discrete_linear_ordered_field
|
|||
[s : discrete_linear_ordered_field A] : discrete_field A :=
|
||||
⦃ discrete_field, s, decidable_equality := dec_eq_of_dec_lt⦄
|
||||
|
||||
theorem pos_of_div_pos (H : 0 < 1 / a) : 0 < a :=
|
||||
have H1 : 0 < 1 / (1 / a), from div_pos_of_pos H,
|
||||
have H2 : 1 / a ≠ 0, from
|
||||
(assume H3 : 1 / a = 0,
|
||||
have H4 : 1 / (1 / a) = 0, from H3⁻¹ ▸ div_zero,
|
||||
absurd H4 (ne.symm (ne_of_lt H1))),
|
||||
(div_div (ne_zero_of_one_div_ne_zero H2)) ▸ H1
|
||||
|
||||
theorem neg_of_div_neg (H : 1 / a < 0) : a < 0 :=
|
||||
have H1 : 0 < - (1 / a), from neg_pos_of_neg H,
|
||||
have Ha : a ≠ 0, from ne_zero_of_one_div_ne_zero (ne_of_lt H),
|
||||
have H2 : 0 < 1 / (-a), from (one_div_neg_eq_neg_one_div Ha)⁻¹ ▸ H1,
|
||||
have H3 : 0 < -a, from pos_of_div_pos H2,
|
||||
neg_of_neg_pos H3
|
||||
|
||||
-- why is mul_le_mul under ordered_ring namespace?
|
||||
theorem le_of_div_le (H : 0 < a) (Hl : 1 / a ≤ 1 / b) : b ≤ a :=
|
||||
have Hb : 0 < b, from pos_of_div_pos (calc
|
||||
0 < 1 / a : div_pos_of_pos H
|
||||
... ≤ 1 / b : Hl),
|
||||
have H' : 1 ≤ a / b, from (calc
|
||||
1 = a / a : div_self (ne.symm (ne_of_lt H))
|
||||
... = a * (1 / a) : div_eq_mul_one_div
|
||||
... ≤ a * (1 / b) : ordered_ring.mul_le_mul_of_nonneg_left Hl (le_of_lt H)
|
||||
... = a / b : div_eq_mul_one_div
|
||||
), le_of_one_le_div Hb H'
|
||||
|
||||
|
||||
theorem le_of_div_le_neg (H : b < 0) (Hl : 1 / a ≤ 1 / b) : b ≤ a :=
|
||||
have Ha : a ≠ 0, from ne_of_lt (neg_of_div_neg (calc
|
||||
1 / a ≤ 1 / b : Hl
|
||||
... < 0 : div_neg_of_neg H)),
|
||||
have H' : -b > 0, from neg_pos_of_neg H,
|
||||
have Hl' : - (1 / b) ≤ - (1 / a), from neg_le_neg Hl,
|
||||
have Hl'' : 1 / - b ≤ 1 / - a, from calc
|
||||
1 / -b = - (1 / b) : one_div_neg_eq_neg_one_div (ne_of_lt H)
|
||||
... ≤ - (1 / a) : Hl'
|
||||
... = 1 / -a : one_div_neg_eq_neg_one_div Ha,
|
||||
le_of_neg_le_neg (le_of_div_le H' Hl'')
|
||||
|
||||
theorem lt_of_div_lt (H : 0 < a) (Hl : 1 / a < 1 / b) : b < a :=
|
||||
have Hb : 0 < b, from pos_of_div_pos (calc
|
||||
0 < 1 / a : div_pos_of_pos H
|
||||
... < 1 / b : Hl),
|
||||
have H : 1 < a / b, from (calc
|
||||
1 = a / a : div_self (ne.symm (ne_of_lt H))
|
||||
... = a * (1 / a) : div_eq_mul_one_div
|
||||
... < a * (1 / b) : mul_lt_mul_of_pos_left Hl H
|
||||
... = a / b : div_eq_mul_one_div),
|
||||
lt_of_one_lt_div Hb H
|
||||
|
||||
|
||||
theorem lt_of_div_lt_neg (H : b < 0) (Hl : 1 / a < 1 / b) : b < a :=
|
||||
have H1 : b ≤ a, from le_of_div_le_neg H (le_of_lt Hl),
|
||||
have Hn : b ≠ a, from
|
||||
(assume Hn' : b = a,
|
||||
have Hl' : 1 / a = 1 / b, from Hn' ▸ refl _,
|
||||
absurd Hl' (ne_of_lt Hl)),
|
||||
lt_of_le_of_ne H1 Hn
|
||||
|
||||
|
||||
theorem div_lt_div_of_lt (Ha : 0 < a) (H : a < b) : 1 / b < 1 / a :=
|
||||
lt_of_not_le
|
||||
(assume H',
|
||||
absurd H (not_lt_of_le (le_of_div_le Ha H')))
|
||||
|
||||
theorem div_le_div_of_le (Ha : 0 < a) (H : a ≤ b) : 1 / b ≤ 1 / a :=
|
||||
le_of_not_lt
|
||||
(assume H',
|
||||
absurd H (not_le_of_lt (lt_of_div_lt Ha H')))
|
||||
|
||||
theorem div_lt_div_of_lt_neg (Hb : b < 0) (H : a < b) : 1 / b < 1 / a :=
|
||||
lt_of_not_le
|
||||
(assume H',
|
||||
absurd H (not_lt_of_le (le_of_div_le_neg Hb H')))
|
||||
|
||||
theorem div_le_div_of_le_neg (Hb : b < 0) (H : a ≤ b) : 1 / b ≤ 1 / a :=
|
||||
le_of_not_lt
|
||||
(assume H',
|
||||
absurd H (not_le_of_lt (lt_of_div_lt_neg Hb H')))
|
||||
|
||||
|
||||
theorem one_lt_div (H1 : 0 < a) (H2 : a < 1) : 1 < 1 / a :=
|
||||
one_div_one ▸ div_lt_div_of_lt H1 H2
|
||||
|
||||
theorem one_le_div (H1 : 0 < a) (H2 : a ≤ 1) : 1 ≤ 1 / a :=
|
||||
one_div_one ▸ div_le_div_of_le H1 H2
|
||||
|
||||
theorem neg_one_lt_div_neg (H1 : a < 0) (H2 : -1 < a) : 1 / a < -1 :=
|
||||
one_div_neg_one_eq_neg_one ▸ div_lt_div_of_lt_neg H1 H2
|
||||
|
||||
theorem neg_one_le_div_neg (H1 : a < 0) (H2 : -1 ≤ a) : 1 / a ≤ -1 :=
|
||||
one_div_neg_one_eq_neg_one ▸ div_le_div_of_le_neg H1 H2
|
||||
|
||||
theorem div_lt_div_of_pos_of_lt_of_pos (Hb : 0 < b) (H : b < a) (Hc : 0 < c) : c / a < c / b :=
|
||||
begin
|
||||
apply (iff.mp (sub_neg_iff_lt _ _)),
|
||||
rewrite [div_eq_mul_one_div, {c / b}div_eq_mul_one_div],
|
||||
rewrite -mul_sub_left_distrib,
|
||||
apply mul_neg_of_pos_of_neg,
|
||||
exact Hc,
|
||||
apply (iff.mp' (sub_neg_iff_lt _ _)),
|
||||
apply div_lt_div_of_lt,
|
||||
exact Hb, exact H
|
||||
end
|
||||
|
||||
end discrete_linear_ordered_field
|
||||
end algebra
|
||||
|
|
|
|||
|
|
@ -100,6 +100,7 @@ section
|
|||
rewrite zero_mul at H,
|
||||
exact H
|
||||
end
|
||||
|
||||
end
|
||||
|
||||
structure linear_ordered_semiring [class] (A : Type)
|
||||
|
|
@ -258,6 +259,7 @@ section
|
|||
rewrite zero_mul at H,
|
||||
exact H
|
||||
end
|
||||
|
||||
end
|
||||
|
||||
-- TODO: we can eliminate mul_pos_of_pos, but now it is not worth the effort to redeclare the
|
||||
|
|
@ -366,6 +368,19 @@ section
|
|||
apply (absurd_a_lt_a Hab)
|
||||
end)
|
||||
(assume Hb : b < 0, or.inr (and.intro Ha Hb)))
|
||||
|
||||
theorem gt_of_mul_lt_mul_neg_left {a b c} (H : c * a < c * b) (Hc : c ≤ 0) : a > b :=
|
||||
have nhc : -c ≥ 0, from neg_nonneg_of_nonpos Hc,
|
||||
have H2 : -(c * b) < -(c * a), from iff.mp' (neg_lt_neg_iff_lt _ _) H,
|
||||
have H3 : (-c) * b < (-c) * a, from calc
|
||||
(-c) * b = - (c * b) : neg_mul_eq_neg_mul
|
||||
... < -(c * a) : H2
|
||||
... = (-c) * a : neg_mul_eq_neg_mul,
|
||||
lt_of_mul_lt_mul_left H3 nhc
|
||||
|
||||
theorem zero_gt_neg_one : -1 < 0 :=
|
||||
neg_zero ▸ (neg_lt_neg zero_lt_one)
|
||||
|
||||
end
|
||||
|
||||
/- TODO: Isabelle's library has all kinds of cancelation rules for the simplifier.
|
||||
|
|
|
|||
|
|
@ -220,6 +220,25 @@ section
|
|||
... ↔ a * e + c - b * e = d : iff.symm !sub_eq_iff_eq_add
|
||||
... ↔ a * e - b * e + c = d : by rewrite sub_add_eq_add_sub
|
||||
... ↔ (a - b) * e + c = d : by rewrite mul_sub_right_distrib
|
||||
|
||||
theorem mul_neg_one_eq_neg : a * (-1) = -a :=
|
||||
have H : a + a * -1 = 0, from calc
|
||||
a + a * -1 = a * 1 + a * -1 : mul_one
|
||||
... = a * (1 + -1) : left_distrib
|
||||
... = a * 0 : add.right_inv
|
||||
... = 0 : mul_zero,
|
||||
symm (neg_eq_of_add_eq_zero H)
|
||||
|
||||
theorem mul_ne_zero_imp_ne_zero {a b} (H : a * b ≠ 0) : a ≠ 0 ∧ b ≠ 0 :=
|
||||
have Ha : a ≠ 0, from
|
||||
(assume Ha1 : a = 0,
|
||||
have H1 : a * b = 0, by rewrite [Ha1, zero_mul],
|
||||
absurd H1 H),
|
||||
have Hb : b ≠ 0, from
|
||||
(assume Hb1 : b = 0,
|
||||
have H1 : a * b = 0, by rewrite [Hb1, mul_zero],
|
||||
absurd H1 H),
|
||||
and.intro Ha Hb
|
||||
end
|
||||
|
||||
structure comm_ring [class] (A : Type) extends ring A, comm_semigroup A
|
||||
|
|
|
|||
Loading…
Reference in a new issue