diff --git a/library/algebra/order.lean b/library/algebra/order.lean index bc7049252..e20650e31 100644 --- a/library/algebra/order.lean +++ b/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 -/ @@ -313,7 +312,7 @@ structure linear_strong_order_pair [class] (A : Type) extends strong_order_pair definition linear_strong_order_pair.to_linear_order_pair [trans-instance] [coercion] [reducible] [s : linear_strong_order_pair A] : linear_order_pair A := -⦃ linear_order_pair, s, strong_order_pair.to_order_pair⦄ +⦃ linear_order_pair, s, strong_order_pair.to_order_pair ⦄ section variable [s : linear_strong_order_pair A] @@ -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 diff --git a/library/algebra/ordered_ring.lean b/library/algebra/ordered_ring.lean index cf70b13be..68b5c5cfe 100644 --- a/library/algebra/ordered_ring.lean +++ b/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 := diff --git a/library/data/int/order.lean b/library/data/int/order.lean index 2e54fb3d9..2f36c795a 100644 --- a/library/data/int/order.lean +++ b/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 diff --git a/library/data/nat/order.lean b/library/data/nat/order.lean index 149385657..9a67c1ea9 100644 --- a/library/data/nat/order.lean +++ b/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 diff --git a/library/data/pnat.lean b/library/data/pnat.lean index 440b52299..4073069af 100644 --- a/library/data/pnat.lean +++ b/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 diff --git a/library/init/nat.lean b/library/init/nat.lean index 2bc07fa85..f7b0c3b88 100644 --- a/library/init/nat.lean +++ b/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