feat(library/data/int/{div,gcd}): add some theorems, to reduce rationals

library/algebra/ordered_ring.lean

@@ -154,6 +154,36 @@ section
     (assume H2 : a ≤ 0,
       have H3 : a * b ≤ 0, from mul_nonpos_of_nonpos_of_nonneg H2 H1,
       not_lt_of_ge H3 H)
+
+  theorem nonneg_of_mul_nonneg_left (H : 0 ≤ a * b) (H1 : 0 < a) : 0 ≤ b :=
+  le_of_not_gt
+    (assume H2 : b < 0,
+      not_le_of_gt (mul_neg_of_pos_of_neg H1 H2) H)
+
+  theorem nonneg_of_mul_nonneg_right (H : 0 ≤ a * b) (H1 : 0 < b) : 0 ≤ a :=
+  le_of_not_gt
+    (assume H2 : a < 0,
+      not_le_of_gt (mul_neg_of_neg_of_pos H2 H1) H)
+
+  theorem neg_of_mul_neg_left (H : a * b < 0) (H1 : 0 ≤ a) : b < 0 :=
+  lt_of_not_ge
+    (assume H2 : b ≥ 0,
+      not_lt_of_ge (mul_nonneg H1 H2) H)
+
+  theorem neg_of_mul_neg_right (H : a * b < 0) (H1 : 0 ≤ b) : a < 0 :=
+  lt_of_not_ge
+    (assume H2 : a ≥ 0,
+      not_lt_of_ge (mul_nonneg H2 H1) H)
+
+  theorem nonpos_of_mul_nonpos_left (H : a * b ≤ 0) (H1 : 0 < a) : b ≤ 0 :=
+  le_of_not_gt
+    (assume H2 : b > 0,
+      not_le_of_gt (mul_pos H1 H2) H)
+
+  theorem nonpos_of_mul_nonpos_right (H : a * b ≤ 0) (H1 : 0 < b) : a ≤ 0 :=
+  le_of_not_gt
+    (assume H2 : a > 0,
+      not_le_of_gt (mul_pos H2 H1) H)
 end
 
 structure ordered_ring [class] (A : Type) extends ring A, ordered_comm_group A, zero_ne_one_class A :=

library/data/int/div.lean

@@ -539,6 +539,14 @@ theorem div_eq_of_eq_mul_left {a b c : ℤ} (H1 : b ≠ 0) (H2 : a = c * b) :
   a div b = c :=
 div_eq_of_eq_mul_right H1 (!mul.comm ▸ H2)
 
+theorem neg_div_of_dvd {a b : ℤ} (H : b ∣ a) : -a div b = -(a div b) :=
+decidable.by_cases
+  (assume H1 : b = 0, by rewrite [H1, *div_zero, neg_zero])
+  (assume H1 : b ≠ 0,
+    dvd.elim H
+      (take c, assume H' : a = b * c,
+        by rewrite [H', neg_mul_eq_mul_neg, *!mul_div_cancel_left H1]))
+
 /- div and ordering -/
 
 theorem div_mul_le (a : ℤ) {b : ℤ} (H : b ≠ 0) : a div b * b ≤ a :=
@@ -613,4 +621,23 @@ theorem le_mul_of_div_le_of_div {a b c : ℤ} (H1 : b > 0) (H2 : b ∣ a) (H3 :
   a ≤ c * b :=
 iff.mp (!div_le_iff_le_mul_of_div H1 H2) H3
 
+theorem div_pos_of_pos_of_dvd {a b : ℤ} (H1 : a > 0) (H2 : b ≥ 0) (H3 : b ∣ a) : a div b > 0 :=
+have H4 : b ≠ 0, from
+  (assume H5 : b = 0,
+    have H6 : a = 0, from eq_zero_of_zero_dvd (H5 ▸ H3),
+    ne_of_gt H1 H6),
+have H6 : (a div b) * b > 0, by rewrite (div_mul_cancel H3); apply H1,
+pos_of_mul_pos_right H6 H2
+
+theorem div_eq_div_of_dvd_of_dvd {a b c d : ℤ} (H1 : b ∣ a) (H2 : d ∣ c) (H3 : b ≠ 0)
+    (H4 : d ≠ 0) (H5 : a * d = b * c) :
+  a div b = c div d :=
+begin
+  apply div_eq_of_eq_mul_right H3,
+  rewrite [-!mul_div_assoc H2],
+  apply eq.symm,
+  apply div_eq_of_eq_mul_left H4,
+  apply eq.symm H5
+end
+
 end int

library/data/int/gcd.lean

@@ -133,6 +133,55 @@ dvd_gcd (dvd.trans !gcd_dvd_left !dvd_mul_left) !gcd_dvd_right
 theorem gcd_dvd_gcd_mul_right (a b c : ℤ) : gcd a b ∣ gcd (a * c) b :=
 !mul.comm ▸ !gcd_dvd_gcd_mul_left
 
+theorem div_gcd_eq_div_gcd_of_nonneg {a₁ b₁ a₂ b₂ : ℤ} (H : a₁ * b₂ = b₁ * a₂)
+    (H1 : b₁ ≠ 0) (H2 : b₂ ≠ 0) (H3 : a₁ ≥ 0) (H4 : a₂ ≥ 0) :
+  a₁ div (gcd a₁ b₁) = a₂ div (gcd a₂ b₂) :=
+begin
+  apply div_eq_div_of_dvd_of_dvd,
+  repeat (apply gcd_dvd_left),
+  intro H', apply H1, apply eq_zero_of_gcd_eq_zero_right H',
+  intro H', apply H2, apply eq_zero_of_gcd_eq_zero_right H',
+  rewrite [-abs_of_nonneg H3 at {1}, -abs_of_nonneg H4 at {2}],
+  rewrite [-gcd_mul_left, -gcd_mul_right, H]
+end
+
+theorem div_gcd_eq_div_gcd {a₁ b₁ a₂ b₂ : ℤ} (H : a₁ * b₂ = b₁ * a₂) (H1 : b₁ > 0) (H2 : b₂ > 0) :
+  a₁ div (gcd a₁ b₁) = a₂ div (gcd a₂ b₂) :=
+or.elim (le_or_gt 0 a₁)
+  (assume H3 : a₁ ≥ 0,
+    have H4 : b₁ * a₂ ≥ 0, by rewrite -H; apply mul_nonneg H3 (le_of_lt H2),
+    have H5 : a₂ ≥ 0, from nonneg_of_mul_nonneg_left H4 H1,
+    div_gcd_eq_div_gcd_of_nonneg H (ne_of_gt H1) (ne_of_gt H2) H3 H5)
+  (assume H3 : a₁ < 0,
+    have H4 : b₁ * a₂ < 0, by rewrite -H; apply mul_neg_of_neg_of_pos H3 H2,
+    assert H5 : a₂ < 0, from neg_of_mul_neg_left H4 (le_of_lt H1),
+    assert H6 : abs a₁ div (gcd (abs a₁) (abs b₁)) = abs a₂ div (gcd (abs a₂) (abs b₂)),
+      begin
+        apply div_gcd_eq_div_gcd_of_nonneg,
+        rewrite [abs_of_pos H1, abs_of_pos H2, abs_of_neg H3, abs_of_neg H5],
+        rewrite [-neg_mul_eq_mul_neg, -neg_mul_eq_neg_mul, H],
+        apply ne_of_gt (abs_pos_of_pos H1),
+        apply ne_of_gt (abs_pos_of_pos H2),
+        repeat (apply abs_nonneg)
+      end,
+    have H7 : -a₁ div (gcd a₁ b₁) = -a₂ div (gcd a₂ b₂),
+      begin
+--        TODO: if you uncomment the next two lines, and comment out the three after it,
+--              it takes Lean 40 seconds to process the file. (The rewrites are succeed,
+--              but do not finish off the goal.)
+--        rewrite [-abs_of_neg H3, -abs_of_neg H5, -gcd_abs_abs a₁],
+--        rewrite [-gcd_abs_abs a₂ b₂],
+        revert H6,
+        rewrite [abs_of_neg H3 at {1}, abs_of_neg H5 at {1}, *gcd_abs_abs],
+        intro H6, apply H6
+      end,
+    calc
+      a₁ div (gcd a₁ b₁) = -(-a₁ div (gcd a₁ b₁)) :
+                             by rewrite [neg_div_of_dvd !gcd_dvd_left, neg_neg]
+                     ... = -(-a₂ div (gcd a₂ b₂)) : H7
+                     ... = a₂ div (gcd a₂ b₂) :
+                             by rewrite [neg_div_of_dvd !gcd_dvd_left, neg_neg])
+
 /- lcm -/
 
 definition lcm (a b : ℤ) : ℤ := of_nat (nat.lcm (nat_abs a) (nat_abs b))