michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/data/rat/order): define abs and sign for rat before migrate

Browse source
This commit is contained in:
Leonardo de Moura 2015-04-27 12:59:02 -07:00
parent d41e055d1c
commit 17c07cdb02
1 changed files with 12 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

23
library/data/rat/order.lean
View file

@ -40,8 +40,8 @@ calc
theorem nonneg_zero : nonneg zero := le.refl 0 theorem nonneg_zero : nonneg zero := le.refl 0
theorem nonneg_add (H1 : nonneg a) (H2 : nonneg b) : nonneg (add a b) := theorem nonneg_add (H1 : nonneg a) (H2 : nonneg b) : nonneg (add a b) :=
show num a * denom b + num b * denom a ≥ 0, show num a * denom b + num b * denom a ≥ 0,
from add_nonneg from add_nonneg
(mul_nonneg H1 (le_of_lt (denom_pos b))) (mul_nonneg H1 (le_of_lt (denom_pos b)))
(mul_nonneg H2 (le_of_lt (denom_pos a))) (mul_nonneg H2 (le_of_lt (denom_pos a)))
@ -60,7 +60,7 @@ theorem ne_zero_of_pos (H : pos a) : ¬ a ≡ zero :=
assume H', ne_of_gt H (num_eq_zero_of_equiv_zero H') 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 := theorem pos_of_nonneg_of_ne_zero (H1 : nonneg a) (H2 : ¬ a ≡ zero) : pos a :=
have H3 : num a ≠ 0, have H3 : num a ≠ 0,
from assume H' : num a = 0, H2 (equiv_zero_of_num_eq_zero H'), from assume H' : num a = 0, H2 (equiv_zero_of_num_eq_zero H'),
lt_of_le_of_ne H1 (ne.symm H3) lt_of_le_of_ne H1 (ne.symm H3)
@ -77,7 +77,7 @@ local attribute prerat.setoid [instance]
/- The ordering on the rationals. /- The ordering on the rationals.
The definitions of pos and nonneg are kept private, because they are only meant for internal The definitions of pos and nonneg are kept private, because they are only meant for internal
use. Users should use a > 0 and a ≥ 0 instead of pos and nonneg. use. Users should use a > 0 and a ≥ 0 instead of pos and nonneg.
-/ -/
@ -109,7 +109,7 @@ quot.induction_on a @prerat.nonneg_total
private theorem nonneg_of_pos : pos a → nonneg a := private theorem nonneg_of_pos : pos a → nonneg a :=
quot.induction_on a @prerat.nonneg_of_pos quot.induction_on a @prerat.nonneg_of_pos
private theorem ne_zero_of_pos : pos a → a ≠ 0 := private theorem ne_zero_of_pos : pos a → a ≠ 0 :=
quot.induction_on a (take u, assume H1 H2, prerat.ne_zero_of_pos H1 (quot.exact H2)) 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 := private theorem pos_of_nonneg_of_ne_zero : nonneg a → ¬ a = 0 → pos a :=
@ -134,7 +134,7 @@ quot.rec_on_subsingleton a (take u, int.decidable_lt 0 (prerat.num u))
definition lt (a b : ℚ) : Prop := pos (b - a) definition lt (a b : ℚ) : Prop := pos (b - a)
definition le (a b : ℚ) : Prop := nonneg (b - a) definition le (a b : ℚ) : Prop := nonneg (b - a)
definition gt [reducible] (a b : ℚ) := lt b a definition gt [reducible] (a b : ℚ) := lt b a
definition ge [reducible] (a b : ℚ) := le b a definition ge [reducible] (a b : ℚ) := le b a
infix < := rat.lt infix < := rat.lt
infix <= := rat.le infix <= := rat.le
@ -143,7 +143,7 @@ infix >= := rat.ge
infix ≥ := rat.ge infix ≥ := rat.ge
infix > := rat.gt infix > := rat.gt
theorem le.refl (a : ℚ) : a ≤ a := theorem le.refl (a : ℚ) : a ≤ a :=
by rewrite [↑rat.le, sub_self]; apply nonneg_zero by rewrite [↑rat.le, sub_self]; apply nonneg_zero
theorem le.trans (H1 : a ≤ b) (H2 : b ≤ c) : a ≤ c := theorem le.trans (H1 : a ≤ b) (H2 : b ≤ c) : a ≤ c :=
@ -166,7 +166,7 @@ or.elim (nonneg_total (b - a))
theorem lt_iff_le_and_ne (a b : ℚ) : a < b ↔ a ≤ b ∧ a ≠ b := theorem lt_iff_le_and_ne (a b : ℚ) : a < b ↔ a ≤ b ∧ a ≠ b :=
iff.intro iff.intro
(assume H : a < b, (assume H : a < b,
have H1 : b - a ≠ 0, from ne_zero_of_pos H, have H1 : b - a ≠ 0, from ne_zero_of_pos H,
have H2 : a ≠ b, from ne.symm (assume H', H1 (H' ▸ !sub_self)), have H2 : a ≠ b, from ne.symm (assume H', H1 (H' ▸ !sub_self)),
and.intro (nonneg_of_pos H) H2) and.intro (nonneg_of_pos H) H2)
@ -204,7 +204,7 @@ take a b, decidable_pos (b - a)
section section
open [classes] algebra open [classes] algebra
protected definition discrete_linear_ordered_field [instance] [reducible] : protected definition discrete_linear_ordered_field [instance] [reducible] :
algebra.discrete_linear_ordered_field rat := algebra.discrete_linear_ordered_field rat :=
⦃algebra.discrete_linear_ordered_field, ⦃algebra.discrete_linear_ordered_field,
rat.discrete_field, rat.discrete_field,
@ -219,7 +219,8 @@ section
mul_pos := @mul_pos, mul_pos := @mul_pos,
decidable_lt := @decidable_lt⦄ decidable_lt := @decidable_lt⦄
-- migrate from algebra with rat definition abs (n : rat) : rat := algebra.abs n
definition sign (n : rat) : rat := algebra.sign n
migrate from algebra with rat replacing abs → abs, sign → sign
end end
end rat end rat