feat(library/algebra/order,library/data/nat/order,library/*): instantiate nat to lattice, add theorems

library/algebra/order.lean

@@ -301,8 +301,7 @@ definition strong_order_pair.to_order_pair [trans-instance] [coercion] [reducibl
   lt_irrefl := lt_irrefl',
   le_of_lt := le_of_lt',
   lt_of_le_of_lt := lt_of_le_of_lt',
-  lt_of_lt_of_le := lt_of_lt_of_le'
-⦄
+  lt_of_lt_of_le := lt_of_lt_of_le' ⦄
 
 /- linear orders -/
 
@@ -450,48 +449,24 @@ section
     le_max_right := le_dlo_max_right,
     max_le := dlo_max_le ⦄
 
-/-
-  definition max (a b : A) : A :=
-  if a < b then b else a
+  /- These don't require decidability, but it is not clear whether it is worth breaking out
+     a new class, linearly_ordered_lattice. Currently nat is the only instance that doesn't
+     use decidable_linear_order (because max and min are defined separately, in init),
+     so we simply reprove these theorems there. -/
 
-  definition min (a b : A) : A :=
-  if a < b then a else b
-
-  theorem max_a_a (a : A) : a = max a a :=
-  eq.rec_on !if_t_t rfl
-
-  theorem max.eq_right {a b : A} (H : a < b) : max a b = b :=
-  if_pos H
-
-  theorem max.eq_left {a b : A} (H : ¬ a < b) : max a b = a :=
-  if_neg H
-
-  theorem max.right_eq {a b : A} (H : a < b) : b = max a b :=
-  eq.rec_on (max.eq_right H) rfl
-
-  theorem max.left_eq {a b : A} (H : ¬ a < b) : a = max a b :=
-  eq.rec_on (max.eq_left H) rfl
-
-  theorem max.left (a b : A) : a ≤ max a b :=
+  theorem lt_min {a b c : A} (H₁ : a < b) (H₂ : a < c) : a < min b c :=
   by_cases
-    (λ h : a < b,   le_of_lt (eq.rec_on (max.right_eq h) h))
-    (λ h : ¬ a < b, eq.rec_on (max.eq_left h) !le.refl)
+    (assume H : b ≤ c, by rewrite (min_eq_left H); apply H₁)
+    (assume H : ¬ b ≤ c,
+      assert H' : c ≤ b, from le_of_lt (lt_of_not_ge H),
+      by rewrite (min_eq_right H'); apply H₂)
 
-  theorem eq_or_lt_of_not_lt (H : ¬ a < b) : a = b ∨ b < a :=
-  have H' : b = a ∨ b < a, from or.swap (lt_or_eq_of_le (le_of_not_gt H)),
-  or.elim H'
-    (take H'' : b = a, or.inl (symm H''))
-    (take H'' : b < a, or.inr H'')
-
-  theorem max.right (a b : A) : b ≤ max a b :=
+  theorem max_lt {a b c : A} (H₁ : a < c) (H₂ : b < c) : max a b < c :=
   by_cases
-    (λ h : a < b,   eq.rec_on (max.eq_right h) !le.refl)
-    (λ h : ¬ a < b, or.rec_on (eq_or_lt_of_not_lt h)
-      (λ heq, eq.rec_on heq (eq.rec_on (max_a_a a) !le.refl))
-      (λ h : b < a,
-        have aux : a = max a b, from max.left_eq (lt.asymm h),
-        eq.rec_on aux (le_of_lt h)))
--/
+    (assume H : a ≤ b, by rewrite (max_eq_right H); apply H₂)
+    (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₁)
 end
 
 end algebra

library/algebra/ordered_ring.lean

@@ -97,7 +97,6 @@ section
     rewrite zero_mul at  H,
     exact H
   end
-
 end
 
 structure linear_ordered_semiring [class] (A : Type)
@@ -185,7 +184,8 @@ section
       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 :=
+structure ordered_ring [class] (A : Type)
+    extends ring A, ordered_comm_group A, zero_ne_one_class A :=
 (mul_nonneg : ∀a b, le zero a → le zero b → le zero (mul a b))
 (mul_pos : ∀a b, lt zero a → lt zero b → lt zero (mul a b))
 
@@ -225,7 +225,8 @@ begin
   exact (iff.mp !sub_pos_iff_lt H2)
 end
 
-definition ordered_ring.to_ordered_semiring [trans-instance] [coercion] [reducible] [s : ordered_ring A] :
+definition ordered_ring.to_ordered_semiring [trans-instance] [coercion] [reducible]
+    [s : ordered_ring A] :
   ordered_semiring A :=
 ⦃ ordered_semiring, s,
   mul_zero                   := mul_zero,
@@ -302,11 +303,10 @@ end
 
 -- TODO: we can eliminate mul_pos_of_pos, but now it is not worth the effort to redeclare the
 -- class instance
-structure linear_ordered_ring [class] (A : Type) extends ordered_ring A, linear_strong_order_pair A :=
+structure linear_ordered_ring [class] (A : Type)
+    extends ordered_ring A, linear_strong_order_pair A :=
   (zero_lt_one : lt zero one)
 
--- print fields linear_ordered_semiring
-
 definition linear_ordered_ring.to_linear_ordered_semiring [trans-instance] [coercion] [reducible]
     [s : linear_ordered_ring A] :
   linear_ordered_semiring A :=

library/data/int/order.lean

@@ -281,6 +281,7 @@ section migrate_algebra
   show decidable (b ≤ a), from _
   definition decidable_gt [instance] (a b : ℤ) : decidable (a > b) :=
   show decidable (b < a), from _
+
   definition min : ℤ → ℤ → ℤ := algebra.min
   definition max : ℤ → ℤ → ℤ := algebra.max
   definition abs : ℤ → ℤ := algebra.abs

library/data/nat/order.lean

@@ -111,7 +111,35 @@ lt_of_lt_of_le H2 H3
 theorem mul_lt_mul_of_pos_right {n m k : ℕ} (H : n < m) (Hk : k > 0) : n * k < m * k :=
 !mul.comm ▸ !mul.comm ▸ mul_lt_mul_of_pos_left H Hk
 
-/- nat is an instance of a linearly ordered semiring -/
+/- min and max -/
+
+-- Because these are defined in init/nat.lean, we cannot use the definitions in algebra.
+
+theorem max_le {n m k : ℕ} (H₁ : n ≤ k) (H₂ : m ≤ k) : max n m ≤ k :=
+decidable.by_cases
+  (assume H : n < m, by rewrite [↑max, if_pos H]; apply H₂)
+  (assume H : ¬ n < m, by rewrite [↑max, if_neg H]; apply H₁)
+
+theorem min_le_left (n m : ℕ) : min n m ≤ n :=
+decidable.by_cases
+  (assume H : n < m, by rewrite [↑min, if_pos H])
+  (assume H : ¬ n < m,
+    assert H' : m ≤ n, from or_resolve_right !lt_or_ge H,
+    by rewrite [↑min, if_neg H]; apply H')
+
+theorem min_le_right (n m : ℕ) : min n m ≤ m :=
+decidable.by_cases
+  (assume H : n < m, by rewrite [↑min, if_pos H]; apply le_of_lt H)
+  (assume H : ¬ n < m,
+    assert H' : m ≤ n, from or_resolve_right !lt_or_ge H,
+    by rewrite [↑min, if_neg H])
+
+theorem le_min {n m k : ℕ} (H₁ : k ≤ n) (H₂ : k ≤ m) : k ≤ min n m :=
+decidable.by_cases
+  (assume H : n < m, by rewrite [↑min, if_pos H]; apply H₁)
+  (assume H : ¬ n < m, by rewrite [↑min, if_neg H]; apply H₂)
+
+/- nat is an instance of a linearly ordered semiring and a lattice-/
 
 section migrate_algebra
   open [classes] algebra
@@ -143,10 +171,22 @@ section migrate_algebra
     mul_lt_mul_of_pos_left     := @mul_lt_mul_of_pos_left,
     mul_lt_mul_of_pos_right    := @mul_lt_mul_of_pos_right ⦄
 
+  protected definition lattice [reducible] : algebra.lattice nat :=
+  ⦃ algebra.lattice, nat.linear_ordered_semiring,
+    min          := min,
+    max          := max,
+    min_le_left  := min_le_left,
+    min_le_right := min_le_right,
+    le_min       := @le_min,
+    le_max_left  := le_max_left,
+    le_max_right := le_max_right,
+    max_le       := @max_le ⦄
+
   local attribute nat.linear_ordered_semiring [instance]
+  local attribute nat.lattice [instance]
 
   migrate from algebra with nat
-    replacing dvd → dvd, has_le.ge → ge, has_lt.gt → gt
+    replacing dvd → dvd, has_le.ge → ge, has_lt.gt → gt, min → min, max → max
     hiding add_pos_of_pos_of_nonneg,  add_pos_of_nonneg_of_pos,
       add_eq_zero_iff_eq_zero_and_eq_zero_of_nonneg_of_nonneg, le_add_of_nonneg_of_le,
       le_add_of_le_of_nonneg, lt_add_of_nonneg_of_lt, lt_add_of_lt_of_nonneg,
@@ -390,4 +430,20 @@ dvd.elim H
     assume H1 : 1 = n * m,
     eq_one_of_mul_eq_one_right H1⁻¹)
 
+/- min and max -/
+
+theorem lt_min {a b c : ℕ} (H₁ : a < b) (H₂ : a < c) : a < min b c :=
+decidable.by_cases
+  (assume H : b ≤ c, by rewrite (min_eq_left H); apply H₁)
+  (assume H : ¬ b ≤ c,
+    assert H' : c ≤ b, from le_of_lt (lt_of_not_ge H),
+    by rewrite (min_eq_right H'); apply H₂)
+
+theorem max_lt {a b c : ℕ} (H₁ : a < c) (H₂ : b < c) : max a b < c :=
+decidable.by_cases
+  (assume H : a ≤ b, by rewrite (max_eq_right H); apply H₂)
+  (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₁)
+
 end nat

library/data/pnat.lean

@@ -73,11 +73,11 @@ 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 :=
-  have Hnat : nat.max a~ b~ = b~, from nat.max_eq_right H,
+  have Hnat : nat.max a~ b~ = b~, from nat.max_eq_right' H,
   pnat.eq Hnat
 
 theorem max_eq_left {a b : ℕ+} (H : ¬ a < b) : max a b = a :=
-  have Hnat : nat.max a~ b~ = a~, from nat.max_eq_left H,
+  have Hnat : nat.max a~ b~ = a~, from nat.max_eq_left' H,
   pnat.eq Hnat
 
 theorem le_of_lt {a b : ℕ+} (H : a < b) : a ≤ b := nat.le_of_lt H

library/init/nat.lean

@@ -5,7 +5,6 @@ Authors: Floris van Doorn, Leonardo de Moura
 -/
 prelude
 import init.wf init.tactic init.num
-
 open eq.ops decidable or
 
 namespace nat
@@ -40,7 +39,6 @@ namespace nat
   notation a - b := sub a b
   notation a * b := mul a b
 
-
   /- properties of ℕ -/
 
   protected definition is_inhabited [instance] : inhabited nat :=
@@ -226,17 +224,18 @@ namespace nat
   theorem max_self (a : ℕ) : max a a = a :=
   eq.rec_on !if_t_t rfl
 
-  theorem max_eq_right {a b : ℕ} (H : a < b) : max a b = b :=
+  theorem max_eq_right' {a b : ℕ} (H : a < b) : max a b = b :=
   if_pos H
 
-  theorem max_eq_left {a b : ℕ} (H : ¬ a < b) : max a b = a :=
+  -- different versions will be defined in algebra
+  theorem max_eq_left' {a b : ℕ} (H : ¬ a < b) : max a b = a :=
   if_neg H
 
   theorem eq_max_right {a b : ℕ} (H : a < b) : b = max a b :=
-  eq.rec_on (max_eq_right H) rfl
+  eq.rec_on (max_eq_right' H) rfl
 
   theorem eq_max_left {a b : ℕ} (H : ¬ a < b) : a = max a b :=
-  eq.rec_on (max_eq_left H) rfl
+  eq.rec_on (max_eq_left' H) rfl
 
   theorem le_max_left (a b : ℕ) : a ≤ max a b :=
   by_cases