diff --git a/library/algebra/order.lean b/library/algebra/order.lean deleted file mode 100644 index 51c3fd6f68..0000000000 --- a/library/algebra/order.lean +++ /dev/null @@ -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 diff --git a/library/data/list.lean b/library/data/list.lean index c5769bcecd..e8e547189b 100644 --- a/library/data/list.lean +++ b/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 diff --git a/library/data/nat.lean b/library/data/nat.lean deleted file mode 100644 index 60bee6dcb0..0000000000 --- a/library/data/nat.lean +++ /dev/null @@ -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 diff --git a/library/init/algebra/default.lean b/library/init/algebra/default.lean index 86c4459107..d0868ee963 100644 --- a/library/init/algebra/default.lean +++ b/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 diff --git a/library/init/algebra/field.lean b/library/init/algebra/field.lean index f14660786b..ccf8f200ce 100644 --- a/library/init/algebra/field.lean +++ b/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) diff --git a/library/init/algebra/order.lean b/library/init/algebra/order.lean index 256d2fe129..0ba02f9998 100644 --- a/library/init/algebra/order.lean +++ b/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₁ diff --git a/library/init/data/nat/lemmas.lean b/library/init/data/nat/lemmas.lean index 81d1184c76..3ee00c413e 100644 --- a/library/init/data/nat/lemmas.lean +++ b/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