fix(library/algebra/order): decidable_linear_order

Add fields for decidable_eq and decidable_le.
We need this because a concrete instance may have its own
implementation that is not definitionally equal to
the old ones defined at library/algebra/order.lean.
Without this change, types such as nat and int would
have multiple definitions for decidable_eq and decidable_le
which are not definitionally equal.

library/algebra/order.lean

@@ -1,33 +0,0 @@
-/-
-Copyright (c) 2014 Jeremy Avigad. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Author: Jeremy Avigad
-
-This ports just the min function and theorems from the lean2 library; additional
-functions will be ported in the future.
--/
-
-/- min -/
-
-definition min {α : Type} [has_le α] (a b : α) [decidable (a ≤ b)] : α :=
-  if a ≤ b then a else b
-
-theorem min_eq_left {α : Type} [has_le α] {a b : α} [decidable (a ≤ b)]
-  (H : a ≤ b) : min a b = a := if_pos H
-
-theorem min_eq_right {α : Type} [weak_order α] {x y : α}
-           [p : decidable (x ≤ y)] (H : (y ≤ x)) : min x y = y :=
-  let q : decidable (x ≤ y) := p in
-  match q with
-  | is_true h :=
-      calc min x y = x : if_pos h
-               ... = y : le_antisymm h H
-  | is_false h := if_neg h
-  end
-
-theorem min_self {α : Type} [has_le α] (x : α) [p : decidable (x ≤ x)] : min x x = x :=
-   let q : decidable (x ≤ x) := p in
-   match q with
-   | is_true  h := if_pos h
-   | is_false h := if_neg h
-   end

library/data/list.lean

@@ -6,8 +6,6 @@ Author: Jeremy Avigad
 This is a minimal port of functions from the lean2 list library.
 -/
 import init.data.list.basic
-import algebra.order
-import data.nat
 
 universe variables u v w
 

library/data/nat.lean

@@ -1,30 +0,0 @@
-/-
-Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Author: Jeremy Avigad
-
-This is a minimal port of functions from the lean2 library.
--/
-import algebra.order
-
-namespace nat
-
-  /- min -/
-
-  theorem min_zero_left (a : ℕ) : min 0 a = 0 := min_eq_left (zero_le a)
-
-  theorem min_zero_right (a : ℕ) : min a 0 = 0 := min_eq_right (zero_le a)
-
-  -- Distribute succ over min
-  theorem min_succ_succ (x y : ℕ) : min (succ x) (succ y) = succ (min x y) :=
-    let f : x ≤ y → min (succ x) (succ y) = succ (min x y) := λp,
-          calc min (succ x) (succ y)
-                     = succ x         : if_pos (succ_le_succ p)
-                 ... = succ (min x y) : congr_arg succ (eq.symm (if_pos p)) in
-    let g : ¬ (x ≤ y) → min (succ x) (succ y) = succ (min x y) := λp,
-          calc min (succ x) (succ y)
-                     = succ y         : if_neg (λeq, p (pred_le_pred eq))
-                 ... = succ (min x y) : congr_arg succ (eq.symm (if_neg p)) in
-    decidable.by_cases f g
-
-end nat

library/init/algebra/default.lean

@@ -5,4 +5,4 @@ Authors: Leonardo de Moura
 -/
 prelude
 import init.algebra.group init.algebra.ordered_group init.algebra.ring init.algebra.ordered_ring
-import init.algebra.field init.algebra.norm_num
+import init.algebra.field init.algebra.norm_num init.algebra.functions

library/init/algebra/field.lean

@@ -10,6 +10,10 @@ prelude
 import init.algebra.ring
 universe variables u
 
+/- Make sure instances defined in this file have lower priority than the ones
+   defined for concrete structures -/
+set_option default_priority 100
+
 class division_ring (α : Type u) extends ring α, has_inv α, zero_ne_one_class α :=
 (mul_inv_cancel : ∀ {a : α}, a ≠ 0 → a * a⁻¹ = 1)
 (inv_mul_cancel : ∀ {a : α}, a ≠ 0 → a⁻¹ * a = 1)

library/init/algebra/order.lean

@@ -39,9 +39,6 @@ class linear_order_pair (α : Type u) extends order_pair α, linear_weak_order
 
 class linear_strong_order_pair (α : Type u) extends strong_order_pair α, linear_weak_order α
 
-class decidable_linear_order (α : Type u) extends linear_strong_order_pair α :=
-(decidable_lt : decidable_rel lt)
-
 @[refl] lemma le_refl [weak_order α] : ∀ a : α, a ≤ a :=
 weak_order.le_refl
 
@@ -210,20 +207,38 @@ match lt_trichotomy a b with
 | or.inr (or.inr hgt) := or.inr hgt
 end
 
-instance [decidable_linear_order α] (a b : α) : decidable (a < b) :=
-decidable_linear_order.decidable_lt α a b
-
-instance [decidable_linear_order α] (a b : α) : decidable (a ≤ b) :=
+/- The following lemma can be used when defining a decidable_linear_order instance, and the concrete structure
+   does not have its own definition for decidable le  -/
+def decidable_le_of_decidable_lt [linear_strong_order_pair α] [∀ a b : α, decidable (a < b)] (a b : α) : decidable (a ≤ b) :=
 if h₁ : a < b      then is_true (le_of_lt h₁)
 else if h₂ : b < a then is_false (not_le_of_gt h₂)
 else                    is_true (le_of_not_gt h₂)
 
+/- The following lemma can be used when defining a decidable_linear_order instance, and the concrete structure
+   does not have its own definition for decidable le -/
+def decidable_eq_of_decidable_lt [linear_strong_order_pair α] [∀ a b : α, decidable (a < b)] (a b : α) : decidable (a = b) :=
+match decidable_le_of_decidable_lt a b with
+| is_true h₁  :=
+  match decidable_le_of_decidable_lt b a with
+  | is_true h₂  := is_true (le_antisymm h₁ h₂)
+  | is_false h₂ := is_false (λ he : a = b, h₂ (he ▸ le_refl a))
+  end
+| is_false h₁ := is_false (λ he : a = b, h₁ (he ▸ le_refl a))
+end
+
+class decidable_linear_order (α : Type u) extends linear_strong_order_pair α :=
+(decidable_lt : decidable_rel lt)
+(decidable_le : decidable_rel le) -- TODO(Leo): add default value using decidable_le_of_decidable_lt
+(decidable_eq : decidable_eq α)   -- TODO(Leo): add default value using decidable_eq_of_decidable_lt
+
+instance [decidable_linear_order α] (a b : α) : decidable (a < b) :=
+decidable_linear_order.decidable_lt α a b
+
+instance [decidable_linear_order α] (a b : α) : decidable (a ≤ b) :=
+decidable_linear_order.decidable_le α a b
+
 instance [decidable_linear_order α] (a b : α) : decidable (a = b) :=
-if h₁ : a ≤ b then
-  if h₂ : b ≤ a
-  then is_true (le_antisymm h₁ h₂)
-  else is_false (λ he : a = b, h₂ (he ▸ le_refl a))
-else is_false (λ he : a = b, h₁ (he ▸ le_refl a))
+decidable_linear_order.decidable_eq α a b
 
 lemma eq_or_lt_of_not_lt [decidable_linear_order α] {a b : α} (h : ¬ a < b) : a = b ∨ b < a :=
 if h₁ : a = b then or.inl h₁

library/init/data/nat/lemmas.lean

@@ -386,7 +386,9 @@ instance : decidable_linear_ordered_semiring nat :=
   mul_le_mul_of_nonneg_right := (take a b c h₁ h₂, nat.mul_le_mul_right c h₁),
   mul_lt_mul_of_pos_left     := @nat.mul_lt_mul_of_pos_left,
   mul_lt_mul_of_pos_right    := @nat.mul_lt_mul_of_pos_right,
-  decidable_lt               := nat.decidable_lt }
+  decidable_lt               := nat.decidable_lt,
+  decidable_le               := nat.decidable_le,
+  decidable_eq               := nat.decidable_eq }
 
 lemma le_of_lt_succ {m n : nat} : m < succ n → m ≤ n :=
 le_of_succ_le_succ
@@ -671,6 +673,25 @@ exists.elim (nat.le.dest h)
   (take l, assume hl : k + l = m,
     by rw [-hl, nat.add_sub_cancel_left, add_comm k, -add_assoc, nat.add_sub_cancel])
 
+lemma min_zero_left (a : ℕ) : min 0 a = 0 :=
+min_eq_left (zero_le a)
+
+lemma min_zero_right (a : ℕ) : min a 0 = 0 :=
+min_eq_right (zero_le a)
+
+-- Distribute succ over min
+lemma min_succ_succ (x y : ℕ) : min (succ x) (succ y) = succ (min x y) :=
+have f : x ≤ y → min (succ x) (succ y) = succ (min x y), from λp,
+  calc min (succ x) (succ y)
+              = succ x         : if_pos (succ_le_succ p)
+          ... = succ (min x y) : congr_arg succ (eq.symm (if_pos p)),
+have g : ¬ (x ≤ y) → min (succ x) (succ y) = succ (min x y), from λp,
+  calc min (succ x) (succ y)
+              = succ y         : if_neg (λeq, p (pred_le_pred eq))
+          ... = succ (min x y) : congr_arg succ (eq.symm (if_neg p)),
+decidable.by_cases f g
+
 /- TODO(Leo): sub + inequalities -/
 
+
 end nat