diff --git a/library/algebra/order.lean b/library/algebra/order.lean index e0527a270..dd15625d9 100644 --- a/library/algebra/order.lean +++ b/library/algebra/order.lean @@ -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 diff --git a/library/algebra/ordered_group.lean b/library/algebra/ordered_group.lean index 199060d3e..f3a0d45ff 100644 --- a/library/algebra/ordered_group.lean +++ b/library/algebra/ordered_group.lean @@ -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 diff --git a/library/algebra/ordered_ring.lean b/library/algebra/ordered_ring.lean index 58ce031a7..cd620bf02 100644 --- a/library/algebra/ordered_ring.lean +++ b/library/algebra/ordered_ring.lean @@ -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 diff --git a/library/algebra/ring.lean b/library/algebra/ring.lean index 32d15fa86..947c68220 100644 --- a/library/algebra/ring.lean +++ b/library/algebra/ring.lean @@ -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) := diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean index 8fc890397..392ee518b 100644 --- a/library/data/int/basic.lean +++ b/library/data/int/basic.lean @@ -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 := diff --git a/library/data/int/order.lean b/library/data/int/order.lean index 37899d657..abe08e05f 100644 --- a/library/data/int/order.lean +++ b/library/data/int/order.lean @@ -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 -/