feat(library/algebra): update algebraic hierarchy to be more constructive

This commit is contained in:
Rob Lewis 2015-05-29 13:33:45 +10:00
parent 7342f342a9
commit 4b67cd1f97
3 changed files with 164 additions and 65 deletions

View file

@ -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')

View file

@ -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]

View file

@ -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) :=