From 6dfcc4610bbd42c493d5701a41a7527431ff3223 Mon Sep 17 00:00:00 2001 From: Rob Lewis Date: Fri, 29 May 2015 13:34:57 +1000 Subject: [PATCH] feat(data): update orderings on int and nat to conform to new algebraic hierarchy --- library/data/int/order.lean | 37 +++++++++++++++++++++++++++++++++++-- library/data/nat/order.lean | 11 ++++++++++- 2 files changed, 45 insertions(+), 3 deletions(-) diff --git a/library/data/int/order.lean b/library/data/int/order.lean index 4f5d3b135..2330ce129 100644 --- a/library/data/int/order.lean +++ b/library/data/int/order.lean @@ -34,6 +34,7 @@ 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, @@ -189,6 +190,12 @@ have H2 : c + a + n = c + b, from ... = c + b : {Hn}, le.intro H2 +theorem add_lt_add_left {a b : ℤ} (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))) + theorem mul_nonneg {a b : ℤ} (Ha : 0 ≤ a) (Hb : 0 ≤ b) : 0 ≤ a * b := obtain (n : ℕ) (Hn : 0 + n = a), from le.elim Ha, obtain (m : ℕ) (Hm : 0 + m = b), from le.elim Hb, @@ -216,6 +223,27 @@ lt.intro ... = of_nat (nat.succ (nat.succ n * m + n)) : nat.add_succ ... = 0 + nat.succ (nat.succ n * m + n) : zero_add)) + +theorem zero_lt_one : (0 : ℤ) < 1 := + by rewrite [↑lt, zero_add]; apply le.refl + +theorem not_le_of_gt {a b : ℤ} (H : a < b) : ¬ b ≤ a := + assume Hba, + let Heq := le.antisymm (le_of_lt H) Hba in + !lt.irrefl (Heq ▸ H) + +theorem lt_of_lt_of_le {a b c : ℤ} (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 + (assume Heq, not_le_of_gt (Heq ▸ Hab) Hbc)) + +theorem lt_of_le_of_lt {a b c : ℤ} (Hab : a ≤ b) (Hbc : b < c) : a < c := + let Hbc' := le_of_lt Hbc in + let Hac := le.trans Hab Hbc' in + (iff.mp' !lt_iff_le_and_ne) (and.intro Hac + (assume Heq, not_le_of_gt (Heq⁻¹ ▸ Hbc) Hab)) + section migrate_algebra open [classes] algebra @@ -227,13 +255,18 @@ section migrate_algebra le_trans := @le.trans, le_antisymm := @le.antisymm, lt := lt, - lt_iff_le_and_ne := lt_iff_le_and_ne, + le_of_lt := @le_of_lt, + lt_irrefl := lt.irrefl, + lt_of_lt_of_le := @lt_of_lt_of_le, + lt_of_le_of_lt := @lt_of_le_of_lt, add_le_add_left := @add_le_add_left, mul_nonneg := @mul_nonneg, mul_pos := @mul_pos, le_iff_lt_or_eq := le_iff_lt_or_eq, le_total := le.total, - zero_ne_one := zero_ne_one⦄ + zero_ne_one := zero_ne_one, + zero_lt_one := zero_lt_one, + add_lt_add_left := @add_lt_add_left⦄ protected definition decidable_linear_ordered_comm_ring [reducible] : algebra.decidable_linear_ordered_comm_ring int := diff --git a/library/data/nat/order.lean b/library/data/nat/order.lean index 299f56db3..0cde8426a 100644 --- a/library/data/nat/order.lean +++ b/library/data/nat/order.lean @@ -90,6 +90,10 @@ le.intro (add.cancel_left k + (n + l) = k + n + l : add.assoc ... = k + m : Hl)) +theorem lt_of_add_lt_add_left {k n m : ℕ} (H : k + n < k + m) : n < m := +let H' := le_of_lt H in +lt_of_le_and_ne (le_of_add_le_add_left H') (assume Heq, !lt.irrefl (Heq ▸ H)) + theorem add_lt_add_left {n m : ℕ} (H : n < m) (k : ℕ) : k + n < k + m := lt_of_succ_le (!add_succ ▸ add_le_add_left (succ_le_of_lt H) k) @@ -157,7 +161,12 @@ section migrate_algebra le_antisymm := @le.antisymm, le_total := @le.total, le_iff_lt_or_eq := @le_iff_lt_or_eq, - lt_iff_le_and_ne := lt_iff_le_and_ne, + le_of_lt := @le_of_lt, + lt_irrefl := @lt.irrefl, + lt_of_lt_of_le := @lt_of_lt_of_le, + lt_of_le_of_lt := @lt_of_le_of_lt, + lt_of_add_lt_add_left := @lt_of_add_lt_add_left, + add_lt_add_left := @add_lt_add_left, add_le_add_left := @add_le_add_left, le_of_add_le_add_left := @le_of_add_le_add_left, zero_ne_one := ne.symm (succ_ne_zero zero),