refactor(library/data/nat/sub,*): get rid of diff, tidy some max and min theorems

library/algebra/order.lean

@@ -467,6 +467,18 @@ section
     (assume H : ¬ a ≤ b,
       assert H' : b ≤ a, from le_of_lt (lt_of_not_ge H),
       by rewrite (max_eq_left H'); apply H₁)
+
+  theorem min_eq_left_of_lt {a b : A} (H : a < b) : min a b = a :=
+  min_eq_left (le_of_lt H)
+
+  theorem min_eq_right_of_lt {a b : A} (H : b < a) : min a b = b :=
+  min_eq_right (le_of_lt H)
+
+  theorem max_eq_left_of_lt {a b : A} (H : b < a) : max a b = a :=
+  max_eq_left (le_of_lt H)
+
+  theorem max_eq_right_of_le {a b : A} (H : a < b) : max a b = b :=
+  max_eq_right (le_of_lt H)
 end
 
 end algebra

library/data/bag.lean

@@ -302,7 +302,7 @@ private lemma max_count_eq (l₁ l₂ : list A) : ∀ {a : A} {l : list A}, a
      end)
     (suppose i : ¬ list.count a l₁ ≥ list.count a l₂, begin
        unfold max_count, subst b,
-       rewrite [if_neg i, list.count_append, count_gen, max_eq_right' (lt_of_not_ge i), count_eq_zero_of_not_mem `a ∉ max_count l₁ l₂ l`]
+       rewrite [if_neg i, list.count_append, count_gen, max_eq_right_of_lt (lt_of_not_ge i), count_eq_zero_of_not_mem `a ∉ max_count l₁ l₂ l`]
      end))
   (suppose a ∈ l,
     assert a ≠ b, from suppose a = b, by subst b; contradiction,
@@ -531,22 +531,22 @@ bag.ext (λ a, begin
       have H₁₃ : count a b₁ ≤ count a b₃, from le.trans H₁₂ H₂₃,
       rewrite [max_eq_right H₂₃, min_eq_left H₁₂, min_eq_left H₁₃, max_self]},
     { intro H₂₃,
-      rewrite [min_eq_left H₁₂, max.comm, max_eq_right' (lt_of_not_ge H₂₃) ],
+      rewrite [min_eq_left H₁₂, max.comm, max_eq_right_of_lt (lt_of_not_ge H₂₃) ],
       apply (@by_cases (count a b₁ ≤ count a b₃)),
       { intro H₁₃, rewrite [min_eq_left H₁₃, max_self, min_eq_left H₁₂] },
       { intro H₁₃,
-        rewrite [min.comm (count a b₁) (count a b₃), min_eq_left' (lt_of_not_ge H₁₃),
-                 min_eq_left H₁₂, max.comm, max_eq_right' (lt_of_not_ge H₁₃)]}}},
+        rewrite [min.comm (count a b₁) (count a b₃), min_eq_left_of_lt (lt_of_not_ge H₁₃),
+                 min_eq_left H₁₂, max.comm, max_eq_right_of_lt (lt_of_not_ge H₁₃)]}}},
   { intro H₁₂, apply (@by_cases (count a b₂ ≤ count a b₃)),
     { intro H₂₃,
       rewrite [max_eq_right H₂₃],
       apply (@by_cases (count a b₁ ≤ count a b₃)),
-      { intro H₁₃, rewrite [min_eq_left H₁₃, min.comm, min_eq_left' (lt_of_not_ge H₁₂), max_eq_right' (lt_of_not_ge H₁₂)] },
-      { intro H₁₃, rewrite [min.comm, min_eq_left' (lt_of_not_ge H₁₃), min.comm, min_eq_left' (lt_of_not_ge H₁₂), max_eq_right H₂₃] } },
+      { intro H₁₃, rewrite [min_eq_left H₁₃, min.comm, min_eq_left_of_lt (lt_of_not_ge H₁₂), max_eq_right_of_lt (lt_of_not_ge H₁₂)] },
+      { intro H₁₃, rewrite [min.comm, min_eq_left_of_lt (lt_of_not_ge H₁₃), min.comm, min_eq_left_of_lt (lt_of_not_ge H₁₂), max_eq_right H₂₃] } },
     { intro H₂₃,
       have H₁₃ : count a b₁ > count a b₃, from lt.trans (lt_of_not_ge H₂₃) (lt_of_not_ge H₁₂),
-      rewrite [max.comm, max_eq_right' (lt_of_not_ge H₂₃), min.comm, min_eq_left' (lt_of_not_ge H₁₂)],
-      rewrite [min.comm, min_eq_left' H₁₃, max.comm, max_eq_right' (lt_of_not_ge H₂₃)] } }
+      rewrite [max.comm, max_eq_right_of_lt (lt_of_not_ge H₂₃), min.comm, min_eq_left_of_lt (lt_of_not_ge H₁₂)],
+      rewrite [min.comm, min_eq_left_of_lt H₁₃, max.comm, max_eq_right_of_lt (lt_of_not_ge H₂₃)] } }
 end)
 
 lemma inter.right_distrib (b₁ b₂ b₃ : bag A) : (b₁ ∪ b₂) ∩ b₃ = (b₁ ∩ b₃) ∪ (b₂ ∩ b₃) :=

library/data/nat/order.lean

@@ -91,8 +91,6 @@ theorem mul_lt_mul_of_pos_right {n m k : ℕ} (H : n < m) (Hk : k > 0) : n * k <
 
 /- min and max -/
 
--- Because these are defined in init/nat.lean, we cannot use the definitions in algebra.
-
 definition max (a b : ℕ) : ℕ := if a < b then b else a
 definition min (a b : ℕ) : ℕ := if a < b then a else b
 
@@ -472,26 +470,90 @@ decidable.by_cases
 theorem max_add_add_right (a b c : ℕ) : max (a + c) (b + c) = max a b + c :=
 by rewrite [add.comm a c, add.comm b c, add.comm _ c]; apply max_add_add_left
 
-theorem max_eq_right' {a b : ℕ} (H : a < b) : max a b = b :=
-if_pos H
+theorem min_eq_left_of_lt {a b : ℕ} (H : a < b) : min a b = a :=
+min_eq_left (le_of_lt H)
 
--- different versions will be defined in algebra
-theorem max_eq_left' {a b : ℕ} (H : ¬ a < b) : max a b = a :=
-if_neg H
+theorem min_eq_right_of_lt {a b : ℕ} (H : b < a) : min a b = b :=
+min_eq_right (le_of_lt H)
 
-lemma min_eq_left' {a b : nat} (H : a < b) : min a b = a :=
-if_pos H
+theorem max_eq_left_of_lt {a b : ℕ} (H : b < a) : max a b = a :=
+max_eq_left (le_of_lt H)
 
-lemma min_eq_right' {a b : nat} (H : ¬ a < b) : min a b = b :=
-if_neg H
+theorem max_eq_right_of_lt {a b : ℕ} (H : a < b) : max a b = b :=
+max_eq_right (le_of_lt H)
 
-/- greatest -/
+/- least and greatest -/
 
-section greatest
+section least_and_greatest
   variable (P : ℕ → Prop)
   variable [decP : ∀ n, decidable (P n)]
   include decP
 
+  -- returns the least i < n satisfying P, or n if there is none
+  definition least : ℕ → ℕ
+    | 0        := 0
+    | (succ n) := if P (least n) then least n else succ n
+
+  theorem least_of_bound {n : ℕ} (H : P n) : P (least P n) :=
+    begin
+      induction n with [m, ih],
+      rewrite ↑least,
+      apply H,
+      rewrite ↑least,
+      cases decidable.em (P (least P m)) with [Hlp, Hlp],
+      rewrite [if_pos Hlp],
+      apply Hlp,
+      rewrite [if_neg Hlp],
+      apply H
+    end
+
+  theorem least_le (n : ℕ) : least P n ≤ n:=
+    begin
+      induction n with [m, ih],
+        {rewrite ↑least},
+      rewrite ↑least,
+      cases decidable.em (P (least P m)) with [Psm, Pnsm],
+      rewrite [if_pos Psm],
+      apply le.trans ih !le_succ,
+      rewrite [if_neg Pnsm]
+    end
+
+ theorem least_of_lt {i n : ℕ} (ltin : i < n) (H : P i) : P (least P n) :=
+   begin
+     induction n with [m, ih],
+     exact absurd ltin !not_lt_zero,
+     rewrite ↑least,
+     cases decidable.em (P (least P m)) with [Psm, Pnsm],
+     rewrite [if_pos Psm],
+     apply Psm,
+     rewrite [if_neg Pnsm],
+     cases (lt_or_eq_of_le (le_of_lt_succ ltin)) with [Hlt, Heq],
+     exact absurd (ih Hlt) Pnsm,
+     rewrite Heq at H,
+     exact absurd (least_of_bound P H) Pnsm
+   end
+
+  theorem ge_least_of_lt {i n : ℕ} (ltin : i < n) (Hi : P i) : i ≥ least P n :=
+    begin
+      induction n with [m, ih],
+      exact absurd ltin !not_lt_zero,
+      rewrite ↑least,
+      cases decidable.em (P (least P m)) with [Psm, Pnsm],
+      rewrite [if_pos Psm],
+      cases (lt_or_eq_of_le (le_of_lt_succ ltin)) with [Hlt, Heq],
+      apply ih Hlt,
+      rewrite Heq,
+      apply least_le,
+      rewrite [if_neg Pnsm],
+      cases (lt_or_eq_of_le (le_of_lt_succ ltin)) with [Hlt, Heq],
+      apply absurd (least_of_lt P Hlt Hi) Pnsm,
+      rewrite Heq at Hi,
+      apply absurd (least_of_bound P Hi) Pnsm
+    end
+
+  theorem least_lt {n i : ℕ} (ltin : i < n) (Hi : P i) : least P n < n :=
+    lt_of_le_of_lt (ge_least_of_lt P ltin Hi) ltin
+
   -- returns the largest i < n satisfying P, or n if there is none.
   definition greatest : ℕ → ℕ
   | 0        := 0
@@ -519,73 +581,8 @@ section greatest
           have neim : i ≠ m, from assume H : i = m, absurd (H ▸ Hi) Pnsm,
           have ltim : i < m, from lt_of_le_of_ne (le_of_lt_succ ltin) neim,
           apply ih ltim}}
- end
+  end
 
- definition least : ℕ → ℕ
-   | 0        := 0
-   | (succ n) := if P (least n) then least n else succ n
-
- theorem least_of_bound {n : ℕ} (H : P n) : P (least P n) :=
-   begin
-     induction n with [m, ih],
-     rewrite ↑least,
-     apply H,
-     rewrite ↑least,
-     cases decidable.em (P (least P m)) with [Hlp, Hlp],
-     rewrite [if_pos Hlp],
-     apply Hlp,
-     rewrite [if_neg Hlp],
-     apply H
-   end
-
- theorem bound_le_least (n : ℕ) : n ≥ least P n :=
-   begin
-     induction n with [m, ih],
-     rewrite ↑least, apply le.refl,
-     rewrite ↑least,
-     cases decidable.em (P (least P m)) with [Psm, Pnsm],
-     rewrite [if_pos Psm],
-     apply le.trans ih !le_succ,
-     rewrite [if_neg Pnsm],
-     apply le.refl
-   end
-
- theorem least_of_lt {i n : ℕ} (ltin : i < n) (H : P i) : P (least P n) :=
-   begin
-     induction n with [m, ih],
-     exact absurd ltin !not_lt_zero,
-     rewrite ↑least,
-     cases decidable.em (P (least P m)) with [Psm, Pnsm],
-     rewrite [if_pos Psm],
-     apply Psm,
-     rewrite [if_neg Pnsm],
-     cases (lt_or_eq_of_le (le_of_lt_succ ltin)) with [Hlt, Heq],
-     exact absurd (ih Hlt) Pnsm,
-     rewrite Heq at H,
-     exact absurd (least_of_bound P H) Pnsm
-   end
-
- theorem ge_least_of_lt {i n : ℕ} (ltin : i < n) (Hi : P i) : i ≥ least P n :=
-   begin
-     induction n with [m, ih],
-     exact absurd ltin !not_lt_zero,
-     rewrite ↑least,
-     cases decidable.em (P (least P m)) with [Psm, Pnsm],
-     rewrite [if_pos Psm],
-     cases (lt_or_eq_of_le (le_of_lt_succ ltin)) with [Hlt, Heq],
-     apply ih Hlt,
-     rewrite Heq,
-     apply bound_le_least,
-     rewrite [if_neg Pnsm],
-     cases (lt_or_eq_of_le (le_of_lt_succ ltin)) with [Hlt, Heq],
-     apply absurd (least_of_lt P Hlt Hi) Pnsm,
-     rewrite Heq at Hi,
-     apply absurd (least_of_bound P Hi) Pnsm
-   end
-
- theorem least_lt {n i : ℕ} (ltin : i < n) (Hi : P i) : least P n < n :=
-   lt_of_le_of_lt (ge_least_of_lt P ltin Hi) ltin
-
-end greatest
+end least_and_greatest
 
 end nat

library/data/nat/sub.lean

@@ -45,7 +45,6 @@ nat.induction_on k
                               ... = succ (n + l) - succ (m + l) : {!add_succ}
                               ... = (n + l) - (m + l)           : !succ_sub_succ
                               ... =  n - m                      : IH)
-
 theorem add_sub_add_left (k n m : ℕ) : (k + n) - (k + m) = n - m :=
 !add.comm ▸ !add.comm ▸ !add_sub_add_right
 
@@ -381,14 +380,23 @@ have H4 : m - n = 0, from eq_zero_of_add_eq_zero_left H,
 have H5 : m ≤ n, from le_of_sub_eq_zero H4,
 le.antisymm H3 H5
 
+theorem dist_eq_zero {n m : ℕ} (H : n = m) : dist n m = 0 :=
+by substvars; rewrite [↑dist, *sub_self, add_zero]
+
 theorem dist_eq_sub_of_le {n m : ℕ} (H : n ≤ m) : dist n m = m - n :=
 calc
   dist n m = 0 + (m - n) : {sub_eq_zero_of_le H}
        ... = m - n       : zero_add
 
+theorem dist_eq_sub_of_lt {n m : ℕ} (H : n < m) : dist n m = m - n :=
+dist_eq_sub_of_le (le_of_lt H)
+
 theorem dist_eq_sub_of_ge {n m : ℕ} (H : n ≥ m) : dist n m = n - m :=
 !dist.comm ▸ dist_eq_sub_of_le H
 
+theorem dist_eq_sub_of_gt {n m : ℕ} (H : n > m) : dist n m = n - m :=
+dist_eq_sub_of_ge (le_of_lt H)
+
 theorem dist_zero_right (n : ℕ) : dist n 0 = n :=
 dist_eq_sub_of_ge !zero_le ⬝ !sub_zero
 
@@ -469,35 +477,21 @@ or.elim !le.total
   (assume H : k ≤ l, !dist.comm ▸ !dist.comm ▸ aux l k H)
   (assume H : l ≤ k, aux k l H)
 
-definition diff [reducible] (i j : nat) :=
-if (i < j) then (j - i) else (i - j)
+lemma dist_eq_max_sub_min {i j : nat} : dist i j = (max i j) - min i j :=
+or.elim (lt_or_ge i j)
+  (suppose i < j, begin rewrite [max_eq_right_of_lt this, min_eq_left_of_lt this, dist_eq_sub_of_lt this] end)
+  (suppose i ≥ j, begin rewrite [max_eq_left this , min_eq_right this, dist_eq_sub_of_ge this] end)
 
-open decidable
-lemma diff_eq_dist {i j : nat} : diff i j = dist i j :=
-by_cases
-  (suppose i < j,
-    by rewrite [if_pos this, ↑dist, sub_eq_zero_of_le (le_of_lt this), zero_add])
-  (suppose ¬ i < j,
-    by rewrite [if_neg this, ↑dist, sub_eq_zero_of_le (le_of_not_gt this)])
+lemma dist_succ {i j : nat} : dist (succ i) (succ j) = dist i j :=
+by rewrite [↑dist, *succ_sub_succ]
 
-lemma diff_eq_max_sub_min {i j : nat} : diff i j = (max i j) - min i j :=
-by_cases
-  (suppose i < j, begin rewrite [↑max, ↑min, *(if_pos this)] end)
-  (suppose ¬ i < j, begin rewrite [↑max, ↑min, *(if_neg this)] end)
+lemma dist_le_max {i j : nat} : dist i j ≤ max i j :=
+begin rewrite dist_eq_max_sub_min, apply sub_le end
 
-lemma diff_succ {i j : nat} : diff (succ i) (succ j) = diff i j :=
-by rewrite [*diff_eq_dist, ↑dist, *succ_sub_succ]
+lemma dist_pos_of_ne {i j : nat} : i ≠ j → dist i j > 0 :=
+assume Pne, lt.by_cases
+  (suppose i < j, begin rewrite [dist_eq_sub_of_lt this], apply sub_pos_of_lt this end)
+  (suppose i = j, by contradiction)
+  (suppose i > j, begin rewrite [dist_eq_sub_of_gt this], apply sub_pos_of_lt this end)
 
-lemma diff_add {i j k : nat} : diff (i + k) (j + k) = diff i j :=
-by rewrite [*diff_eq_dist, dist_add_add_right]
-
-lemma diff_le_max {i j : nat} : diff i j ≤ max i j :=
-begin rewrite diff_eq_max_sub_min, apply sub_le end
-
-lemma diff_gt_zero_of_ne {i j : nat} : i ≠ j → diff i j > 0 :=
-assume Pne, by_cases
-  (suppose i < j, begin rewrite [if_pos this], apply sub_pos_of_lt this end)
-  (suppose ¬ i < j, begin
-    rewrite [if_neg this], apply sub_pos_of_lt,
-    apply lt_of_le_and_ne (nat.le_of_not_gt this) (ne.symm Pne) end)
 end nat

library/data/pnat.lean

@@ -61,10 +61,10 @@ theorem max_right (a b : ℕ+) : max a b ≥ b := !le_max_right
 theorem max_left (a b : ℕ+) : max a b ≥ a := !le_max_left
 
 theorem max_eq_right {a b : ℕ+} (H : a < b) : max a b = b :=
-  pnat.eq (nat.max_eq_right' H)
+  pnat.eq (nat.max_eq_right_of_lt H)
 
 theorem max_eq_left {a b : ℕ+} (H : ¬ a < b) : max a b = a :=
-  pnat.eq (nat.max_eq_left' H)
+  pnat.eq (nat.max_eq_left (le_of_not_gt H))
 
 theorem le_of_lt {a b : ℕ+} : a < b → a ≤ b := nat.le_of_lt
 

library/theories/group_theory/cyclic.lean

@@ -38,11 +38,11 @@ assume Pe, or.elim (lt_or_ge i j)
   (assume Piltj, begin rewrite [sub_eq_zero_of_le (nat.le_of_lt Piltj)] end)
   (assume Pigej, begin rewrite [pow_sub a Pigej, Pe, mul.right_inv] end)
 
-lemma pow_diff_eq_one_of_pow_eq {a : A} {i j : nat} :
-  a^i = a^j → a^(diff i j) = 1 :=
-assume Pe, decidable.by_cases
-  (suppose i < j, by rewrite [if_pos this]; exact pow_sub_eq_one_of_pow_eq (eq.symm Pe))
-  (suppose ¬ i < j, by rewrite [if_neg this]; exact pow_sub_eq_one_of_pow_eq Pe)
+lemma pow_dist_eq_one_of_pow_eq {a : A} {i j : nat} :
+  a^i = a^j → a^(dist i j) = 1 :=
+assume Pe, or.elim (lt_or_ge i j)
+  (suppose i < j, by rewrite [dist_eq_sub_of_lt this]; exact pow_sub_eq_one_of_pow_eq (eq.symm Pe))
+  (suppose i ≥ j, by rewrite [dist_eq_sub_of_ge this]; exact pow_sub_eq_one_of_pow_eq Pe)
 
 lemma pow_madd {a : A} {n : nat} {i j : fin (succ n)} :
   a^(succ n) = 1 → a^(val (i + j)) = a^i * a^j :=
@@ -71,12 +71,12 @@ obtain i₁ P₁, from exists_not_of_not_forall Pninj,
 obtain i₂ P₂, from exists_not_of_not_forall P₁,
 obtain Pfe Pne, from iff.elim_left not_implies_iff_and_not P₂,
 assert Pvne : val i₁ ≠ val i₂, from assume Pveq, absurd (eq_of_veq Pveq) Pne,
-exists.intro (pred (diff i₁ i₂)) (begin
-  rewrite [succ_pred_of_pos (diff_gt_zero_of_ne Pvne)], apply and.intro,
+exists.intro (pred (dist i₁ i₂)) (begin
+  rewrite [succ_pred_of_pos (dist_pos_of_ne Pvne)], apply and.intro,
     apply lt_of_succ_lt_succ,
-    rewrite [succ_pred_of_pos (diff_gt_zero_of_ne Pvne)],
-    apply nat.lt_of_le_of_lt diff_le_max (max_lt i₁ i₂),
-    apply pow_diff_eq_one_of_pow_eq Pfe
+    rewrite [succ_pred_of_pos (dist_pos_of_ne Pvne)],
+    apply nat.lt_of_le_of_lt dist_le_max (max_lt i₁ i₂),
+    apply pow_dist_eq_one_of_pow_eq Pfe
   end)
 
 -- Another possibility is to generate a list of powers and use find to get the first
@@ -164,10 +164,10 @@ lemma eq_zero_of_pow_eq_one {a : A} : ∀ {n : nat}, a^n = 1 → n < order a →
 lemma pow_fin_inj (a : A) (n : nat) : injective (pow_fin a n) :=
 take i j,
 suppose a^(i + n) = a^(j + n),
-have    a^(diff i j) = 1, from diff_add ▸ pow_diff_eq_one_of_pow_eq this,
-have    diff i j = 0,     from
-  eq_zero_of_pow_eq_one this (nat.lt_of_le_of_lt diff_le_max (max_lt i j)),
-eq_of_veq (eq_of_dist_eq_zero (diff_eq_dist ▸ this))
+have    a^(dist i j) = 1, begin apply !dist_add_add_right ▸ (pow_dist_eq_one_of_pow_eq this) end,
+have    dist i j = 0,     from
+  eq_zero_of_pow_eq_one this (nat.lt_of_le_of_lt dist_le_max (max_lt i j)),
+eq_of_veq (eq_of_dist_eq_zero this)
 
 lemma cyc_eq_cyc (a : A) (n : nat) : cyc_pow_fin a n = cyc a :=
 assert Psub : cyc_pow_fin a n ⊆ cyc a, from subset_of_forall

library/theories/group_theory/pgroup.lean

@@ -1,7 +1,6 @@
 /-
 Copyright (c) 2015 Haitao Zhang. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
 Author : Haitao Zhang
 -/