From 4b67cd1f97e595bf0ffbf4450157681477a63f1c Mon Sep 17 00:00:00 2001 From: Rob Lewis Date: Fri, 29 May 2015 13:33:45 +1000 Subject: [PATCH] feat(library/algebra): update algebraic hierarchy to be more constructive --- library/algebra/order.lean | 163 ++++++++++++++++++++--------- library/algebra/ordered_group.lean | 53 ++++++++-- library/algebra/ordered_ring.lean | 13 ++- 3 files changed, 164 insertions(+), 65 deletions(-) diff --git a/library/algebra/order.lean b/library/algebra/order.lean index 5085627797..14d45adee8 100644 --- a/library/algebra/order.lean +++ b/library/algebra/order.lean @@ -116,63 +116,31 @@ wf.rec_on x H /- structures with a weak and a strict order -/ structure order_pair [class] (A : Type) extends weak_order A, has_lt A := -(lt_iff_le_and_ne : ∀a b, lt a b ↔ (le a b ∧ a ≠ b)) +(le_of_lt : ∀ a b, lt a b → le a b) +(lt_of_lt_of_le : ∀ a b c, lt a b → le b c → lt a c) +(lt_of_le_of_lt : ∀ a b c, le a b → lt b c → lt a c) +(lt_irrefl : ∀ a, ¬ lt a a) +--lt_iff_le_and_ne : a < b ↔ (a ≤ b ∧ a ≠ b) section variable [s : order_pair A] variables {a b c : A} include s - theorem lt_iff_le_and_ne : a < b ↔ (a ≤ b ∧ a ≠ b) := - !order_pair.lt_iff_le_and_ne + theorem le_of_lt : a < b → a ≤ b := !order_pair.le_of_lt - theorem le_of_lt (H : a < b) : a ≤ b := - and.elim_left (iff.mp lt_iff_le_and_ne H) + theorem lt_of_lt_of_le [trans] : a < b → b ≤ c → a < c := !order_pair.lt_of_lt_of_le - theorem lt_of_le_of_ne (H1 : a ≤ b) (H2 : a ≠ b) : a < b := - iff.mp (iff.symm lt_iff_le_and_ne) (and.intro H1 H2) + theorem lt_of_le_of_lt [trans] : a ≤ b → b < c → a < c := !order_pair.lt_of_le_of_lt - private theorem lt_irrefl (s' : order_pair A) (a : A) : ¬ a < a := - assume H : a < a, - have H1 : a ≠ a, from and.elim_right (iff.mp !lt_iff_le_and_ne H), - H1 rfl + private theorem lt_irrefl (s' : order_pair A) (a : A) : ¬ a < a := !order_pair.lt_irrefl private theorem lt_trans (s' : order_pair A) (a b c: A) (lt_ab : a < b) (lt_bc : b < c) : a < c := - have le_ab : a ≤ b, from le_of_lt lt_ab, - have le_bc : b ≤ c, from le_of_lt lt_bc, - have le_ac : a ≤ c, from le.trans le_ab le_bc, - have ne_ac : a ≠ c, from - assume eq_ac : a = c, - have le_ba : b ≤ a, from eq_ac⁻¹ ▸ le_bc, - have eq_ab : a = b, from le.antisymm le_ab le_ba, - have ne_ab : a ≠ b, from and.elim_right (iff.mp lt_iff_le_and_ne lt_ab), - ne_ab eq_ab, - show a < c, from lt_of_le_of_ne le_ac ne_ac + lt_of_lt_of_le lt_ab (le_of_lt lt_bc) definition order_pair.to_strict_order [instance] [coercion] [reducible] : strict_order A := ⦃ strict_order, s, lt_irrefl := lt_irrefl s, lt_trans := lt_trans s ⦄ - theorem lt_of_lt_of_le [trans] : a < b → b ≤ c → a < c := - assume lt_ab : a < b, - assume le_bc : b ≤ c, - have le_ac : a ≤ c, from le.trans (le_of_lt lt_ab) le_bc, - have ne_ac : a ≠ c, from - assume eq_ac : a = c, - have le_ba : b ≤ a, from eq_ac⁻¹ ▸ le_bc, - have eq_ab : a = b, from le.antisymm (le_of_lt lt_ab) le_ba, - show false, from ne_of_lt lt_ab eq_ab, - show a < c, from lt_of_le_of_ne le_ac ne_ac - - theorem lt_of_le_of_lt [trans] : a ≤ b → b < c → a < c := - assume le_ab : a ≤ b, - assume lt_bc : b < c, - have le_ac : a ≤ c, from le.trans le_ab (le_of_lt lt_bc), - have ne_ac : a ≠ c, from - assume eq_ac : a = c, - have le_cb : c ≤ b, from eq_ac ▸ le_ab, - have eq_bc : b = c, from le.antisymm (le_of_lt lt_bc) le_cb, - show false, from ne_of_lt lt_bc eq_bc, - show a < c, from lt_of_le_of_ne le_ac ne_ac theorem gt_of_gt_of_ge [trans] (H1 : a > b) (H2 : b ≥ c) : a > c := lt_of_le_of_lt H2 H1 @@ -187,8 +155,9 @@ section lt.irrefl _ (lt_of_le_of_lt H H1) end -structure strong_order_pair [class] (A : Type) extends order_pair A := +structure strong_order_pair [class] (A : Type) extends weak_order A, has_lt A := --order_pair A := (le_iff_lt_or_eq : ∀a b, le a b ↔ lt a b ∨ a = b) +(lt_irrefl : ∀ a, ¬ lt a a) theorem le_iff_lt_or_eq [s : strong_order_pair A] {a b : A} : a ≤ b ↔ a < b ∨ a = b := !strong_order_pair.le_iff_lt_or_eq @@ -196,6 +165,60 @@ theorem le_iff_lt_or_eq [s : strong_order_pair A] {a b : A} : a ≤ b ↔ a < b theorem lt_or_eq_of_le [s : strong_order_pair A] {a b : A} (le_ab : a ≤ b) : a < b ∨ a = b := iff.mp le_iff_lt_or_eq le_ab +theorem le_of_lt_or_eq [s : strong_order_pair A] {a b : A} (lt_or_eq : a < b ∨ a = b) : a ≤ b := + iff.mp' le_iff_lt_or_eq lt_or_eq + +private theorem lt_irrefl' [s : strong_order_pair A] (a : A) : ¬ a < a := + !strong_order_pair.lt_irrefl + +private theorem le_of_lt' [s : strong_order_pair A] (a b : A) : a < b → a ≤ b := + take Hlt, le_of_lt_or_eq (or.inl Hlt) + +private theorem lt_iff_le_and_ne [s : strong_order_pair A] {a b : A} : a < b ↔ (a ≤ b ∧ a ≠ b) := + iff.intro + (take Hlt, and.intro (le_of_lt_or_eq (or.inl Hlt)) (take Hab, absurd (Hab ▸ Hlt) !lt_irrefl')) + (take Hand, + have Hor : a < b ∨ a = b, from lt_or_eq_of_le (and.left Hand), + or_resolve_left Hor (and.right Hand)) + +theorem lt_of_le_of_ne [s : strong_order_pair A] {a b : A} : a ≤ b → a ≠ b → a < b := + take H1 H2, iff.mp' lt_iff_le_and_ne (and.intro H1 H2) + +private theorem ne_of_lt' [s : strong_order_pair A] {a b : A} (H : a < b) : a ≠ b := + and.right ((iff.mp lt_iff_le_and_ne) H) + +private theorem lt_of_lt_of_le' [s : strong_order_pair A] (a b c : A) : a < b → b ≤ c → a < c := + assume lt_ab : a < b, + assume le_bc : b ≤ c, + have le_ac : a ≤ c, from le.trans (le_of_lt' _ _ lt_ab) le_bc, + have ne_ac : a ≠ c, from + assume eq_ac : a = c, + have le_ba : b ≤ a, from eq_ac⁻¹ ▸ le_bc, + have eq_ab : a = b, from le.antisymm (le_of_lt' _ _ lt_ab) le_ba, + show false, from ne_of_lt' lt_ab eq_ab, + show a < c, from iff.mp' (lt_iff_le_and_ne) (and.intro le_ac ne_ac) + + theorem lt_of_le_of_lt' [s : strong_order_pair A] (a b c : A) : a ≤ b → b < c → a < c := + assume le_ab : a ≤ b, + assume lt_bc : b < c, + have le_ac : a ≤ c, from le.trans le_ab (le_of_lt' _ _ lt_bc), + have ne_ac : a ≠ c, from + assume eq_ac : a = c, + have le_cb : c ≤ b, from eq_ac ▸ le_ab, + have eq_bc : b = c, from le.antisymm (le_of_lt' _ _ lt_bc) le_cb, + show false, from ne_of_lt' lt_bc eq_bc, + show a < c, from iff.mp' (lt_iff_le_and_ne) (and.intro le_ac ne_ac) + + +definition strong_order_pair.to_order_pair [instance] [coercion] [reducible] [s : strong_order_pair A] + : order_pair A := + ⦃ order_pair, s, + 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' + ⦄ + -- We can also construct a strong order pair by defining a strict order, and then defining -- x ≤ y ↔ x < y ∨ x = y @@ -235,13 +258,55 @@ iff.intro iff.mp !strict_order_with_le.le_iff_lt_or_eq (and.elim_left H), show a < b, from or_resolve_left H1 (and.elim_right H)) +private theorem le_of_lt' (s : strict_order_with_le A) (a b : A) : a < b → a ≤ b := + take Hlt, and.left (iff.mp (lt_iff_le_ne s _ _) Hlt) + +private theorem lt_trans (s : strict_order_with_le A) (a b c: A) (lt_ab : a < b) (lt_bc : b < c) : a < c := + have le_ab : a ≤ b, from le_of_lt' s _ _ lt_ab, + have le_bc : b ≤ c, from le_of_lt' s _ _ lt_bc, + have le_ac : a ≤ c, from le_trans s _ _ _ le_ab le_bc, + have ne_ac : a ≠ c, from + assume eq_ac : a = c, + have le_ba : b ≤ a, from eq_ac⁻¹ ▸ le_bc, + have eq_ab : a = b, from le_antisymm s a b le_ab le_ba, + have ne_ab : a ≠ b, from and.elim_right ((iff.mp (lt_iff_le_ne s a b)) lt_ab), + ne_ab eq_ab, + show a < c, from (iff.mp' !lt_iff_le_ne) (and.intro le_ac ne_ac) + + theorem lt_of_lt_of_le' (s : strict_order_with_le A) (a b c : A) : a < b → b ≤ c → a < c := + assume lt_ab : a < b, + assume le_bc : b ≤ c, + have le_ac : a ≤ c, from le_trans s _ _ _ (le_of_lt' s _ _ lt_ab) le_bc, + have ne_ac : a ≠ c, from + assume eq_ac : a = c, + have le_ba : b ≤ a, from eq_ac⁻¹ ▸ le_bc, + have eq_ab : a = b, from le_antisymm s _ _ (le_of_lt' s _ _ lt_ab) le_ba, + show false, from ne_of_lt lt_ab eq_ab, + show a < c, from iff.mp' (lt_iff_le_ne s _ _) (and.intro le_ac ne_ac) + + theorem lt_of_le_of_lt'' (s : strict_order_with_le A) (a b c : A) : a ≤ b → b < c → a < c := + assume le_ab : a ≤ b, + assume lt_bc : b < c, + have le_ac : a ≤ c, from le_trans s _ _ _ le_ab (le_of_lt' s _ _ lt_bc), + have ne_ac : a ≠ c, from + assume eq_ac : a = c, + have le_cb : c ≤ b, from eq_ac ▸ le_ab, + have eq_bc : b = c, from le_antisymm s _ _ (le_of_lt' s _ _ lt_bc) le_cb, + show false, from ne_of_lt lt_bc eq_bc, + show a < c, from iff.mp' (lt_iff_le_ne s _ _) (and.intro le_ac ne_ac) + + definition strict_order_with_le.to_order_pair [instance] [coercion] [reducible] [s : strict_order_with_le A] : strong_order_pair A := ⦃ strong_order_pair, s, le_refl := le_refl s, le_trans := le_trans s, - le_antisymm := le_antisymm s, - lt_iff_le_and_ne := lt_iff_le_ne s ⦄ + le_antisymm := le_antisymm s ⦄ + --le_of_lt := le_of_lt' s, + --lt_of_le_of_lt := lt_of_le_of_lt' s, + --lt_of_lt_of_le := lt_of_lt_of_le' s ⦄ + --lt_iff_le_and_ne := lt_iff_le_ne s ⦄ + /- linear orders -/ @@ -250,6 +315,10 @@ structure linear_order_pair [class] (A : Type) extends order_pair A, linear_weak structure linear_strong_order_pair [class] (A : Type) extends strong_order_pair A, linear_weak_order A +definition linear_strong_order_pair.to_linear_order_pair [instance] [coercion] [reducible] + [s : linear_strong_order_pair A] : linear_order_pair A := + ⦃ linear_order_pair, s, strong_order_pair.to_order_pair⦄ + section variable [s : linear_strong_order_pair A] variables (a b c : A) @@ -270,10 +339,6 @@ section (assume H, H1 H) (assume H, or.elim H (assume H', H2 H') (assume H', H3 H')) - definition linear_strong_order_pair.to_linear_order_pair [instance] [coercion] [reducible] - : linear_order_pair A := - ⦃ linear_order_pair, s ⦄ - theorem le_of_not_gt {a b : A} (H : ¬ a > b) : a ≤ b := lt.by_cases (assume H', absurd H' H) (assume H', H' ▸ !le.refl) (assume H', le_of_lt H') diff --git a/library/algebra/ordered_group.lean b/library/algebra/ordered_group.lean index 87a6f3394a..a8fab7a7bd 100644 --- a/library/algebra/ordered_group.lean +++ b/library/algebra/ordered_group.lean @@ -22,12 +22,23 @@ structure ordered_cancel_comm_monoid [class] (A : Type) extends add_comm_monoid add_left_cancel_semigroup A, add_right_cancel_semigroup A, order_pair A := (add_le_add_left : ∀a b, le a b → ∀c, le (add c a) (add c b)) (le_of_add_le_add_left : ∀a b c, le (add a b) (add a c) → le b c) +(add_lt_add_left : ∀a b, lt a b → ∀c, lt (add c a) (add c b)) +(lt_of_add_lt_add_left : ∀a b c, lt (add a b) (add a c) → lt b c) section variables [s : ordered_cancel_comm_monoid A] variables {a b c d e : A} include s + theorem add_lt_add_left (H : a < b) (c : A) : c + a < c + b := + !ordered_cancel_comm_monoid.add_lt_add_left H c + + theorem add_lt_add_right (H : a < b) (c : A) : a + c < b + c := + begin + rewrite [add.comm, {b + _}add.comm], + exact (add_lt_add_left H c) + end + theorem add_le_add_left (H : a ≤ b) (c : A) : c + a ≤ c + b := !ordered_cancel_comm_monoid.add_le_add_left H c @@ -37,19 +48,15 @@ section theorem add_le_add (Hab : a ≤ b) (Hcd : c ≤ d) : a + c ≤ b + d := le.trans (add_le_add_right Hab c) (add_le_add_left Hcd b) - theorem add_lt_add_left (H : a < b) (c : A) : c + a < c + b := +/- theorem add_lt_add_left (H : a < b) (c : A) : c + a < c + b := have H1 : c + a ≤ c + b, from add_le_add_left (le_of_lt H) c, have H2 : c + a ≠ c + b, from take H3 : c + a = c + b, have H4 : a = b, from add.left_cancel H3, ne_of_lt H H4, - lt_of_le_of_ne H1 H2 + sorry--lt_of_le_of_ne H1 H2-/ + - theorem add_lt_add_right (H : a < b) (c : A) : a + c < b + c := - begin - rewrite [add.comm, {b + _}add.comm], - exact (add_lt_add_left H c) - end theorem le_add_of_nonneg_right (H : b ≥ 0) : a ≤ a + b := begin @@ -86,10 +93,11 @@ section le_of_add_le_add_left (show b + a ≤ b + c, begin rewrite [add.comm, {b + _}add.comm], exact H end) theorem lt_of_add_lt_add_left (H : a + b < a + c) : b < c := - have H1 : b ≤ c, from le_of_add_le_add_left (le_of_lt H), + !ordered_cancel_comm_monoid.lt_of_add_lt_add_left H + /-have H1 : b ≤ c, from le_of_add_le_add_left (le_of_lt H), have H2 : b ≠ c, from assume H3 : b = c, lt.irrefl _ (H3 ▸ H), - lt_of_le_of_ne H1 H2 + sorry --lt_of_le_of_ne H1 H2-/ theorem lt_of_add_lt_add_right (H : a + b < c + b) : a < c := lt_of_add_lt_add_left ((add.comm a b) ▸ (add.comm c b) ▸ H) @@ -208,17 +216,26 @@ end structure ordered_comm_group [class] (A : Type) extends add_comm_group A, order_pair 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)) +--(le_of_add_le_add_left : ∀a b c, le (add a b) (add a c) → le b c) +--(lt_of_add_lt_add_left : ∀a b c, lt (add a b) (add a c) → lt 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 := +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' + definition ordered_comm_group.to_ordered_cancel_comm_monoid [instance] [coercion] [reducible] [s : ordered_comm_group A] : ordered_cancel_comm_monoid A := ⦃ ordered_cancel_comm_monoid, s, add_left_cancel := @add.left_cancel A s, add_right_cancel := @add.right_cancel A s, - le_of_add_le_add_left := @ordered_comm_group.le_of_add_le_add_left A s ⦄ + le_of_add_le_add_left := @ordered_comm_group.le_of_add_le_add_left A s, + lt_of_add_lt_add_left := @ordered_comm_group.lt_of_add_lt_add_left A s⦄ section variables [s : ordered_comm_group A] (a b c d e : A) @@ -397,7 +414,21 @@ section end structure decidable_linear_ordered_comm_group [class] (A : Type) - extends ordered_comm_group A, decidable_linear_order 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)) + +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_ordered_comm_group [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, + 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] diff --git a/library/algebra/ordered_ring.lean b/library/algebra/ordered_ring.lean index 370846cb0f..83dd831ffd 100644 --- a/library/algebra/ordered_ring.lean +++ b/library/algebra/ordered_ring.lean @@ -11,7 +11,7 @@ of "linear_ordered_comm_ring". This development is modeled after Isabelle's libr import algebra.ordered_group algebra.ring open eq eq.ops -namespace algebra +namespace algebra variable {A : Type} @@ -197,7 +197,8 @@ definition ordered_ring.to_ordered_semiring [instance] [coercion] [reducible] [s mul_le_mul_of_nonneg_left := @ordered_ring.mul_le_mul_of_nonneg_left A s, mul_le_mul_of_nonneg_right := @ordered_ring.mul_le_mul_of_nonneg_right A s, mul_lt_mul_of_pos_left := @ordered_ring.mul_lt_mul_of_pos_left A s, - mul_lt_mul_of_pos_right := @ordered_ring.mul_lt_mul_of_pos_right A s ⦄ + mul_lt_mul_of_pos_right := @ordered_ring.mul_lt_mul_of_pos_right A s, + lt_of_add_lt_add_left := @lt_of_add_lt_add_left A s⦄ section variable [s : ordered_ring A] @@ -262,7 +263,8 @@ 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 @@ -279,7 +281,8 @@ definition linear_ordered_ring.to_linear_ordered_semiring [instance] [coercion] mul_le_mul_of_nonneg_right := @mul_le_mul_of_nonneg_right A s, mul_lt_mul_of_pos_left := @mul_lt_mul_of_pos_left A s, mul_lt_mul_of_pos_right := @mul_lt_mul_of_pos_right A s, - le_total := linear_ordered_ring.le_total ⦄ + le_total := linear_ordered_ring.le_total, + lt_of_add_lt_add_left := @lt_of_add_lt_add_left A s ⦄ structure linear_ordered_comm_ring [class] (A : Type) extends linear_ordered_ring A, comm_monoid A @@ -336,7 +339,7 @@ section (assume H : a ≤ 0, mul_nonneg_of_nonpos_of_nonpos H H) theorem zero_le_one : 0 ≤ (1:A) := one_mul 1 ▸ mul_self_nonneg 1 - theorem zero_lt_one : 0 < (1:A) := lt_of_le_of_ne zero_le_one zero_ne_one + theorem zero_lt_one : 0 < (1:A) := linear_ordered_ring.zero_lt_one A theorem pos_and_pos_or_neg_and_neg_of_mul_pos {a b : A} (Hab : a * b > 0) : (a > 0 ∧ b > 0) ∨ (a < 0 ∧ b < 0) :=