michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(library/algebra/ordered_ring): using new structure instance syntax sugar to define instances

Browse source
This commit is contained in:
Leonardo de Moura 2015-01-16 18:00:59 -08:00
parent 3d63c0b5dc
commit 50fe085374
1 changed files with 31 additions and 44 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

75
library/algebra/ordered_ring.lean
View file

@ -146,16 +146,13 @@ structure ordered_ring [class] (A : Type) extends ring A, ordered_comm_group A :
definition ordered_ring.to_ordered_semiring [instance] [coercion] [s : ordered_ring A] : definition ordered_ring.to_ordered_semiring [instance] [coercion] [s : ordered_ring A] :
ordered_semiring A := ordered_semiring A :=
ordered_semiring.mk ordered_ring.add ordered_ring.add_assoc !ordered_ring.zero ⦃ ordered_semiring,
ordered_ring.zero_add ordered_ring.add_zero ordered_ring.add_comm ordered_ring.mul mul_zero := mul_zero,
ordered_ring.mul_assoc !ordered_ring.one ordered_ring.one_mul ordered_ring.mul_one zero_mul := zero_mul,
ordered_ring.left_distrib ordered_ring.right_distrib add_left_cancel := @add.left_cancel A _,
zero_mul mul_zero !ordered_ring.zero_ne_one add_right_cancel := @add.right_cancel A _,
(@add.left_cancel A _) (@add.right_cancel A _) le_of_add_le_add_left := @le_of_add_le_add_left A _,
ordered_ring.le ordered_ring.le_refl ordered_ring.le_trans ordered_ring.le_antisymm mul_le_mul_of_nonneg_left := take a b c,
ordered_ring.lt ordered_ring.lt_iff_le_ne ordered_ring.add_le_add_left
(@le_of_add_le_add_left A _)
(take a b c,
assume Hab : a ≤ b, assume Hab : a ≤ b,
assume Hc : 0 ≤ c, assume Hc : 0 ≤ c,
show c * a ≤ c * b, show c * a ≤ c * b,
@ -163,8 +160,8 @@ ordered_semiring.mk ordered_ring.add ordered_ring.add_assoc !ordered_ring.zero
have H1 : 0 ≤ b - a, from iff.elim_right !sub_nonneg_iff_le Hab, have H1 : 0 ≤ b - a, from iff.elim_right !sub_nonneg_iff_le Hab,
have H2 : 0 ≤ c * (b - a), from ordered_ring.mul_nonneg _ _ Hc H1, have H2 : 0 ≤ c * (b - a), from ordered_ring.mul_nonneg _ _ Hc H1,
iff.mp !sub_nonneg_iff_le (!mul_sub_left_distrib ▸ H2) iff.mp !sub_nonneg_iff_le (!mul_sub_left_distrib ▸ H2)
qed) qed,
(take a b c, mul_le_mul_of_nonneg_right := take a b c,
assume Hab : a ≤ b, assume Hab : a ≤ b,
assume Hc : 0 ≤ c, assume Hc : 0 ≤ c,
show a * c ≤ b * c, show a * c ≤ b * c,
@ -172,8 +169,8 @@ ordered_semiring.mk ordered_ring.add ordered_ring.add_assoc !ordered_ring.zero
have H1 : 0 ≤ b - a, from iff.elim_right !sub_nonneg_iff_le Hab, have H1 : 0 ≤ b - a, from iff.elim_right !sub_nonneg_iff_le Hab,
have H2 : 0 ≤ (b - a) * c, from ordered_ring.mul_nonneg _ _ H1 Hc, have H2 : 0 ≤ (b - a) * c, from ordered_ring.mul_nonneg _ _ H1 Hc,
iff.mp !sub_nonneg_iff_le (!mul_sub_right_distrib ▸ H2) iff.mp !sub_nonneg_iff_le (!mul_sub_right_distrib ▸ H2)
qed) qed,
(take a b c, mul_lt_mul_of_pos_left := take a b c,
assume Hab : a < b, assume Hab : a < b,
assume Hc : 0 < c, assume Hc : 0 < c,
show c * a < c * b, show c * a < c * b,
@ -181,8 +178,8 @@ ordered_semiring.mk ordered_ring.add ordered_ring.add_assoc !ordered_ring.zero
have H1 : 0 < b - a, from iff.elim_right !sub_pos_iff_lt Hab, have H1 : 0 < b - a, from iff.elim_right !sub_pos_iff_lt Hab,
have H2 : 0 < c * (b - a), from ordered_ring.mul_pos _ _ Hc H1, have H2 : 0 < c * (b - a), from ordered_ring.mul_pos _ _ Hc H1,
iff.mp !sub_pos_iff_lt (!mul_sub_left_distrib ▸ H2) iff.mp !sub_pos_iff_lt (!mul_sub_left_distrib ▸ H2)
qed) qed,
(take a b c, mul_lt_mul_of_pos_right := take a b c,
assume Hab : a < b, assume Hab : a < b,
assume Hc : 0 < c, assume Hc : 0 < c,
show a * c < b * c, show a * c < b * c,
@ -190,7 +187,8 @@ ordered_semiring.mk ordered_ring.add ordered_ring.add_assoc !ordered_ring.zero
have H1 : 0 < b - a, from iff.elim_right !sub_pos_iff_lt Hab, have H1 : 0 < b - a, from iff.elim_right !sub_pos_iff_lt Hab,
have H2 : 0 < (b - a) * c, from ordered_ring.mul_pos _ _ H1 Hc, have H2 : 0 < (b - a) * c, from ordered_ring.mul_pos _ _ H1 Hc,
iff.mp !sub_pos_iff_lt (!mul_sub_right_distrib ▸ H2) iff.mp !sub_pos_iff_lt (!mul_sub_right_distrib ▸ H2)
qed) qed,
using s ⦄
section section
variable [s : ordered_ring A] variable [s : ordered_ring A]
@ -245,20 +243,18 @@ structure linear_ordered_ring [class] (A : Type) extends ordered_ring A, linear_
definition linear_ordered_ring.to_linear_ordered_semiring [instance] [coercion] definition linear_ordered_ring.to_linear_ordered_semiring [instance] [coercion]
[s : linear_ordered_ring A] : [s : linear_ordered_ring A] :
linear_ordered_semiring A := linear_ordered_semiring A :=
linear_ordered_semiring.mk linear_ordered_ring.add linear_ordered_ring.add_assoc ⦃ linear_ordered_semiring,
(@linear_ordered_ring.zero _ _) linear_ordered_ring.zero_add linear_ordered_ring.add_zero mul_zero := mul_zero,
linear_ordered_ring.add_comm linear_ordered_ring.mul linear_ordered_ring.mul_assoc zero_mul := zero_mul,
(@linear_ordered_ring.one _ _) linear_ordered_ring.one_mul linear_ordered_ring.mul_one add_left_cancel := @add.left_cancel A _,
linear_ordered_ring.left_distrib linear_ordered_ring.right_distrib add_right_cancel := @add.right_cancel A _,
zero_mul mul_zero !ordered_ring.zero_ne_one le_of_add_le_add_left := @le_of_add_le_add_left A _,
(@add.left_cancel A _) (@add.right_cancel A _) mul_le_mul_of_nonneg_left := @mul_le_mul_of_nonneg_left A _,
linear_ordered_ring.le linear_ordered_ring.le_refl linear_ordered_ring.le_trans mul_le_mul_of_nonneg_right := @mul_le_mul_of_nonneg_right A _,
linear_ordered_ring.le_antisymm mul_lt_mul_of_pos_left := @mul_lt_mul_of_pos_left A _,
linear_ordered_ring.lt linear_ordered_ring.lt_iff_le_ne linear_ordered_ring.add_le_add_left mul_lt_mul_of_pos_right := @mul_lt_mul_of_pos_right A _,
(@le_of_add_le_add_left A _) le_total := linear_ordered_ring.le_total,
(@mul_le_mul_of_nonneg_left A _) (@mul_le_mul_of_nonneg_right A _) using s ⦄
(@mul_lt_mul_of_pos_left A _) (@mul_lt_mul_of_pos_right A _)
linear_ordered_ring.le_iff_lt_or_eq linear_ordered_ring.le_total
structure linear_ordered_comm_ring [class] (A : Type) extends linear_ordered_ring A, comm_monoid A structure linear_ordered_comm_ring [class] (A : Type) extends linear_ordered_ring A, comm_monoid A
@ -266,18 +262,8 @@ structure linear_ordered_comm_ring [class] (A : Type) extends linear_ordered_rin
definition linear_ordered_comm_ring.to_integral_domain [instance] [coercion] definition linear_ordered_comm_ring.to_integral_domain [instance] [coercion]
[s: linear_ordered_comm_ring A] : [s: linear_ordered_comm_ring A] :
integral_domain A := integral_domain A :=
integral_domain.mk linear_ordered_comm_ring.add linear_ordered_comm_ring.add_assoc ⦃ integral_domain,
(@linear_ordered_comm_ring.zero _ _) eq_zero_or_eq_zero_of_mul_eq_zero := take a b,
linear_ordered_comm_ring.zero_add linear_ordered_comm_ring.add_zero
linear_ordered_comm_ring.neg linear_ordered_comm_ring.add_left_inv
linear_ordered_comm_ring.add_comm
linear_ordered_comm_ring.mul linear_ordered_comm_ring.mul_assoc
(@linear_ordered_comm_ring.one _ _)
linear_ordered_comm_ring.one_mul linear_ordered_comm_ring.mul_one
linear_ordered_comm_ring.left_distrib linear_ordered_comm_ring.right_distrib
(@linear_ordered_comm_ring.zero_ne_one _ _)
linear_ordered_comm_ring.mul_comm
(take a b,
assume H : a * b = 0, assume H : a * b = 0,
show a = 0 ∨ b = 0, from show a = 0 ∨ b = 0, from
lt.by_cases lt.by_cases
@ -291,7 +277,8 @@ integral_domain.mk linear_ordered_comm_ring.add linear_ordered_comm_ring.add_ass
lt.by_cases lt.by_cases
(assume Hb : 0 < b, absurd (H ▸ mul_neg_of_neg_of_pos Ha Hb) (lt.irrefl 0)) (assume Hb : 0 < b, absurd (H ▸ mul_neg_of_neg_of_pos Ha Hb) (lt.irrefl 0))
(assume Hb : 0 = b, or.inr (Hb⁻¹)) (assume Hb : 0 = b, or.inr (Hb⁻¹))
(assume Hb : 0 > b, absurd (H ▸ mul_pos_of_neg_of_neg Ha Hb) (lt.irrefl 0)))) (assume Hb : 0 > b, absurd (H ▸ mul_pos_of_neg_of_neg Ha Hb) (lt.irrefl 0))),
using s ⦄
section section
variable [s : linear_ordered_ring A] variable [s : linear_ordered_ring A]