feat/refactor(library/data/{int,rat}/*): improve casting from nat to int to rat

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]

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]

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)
 

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)
 

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