From b94d0a948d27d975959548d75c7673c776e8a2a2 Mon Sep 17 00:00:00 2001 From: Rob Lewis Date: Tue, 16 Jun 2015 16:55:06 +1000 Subject: [PATCH] chore(library/data/real): replace theorems with more general versions from algebra --- library/algebra/ordered_group_2.lean | 561 --------------------------- library/data/pnat.lean | 20 + library/data/real/basic.lean | 104 ++--- library/data/real/complete.lean | 3 +- 4 files changed, 54 insertions(+), 634 deletions(-) delete mode 100644 library/algebra/ordered_group_2.lean diff --git a/library/algebra/ordered_group_2.lean b/library/algebra/ordered_group_2.lean deleted file mode 100644 index 63a50a745..000000000 --- a/library/algebra/ordered_group_2.lean +++ /dev/null @@ -1,561 +0,0 @@ -/- -Copyright (c) 2014 Jeremy Avigad. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Jeremy Avigad - -Partially ordered additive groups, modeled on Isabelle's library. We could refine the structures, -but we would have to declare more inheritance paths. --/ - -import logic.eq data.unit data.sigma data.prod -import algebra.function algebra.binary -import algebra.group algebra.order -open eq eq.ops -- note: ⁻¹ will be overloaded - -namespace algebra - -variable {A : Type} - -/- partially ordered monoids, such as the natural numbers -/ - -structure ordered_cancel_comm_monoid [class] (A : Type) extends add_comm_monoid A, - add_left_cancel_semigroup A, add_right_cancel_semigroup A, order_pair A := -(add_le_add_left : ∀a b, le a b → ∀c, le (add c a) (add c b)) -(le_of_add_le_add_left : ∀a b c, le (add a b) (add a c) → le b c) - -section - variables [s : ordered_cancel_comm_monoid A] - variables {a b c d e : A} - include s - - theorem add_le_add_left (H : a ≤ b) (c : A) : c + a ≤ c + b := - !ordered_cancel_comm_monoid.add_le_add_left H c - - theorem add_le_add_right (H : a ≤ b) (c : A) : a + c ≤ b + c := - (add.comm c a) ▸ (add.comm c b) ▸ (add_le_add_left H c) - - theorem add_le_add (Hab : a ≤ b) (Hcd : c ≤ d) : a + c ≤ b + d := - le.trans (add_le_add_right Hab c) (add_le_add_left Hcd b) - - theorem add_lt_add_left (H : a < b) (c : A) : c + a < c + b := - have H1 : c + a ≤ c + b, from add_le_add_left (le_of_lt H) c, - have H2 : c + a ≠ c + b, from - take H3 : c + a = c + b, - have H4 : a = b, from add.left_cancel H3, - ne_of_lt H H4, - sorry--lt_of_le_of_ne H1 H2 - - theorem add_lt_add_right (H : a < b) (c : A) : a + c < b + c := - begin - rewrite [add.comm, {b + _}add.comm], - exact (add_lt_add_left H c) - end - - theorem le_add_of_nonneg_right (H : b ≥ 0) : a ≤ a + b := - begin - have H1 : a + b ≥ a + 0, from add_le_add_left H a, - rewrite add_zero at H1, - exact H1 - end - - theorem le_add_of_nonneg_left (H : b ≥ 0) : a ≤ b + a := - begin - have H1 : 0 + a ≤ b + a, from add_le_add_right H a, - rewrite zero_add at H1, - exact H1 - end - - theorem add_lt_add (Hab : a < b) (Hcd : c < d) : a + c < b + d := - lt.trans (add_lt_add_right Hab c) (add_lt_add_left Hcd b) - - theorem add_lt_add_of_le_of_lt (Hab : a ≤ b) (Hcd : c < d) : a + c < b + d := - lt_of_le_of_lt (add_le_add_right Hab c) (add_lt_add_left Hcd b) - - theorem add_lt_add_of_lt_of_le (Hab : a < b) (Hcd : c ≤ d) : a + c < b + d := - lt_of_lt_of_le (add_lt_add_right Hab c) (add_le_add_left Hcd b) - - theorem lt_add_of_pos_right (H : b > 0) : a < a + b := !add_zero ▸ add_lt_add_left H a - - theorem lt_add_of_pos_left (H : b > 0) : a < b + a := !zero_add ▸ add_lt_add_right H a - - -- here we start using le_of_add_le_add_left. - theorem le_of_add_le_add_left (H : a + b ≤ a + c) : b ≤ c := - !ordered_cancel_comm_monoid.le_of_add_le_add_left H - - theorem le_of_add_le_add_right (H : a + b ≤ c + b) : a ≤ c := - le_of_add_le_add_left (show b + a ≤ b + c, begin rewrite [add.comm, {b + _}add.comm], exact H end) - - theorem lt_of_add_lt_add_left (H : a + b < a + c) : b < c := - have H1 : b ≤ c, from le_of_add_le_add_left (le_of_lt H), - have H2 : b ≠ c, from - assume H3 : b = c, lt.irrefl _ (H3 ▸ H), - sorry --lt_of_le_of_ne H1 H2 - - theorem lt_of_add_lt_add_right (H : a + b < c + b) : a < c := - lt_of_add_lt_add_left ((add.comm a b) ▸ (add.comm c b) ▸ H) - - theorem add_le_add_left_iff (a b c : A) : a + b ≤ a + c ↔ b ≤ c := - iff.intro le_of_add_le_add_left (assume H, add_le_add_left H _) - - theorem add_le_add_right_iff (a b c : A) : a + b ≤ c + b ↔ a ≤ c := - iff.intro le_of_add_le_add_right (assume H, add_le_add_right H _) - - theorem add_lt_add_left_iff (a b c : A) : a + b < a + c ↔ b < c := - iff.intro lt_of_add_lt_add_left (assume H, add_lt_add_left H _) - - theorem add_lt_add_right_iff (a b c : A) : a + b < c + b ↔ a < c := - iff.intro lt_of_add_lt_add_right (assume H, add_lt_add_right H _) - - -- here we start using properties of zero. - theorem add_nonneg (Ha : 0 ≤ a) (Hb : 0 ≤ b) : 0 ≤ a + b := - !zero_add ▸ (add_le_add Ha Hb) - - theorem add_pos (Ha : 0 < a) (Hb : 0 < b) : 0 < a + b := - !zero_add ▸ (add_lt_add Ha Hb) - - theorem add_pos_of_pos_of_nonneg (Ha : 0 < a) (Hb : 0 ≤ b) : 0 < a + b := - !zero_add ▸ (add_lt_add_of_lt_of_le Ha Hb) - - theorem add_pos_of_nonneg_of_pos (Ha : 0 ≤ a) (Hb : 0 < b) : 0 < a + b := - !zero_add ▸ (add_lt_add_of_le_of_lt Ha Hb) - - theorem add_nonpos (Ha : a ≤ 0) (Hb : b ≤ 0) : a + b ≤ 0 := - !zero_add ▸ (add_le_add Ha Hb) - - theorem add_neg (Ha : a < 0) (Hb : b < 0) : a + b < 0 := - !zero_add ▸ (add_lt_add Ha Hb) - - theorem add_neg_of_neg_of_nonpos (Ha : a < 0) (Hb : b ≤ 0) : a + b < 0 := - !zero_add ▸ (add_lt_add_of_lt_of_le Ha Hb) - - theorem add_neg_of_nonpos_of_neg (Ha : a ≤ 0) (Hb : b < 0) : a + b < 0 := - !zero_add ▸ (add_lt_add_of_le_of_lt Ha Hb) - - -- TODO: add nonpos version (will be easier with simplifier) - theorem add_eq_zero_iff_eq_zero_and_eq_zero_of_nonneg_of_nonneg - (Ha : 0 ≤ a) (Hb : 0 ≤ b) : a + b = 0 ↔ a = 0 ∧ b = 0 := - iff.intro - (assume Hab : a + b = 0, - have Ha' : a ≤ 0, from - calc - a = a + 0 : by rewrite add_zero - ... ≤ a + b : add_le_add_left Hb - ... = 0 : Hab, - have Haz : a = 0, from le.antisymm Ha' Ha, - have Hb' : b ≤ 0, from - calc - b = 0 + b : by rewrite zero_add - ... ≤ a + b : add_le_add_right Ha - ... = 0 : Hab, - have Hbz : b = 0, from le.antisymm Hb' Hb, - and.intro Haz Hbz) - (assume Hab : a = 0 ∧ b = 0, - obtain Ha' Hb', from Hab, - by rewrite [Ha', Hb', add_zero]) - - theorem le_add_of_nonneg_of_le (Ha : 0 ≤ a) (Hbc : b ≤ c) : b ≤ a + c := - !zero_add ▸ add_le_add Ha Hbc - - theorem le_add_of_le_of_nonneg (Hbc : b ≤ c) (Ha : 0 ≤ a) : b ≤ c + a := - !add_zero ▸ add_le_add Hbc Ha - - theorem lt_add_of_pos_of_le (Ha : 0 < a) (Hbc : b ≤ c) : b < a + c := - !zero_add ▸ add_lt_add_of_lt_of_le Ha Hbc - - theorem lt_add_of_le_of_pos (Hbc : b ≤ c) (Ha : 0 < a) : b < c + a := - !add_zero ▸ add_lt_add_of_le_of_lt Hbc Ha - - theorem add_le_of_nonpos_of_le (Ha : a ≤ 0) (Hbc : b ≤ c) : a + b ≤ c := - !zero_add ▸ add_le_add Ha Hbc - - theorem add_le_of_le_of_nonpos (Hbc : b ≤ c) (Ha : a ≤ 0) : b + a ≤ c := - !add_zero ▸ add_le_add Hbc Ha - - theorem add_lt_of_neg_of_le (Ha : a < 0) (Hbc : b ≤ c) : a + b < c := - !zero_add ▸ add_lt_add_of_lt_of_le Ha Hbc - - theorem add_lt_of_le_of_neg (Hbc : b ≤ c) (Ha : a < 0) : b + a < c := - !add_zero ▸ add_lt_add_of_le_of_lt Hbc Ha - - theorem lt_add_of_nonneg_of_lt (Ha : 0 ≤ a) (Hbc : b < c) : b < a + c := - !zero_add ▸ add_lt_add_of_le_of_lt Ha Hbc - - theorem lt_add_of_lt_of_nonneg (Hbc : b < c) (Ha : 0 ≤ a) : b < c + a := - !add_zero ▸ add_lt_add_of_lt_of_le Hbc Ha - - theorem lt_add_of_pos_of_lt (Ha : 0 < a) (Hbc : b < c) : b < a + c := - !zero_add ▸ add_lt_add Ha Hbc - - theorem lt_add_of_lt_of_pos (Hbc : b < c) (Ha : 0 < a) : b < c + a := - !add_zero ▸ add_lt_add Hbc Ha - - theorem add_lt_of_nonpos_of_lt (Ha : a ≤ 0) (Hbc : b < c) : a + b < c := - !zero_add ▸ add_lt_add_of_le_of_lt Ha Hbc - - theorem add_lt_of_lt_of_nonpos (Hbc : b < c) (Ha : a ≤ 0) : b + a < c := - !add_zero ▸ add_lt_add_of_lt_of_le Hbc Ha - - theorem add_lt_of_neg_of_lt (Ha : a < 0) (Hbc : b < c) : a + b < c := - !zero_add ▸ add_lt_add Ha Hbc - - theorem add_lt_of_lt_of_neg (Hbc : b < c) (Ha : a < 0) : b + a < c := - !add_zero ▸ add_lt_add Hbc Ha -end - --- TODO: add properties of max and min - -/- partially ordered groups -/ - -structure ordered_comm_group [class] (A : Type) extends add_comm_group A, order_pair A := -(add_le_add_left : ∀a b, le a b → ∀c, le (add c a) (add c b)) - -theorem ordered_comm_group.le_of_add_le_add_left [s : ordered_comm_group A] {a b c : A} (H : a + b ≤ a + c) : b ≤ c := -assert H' : -a + (a + b) ≤ -a + (a + c), from ordered_comm_group.add_le_add_left _ _ H _, -by rewrite *neg_add_cancel_left at H'; exact H' - -definition ordered_comm_group.to_ordered_cancel_comm_monoid [instance] [coercion] [reducible] - [s : ordered_comm_group A] : ordered_cancel_comm_monoid A := -⦃ ordered_cancel_comm_monoid, s, - add_left_cancel := @add.left_cancel A s, - add_right_cancel := @add.right_cancel A s, - le_of_add_le_add_left := @ordered_comm_group.le_of_add_le_add_left A s ⦄ - -section - variables [s : ordered_comm_group A] (a b c d e : A) - include s - - theorem neg_le_neg {a b : A} (H : a ≤ b) : -b ≤ -a := - have H1 : 0 ≤ -a + b, from !add.left_inv ▸ !(add_le_add_left H), - !add_neg_cancel_right ▸ !zero_add ▸ add_le_add_right H1 (-b) - - theorem le_of_neg_le_neg {a b : A} (H : -b ≤ -a) : a ≤ b := - neg_neg a ▸ neg_neg b ▸ neg_le_neg H - - theorem neg_le_neg_iff_le : -a ≤ -b ↔ b ≤ a := - iff.intro le_of_neg_le_neg neg_le_neg - - theorem nonneg_of_neg_nonpos {a : A} (H : -a ≤ 0) : 0 ≤ a := - le_of_neg_le_neg (neg_zero⁻¹ ▸ H) - - theorem neg_nonpos_of_nonneg {a : A} (H : 0 ≤ a) : -a ≤ 0 := - neg_zero ▸ neg_le_neg H - - theorem neg_nonpos_iff_nonneg : -a ≤ 0 ↔ 0 ≤ a := - iff.intro nonneg_of_neg_nonpos neg_nonpos_of_nonneg - - theorem nonpos_of_neg_nonneg {a : A} (H : 0 ≤ -a) : a ≤ 0 := - le_of_neg_le_neg (neg_zero⁻¹ ▸ H) - - theorem neg_nonneg_of_nonpos {a : A} (H : a ≤ 0) : 0 ≤ -a := - neg_zero ▸ neg_le_neg H - - theorem neg_nonneg_iff_nonpos : 0 ≤ -a ↔ a ≤ 0 := - iff.intro nonpos_of_neg_nonneg neg_nonneg_of_nonpos - - theorem neg_lt_neg {a b : A} (H : a < b) : -b < -a := - have H1 : 0 < -a + b, from !add.left_inv ▸ !(add_lt_add_left H), - !add_neg_cancel_right ▸ !zero_add ▸ add_lt_add_right H1 (-b) - - theorem lt_of_neg_lt_neg {a b : A} (H : -b < -a) : a < b := - neg_neg a ▸ neg_neg b ▸ neg_lt_neg H - - theorem neg_lt_neg_iff_lt : -a < -b ↔ b < a := - iff.intro lt_of_neg_lt_neg neg_lt_neg - - theorem pos_of_neg_neg {a : A} (H : -a < 0) : 0 < a := - lt_of_neg_lt_neg (neg_zero⁻¹ ▸ H) - - theorem neg_neg_of_pos {a : A} (H : 0 < a) : -a < 0 := - neg_zero ▸ neg_lt_neg H - - theorem neg_neg_iff_pos : -a < 0 ↔ 0 < a := - iff.intro pos_of_neg_neg neg_neg_of_pos - - theorem neg_of_neg_pos {a : A} (H : 0 < -a) : a < 0 := - lt_of_neg_lt_neg (neg_zero⁻¹ ▸ H) - - theorem neg_pos_of_neg {a : A} (H : a < 0) : 0 < -a := - neg_zero ▸ neg_lt_neg H - - theorem neg_pos_iff_neg : 0 < -a ↔ a < 0 := - iff.intro neg_of_neg_pos neg_pos_of_neg - - theorem le_neg_iff_le_neg : a ≤ -b ↔ b ≤ -a := !neg_neg ▸ !neg_le_neg_iff_le - - theorem neg_le_iff_neg_le : -a ≤ b ↔ -b ≤ a := !neg_neg ▸ !neg_le_neg_iff_le - - theorem lt_neg_iff_lt_neg : a < -b ↔ b < -a := !neg_neg ▸ !neg_lt_neg_iff_lt - - theorem neg_lt_iff_neg_lt : -a < b ↔ -b < a := !neg_neg ▸ !neg_lt_neg_iff_lt - - theorem sub_nonneg_iff_le : 0 ≤ a - b ↔ b ≤ a := !sub_self ▸ !add_le_add_right_iff - - theorem sub_nonpos_iff_le : a - b ≤ 0 ↔ a ≤ b := !sub_self ▸ !add_le_add_right_iff - - theorem sub_pos_iff_lt : 0 < a - b ↔ b < a := !sub_self ▸ !add_lt_add_right_iff - - theorem sub_neg_iff_lt : a - b < 0 ↔ a < b := !sub_self ▸ !add_lt_add_right_iff - - theorem add_le_iff_le_neg_add : a + b ≤ c ↔ b ≤ -a + c := - have H: a + b ≤ c ↔ -a + (a + b) ≤ -a + c, from iff.symm (!add_le_add_left_iff), - !neg_add_cancel_left ▸ H - - theorem add_le_iff_le_sub_left : a + b ≤ c ↔ b ≤ c - a := - by rewrite [sub_eq_add_neg, {c+_}add.comm]; apply add_le_iff_le_neg_add - - theorem add_le_iff_le_sub_right : a + b ≤ c ↔ a ≤ c - b := - have H: a + b ≤ c ↔ a + b - b ≤ c - b, from iff.symm (!add_le_add_right_iff), - !add_neg_cancel_right ▸ H - - theorem le_add_iff_neg_add_le : a ≤ b + c ↔ -b + a ≤ c := - assert H: a ≤ b + c ↔ -b + a ≤ -b + (b + c), from iff.symm (!add_le_add_left_iff), - by rewrite neg_add_cancel_left at H; exact H - - theorem le_add_iff_sub_left_le : a ≤ b + c ↔ a - b ≤ c := - by rewrite [sub_eq_add_neg, {a+_}add.comm]; apply le_add_iff_neg_add_le - - theorem le_add_iff_sub_right_le : a ≤ b + c ↔ a - c ≤ b := - assert H: a ≤ b + c ↔ a - c ≤ b + c - c, from iff.symm (!add_le_add_right_iff), - by rewrite add_neg_cancel_right at H; exact H - - theorem add_lt_iff_lt_neg_add_left : a + b < c ↔ b < -a + c := - assert H: a + b < c ↔ -a + (a + b) < -a + c, from iff.symm (!add_lt_add_left_iff), - begin rewrite neg_add_cancel_left at H, exact H end - - theorem add_lt_iff_lt_neg_add_right : a + b < c ↔ a < -b + c := - by rewrite add.comm; apply add_lt_iff_lt_neg_add_left - - theorem add_lt_iff_lt_sub_left : a + b < c ↔ b < c - a := - begin - rewrite [sub_eq_add_neg, {c+_}add.comm], - apply add_lt_iff_lt_neg_add_left - end - - theorem add_lt_add_iff_lt_sub_right : a + b < c ↔ a < c - b := - assert H: a + b < c ↔ a + b - b < c - b, from iff.symm (!add_lt_add_right_iff), - by rewrite add_neg_cancel_right at H; exact H - - theorem lt_add_iff_neg_add_lt_left : a < b + c ↔ -b + a < c := - assert H: a < b + c ↔ -b + a < -b + (b + c), from iff.symm (!add_lt_add_left_iff), - by rewrite neg_add_cancel_left at H; exact H - - theorem lt_add_iff_neg_add_lt_right : a < b + c ↔ -c + a < b := - by rewrite add.comm; apply lt_add_iff_neg_add_lt_left - - theorem lt_add_iff_sub_lt_left : a < b + c ↔ a - b < c := - by rewrite [sub_eq_add_neg, {a + _}add.comm]; apply lt_add_iff_neg_add_lt_left - - theorem lt_add_iff_sub_lt_right : a < b + c ↔ a - c < b := - by rewrite add.comm; apply lt_add_iff_sub_lt_left - - -- TODO: the Isabelle library has varations on a + b ≤ b ↔ a ≤ 0 - theorem le_iff_le_of_sub_eq_sub {a b c d : A} (H : a - b = c - d) : a ≤ b ↔ c ≤ d := - calc - a ≤ b ↔ a - b ≤ 0 : iff.symm (sub_nonpos_iff_le a b) - ... = (c - d ≤ 0) : by rewrite H - ... ↔ c ≤ d : sub_nonpos_iff_le c d - - theorem lt_iff_lt_of_sub_eq_sub {a b c d : A} (H : a - b = c - d) : a < b ↔ c < d := - calc - a < b ↔ a - b < 0 : iff.symm (sub_neg_iff_lt a b) - ... = (c - d < 0) : by rewrite H - ... ↔ c < d : sub_neg_iff_lt c d - - theorem sub_le_sub_left {a b : A} (H : a ≤ b) (c : A) : c - b ≤ c - a := - add_le_add_left (neg_le_neg H) c - - theorem sub_le_sub_right {a b : A} (H : a ≤ b) (c : A) : a - c ≤ b - c := add_le_add_right H (-c) - - theorem sub_le_sub {a b c d : A} (Hab : a ≤ b) (Hcd : c ≤ d) : a - d ≤ b - c := - add_le_add Hab (neg_le_neg Hcd) - - theorem sub_lt_sub_left {a b : A} (H : a < b) (c : A) : c - b < c - a := - add_lt_add_left (neg_lt_neg H) c - - theorem sub_lt_sub_right {a b : A} (H : a < b) (c : A) : a - c < b - c := add_lt_add_right H (-c) - - theorem sub_lt_sub {a b c d : A} (Hab : a < b) (Hcd : c < d) : a - d < b - c := - add_lt_add Hab (neg_lt_neg Hcd) - - theorem sub_lt_sub_of_le_of_lt {a b c d : A} (Hab : a ≤ b) (Hcd : c < d) : a - d < b - c := - add_lt_add_of_le_of_lt Hab (neg_lt_neg Hcd) - - theorem sub_lt_sub_of_lt_of_le {a b c d : A} (Hab : a < b) (Hcd : c ≤ d) : a - d < b - c := - add_lt_add_of_lt_of_le Hab (neg_le_neg Hcd) - - theorem sub_le_self (a : A) {b : A} (H : b ≥ 0) : a - b ≤ a := - calc - a - b = a + -b : rfl - ... ≤ a + 0 : add_le_add_left (neg_nonpos_of_nonneg H) - ... = a : by rewrite add_zero - - theorem sub_lt_self (a : A) {b : A} (H : b > 0) : a - b < a := - calc - a - b = a + -b : rfl - ... < a + 0 : add_lt_add_left (neg_neg_of_pos H) - ... = a : by rewrite add_zero -end - -structure decidable_linear_ordered_comm_group [class] (A : Type) - extends add_comm_group A, decidable_linear_order A := - (add_le_add_left : ∀ a b, le a b → ∀ c, le (add c a) (add c b)) - -private theorem add_le_add_left' (A : Type) (s : decidable_linear_ordered_comm_group A) (a b : A) : - a ≤ b → (∀ c : A, c + a ≤ c + b) := - decidable_linear_ordered_comm_group.add_le_add_left a b - -definition decidable_linear_ordered_comm_group.to_ordered_comm_group [instance] [reducible] [coercion] - (A : Type) [s : decidable_linear_ordered_comm_group A] : ordered_comm_group A := - ⦃ordered_comm_group, s, - le_of_lt := @le_of_lt A s, - add_le_add_left := add_le_add_left' A s, - lt_of_le_of_lt := @lt_of_le_of_lt A s, - lt_of_lt_of_le := @lt_of_lt_of_le A s⦄ - -section - variables [s : decidable_linear_ordered_comm_group A] - variables {a b c d e : A} - include s - - theorem eq_zero_of_neg_eq (H : -a = a) : a = 0 := - lt.by_cases - (assume H1 : a < 0, - have H2: a > 0, from H ▸ neg_pos_of_neg H1, - absurd H1 (lt.asymm H2)) - (assume H1 : a = 0, H1) - (assume H1 : a > 0, - have H2: a < 0, from H ▸ neg_neg_of_pos H1, - absurd H1 (lt.asymm H2)) - - definition abs (a : A) : A := if 0 ≤ a then a else -a - - theorem abs_of_nonneg (H : a ≥ 0) : abs a = a := if_pos H - - theorem abs_of_pos (H : a > 0) : abs a = a := if_pos (le_of_lt H) - - theorem abs_of_neg (H : a < 0) : abs a = -a := if_neg (not_le_of_gt H) - - theorem abs_zero : abs 0 = (0:A) := abs_of_nonneg (le.refl _) - - 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) : 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) : 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 - ... = abs a : abs_of_nonpos H) - - theorem abs_abs (a : A) : abs (abs a) = abs a := abs_of_nonneg !abs_nonneg - - 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 ≤ abs a := - !abs_neg ▸ !le_abs_self - - 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) : 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) : abs a > 0 := - by rewrite (abs_of_pos H); exact H - - 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) : 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) : 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 (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) : abs a ≤ b := - abs.by_cases H1 H2 - - 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 - section - 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 - abs (a + b) ≤ abs (a + b) : le.refl - ... = a + b : by rewrite (abs_of_nonneg H1) - ... = abs a + b : by rewrite (abs_of_nonneg H2) - ... = abs a + abs b : by rewrite (abs_of_nonneg H3)) - (assume H3 : ¬ b ≥ 0, - assert H4 : b ≤ 0, from le_of_lt (lt_of_not_ge H3), - calc - abs (a + b) = a + b : by rewrite (abs_of_nonneg H1) - ... = abs a + b : by rewrite (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 : by rewrite (abs_of_nonpos H4)) - - 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 - assume H4 : a < 0, - have H5 : a + b < 0, from !add_zero ▸ add_lt_add_of_lt_of_le H4 H2, - not_lt_of_ge H1 H5, - aux1 H1 (le_of_not_gt H3)) - (assume H2 : 0 ≤ b, - begin - have H3 : abs (b + a) ≤ abs b + abs a, - begin - rewrite add.comm at H1, - exact aux1 H1 H2 - end, - rewrite [add.comm, {abs a + _}add.comm], - exact H3 - end) - - 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, - assert H3 : -a + -b = -(a + b), by rewrite neg_add, - assert H4 : -(a + b) ≥ 0, from iff.mp' (neg_nonneg_iff_nonpos (a+b)) H2, - have H5 : -a + -b ≥ 0, begin rewrite -H3 at H4, exact H4 end, - calc - abs (a + b) = abs (-a + -b) : by rewrite [-abs_neg, neg_add] - ... ≤ abs (-a) + abs (-b) : aux2 H5 - ... = abs a + abs b : by rewrite *abs_neg) - end - - 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 - abs a - abs b + abs b = abs a : by rewrite sub_add_cancel - ... = abs (a - b + b) : by rewrite sub_add_cancel - ... ≤ abs (a - b) + abs b : abs_add_le_abs_add_abs, - algebra.le_of_add_le_add_right H1 -end - -end algebra diff --git a/library/data/pnat.lean b/library/data/pnat.lean index 56f1563cd..13d723de3 100644 --- a/library/data/pnat.lean +++ b/library/data/pnat.lean @@ -300,5 +300,25 @@ theorem pnat_cancel' (n m : ℕ+) : (n * n * m)⁻¹ * (rat_of_pnat n * rat_of_p rewrite [rat.mul.comm, *inv_mul_eq_mul_inv, simp, *inv_cancel_left, *rat.one_mul] end +definition pceil (a : ℚ) : ℕ+ := pnat.pos (ubound a) !ubound_pos + +theorem pceil_helper {a : ℚ} {n : ℕ+} (H : pceil a ≤ n) (Ha : a > 0) : n⁻¹ ≤ 1 / a := + begin + apply rat.le.trans, + apply inv_ge_of_le H, + apply div_le_div_of_le, + apply Ha, + apply ubound_ge + end + +theorem inv_pceil_div (a b : ℚ) (Ha : a > 0) (Hb : b > 0) : (pceil (a / b))⁻¹ ≤ b / a := + begin + rewrite -(@div_div' (b / a)), + apply div_le_div_of_le, + apply div_pos_of_pos, + apply pos_div_of_pos_of_pos Hb Ha, + rewrite [(div_div_eq_mul_div (ne_of_gt Hb) (ne_of_gt Ha)), rat.one_mul], + apply ubound_ge + end end pnat diff --git a/library/data/real/basic.lean b/library/data/real/basic.lean index f14c392e9..19a672191 100644 --- a/library/data/real/basic.lean +++ b/library/data/real/basic.lean @@ -21,10 +21,6 @@ local notation 1 := rat.of_num 1 ------------------------------------- -- theorems to add to (ordered) field and/or rat -theorem div_two (a : ℚ) : (a + a) / (1 + 1) = a := sorry - -theorem two_pos : (1 : ℚ) + 1 > 0 := rat.add_pos rat.zero_lt_one rat.zero_lt_one - theorem find_midpoint {a b : ℚ} (H : a > b) : ∃ c : ℚ, a > b + c := exists.intro ((a - b) / (1 + 1)) (have H2 [visible] : a + a > (b + b) + (a - b), from calc @@ -32,32 +28,19 @@ theorem find_midpoint {a b : ℚ} (H : a > b) : ∃ c : ℚ, a > b + c := ... = b + a + b - b : rat.add_sub_cancel ... = (b + b) + (a - b) : sorry, -- simp have H3 [visible] : (a + a) / (1 + 1) > ((b + b) + (a - b)) / (1 + 1), - from div_lt_div_of_lt_of_pos H2 two_pos, + from div_lt_div_of_lt_of_pos H2 dec_trivial, by rewrite [div_two at H3, -div_add_div_same at H3, div_two at H3]; exact H3) theorem add_sub_comm (a b c d : ℚ) : a + b - (c + d) = (a - c) + (b - d) := sorry -theorem div_helper (a b : ℚ) : (1 / (a * b)) * a = 1 / b := sorry - -theorem distrib_three_right (a b c d : ℚ) : (a + b + c) * d = a * d + b * d + c * d := sorry - -theorem mul_le_mul_of_mul_div_le (a b c d : ℚ) : a * (b / c) ≤ d → b * a ≤ d * c := sorry - -definition pceil (a : ℚ) : ℕ+ := pnat.pos (ubound a) !ubound_pos - -theorem pceil_helper {a : ℚ} {n : ℕ+} (H : pceil a ≤ n) : n⁻¹ ≤ 1 / a := sorry - -theorem inv_pceil_div (a b : ℚ) (Ha : a > 0) (Hb : b > 0) : (pceil (a / b))⁻¹ ≤ b / a := sorry - - theorem s_mul_assoc_lemma_4 {n : ℕ+} {ε q : ℚ} (Hε : ε > 0) (Hq : q > 0) (H : n ≥ pceil (q / ε)) : q * n⁻¹ ≤ ε := begin - let H2 := pceil_helper H, + let H2 := pceil_helper H (pos_div_of_pos_of_pos Hq Hε), let H3 := mul_le_of_le_div (pos_div_of_pos_of_pos Hq Hε) H2, rewrite -(one_mul ε), apply mul_le_mul_of_mul_div_le, - assumption + repeat assumption end ------------------------------------- @@ -80,10 +63,8 @@ theorem squeeze {a b : ℚ} (H : ∀ j : ℕ+, a ≤ b + j⁻¹ + j⁻¹ + j⁻ exact absurd !H (not_le_of_gt Ha) end - theorem squeeze_2 {a b : ℚ} (H : ∀ ε : ℚ, ε > 0 → a ≥ b - ε) : a ≥ b := sorry - theorem rewrite_helper (a b c d : ℚ) : a * b - c * d = a * (b - d) + (a - c) * d := sorry @@ -106,11 +87,9 @@ theorem factor_lemma (a b c d e : ℚ) : abs (a + b + c - (d + (b + e))) = abs ( theorem factor_lemma_2 (a b c d : ℚ) : (a + b) + (c + d) = (a + c) + (d + b) := sorry - ------------------------------------- -- The only sorry's after this point are for the simplifier. --------------------------------------- -------------------------------------- -- define cauchy sequences and equivalence. show equivalence actually is one @@ -206,7 +185,8 @@ theorem pnat_bound {ε : ℚ} (Hε : ε > 0) : ∃ p : ℕ+, p⁻¹ ≤ ε := existsi (pceil (1 / ε)), rewrite -(rat.div_div (rat.ne_of_gt Hε)) at {2}, apply pceil_helper, - apply le.refl + apply le.refl, + apply div_pos_of_pos Hε end theorem bdd_of_eq_var {s t : seq} (Hs : regular s) (Ht : regular t) (Heq : s ≡ t) : @@ -500,7 +480,7 @@ theorem s_mul_assoc {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : regula apply Hs, apply Ht, apply Hu, - rewrite [*s_mul_assoc_lemma_3, -distrib_three_right], + rewrite [*s_mul_assoc_lemma_3, -rat.distrib_three_right], apply s_mul_assoc_lemma_4, apply a, repeat apply rat.add_pos, @@ -608,6 +588,7 @@ theorem mul_bound_helper {s t : seq} (Hs : regular s) (Ht : regular t) (a b c : apply rat.le.trans, apply rat.mul_le_mul_of_nonneg_right, apply pceil_helper Hn, + repeat (apply rat.mul_pos | apply rat.add_pos | apply inv_pos | apply rat_of_pnat_is_pos), apply rat.le_of_lt, apply rat.add_pos, apply rat.mul_pos, @@ -618,7 +599,11 @@ theorem mul_bound_helper {s t : seq} (Hs : regular s) (Ht : regular t) (a b c : apply rat.add_pos, repeat apply inv_pos, apply rat_of_pnat_is_pos, - rewrite div_helper, + have H : (rat_of_pnat (K s) * (b⁻¹ + c⁻¹) + (a⁻¹ + c⁻¹) * rat_of_pnat (K t)) ≠ 0, begin + apply rat.ne_of_gt, + repeat (apply rat.mul_pos | apply rat.add_pos | apply inv_pos | apply rat_of_pnat_is_pos) + end, + rewrite (rat.div_helper H), apply rat.le.refl end, apply rat.add_le_add, @@ -786,55 +771,30 @@ theorem diff_equiv_zero_of_equiv {s t : seq} (Hs : regular s) (Ht : regular t) ( theorem mul_well_defined_half1 {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : regular u) (Etu : t ≡ u) : smul s t ≡ smul s u := begin - let Hst := reg_mul_reg Hs Ht, - let Hsu := reg_mul_reg Hs Hu, - let Hnu := reg_neg_reg Hu, - let Hstu := reg_add_reg Hst Hsu, - let Hsnu := reg_mul_reg Hs Hnu, - let Htnu := reg_add_reg Ht Hnu, --- let Hstsu := reg_add_reg Hst Hsnu, - apply equiv_of_diff_equiv_zero, - apply Hst, - apply Hsu, - apply equiv.trans, - apply reg_add_reg, - apply Hst, - apply reg_neg_reg Hsu, - rotate 1, - apply zero_is_reg, - apply equiv.symm, - apply add_well_defined, - rotate 2, - apply reg_mul_reg Hs Ht, - apply reg_neg_reg Hsu, - apply equiv.refl, - apply mul_neg_equiv_neg_mul, - apply equiv.trans, - rotate 3, - apply equiv.symm, - apply s_distrib, - repeat assumption, - rotate 1, - apply reg_add_reg Hst Hsnu, - apply Hst, - apply Hsnu, - apply reg_add_reg Hst Hsnu, - apply reg_mul_reg Hs, - apply reg_add_reg Ht Hnu, - apply zero_is_reg, - apply mul_zero_equiv_zero, - rotate 2, - apply diff_equiv_zero_of_equiv, - repeat assumption + apply equiv_of_diff_equiv_zero, + rotate 2, + apply equiv.trans, + rotate 3, + apply equiv.symm, + apply add_well_defined, + rotate 4, + apply equiv.refl, + apply mul_neg_equiv_neg_mul, + apply equiv.trans, + rotate 3, + apply equiv.symm, + apply s_distrib, + rotate 3, + apply mul_zero_equiv_zero, + rotate 2, + apply diff_equiv_zero_of_equiv, + repeat (assumption | apply reg_mul_reg | apply reg_neg_reg | apply reg_add_reg | + apply zero_is_reg) end theorem mul_well_defined_half2 {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : regular u) (Est : s ≡ t) : smul s u ≡ smul t u := begin - let Hsu := reg_mul_reg Hs Hu, - let Hus := reg_mul_reg Hu Hs, - let Htu := reg_mul_reg Ht Hu, - let Hut := reg_mul_reg Hu Ht, apply equiv.trans, rotate 3, apply s_mul_comm, @@ -845,7 +805,7 @@ theorem mul_well_defined_half2 {s t u : seq} (Hs : regular s) (Ht : regular t) ( apply Ht, rotate 1, apply s_mul_comm, - repeat assumption + repeat (assumption | apply reg_mul_reg) end theorem mul_well_defined {s t u v : seq} (Hs : regular s) (Ht : regular t) (Hu : regular u) diff --git a/library/data/real/complete.lean b/library/data/real/complete.lean index 132032f03..7c275188d 100644 --- a/library/data/real/complete.lean +++ b/library/data/real/complete.lean @@ -11,7 +11,8 @@ At this point, we no longer proceed constructively: this file makes heavy use of Here, we show that ℝ is complete. -/ -import data.real.basic data.real.order data.real.division data.rat data.nat data.pnat logic.axioms.classical +import data.real.basic data.real.order data.real.division data.rat data.nat data.pnat +import logic.axioms.classical open -[coercions] rat local notation 0 := rat.of_num 0 local notation 1 := rat.of_num 1