From a64c0ea8458b0b7963a97f0f52be2b446766d56d Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Mon, 25 May 2015 21:52:20 +1000 Subject: [PATCH] feat/refactor(library/data/{int,rat}/*): improve casting from nat to int to rat --- library/data/int/basic.lean | 4 ++-- library/data/int/div.lean | 21 +++++++++++---------- library/data/int/order.lean | 26 ++++++++++++-------------- library/data/rat/basic.lean | 13 ++++++++++++- library/data/rat/order.lean | 33 +++++++++++++++++++++++++-------- 5 files changed, 62 insertions(+), 35 deletions(-) diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean index fb4524bbc..074223d99 100644 --- a/library/data/int/basic.lean +++ b/library/data/int/basic.lean @@ -643,10 +643,10 @@ end migrate_algebra /- additional properties -/ -theorem of_nat_sub_of_nat {m n : ℕ} (H : #nat m ≥ n) : of_nat m - of_nat n = of_nat (#nat m - n) := +theorem of_nat_sub {m n : ℕ} (H : #nat m ≥ n) : of_nat (#nat m - n) = of_nat m - of_nat n := have H1 : m = (#nat m - n + n), from (nat.sub_add_cancel H)⁻¹, have H2 : m = (#nat m - n) + n, from congr_arg of_nat H1, -sub_eq_of_eq_add H2 +(sub_eq_of_eq_add H2)⁻¹ theorem neg_succ_of_nat_eq' (m : ℕ) : -[m +1] = -m - 1 := by rewrite [neg_succ_of_nat_eq, of_nat_add, neg_add] diff --git a/library/data/int/div.lean b/library/data/int/div.lean index 203fcec9d..783fbf371 100644 --- a/library/data/int/div.lean +++ b/library/data/int/div.lean @@ -182,14 +182,14 @@ have H1 : abs b > 0, from abs_pos_of_ne_zero H, have H2 : (#nat nat_abs b > 0), from lt_of_of_nat_lt_of_nat (!of_nat_nat_abs⁻¹ ▸ H1), calc m mod (abs b) = (#nat m mod (nat_abs b)) : of_nat_mod_abs m b - ... < nat_abs b : of_nat_lt_of_nat (nat.mod_lt H2) + ... < nat_abs b : of_nat_lt_of_nat_of_lt (nat.mod_lt H2) ... = abs b : of_nat_nat_abs _ theorem mod_nonneg (a : ℤ) {b : ℤ} (H : b ≠ 0) : a mod b ≥ 0 := have H1 : abs b > 0, from abs_pos_of_ne_zero H, have H2 : a mod (abs b) ≥ 0, from int.cases_on a - (take m, (of_nat_mod_abs m b)⁻¹ ▸ !of_nat_nonneg) + (take m, (of_nat_mod_abs m b)⁻¹ ▸ of_nat_nonneg (nat.modulo m (nat_abs b))) (take m, have H3 : 1 + m mod (abs b) ≤ (abs b), from (!add.comm ▸ add_one_le_of_lt (of_nat_mod_abs_lt m H)), @@ -238,21 +238,21 @@ or.elim (nat.lt_or_ge m (#nat n * k)) Hm⁻¹ ▸ (calc (-[m +1] + n * k) div k = (n * k - (m + 1)) div k : by rewrite [add.comm, neg_succ_of_nat_eq] ... = ((#nat n * k) - (#nat m + 1)) div k : rfl - ... = (#nat n * k - (m + 1)) div k : {of_nat_sub_of_nat H3} + ... = (#nat n * k - (m + 1)) div k : {(of_nat_sub H3)⁻¹} ... = #nat (n * k - (m + 1)) div k : of_nat_div_of_nat ... = #nat (k * n - (m + 1)) div k : nat.mul.comm ... = #nat n - m div k - 1 : nat.mul_sub_div_of_lt (!nat.mul.comm ▸ m_lt_nk) ... = #nat n - (m div k + 1) : nat.sub_sub - ... = n - (#nat m div k + 1) : of_nat_sub_of_nat H4 + ... = n - (#nat m div k + 1) : of_nat_sub H4 ... = -(m div k + 1) + n : by rewrite [add.comm, -sub_eq_add_neg, of_nat_add, of_nat_div_of_nat] ... = -[m +1] div k + n : - neg_succ_of_nat_div m (of_nat_lt_of_nat H2))) + neg_succ_of_nat_div m (of_nat_lt_of_nat_of_lt H2))) (assume nk_le_m : #nat n * k ≤ m, eq.symm (Hm⁻¹ ▸ (calc -[m +1] div k + n = -(m div k + 1) + n : - neg_succ_of_nat_div m (of_nat_lt_of_nat H2) + neg_succ_of_nat_div m (of_nat_lt_of_nat_of_lt H2) ... = -((#nat m div k) + 1) + n : of_nat_div_of_nat ... = -((#nat (m - n * k + n * k) div k) + 1) + n : nat.sub_add_cancel nk_le_m ... = -((#nat (m - n * k) div k + n) + 1) + n : nat.add_mul_div_self H2 @@ -260,9 +260,9 @@ or.elim (nat.lt_or_ge m (#nat n * k)) by rewrite [of_nat_add, *neg_add, add.right_comm, neg_add_cancel_right, of_nat_div_of_nat] ... = -[(#nat m - n * k) +1] div k : - neg_succ_of_nat_div _ (of_nat_lt_of_nat H2) + neg_succ_of_nat_div _ (of_nat_lt_of_nat_of_lt H2) ... = -((#nat m - n * k) + 1) div k : rfl - ... = -(m - (#nat n * k) + 1) div k : of_nat_sub_of_nat nk_le_m + ... = -(m - (#nat n * k) + 1) div k : of_nat_sub nk_le_m ... = (-(m + 1) + n * k) div k : by rewrite [sub_eq_add_neg, -*add.assoc, *neg_add, neg_neg, add.right_comm] ... = (-[m +1] + n * k) div k : rfl))) @@ -378,7 +378,7 @@ obtain (m : ℕ) (Hm : a = m), from exists_eq_of_nat Ha, obtain (n : ℕ) (Hn : b = n), from exists_eq_of_nat Hb, calc a div b = #nat m div n : by rewrite [Hm, Hn, of_nat_div_of_nat] - ... ≤ m : of_nat_le_of_nat !nat.div_le + ... ≤ m : of_nat_le_of_nat_of_le !nat.div_le ... = a : Hm theorem abs_div_le_abs (a b : ℤ) : abs (a div b) ≤ abs a := @@ -394,7 +394,8 @@ have H : ∀a b, b > 0 → abs (a div b) ≤ abs a, from ... = abs a : abs_of_nonneg H2) (assume H2 : a < 0, have H3 : -a - 1 ≥ 0, from le_sub_one_of_lt (neg_pos_of_neg H2), - have H4 : (-a - 1) div b + 1 ≥ 0, from add_nonneg (div_nonneg H3 (le_of_lt H1)) (of_nat_le_of_nat !nat.zero_le), + have H4 : (-a - 1) div b + 1 ≥ 0, + from add_nonneg (div_nonneg H3 (le_of_lt H1)) (of_nat_le_of_nat_of_le !nat.zero_le), have H5 : (-a - 1) div b ≤ -a - 1, from div_le_of_nonneg_of_nonneg H3 (le_of_lt H1), calc abs (a div b) = abs ((-a - 1) div b + 1) : by rewrite [div_of_neg_of_pos H2 H1, abs_neg] diff --git a/library/data/int/order.lean b/library/data/int/order.lean index 1c154b1e9..5be61940c 100644 --- a/library/data/int/order.lean +++ b/library/data/int/order.lean @@ -51,7 +51,7 @@ or.elim (nonneg_or_nonneg_neg (b - a)) have H1 : nonneg (a - b), from H0 ▸ H, -- too bad: can't do it in one step or.inr H1) -theorem of_nat_le_of_nat {m n : ℕ} (H : #nat m ≤ n) : of_nat m ≤ of_nat n := +theorem of_nat_le_of_nat_of_le {m n : ℕ} (H : #nat m ≤ n) : of_nat m ≤ of_nat n := obtain (k : ℕ) (Hk : m + k = n), from nat.le.elim H, le.intro (Hk ▸ (of_nat_add m k)⁻¹) @@ -60,8 +60,8 @@ obtain (k : ℕ) (Hk : of_nat m + of_nat k = of_nat n), from le.elim H, have H1 : m + k = n, from of_nat.inj (of_nat_add m k ⬝ Hk), nat.le.intro H1 -theorem of_nat_le_of_nat_iff (m n : ℕ) : of_nat m ≤ of_nat n ↔ m ≤ n := -iff.intro le_of_of_nat_le_of_nat of_nat_le_of_nat +theorem of_nat_le_of_nat (m n : ℕ) : of_nat m ≤ of_nat n ↔ m ≤ n := +iff.intro le_of_of_nat_le_of_nat of_nat_le_of_nat_of_le theorem lt_add_succ (a : ℤ) (n : ℕ) : a < a + succ n := le.intro (show a + 1 + n = a + succ n, from @@ -81,18 +81,18 @@ have H2 : a + succ n = b, from ... = b : Hn, exists.intro n H2 -theorem of_nat_lt_of_nat_iff (n m : ℕ) : of_nat n < of_nat m ↔ n < m := +theorem of_nat_lt_of_nat (n m : ℕ) : of_nat n < of_nat m ↔ n < m := calc of_nat n < of_nat m ↔ of_nat n + 1 ≤ of_nat m : iff.refl ... ↔ of_nat (succ n) ≤ of_nat m : of_nat_succ n ▸ !iff.refl - ... ↔ succ n ≤ m : of_nat_le_of_nat_iff + ... ↔ succ n ≤ m : of_nat_le_of_nat ... ↔ n < m : iff.symm (lt_iff_succ_le _ _) theorem lt_of_of_nat_lt_of_nat {m n : ℕ} (H : of_nat m < of_nat n) : #nat m < n := -iff.mp !of_nat_lt_of_nat_iff H +iff.mp !of_nat_lt_of_nat H -theorem of_nat_lt_of_nat {m n : ℕ} (H : #nat m < n) : of_nat m < of_nat n := -iff.mp' !of_nat_lt_of_nat_iff H +theorem of_nat_lt_of_nat_of_lt {m n : ℕ} (H : #nat m < n) : of_nat m < of_nat n := +iff.mp' !of_nat_lt_of_nat H /- show that the integers form an ordered additive group -/ @@ -266,7 +266,10 @@ end migrate_algebra /- more facts specific to int -/ -theorem nonneg_of_nat (n : ℕ) : 0 ≤ of_nat n := trivial +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 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, @@ -321,11 +324,6 @@ le_of_lt_add_one (!sub_add_cancel⁻¹ ▸ H) theorem lt_of_le_sub_one {a b : ℤ} (H : a ≤ b - 1) : a < b := !sub_add_cancel ▸ (lt_add_one_of_le H) -theorem of_nat_nonneg (n : ℕ) : of_nat n ≥ 0 := trivial - -theorem of_nat_pos {n : ℕ} (Hpos : #nat n > 0) : of_nat n > 0 := -of_nat_lt_of_nat Hpos - theorem sign_of_succ (n : nat) : sign (succ n) = 1 := sign_of_pos (of_nat_pos !nat.succ_pos) diff --git a/library/data/rat/basic.lean b/library/data/rat/basic.lean index 3c0966de7..1469bbbb4 100644 --- a/library/data/rat/basic.lean +++ b/library/data/rat/basic.lean @@ -74,7 +74,7 @@ setoid.mk equiv equiv.is_equivalence /- field operations -/ -private theorem of_nat_succ_pos (n : nat) : of_nat (nat.succ n) > 0 := +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 @@ -333,6 +333,17 @@ 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_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 := +by rewrite [*of_nat_eq, int.of_nat_add, rat.of_int_add] + +theorem of_nat_mul (a b : ℕ) : of_nat (#nat a * b) = of_nat a * of_nat b := +by rewrite [*of_nat_eq, int.of_nat_mul, rat.of_int_mul] + +theorem of_nat_sub {a b : ℕ} (H : #nat a ≥ b) : of_nat (#nat a - b) = of_nat a - of_nat b := +by rewrite [*of_nat_eq, int.of_nat_sub H, rat.of_int_sub] + theorem add.comm (a b : ℚ) : a + b = b + a := quot.induction_on₂ a b (take u v, quot.sound !prerat.add.comm) diff --git a/library/data/rat/order.lean b/library/data/rat/order.lean index e43ab8af8..65a05d7b3 100644 --- a/library/data/rat/order.lean +++ b/library/data/rat/order.lean @@ -153,19 +153,35 @@ infix >= := rat.ge infix ≥ := rat.ge infix > := rat.gt -theorem of_int_lt_of_int (a b : ℤ) : (#int a < b) ↔ of_int a < of_int b := -calc +theorem of_int_lt_of_int (a b : ℤ) : of_int a < of_int b ↔ (#int a < b) := +iff.symm (calc (#int a < b) ↔ (#int b - a > 0) : iff.symm !int.sub_pos_iff_lt ... ↔ pos (of_int (#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 + ... ↔ of_int a < of_int b : iff.rfl) -theorem of_int_le_of_int (a b : ℤ) : (#int a ≤ b) ↔ of_int a ≤ of_int b := -calc +theorem of_int_le_of_int (a b : ℤ) : of_int a ≤ of_int b ↔ (#int a ≤ b) := +iff.symm (calc (#int a ≤ b) ↔ (#int b - a ≥ 0) : iff.symm !int.sub_nonneg_iff_le ... ↔ nonneg (of_int (#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 + ... ↔ of_int a ≤ of_int b : iff.rfl) + +theorem of_int_pos (a : ℤ) : (of_int a > 0) ↔ (#int a > 0) := !of_int_lt_of_int + +theorem of_int_nonneg (a : ℤ) : (of_int a ≥ 0) ↔ (#int a ≥ 0) := !of_int_le_of_int + +theorem of_nat_lt_of_nat (a b : ℕ) : of_nat a < of_nat b ↔ (#nat a < b) := +by rewrite [*of_nat_eq, propext !of_int_lt_of_int]; apply int.of_nat_lt_of_nat + +theorem of_nat_le_of_nat (a b : ℕ) : of_nat a ≤ of_nat b ↔ (#nat a ≤ b) := +by rewrite [*of_nat_eq, propext !of_int_le_of_int]; apply int.of_nat_le_of_nat + +theorem of_nat_pos (a : ℕ) : (of_nat a > 0) ↔ (#nat a > nat.zero) := +!of_nat_lt_of_nat + +theorem of_nat_nonneg (a : ℕ) : (of_nat a ≥ 0) ↔ (#nat a ≥ nat.zero) := +!of_nat_le_of_nat theorem le.refl (a : ℚ) : a ≤ a := by rewrite [↑rat.le, sub_self]; apply nonneg_zero @@ -249,7 +265,8 @@ section migrate_algebra definition abs (n : rat) : rat := algebra.abs n definition sign (n : rat) : rat := algebra.sign n --- migrate from algebra with rat --- replacing has_le.ge → ge, has_lt.gt → gt, sub → sub, abs → abs, sign → sign, dvd → dvd, divide → divide + migrate from algebra with rat + replacing has_le.ge → ge, has_lt.gt → gt, sub → sub, abs → abs, sign → sign, dvd → dvd, + divide → divide end migrate_algebra end rat