feat(library/rat/basic.lean): add reduce for rat, and num and denom
This commit is contained in:
Jeremy Avigad
Leonardo de Moura
parent
0b335230d7
commit
658c5a2c49
8 changed files with 253 additions and 155 deletions
|
|
@ -133,7 +133,7 @@ dvd_gcd (dvd.trans !gcd_dvd_left !dvd_mul_left) !gcd_dvd_right
|
|||
theorem gcd_dvd_gcd_mul_right (a b c : ℤ) : gcd a b ∣ gcd (a * c) b :=
|
||||
!mul.comm ▸ !gcd_dvd_gcd_mul_left
|
||||
|
||||
theorem div_gcd_eq_div_gcd_of_nonneg {a₁ b₁ a₂ b₂ : ℤ} (H : a₁ * b₂ = b₁ * a₂)
|
||||
theorem div_gcd_eq_div_gcd_of_nonneg {a₁ b₁ a₂ b₂ : ℤ} (H : a₁ * b₂ = a₂ * b₁)
|
||||
(H1 : b₁ ≠ 0) (H2 : b₂ ≠ 0) (H3 : a₁ ≥ 0) (H4 : a₂ ≥ 0) :
|
||||
a₁ div (gcd a₁ b₁) = a₂ div (gcd a₂ b₂) :=
|
||||
begin
|
||||
|
|
@ -142,24 +142,24 @@ begin
|
|||
intro H', apply H1, apply eq_zero_of_gcd_eq_zero_right H',
|
||||
intro H', apply H2, apply eq_zero_of_gcd_eq_zero_right H',
|
||||
rewrite [-abs_of_nonneg H3 at {1}, -abs_of_nonneg H4 at {2}],
|
||||
rewrite [-gcd_mul_left, -gcd_mul_right, H]
|
||||
rewrite [-gcd_mul_left, -gcd_mul_right, H, mul.comm b₁]
|
||||
end
|
||||
|
||||
theorem div_gcd_eq_div_gcd {a₁ b₁ a₂ b₂ : ℤ} (H : a₁ * b₂ = b₁ * a₂) (H1 : b₁ > 0) (H2 : b₂ > 0) :
|
||||
theorem div_gcd_eq_div_gcd {a₁ b₁ a₂ b₂ : ℤ} (H : a₁ * b₂ = a₂ * b₁) (H1 : b₁ > 0) (H2 : b₂ > 0) :
|
||||
a₁ div (gcd a₁ b₁) = a₂ div (gcd a₂ b₂) :=
|
||||
or.elim (le_or_gt 0 a₁)
|
||||
(assume H3 : a₁ ≥ 0,
|
||||
have H4 : b₁ * a₂ ≥ 0, by rewrite -H; apply mul_nonneg H3 (le_of_lt H2),
|
||||
have H5 : a₂ ≥ 0, from nonneg_of_mul_nonneg_left H4 H1,
|
||||
have H4 : a₂ * b₁ ≥ 0, by rewrite -H; apply mul_nonneg H3 (le_of_lt H2),
|
||||
have H5 : a₂ ≥ 0, from nonneg_of_mul_nonneg_right H4 H1,
|
||||
div_gcd_eq_div_gcd_of_nonneg H (ne_of_gt H1) (ne_of_gt H2) H3 H5)
|
||||
(assume H3 : a₁ < 0,
|
||||
have H4 : b₁ * a₂ < 0, by rewrite -H; apply mul_neg_of_neg_of_pos H3 H2,
|
||||
assert H5 : a₂ < 0, from neg_of_mul_neg_left H4 (le_of_lt H1),
|
||||
have H4 : a₂ * b₁ < 0, by rewrite -H; apply mul_neg_of_neg_of_pos H3 H2,
|
||||
assert H5 : a₂ < 0, from neg_of_mul_neg_right H4 (le_of_lt H1),
|
||||
assert H6 : abs a₁ div (gcd (abs a₁) (abs b₁)) = abs a₂ div (gcd (abs a₂) (abs b₂)),
|
||||
begin
|
||||
apply div_gcd_eq_div_gcd_of_nonneg,
|
||||
rewrite [abs_of_pos H1, abs_of_pos H2, abs_of_neg H3, abs_of_neg H5],
|
||||
rewrite [-neg_mul_eq_mul_neg, -neg_mul_eq_neg_mul, H],
|
||||
rewrite [-*neg_mul_eq_neg_mul, H],
|
||||
apply ne_of_gt (abs_pos_of_pos H1),
|
||||
apply ne_of_gt (abs_pos_of_pos H2),
|
||||
repeat (apply abs_nonneg)
|
||||
|
|
|
|||
|
|
@ -34,7 +34,6 @@ int.cases_on a (take n H, exists.intro n rfl) (take n' H, false.elim H)
|
|||
private theorem nonneg_or_nonneg_neg (a : ℤ) : nonneg a ∨ nonneg (-a) :=
|
||||
int.cases_on a (take n, or.inl trivial) (take n, or.inr trivial)
|
||||
|
||||
|
||||
theorem le.intro {a b : ℤ} {n : ℕ} (H : a + n = b) : a ≤ b :=
|
||||
have H1 : b - a = n, from (eq_add_neg_of_add_eq (!add.comm ▸ H))⁻¹,
|
||||
have H2 : nonneg n, from true.intro,
|
||||
|
|
@ -299,6 +298,9 @@ theorem of_nat_nonneg (n : ℕ) : 0 ≤ of_nat n := trivial
|
|||
theorem of_nat_pos {n : ℕ} (Hpos : #nat n > 0) : of_nat n > 0 :=
|
||||
of_nat_lt_of_nat_of_lt Hpos
|
||||
|
||||
theorem of_nat_succ_pos (n : nat) : of_nat (nat.succ n) > 0 :=
|
||||
of_nat_pos !nat.succ_pos
|
||||
|
||||
theorem exists_eq_of_nat {a : ℤ} (H : 0 ≤ a) : ∃n : ℕ, a = of_nat n :=
|
||||
obtain (n : ℕ) (H1 : 0 + of_nat n = a), from le.elim H,
|
||||
exists.intro n (!zero_add ▸ (H1⁻¹))
|
||||
|
|
|
|||
|
|
@ -74,9 +74,6 @@ setoid.mk equiv equiv.is_equivalence
|
|||
|
||||
/- field operations -/
|
||||
|
||||
theorem of_nat_succ_pos (n : nat) : of_nat (nat.succ n) > 0 :=
|
||||
of_nat_pos !nat.succ_pos
|
||||
|
||||
definition of_int (i : int) : prerat := prerat.mk i 1 !of_nat_succ_pos
|
||||
|
||||
definition zero : prerat := of_int 0
|
||||
|
|
@ -104,6 +101,9 @@ theorem of_int_mul (a b : ℤ) : of_int (#int a * b) ≡ mul (of_int a) (of_int
|
|||
theorem of_int_neg (a : ℤ) : of_int (#int -a) ≡ neg (of_int a) :=
|
||||
!equiv.refl
|
||||
|
||||
theorem of_int.inj {a b : ℤ} : of_int a ≡ of_int b → a = b :=
|
||||
by rewrite [↑of_int, ↑equiv, *mul_one]; intros; assumption
|
||||
|
||||
definition inv : prerat → prerat
|
||||
| inv (prerat.mk nat.zero d dp) := zero
|
||||
| inv (prerat.mk (nat.succ n) d dp) := prerat.mk d (nat.succ n) !of_nat_succ_pos
|
||||
|
|
@ -261,6 +261,64 @@ begin
|
|||
exact zero_ne_one
|
||||
end
|
||||
|
||||
theorem mul_denom_equiv (a : prerat) : mul a (of_int (denom a)) ≡ of_int (num a) :=
|
||||
by esimp [mul, of_int, equiv]; rewrite [*int.mul_one]
|
||||
|
||||
/- Reducing a fraction to lowest terms. Needed to choose a canonical representative of rat, and
|
||||
define numerator and denominator. -/
|
||||
|
||||
definition reduce : prerat → prerat
|
||||
| (mk an ad adpos) :=
|
||||
have pos : ad div gcd an ad > 0, from div_pos_of_pos_of_dvd adpos !gcd_nonneg !gcd_dvd_right,
|
||||
if an = 0 then prerat.zero
|
||||
else mk (an div gcd an ad) (ad div gcd an ad) pos
|
||||
|
||||
protected theorem eq {a b : prerat} (Hn : num a = num b) (Hd : denom a = denom b) : a = b :=
|
||||
begin
|
||||
cases a with [an, ad, adpos],
|
||||
cases b with [bn, bd, bdpos],
|
||||
generalize adpos, generalize bdpos,
|
||||
esimp at *,
|
||||
rewrite [Hn, Hd],
|
||||
intros, apply rfl
|
||||
end
|
||||
|
||||
theorem reduce_equiv : ∀ a : prerat, reduce a ≡ a
|
||||
| (mk an ad adpos) :=
|
||||
decidable.by_cases
|
||||
(assume anz : an = 0,
|
||||
by krewrite [↑reduce, if_pos anz, ↑equiv, anz, *zero_mul])
|
||||
(assume annz : an ≠ 0,
|
||||
by rewrite [↑reduce, if_neg annz, ↑equiv, int.mul.comm, -!mul_div_assoc !gcd_dvd_left,
|
||||
-!mul_div_assoc !gcd_dvd_right, int.mul.comm])
|
||||
|
||||
theorem reduce_eq_reduce : ∀{a b : prerat}, a ≡ b → reduce a = reduce b
|
||||
| (mk an ad adpos) (mk bn bd bdpos) :=
|
||||
assume H : an * bd = bn * ad,
|
||||
decidable.by_cases
|
||||
(assume anz : an = 0,
|
||||
have H' : bn * ad = 0, by rewrite [-H, anz, zero_mul],
|
||||
assert bnz : bn = 0, from or_resolve_left (eq_zero_or_eq_zero_of_mul_eq_zero H') (ne_of_gt adpos),
|
||||
by rewrite [↑reduce, if_pos anz, if_pos bnz])
|
||||
(assume annz : an ≠ 0,
|
||||
assert bnnz : bn ≠ 0, from
|
||||
assume bnz,
|
||||
have H' : an * bd = 0, by rewrite [H, bnz, zero_mul],
|
||||
have anz : an = 0, from or_resolve_left (eq_zero_or_eq_zero_of_mul_eq_zero H') (ne_of_gt bdpos),
|
||||
show false, from annz anz,
|
||||
begin
|
||||
rewrite [↑reduce, if_neg annz, if_neg bnnz],
|
||||
apply prerat.eq,
|
||||
{apply div_gcd_eq_div_gcd H adpos bdpos},
|
||||
{esimp, rewrite [gcd.comm, gcd.comm bn],
|
||||
apply div_gcd_eq_div_gcd_of_nonneg,
|
||||
rewrite [int.mul.comm, -H, int.mul.comm],
|
||||
apply annz,
|
||||
apply bnnz,
|
||||
apply le_of_lt adpos,
|
||||
apply le_of_lt bdpos},
|
||||
end)
|
||||
|
||||
end prerat
|
||||
|
||||
/-
|
||||
|
|
@ -276,46 +334,49 @@ namespace rat
|
|||
|
||||
/- operations -/
|
||||
|
||||
-- these coercions do not work: rat is not an inductive type
|
||||
definition of_int [coercion] (i : ℤ) : ℚ := ⟦prerat.of_int i⟧
|
||||
definition of_nat [coercion] (n : ℕ) : ℚ := ⟦prerat.of_int n⟧
|
||||
definition of_num [coercion] [reducible] (n : num) : ℚ := of_int (int.of_num n)
|
||||
|
||||
definition add : ℚ → ℚ → ℚ :=
|
||||
quot.lift₂
|
||||
(λa b : prerat, ⟦prerat.add a b⟧)
|
||||
(λ a b : prerat, ⟦prerat.add a b⟧)
|
||||
(take a1 a2 b1 b2, assume H1 H2, quot.sound (prerat.add_equiv_add H1 H2))
|
||||
|
||||
definition mul : ℚ → ℚ → ℚ :=
|
||||
quot.lift₂
|
||||
(λa b : prerat, ⟦prerat.mul a b⟧)
|
||||
(λ a b : prerat, ⟦prerat.mul a b⟧)
|
||||
(take a1 a2 b1 b2, assume H1 H2, quot.sound (prerat.mul_equiv_mul H1 H2))
|
||||
|
||||
definition neg : ℚ → ℚ :=
|
||||
quot.lift
|
||||
(λa : prerat, ⟦prerat.neg a⟧)
|
||||
(λ a : prerat, ⟦prerat.neg a⟧)
|
||||
(take a1 a2, assume H, quot.sound (prerat.neg_equiv_neg H))
|
||||
|
||||
definition inv : ℚ → ℚ :=
|
||||
quot.lift
|
||||
(λa : prerat, ⟦prerat.inv a⟧)
|
||||
(λ a : prerat, ⟦prerat.inv a⟧)
|
||||
(take a1 a2, assume H, quot.sound (prerat.inv_equiv_inv H))
|
||||
|
||||
definition zero := ⟦prerat.zero⟧
|
||||
definition one := ⟦prerat.one⟧
|
||||
definition reduce : ℚ → prerat :=
|
||||
quot.lift
|
||||
(λ a : prerat, prerat.reduce a)
|
||||
@prerat.reduce_eq_reduce
|
||||
|
||||
infix `+` := rat.add
|
||||
infix `*` := rat.mul
|
||||
prefix `-` := rat.neg
|
||||
postfix `⁻¹` := rat.inv
|
||||
definition num (a : ℚ) : ℤ := prerat.num (reduce a)
|
||||
definition denom (a : ℚ) : ℤ := prerat.denom (reduce a)
|
||||
|
||||
theorem denom_pos (a : ℚ): denom a > 0 :=
|
||||
prerat.denom_pos (reduce a)
|
||||
|
||||
infix + := rat.add
|
||||
infix * := rat.mul
|
||||
prefix - := rat.neg
|
||||
|
||||
definition sub [reducible] (a b : rat) : rat := a + (-b)
|
||||
|
||||
infix `-` := rat.sub
|
||||
|
||||
-- TODO: this is a workaround, since the coercions from numerals do not work
|
||||
notation 0 := zero
|
||||
notation 1 := one
|
||||
postfix ⁻¹ := rat.inv
|
||||
infix - := rat.sub
|
||||
|
||||
/- properties -/
|
||||
|
||||
|
|
@ -333,6 +394,9 @@ calc
|
|||
of_int (#int a - b) = of_int a + of_int (#int -b) : of_int_add
|
||||
... = of_int a - of_int b : {of_int_neg b}
|
||||
|
||||
theorem of_int.inj {a b : ℤ} (H : of_int a = of_int b) : a = b :=
|
||||
sorry
|
||||
|
||||
theorem of_nat_eq (a : ℕ) : of_nat a = of_int (int.of_nat a) := rfl
|
||||
|
||||
theorem of_nat_add (a b : ℕ) : of_nat (#nat a + b) = of_nat a + of_nat b :=
|
||||
|
|
@ -384,7 +448,7 @@ quot.induction_on a
|
|||
theorem inv_mul_cancel {a : ℚ} (H : a ≠ 0) : a⁻¹ * a = 1 :=
|
||||
!mul.comm ▸ mul_inv_cancel H
|
||||
|
||||
theorem zero_ne_one : (#rat 0 ≠ 1) :=
|
||||
theorem zero_ne_one : (0 : ℚ) ≠ 1 :=
|
||||
assume H, prerat.zero_not_equiv_one (quot.exact H)
|
||||
|
||||
definition has_decidable_eq [instance] : decidable_eq ℚ :=
|
||||
|
|
@ -397,6 +461,13 @@ take a b, quot.rec_on_subsingleton₂ a b
|
|||
theorem inv_zero : inv 0 = 0 :=
|
||||
quot.sound (prerat.inv_zero' ▸ !prerat.equiv.refl)
|
||||
|
||||
theorem quot_reduce (a : ℚ) : ⟦reduce a⟧ = a :=
|
||||
quot.induction_on a (take u, quot.sound !prerat.reduce_equiv)
|
||||
|
||||
theorem mul_denom (a : ℚ) : a * denom a = num a :=
|
||||
have H : ⟦reduce a⟧ * of_int (denom a) = of_int (num a), from quot.sound (!prerat.mul_denom_equiv),
|
||||
quot_reduce a ▸ H
|
||||
|
||||
section migrate_algebra
|
||||
open [classes] algebra
|
||||
|
||||
|
|
@ -433,4 +504,21 @@ section migrate_algebra
|
|||
replacing sub → rat.sub, divide → divide, dvd → dvd
|
||||
|
||||
end migrate_algebra
|
||||
|
||||
theorem eq_num_div_denom (a : ℚ) : a = num a / denom a :=
|
||||
have H : of_int (denom a) ≠ 0, from assume H', ne_of_gt (denom_pos a) (of_int.inj H'),
|
||||
iff.mp' (eq_div_iff_mul_eq H) (mul_denom a)
|
||||
|
||||
theorem of_nat_div {a b : ℤ} (H : b ∣ a) : of_int (a div b) = of_int a / of_int b :=
|
||||
decidable.by_cases
|
||||
(assume bz : b = 0,
|
||||
by rewrite [bz, div_zero, int.div_zero])
|
||||
(assume bnz : b ≠ 0,
|
||||
have bnz' : of_int b ≠ 0, from assume oibz, bnz (of_int.inj oibz),
|
||||
have H' : of_int (a div b) * of_int b = of_int a, from
|
||||
int.dvd.elim H
|
||||
(take c, assume Hc : a = b * c,
|
||||
by rewrite [Hc, !int.mul_div_cancel_left bnz, mul.comm]),
|
||||
iff.mp' (eq_div_iff_mul_eq bnz') H')
|
||||
|
||||
end rat
|
||||
|
|
|
|||
|
|
@ -10,7 +10,7 @@ import data.int algebra.ordered_field .basic
|
|||
open quot eq.ops
|
||||
|
||||
/- the ordering on representations -/
|
||||
|
||||
|
||||
namespace prerat
|
||||
section int_notation
|
||||
open int
|
||||
|
|
@ -126,7 +126,7 @@ private theorem pos_of_nonneg_of_ne_zero : nonneg a → ¬ a = 0 → pos a :=
|
|||
quot.induction_on a
|
||||
(take u,
|
||||
assume H1 : nonneg ⟦u⟧,
|
||||
assume H2 : ⟦u⟧ ≠ 0,
|
||||
assume H2 : ⟦u⟧ ≠ (rat.of_num 0),
|
||||
have H3 : ¬ (prerat.equiv u prerat.zero), from assume H, H2 (quot.sound H),
|
||||
prerat.pos_of_nonneg_of_ne_zero H1 H3)
|
||||
|
||||
|
|
@ -204,7 +204,7 @@ or.elim (nonneg_total (b - a))
|
|||
(assume H, or.inl H)
|
||||
(assume H, or.inr (!neg_sub ▸ H))
|
||||
|
||||
theorem le.by_cases {P : Prop} (a b : ℚ) (H : a ≤ b → P) (H2 : b ≤ a → P) : P :=
|
||||
theorem le.by_cases {P : Prop} (a b : ℚ) (H : a ≤ b → P) (H2 : b ≤ a → P) : P :=
|
||||
or.elim (!rat.le.total) H H2
|
||||
|
||||
theorem lt_iff_le_and_ne (a b : ℚ) : a < b ↔ a ≤ b ∧ a ≠ b :=
|
||||
|
|
@ -229,16 +229,16 @@ iff.intro
|
|||
(assume H1 : a < b, and.left (iff.mp !lt_iff_le_and_ne H1))
|
||||
(assume H1 : a = b, H1 ▸ !le.refl))
|
||||
|
||||
theorem add_le_add_left (H : a ≤ b) (c: ℚ) : c + a ≤ c + b :=
|
||||
theorem add_le_add_left (H : a ≤ b) (c : ℚ) : c + a ≤ c + b :=
|
||||
have H1 : c + b - (c + a) = b - a,
|
||||
by rewrite [↑sub, neg_add, -add.assoc, add.comm c, add_neg_cancel_right],
|
||||
show nonneg (c + b - (c + a)), from H1⁻¹ ▸ H
|
||||
|
||||
theorem mul_nonneg (H1 : a ≥ 0) (H2 : b ≥ 0) : a * b ≥ 0 :=
|
||||
theorem mul_nonneg (H1 : a ≥ (0 : ℚ)) (H2 : b ≥ (0 : ℚ)) : a * b ≥ (0 : ℚ) :=
|
||||
have H : nonneg (a * b), from nonneg_mul (!sub_zero ▸ H1) (!sub_zero ▸ H2),
|
||||
!sub_zero⁻¹ ▸ H
|
||||
|
||||
theorem mul_pos (H1 : a > 0) (H2 : b > 0) : a * b > 0 :=
|
||||
theorem mul_pos (H1 : a > (0 : ℚ)) (H2 : b > (0 : ℚ)) : a * b > (0 : ℚ) :=
|
||||
have H : pos (a * b), from pos_mul (!sub_zero ▸ H1) (!sub_zero ▸ H2),
|
||||
!sub_zero⁻¹ ▸ H
|
||||
|
||||
|
|
@ -247,17 +247,17 @@ take a b, decidable_pos (b - a)
|
|||
|
||||
theorem le_of_lt (H : a < b) : a ≤ b := iff.mp' !le_iff_lt_or_eq (or.inl H)
|
||||
|
||||
theorem lt_irrefl (a : ℚ) : ¬ a < a :=
|
||||
theorem lt_irrefl (a : ℚ) : ¬ a < a :=
|
||||
take Ha,
|
||||
let Hand := (iff.mp !lt_iff_le_and_ne) Ha in
|
||||
let Hand := (iff.mp !lt_iff_le_and_ne) Ha in
|
||||
(and.right Hand) rfl
|
||||
|
||||
theorem not_le_of_gt (H : a < b) : ¬ b ≤ a :=
|
||||
assume Hba,
|
||||
let Heq := le.antisymm (le_of_lt H) Hba in
|
||||
!lt_irrefl (Heq ▸ H)
|
||||
let Heq := le.antisymm (le_of_lt H) Hba in
|
||||
!lt_irrefl (Heq ▸ H)
|
||||
|
||||
theorem lt_of_lt_of_le (Hab : a < b) (Hbc : b ≤ c) : a < c :=
|
||||
theorem lt_of_lt_of_le (Hab : a < b) (Hbc : b ≤ c) : a < c :=
|
||||
let Hab' := le_of_lt Hab in
|
||||
let Hac := le.trans Hab' Hbc in
|
||||
(iff.mp' !lt_iff_le_and_ne) (and.intro Hac
|
||||
|
|
@ -275,8 +275,8 @@ theorem zero_lt_one : (0 : ℚ) < 1 := trivial
|
|||
-- apply sorry
|
||||
-- end
|
||||
|
||||
theorem add_lt_add_left (H : a < b) (c : ℚ) : c + a < c + b :=
|
||||
let H' := le_of_lt H in
|
||||
theorem add_lt_add_left (H : a < b) (c : ℚ) : c + a < c + b :=
|
||||
let H' := le_of_lt H in
|
||||
(iff.mp' (lt_iff_le_and_ne _ _)) (and.intro (add_le_add_left H' _)
|
||||
(take Heq, let Heq' := add_left_cancel Heq in
|
||||
!lt_irrefl (Heq' ▸ H)))
|
||||
|
|
|
|||
|
|
@ -14,6 +14,8 @@ To do:
|
|||
import data.nat data.rat.order
|
||||
open nat eq eq.ops
|
||||
open -[coercions] rat
|
||||
local notation 0 := rat.of_num 0
|
||||
local notation 1 := rat.of_num 1
|
||||
----------------------------------------------------------------------------------------------------
|
||||
|
||||
-----------------------------------------------
|
||||
|
|
@ -730,7 +732,7 @@ theorem neg_s_cancel (s : seq) (H : regular s) : sadd s (sneg s) ≡ zero :=
|
|||
apply zero_is_reg
|
||||
end
|
||||
|
||||
theorem add_well_defined {s t u v : seq} (Hs : regular s) (Ht : regular t) (Hu : regular u)
|
||||
theorem add_well_defined {s t u v : seq} (Hs : regular s) (Ht : regular t) (Hu : regular u)
|
||||
(Hv : regular v) (Esu : s ≡ u) (Etv : t ≡ v) : sadd s t ≡ sadd u v :=
|
||||
begin
|
||||
rewrite [↑sadd, ↑equiv at *],
|
||||
|
|
@ -1070,7 +1072,7 @@ theorem zero_nequiv_one : ¬ zero ≡ one :=
|
|||
pone⁻¹ = 1 : by rewrite -pone_inv
|
||||
... = abs 1 : abs_of_pos zero_lt_one
|
||||
... ≤ 2⁻¹ : H,
|
||||
let H'' := ge_of_inv_le H',
|
||||
let H'' := ge_of_inv_le H',
|
||||
apply absurd (one_lt_two) (pnat.not_lt_of_le (pnat.le_of_lt H''))
|
||||
end
|
||||
|
||||
|
|
@ -1155,7 +1157,7 @@ theorem r_distrib (s t u : reg_seq) : requiv (s * (t + u)) (s * t + s * u) :=
|
|||
s_distrib (reg_seq.is_reg s) (reg_seq.is_reg t) (reg_seq.is_reg u)
|
||||
|
||||
theorem r_zero_nequiv_one : ¬ requiv r_zero r_one :=
|
||||
zero_nequiv_one
|
||||
zero_nequiv_one
|
||||
|
||||
----------------------------------------------
|
||||
-- take quotients to get ℝ and show it's a comm ring
|
||||
|
|
@ -1219,7 +1221,7 @@ theorem distrib (x y z : ℝ) : x * (y + z) = x * y + x * z :=
|
|||
theorem distrib_l (x y z : ℝ) : (x + y) * z = x * z + y * z :=
|
||||
by rewrite [mul_comm, distrib, {x * _}mul_comm, {y * _}mul_comm] -- this shouldn't be necessary
|
||||
|
||||
theorem zero_ne_one : ¬ zero = one :=
|
||||
theorem zero_ne_one : ¬ zero = one :=
|
||||
take H : zero = one,
|
||||
absurd (quot.exact H) (r_zero_nequiv_one)
|
||||
|
||||
|
|
|
|||
|
|
@ -10,9 +10,11 @@ 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 logic.axioms.classical
|
||||
open -[coercions] rat
|
||||
open -[coercions] rat
|
||||
local notation 0 := rat.of_num 0
|
||||
local notation 1 := rat.of_num 1
|
||||
open -[coercions] nat
|
||||
open algebra
|
||||
open eq.ops
|
||||
|
|
@ -36,7 +38,7 @@ theorem const_reg (a : ℚ) : regular (const a) :=
|
|||
|
||||
definition r_const (a : ℚ) : reg_seq := reg_seq.mk (const a) (const_reg a)
|
||||
|
||||
theorem rat_approx_l1 {s : seq} (H : regular s) :
|
||||
theorem rat_approx_l1 {s : seq} (H : regular s) :
|
||||
∀ n : ℕ+, ∃ q : ℚ, ∃ N : ℕ+, ∀ m : ℕ+, m ≥ N → abs (s m - q) ≤ n⁻¹ :=
|
||||
begin
|
||||
intro n,
|
||||
|
|
@ -50,8 +52,8 @@ theorem rat_approx_l1 {s : seq} (H : regular s) :
|
|||
apply inv_ge_of_le Hm
|
||||
end
|
||||
|
||||
theorem rat_approx {s : seq} (H : regular s) :
|
||||
∀ n : ℕ+, ∃ q : ℚ, s_le (s_abs (sadd s (sneg (const q)))) (const n⁻¹) :=
|
||||
theorem rat_approx {s : seq} (H : regular s) :
|
||||
∀ n : ℕ+, ∃ q : ℚ, s_le (s_abs (sadd s (sneg (const q)))) (const n⁻¹) :=
|
||||
begin
|
||||
intro m,
|
||||
rewrite ↑s_le,
|
||||
|
|
@ -81,11 +83,11 @@ theorem rat_approx {s : seq} (H : regular s) :
|
|||
apply inv_pos
|
||||
end
|
||||
|
||||
definition r_abs (s : reg_seq) : reg_seq :=
|
||||
definition r_abs (s : reg_seq) : reg_seq :=
|
||||
reg_seq.mk (s_abs (reg_seq.sq s)) (abs_reg_of_reg (reg_seq.is_reg s))
|
||||
|
||||
theorem abs_well_defined {s t : seq} (Hs : regular s) (Ht : regular t) (Heq : s ≡ t) :
|
||||
s_abs s ≡ s_abs t :=
|
||||
s_abs s ≡ s_abs t :=
|
||||
begin
|
||||
rewrite [↑equiv at *],
|
||||
intro n,
|
||||
|
|
@ -95,11 +97,11 @@ theorem abs_well_defined {s t : seq} (Hs : regular s) (Ht : regular t) (Heq : s
|
|||
apply Heq
|
||||
end
|
||||
|
||||
theorem r_abs_well_defined {s t : reg_seq} (H : requiv s t) : requiv (r_abs s) (r_abs t) :=
|
||||
theorem r_abs_well_defined {s t : reg_seq} (H : requiv s t) : requiv (r_abs s) (r_abs t) :=
|
||||
abs_well_defined (reg_seq.is_reg s) (reg_seq.is_reg t) H
|
||||
|
||||
theorem r_rat_approx (s : reg_seq) :
|
||||
∀ n : ℕ+, ∃ q : ℚ, r_le (r_abs (radd s (rneg (r_const q)))) (r_const n⁻¹) :=
|
||||
∀ 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⁻¹) :=
|
||||
|
|
@ -123,7 +125,7 @@ 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) :=
|
||||
theorem add_consts (a b : ℚ) : sadd (const a) (const b) ≡ const (a + b) :=
|
||||
begin
|
||||
rewrite [↑sadd, ↑const],
|
||||
apply equiv.refl
|
||||
|
|
@ -158,7 +160,7 @@ theorem r_le_of_const_le_const {a b : ℚ} (H : r_le (r_const a) (r_const 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
|
||||
begin
|
||||
apply eq_of_bdd,
|
||||
apply abs_reg_of_reg Hs,
|
||||
apply Hs,
|
||||
|
|
@ -174,7 +176,7 @@ theorem equiv_abs_of_ge_zero {s : seq} (Hs : regular s) (Hz : s_le zero s) : s_a
|
|||
apply inv_pos,
|
||||
intro Hneg,
|
||||
let Hneg' := lt_of_not_ge Hneg,
|
||||
have Hsn : -s n - s n > 0, from add_pos (neg_pos_of_neg Hneg') (neg_pos_of_neg Hneg'),
|
||||
have Hsn : -s n - s n > 0, from add_pos (neg_pos_of_neg Hneg') (neg_pos_of_neg Hneg'),
|
||||
rewrite [rat.abs_of_neg Hneg', rat.abs_of_pos Hsn],
|
||||
apply rat.le.trans,
|
||||
apply rat.add_le_add,
|
||||
|
|
@ -220,13 +222,13 @@ theorem equiv_neg_abs_of_le_zero {s : seq} (Hs : regular s) (Hz : s_le s zero) :
|
|||
intro Hneg,
|
||||
let Hneg' := lt_of_not_ge Hneg,
|
||||
rewrite [rat.abs_of_neg Hneg', ↑sneg, rat.sub_neg_eq_add, rat.neg_add_eq_sub, rat.sub_self,
|
||||
abs_zero],
|
||||
abs_zero],
|
||||
apply rat.le_of_lt,
|
||||
apply inv_pos
|
||||
end
|
||||
|
||||
theorem r_equiv_abs_of_ge_zero {s : reg_seq} (Hz : r_le r_zero s) : requiv (r_abs s) s :=
|
||||
equiv_abs_of_ge_zero (reg_seq.is_reg s) Hz
|
||||
equiv_abs_of_ge_zero (reg_seq.is_reg s) Hz
|
||||
|
||||
theorem r_equiv_neg_abs_of_le_zero {s : reg_seq} (Hz : r_le s r_zero) : requiv (r_abs s) (-s) :=
|
||||
equiv_neg_abs_of_le_zero (reg_seq.is_reg s) Hz
|
||||
|
|
@ -241,23 +243,23 @@ theorem rewrite_helper10 (a b c d : ℝ) : c - d = (c - a) + (a - b) + (b - d) :
|
|||
|
||||
definition rep (x : ℝ) : reg_seq := some (quot.exists_rep x)
|
||||
|
||||
definition const (a : ℚ) : ℝ := quot.mk (s.r_const a)
|
||||
definition const (a : ℚ) : ℝ := quot.mk (s.r_const a)
|
||||
|
||||
theorem add_consts (a b : ℚ) : const a + const b = const (a + b) :=
|
||||
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⁻¹) :=
|
||||
theorem add_half_const (n : ℕ+) : const (2 * n)⁻¹ + const (2 * n)⁻¹ = const (n⁻¹) :=
|
||||
by rewrite [add_consts, padd_halves]
|
||||
|
||||
theorem const_le_const_of_le (a b : ℚ) : a ≤ b → const a ≤ const b :=
|
||||
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 :=
|
||||
theorem le_of_const_le_const (a b : ℚ) : const a ≤ const b → a ≤ b :=
|
||||
s.r_le_of_const_le_const
|
||||
|
||||
definition re_abs (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))
|
||||
|
||||
theorem r_abs_nonneg {x : ℝ} : 0 ≤ x → re_abs x = x :=
|
||||
|
|
@ -293,7 +295,7 @@ theorem rat_approx (x : ℝ) : ∀ n : ℕ+, ∃ q : ℚ, abs (x - const q) ≤
|
|||
|
||||
definition approx (x : ℝ) (n : ℕ+) := some (rat_approx x n)
|
||||
|
||||
theorem approx_spec (x : ℝ) (n : ℕ+) : abs (x - (const (approx x n))) ≤ const n⁻¹ :=
|
||||
theorem approx_spec (x : ℝ) (n : ℕ+) : abs (x - (const (approx x n))) ≤ const n⁻¹ :=
|
||||
some_spec (rat_approx x n)
|
||||
|
||||
theorem approx_spec' (x : ℝ) (n : ℕ+) : abs ((const (approx x n)) - x) ≤ const n⁻¹ :=
|
||||
|
|
@ -310,7 +312,7 @@ definition cauchy (X : r_seq) (M : ℕ+ → ℕ+) :=
|
|||
theorem cauchy_of_converges_to {X : r_seq} {a : ℝ} {N : ℕ+ → ℕ+} (Hc : converges_to X a N) :
|
||||
cauchy X (λ k, N (2 * k)) :=
|
||||
begin
|
||||
intro k m n Hm Hn,
|
||||
intro k m n Hm Hn,
|
||||
rewrite (rewrite_helper9 a),
|
||||
apply algebra.le.trans,
|
||||
apply algebra.abs_add_le_abs_add_abs,
|
||||
|
|
@ -334,13 +336,13 @@ theorem Nb_spec_left (M : ℕ+ → ℕ+) (k : ℕ+) : 3 * k ≤ Nb M k := !max_l
|
|||
definition lim_seq {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) : seq :=
|
||||
λ k, approx (X (Nb M k)) (2 * k)
|
||||
|
||||
theorem lim_seq_reg_helper {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) {m n : ℕ+}
|
||||
theorem lim_seq_reg_helper {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) {m n : ℕ+}
|
||||
(Hmn : M (2 * n) ≤M (2 * m)) :
|
||||
abs (const (lim_seq Hc m) - X (Nb M m)) + abs (X (Nb M m) - X (Nb M n)) + abs
|
||||
(X (Nb M n) - const (lim_seq Hc n)) ≤ const (m⁻¹ + n⁻¹) :=
|
||||
begin
|
||||
apply algebra.le.trans,
|
||||
apply algebra.add_le_add_three,
|
||||
apply algebra.add_le_add_three,
|
||||
apply approx_spec',
|
||||
rotate 1,
|
||||
apply approx_spec,
|
||||
|
|
@ -359,14 +361,14 @@ theorem lim_seq_reg_helper {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) {m
|
|||
apply pnat.mul_le_mul_left
|
||||
end
|
||||
|
||||
theorem lim_seq_reg {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) : regular (lim_seq Hc) :=
|
||||
theorem lim_seq_reg {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) : regular (lim_seq Hc) :=
|
||||
begin
|
||||
rewrite ↑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,
|
||||
apply algebra.abs_add_three,
|
||||
apply algebra.abs_add_three,
|
||||
let Hor := decidable.em (M (2 * m) ≥ M (2 * n)),
|
||||
apply or.elim Hor,
|
||||
intro Hor1,
|
||||
|
|
@ -378,7 +380,7 @@ theorem lim_seq_reg {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) : regular
|
|||
apply lim_seq_reg_helper Hc Hor2'
|
||||
end
|
||||
|
||||
theorem lim_seq_spec {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) (k : ℕ+) :
|
||||
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⁻¹) :=
|
||||
begin
|
||||
apply s.const_bound,
|
||||
|
|
@ -389,26 +391,26 @@ definition r_lim_seq {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) : reg_seq
|
|||
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 (((r_lim_seq Hc) + -s.r_const ((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) : ℝ :=
|
||||
quot.mk (r_lim_seq Hc)
|
||||
|
||||
theorem re_lim_spec {x : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy x M) (k : ℕ+) :
|
||||
theorem re_lim_spec {x : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy x M) (k : ℕ+) :
|
||||
re_abs ((lim Hc) - (const ((lim_seq Hc) k))) ≤ const k⁻¹ :=
|
||||
r_lim_seq_spec Hc k
|
||||
r_lim_seq_spec Hc k
|
||||
|
||||
theorem lim_spec' {x : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy x M) (k : ℕ+) :
|
||||
theorem lim_spec' {x : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy x M) (k : ℕ+) :
|
||||
abs ((lim Hc) - (const ((lim_seq Hc) k))) ≤ const k⁻¹ :=
|
||||
by rewrite -re_abs_is_abs; apply re_lim_spec
|
||||
|
||||
theorem lim_spec {x : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy x M) (k : ℕ+) :
|
||||
theorem lim_spec {x : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy x M) (k : ℕ+) :
|
||||
abs ((const ((lim_seq Hc) k)) - (lim Hc)) ≤ const (k)⁻¹ :=
|
||||
by rewrite algebra.abs_sub; apply lim_spec'
|
||||
|
||||
theorem converges_of_cauchy {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) :
|
||||
converges_to X (lim Hc) (Nb M) :=
|
||||
theorem converges_of_cauchy {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) :
|
||||
converges_to X (lim Hc) (Nb M) :=
|
||||
begin
|
||||
intro k n Hn,
|
||||
rewrite (rewrite_helper10 (X (Nb M n)) (const (lim_seq Hc n))),
|
||||
|
|
|
|||
|
|
@ -10,8 +10,10 @@ and excluded middle.
|
|||
-/
|
||||
|
||||
import data.real.basic data.real.order data.rat data.nat logic.axioms.classical
|
||||
open -[coercions] rat
|
||||
open -[coercions] rat
|
||||
open -[coercions] nat
|
||||
local notation 0 := rat.of_num 0
|
||||
local notation 1 := rat.of_num 1
|
||||
open eq.ops
|
||||
|
||||
|
||||
|
|
@ -22,7 +24,7 @@ namespace s
|
|||
-----------------------------
|
||||
-- helper lemmas
|
||||
|
||||
theorem abs_sub_square (a b : ℚ) : abs (a - b) * abs (a - b) = a * a + b * b - (1 + 1) * a * b :=
|
||||
theorem abs_sub_square (a b : ℚ) : abs (a - b) * abs (a - b) = a * a + b * b - (1 + 1) * a * b :=
|
||||
sorry --begin rewrite [abs_mul_self, *rat.left_distrib, *rat.right_distrib, *one_mul] end
|
||||
|
||||
theorem neg_add_rewrite {a b : ℚ} : a + -b = -(b + -a) := sorry
|
||||
|
|
@ -50,10 +52,10 @@ theorem pnat_cancel' (n m : ℕ+) : (n * n * m)⁻¹ * (pnat.to_rat n * pnat.to_
|
|||
theorem forall_of_not_exists {A : Type} {P : A → Prop} (H : ¬ ∃ a : A, P a) : ∀ a : A, ¬ P a :=
|
||||
take a, assume Ha, H (exists.intro a Ha)
|
||||
|
||||
theorem and_of_not_or {a b : Prop} (H : ¬ (a ∨ b)) : ¬ a ∧ ¬ b :=
|
||||
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 :=
|
||||
theorem ne_zero_of_abs_ne_zero {a : ℚ} (H : abs a ≠ 0) : a ≠ 0 :=
|
||||
assume Ha, H (Ha⁻¹ ▸ abs_zero)
|
||||
|
||||
-----------------------------
|
||||
|
|
@ -162,17 +164,17 @@ theorem s_inv_of_sep_gt_p {s : seq} (Hs : regular s) (Hsep : sep s zero) {n :
|
|||
apply dif_neg (pnat.not_lt_of_le Hn)
|
||||
end
|
||||
|
||||
theorem s_inv_of_pos_lt_p {s : seq} (Hs : regular s) (Hpos : pos s) {n : ℕ+}
|
||||
theorem s_inv_of_pos_lt_p {s : seq} (Hs : regular s) (Hpos : pos s) {n : ℕ+}
|
||||
(Hn : n < (pb Hs Hpos)) : s_inv Hs n = 1 / s ((pb Hs Hpos) * (pb Hs Hpos) * (pb Hs Hpos)) :=
|
||||
s_inv_of_sep_lt_p Hs (sep_zero_of_pos Hs Hpos) Hn
|
||||
|
||||
|
||||
theorem s_inv_of_pos_gt_p {s : seq} (Hs : regular s) (Hpos : pos s) {n : ℕ+}
|
||||
theorem s_inv_of_pos_gt_p {s : seq} (Hs : regular s) (Hpos : pos s) {n : ℕ+}
|
||||
(Hn : n ≥ (pb Hs Hpos)) : s_inv Hs n = 1 / s ((pb Hs Hpos) * (pb Hs Hpos) * n) :=
|
||||
s_inv_of_sep_gt_p Hs (sep_zero_of_pos Hs Hpos) Hn
|
||||
|
||||
theorem le_ps {s : seq} (Hs : regular s) (Hsep : sep s zero) (n : ℕ+) :
|
||||
abs (s_inv Hs n) ≤ (pnat.to_rat (ps Hs Hsep)) :=
|
||||
abs (s_inv Hs n) ≤ (pnat.to_rat (ps Hs Hsep)) :=
|
||||
if Hn : n < ps Hs Hsep then
|
||||
(begin
|
||||
rewrite [(s_inv_of_sep_lt_p Hs Hsep Hn), abs_one_div],
|
||||
|
|
@ -202,7 +204,7 @@ theorem s_inv_of_zero {s : seq} (Hs : regular s) (Hz : ¬ sep s zero) : s_inv Hs
|
|||
apply s_inv_of_zero' Hs Hz n
|
||||
end
|
||||
|
||||
theorem s_ne_zero_of_ge_p {s : seq} (Hs : regular s) (Hsep : sep s zero) {n : ℕ+}
|
||||
theorem s_ne_zero_of_ge_p {s : seq} (Hs : regular s) (Hsep : sep s zero) {n : ℕ+}
|
||||
(Hn : n ≥ (ps Hs Hsep)) : s n ≠ 0 :=
|
||||
begin
|
||||
let Hps := ps_spec Hs Hsep,
|
||||
|
|
@ -218,12 +220,12 @@ theorem reg_inv_reg {s : seq} (Hs : regular s) (Hsep : sep s zero) : regular (s_
|
|||
begin
|
||||
rewrite ↑regular,
|
||||
intros,
|
||||
have Hsp : s ((ps Hs Hsep) * (ps Hs Hsep) * (ps Hs Hsep)) ≠ 0, from
|
||||
have Hsp : s ((ps Hs Hsep) * (ps Hs Hsep) * (ps Hs Hsep)) ≠ 0, from
|
||||
s_ne_zero_of_ge_p Hs Hsep !pnat.mul_le_mul_left,
|
||||
have Hspn : s ((ps Hs Hsep) * (ps Hs Hsep) * n) ≠ 0, from
|
||||
have Hspn : s ((ps Hs Hsep) * (ps Hs Hsep) * n) ≠ 0, from
|
||||
s_ne_zero_of_ge_p Hs Hsep (show (ps Hs Hsep) * (ps Hs Hsep) * n ≥ ps Hs Hsep, by
|
||||
rewrite pnat_mul_assoc; apply pnat.mul_le_mul_right),
|
||||
have Hspm : s ((ps Hs Hsep) * (ps Hs Hsep) * m) ≠ 0, from
|
||||
have Hspm : s ((ps Hs Hsep) * (ps Hs Hsep) * m) ≠ 0, from
|
||||
s_ne_zero_of_ge_p Hs Hsep (show (ps Hs Hsep) * (ps Hs Hsep) * m ≥ ps Hs Hsep, by
|
||||
rewrite pnat_mul_assoc; apply pnat.mul_le_mul_right),
|
||||
apply @decidable.cases_on (m < (ps Hs Hsep)) _ _,
|
||||
|
|
@ -234,7 +236,7 @@ theorem reg_inv_reg {s : seq} (Hs : regular s) (Hsep : sep s zero) : regular (s_
|
|||
rewrite [sub_self, abs_zero],
|
||||
apply add_invs_nonneg,
|
||||
intro Hnlt,
|
||||
rewrite [(s_inv_of_sep_lt_p Hs Hsep Hmlt),
|
||||
rewrite [(s_inv_of_sep_lt_p Hs Hsep Hmlt),
|
||||
(s_inv_of_sep_gt_p Hs Hsep (pnat.le_of_not_lt Hnlt))],
|
||||
rewrite [(div_sub_div Hsp Hspn), div_eq_mul_one_div, *abs_mul, *mul_one, *one_mul],
|
||||
apply rat.le.trans,
|
||||
|
|
@ -327,7 +329,7 @@ theorem mul_inv {s : seq} (Hs : regular s) (Hsep : sep s zero) : smul s (s_inv H
|
|||
existsi max (ps Hs Hsep) j,
|
||||
intro n Hn,
|
||||
have Hnz : s_inv Hs ((K₂ s (s_inv Hs)) * 2 * n) ≠ 0, from s_inv_ne_zero Hs Hsep _,
|
||||
xrewrite [↑smul, ↑one, rat.mul.comm, -(mul_one_div_cancel Hnz),
|
||||
xrewrite [↑smul, ↑one, rat.mul.comm, -(mul_one_div_cancel Hnz),
|
||||
-rat.mul_sub_left_distrib, abs_mul],
|
||||
apply rat.le.trans,
|
||||
apply rat.mul_le_mul_of_nonneg_right,
|
||||
|
|
@ -343,8 +345,8 @@ theorem mul_inv {s : seq} (Hs : regular s) (Hsep : sep s zero) : smul s (s_inv H
|
|||
apply pnat.mul_le_mul_left
|
||||
end,
|
||||
have Hnz' : s (((ps Hs Hsep) * (ps Hs Hsep)) * ((K₂ s (s_inv Hs)) * 2 * n)) ≠ 0, from
|
||||
s_ne_zero_of_ge_p Hs Hsep
|
||||
(show ps Hs Hsep ≤ ((ps Hs Hsep) * (ps Hs Hsep)) * ((K₂ s (s_inv Hs)) * 2 * n),
|
||||
s_ne_zero_of_ge_p Hs Hsep
|
||||
(show ps Hs Hsep ≤ ((ps Hs Hsep) * (ps Hs Hsep)) * ((K₂ s (s_inv Hs)) * 2 * n),
|
||||
by rewrite *pnat_mul_assoc; apply pnat.mul_le_mul_right),
|
||||
xrewrite [(s_inv_of_sep_gt_p Hs Hsep Hp), (div_div Hnz')],
|
||||
apply rat.le.trans,
|
||||
|
|
@ -352,7 +354,7 @@ theorem mul_inv {s : seq} (Hs : regular s) (Hsep : sep s zero) : smul s (s_inv H
|
|||
apply Hs,
|
||||
apply le_of_lt,
|
||||
apply rat_of_pnat_is_pos,
|
||||
xrewrite [rat.mul.left_distrib, pnat_mul_comm ((ps Hs Hsep) * (ps Hs Hsep)), *pnat_mul_assoc,
|
||||
xrewrite [rat.mul.left_distrib, pnat_mul_comm ((ps Hs Hsep) * (ps Hs Hsep)), *pnat_mul_assoc,
|
||||
*(@pnat_div_helper (K₂ s (s_inv Hs))), -*rat.mul.assoc, *pnat.inv_cancel,
|
||||
*one_mul, -(padd_halves j)],
|
||||
apply rat.add_le_add,
|
||||
|
|
@ -464,13 +466,13 @@ theorem inv_well_defined {s t : seq} (Hs : regular s) (Ht : regular t) (Heq : s
|
|||
apply one_is_reg
|
||||
end)
|
||||
else
|
||||
(have H : s_inv Hs = zero, from funext (λ n, dif_neg Hsep),
|
||||
have Hsept : ¬ sep t zero, from
|
||||
(have H : s_inv Hs = zero, from funext (λ n, dif_neg Hsep),
|
||||
have Hsept : ¬ sep t zero, from
|
||||
assume H', Hsep (sep_of_equiv_sep Ht Hs (equiv.symm _ _ Heq) H'),
|
||||
have H' : s_inv Ht = zero, from funext (λ n, dif_neg Hsept),
|
||||
H'⁻¹ ▸ (H⁻¹ ▸ equiv.refl zero))
|
||||
|
||||
theorem s_neg_neg {s : seq} : sneg (sneg s) ≡ s :=
|
||||
theorem s_neg_neg {s : seq} : sneg (sneg s) ≡ s :=
|
||||
begin
|
||||
rewrite [↑equiv, ↑sneg],
|
||||
intro n,
|
||||
|
|
@ -479,7 +481,7 @@ theorem s_neg_neg {s : seq} : sneg (sneg s) ≡ s :=
|
|||
end
|
||||
|
||||
theorem s_neg_sub {s t : seq} (Hs : regular s) (Ht : regular t) :
|
||||
sneg (sadd s (sneg t)) ≡ sadd t (sneg s) :=
|
||||
sneg (sadd s (sneg t)) ≡ sadd t (sneg s) :=
|
||||
begin
|
||||
apply equiv.trans,
|
||||
rotate 3,
|
||||
|
|
@ -526,7 +528,7 @@ theorem s_le_total {s t : seq} (Hs : regular s) (Ht : regular t) : s_le s t ∨
|
|||
repeat (assumption | apply reg_add_reg | apply reg_neg_reg)
|
||||
end
|
||||
|
||||
theorem s_le_of_not_lt {s t : seq} (Hle : ¬ s_lt s t) : s_le t s :=
|
||||
theorem s_le_of_not_lt {s t : seq} (Hle : ¬ s_lt s t) : s_le t s :=
|
||||
begin
|
||||
rewrite [↑s_le, ↑nonneg, ↑s_lt at Hle, ↑pos at Hle],
|
||||
let Hle' := forall_of_not_exists Hle,
|
||||
|
|
@ -552,11 +554,11 @@ theorem s_zero_inv_equiv_zero : s_inv zero_is_reg ≡ zero :=
|
|||
by rewrite s_inv_zero; apply equiv.refl
|
||||
|
||||
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 :=
|
||||
s_lt s t ∨ s ≡ t :=
|
||||
if H : s ≡ t then or.inr H else
|
||||
or.inl (lt_of_le_and_sep Hs Ht (and.intro Hle (sep_of_nequiv Hs Ht H)))
|
||||
|
||||
theorem s_le_of_equiv_le_left {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : regular u)
|
||||
theorem s_le_of_equiv_le_left {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : regular u)
|
||||
(Heq : s ≡ t) (Hle : s_le s u) : s_le t u :=
|
||||
begin
|
||||
rewrite ↑s_le at *,
|
||||
|
|
@ -570,7 +572,7 @@ theorem s_le_of_equiv_le_left {s t u : seq} (Hs : regular s) (Ht : regular t) (H
|
|||
repeat (assumption | apply reg_add_reg | apply reg_neg_reg)
|
||||
end
|
||||
|
||||
theorem s_le_of_equiv_le_right {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : regular u)
|
||||
theorem s_le_of_equiv_le_right {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : regular u)
|
||||
(Heq : t ≡ u) (Hle : s_le s t) : s_le s u :=
|
||||
begin
|
||||
rewrite ↑s_le at *,
|
||||
|
|
@ -585,13 +587,13 @@ theorem s_le_of_equiv_le_right {s t u : seq} (Hs : regular s) (Ht : regular t) (
|
|||
|
||||
-----------------------------
|
||||
|
||||
definition r_inv (s : reg_seq) : reg_seq := reg_seq.mk (s_inv (reg_seq.is_reg s))
|
||||
(if H : sep (reg_seq.sq s) zero then reg_inv_reg (reg_seq.is_reg s) H else
|
||||
definition r_inv (s : reg_seq) : reg_seq := reg_seq.mk (s_inv (reg_seq.is_reg s))
|
||||
(if H : sep (reg_seq.sq s) zero then reg_inv_reg (reg_seq.is_reg s) H else
|
||||
have Hz : s_inv (reg_seq.is_reg s) = zero, from funext (λ n, dif_neg H), Hz⁻¹ ▸ zero_is_reg)
|
||||
|
||||
theorem r_inv_zero : requiv (r_inv r_zero) r_zero :=
|
||||
theorem r_inv_zero : requiv (r_inv r_zero) r_zero :=
|
||||
s_zero_inv_equiv_zero
|
||||
|
||||
|
||||
|
||||
theorem r_inv_well_defined {s t : reg_seq} (H : requiv s t) : requiv (r_inv s) (r_inv t) :=
|
||||
inv_well_defined (reg_seq.is_reg s) (reg_seq.is_reg t) H
|
||||
|
|
@ -599,7 +601,7 @@ theorem r_inv_well_defined {s t : reg_seq} (H : requiv s t) : requiv (r_inv s) (
|
|||
theorem r_le_total (s t : reg_seq) : r_le s t ∨ r_le t s :=
|
||||
s_le_total (reg_seq.is_reg s) (reg_seq.is_reg t)
|
||||
|
||||
theorem r_mul_inv (s : reg_seq) (Hsep : r_sep s r_zero) : requiv (s * (r_inv s)) r_one :=
|
||||
theorem r_mul_inv (s : reg_seq) (Hsep : r_sep s r_zero) : requiv (s * (r_inv s)) r_one :=
|
||||
mul_inv (reg_seq.is_reg s) Hsep
|
||||
|
||||
theorem r_sep_of_nequiv (s t : reg_seq) (Hneq : ¬ requiv s t) : r_sep s t :=
|
||||
|
|
@ -626,7 +628,7 @@ postfix `⁻¹` := inv
|
|||
theorem le_total (x y : ℝ) : x ≤ y ∨ y ≤ x :=
|
||||
quot.induction_on₂ x y (λ s t, s.r_le_total s t)
|
||||
|
||||
theorem mul_inv' (x : ℝ) : x ≢ zero → x * x⁻¹ = one :=
|
||||
theorem mul_inv' (x : ℝ) : x ≢ zero → x * x⁻¹ = one :=
|
||||
quot.induction_on x (λ s H, quot.sound (s.r_mul_inv s H))
|
||||
|
||||
theorem inv_mul' (x : ℝ) : x ≢ zero → x⁻¹ * x = one :=
|
||||
|
|
@ -639,7 +641,7 @@ theorem sep_of_neq {x y : ℝ} : ¬ x = y → x ≢ y :=
|
|||
quot.induction_on₂ x y (λ s t H, s.r_sep_of_nequiv s t (assume Heq, H (quot.sound Heq)))
|
||||
|
||||
theorem sep_is_neq (x y : ℝ) : (x ≢ y) = (¬ x = y) :=
|
||||
propext (iff.intro neq_of_sep sep_of_neq)
|
||||
propext (iff.intro neq_of_sep sep_of_neq)
|
||||
|
||||
theorem mul_inv (x : ℝ) : x ≠ zero → x * x⁻¹ = one := !sep_is_neq ▸ !mul_inv'
|
||||
|
||||
|
|
@ -648,15 +650,15 @@ theorem inv_mul (x : ℝ) : x ≠ zero → x⁻¹ * x = one := !sep_is_neq ▸ !
|
|||
theorem inv_zero : zero⁻¹ = zero := quot.sound (s.r_inv_zero)
|
||||
|
||||
theorem lt_or_eq_of_le (x y : ℝ) : x ≤ y → x < y ∨ x = y :=
|
||||
quot.induction_on₂ x y (λ s t H, or.elim (s.r_lt_or_equiv_of_le s t H)
|
||||
quot.induction_on₂ x y (λ s t H, or.elim (s.r_lt_or_equiv_of_le s t H)
|
||||
(assume H1, or.inl H1)
|
||||
(assume H2, or.inr (quot.sound H2)))
|
||||
|
||||
theorem le_iff_lt_or_eq (x y : ℝ) : x ≤ y ↔ x < y ∨ x = y :=
|
||||
theorem le_iff_lt_or_eq (x y : ℝ) : x ≤ y ↔ x < y ∨ x = y :=
|
||||
iff.intro (lt_or_eq_of_le x y) (le_of_lt_or_eq x y)
|
||||
|
||||
theorem dec_lt : decidable_rel lt :=
|
||||
begin
|
||||
theorem dec_lt : decidable_rel lt :=
|
||||
begin
|
||||
rewrite ↑decidable_rel,
|
||||
intros,
|
||||
apply prop_decidable
|
||||
|
|
@ -664,7 +666,7 @@ theorem dec_lt : decidable_rel lt :=
|
|||
|
||||
open [classes] algebra
|
||||
definition linear_ordered_field [instance] : algebra.discrete_linear_ordered_field ℝ :=
|
||||
⦃ algebra.discrete_linear_ordered_field, comm_ring, ordered_ring,
|
||||
⦃ algebra.discrete_linear_ordered_field, comm_ring, ordered_ring,
|
||||
le_total := le_total,
|
||||
mul_inv_cancel := mul_inv,
|
||||
inv_mul_cancel := inv_mul,
|
||||
|
|
|
|||
|
|
@ -12,10 +12,12 @@ To do:
|
|||
-/
|
||||
|
||||
import data.real.basic data.rat data.nat
|
||||
open -[coercions] rat
|
||||
open -[coercions] rat
|
||||
open -[coercions] nat
|
||||
open eq eq.ops
|
||||
|
||||
local notation 0 := rat.of_num 0
|
||||
local notation 1 := rat.of_num 1
|
||||
|
||||
----------------------------------------------------------------------------------------------------
|
||||
|
||||
-- pnat theorems
|
||||
|
|
@ -28,7 +30,7 @@ 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 :=
|
||||
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
|
||||
|
|
@ -40,12 +42,12 @@ theorem rewrite_helper8 (a b c : ℚ) : a - b = c - b + (a - c) := sorry -- simp
|
|||
|
||||
---------
|
||||
namespace s
|
||||
definition pos (s : seq) := ∃ n : ℕ+, n⁻¹ < (s n)
|
||||
definition pos (s : seq) := ∃ n : ℕ+, n⁻¹ < (s n)
|
||||
|
||||
definition nonneg (s : seq) := ∀ n : ℕ+, -(n⁻¹) ≤ s n
|
||||
|
||||
theorem bdd_away_of_pos {s : seq} (Hs : regular s) (H : pos s) :
|
||||
∃ N : ℕ+, ∀ n : ℕ+, n ≥ N → (s n) ≥ N⁻¹ :=
|
||||
∃ N : ℕ+, ∀ n : ℕ+, n ≥ N → (s n) ≥ N⁻¹ :=
|
||||
begin
|
||||
apply exists.elim H,
|
||||
intro n Hn,
|
||||
|
|
@ -73,7 +75,7 @@ theorem bdd_away_of_pos {s : seq} (Hs : regular s) (H : pos s) :
|
|||
apply Hin
|
||||
end
|
||||
|
||||
theorem pos_of_bdd_away {s : seq} (H : ∃ N : ℕ+, ∀ n : ℕ+, n ≥ N → (s n) ≥ N⁻¹) : pos s :=
|
||||
theorem pos_of_bdd_away {s : seq} (H : ∃ N : ℕ+, ∀ n : ℕ+, n ≥ N → (s n) ≥ N⁻¹) : pos s :=
|
||||
begin
|
||||
rewrite ↑pos,
|
||||
apply exists.elim H,
|
||||
|
|
@ -87,11 +89,11 @@ theorem pos_of_bdd_away {s : seq} (H : ∃ N : ℕ+, ∀ n : ℕ+, n ≥ N → (
|
|||
end
|
||||
|
||||
theorem bdd_within_of_nonneg {s : seq} (Hs : regular s) (H : nonneg s) :
|
||||
∀ n : ℕ+, ∃ N : ℕ+, ∀ m : ℕ+, m ≥ N → s m ≥ -n⁻¹ :=
|
||||
∀ n : ℕ+, ∃ N : ℕ+, ∀ m : ℕ+, m ≥ N → s m ≥ -n⁻¹ :=
|
||||
begin
|
||||
intros,
|
||||
existsi n,
|
||||
intro m Hm,
|
||||
intro m Hm,
|
||||
rewrite ↑nonneg at H,
|
||||
apply le.trans,
|
||||
apply neg_le_neg,
|
||||
|
|
@ -100,8 +102,8 @@ theorem bdd_within_of_nonneg {s : seq} (Hs : regular s) (H : nonneg s) :
|
|||
apply H
|
||||
end
|
||||
|
||||
theorem nonneg_of_bdd_within {s : seq} (Hs : regular s)
|
||||
(H : ∀n : ℕ+, ∃ N : ℕ+, ∀ m : ℕ+, m ≥ N → s m ≥ -n⁻¹) : nonneg s :=
|
||||
theorem nonneg_of_bdd_within {s : seq} (Hs : regular s)
|
||||
(H : ∀n : ℕ+, ∃ N : ℕ+, ∀ m : ℕ+, m ≥ N → s m ≥ -n⁻¹) : nonneg s :=
|
||||
begin
|
||||
rewrite ↑nonneg,
|
||||
intro k,
|
||||
|
|
@ -272,7 +274,7 @@ theorem s_neg_add_eq_s_add_neg (s t : seq) : sneg (sadd s t) ≡ sadd (sneg s) (
|
|||
apply add_invs_nonneg
|
||||
end
|
||||
|
||||
theorem equiv_cancel_middle {s t u : seq} (Hs : regular s) (Ht : regular t)
|
||||
theorem equiv_cancel_middle {s t u : seq} (Hs : regular s) (Ht : regular t)
|
||||
(Hu : regular u) : sadd (sadd u t) (sneg (sadd u s)) ≡ sadd t (sneg s) :=
|
||||
begin
|
||||
let Hz := zero_is_reg,
|
||||
|
|
@ -315,15 +317,15 @@ theorem add_le_add_of_le_right {s t : seq} (Hs : regular s) (Ht : regular t) (Ls
|
|||
begin
|
||||
intro u Hu,
|
||||
rewrite [↑s_le at *],
|
||||
apply nonneg_of_nonneg_equiv,
|
||||
apply nonneg_of_nonneg_equiv,
|
||||
rotate 2,
|
||||
apply equiv.symm,
|
||||
apply equiv_cancel_middle,
|
||||
repeat (apply reg_add_reg | apply reg_neg_reg | assumption)
|
||||
end
|
||||
|
||||
theorem s_add_lt_add_left {s t : seq} (Hs : regular s) (Ht : regular t) (Hst : s_lt s t) {u : seq}
|
||||
(Hu : regular u) : s_lt (sadd u s) (sadd u t) :=
|
||||
theorem s_add_lt_add_left {s t : seq} (Hs : regular s) (Ht : regular t) (Hst : s_lt s t) {u : seq}
|
||||
(Hu : regular u) : s_lt (sadd u s) (sadd u t) :=
|
||||
begin
|
||||
rewrite ↑s_lt at *,
|
||||
apply pos_of_pos_equiv,
|
||||
|
|
@ -333,7 +335,7 @@ theorem s_add_lt_add_left {s t : seq} (Hs : regular s) (Ht : regular t) (Hst : s
|
|||
repeat (apply reg_add_reg | apply reg_neg_reg | assumption)
|
||||
end
|
||||
|
||||
theorem add_nonneg_of_nonneg {s t : seq} (Hs : nonneg s) (Ht : nonneg t) : nonneg (sadd s t) :=
|
||||
theorem add_nonneg_of_nonneg {s t : seq} (Hs : nonneg s) (Ht : nonneg t) : nonneg (sadd s t) :=
|
||||
begin
|
||||
rewrite [↑nonneg at *, ↑sadd],
|
||||
intros,
|
||||
|
|
@ -351,7 +353,7 @@ theorem le.trans {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : regular u
|
|||
have H' : nonneg (sadd (sadd u (sadd (sneg t) t)) (sneg s)), begin
|
||||
apply nonneg_of_nonneg_equiv,
|
||||
rotate 2,
|
||||
apply add_well_defined,
|
||||
apply add_well_defined,
|
||||
rotate 4,
|
||||
apply s_add_assoc,
|
||||
repeat (apply reg_add_reg | apply reg_neg_reg | assumption),
|
||||
|
|
@ -427,7 +429,7 @@ theorem le_and_sep_of_lt {s t : seq} (Hs : regular s) (Ht : regular t) (Lst : s_
|
|||
sadd t (sneg s) n ≥ sadd t (sneg s) N - N⁻¹ - n⁻¹ : Habs
|
||||
... ≥ 0 - n⁻¹: begin
|
||||
apply rat.sub_le_sub_right,
|
||||
apply le_of_lt,
|
||||
apply le_of_lt,
|
||||
apply (iff.mp' (sub_pos_iff_lt _ _)),
|
||||
apply HN
|
||||
end
|
||||
|
|
@ -462,11 +464,11 @@ theorem s_neg_zero : sneg zero ≡ zero :=
|
|||
begin
|
||||
rewrite ↑[sneg, zero, equiv],
|
||||
intros,
|
||||
rewrite [sub_zero, abs_neg, abs_zero],
|
||||
rewrite [sub_zero, abs_neg, abs_zero],
|
||||
apply add_invs_nonneg
|
||||
end
|
||||
|
||||
theorem s_sub_zero {s : seq} (Hs : regular s) : sadd s (sneg zero) ≡ s :=
|
||||
theorem s_sub_zero {s : seq} (Hs : regular s) : sadd s (sneg zero) ≡ s :=
|
||||
begin
|
||||
apply equiv.trans,
|
||||
rotate 3,
|
||||
|
|
@ -488,7 +490,7 @@ theorem s_pos_of_gt_zero {s : seq} (Hs : regular s) (Hgz : s_lt zero s) : pos s
|
|||
apply zero_is_reg
|
||||
end
|
||||
|
||||
theorem s_gt_zero_of_pos {s : seq} (Hs : regular s) (Hp : pos s) : s_lt zero s :=
|
||||
theorem s_gt_zero_of_pos {s : seq} (Hs : regular s) (Hp : pos s) : s_lt zero s :=
|
||||
begin
|
||||
rewrite ↑s_lt,
|
||||
apply pos_of_pos_equiv,
|
||||
|
|
@ -498,7 +500,7 @@ theorem s_gt_zero_of_pos {s : seq} (Hs : regular s) (Hp : pos s) : s_lt zero s :
|
|||
repeat assumption
|
||||
end
|
||||
|
||||
theorem s_nonneg_of_ge_zero {s : seq} (Hs : regular s) (Hgz : s_le zero s) : nonneg s :=
|
||||
theorem s_nonneg_of_ge_zero {s : seq} (Hs : regular s) (Hgz : s_le zero s) : nonneg s :=
|
||||
begin
|
||||
rewrite ↑s_le at *,
|
||||
apply nonneg_of_nonneg_equiv,
|
||||
|
|
@ -507,7 +509,7 @@ theorem s_nonneg_of_ge_zero {s : seq} (Hs : regular s) (Hgz : s_le zero s) : non
|
|||
repeat (assumption | apply reg_add_reg | apply reg_neg_reg | apply zero_is_reg)
|
||||
end
|
||||
|
||||
theorem s_ge_zero_of_nonneg {s : seq} (Hs : regular s) (Hn : nonneg s) : s_le zero s :=
|
||||
theorem s_ge_zero_of_nonneg {s : seq} (Hs : regular s) (Hn : nonneg s) : s_le zero s :=
|
||||
begin
|
||||
rewrite ↑s_le,
|
||||
apply nonneg_of_nonneg_equiv,
|
||||
|
|
@ -567,7 +569,7 @@ theorem s_mul_pos_of_pos {s t : seq} (Hs : regular s) (Ht : regular t) (Hps : po
|
|||
|
||||
theorem s_mul_gt_zero_of_gt_zero {s t : seq} (Hs : regular s) (Ht : regular t)
|
||||
(Hzs : s_lt zero s) (Hzt : s_lt zero t) : s_lt zero (smul s t) :=
|
||||
s_gt_zero_of_pos
|
||||
s_gt_zero_of_pos
|
||||
(reg_mul_reg Hs Ht)
|
||||
(s_mul_pos_of_pos Hs Ht (s_pos_of_gt_zero Hs Hzs) (s_pos_of_gt_zero Ht Hzt))
|
||||
|
||||
|
|
@ -619,7 +621,7 @@ theorem s_mul_nonneg_of_pos_of_zero {s t : seq} (Hs : regular s) (Ht : regular t
|
|||
repeat (assumption | apply reg_mul_reg | apply zero_is_reg)
|
||||
end
|
||||
|
||||
theorem s_mul_nonneg_of_nonneg {s t : seq} (Hs : regular s) (Ht : regular t)
|
||||
theorem s_mul_nonneg_of_nonneg {s t : seq} (Hs : regular s) (Ht : regular t)
|
||||
(Hps : nonneg s) (Hpt : nonneg t) : nonneg (smul s t) :=
|
||||
begin
|
||||
intro n,
|
||||
|
|
@ -784,7 +786,7 @@ theorem lt_well_defined {s t u v : seq} (Hs : regular s) (Ht : regular t) (Hu :
|
|||
|
||||
|
||||
theorem sep_well_defined {s t u v : seq} (Hs : regular s) (Ht : regular t) (Hu : regular u)
|
||||
(Hv : regular v) (Hsu : s ≡ u) (Htv : t ≡ v) : s ≢ t ↔ u ≢ v :=
|
||||
(Hv : regular v) (Hsu : s ≡ u) (Htv : t ≡ v) : s ≢ t ↔ u ≢ v :=
|
||||
begin
|
||||
rewrite ↑sep,
|
||||
apply iff.intro,
|
||||
|
|
@ -819,7 +821,7 @@ theorem s_lt_of_lt_of_le {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : r
|
|||
have Hcan : ∀ m, sadd u (sneg s) m = (sadd t (sneg s)) m + (sadd u (sneg t)) m, begin
|
||||
intro m,
|
||||
rewrite [↑sadd, ↑sneg, -rewrite_helper8]
|
||||
end,
|
||||
end,
|
||||
rewrite [↑s_lt at *, ↑s_le at *],
|
||||
apply exists.elim (bdd_away_of_pos Rtns Hst),
|
||||
intro Nt HNt,
|
||||
|
|
@ -859,7 +861,7 @@ theorem s_lt_of_le_of_lt {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : r
|
|||
have Hcan : ∀ m, sadd u (sneg s) m = (sadd t (sneg s)) m + (sadd u (sneg t)) m, begin
|
||||
intro m,
|
||||
rewrite [↑sadd, ↑sneg, -rewrite_helper8]
|
||||
end,
|
||||
end,
|
||||
rewrite [↑s_lt at *, ↑s_le at *],
|
||||
apply exists.elim (bdd_away_of_pos Runt Htu),
|
||||
intro Nu HNu,
|
||||
|
|
@ -938,7 +940,7 @@ theorem r_le.refl (s : reg_seq) : r_le s s := le.refl (reg_seq.is_reg s)
|
|||
theorem r_le.trans {s t u : reg_seq} (Hst : r_le s t) (Htu : r_le t u) : r_le s u :=
|
||||
le.trans (reg_seq.is_reg s) (reg_seq.is_reg t) (reg_seq.is_reg u) Hst Htu
|
||||
|
||||
theorem r_equiv_of_le_of_ge {s t : reg_seq} (Hs : r_le s t) (Hu : r_le t s) :
|
||||
theorem r_equiv_of_le_of_ge {s t : reg_seq} (Hs : r_le s t) (Hu : r_le t s) :
|
||||
requiv s t :=
|
||||
equiv_of_le_of_ge (reg_seq.is_reg s) (reg_seq.is_reg t) Hs Hu
|
||||
|
||||
|
|
@ -950,14 +952,14 @@ theorem r_add_le_add_of_le_right {s t : reg_seq} (H : r_le s t) (u : reg_seq) :
|
|||
add_le_add_of_le_right (reg_seq.is_reg s) (reg_seq.is_reg t) H
|
||||
(reg_seq.sq u) (reg_seq.is_reg u)
|
||||
|
||||
theorem r_add_le_add_of_le_right_var (s t u : reg_seq) (H : r_le s t) :
|
||||
theorem r_add_le_add_of_le_right_var (s t u : reg_seq) (H : r_le s t) :
|
||||
r_le (u + s) (u + t) := r_add_le_add_of_le_right H u
|
||||
|
||||
theorem r_mul_pos_of_pos {s t : reg_seq} (Hs : r_lt r_zero s) (Ht : r_lt r_zero t) :
|
||||
theorem r_mul_pos_of_pos {s t : reg_seq} (Hs : r_lt r_zero s) (Ht : r_lt r_zero t) :
|
||||
r_lt r_zero (s * t) :=
|
||||
s_mul_gt_zero_of_gt_zero (reg_seq.is_reg s) (reg_seq.is_reg t) Hs Ht
|
||||
|
||||
theorem r_mul_nonneg_of_nonneg {s t : reg_seq} (Hs : r_le r_zero s) (Ht : r_le r_zero t) :
|
||||
theorem r_mul_nonneg_of_nonneg {s t : reg_seq} (Hs : r_le r_zero s) (Ht : r_le r_zero t) :
|
||||
r_le r_zero (s * t) :=
|
||||
s_mul_ge_zero_of_ge_zero (reg_seq.is_reg s) (reg_seq.is_reg t) Hs Ht
|
||||
|
||||
|
|
@ -1036,7 +1038,7 @@ theorem mul_ge_zero_of_ge_zero (x y : ℝ) : zero ≤ x → zero ≤ y → zero
|
|||
|
||||
theorem not_sep_self (x : ℝ) : ¬ x ≢ x :=
|
||||
quot.induction_on x (λ s, s.r_not_sep_self s)
|
||||
|
||||
|
||||
theorem not_lt_self (x : ℝ) : ¬ x < x :=
|
||||
quot.induction_on x (λ s, s.r_not_lt_self s)
|
||||
|
||||
|
|
@ -1049,7 +1051,7 @@ theorem lt_of_le_of_lt (x y z : ℝ) : x ≤ y → y < z → x < z :=
|
|||
theorem lt_of_lt_of_le (x y z : ℝ) : x < y → y ≤ z → x < z :=
|
||||
quot.induction_on₃ x y z (λ s t u H H', s.r_lt_of_lt_of_le H H')
|
||||
|
||||
theorem add_lt_add_left_var (x y z : ℝ) : x < y → z + x < z + y :=
|
||||
theorem add_lt_add_left_var (x y z : ℝ) : x < y → z + x < z + y :=
|
||||
quot.induction_on₃ x y z (λ s t u, s.r_add_lt_add_left_var s t u)
|
||||
|
||||
theorem add_lt_add_left (x y : ℝ) : x < y → ∀ z : ℝ, z + x < z + y :=
|
||||
|
|
@ -1059,8 +1061,8 @@ theorem zero_lt_one : zero < one := s.r_zero_lt_one
|
|||
|
||||
theorem le_of_lt_or_eq (x y : ℝ) : x < y ∨ x = y → x ≤ y :=
|
||||
(quot.induction_on₂ x y (λ s t H, or.elim H (take H', begin
|
||||
apply s.r_le_of_lt_or_eq,
|
||||
apply or.inl H'
|
||||
apply s.r_le_of_lt_or_eq,
|
||||
apply or.inl H'
|
||||
end)
|
||||
(take H', begin
|
||||
apply s.r_le_of_lt_or_eq,
|
||||
|
|
@ -1071,11 +1073,11 @@ theorem le_of_lt_or_eq (x y : ℝ) : x < y ∨ x = y → x ≤ y :=
|
|||
-- 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)
|
||||
(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),
|
||||
let H'' := iff.mp' (s.r_le_iff_lt_or_equiv s t),
|
||||
apply H'' (or.inl H')
|
||||
end)
|
||||
(take H', begin
|
||||
|
|
@ -1105,7 +1107,7 @@ definition ordered_ring : algebra.ordered_ring ℝ :=
|
|||
|
||||
-----------------------------------
|
||||
--- 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) := sorry
|
||||
|
||||
/-theorem sep_is_eq (x y : ℝ) : x ≢ y = ¬ (x = y) := begin
|
||||
apply propext,
|
||||
|
|
|
|||
Loading…
Reference in a new issue