2015-04-27 17:24:18 +00:00
|
|
|
|
/-
|
|
|
|
|
Copyright (c) 2015 Jeremy Avigad. All rights reserved.
|
|
|
|
|
Released under Apache 2.0 license as described in the file LICENSE.
|
|
|
|
|
Author: Jeremy Avigad
|
|
|
|
|
|
|
|
|
|
Adds the ordering, and instantiates the rationals as an ordered field.
|
|
|
|
|
-/
|
2015-10-09 01:35:37 +00:00
|
|
|
|
import data.int algebra.ordered_field algebra.group_power data.rat.basic
|
2015-04-27 17:24:18 +00:00
|
|
|
|
open quot eq.ops
|
2015-10-12 03:35:45 +00:00
|
|
|
|
open algebra
|
2015-04-27 17:24:18 +00:00
|
|
|
|
|
|
|
|
|
/- the ordering on representations -/
|
2015-06-10 02:46:30 +00:00
|
|
|
|
|
2015-04-27 17:24:18 +00:00
|
|
|
|
namespace prerat
|
|
|
|
|
section int_notation
|
|
|
|
|
open int
|
|
|
|
|
|
|
|
|
|
variables {a b : prerat}
|
|
|
|
|
|
|
|
|
|
definition pos (a : prerat) : Prop := num a > 0
|
|
|
|
|
|
2015-05-23 02:21:08 +00:00
|
|
|
|
definition nonneg (a : prerat) : Prop := num a ≥ 0
|
|
|
|
|
|
2015-10-09 01:35:37 +00:00
|
|
|
|
theorem pos_of_int (a : ℤ) : pos (of_int a) ↔ (a > 0) :=
|
2015-05-23 02:21:08 +00:00
|
|
|
|
!iff.rfl
|
|
|
|
|
|
2015-10-09 01:35:37 +00:00
|
|
|
|
theorem nonneg_of_int (a : ℤ) : nonneg (of_int a) ↔ (a ≥ 0) :=
|
2015-05-23 02:21:08 +00:00
|
|
|
|
!iff.rfl
|
|
|
|
|
|
2015-04-27 17:24:18 +00:00
|
|
|
|
theorem pos_eq_pos_of_equiv {a b : prerat} (H1 : a ≡ b) : pos a = pos b :=
|
|
|
|
|
propext (iff.intro (num_pos_of_equiv H1) (num_pos_of_equiv H1⁻¹))
|
|
|
|
|
|
|
|
|
|
theorem nonneg_eq_nonneg_of_equiv (H : a ≡ b) : nonneg a = nonneg b :=
|
|
|
|
|
have H1 : (0 = num a) = (0 = num b),
|
|
|
|
|
from propext (iff.intro
|
|
|
|
|
(assume H2, eq.symm (num_eq_zero_of_equiv H H2⁻¹))
|
|
|
|
|
(assume H2, eq.symm (num_eq_zero_of_equiv H⁻¹ H2⁻¹))),
|
|
|
|
|
calc
|
|
|
|
|
nonneg a = (pos a ∨ 0 = num a) : propext !le_iff_lt_or_eq
|
|
|
|
|
... = (pos b ∨ 0 = num a) : pos_eq_pos_of_equiv H
|
|
|
|
|
... = (pos b ∨ 0 = num b) : H1
|
|
|
|
|
... = nonneg b : propext !le_iff_lt_or_eq
|
|
|
|
|
|
|
|
|
|
theorem nonneg_zero : nonneg zero := le.refl 0
|
|
|
|
|
|
|
|
|
|
theorem nonneg_add (H1 : nonneg a) (H2 : nonneg b) : nonneg (add a b) :=
|
2015-04-27 19:59:02 +00:00
|
|
|
|
show num a * denom b + num b * denom a ≥ 0,
|
|
|
|
|
from add_nonneg
|
2015-04-27 17:24:18 +00:00
|
|
|
|
(mul_nonneg H1 (le_of_lt (denom_pos b)))
|
|
|
|
|
(mul_nonneg H2 (le_of_lt (denom_pos a)))
|
|
|
|
|
|
|
|
|
|
theorem nonneg_antisymm (H1 : nonneg a) (H2 : nonneg (neg a)) : a ≡ zero :=
|
|
|
|
|
have H3 : num a = 0, from le.antisymm (nonpos_of_neg_nonneg H2) H1,
|
|
|
|
|
equiv_zero_of_num_eq_zero H3
|
|
|
|
|
|
|
|
|
|
theorem nonneg_total (a : prerat) : nonneg a ∨ nonneg (neg a) :=
|
|
|
|
|
or.elim (le.total 0 (num a))
|
2015-07-20 04:15:20 +00:00
|
|
|
|
(suppose 0 ≤ num a, or.inl this)
|
|
|
|
|
(suppose 0 ≥ num a, or.inr (neg_nonneg_of_nonpos this))
|
2015-04-27 17:24:18 +00:00
|
|
|
|
|
|
|
|
|
theorem nonneg_of_pos (H : pos a) : nonneg a := le_of_lt H
|
|
|
|
|
|
|
|
|
|
theorem ne_zero_of_pos (H : pos a) : ¬ a ≡ zero :=
|
|
|
|
|
assume H', ne_of_gt H (num_eq_zero_of_equiv_zero H')
|
|
|
|
|
|
|
|
|
|
theorem pos_of_nonneg_of_ne_zero (H1 : nonneg a) (H2 : ¬ a ≡ zero) : pos a :=
|
2015-07-20 04:15:20 +00:00
|
|
|
|
have num a ≠ 0, from suppose num a = 0, H2 (equiv_zero_of_num_eq_zero this),
|
|
|
|
|
lt_of_le_of_ne H1 (ne.symm this)
|
2015-04-27 17:24:18 +00:00
|
|
|
|
|
|
|
|
|
theorem nonneg_mul (H1 : nonneg a) (H2 : nonneg b) : nonneg (mul a b) :=
|
|
|
|
|
mul_nonneg H1 H2
|
|
|
|
|
|
|
|
|
|
theorem pos_mul (H1 : pos a) (H2 : pos b) : pos (mul a b) :=
|
|
|
|
|
mul_pos H1 H2
|
|
|
|
|
|
|
|
|
|
end int_notation
|
|
|
|
|
end prerat
|
|
|
|
|
|
|
|
|
|
local attribute prerat.setoid [instance]
|
|
|
|
|
|
|
|
|
|
/- The ordering on the rationals.
|
|
|
|
|
|
2015-04-27 19:59:02 +00:00
|
|
|
|
The definitions of pos and nonneg are kept private, because they are only meant for internal
|
2015-04-27 17:24:18 +00:00
|
|
|
|
use. Users should use a > 0 and a ≥ 0 instead of pos and nonneg.
|
|
|
|
|
-/
|
|
|
|
|
|
|
|
|
|
namespace rat
|
2015-10-09 01:35:37 +00:00
|
|
|
|
open nat int
|
2015-04-27 17:24:18 +00:00
|
|
|
|
variables {a b c : ℚ}
|
|
|
|
|
|
|
|
|
|
/- transfer properties of pos and nonneg -/
|
|
|
|
|
|
|
|
|
|
private definition pos (a : ℚ) : Prop :=
|
|
|
|
|
quot.lift prerat.pos @prerat.pos_eq_pos_of_equiv a
|
|
|
|
|
|
|
|
|
|
private definition nonneg (a : ℚ) : Prop :=
|
|
|
|
|
quot.lift prerat.nonneg @prerat.nonneg_eq_nonneg_of_equiv a
|
|
|
|
|
|
2015-10-09 01:35:37 +00:00
|
|
|
|
private theorem pos_of_int (a : ℤ) : (a > 0) ↔ pos (of_int a) :=
|
2015-05-23 02:21:08 +00:00
|
|
|
|
prerat.pos_of_int a
|
|
|
|
|
|
2015-10-09 01:35:37 +00:00
|
|
|
|
private theorem nonneg_of_int (a : ℤ) : (a ≥ 0) ↔ nonneg (of_int a) :=
|
2015-05-23 02:21:08 +00:00
|
|
|
|
prerat.nonneg_of_int a
|
|
|
|
|
|
2015-04-27 17:24:18 +00:00
|
|
|
|
private theorem nonneg_zero : nonneg 0 := prerat.nonneg_zero
|
|
|
|
|
|
|
|
|
|
private theorem nonneg_add : nonneg a → nonneg b → nonneg (a + b) :=
|
|
|
|
|
quot.induction_on₂ a b @prerat.nonneg_add
|
|
|
|
|
|
|
|
|
|
private theorem nonneg_antisymm : nonneg a → nonneg (-a) → a = 0 :=
|
|
|
|
|
quot.induction_on a
|
|
|
|
|
(take u, assume H1 H2,
|
|
|
|
|
quot.sound (prerat.nonneg_antisymm H1 H2))
|
|
|
|
|
|
|
|
|
|
private theorem nonneg_total (a : ℚ) : nonneg a ∨ nonneg (-a) :=
|
|
|
|
|
quot.induction_on a @prerat.nonneg_total
|
|
|
|
|
|
|
|
|
|
private theorem nonneg_of_pos : pos a → nonneg a :=
|
|
|
|
|
quot.induction_on a @prerat.nonneg_of_pos
|
|
|
|
|
|
2015-04-27 19:59:02 +00:00
|
|
|
|
private theorem ne_zero_of_pos : pos a → a ≠ 0 :=
|
2015-04-27 17:24:18 +00:00
|
|
|
|
quot.induction_on a (take u, assume H1 H2, prerat.ne_zero_of_pos H1 (quot.exact H2))
|
|
|
|
|
|
|
|
|
|
private theorem pos_of_nonneg_of_ne_zero : nonneg a → ¬ a = 0 → pos a :=
|
|
|
|
|
quot.induction_on a
|
|
|
|
|
(take u,
|
2015-07-20 04:15:20 +00:00
|
|
|
|
assume h : nonneg ⟦u⟧,
|
|
|
|
|
suppose ⟦u⟧ ≠ (rat.of_num 0),
|
|
|
|
|
have ¬ (prerat.equiv u prerat.zero), from assume H, this (quot.sound H),
|
|
|
|
|
prerat.pos_of_nonneg_of_ne_zero h this)
|
2015-04-27 17:24:18 +00:00
|
|
|
|
|
|
|
|
|
private theorem nonneg_mul : nonneg a → nonneg b → nonneg (a * b) :=
|
|
|
|
|
quot.induction_on₂ a b @prerat.nonneg_mul
|
|
|
|
|
|
|
|
|
|
private theorem pos_mul : pos a → pos b → pos (a * b) :=
|
|
|
|
|
quot.induction_on₂ a b @prerat.pos_mul
|
|
|
|
|
|
|
|
|
|
private definition decidable_pos (a : ℚ) : decidable (pos a) :=
|
|
|
|
|
quot.rec_on_subsingleton a (take u, int.decidable_lt 0 (prerat.num u))
|
|
|
|
|
|
|
|
|
|
/- define order in terms of pos and nonneg -/
|
|
|
|
|
|
2015-10-09 01:35:37 +00:00
|
|
|
|
protected definition lt (a b : ℚ) : Prop := pos (b - a)
|
|
|
|
|
protected definition le (a b : ℚ) : Prop := nonneg (b - a)
|
|
|
|
|
|
|
|
|
|
definition rat_has_lt [reducible] [instance] [priority rat.prio] : has_lt rat :=
|
|
|
|
|
has_lt.mk rat.lt
|
|
|
|
|
|
|
|
|
|
definition rat_has_le [reducible] [instance] [priority rat.prio] : has_le rat :=
|
|
|
|
|
has_le.mk rat.le
|
2015-04-27 17:24:18 +00:00
|
|
|
|
|
2015-10-23 02:18:14 +00:00
|
|
|
|
protected lemma lt_def (a b : ℚ) : (a < b) = pos (b - a) :=
|
2015-10-09 01:35:37 +00:00
|
|
|
|
rfl
|
2015-04-27 17:24:18 +00:00
|
|
|
|
|
2015-10-23 02:18:14 +00:00
|
|
|
|
protected lemma le_def (a b : ℚ) : (a ≤ b) = nonneg (b - a) :=
|
2015-10-09 01:35:37 +00:00
|
|
|
|
rfl
|
|
|
|
|
|
|
|
|
|
theorem of_int_lt_of_int_iff (a b : ℤ) : of_int a < of_int b ↔ a < b :=
|
2015-05-25 11:52:20 +00:00
|
|
|
|
iff.symm (calc
|
2015-10-09 01:35:37 +00:00
|
|
|
|
a < b ↔ b - a > 0 : iff.symm !sub_pos_iff_lt
|
|
|
|
|
... ↔ pos (of_int (b - a)) : iff.symm !pos_of_int
|
|
|
|
|
... ↔ pos (of_int b - of_int a) : !of_int_sub ▸ iff.rfl
|
|
|
|
|
... ↔ of_int a < of_int b : iff.rfl)
|
2015-05-23 02:21:08 +00:00
|
|
|
|
|
2015-10-09 01:35:37 +00:00
|
|
|
|
theorem of_int_lt_of_int_of_lt {a b : ℤ} (H : a < b) : of_int a < of_int b :=
|
2015-09-12 14:00:34 +00:00
|
|
|
|
iff.mpr !of_int_lt_of_int_iff H
|
|
|
|
|
|
2015-10-09 01:35:37 +00:00
|
|
|
|
theorem lt_of_of_int_lt_of_int {a b : ℤ} (H : of_int a < of_int b) : a < b :=
|
2015-09-12 14:00:34 +00:00
|
|
|
|
iff.mp !of_int_lt_of_int_iff H
|
|
|
|
|
|
2015-10-09 01:35:37 +00:00
|
|
|
|
theorem of_int_le_of_int_iff (a b : ℤ) : of_int a ≤ of_int b ↔ (a ≤ b) :=
|
2015-05-25 11:52:20 +00:00
|
|
|
|
iff.symm (calc
|
2015-10-09 01:35:37 +00:00
|
|
|
|
a ≤ b ↔ b - a ≥ 0 : iff.symm !sub_nonneg_iff_le
|
|
|
|
|
... ↔ nonneg (of_int (b - a)) : iff.symm !nonneg_of_int
|
|
|
|
|
... ↔ nonneg (of_int b - of_int a) : !of_int_sub ▸ iff.rfl
|
|
|
|
|
... ↔ of_int a ≤ of_int b : iff.rfl)
|
2015-05-25 11:52:20 +00:00
|
|
|
|
|
2015-10-09 01:35:37 +00:00
|
|
|
|
theorem of_int_le_of_int_of_le {a b : ℤ} (H : a ≤ b) : of_int a ≤ of_int b :=
|
2015-09-12 14:00:34 +00:00
|
|
|
|
iff.mpr !of_int_le_of_int_iff H
|
|
|
|
|
|
2015-10-09 01:35:37 +00:00
|
|
|
|
theorem le_of_of_int_le_of_int {a b : ℤ} (H : of_int a ≤ of_int b) : a ≤ b :=
|
2015-09-12 14:00:34 +00:00
|
|
|
|
iff.mp !of_int_le_of_int_iff H
|
|
|
|
|
|
2015-10-09 01:35:37 +00:00
|
|
|
|
theorem of_nat_lt_of_nat_iff (a b : ℕ) : of_nat a < of_nat b ↔ a < b :=
|
2015-09-12 14:00:34 +00:00
|
|
|
|
by rewrite [*of_nat_eq, of_int_lt_of_int_iff, int.of_nat_lt_of_nat_iff]
|
|
|
|
|
|
2015-10-09 01:35:37 +00:00
|
|
|
|
theorem of_nat_lt_of_nat_of_lt {a b : ℕ} (H : a < b) : of_nat a < of_nat b :=
|
2015-09-12 14:00:34 +00:00
|
|
|
|
iff.mpr !of_nat_lt_of_nat_iff H
|
2015-05-25 11:52:20 +00:00
|
|
|
|
|
2015-10-09 01:35:37 +00:00
|
|
|
|
theorem lt_of_of_nat_lt_of_nat {a b : ℕ} (H : of_nat a < of_nat b) : a < b :=
|
2015-09-12 14:00:34 +00:00
|
|
|
|
iff.mp !of_nat_lt_of_nat_iff H
|
2015-05-25 11:52:20 +00:00
|
|
|
|
|
2015-10-09 01:35:37 +00:00
|
|
|
|
theorem of_nat_le_of_nat_iff (a b : ℕ) : of_nat a ≤ of_nat b ↔ a ≤ b :=
|
2015-09-12 14:00:34 +00:00
|
|
|
|
by rewrite [*of_nat_eq, of_int_le_of_int_iff, int.of_nat_le_of_nat_iff]
|
2015-05-25 11:52:20 +00:00
|
|
|
|
|
2015-10-09 01:35:37 +00:00
|
|
|
|
theorem of_nat_le_of_nat_of_le {a b : ℕ} (H : a ≤ b) : of_nat a ≤ of_nat b :=
|
2015-09-12 14:00:34 +00:00
|
|
|
|
iff.mpr !of_nat_le_of_nat_iff H
|
2015-05-25 11:52:20 +00:00
|
|
|
|
|
2015-10-09 01:35:37 +00:00
|
|
|
|
theorem le_of_of_nat_le_of_nat {a b : ℕ} (H : of_nat a ≤ of_nat b) : a ≤ b :=
|
2015-09-12 14:00:34 +00:00
|
|
|
|
iff.mp !of_nat_le_of_nat_iff H
|
2015-05-25 11:52:20 +00:00
|
|
|
|
|
2015-06-16 02:48:57 +00:00
|
|
|
|
theorem of_nat_nonneg (a : ℕ) : (of_nat a ≥ 0) :=
|
2015-09-12 14:00:34 +00:00
|
|
|
|
of_nat_le_of_nat_of_le !nat.zero_le
|
2015-05-23 02:21:08 +00:00
|
|
|
|
|
2015-10-23 02:18:14 +00:00
|
|
|
|
protected theorem le_refl (a : ℚ) : a ≤ a :=
|
|
|
|
|
by rewrite [rat.le_def, sub_self]; apply nonneg_zero
|
2015-04-27 17:24:18 +00:00
|
|
|
|
|
2015-10-23 02:18:14 +00:00
|
|
|
|
protected theorem le_trans (H1 : a ≤ b) (H2 : b ≤ c) : a ≤ c :=
|
2015-04-27 17:24:18 +00:00
|
|
|
|
assert H3 : nonneg (c - b + (b - a)), from nonneg_add H2 H1,
|
|
|
|
|
begin
|
|
|
|
|
revert H3,
|
2015-10-13 20:16:19 +00:00
|
|
|
|
rewrite [rat.sub.def, add.assoc, sub_eq_add_neg, neg_add_cancel_left],
|
2015-04-27 17:24:18 +00:00
|
|
|
|
intro H3, apply H3
|
|
|
|
|
end
|
|
|
|
|
|
2015-10-23 02:18:14 +00:00
|
|
|
|
protected theorem le_antisymm (H1 : a ≤ b) (H2 : b ≤ a) : a = b :=
|
2015-04-27 17:24:18 +00:00
|
|
|
|
have H3 : nonneg (-(a - b)), from !neg_sub⁻¹ ▸ H1,
|
|
|
|
|
have H4 : a - b = 0, from nonneg_antisymm H2 H3,
|
|
|
|
|
eq_of_sub_eq_zero H4
|
|
|
|
|
|
2015-10-23 02:18:14 +00:00
|
|
|
|
protected theorem le_total (a b : ℚ) : a ≤ b ∨ b ≤ a :=
|
2015-04-27 17:24:18 +00:00
|
|
|
|
or.elim (nonneg_total (b - a))
|
|
|
|
|
(assume H, or.inl H)
|
2015-10-09 01:35:37 +00:00
|
|
|
|
(assume H, or.inr begin rewrite neg_sub at H, exact H end)
|
2015-04-27 17:24:18 +00:00
|
|
|
|
|
2015-10-23 02:18:14 +00:00
|
|
|
|
protected theorem le_by_cases {P : Prop} (a b : ℚ) (H : a ≤ b → P) (H2 : b ≤ a → P) : P :=
|
|
|
|
|
or.elim (!rat.le_total) H H2
|
2015-05-29 04:09:13 +00:00
|
|
|
|
|
2015-10-23 02:18:14 +00:00
|
|
|
|
protected theorem lt_iff_le_and_ne (a b : ℚ) : a < b ↔ a ≤ b ∧ a ≠ b :=
|
2015-04-27 17:24:18 +00:00
|
|
|
|
iff.intro
|
2015-04-27 19:59:02 +00:00
|
|
|
|
(assume H : a < b,
|
2015-07-20 04:15:20 +00:00
|
|
|
|
have b - a ≠ 0, from ne_zero_of_pos H,
|
|
|
|
|
have a ≠ b, from ne.symm (assume H', this (H' ▸ !sub_self)),
|
|
|
|
|
and.intro (nonneg_of_pos H) this)
|
2015-04-27 17:24:18 +00:00
|
|
|
|
(assume H : a ≤ b ∧ a ≠ b,
|
2015-05-06 01:26:12 +00:00
|
|
|
|
obtain aleb aneb, from H,
|
2015-07-20 04:15:20 +00:00
|
|
|
|
have b - a ≠ 0, from (assume H', aneb (eq_of_sub_eq_zero H')⁻¹),
|
|
|
|
|
pos_of_nonneg_of_ne_zero aleb this)
|
2015-04-27 17:24:18 +00:00
|
|
|
|
|
2015-10-23 02:18:14 +00:00
|
|
|
|
protected theorem le_iff_lt_or_eq (a b : ℚ) : a ≤ b ↔ a < b ∨ a = b :=
|
2015-04-27 17:24:18 +00:00
|
|
|
|
iff.intro
|
2015-07-20 04:15:20 +00:00
|
|
|
|
(assume h : a ≤ b,
|
2015-04-27 17:24:18 +00:00
|
|
|
|
decidable.by_cases
|
2015-07-20 04:15:20 +00:00
|
|
|
|
(suppose a = b, or.inr this)
|
2015-10-23 02:18:14 +00:00
|
|
|
|
(suppose a ≠ b, or.inl (iff.mpr !rat.lt_iff_le_and_ne (and.intro h this))))
|
2015-07-20 04:15:20 +00:00
|
|
|
|
(suppose a < b ∨ a = b,
|
|
|
|
|
or.elim this
|
2015-10-23 02:18:14 +00:00
|
|
|
|
(suppose a < b, and.left (iff.mp !rat.lt_iff_le_and_ne this))
|
|
|
|
|
(suppose a = b, this ▸ !rat.le_refl))
|
2015-04-27 17:24:18 +00:00
|
|
|
|
|
2015-08-17 03:23:03 +00:00
|
|
|
|
private theorem to_nonneg : a ≥ 0 → nonneg a :=
|
2015-06-10 23:56:17 +00:00
|
|
|
|
by intros; rewrite -sub_zero; eassumption
|
|
|
|
|
|
2015-10-23 02:18:14 +00:00
|
|
|
|
protected theorem add_le_add_left (H : a ≤ b) (c : ℚ) : c + a ≤ c + b :=
|
2015-07-20 04:15:20 +00:00
|
|
|
|
have c + b - (c + a) = b - a,
|
2015-10-09 01:35:37 +00:00
|
|
|
|
by rewrite [sub.def, neg_add, -add.assoc, add.comm c, add_neg_cancel_right],
|
2015-07-20 04:15:20 +00:00
|
|
|
|
show nonneg (c + b - (c + a)), from this⁻¹ ▸ H
|
2015-04-27 17:24:18 +00:00
|
|
|
|
|
2015-10-23 02:18:14 +00:00
|
|
|
|
protected theorem mul_nonneg (H1 : a ≥ (0 : ℚ)) (H2 : b ≥ (0 : ℚ)) : a * b ≥ (0 : ℚ) :=
|
2015-10-09 01:35:37 +00:00
|
|
|
|
assert nonneg (a * b), from nonneg_mul (to_nonneg H1) (to_nonneg H2),
|
|
|
|
|
begin rewrite -sub_zero at this, exact this end
|
2015-04-27 17:24:18 +00:00
|
|
|
|
|
2015-08-17 03:23:03 +00:00
|
|
|
|
private theorem to_pos : a > 0 → pos a :=
|
2015-06-10 23:56:17 +00:00
|
|
|
|
by intros; rewrite -sub_zero; eassumption
|
|
|
|
|
|
2015-10-23 02:18:14 +00:00
|
|
|
|
protected theorem mul_pos (H1 : a > (0 : ℚ)) (H2 : b > (0 : ℚ)) : a * b > (0 : ℚ) :=
|
2015-10-09 01:35:37 +00:00
|
|
|
|
assert pos (a * b), from pos_mul (to_pos H1) (to_pos H2),
|
|
|
|
|
begin rewrite -sub_zero at this, exact this end
|
2015-04-27 17:24:18 +00:00
|
|
|
|
|
2015-04-27 17:33:21 +00:00
|
|
|
|
definition decidable_lt [instance] : decidable_rel rat.lt :=
|
2015-04-27 17:24:18 +00:00
|
|
|
|
take a b, decidable_pos (b - a)
|
|
|
|
|
|
2015-10-23 02:18:14 +00:00
|
|
|
|
protected theorem le_of_lt (H : a < b) : a ≤ b := iff.mpr !rat.le_iff_lt_or_eq (or.inl H)
|
2015-05-29 04:09:13 +00:00
|
|
|
|
|
2015-10-23 02:18:14 +00:00
|
|
|
|
protected theorem lt_irrefl (a : ℚ) : ¬ a < a :=
|
2015-07-20 04:15:20 +00:00
|
|
|
|
take Ha,
|
2015-10-23 02:18:14 +00:00
|
|
|
|
let Hand := (iff.mp !rat.lt_iff_le_and_ne) Ha in
|
2015-05-29 04:09:13 +00:00
|
|
|
|
(and.right Hand) rfl
|
|
|
|
|
|
2015-10-23 02:18:14 +00:00
|
|
|
|
protected theorem not_le_of_gt (H : a < b) : ¬ b ≤ a :=
|
2015-07-20 04:15:20 +00:00
|
|
|
|
assume Hba,
|
2015-10-23 02:18:14 +00:00
|
|
|
|
let Heq := rat.le_antisymm (rat.le_of_lt H) Hba in
|
|
|
|
|
!rat.lt_irrefl (Heq ▸ H)
|
|
|
|
|
|
|
|
|
|
protected theorem lt_of_lt_of_le (Hab : a < b) (Hbc : b ≤ c) : a < c :=
|
|
|
|
|
let Hab' := rat.le_of_lt Hab in
|
|
|
|
|
let Hac := rat.le_trans Hab' Hbc in
|
|
|
|
|
(iff.mpr !rat.lt_iff_le_and_ne) (and.intro Hac
|
|
|
|
|
(assume Heq, rat.not_le_of_gt (Heq ▸ Hab) Hbc))
|
|
|
|
|
|
|
|
|
|
protected theorem lt_of_le_of_lt (Hab : a ≤ b) (Hbc : b < c) : a < c :=
|
|
|
|
|
let Hbc' := rat.le_of_lt Hbc in
|
|
|
|
|
let Hac := rat.le_trans Hab Hbc' in
|
|
|
|
|
(iff.mpr !rat.lt_iff_le_and_ne) (and.intro Hac
|
|
|
|
|
(assume Heq, rat.not_le_of_gt (Heq⁻¹ ▸ Hbc) Hab))
|
|
|
|
|
|
|
|
|
|
protected theorem zero_lt_one : (0 : ℚ) < 1 := trivial
|
|
|
|
|
|
|
|
|
|
protected theorem add_lt_add_left (H : a < b) (c : ℚ) : c + a < c + b :=
|
|
|
|
|
let H' := rat.le_of_lt H in
|
|
|
|
|
(iff.mpr (rat.lt_iff_le_and_ne _ _)) (and.intro (rat.add_le_add_left H' _)
|
2015-05-29 04:09:13 +00:00
|
|
|
|
(take Heq, let Heq' := add_left_cancel Heq in
|
2015-10-23 02:18:14 +00:00
|
|
|
|
!rat.lt_irrefl (Heq' ▸ H)))
|
2015-05-29 04:09:13 +00:00
|
|
|
|
|
2015-10-09 21:50:17 +00:00
|
|
|
|
protected definition discrete_linear_ordered_field [reducible] [trans_instance] :
|
2015-04-27 17:24:18 +00:00
|
|
|
|
algebra.discrete_linear_ordered_field rat :=
|
2015-10-09 01:35:37 +00:00
|
|
|
|
⦃algebra.discrete_linear_ordered_field,
|
|
|
|
|
rat.discrete_field,
|
2015-10-23 02:18:14 +00:00
|
|
|
|
le_refl := rat.le_refl,
|
|
|
|
|
le_trans := @rat.le_trans,
|
|
|
|
|
le_antisymm := @rat.le_antisymm,
|
|
|
|
|
le_total := @rat.le_total,
|
|
|
|
|
le_of_lt := @rat.le_of_lt,
|
|
|
|
|
lt_irrefl := rat.lt_irrefl,
|
|
|
|
|
lt_of_lt_of_le := @rat.lt_of_lt_of_le,
|
|
|
|
|
lt_of_le_of_lt := @rat.lt_of_le_of_lt,
|
|
|
|
|
le_iff_lt_or_eq := @rat.le_iff_lt_or_eq,
|
|
|
|
|
add_le_add_left := @rat.add_le_add_left,
|
|
|
|
|
mul_nonneg := @rat.mul_nonneg,
|
|
|
|
|
mul_pos := @rat.mul_pos,
|
2015-10-09 01:35:37 +00:00
|
|
|
|
decidable_lt := @decidable_lt,
|
2015-10-23 02:18:14 +00:00
|
|
|
|
zero_lt_one := rat.zero_lt_one,
|
|
|
|
|
add_lt_add_left := @rat.add_lt_add_left⦄
|
2015-06-16 03:13:43 +00:00
|
|
|
|
|
2015-09-13 00:04:57 +00:00
|
|
|
|
theorem of_nat_abs (a : ℤ) : abs (of_int a) = of_nat (int.nat_abs a) :=
|
2015-07-20 04:15:20 +00:00
|
|
|
|
assert ∀ n : ℕ, of_int (int.neg_succ_of_nat n) = - of_nat (nat.succ n), from λ n, rfl,
|
|
|
|
|
int.induction_on a
|
2015-09-12 14:00:34 +00:00
|
|
|
|
(take b, abs_of_nonneg !of_nat_nonneg)
|
|
|
|
|
(take b, by rewrite [this, abs_neg, abs_of_nonneg !of_nat_nonneg])
|
2015-06-16 03:13:43 +00:00
|
|
|
|
|
2015-09-13 00:04:57 +00:00
|
|
|
|
theorem eq_zero_of_nonneg_of_forall_lt {x : ℚ} (xnonneg : x ≥ 0) (H : ∀ ε, ε > 0 → x < ε) :
|
|
|
|
|
x = 0 :=
|
|
|
|
|
decidable.by_contradiction
|
|
|
|
|
(suppose x ≠ 0,
|
|
|
|
|
have x > 0, from lt_of_le_of_ne xnonneg (ne.symm this),
|
|
|
|
|
have x < x, from H x this,
|
|
|
|
|
show false, from !lt.irrefl this)
|
|
|
|
|
|
|
|
|
|
theorem eq_zero_of_nonneg_of_forall_le {x : ℚ} (xnonneg : x ≥ 0) (H : ∀ ε, ε > 0 → x ≤ ε) :
|
|
|
|
|
x = 0 :=
|
|
|
|
|
have H' : ∀ ε, ε > 0 → x < ε, from
|
2015-10-09 01:35:37 +00:00
|
|
|
|
take ε, suppose h₁ : ε > 0,
|
|
|
|
|
have ε / 2 > 0, from div_pos_of_pos_of_pos h₁ two_pos,
|
2015-09-13 00:04:57 +00:00
|
|
|
|
have x ≤ ε / 2, from H _ this,
|
2015-10-09 01:35:37 +00:00
|
|
|
|
show x < ε, from lt_of_le_of_lt this (div_two_lt_of_pos h₁),
|
2015-09-13 00:04:57 +00:00
|
|
|
|
eq_zero_of_nonneg_of_forall_lt xnonneg H'
|
|
|
|
|
|
|
|
|
|
theorem eq_zero_of_forall_abs_le {x : ℚ} (H : ∀ ε, ε > 0 → abs x ≤ ε) :
|
|
|
|
|
x = 0 :=
|
|
|
|
|
decidable.by_contradiction
|
|
|
|
|
(suppose x ≠ 0,
|
|
|
|
|
have abs x = 0, from eq_zero_of_nonneg_of_forall_le !abs_nonneg H,
|
|
|
|
|
show false, from `x ≠ 0` (eq_zero_of_abs_eq_zero this))
|
|
|
|
|
|
|
|
|
|
theorem eq_of_forall_abs_sub_le {x y : ℚ} (H : ∀ ε, ε > 0 → abs (x - y) ≤ ε) :
|
|
|
|
|
x = y :=
|
|
|
|
|
have x - y = 0, from eq_zero_of_forall_abs_le H,
|
|
|
|
|
eq_of_sub_eq_zero this
|
|
|
|
|
|
2015-08-17 03:23:03 +00:00
|
|
|
|
section
|
|
|
|
|
open int
|
|
|
|
|
|
|
|
|
|
theorem num_nonneg_of_nonneg {q : ℚ} (H : q ≥ 0) : num q ≥ 0 :=
|
|
|
|
|
have of_int (num q) ≥ of_int 0,
|
|
|
|
|
begin
|
|
|
|
|
rewrite [-mul_denom],
|
2015-10-23 02:18:14 +00:00
|
|
|
|
apply rat.mul_nonneg H,
|
2015-10-13 00:18:10 +00:00
|
|
|
|
rewrite [-of_int_zero, of_int_le_of_int_iff],
|
2015-08-17 03:23:03 +00:00
|
|
|
|
exact int.le_of_lt !denom_pos
|
|
|
|
|
end,
|
2015-09-12 14:00:34 +00:00
|
|
|
|
show num q ≥ 0, from le_of_of_int_le_of_int this
|
2015-08-17 03:23:03 +00:00
|
|
|
|
|
|
|
|
|
theorem num_pos_of_pos {q : ℚ} (H : q > 0) : num q > 0 :=
|
|
|
|
|
have of_int (num q) > of_int 0,
|
|
|
|
|
begin
|
|
|
|
|
rewrite [-mul_denom],
|
2015-10-23 02:18:14 +00:00
|
|
|
|
apply rat.mul_pos H,
|
2015-10-13 00:18:10 +00:00
|
|
|
|
rewrite [-of_int_zero, of_int_lt_of_int_iff],
|
2015-08-17 03:23:03 +00:00
|
|
|
|
exact !denom_pos
|
|
|
|
|
end,
|
2015-09-12 14:00:34 +00:00
|
|
|
|
show num q > 0, from lt_of_of_int_lt_of_int this
|
2015-08-17 03:23:03 +00:00
|
|
|
|
|
|
|
|
|
theorem num_neg_of_neg {q : ℚ} (H : q < 0) : num q < 0 :=
|
|
|
|
|
have of_int (num q) < of_int 0,
|
|
|
|
|
begin
|
|
|
|
|
rewrite [-mul_denom],
|
|
|
|
|
apply mul_neg_of_neg_of_pos H,
|
2015-10-09 01:35:37 +00:00
|
|
|
|
change of_int (denom q) > of_int 0,
|
2015-10-09 21:50:17 +00:00
|
|
|
|
xrewrite [of_int_lt_of_int_iff],
|
2015-08-17 03:23:03 +00:00
|
|
|
|
exact !denom_pos
|
|
|
|
|
end,
|
2015-09-12 14:00:34 +00:00
|
|
|
|
show num q < 0, from lt_of_of_int_lt_of_int this
|
2015-08-17 03:23:03 +00:00
|
|
|
|
|
|
|
|
|
theorem num_nonpos_of_nonpos {q : ℚ} (H : q ≤ 0) : num q ≤ 0 :=
|
|
|
|
|
have of_int (num q) ≤ of_int 0,
|
|
|
|
|
begin
|
|
|
|
|
rewrite [-mul_denom],
|
|
|
|
|
apply mul_nonpos_of_nonpos_of_nonneg H,
|
2015-10-09 01:35:37 +00:00
|
|
|
|
change of_int (denom q) ≥ of_int 0,
|
2015-10-09 21:50:17 +00:00
|
|
|
|
xrewrite [of_int_le_of_int_iff],
|
2015-08-17 03:23:03 +00:00
|
|
|
|
exact int.le_of_lt !denom_pos
|
|
|
|
|
end,
|
2015-09-12 14:00:34 +00:00
|
|
|
|
show num q ≤ 0, from le_of_of_int_le_of_int this
|
2015-08-17 03:23:03 +00:00
|
|
|
|
end
|
|
|
|
|
|
2015-06-16 03:13:43 +00:00
|
|
|
|
definition ubound : ℚ → ℕ := λ a : ℚ, nat.succ (int.nat_abs (num a))
|
|
|
|
|
|
|
|
|
|
theorem ubound_ge (a : ℚ) : of_nat (ubound a) ≥ a :=
|
2015-07-20 04:15:20 +00:00
|
|
|
|
have h : abs a * abs (of_int (denom a)) = abs (of_int (num a)), from
|
|
|
|
|
!abs_mul ▸ !mul_denom ▸ rfl,
|
2015-09-12 14:00:34 +00:00
|
|
|
|
assert of_int (denom a) > 0, from of_int_lt_of_int_of_lt !denom_pos,
|
2015-07-20 04:15:20 +00:00
|
|
|
|
have 1 ≤ abs (of_int (denom a)), begin
|
|
|
|
|
rewrite (abs_of_pos this),
|
2015-09-12 14:00:34 +00:00
|
|
|
|
apply of_int_le_of_int_of_le,
|
2015-06-16 03:13:43 +00:00
|
|
|
|
apply denom_pos
|
|
|
|
|
end,
|
2015-07-20 04:15:20 +00:00
|
|
|
|
have abs a ≤ abs (of_int (num a)), from
|
|
|
|
|
le_of_mul_le_of_ge_one (h ▸ !le.refl) !abs_nonneg this,
|
|
|
|
|
calc
|
|
|
|
|
a ≤ abs a : le_abs_self
|
|
|
|
|
... ≤ abs (of_int (num a)) : this
|
2015-10-09 01:35:37 +00:00
|
|
|
|
... ≤ abs (of_int (num a)) + 1 : le_add_of_nonneg_right trivial
|
2015-09-13 00:04:57 +00:00
|
|
|
|
... = of_nat (int.nat_abs (num a)) + 1 : of_nat_abs
|
2015-06-16 03:13:43 +00:00
|
|
|
|
... = of_nat (nat.succ (int.nat_abs (num a))) : of_nat_add
|
|
|
|
|
|
2015-10-09 01:35:37 +00:00
|
|
|
|
theorem ubound_pos (a : ℚ) : ubound a > 0 :=
|
|
|
|
|
!nat.succ_pos
|
|
|
|
|
|
|
|
|
|
open nat
|
2015-06-16 03:13:43 +00:00
|
|
|
|
|
2015-10-09 01:35:37 +00:00
|
|
|
|
theorem binary_nat_bound (a : ℕ) : of_nat a ≤ 2^a :=
|
2015-09-14 17:39:01 +00:00
|
|
|
|
nat.induction_on a (zero_le_one)
|
2015-10-09 01:35:37 +00:00
|
|
|
|
(take n : nat, assume Hn,
|
2015-09-14 17:39:01 +00:00
|
|
|
|
calc
|
|
|
|
|
of_nat (nat.succ n) = (of_nat n) + 1 : of_nat_add
|
2015-10-09 01:35:37 +00:00
|
|
|
|
... ≤ 2^n + 1 : algebra.add_le_add_right Hn
|
|
|
|
|
... ≤ 2^n + (2:rat)^n : add_le_add_left (pow_ge_one_of_ge_one two_ge_one _)
|
|
|
|
|
... = 2^(succ n) : pow_two_add)
|
2015-09-14 17:39:01 +00:00
|
|
|
|
|
2015-10-09 01:35:37 +00:00
|
|
|
|
theorem binary_bound (a : ℚ) : ∃ n : ℕ, a ≤ 2^n :=
|
2015-09-14 17:39:01 +00:00
|
|
|
|
exists.intro (ubound a) (calc
|
|
|
|
|
a ≤ of_nat (ubound a) : ubound_ge
|
2015-10-09 01:35:37 +00:00
|
|
|
|
... ≤ 2^(ubound a) : binary_nat_bound)
|
2015-09-14 17:39:01 +00:00
|
|
|
|
|
2015-04-27 17:24:18 +00:00
|
|
|
|
end rat
|