refactor(library/algebra/{lattice,order},library/data/nat): split lattice from order, make nat an instance of discrete linear order

library/algebra/algebra.md

@@ -3,10 +3,12 @@ algebra
 
 Algebraic structures.
 
+* [prio](prio.lean) : priority for algebraic operations
 * [function](function.lean)
 * [relation](relation.lean)
 * [binary](binary.lean) : binary operations
-* [wf](wf.lean) : well-founded relations
+* [order](order.lean)
+* [lattice](lattice.lean)
 * [group](group.lean)
 * [group_power](group_power.lean) : nat and int powers
 * [group_bigops](group_bigops.lean) : finite products and sums
@@ -19,3 +21,4 @@ Algebraic structures.
 
 * [category](category/category.md) : category theory
 
+We set a low priority for algebraic operations, so that the elaborator tries concrete structures first.

library/algebra/lattice.lean

@@ -0,0 +1,112 @@
+/-
+Copyright (c) 2014 Jeremy Avigad. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Jeremy Avigad
+-/
+import .order
+
+namespace algebra
+
+variable {A : Type}
+
+/- lattices (we could split this to upper- and lower-semilattices, if needed) -/
+
+structure lattice [class] (A : Type) extends weak_order A :=
+(inf : A → A → A)
+(sup : A → A → A)
+(inf_le_left : ∀ a b, le (inf a b) a)
+(inf_le_right : ∀ a b, le (inf a b) b)
+(le_inf : ∀a b c, le c a → le c b → le c (inf a b))
+(le_sup_left : ∀ a b, le a (sup a b))
+(le_sup_right : ∀ a b, le b (sup a b))
+(sup_le : ∀ a b c, le a c → le b c → le (sup a b) c)
+
+definition inf := @lattice.inf
+definition sup := @lattice.sup
+infix `⊓`:70 := inf
+infix `⊔`:65 := sup
+
+section
+  variable [s : lattice A]
+  include s
+
+  theorem inf_le_left (a b : A) : a ⊓ b ≤ a := !lattice.inf_le_left
+
+  theorem inf_le_right (a b : A) : a ⊓ b ≤ b := !lattice.inf_le_right
+
+  theorem le_inf {a b c : A} (H₁ : c ≤ a) (H₂ : c ≤ b) : c ≤ a ⊓ b := !lattice.le_inf H₁ H₂
+
+  theorem le_sup_left (a b : A) : a ≤ a ⊔ b := !lattice.le_sup_left
+
+  theorem le_sup_right (a b : A) : b ≤ a ⊔ b := !lattice.le_sup_right
+
+  theorem sup_le {a b c : A} (H₁ : a ≤ c) (H₂ : b ≤ c) : a ⊔ b ≤ c := !lattice.sup_le H₁ H₂
+
+  /- inf -/
+
+  theorem eq_inf {a b c : A} (H₁ : c ≤ a) (H₂ : c ≤ b) (H₃ : ∀{d}, d ≤ a → d ≤ b → d ≤ c) :
+    c = a ⊓ b :=
+  le.antisymm (le_inf H₁ H₂) (H₃ !inf_le_left !inf_le_right)
+
+  theorem inf.comm (a b : A) : a ⊓ b = b ⊓ a :=
+  eq_inf !inf_le_right !inf_le_left (λ c H₁ H₂, le_inf H₂ H₁)
+
+  theorem inf.assoc (a b c : A) : (a ⊓ b) ⊓ c = a ⊓ (b ⊓ c) :=
+  begin
+    apply eq_inf,
+    { apply le.trans, apply inf_le_left, apply inf_le_left },
+    { apply le_inf, apply le.trans, apply inf_le_left, apply inf_le_right, apply inf_le_right },
+    { intros [d, H₁, H₂], apply le_inf, apply le_inf H₁, apply le.trans H₂, apply inf_le_left,
+      apply le.trans H₂, apply inf_le_right }
+  end
+
+  theorem inf.left_comm (a b c : A) : a ⊓ (b ⊓ c) = b ⊓ (a ⊓ c) :=
+  binary.left_comm (@inf.comm A s) (@inf.assoc A s) a b c
+
+  theorem inf.right_comm (a b c : A) : (a ⊓ b) ⊓ c = (a ⊓ c) ⊓ b :=
+  binary.right_comm (@inf.comm A s) (@inf.assoc A s) a b c
+
+  theorem inf_self (a : A) : a ⊓ a = a :=
+  by apply eq.symm; apply eq_inf (le.refl a) !le.refl; intros; assumption
+
+  theorem inf_eq_left {a b : A} (H : a ≤ b) : a ⊓ b = a :=
+  by apply eq.symm; apply eq_inf !le.refl H; intros; assumption
+
+  theorem inf_eq_right {a b : A} (H : b ≤ a) : a ⊓ b = b :=
+  eq.subst !inf.comm (inf_eq_left H)
+
+  /- sup -/
+
+  theorem eq_sup {a b c : A} (H₁ : a ≤ c) (H₂ : b ≤ c) (H₃ : ∀{d}, a ≤ d → b ≤ d → c ≤ d) :
+    c = a ⊔ b :=
+  le.antisymm (H₃ !le_sup_left !le_sup_right) (sup_le H₁ H₂)
+
+  theorem sup.comm (a b : A) : a ⊔ b = b ⊔ a :=
+  eq_sup !le_sup_right !le_sup_left (λ c H₁ H₂, sup_le H₂ H₁)
+
+  theorem sup.assoc (a b c : A) : (a ⊔ b) ⊔ c = a ⊔ (b ⊔ c) :=
+  begin
+    apply eq_sup,
+    { apply le.trans, apply le_sup_left a b, apply le_sup_left },
+    { apply sup_le, apply le.trans, apply le_sup_right a b, apply le_sup_left, apply le_sup_right },
+    { intros [d, H₁, H₂], apply sup_le, apply sup_le H₁, apply le.trans !le_sup_left H₂,
+      apply le.trans !le_sup_right H₂}
+  end
+
+  theorem sup.left_comm (a b c : A) : a ⊔ (b ⊔ c) = b ⊔ (a ⊔ c) :=
+  binary.left_comm (@sup.comm A s) (@sup.assoc A s) a b c
+
+  theorem sup.right_comm (a b c : A) : (a ⊔ b) ⊔ c = (a ⊔ c) ⊔ b :=
+  binary.right_comm (@sup.comm A s) (@sup.assoc A s) a b c
+
+  theorem sup_self (a : A) : a ⊔ a = a :=
+  by apply eq.symm; apply eq_sup (le.refl a) !le.refl; intros; assumption
+
+  theorem sup_eq_left {a b : A} (H : b ≤ a) : a ⊔ b = a :=
+  by apply eq.symm; apply eq_sup !le.refl H; intros; assumption
+
+  theorem sup_eq_right {a b : A} (H : a ≤ b) : a ⊔ b = b :=
+  eq.subst !sup.comm (sup_eq_left H)
+end
+
+end algebra

library/algebra/order.lean

@@ -103,104 +103,6 @@ theorem wf.ind_on.{u v} {A : Type.{u}} [s : wf_strict_order.{u 0} A] {P : A →
     (x : A) (H : ∀x, (∀y, wf_strict_order.lt y x → P y) → P x) : P x :=
 wf.rec_on x H
 
-/- lattices (we could split this to upper- and lower-semilattices, if needed) -/
-
-structure lattice [class] (A : Type) extends weak_order A :=
-(min : A → A → A)
-(max : A → A → A)
-(min_le_left : ∀ a b, le (min a b) a)
-(min_le_right : ∀ a b, le (min a b) b)
-(le_min : ∀a b c, le c a → le c b → le c (min a b))
-(le_max_left : ∀ a b, le a (max a b))
-(le_max_right : ∀ a b, le b (max a b))
-(max_le : ∀ a b c, le a c → le b c → le (max a b) c)
-
-definition min := @lattice.min
-definition max := @lattice.max
-
-section
-  variable [s : lattice A]
-  include s
-
-  theorem min_le_left (a b : A) : min a b ≤ a := !lattice.min_le_left
-
-  theorem min_le_right (a b : A) : min a b ≤ b := !lattice.min_le_right
-
-  theorem le_min {a b c : A} (H₁ : c ≤ a) (H₂ : c ≤ b) : c ≤ min a b := !lattice.le_min H₁ H₂
-
-  theorem le_max_left (a b : A) : a ≤ max a b := !lattice.le_max_left
-
-  theorem le_max_right (a b : A) : b ≤ max a b := !lattice.le_max_right
-
-  theorem max_le {a b c : A} (H₁ : a ≤ c) (H₂ : b ≤ c) : max a b ≤ c := !lattice.max_le H₁ H₂
-
-  /- min -/
-
-  theorem eq_min {a b c : A} (H₁ : c ≤ a) (H₂ : c ≤ b) (H₃ : ∀{d}, d ≤ a → d ≤ b → d ≤ c) :
-    c = min a b :=
-  le.antisymm (le_min H₁ H₂) (H₃ !min_le_left !min_le_right)
-
-  theorem min.comm (a b : A) : min a b = min b a :=
-  eq_min !min_le_right !min_le_left (λ c H₁ H₂, le_min H₂ H₁)
-
-  theorem min.assoc (a b c : A) : min (min a b) c = min a (min b c) :=
-  begin
-    apply eq_min,
-    { apply le.trans, apply min_le_left, apply min_le_left },
-    { apply le_min, apply le.trans, apply min_le_left, apply min_le_right, apply min_le_right },
-    { intros [d, H₁, H₂], apply le_min, apply le_min H₁, apply le.trans H₂, apply min_le_left,
-      apply le.trans H₂, apply min_le_right }
-  end
-
-  theorem min.left_comm (a b c : A) : min a (min b c) = min b (min a c) :=
-  binary.left_comm (@min.comm A s) (@min.assoc A s) a b c
-
-  theorem min.right_comm (a b c : A) : min (min a b) c = min (min a c) b :=
-  binary.right_comm (@min.comm A s) (@min.assoc A s) a b c
-
-  theorem min_self (a : A) : min a a = a :=
-  by apply eq.symm; apply eq_min (le.refl a) !le.refl; intros; assumption
-
-  theorem min_eq_left {a b : A} (H : a ≤ b) : min a b = a :=
-  by apply eq.symm; apply eq_min !le.refl H; intros; assumption
-
-  theorem min_eq_right {a b : A} (H : b ≤ a) : min a b = b :=
-  eq.subst !min.comm (min_eq_left H)
-
-  /- max -/
-
-  theorem eq_max {a b c : A} (H₁ : a ≤ c) (H₂ : b ≤ c) (H₃ : ∀{d}, a ≤ d → b ≤ d → c ≤ d) :
-    c = max a b :=
-  le.antisymm (H₃ !le_max_left !le_max_right) (max_le H₁ H₂)
-
-  theorem max.comm (a b : A) : max a b = max b a :=
-  eq_max !le_max_right !le_max_left (λ c H₁ H₂, max_le H₂ H₁)
-
-  theorem max.assoc (a b c : A) : max (max a b) c = max a (max b c) :=
-  begin
-    apply eq_max,
-    { apply le.trans, apply le_max_left a b, apply le_max_left },
-    { apply max_le, apply le.trans, apply le_max_right a b, apply le_max_left, apply le_max_right },
-    { intros [d, H₁, H₂], apply max_le, apply max_le H₁, apply le.trans !le_max_left H₂,
-      apply le.trans !le_max_right H₂}
-  end
-
-  theorem max.left_comm (a b c : A) : max a (max b c) = max b (max a c) :=
-  binary.left_comm (@max.comm A s) (@max.assoc A s) a b c
-
-  theorem max.right_comm (a b c : A) : max (max a b) c = max (max a c) b :=
-  binary.right_comm (@max.comm A s) (@max.assoc A s) a b c
-
-  theorem max_self (a : A) : max a a = a :=
-  by apply eq.symm; apply eq_max (le.refl a) !le.refl; intros; assumption
-
-  theorem max_eq_left {a b : A} (H : b ≤ a) : max a b = a :=
-  by apply eq.symm; apply eq_max !le.refl H; intros; assumption
-
-  theorem max_eq_right {a b : A} (H : a ≤ b) : max a b = b :=
-  eq.subst !max.comm (max_eq_left H)
-end
-
 /- structures with a weak and a strict order -/
 
 structure order_pair [class] (A : Type) extends weak_order A, has_lt A :=
@@ -403,70 +305,106 @@ section
     lt.cases a b t_lt t_eq t_gt = t_gt :=
   if_neg (ne.symm (ne_of_lt H)) ⬝ if_neg (lt.asymm H)
 
-  private definition dlo_min (a b : A) : A := if a ≤ b then a else b
+  definition min (a b : A) : A := if a ≤ b then a else b
+  definition max (a b : A) : A := if a ≤ b then b else a
 
-  private definition dlo_max (a b : A) : A := if a ≤ b then b else a
+  /- these show min and max form a lattice -/
 
-  private theorem dlo_min_le_left (a b : A) : dlo_min a b ≤ a :=
+  theorem min_le_left (a b : A) : min a b ≤ a :=
   by_cases
-    (assume H : a ≤ b, by rewrite [↑dlo_min, if_pos H]; apply le.refl)
+    (assume H : a ≤ b, by rewrite [↑min, if_pos H]; apply le.refl)
-    (assume H : ¬ a ≤ b, by rewrite [↑dlo_min, if_neg H]; apply le_of_lt (lt_of_not_ge H))
+    (assume H : ¬ a ≤ b, by rewrite [↑min, if_neg H]; apply le_of_lt (lt_of_not_ge H))
 
-  private theorem dlo_min_le_right (a b : A) : dlo_min a b ≤ b :=
+  theorem min_le_right (a b : A) : min a b ≤ b :=
   by_cases
-    (assume H : a ≤ b, by rewrite [↑dlo_min, if_pos H]; apply H)
+    (assume H : a ≤ b, by rewrite [↑min, if_pos H]; apply H)
-    (assume H : ¬ a ≤ b, by rewrite [↑dlo_min, if_neg H]; apply le.refl)
+    (assume H : ¬ a ≤ b, by rewrite [↑min, if_neg H]; apply le.refl)
 
-  private theorem le_dlo_min (a b c : A) (H₁ : c ≤ a) (H₂ : c ≤ b) : c ≤ dlo_min a b :=
+  theorem le_min {a b c : A} (H₁ : c ≤ a) (H₂ : c ≤ b) : c ≤ min a b :=
   by_cases
-    (assume H : a ≤ b, by rewrite [↑dlo_min, if_pos H]; apply H₁)
+    (assume H : a ≤ b, by rewrite [↑min, if_pos H]; apply H₁)
-    (assume H : ¬ a ≤ b, by rewrite [↑dlo_min, if_neg H]; apply H₂)
+    (assume H : ¬ a ≤ b, by rewrite [↑min, if_neg H]; apply H₂)
 
-  private theorem le_dlo_max_left (a b : A) : a ≤ dlo_max a b :=
+  theorem le_max_left (a b : A) : a ≤ max a b :=
   by_cases
-    (assume H : a ≤ b, by rewrite [↑dlo_max, if_pos H]; apply H)
+    (assume H : a ≤ b, by rewrite [↑max, if_pos H]; apply H)
-    (assume H : ¬ a ≤ b, by rewrite [↑dlo_max, if_neg H]; apply le.refl)
+    (assume H : ¬ a ≤ b, by rewrite [↑max, if_neg H]; apply le.refl)
 
-  private theorem le_dlo_max_right (a b : A) : b ≤ dlo_max a b :=
+  theorem le_max_right (a b : A) : b ≤ max a b :=
   by_cases
-    (assume H : a ≤ b, by rewrite [↑dlo_max, if_pos H]; apply le.refl)
+    (assume H : a ≤ b, by rewrite [↑max, if_pos H]; apply le.refl)
-    (assume H : ¬ a ≤ b, by rewrite [↑dlo_max, if_neg H]; apply le_of_lt (lt_of_not_ge H))
+    (assume H : ¬ a ≤ b, by rewrite [↑max, if_neg H]; apply le_of_lt (lt_of_not_ge H))
 
-  private theorem dlo_max_le (a b c : A) (H₁ : a ≤ c) (H₂ : b ≤ c) : dlo_max a b ≤ c :=
+  theorem max_le {a b c : A} (H₁ : a ≤ c) (H₂ : b ≤ c) : max a b ≤ c :=
   by_cases
-    (assume H : a ≤ b, by rewrite [↑dlo_max, if_pos H]; apply H₂)
+    (assume H : a ≤ b, by rewrite [↑max, if_pos H]; apply H₂)
-    (assume H : ¬ a ≤ b, by rewrite [↑dlo_max, if_neg H]; apply H₁)
+    (assume H : ¬ a ≤ b, by rewrite [↑max, if_neg H]; apply H₁)
 
-  definition decidable_linear_order.to_lattice [trans-instance] [coercion] [reducible] :
+  /- these are also proved for lattices, but with inf and sup in place of min and max -/
-    lattice A :=
-  ⦃ lattice, s,
-    min := dlo_min,
-    max := dlo_max,
-    min_le_left := dlo_min_le_left,
-    min_le_right := dlo_min_le_right,
-    le_min := le_dlo_min,
-    le_max_left := le_dlo_max_left,
-    le_max_right := le_dlo_max_right,
-    max_le := dlo_max_le ⦄
 
-  /- These don't require decidability, but it is not clear whether it is worth breaking out
+  theorem eq_min {a b c : A} (H₁ : c ≤ a) (H₂ : c ≤ b) (H₃ : ∀{d}, d ≤ a → d ≤ b → d ≤ c) :
-     a new class, linearly_ordered_lattice. Currently nat is the only instance that doesn't
+    c = min a b :=
-     use decidable_linear_order (because max and min are defined separately, in init),
+  le.antisymm (le_min H₁ H₂) (H₃ !min_le_left !min_le_right)
-     so we simply reprove these theorems there. -/
 
-  theorem lt_min {a b c : A} (H₁ : a < b) (H₂ : a < c) : a < min b c :=
+  theorem min.comm (a b : A) : min a b = min b a :=
-  by_cases
+  eq_min !min_le_right !min_le_left (λ c H₁ H₂, le_min H₂ H₁)
-    (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 : A} (H₁ : a < c) (H₂ : b < c) : max a b < c :=
+  theorem min.assoc (a b c : A) : min (min a b) c = min a (min b c) :=
-  by_cases
+  begin
-    (assume H : a ≤ b, by rewrite (max_eq_right H); apply H₂)
+    apply eq_min,
-    (assume H : ¬ a ≤ b,
+    { apply le.trans, apply min_le_left, apply min_le_left },
-      assert H' : b ≤ a, from le_of_lt (lt_of_not_ge H),
+    { apply le_min, apply le.trans, apply min_le_left, apply min_le_right, apply min_le_right },
-      by rewrite (max_eq_left H'); apply H₁)
+    { intros [d, H₁, H₂], apply le_min, apply le_min H₁, apply le.trans H₂, apply min_le_left,
+      apply le.trans H₂, apply min_le_right }
+  end
+
+  theorem min.left_comm (a b c : A) : min a (min b c) = min b (min a c) :=
+  binary.left_comm (@min.comm A s) (@min.assoc A s) a b c
+
+  theorem min.right_comm (a b c : A) : min (min a b) c = min (min a c) b :=
+  binary.right_comm (@min.comm A s) (@min.assoc A s) a b c
+
+  theorem min_self (a : A) : min a a = a :=
+  by apply eq.symm; apply eq_min (le.refl a) !le.refl; intros; assumption
+
+  theorem min_eq_left {a b : A} (H : a ≤ b) : min a b = a :=
+  by apply eq.symm; apply eq_min !le.refl H; intros; assumption
+
+  theorem min_eq_right {a b : A} (H : b ≤ a) : min a b = b :=
+  eq.subst !min.comm (min_eq_left H)
+
+  theorem eq_max {a b c : A} (H₁ : a ≤ c) (H₂ : b ≤ c) (H₃ : ∀{d}, a ≤ d → b ≤ d → c ≤ d) :
+    c = max a b :=
+  le.antisymm (H₃ !le_max_left !le_max_right) (max_le H₁ H₂)
+
+  theorem max.comm (a b : A) : max a b = max b a :=
+  eq_max !le_max_right !le_max_left (λ c H₁ H₂, max_le H₂ H₁)
+
+  theorem max.assoc (a b c : A) : max (max a b) c = max a (max b c) :=
+  begin
+    apply eq_max,
+    { apply le.trans, apply le_max_left a b, apply le_max_left },
+    { apply max_le, apply le.trans, apply le_max_right a b, apply le_max_left, apply le_max_right },
+    { intros [d, H₁, H₂], apply max_le, apply max_le H₁, apply le.trans !le_max_left H₂,
+      apply le.trans !le_max_right H₂}
+  end
+
+  theorem max.left_comm (a b c : A) : max a (max b c) = max b (max a c) :=
+  binary.left_comm (@max.comm A s) (@max.assoc A s) a b c
+
+  theorem max.right_comm (a b c : A) : max (max a b) c = max (max a c) b :=
+  binary.right_comm (@max.comm A s) (@max.assoc A s) a b c
+
+  theorem max_self (a : A) : max a a = a :=
+  by apply eq.symm; apply eq_max (le.refl a) !le.refl; intros; assumption
+
+  theorem max_eq_left {a b : A} (H : b ≤ a) : max a b = a :=
+  by apply eq.symm; apply eq_max !le.refl H; intros; assumption
+
+  theorem max_eq_right {a b : A} (H : a ≤ b) : max a b = b :=
+  eq.subst !max.comm (max_eq_left H)
+
+  /- these rely on lt_of_lt -/
 
   theorem min_eq_left_of_lt {a b : A} (H : a < b) : min a b = a :=
   min_eq_left (le_of_lt H)
@@ -477,8 +415,20 @@ section
   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 :=
+  theorem max_eq_right_of_lt {a b : A} (H : a < b) : max a b = b :=
   max_eq_right (le_of_lt H)
+
+  /- these use the fact that it is a linear ordering -/
+
+  theorem lt_min {a b c : A} (H₁ : a < b) (H₂ : a < c) : a < min b c :=
+  or.elim !le_or_gt
+    (assume H : b ≤ c, by rewrite (min_eq_left H); apply H₁)
+    (assume H : b > c, by rewrite (min_eq_right_of_lt H); apply H₂)
+
+  theorem max_lt {a b c : A} (H₁ : a < c) (H₂ : b < c) : max a b < c :=
+  or.elim !le_or_gt
+    (assume H : a ≤ b, by rewrite (max_eq_right H); apply H₂)
+    (assume H : a > b, by rewrite (max_eq_left_of_lt H); apply H₁)
 end
 
 end algebra

library/algebra/ordered_group.lean

@@ -200,11 +200,13 @@ structure ordered_comm_group [class] (A : Type) extends add_comm_group A, order_
 (add_le_add_left : ∀a b, le a b → ∀c, le (add c a) (add c b))
 (add_lt_add_left : ∀a b, lt a b → ∀ c, lt (add c a) (add c b))
 
-theorem ordered_comm_group.le_of_add_le_add_left [s : ordered_comm_group A] {a b c : A} (H : a + b ≤ a + c) : b ≤ c :=
+theorem ordered_comm_group.le_of_add_le_add_left [s : ordered_comm_group A] {a b c : A}
+  (H : a + b ≤ a + c) : b ≤ c :=
 assert H' : -a + (a + b) ≤ -a + (a + c), from ordered_comm_group.add_le_add_left _ _ H _,
 by rewrite *neg_add_cancel_left at H'; exact H'
 
-theorem ordered_comm_group.lt_of_add_lt_add_left [s : ordered_comm_group A] {a b c : A} (H : a + b < a + c) : b < c :=
+theorem ordered_comm_group.lt_of_add_lt_add_left [s : ordered_comm_group A] {a b c : A}
+  (H : a + b < a + c) : b < c :=
 assert H' : -a + (a + b) < -a + (a + c), from ordered_comm_group.add_lt_add_left _ _ H _,
 by rewrite *neg_add_cancel_left at H'; exact H'
 
@@ -555,16 +557,28 @@ section
     !neg_add ▸ neg_le_neg (le_add_of_nonneg_left (le_of_lt H))
 end
 
-/- partially ordered groups with min and max -/
+/- linear ordered group with decidable order -/
 
-structure lattice_ordered_comm_group [class] (A : Type)
+structure decidable_linear_ordered_comm_group [class] (A : Type)
-    extends ordered_comm_group A, lattice A
+    extends add_comm_group A, decidable_linear_order A :=
+    (add_le_add_left : ∀ a b, le a b → ∀ c, le (add c a) (add c b))
+    (add_lt_add_left : ∀ a b, lt a b → ∀ c, lt (add c a) (add c b))
+
+definition decidable_linear_ordered_comm_group.to_ordered_comm_group
+      [trans-instance] [reducible] [coercion]
+   (A : Type) [s : decidable_linear_ordered_comm_group A] : ordered_comm_group A :=
+⦃ ordered_comm_group, s,
+  le_of_lt := @le_of_lt A s,
+  lt_of_le_of_lt := @lt_of_le_of_lt A s,
+  lt_of_lt_of_le := @lt_of_lt_of_le A s ⦄
 
 section
-  variables [s : lattice_ordered_comm_group A]
+  variables [s : decidable_linear_ordered_comm_group A]
-  variables (a b c : A)
+  variables {a b c d e : A}
   include s
 
+  /- these can be generalized to a lattice ordered group -/
+
   theorem min_add_add_left : min (a + b) (a + c) = a + min b c :=
   eq.symm (eq_min
     (show a + min b c ≤ a + b, from add_le_add_left !min_le_left _)
@@ -645,32 +659,8 @@ section
 
   theorem ne_zero_of_abs_ne_zero {a : A} (H : abs a ≠ 0) : a ≠ 0 :=
    assume Ha, H (Ha⁻¹ ▸ abs_zero)
-end
 
-/- linear ordered group with decidable order -/
+  /- these assume a linear order -/
-
-structure decidable_linear_ordered_comm_group [class] (A : Type)
-    extends add_comm_group A, decidable_linear_order A :=
-    (add_le_add_left : ∀ a b, le a b → ∀ c, le (add c a) (add c b))
-    (add_lt_add_left : ∀ a b, lt a b → ∀ c, lt (add c a) (add c b))
-
-private theorem add_le_add_left' (A : Type) (s : decidable_linear_ordered_comm_group A) (a b : A) :
-                a ≤ b → (∀ c : A, c + a ≤ c + b) :=
-  decidable_linear_ordered_comm_group.add_le_add_left a b
-
-definition decidable_linear_ordered_comm_group.to_lattice_ordered_comm_group
-      [trans-instance] [reducible] [coercion]
-   (A : Type) [s : decidable_linear_ordered_comm_group A] : lattice_ordered_comm_group A :=
-⦃ lattice_ordered_comm_group, s, decidable_linear_order.to_lattice,
-  le_of_lt := @le_of_lt A s,
-  add_le_add_left := add_le_add_left' A s,
-  lt_of_le_of_lt := @lt_of_le_of_lt A s,
-  lt_of_lt_of_le := @lt_of_lt_of_le A s ⦄
-
-section
-  variables [s : decidable_linear_ordered_comm_group A]
-  variables {a b c d e : A}
-  include s
 
   theorem eq_zero_of_neg_eq (H : -a = a) : a = 0 :=
   lt.by_cases

library/algebra/ordered_ring.lean

@@ -15,9 +15,11 @@ namespace algebra
 
 variable {A : Type}
 
-definition absurd_a_lt_a {B : Type} {a : A} [s : strict_order A] (H : a < a) : B :=
+private definition absurd_a_lt_a {B : Type} {a : A} [s : strict_order A] (H : a < a) : B :=
 absurd H (lt.irrefl a)
 
+/- semiring structures -/
+
 structure ordered_semiring [class] (A : Type)
   extends semiring A, ordered_cancel_comm_monoid A :=
 (mul_le_mul_of_nonneg_left: ∀a b c, le a b → le zero c → le (mul c a) (mul c b))
@@ -187,6 +189,11 @@ section
       not_le_of_gt (mul_pos H2 H1) H)
 end
 
+structure decidable_linear_ordered_semiring [class] (A : Type)
+  extends linear_ordered_semiring A, decidable_linear_order A
+
+/- ring structures -/
+
 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))

library/data/bag.lean

@@ -516,10 +516,10 @@ calc empty ∩ b = b ∩ empty : inter.comm
 
 lemma append_union_inter (b₁ b₂ : bag A) : (b₁ ∪ b₂) ++ (b₁ ∩ b₂) = b₁ ++ b₂ :=
 bag.ext (λ a, begin
-  rewrite [*count_append, count_inter, count_union], unfold [max, min],
+  rewrite [*count_append, count_inter, count_union],
-  apply (@by_cases (count a b₁ < count a b₂)),
+  apply (or.elim (lt_or_ge (count a b₁) (count a b₂))),
-  { intro H, rewrite [*if_pos H, add.comm] },
+  { intro H, rewrite [min_eq_left_of_lt H, max_eq_right_of_lt H, add.comm] },
-  { intro H, rewrite [*if_neg H, add.comm] }
+  { intro H, rewrite [min_eq_right H, max_eq_left H, add.comm] }
 end)
 
 lemma inter.left_distrib (b₁ b₂ b₃ : bag A) : b₁ ∩ (b₂ ∪ b₃) = (b₁ ∩ b₂) ∪ (b₁ ∩ b₃) :=
@@ -620,10 +620,10 @@ open decidable
 
 lemma union_subbag_append (b₁ b₂ : bag A) : b₁ ∪ b₂ ⊆ b₁ ++ b₂ :=
 subbag.intro (take a, begin
-  rewrite [count_append, count_union], unfold max,
+  rewrite [count_append, count_union],
-  exact by_cases
+  exact (or.elim !lt_or_ge)
-   (suppose count a b₁ < count a b₂,   by rewrite [if_pos this]; apply le_add_left)
+   (suppose count a b₁ < count a b₂,   by rewrite [max_eq_right_of_lt this]; apply le_add_left)
-   (suppose ¬ count a b₁ < count a b₂, by rewrite [if_neg this]; apply le_add_right)
+   (suppose count a b₁ ≥ count a b₂, by rewrite [max_eq_left this]; apply le_add_right)
 end)
 
 lemma subbag_insert (a : A) (b : bag A) : b ⊆ insert a b :=

library/data/nat/order.lean

@@ -90,7 +90,7 @@ theorem mul_lt_mul_of_pos_right {n m k : ℕ} (H : n < m) (Hk : k > 0) : n * k <
 !mul.comm ▸ !mul.comm ▸ mul_lt_mul_of_pos_left H Hk
 
 /- min and max -/
-
+/-
 definition max (a b : ℕ) : ℕ := if a < b then b else a
 definition min (a b : ℕ) : ℕ := if a < b then a else b
 
@@ -131,16 +131,17 @@ lt.by_cases
 theorem le_max_left (a b : ℕ) : a ≤ max a b :=
 if h : a < b then le_of_lt (eq.rec_on (eq_max_right h) h)
 else (eq_max_left h) ▸ !le.refl
+-/
 
-/- nat is an instance of a linearly ordered semiring and a lattice-/
+/- nat is an instance of a linearly ordered semiring and a lattice -/
 
 section migrate_algebra
   open [classes] algebra
   local attribute nat.comm_semiring [instance]
 
-  protected definition linear_ordered_semiring [reducible] :
+  protected definition decidable_linear_ordered_semiring [reducible] :
-    algebra.linear_ordered_semiring nat :=
+    algebra.decidable_linear_ordered_semiring nat :=
-  ⦃ algebra.linear_ordered_semiring, nat.comm_semiring,
+  ⦃ algebra.decidable_linear_ordered_semiring, nat.comm_semiring,
     add_left_cancel            := @add.cancel_left,
     add_right_cancel           := @add.cancel_right,
     lt                         := lt,
@@ -162,8 +163,10 @@ section migrate_algebra
     mul_le_mul_of_nonneg_left  := (take a b c H1 H2, mul_le_mul_left c H1),
     mul_le_mul_of_nonneg_right := (take a b c H1 H2, mul_le_mul_right c H1),
     mul_lt_mul_of_pos_left     := @mul_lt_mul_of_pos_left,
-    mul_lt_mul_of_pos_right    := @mul_lt_mul_of_pos_right ⦄
+    mul_lt_mul_of_pos_right    := @mul_lt_mul_of_pos_right,
+    decidable_lt               := nat.decidable_lt ⦄
 
+/-
   protected definition lattice [reducible] : algebra.lattice nat :=
   ⦃ algebra.lattice, nat.linear_ordered_semiring,
     min          := min,
@@ -177,6 +180,11 @@ section migrate_algebra
 
   local attribute nat.linear_ordered_semiring [instance]
   local attribute nat.lattice [instance]
+-/
+  local attribute nat.decidable_linear_ordered_semiring [instance]
+
+  definition min : ℕ → ℕ → ℕ := algebra.min
+  definition max : ℕ → ℕ → ℕ := algebra.max
 
   migrate from algebra with nat
     replacing dvd → dvd, has_le.ge → ge, has_lt.gt → gt, min → min, max → max
@@ -417,32 +425,17 @@ theorem zero_max [simp] (a : ℕ) : max 0 a = a :=
 by rewrite [max_eq_right !zero_le]
 
 theorem min_succ_succ [simp] (a b : ℕ) : min (succ a) (succ b) = succ (min a b) :=
-by_cases
+or.elim !lt_or_ge
-  (suppose a < b,   by unfold min; rewrite [if_pos this, if_pos (succ_lt_succ this)])
+  (suppose a < b, by rewrite [min_eq_left_of_lt this, min_eq_left_of_lt (succ_lt_succ this)])
-  (suppose ¬ a < b,
+  (suppose a ≥ b, by rewrite [min_eq_right this, min_eq_right (succ_le_succ this)])
-   assert h : ¬ succ a < succ b, from assume h, absurd (lt_of_succ_lt_succ h) this,
-   by unfold min; rewrite [if_neg this, if_neg h])
 
 theorem max_succ_succ [simp] (a b : ℕ) : max (succ a) (succ b) = succ (max a b) :=
-by_cases
+or.elim !lt_or_ge
-  (suppose a < b,   by unfold max; rewrite [if_pos this, if_pos (succ_lt_succ this)])
+  (suppose a < b, by rewrite [max_eq_right_of_lt this, max_eq_right_of_lt (succ_lt_succ this)])
-  (suppose ¬ a < b,
+  (suppose a ≥ b, by rewrite [max_eq_left this, max_eq_left (succ_le_succ this)])
-   assert ¬ succ a < succ b, from assume h, absurd (lt_of_succ_lt_succ h) this,
-   by unfold max; rewrite [if_neg `¬ a < b`, if_neg `¬ succ a < succ b`])
 
-theorem lt_min {a b c : ℕ} (H₁ : a < b) (H₂ : a < c) : a < min b c :=
+/- In algebra.ordered_group, these next four are only proved for additive groups, not additive
-decidable.by_cases
+   semigroups. -/
-  (suppose b ≤ c, by rewrite (min_eq_left this); apply H₁)
-  (suppose ¬ b ≤ c,
-   assert c ≤ b, from le_of_lt (lt_of_not_ge this),
-   by rewrite (min_eq_right this); apply H₂)
-
-theorem max_lt {a b c : ℕ} (H₁ : a < c) (H₂ : b < c) : max a b < c :=
-decidable.by_cases
-  (suppose a ≤ b, by rewrite (max_eq_right this); apply H₂)
-  (suppose ¬ a ≤ b,
-   assert b ≤ a, from le_of_lt (lt_of_not_ge this),
-   by rewrite (max_eq_left this); apply H₁)
 
 theorem min_add_add_left (a b c : ℕ) : min (a + b) (a + c) = a + min b c :=
 decidable.by_cases
@@ -470,18 +463,6 @@ 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 min_eq_left_of_lt {a b : ℕ} (H : a < b) : min a b = a :=
-min_eq_left (le_of_lt H)
-
-theorem min_eq_right_of_lt {a b : ℕ} (H : b < a) : min a b = b :=
-min_eq_right (le_of_lt H)
-
-theorem max_eq_left_of_lt {a b : ℕ} (H : b < a) : max a b = a :=
-max_eq_left (le_of_lt H)
-
-theorem max_eq_right_of_lt {a b : ℕ} (H : a < b) : max a b = b :=
-max_eq_right (le_of_lt H)
-
 /- least and greatest -/
 
 section least_and_greatest

library/data/nat/power.lean

@@ -12,7 +12,7 @@ namespace nat
 section migrate_algebra
   open [classes] algebra
   local attribute nat.comm_semiring [instance]
-  local attribute nat.linear_ordered_semiring [instance]
+  local attribute nat.decidable_linear_ordered_semiring [instance]
 
   definition pow (a : ℕ) (n : ℕ) : ℕ := algebra.pow a n
   infix ^ := pow