chore(library/real): replace theorems with versions from algebra
This commit is contained in:
Rob Lewis
Leonardo de Moura
parent
f7ab2780d4
commit
a72ca936c0
3 changed files with 55 additions and 109 deletions
|
|
@ -21,15 +21,17 @@ local notation 1 := rat.of_num 1
|
|||
-------------------------------------
|
||||
-- theorems to add to (ordered) field and/or rat
|
||||
|
||||
theorem find_midpoint {a b : ℚ} (H : a > b) : ∃ c : ℚ, a > b + c :=
|
||||
-- this can move to pnat once sorry is filled in
|
||||
theorem find_midpoint {a b : ℚ} (H : a > b) : ∃ c : ℚ, a > b + c ∧ c > 0 :=
|
||||
exists.intro ((a - b) / (1 + 1))
|
||||
(have H2 [visible] : a + a > (b + b) + (a - b), from calc
|
||||
(and.intro (have H2 [visible] : a + a > (b + b) + (a - b), from calc
|
||||
a + a > b + a : rat.add_lt_add_right H
|
||||
... = 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 dec_trivial,
|
||||
by rewrite [div_two at H3, -div_add_div_same at H3, div_two at H3]; exact H3)
|
||||
(pos_div_of_pos_of_pos (iff.mp' !sub_pos_iff_lt H) dec_trivial))
|
||||
|
||||
theorem add_sub_comm (a b c d : ℚ) : a + b - (c + d) = (a - c) + (b - d) := sorry
|
||||
|
||||
|
|
@ -47,7 +49,8 @@ theorem s_mul_assoc_lemma_4 {n : ℕ+} {ε q : ℚ} (Hε : ε > 0) (Hq : q > 0)
|
|||
-- small helper lemmas
|
||||
|
||||
theorem s_mul_assoc_lemma_3 (a b n : ℕ+) (p : ℚ) :
|
||||
p * ((a * n)⁻¹ + (b * n)⁻¹) = p * (a⁻¹ + b⁻¹) * n⁻¹ := sorry
|
||||
p * ((a * n)⁻¹ + (b * n)⁻¹) = p * (a⁻¹ + b⁻¹) * n⁻¹ :=
|
||||
by rewrite [rat.mul.assoc, rat.right_distrib, *inv_mul_eq_mul_inv]
|
||||
|
||||
theorem find_thirds (a b : ℚ) : ∃ n : ℕ+, a + n⁻¹ + n⁻¹ + n⁻¹ < a + b := sorry
|
||||
|
||||
|
|
@ -56,14 +59,22 @@ theorem squeeze {a b : ℚ} (H : ∀ j : ℕ+, a ≤ b + j⁻¹ + j⁻¹ + j⁻
|
|||
apply rat.le_of_not_gt,
|
||||
intro Hb,
|
||||
apply (exists.elim (find_midpoint Hb)),
|
||||
intros c Hc,
|
||||
intro c Hc,
|
||||
apply (exists.elim (find_thirds b c)),
|
||||
intros j Hbj,
|
||||
have Ha : a > b + j⁻¹ + j⁻¹ + j⁻¹, from lt.trans Hbj Hc,
|
||||
intro j Hbj,
|
||||
have Ha : a > b + j⁻¹ + j⁻¹ + j⁻¹, from lt.trans Hbj (and.left Hc),
|
||||
exact absurd !H (not_le_of_gt Ha)
|
||||
end
|
||||
|
||||
theorem squeeze_2 {a b : ℚ} (H : ∀ ε : ℚ, ε > 0 → a ≥ b - ε) : a ≥ b := sorry
|
||||
theorem squeeze_2 {a b : ℚ} (H : ∀ ε : ℚ, ε > 0 → a ≥ b - ε) : a ≥ b :=
|
||||
begin
|
||||
apply rat.le_of_not_gt,
|
||||
intro Hb,
|
||||
apply (exists.elim (find_midpoint Hb)),
|
||||
intro c Hc,
|
||||
let Hc' := H c (and.right Hc),
|
||||
apply (rat.not_le_of_gt (and.left Hc)) ((iff.mp' !le_add_iff_sub_right_le) Hc')
|
||||
end
|
||||
|
||||
theorem rewrite_helper (a b c d : ℚ) : a * b - c * d = a * (b - d) + (a - c) * d :=
|
||||
sorry
|
||||
|
|
|
|||
|
|
@ -12,11 +12,10 @@ and excluded middle.
|
|||
import data.real.basic data.real.order data.rat data.nat logic.axioms.classical
|
||||
open -[coercions] rat
|
||||
open -[coercions] nat
|
||||
local notation 0 := rat.of_num 0
|
||||
local notation 1 := rat.of_num 1
|
||||
open eq.ops pnat
|
||||
|
||||
|
||||
local notation 0 := rat.of_num 0
|
||||
local notation 1 := rat.of_num 1
|
||||
local notation 2 := pnat.pos (nat.of_num 2) dec_trivial
|
||||
|
||||
namespace s
|
||||
|
|
@ -24,18 +23,13 @@ namespace s
|
|||
-----------------------------
|
||||
-- helper lemmas
|
||||
|
||||
theorem abs_sub_square (a b : ℚ) : abs (a - b) * abs (a - b) = a * a + b * b - (1 + 1) * a * b :=
|
||||
by rewrite [abs_mul_self, *rat.mul_sub_left_distrib, *rat.mul_sub_right_distrib,
|
||||
sub_add_eq_sub_sub, sub_neg_eq_add, *rat.right_distrib, sub_add_eq_sub_sub, *one_mul,
|
||||
*add.assoc, {_ + b * b}add.comm, {_ + (b * b + _)}add.comm, mul.comm b a, *add.assoc]
|
||||
|
||||
theorem neg_add_rewrite {a b : ℚ} : a + -b = -(b + -a) := sorry
|
||||
|
||||
theorem abs_abs_sub_abs_le_abs_sub (a b : ℚ) : abs (abs a - abs b) ≤ abs (a - b) :=
|
||||
begin
|
||||
apply rat.nonneg_le_nonneg_of_squares_le,
|
||||
repeat apply abs_nonneg,
|
||||
rewrite [*(abs_sub_square _ _), *abs_abs, *abs_mul_self],
|
||||
rewrite [*abs_sub_square, *abs_abs, *abs_mul_self],
|
||||
apply sub_le_sub_left,
|
||||
rewrite *rat.mul.assoc,
|
||||
apply rat.mul_le_mul_of_nonneg_left,
|
||||
|
|
@ -51,15 +45,11 @@ theorem forall_of_not_exists {A : Type} {P : A → Prop} (H : ¬ ∃ a : A, P a)
|
|||
theorem and_of_not_or {a b : Prop} (H : ¬ (a ∨ b)) : ¬ a ∧ ¬ b :=
|
||||
and.intro (assume H', H (or.inl H')) (assume H', H (or.inr H'))
|
||||
|
||||
theorem ne_zero_of_abs_ne_zero {a : ℚ} (H : abs a ≠ 0) : a ≠ 0 :=
|
||||
assume Ha, H (Ha⁻¹ ▸ abs_zero)
|
||||
|
||||
-----------------------------
|
||||
-- Facts about absolute values of sequences, to define inverse
|
||||
|
||||
definition s_abs (s : seq) : seq := λ n, abs (s n)
|
||||
|
||||
|
||||
theorem abs_reg_of_reg {s : seq} (Hs : regular s) : regular (s_abs s) :=
|
||||
begin
|
||||
rewrite ↑regular at *,
|
||||
|
|
|
|||
|
|
@ -17,20 +17,31 @@ open -[coercions] nat
|
|||
open eq eq.ops pnat
|
||||
local notation 0 := rat.of_num 0
|
||||
local notation 1 := rat.of_num 1
|
||||
notation 2 := pnat.pos (of_num 2) dec_trivial
|
||||
|
||||
----------------------------------------------------------------------------------------------------
|
||||
|
||||
-- pnat theorems
|
||||
|
||||
notation 2 := pnat.pos (of_num 2) dec_trivial
|
||||
|
||||
-- rat theorems
|
||||
theorem ge_sub_of_abs_sub_le_left {a b c : ℚ} (H : abs (a - b) ≤ c) : a ≥ b - c := sorry
|
||||
|
||||
theorem ge_sub_of_abs_sub_le_right {a b c : ℚ} (H : abs (a - b) ≤ c) : b ≥ a - c :=
|
||||
ge_sub_of_abs_sub_le_left (!abs_sub ▸ H)
|
||||
|
||||
theorem sep_by_inv {a b : ℚ} (H : a > b) : ∃ N : ℕ+, a > (b + N⁻¹ + N⁻¹) := sorry
|
||||
-- this could be moved to pnat, but it uses find_midpoint which still has sorries in real.basic
|
||||
theorem sep_by_inv {a b : ℚ} (H : a > b) : ∃ N : ℕ+, a > (b + N⁻¹ + N⁻¹) :=
|
||||
begin
|
||||
apply exists.elim (find_midpoint H),
|
||||
intro c Hc,
|
||||
existsi (pceil ((1 + 1 + 1) / c)),
|
||||
apply rat.lt.trans,
|
||||
rotate 1,
|
||||
apply and.left Hc,
|
||||
rewrite rat.add.assoc,
|
||||
apply rat.add_lt_add_left,
|
||||
rewrite -(@rat.add_halves c) at {3},
|
||||
apply rat.add_lt_add,
|
||||
repeat (apply lt_of_le_of_lt;
|
||||
apply inv_pceil_div;
|
||||
apply dec_trivial;
|
||||
apply and.right Hc;
|
||||
apply div_lt_div_of_pos_of_lt_of_pos;
|
||||
repeat (apply dec_trivial);
|
||||
apply and.right Hc)
|
||||
end
|
||||
|
||||
theorem helper_1 {a : ℚ} (H : a > 0) : -a + -a ≤ -a := sorry
|
||||
|
||||
|
|
@ -159,8 +170,8 @@ theorem pos_of_pos_equiv {s t : seq} (Hs : regular s) (Heq : s ≡ t) (Hp : pos
|
|||
end
|
||||
|
||||
|
||||
theorem nonneg_of_nonneg_equiv {s t : seq} (Hs : regular s) (Ht : regular t) (Heq : s ≡ t) (Hp : nonneg s) :
|
||||
nonneg t :=
|
||||
theorem nonneg_of_nonneg_equiv {s t : seq} (Hs : regular s) (Ht : regular t) (Heq : s ≡ t)
|
||||
(Hp : nonneg s) : nonneg t :=
|
||||
begin
|
||||
apply nonneg_of_bdd_within,
|
||||
apply Ht,
|
||||
|
|
@ -342,11 +353,13 @@ theorem add_nonneg_of_nonneg {s t : seq} (Hs : nonneg s) (Ht : nonneg t) : nonne
|
|||
apply Ht
|
||||
end
|
||||
|
||||
theorem le.trans {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : regular u) (Lst : s_le s t) (Ltu : s_le t u) : s_le s u :=
|
||||
theorem le.trans {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : regular u) (Lst : s_le s t)
|
||||
(Ltu : s_le t u) : s_le s u :=
|
||||
begin
|
||||
rewrite ↑s_le at *,
|
||||
let Rz := zero_is_reg,
|
||||
have Hsum : nonneg (sadd (sadd u (sneg t)) (sadd t (sneg s)) ), from add_nonneg_of_nonneg Ltu Lst,
|
||||
have Hsum : nonneg (sadd (sadd u (sneg t)) (sadd t (sneg s))),
|
||||
from add_nonneg_of_nonneg Ltu Lst,
|
||||
have H' : nonneg (sadd (sadd u (sadd (sneg t) t)) (sneg s)), begin
|
||||
apply nonneg_of_nonneg_equiv,
|
||||
rotate 2,
|
||||
|
|
@ -384,7 +397,8 @@ theorem le.trans {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : regular u
|
|||
repeat (apply reg_add_reg | apply reg_neg_reg | assumption)
|
||||
end
|
||||
|
||||
theorem equiv_of_le_of_ge {s t : seq} (Hs : regular s) (Ht : regular t) (Lst : s_le s t) (Lts : s_le t s) : s ≡ t :=
|
||||
theorem equiv_of_le_of_ge {s t : seq} (Hs : regular s) (Ht : regular t) (Lst : s_le s t)
|
||||
(Lts : s_le t s) : s ≡ t :=
|
||||
begin
|
||||
apply equiv_of_diff_equiv_zero,
|
||||
rotate 2,
|
||||
|
|
@ -411,7 +425,8 @@ theorem equiv_of_le_of_ge {s t : seq} (Hs : regular s) (Ht : regular t) (Lst : s
|
|||
definition sep (s t : seq) := s_lt s t ∨ s_lt t s
|
||||
local infix `≢` : 50 := sep
|
||||
|
||||
theorem le_and_sep_of_lt {s t : seq} (Hs : regular s) (Ht : regular t) (Lst : s_lt s t) : s_le s t ∧ sep s t :=
|
||||
theorem le_and_sep_of_lt {s t : seq} (Hs : regular s) (Ht : regular t) (Lst : s_lt s t) :
|
||||
s_le s t ∧ sep s t :=
|
||||
begin
|
||||
apply and.intro,
|
||||
rewrite [↑s_lt at *, ↑pos at *, ↑s_le, ↑nonneg],
|
||||
|
|
@ -435,7 +450,8 @@ theorem le_and_sep_of_lt {s t : seq} (Hs : regular s) (Ht : regular t) (Lst : s_
|
|||
exact or.inl Lst
|
||||
end
|
||||
|
||||
theorem lt_of_le_and_sep {s t : seq} (Hs : regular s) (Ht : regular t) (H : s_le s t ∧ sep s t) : s_lt s t :=
|
||||
theorem lt_of_le_and_sep {s t : seq} (Hs : regular s) (Ht : regular t) (H : s_le s t ∧ sep s t) :
|
||||
s_lt s t :=
|
||||
begin
|
||||
let Le := and.left H,
|
||||
let Hsep := and.right H,
|
||||
|
|
@ -891,26 +907,6 @@ theorem s_lt_of_le_of_lt {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : r
|
|||
end
|
||||
|
||||
|
||||
|
||||
--------
|
||||
-- These are currently needed for lin_ordered_comm_ring.
|
||||
|
||||
/-theorem le_or_ge {s t : seq} (Hs : regular s) (Ht : regular t) : s_le s t ∨ s_le t s :=
|
||||
sorry
|
||||
|
||||
theorem lt_or_equiv_of_le {s t : seq} (Hs : regular s) (Ht : regular t) (Hle : s_le s t) :
|
||||
s_lt s t ∨ s ≡ t :=
|
||||
begin
|
||||
apply sorry
|
||||
end -- this is not constructive
|
||||
|
||||
theorem le_iff_lt_or_equiv {s t : seq} (Hs : regular s) (Ht : regular t) :
|
||||
s_le s t ↔ s_lt s t ∨ s ≡ t :=
|
||||
iff.intro (lt_or_equiv_of_le Hs Ht) (le_of_lt_or_equiv Hs Ht)-/
|
||||
|
||||
|
||||
|
||||
|
||||
-------- lift to reg_seqs
|
||||
definition r_lt (s t : reg_seq) := s_lt (reg_seq.sq s) (reg_seq.sq t)
|
||||
definition r_le (s t : reg_seq) := s_le (reg_seq.sq s) (reg_seq.sq t)
|
||||
|
|
@ -986,15 +982,6 @@ 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
|
||||
|
||||
----------
|
||||
-- earlier versions are sorried
|
||||
/-theorem r_le_iff_lt_or_equiv (s t : reg_seq) : r_le s t ↔ r_lt s t ∨ requiv s t :=
|
||||
le_iff_lt_or_equiv (reg_seq.is_reg s) (reg_seq.is_reg t)
|
||||
|
||||
theorem r_le_or_ge (s t : reg_seq) : r_le s t ∨ r_le t s :=
|
||||
le_or_ge (reg_seq.is_reg s) (reg_seq.is_reg t)-/
|
||||
-----------
|
||||
|
||||
end s
|
||||
|
||||
open real
|
||||
|
|
@ -1066,26 +1053,6 @@ theorem le_of_lt_or_eq (x y : ℝ) : x < y ∨ x = y → x ≤ y :=
|
|||
apply (or.inr (quot.exact H'))
|
||||
end)))
|
||||
|
||||
----------
|
||||
-- earlier versions are sorried
|
||||
/-theorem le_iff_lt_or_eq (x y : ℝ) : x ≤ y ↔ x < y ∨ x = y :=
|
||||
iff.intro
|
||||
(quot.induction_on₂ x y (λ s t H, or.elim (iff.mp ((s.r_le_iff_lt_or_equiv s t)) H)
|
||||
(take H1, or.inl H1)
|
||||
(take H2, or.inr (quot.sound H2))))
|
||||
(quot.induction_on₂ x y (λ s t H, or.elim H (take H', begin
|
||||
let H'' := iff.mp' (s.r_le_iff_lt_or_equiv s t),
|
||||
apply H'' (or.inl H')
|
||||
end)
|
||||
(take H', begin
|
||||
let H'' := iff.mp' (s.r_le_iff_lt_or_equiv s t),
|
||||
apply H'' (or.inr (quot.exact H'))
|
||||
end)))
|
||||
|
||||
theorem le_or_ge (x y : ℝ) : x ≤ y ∨ y ≤ x :=
|
||||
quot.induction_on₂ x y (λ s t, s.r_le_or_ge s t)-/
|
||||
-------------
|
||||
|
||||
definition ordered_ring : algebra.ordered_ring ℝ :=
|
||||
⦃ algebra.ordered_ring, comm_ring,
|
||||
le_refl := le.refl,
|
||||
|
|
@ -1102,26 +1069,4 @@ definition ordered_ring : algebra.ordered_ring ℝ :=
|
|||
add_lt_add_left := add_lt_add_left
|
||||
⦄
|
||||
|
||||
-----------------------------------
|
||||
--- here is where classical logic comes in
|
||||
--theorem sep_is_eq (x y : ℝ) : x ≢ y = ¬ (x = y) := sorry
|
||||
|
||||
/-theorem sep_is_eq (x y : ℝ) : x ≢ y = ¬ (x = y) := begin
|
||||
apply propext,
|
||||
apply iff.intro,
|
||||
intro Hsep,
|
||||
intro Heq,
|
||||
rewrite Heq at Hsep,
|
||||
apply absurd Hsep !not_sep_self,
|
||||
intro Hneq,
|
||||
end-/
|
||||
|
||||
/-definition linear_ordered_comm_ring : algebra.linear_ordered_comm_ring ℝ :=
|
||||
⦃ algebra.linear_ordered_comm_ring, ordered_ring, comm_ring,
|
||||
zero_lt_one := zero_lt_one,
|
||||
le_total := le_or_ge,
|
||||
le_iff_lt_or_eq := le_iff_lt_or_eq
|
||||
⦄-/
|
||||
|
||||
|
||||
end real
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue