From 4161b9ccbf3b5695d342448a8e41faf81ee840fc Mon Sep 17 00:00:00 2001 From: Rob Lewis Date: Tue, 23 Jun 2015 22:17:50 +1000 Subject: [PATCH] feat(library/data/real): rearrange constant sequence theorems to introduce rat coercion earlier. begin migrating theorems from algebra --- library/data/real/basic.lean | 35 +++++++++ library/data/real/complete.lean | 129 +++++++++++++------------------- library/data/real/division.lean | 1 + library/data/real/order.lean | 48 +++++++++++- 4 files changed, 134 insertions(+), 79 deletions(-) diff --git a/library/data/real/basic.lean b/library/data/real/basic.lean index 2b43d31fb..2c7f167f2 100644 --- a/library/data/real/basic.lean +++ b/library/data/real/basic.lean @@ -103,6 +103,7 @@ theorem factor_lemma_2 (a b c d : ℚ) : (a + b) + (c + d) = (a + c) + (d + b) : -------------------------------------- -- define cauchy sequences and equivalence. show equivalence actually is one +namespace s notation `seq` := ℕ+ → ℚ @@ -884,6 +885,24 @@ theorem zero_nequiv_one : ¬ zero ≡ one := apply absurd (one_lt_two) (not_lt_of_ge H'') end +--------------------------------------------- +-- constant sequences + +definition const (a : ℚ) : seq := λ n, a + +theorem const_reg (a : ℚ) : regular (const a) := + begin + intros, + rewrite [↑const, rat.sub_self, abs_zero], + apply add_invs_nonneg + end + +theorem add_consts (a b : ℚ) : sadd (const a) (const b) ≡ const (a + b) := + begin + rewrite [↑sadd, ↑const], + apply equiv.refl + end + --------------------------------------------- -- create the type of regular sequences and lift theorems @@ -967,10 +986,16 @@ theorem r_distrib (s t u : reg_seq) : requiv (s * (t + u)) (s * t + s * u) := theorem r_zero_nequiv_one : ¬ requiv r_zero r_one := zero_nequiv_one +definition r_const (a : ℚ) : reg_seq := reg_seq.mk (const a) (const_reg a) + +theorem r_add_consts (a b : ℚ) : requiv (r_const a + r_const b) (r_const (a + b)) := add_consts a b + +end s ---------------------------------------------- -- take quotients to get ℝ and show it's a comm ring namespace real +open s definition real := quot reg_seq.to_setoid notation `ℝ` := real @@ -1054,4 +1079,14 @@ definition comm_ring [reducible] : algebra.comm_ring ℝ := apply mul_comm end +definition const (a : ℚ) : ℝ := quot.mk (s.r_const a) + +theorem add_consts (a b : ℚ) : const a + const b = const (a + b) := + quot.sound (s.r_add_consts a b) + +theorem sub_consts (a b : ℚ) : const a + -const b = const (a - b) := !add_consts + +theorem add_half_const (n : ℕ+) : const (2 * n)⁻¹ + const (2 * n)⁻¹ = const (n⁻¹) := + by rewrite [add_consts, pnat.add_halves] + end real diff --git a/library/data/real/complete.lean b/library/data/real/complete.lean index 7c275188d..c02e6fe4a 100644 --- a/library/data/real/complete.lean +++ b/library/data/real/complete.lean @@ -27,18 +27,6 @@ local notation 3 := pnat.pos (nat.of_num 3) dec_trivial namespace s -theorem nonneg_of_ge_neg_invs (a : ℚ) (H : ∀ n : ℕ+, -n⁻¹ ≤ a) : 0 ≤ a := sorry - -definition const (a : ℚ) : seq := λ n, a - -theorem const_reg (a : ℚ) : regular (const a) := - begin - intros, - rewrite [↑const, sub_self, abs_zero], - apply add_invs_nonneg - end - -definition r_const (a : ℚ) : reg_seq := reg_seq.mk (const a) (const_reg a) theorem rat_approx_l1 {s : seq} (H : regular s) : ∀ n : ℕ+, ∃ q : ℚ, ∃ N : ℕ+, ∀ m : ℕ+, m ≥ N → abs (s m - q) ≤ n⁻¹ := @@ -106,7 +94,8 @@ theorem r_rat_approx (s : reg_seq) : ∀ n : ℕ+, ∃ q : ℚ, r_le (r_abs (radd s (rneg (r_const q)))) (r_const n⁻¹) := rat_approx (reg_seq.is_reg s) -theorem const_bound {s : seq} (Hs : regular s) (n : ℕ+) : s_le (s_abs (sadd s (sneg (const (s n))))) (const n⁻¹) := +theorem const_bound {s : seq} (Hs : regular s) (n : ℕ+) : + s_le (s_abs (sadd s (sneg (const (s n))))) (const n⁻¹) := begin rewrite ↑[s_le, nonneg, s_abs, sadd, sneg, const], intro m, @@ -127,40 +116,6 @@ theorem abs_const (a : ℚ) : const (abs a) ≡ s_abs (const a) := theorem r_abs_const (a : ℚ) : requiv (r_const (abs a) ) (r_abs (r_const a)) := abs_const a -theorem add_consts (a b : ℚ) : sadd (const a) (const b) ≡ const (a + b) := - begin - rewrite [↑sadd, ↑const], - apply equiv.refl - end - -theorem r_add_consts (a b : ℚ) : requiv (r_const a + r_const b) (r_const (a + b)) := add_consts a b - -theorem const_le_const_of_le {a b : ℚ} (H : a ≤ b) : s_le (const a) (const b) := - begin - rewrite [↑s_le, ↑nonneg], - intro n, - rewrite [↑sadd, ↑sneg, ↑const], - apply rat.le.trans, - apply rat.neg_nonpos_of_nonneg, - apply rat.le_of_lt, - apply inv_pos, - apply iff.mp' !rat.sub_nonneg_iff_le, - apply H - end - -theorem le_of_const_le_const {a b : ℚ} (H : s_le (const a) (const b)) : a ≤ b := - begin - rewrite [↑s_le at H, ↑nonneg at H, ↑sadd at H, ↑sneg at H, ↑const at H], - apply iff.mp !rat.sub_nonneg_iff_le, - apply nonneg_of_ge_neg_invs _ H - end - -theorem r_const_le_const_of_le {a b : ℚ} (H : a ≤ b) : r_le (r_const a) (r_const b) := - const_le_const_of_le H - -theorem r_le_of_const_le_const {a b : ℚ} (H : r_le (r_const a) (r_const b)) : a ≤ b := - le_of_const_le_const H - theorem equiv_abs_of_ge_zero {s : seq} (Hs : regular s) (Hz : s_le zero s) : s_abs s ≡ s := begin apply eq_of_bdd, @@ -238,6 +193,18 @@ theorem r_equiv_neg_abs_of_le_zero {s : reg_seq} (Hz : r_le s r_zero) : requiv ( end s namespace real +open [classes] s + +/-- +definition const (a : ℚ) : ℝ := quot.mk (s.r_const a) + +theorem add_consts (a b : ℚ) : const a + const b = const (a + b) := + quot.sound (s.r_add_consts a b) + +theorem sub_consts (a b : ℚ) : const a + -const b = const (a - b) := !add_consts + +theorem add_half_const (n : ℕ+) : const (2 * n)⁻¹ + const (2 * n)⁻¹ = const (n⁻¹) := + by rewrite [add_consts, pnat.add_halves]-/ theorem p_add_fractions (n : ℕ+) : (2 * n)⁻¹ + (2 * 3 * n)⁻¹ + (3 * n)⁻¹ = n⁻¹ := sorry @@ -245,23 +212,7 @@ theorem rewrite_helper9 (a b c : ℝ) : b - c = (b - a) - (c - a) := sorry theorem rewrite_helper10 (a b c d : ℝ) : c - d = (c - a) + (a - b) + (b - d) := sorry -definition rep (x : ℝ) : reg_seq := some (quot.exists_rep x) - -definition const (a : ℚ) : ℝ := quot.mk (s.r_const a) - -theorem add_consts (a b : ℚ) : const a + const b = const (a + b) := - quot.sound (s.r_add_consts a b) - -theorem sub_consts (a b : ℚ) : const a - const b = const (a - b) := !add_consts - -theorem add_half_const (n : ℕ+) : const (2 * n)⁻¹ + const (2 * n)⁻¹ = const (n⁻¹) := - by rewrite [add_consts, pnat.add_halves] - -theorem const_le_const_of_le (a b : ℚ) : a ≤ b → const a ≤ const b := - s.r_const_le_const_of_le - -theorem le_of_const_le_const (a b : ℚ) : const a ≤ const b → a ≤ b := - s.r_le_of_const_le_const +definition rep (x : ℝ) : s.reg_seq := some (quot.exists_rep x) definition re_abs (x : ℝ) : ℝ := quot.lift_on x (λ a, quot.mk (s.r_abs a)) (take a b Hab, quot.sound (s.r_abs_well_defined Hab)) @@ -312,6 +263,26 @@ definition converges_to (X : r_seq) (a : ℝ) (N : ℕ+ → ℕ+) := definition cauchy (X : r_seq) (M : ℕ+ → ℕ+) := ∀ k : ℕ+, ∀ m n : ℕ+, m ≥ M k → n ≥ M k → abs (X m - X n) ≤ const k⁻¹ +--set_option pp.implicit true +--set_option pp.coercions true + +--check add_half_const +--check const + +-- Lean is using algebra operations in these theorems, instead of the ones defined directly on real. +-- Need to finish the migration to real to fix this. + +--set_option pp.all true +theorem add_consts2 (a b : ℚ) : const a + const b = const (a + b) := + !add_consts --quot.sound (s.r_add_consts a b) +--check add_consts +--check add_consts2 + +theorem sub_consts2 (a b : ℚ) : const a - const b = const (a - b) := !sub_consts + +theorem add_half_const2 (n : ℕ+) : const (2 * n)⁻¹ + const (2 * n)⁻¹ = const (n⁻¹) := + by xrewrite [add_consts2, pnat.add_halves] + theorem cauchy_of_converges_to {X : r_seq} {a : ℝ} {N : ℕ+ → ℕ+} (Hc : converges_to X a N) : cauchy X (λ k, N (2 * k)) := @@ -327,7 +298,7 @@ theorem cauchy_of_converges_to {X : r_seq} {a : ℝ} {N : ℕ+ → ℕ+} (Hc : c rewrite algebra.abs_neg, apply Hc, apply Hn, - rewrite add_half_const, + xrewrite add_half_const2, apply !algebra.le.refl end @@ -337,7 +308,7 @@ theorem Nb_spec_right (M : ℕ+ → ℕ+) (k : ℕ+) : M (2 * k) ≤ Nb M k := ! theorem Nb_spec_left (M : ℕ+ → ℕ+) (k : ℕ+) : 3 * k ≤ Nb M k := !max_left -definition lim_seq {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) : seq := +definition lim_seq {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) : ℕ+ → ℚ := λ k, approx (X (Nb M k)) (2 * k) theorem lim_seq_reg_helper {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) {m n : ℕ+} @@ -358,20 +329,22 @@ theorem lim_seq_reg_helper {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) {m apply pnat.le.trans, apply Hmn, apply Nb_spec_right, - rewrite [*add_consts, rat.add.assoc, pnat.add_halves], + rewrite [*add_consts2, rat.add.assoc, pnat.add_halves], apply const_le_const_of_le, apply rat.add_le_add_right, apply inv_ge_of_le, apply pnat.mul_le_mul_left end -theorem lim_seq_reg {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) : regular (lim_seq Hc) := +-- the remaineder is commented out temporarily, until migration is finished. + +/-theorem lim_seq_reg {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) : s.regular (lim_seq Hc) := begin - rewrite ↑regular, + rewrite ↑s.regular, intro m n, apply le_of_const_le_const, - rewrite [abs_const, -sub_consts, (rewrite_helper10 (X (Nb M m)) (X (Nb M n)))], - apply algebra.le.trans, + rewrite [abs_const, -sub_consts, -sub_eq_add_neg, (rewrite_helper10 (X (Nb M m)) (X (Nb M n)))],--, -sub_consts2, (rewrite_helper10 (X (Nb M m)) (X (Nb M n)))], + apply real.le.trans, apply algebra.abs_add_three, let Hor := decidable.em (M (2 * m) ≥ M (2 * n)), apply or.elim Hor, @@ -379,23 +352,23 @@ theorem lim_seq_reg {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) : regular apply lim_seq_reg_helper Hc Hor1, intro Hor2, let Hor2' := pnat.le_of_lt (pnat.lt_of_not_le Hor2), - rewrite [algebra.abs_sub (X (Nb M n)), algebra.abs_sub (X (Nb M m)), algebra.abs_sub, -- ??? + rewrite [real.abs_sub (X (Nb M n)), algebra.abs_sub (X (Nb M m)), algebra.abs_sub, -- ??? rat.add.comm, algebra.add_comm_three], apply lim_seq_reg_helper Hc Hor2' end theorem lim_seq_spec {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) (k : ℕ+) : - s.s_le (s.s_abs (sadd (lim_seq Hc) (sneg (s.const (lim_seq Hc k))) )) (s.const k⁻¹) := + s.s_le (s.s_abs (s.sadd (lim_seq Hc) (s.sneg (s.const (lim_seq Hc k))) )) (s.const k⁻¹) := begin apply s.const_bound, apply lim_seq_reg end -definition r_lim_seq {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) : reg_seq := - reg_seq.mk (lim_seq Hc) (lim_seq_reg Hc) +definition r_lim_seq {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) : s.reg_seq := + s.reg_seq.mk (lim_seq Hc) (lim_seq_reg Hc) theorem r_lim_seq_spec {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) (k : ℕ+) : - s.r_le (s.r_abs (((r_lim_seq Hc) + -s.r_const ((reg_seq.sq (r_lim_seq Hc)) k)))) (s.r_const (k)⁻¹) := + s.r_le (s.r_abs (( s.radd (r_lim_seq Hc) (s.rneg (s.r_const ((s.reg_seq.sq (r_lim_seq Hc)) k)))))) (s.r_const (k)⁻¹) := lim_seq_spec Hc k definition lim {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) : ℝ := @@ -441,7 +414,7 @@ theorem converges_of_cauchy {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) : rewrite ↑lim_seq, apply approx_spec, apply lim_spec, - rewrite 2 add_consts, + rewrite 2 add_consts2, apply const_le_const_of_le, apply rat.le.trans, apply add_le_add_three, @@ -461,6 +434,6 @@ theorem converges_of_cauchy {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) : apply Nb_spec_left, rewrite [-*pnat.mul.assoc, p_add_fractions], apply rat.le.refl - end + end-/ end real diff --git a/library/data/real/division.lean b/library/data/real/division.lean index 0df84670c..0e8d78793 100644 --- a/library/data/real/division.lean +++ b/library/data/real/division.lean @@ -606,6 +606,7 @@ end s namespace real +open [classes] s definition inv (x : ℝ) : ℝ := quot.lift_on x (λ a, quot.mk (s.r_inv a)) (λ a b H, quot.sound (s.r_inv_well_defined H)) diff --git a/library/data/real/order.lean b/library/data/real/order.lean index f49c06467..22752874b 100644 --- a/library/data/real/order.lean +++ b/library/data/real/order.lean @@ -47,6 +47,7 @@ theorem helper_1 {a : ℚ} (H : a > 0) : -a + -a ≤ -a := sorry theorem rewrite_helper8 (a b c : ℚ) : a - b = c - b + (a - c) := sorry -- simp +theorem nonneg_of_ge_neg_invs (a : ℚ) (H : ∀ n : ℕ+, -n⁻¹ ≤ a) : 0 ≤ a := sorry --------- namespace s @@ -906,6 +907,28 @@ theorem s_lt_of_le_of_lt {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : r apply max_left end +----------------------------- +-- const theorems + +theorem const_le_const_of_le {a b : ℚ} (H : a ≤ b) : s_le (const a) (const b) := + begin + rewrite [↑s_le, ↑nonneg], + intro n, + rewrite [↑sadd, ↑sneg, ↑const], + apply rat.le.trans, + apply rat.neg_nonpos_of_nonneg, + apply rat.le_of_lt, + apply inv_pos, + apply iff.mp' !rat.sub_nonneg_iff_le, + apply H + end + +theorem le_of_const_le_const {a b : ℚ} (H : s_le (const a) (const b)) : a ≤ b := + begin + rewrite [↑s_le at H, ↑nonneg at H, ↑sadd at H, ↑sneg at H, ↑const at H], + apply iff.mp !rat.sub_nonneg_iff_le, + apply nonneg_of_ge_neg_invs _ H + end -------- lift to reg_seqs definition r_lt (s t : reg_seq) := s_lt (reg_seq.sq s) (reg_seq.sq t) @@ -982,9 +1005,16 @@ theorem r_zero_lt_one : r_lt r_zero r_one := s_zero_lt_one theorem r_le_of_lt_or_eq (s t : reg_seq) (H : r_lt s t ∨ requiv s t) : r_le s t := le_of_lt_or_equiv (reg_seq.is_reg s) (reg_seq.is_reg t) H +theorem r_const_le_const_of_le {a b : ℚ} (H : a ≤ b) : r_le (r_const a) (r_const b) := + const_le_const_of_le H + +theorem r_le_of_const_le_const {a b : ℚ} (H : r_le (r_const a) (r_const b)) : a ≤ b := + le_of_const_le_const H + end s open real +open [classes] s namespace real definition lt (x y : ℝ) := quot.lift_on₂ x y (λ a b, s.r_lt a b) s.r_lt_well_defined @@ -1053,7 +1083,10 @@ theorem le_of_lt_or_eq (x y : ℝ) : x < y ∨ x = y → x ≤ y := apply (or.inr (quot.exact H')) end))) -definition ordered_ring : algebra.ordered_ring ℝ := +section migrate_reals +open [classes] algebra + +definition ordered_ring [reducible] : algebra.ordered_ring ℝ := ⦃ algebra.ordered_ring, comm_ring, le_refl := le.refl, le_trans := le.trans, @@ -1068,5 +1101,18 @@ definition ordered_ring : algebra.ordered_ring ℝ := le_of_lt := le_of_lt, add_lt_add_left := add_lt_add_left ⦄ +local attribute real.ordered_ring [instance] +--set_option migrate.trace true +migrate from algebra with real + +end migrate_reals +theorem const_le_const_of_le (a b : ℚ) : a ≤ b → const a ≤ const b := + s.r_const_le_const_of_le + +theorem le_of_const_le_const (a b : ℚ) : const a ≤ const b → a ≤ b := + s.r_le_of_const_le_const end real + +--print prefix real +--check @real.lt