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

feat(library/algebra/ordered_ring,library/data/int/): add sign and theorems about abs, make int an instance, port theorems

Browse source
This commit is contained in:
Jeremy Avigad 2015-01-21 15:50:42 -05:00 committed by Leonardo de Moura
parent 58057c5d99
commit 44642a4285
6 changed files with 265 additions and 19 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
library/algebra/order.lean
View file

@ -333,6 +333,22 @@ section
(assume H : ¬ a ≤ b,
(inr (assume H1 : a = b, H (H1 ▸ !le.refl))))
-- testing equality first may result in more definitional equalities
definition lt.cases {B : Type} (a b : A) (t_lt t_eq t_gt : B) : B :=
if a = b then t_eq else (if a < b then t_lt else t_gt)
theorem lt.cases_of_eq {B : Type} {a b : A} {t_lt t_eq t_gt : B} (H : a = b) :
lt.cases a b t_lt t_eq t_gt = t_eq := if_pos H
theorem lt.cases_of_lt {B : Type} {a b : A} {t_lt t_eq t_gt : B} (H : a < b) :
lt.cases a b t_lt t_eq t_gt = t_lt :=
if_neg (ne_of_lt H) ⬝ if_pos H
theorem lt.cases_of_gt {B : Type} {a b : A} {t_lt t_eq t_gt : B} (H : a > b) :
lt.cases a b t_lt t_eq t_gt = t_gt :=
if_neg (ne.symm (ne_of_lt H)) ⬝ if_neg (lt.asymm H)
/-
definition lt.by_cases' {a b : A} {P : Type}
(H1 : a < b → P) (H2 : a = b → P) (H3 : b < a → P) : P :=
if H4 : a < b then H1 H4 else
@ -355,6 +371,7 @@ section
have H5 [visible] : ¬ a < b, from lt.asymm H4,
have H6 [visible] : a ≠ b, from (assume H7: a = b, lt.irrefl b (H7 ▸ H4)),
dif_neg H6 ▸ dif_neg H5
-/
end
end algebra

7
library/algebra/ordered_group.lean
View file

@ -464,7 +464,7 @@ section
theorem abs_pos_of_ne_zero (H : a ≠ 0) : |a| > 0 :=
or.elim (lt_or_gt_of_ne H) abs_pos_of_neg abs_pos_of_pos
theorem abs_sub : |a - b| = |b - a| :=
theorem abs_sub (a b : A) : |a - b| = |b - a| :=
calc
|a - b| = |-(b - a)| : neg_sub
... = |b - a| : abs_neg
@ -481,7 +481,7 @@ section
abs.by_cases H1 H2
-- the triangle inequality
theorem abs_add_le_abs_add_abs : |a + b| ≤ |a| + |b| :=
theorem abs_add_le_abs_add_abs (a b : A) : |a + b| ≤ |a| + |b| :=
have aux1 : ∀{a b}, a + b ≥ 0 → a ≥ 0 → |a + b| ≤ |a| + |b|,
proof
take a b,
@ -535,14 +535,13 @@ section
... = |a| + |b| : abs_neg)
qed
theorem abs_sub_abs_le_abs_sub : |a| - |b| ≤ |a - b| :=
theorem abs_sub_abs_le_abs_sub (a b : A) : |a| - |b| ≤ |a - b| :=
have H1 : |a| - |b| + |b| ≤ |a - b| + |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,
algebra.le_of_add_le_add_right H1
end
end algebra

186
library/algebra/ordered_ring.lean
View file

@ -233,13 +233,16 @@ lt.by_cases
lt.by_cases
(assume Hb : 0 < b, absurd (H ▸ show 0 < a * b, from mul_pos Ha Hb) (lt.irrefl 0))
(assume Hb : 0 = b, or.inr (Hb⁻¹))
(assume Hb : 0 > b, absurd (H ▸ show 0 > a * b, from mul_neg_of_pos_of_neg Ha Hb) (lt.irrefl 0)))
(assume Hb : 0 > b,
absurd (H ▸ show 0 > a * b, from mul_neg_of_pos_of_neg Ha Hb) (lt.irrefl 0)))
(assume Ha : 0 = a, or.inl (Ha⁻¹))
(assume Ha : 0 > a,
lt.by_cases
(assume Hb : 0 < b, absurd (H ▸ show 0 > a * b, from mul_neg_of_neg_of_pos Ha Hb) (lt.irrefl 0))
(assume Hb : 0 < b,
absurd (H ▸ show 0 > a * b, from mul_neg_of_neg_of_pos Ha Hb) (lt.irrefl 0))
(assume Hb : 0 = b, or.inr (Hb⁻¹))
(assume Hb : 0 > b, absurd (H ▸ show 0 < a * b, from mul_pos_of_neg_of_neg Ha Hb) (lt.irrefl 0)))
(assume Hb : 0 > b,
absurd (H ▸ show 0 < a * b, from mul_pos_of_neg_of_neg Ha Hb) (lt.irrefl 0)))
-- Linearity implies no zero divisors. Doesn't need commutativity.
definition linear_ordered_comm_ring.to_integral_domain [instance] [coercion]
@ -282,15 +285,178 @@ section
(assume Hb : b < 0, or.inr (and.intro Ha Hb)))
end
/-
Still left to do:
/- TODO: Isabelle's library has all kinds of cancelation rules for the simplifier.
Search on mult_le_cancel_right1 in Rings.thy. -/
Isabelle's library has all kinds of cancelation rules for the simplifier, search on
mult_le_cancel_right1 in Rings.thy.
structure decidable_linear_ordered_comm_ring [class] (A : Type) extends linear_ordered_comm_ring A,
decidable_linear_ordered_comm_group A
Properties of abs, sgn, and dvd.
section
variable [s : decidable_linear_ordered_comm_ring A]
variables {a b c : A}
include s
Multiplication and one, starting with mult_right_le_one_le.
-/
definition sign (a : A) : A := lt.cases a 0 (-1) 0 1
theorem sign_of_neg (H : a < 0) : sign a = -1 := lt.cases_of_lt H
theorem sign_zero : sign 0 = 0 := lt.cases_of_eq rfl
theorem sign_of_pos (H : a > 0) : sign a = 1 := lt.cases_of_gt H
theorem sign_one : sign 1 = 1 := sign_of_pos zero_lt_one
theorem sign_neg_one : sign (-1) = -1 := sign_of_neg (neg_neg_of_pos zero_lt_one)
theorem sign_sign (a : A) : sign (sign a) = sign a :=
lt.by_cases
(assume H : a > 0,
calc
sign (sign a) = sign 1 : {sign_of_pos H}
... = 1 : sign_one
... = sign a : sign_of_pos H)
(assume H : 0 = a,
calc
sign (sign a) = sign (sign 0) : H
... = sign 0 : sign_zero
... = sign a : H)
(assume H : a < 0,
calc
sign (sign a) = sign (-1) : {sign_of_neg H}
... = -1 : sign_neg_one
... = sign a : sign_of_neg H)
theorem pos_of_sign_eq_one (H : sign a = 1) : a > 0 :=
lt.by_cases
(assume H1 : 0 < a, H1)
(assume H1 : 0 = a, absurd (sign_zero⁻¹ ⬝ (H1⁻¹ ▸ H)) zero_ne_one)
(assume H1 : 0 > a,
have H2 : -1 = 1, from (sign_of_neg H1)⁻¹ ⬝ H,
absurd ((eq_zero_of_neg_eq H2)⁻¹) zero_ne_one)
theorem eq_zero_of_sign_eq_zero (H : sign a = 0) : a = 0 :=
lt.by_cases
(assume H1 : 0 < a, absurd (H⁻¹ ⬝ sign_of_pos H1) zero_ne_one)
(assume H1 : 0 = a, H1⁻¹)
(assume H1 : 0 > a,
have H2 : 0 = -1, from H⁻¹ ⬝ sign_of_neg H1,
have H3 : 1 = 0, from eq_neg_of_eq_neg H2 ⬝ neg_zero,
absurd (H3⁻¹) zero_ne_one)
theorem neg_of_sign_eq_neg_one (H : sign a = -1) : a < 0 :=
lt.by_cases
(assume H1 : 0 < a,
have H2 : -1 = 1, from H⁻¹ ⬝ (sign_of_pos H1),
absurd ((eq_zero_of_neg_eq H2)⁻¹) zero_ne_one)
(assume H1 : 0 = a,
have H2 : 0 = -1, from (H1 ▸ sign_zero)⁻¹ ⬝ H,
have H3 : 1 = 0, from eq_neg_of_eq_neg H2 ⬝ neg_zero,
absurd (H3⁻¹) zero_ne_one)
(assume H1 : 0 > a, H1)
theorem sign_neg (a : A) : sign (-a) = -(sign a) :=
lt.by_cases
(assume H1 : 0 < a,
calc
sign (-a) = -1 : sign_of_neg (neg_neg_of_pos H1)
... = -(sign a) : {(sign_of_pos H1)⁻¹})
(assume H1 : 0 = a,
calc
sign (-a) = sign (-0) : H1
... = sign 0 : {neg_zero} -- TODO: why do we need {}?
... = 0 : sign_zero
... = -0 : neg_zero
... = -(sign 0) : sign_zero
... = -(sign a) : H1)
(assume H1 : 0 > a,
calc
sign (-a) = 1 : sign_of_pos (neg_pos_of_neg H1)
... = -(-1) : neg_neg
... = -(sign a) : {(sign_of_neg H1)⁻¹})
-- 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 :=
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)⁻¹})
(assume H1 : 0 = a,
calc
|a| = |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
... = -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| :=
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)⁻¹})
(assume H1 : 0 = a,
calc
a = 0 : H1
... = 0 * |a| : zero_mul
... = sign 0 * |a| : sign_zero
... = sign a * |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)⁻¹})
theorem abs_dvd_iff_dvd (a b : A) : |a| | b ↔ a | b :=
abs.by_cases !iff.refl !neg_dvd_iff_dvd
theorem dvd_abs_iff (a b : A) : a | |b| ↔ a | b :=
abs.by_cases !iff.refl !dvd_neg_iff_dvd
theorem abs_mul (a b : A) : |a * b| = |a| * |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)⁻¹})
(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)⁻¹}))
(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)⁻¹})
(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)⁻¹}))
theorem abs_mul_self (a : A) : |a| * |a| = a * a :=
abs.by_cases rfl !neg_mul_neg
end
/- TODO: Multiplication and one, starting with mult_right_le_one_le. -/
end algebra

11
library/algebra/ring.lean
View file

@ -183,13 +183,13 @@ section
... = 0 : zero_mul)
theorem neg_mul_eq_mul_neg : -(a * b) = a * -b :=
neg_eq_of_add_eq_zero
neg_eq_of_add_eq_zero
(calc
a * b + a * -b = a * (b + -b) : left_distrib
... = a * 0 : add.right_inv
... = 0 : mul_zero)
theorem neg_mul_neg_eq : -a * -b = a * b :=
theorem neg_mul_neg : -a * -b = a * b :=
calc
-a * -b = -(a * -b) : !neg_mul_eq_neg_mul⁻¹
... = - -(a * b) : neg_mul_eq_mul_neg
@ -197,6 +197,11 @@ section
theorem neg_mul_comm : -a * b = a * -b := !neg_mul_eq_neg_mul⁻¹ ⬝ !neg_mul_eq_mul_neg
theorem neg_eq_neg_one_mul : -a = -1 * a :=
calc
-a = -(1 * a) : one_mul a ▸ rfl
... = -1 * a : neg_mul_eq_neg_mul
theorem mul_sub_left_distrib : a * (b - c) = a * b - a * c :=
calc
a * (b - c) = a * b + a * -c : left_distrib
@ -270,7 +275,7 @@ section
(take c, assume H' : a * c = b,
dvd.intro
(calc
-a * -c = a * c : neg_mul_neg_eq
-a * -c = a * c : neg_mul_neg
... = b : H')))
theorem dvd_sub (H₁ : a | b) (H₂ : a | c) : a | (b - c) :=

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

@ -426,7 +426,7 @@ theorem padd_pneg (p : ℕ × ℕ) : padd p (pneg p) ≡ (0, 0) :=
show pr1 p + pr2 p + 0 = pr2 p + pr1 p + 0, from !nat.add.comm ▸ rfl
theorem padd_padd_pneg (p q : ℕ × ℕ) : padd (padd p q) (pneg q) ≡ p :=
show pr1 p + pr1 q + pr2 q + pr2 p = pr2 p + pr2 q + pr1 q + pr1 p, by simp
show pr1 p + pr1 q + pr2 q + pr2 p = pr2 p + pr2 q + pr1 q + pr1 p, from by simp
theorem add.left_inv (a : ℤ) : -a + a = 0 :=
have H : repr (-a + a) ≡ repr 0, from
@ -718,8 +718,9 @@ section port_algebra
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
theorem neg_mul_eq_mul_neg : ∀a b : ℤ, -(a * b) = a * -b := algebra.neg_mul_eq_mul_neg
theorem neg_mul_neg_eq : ∀a b : ℤ, -a * -b = a * b := algebra.neg_mul_neg_eq
theorem neg_mul_neg : ∀a b : ℤ, -a * -b = a * b := algebra.neg_mul_neg
theorem neg_mul_comm : ∀a b : ℤ, -a * b = a * -b := algebra.neg_mul_comm
theorem neg_eq_neg_one_mul : ∀a : ℤ, -a = -1 * a := algebra.neg_eq_neg_one_mul
theorem mul_sub_left_distrib : ∀a b c : ℤ, a * (b - c) = a * b - a * c :=
algebra.mul_sub_left_distrib
theorem mul_sub_right_distrib : ∀a b c : ℤ, (a - b) * c = a * c - b * c :=

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

@ -219,6 +219,13 @@ section
add.comm mul mul.assoc (of_num 1) one_mul mul_one mul.left_distrib mul.right_distrib
zero_ne_one le le.refl @le.trans @le.antisymm lt lt_iff_le_and_ne @add_le_add_left
@mul_nonneg @mul_pos le_iff_lt_or_eq le.total mul.comm
protected definition decidable_linear_ordered_comm_ring [instance] :
algebra.decidable_linear_ordered_comm_ring int :=
⦃algebra.decidable_linear_ordered_comm_ring,
int.linear_ordered_comm_ring,
decidable_lt := decidable_lt⦄
end
/- instantiate ordered ring theorems to int -/
@ -414,6 +421,36 @@ section port_algebra
theorem sub_lt_sub_of_lt_of_le : ∀{a b c d : ℤ}, a < b → c ≤ d → a - d < b - c :=
@algebra.sub_lt_sub_of_lt_of_le _ _
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|) :=
@algebra.abs.by_cases _ _
theorem abs_le_of_le_of_neg_le : ∀{a b : ℤ}, a ≤ b → -a ≤ b → |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 :=
@algebra.abs_lt_of_lt_of_neg_lt _ _
theorem abs_add_le_abs_add_abs : ∀a b : ℤ, |a + b| ≤ |a| + |b| :=
algebra.abs_add_le_abs_add_abs
theorem abs_sub_abs_le_abs_sub : ∀a b : ℤ, |a| - |b| ≤ |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 :=
@algebra.mul_le_mul_of_nonneg_left _ _
theorem mul_le_mul_of_nonneg_right : ∀{a b c : ℤ}, a ≤ b → 0 ≤ c → a * c ≤ b * c :=
@ -465,6 +502,27 @@ section port_algebra
theorem zero_lt_one : #int 0 < 1 := trivial
theorem pos_and_pos_or_neg_and_neg_of_mul_pos : ∀{a b : ℤ}, a * b > 0 →
(a > 0 ∧ b > 0) ∨ (a < 0 ∧ b < 0) := @algebra.pos_and_pos_or_neg_and_neg_of_mul_pos _ _
definition sign : ∀a : ℤ, ℤ := algebra.sign
theorem sign_of_neg : ∀{a : ℤ}, a < 0 → sign a = -1 := @algebra.sign_of_neg _ _
theorem sign_zero : sign 0 = 0 := algebra.sign_zero
theorem sign_of_pos : ∀{a : ℤ}, a > 0 → sign a = 1 := @algebra.sign_of_pos _ _
theorem sign_one : sign 1 = 1 := algebra.sign_one
theorem sign_neg_one : sign (-1) = -1 := algebra.sign_neg_one
theorem sign_sign : ∀a : ℤ, sign (sign a) = sign a := algebra.sign_sign
theorem pos_of_sign_eq_one : ∀{a : ℤ}, sign a = 1 → a > 0 := @algebra.pos_of_sign_eq_one _ _
theorem eq_zero_of_sign_eq_zero : ∀{a : ℤ}, sign a = 0 → a = 0 :=
@algebra.eq_zero_of_sign_eq_zero _ _
theorem neg_of_sign_eq_neg_one : ∀{a : ℤ}, sign a = -1 → a < 0 :=
@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
end port_algebra
/- more facts specific to int -/