feat(library/data/rat/{basic,order}.lean): add property of of_int

library/data/rat/basic.lean

@@ -97,6 +97,15 @@ prerat.mk (num a * num b) (denom a * denom b) (mul_denom_pos a b)
 definition neg (a : prerat) : prerat :=
 prerat.mk (- num a) (denom a) (denom_pos a)
 
+theorem of_int_add (a b : ℤ) : of_int (#int a + b) ≡ add (of_int a) (of_int b) :=
+by esimp [equiv, num, denom, one, add, of_int]; rewrite [*int.mul_one]
+
+theorem of_int_mul (a b : ℤ) : of_int (#int a * b) ≡ mul (of_int a) (of_int b) :=
+!equiv.refl
+
+theorem of_int_neg (a : ℤ) : of_int (#int -a) ≡ neg (of_int a) :=
+!equiv.refl
+
 definition inv : prerat → prerat
 | inv (prerat.mk nat.zero d dp) := zero
 | inv (prerat.mk (nat.succ n) d dp) := prerat.mk d (nat.succ n) !of_nat_succ_pos
@@ -312,6 +321,20 @@ notation 1 := one
 
 /- properties -/
 
+theorem of_int_add (a b : ℤ) : of_int (#int a + b) = of_int a + of_int b :=
+quot.sound (prerat.of_int_add a b)
+
+theorem of_int_mul (a b : ℤ) : of_int (#int a * b) = of_int a * of_int b :=
+quot.sound (prerat.of_int_mul a b)
+
+theorem of_int_neg (a : ℤ) : of_int (#int -a) = -(of_int a) :=
+quot.sound (prerat.of_int_neg a)
+
+theorem of_int_sub (a b : ℤ) : of_int (#int a - b) = of_int a - of_int b :=
+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 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

@@ -21,11 +21,17 @@ variables {a b : prerat}
 
 definition pos (a : prerat) : Prop := num a > 0
 
+definition nonneg (a : prerat) : Prop := num a ≥ 0
+
+theorem pos_of_int (a : ℤ) : pos (of_int a) ↔ (#int a > 0) :=
+!iff.rfl
+
+theorem nonneg_of_int (a : ℤ) : nonneg (of_int a) ↔ (#int a ≥ 0) :=
+!iff.rfl
+
 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⁻¹))
 
-definition nonneg (a : prerat) : Prop := num a ≥ 0
-
 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
@@ -93,6 +99,12 @@ 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
 
+private theorem pos_of_int (a : ℤ) : (#int a > 0) ↔ pos (of_int a) :=
+prerat.pos_of_int a
+
+private theorem nonneg_of_int (a : ℤ) : (#int a ≥ 0) ↔ nonneg (of_int a) :=
+prerat.nonneg_of_int a
+
 private theorem nonneg_zero : nonneg 0 := prerat.nonneg_zero
 
 private theorem nonneg_add : nonneg a → nonneg b → nonneg (a + b) :=
@@ -143,6 +155,20 @@ 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
+  (#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
+
+theorem of_int_le_of_int (a b : ℤ) : (#int a ≤ b) ↔ of_int a ≤ of_int b :=
+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
+
 theorem le.refl (a : ℚ) : a ≤ a :=
 by rewrite [↑rat.le, sub_self]; apply nonneg_zero
 
@@ -225,7 +251,7 @@ 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