feat(hott/algebra): define additive structures to be multiplicative structures
This commit is contained in:
Floris van Doorn
parent
8d6010ccad
commit
c884e7bbb9
11 changed files with 306 additions and 151 deletions
|
|
@ -59,20 +59,27 @@ abbreviation eq_of_mul_eq_mul_right' := @mul.right_cancel
|
|||
|
||||
/- additive semigroup -/
|
||||
|
||||
structure add_semigroup [class] (A : Type) extends has_add A :=
|
||||
(is_set_carrier : is_set A)
|
||||
(add_assoc : Πa b c, add (add a b) c = add a (add b c))
|
||||
definition add_semigroup [class] : Type → Type := semigroup
|
||||
|
||||
attribute add_semigroup.is_set_carrier [instance] [priority 900]
|
||||
definition add_semigroup.is_set_carrier [instance] [priority 900] (A : Type) [H : add_semigroup A] :
|
||||
is_set A :=
|
||||
@semigroup.is_set_carrier A H
|
||||
|
||||
definition has_add_of_add_semigroup [reducible] [trans_instance] (A : Type) [H : add_semigroup A] :
|
||||
has_add A :=
|
||||
has_add.mk (@mul A (@semigroup.to_has_mul A H))
|
||||
|
||||
definition add.assoc [s : add_semigroup A] (a b c : A) : a + b + c = a + (b + c) :=
|
||||
!add_semigroup.add_assoc
|
||||
@mul.assoc A s a b c
|
||||
|
||||
structure add_comm_semigroup [class] (A : Type) extends add_semigroup A :=
|
||||
(add_comm : Πa b, add a b = add b a)
|
||||
definition add_comm_semigroup [class] : Type → Type := comm_semigroup
|
||||
|
||||
definition add_semigroup_of_add_comm_semigroup [reducible] [trans_instance] (A : Type)
|
||||
[H : add_comm_semigroup A] : add_semigroup A :=
|
||||
@comm_semigroup.to_semigroup A H
|
||||
|
||||
definition add.comm [s : add_comm_semigroup A] (a b : A) : a + b = b + a :=
|
||||
!add_comm_semigroup.add_comm
|
||||
@mul.comm A s a b
|
||||
|
||||
theorem add.left_comm [s : add_comm_semigroup A] (a b c : A) :
|
||||
a + (b + c) = b + (a + c) :=
|
||||
|
|
@ -81,21 +88,27 @@ binary.left_comm (@add.comm A _) (@add.assoc A _) a b c
|
|||
theorem add.right_comm [s : add_comm_semigroup A] (a b c : A) : (a + b) + c = (a + c) + b :=
|
||||
binary.right_comm (@add.comm A _) (@add.assoc A _) a b c
|
||||
|
||||
structure add_left_cancel_semigroup [class] (A : Type) extends add_semigroup A :=
|
||||
(add_left_cancel : Πa b c, add a b = add a c → b = c)
|
||||
definition add_left_cancel_semigroup [class] : Type → Type := left_cancel_semigroup
|
||||
|
||||
definition add_semigroup_of_add_left_cancel_semigroup [reducible] [trans_instance] (A : Type)
|
||||
[H : add_left_cancel_semigroup A] : add_semigroup A :=
|
||||
@left_cancel_semigroup.to_semigroup A H
|
||||
|
||||
definition add.left_cancel [s : add_left_cancel_semigroup A] {a b c : A} :
|
||||
a + b = a + c → b = c :=
|
||||
!add_left_cancel_semigroup.add_left_cancel
|
||||
@mul.left_cancel A s a b c
|
||||
|
||||
abbreviation eq_of_add_eq_add_left := @add.left_cancel
|
||||
|
||||
structure add_right_cancel_semigroup [class] (A : Type) extends add_semigroup A :=
|
||||
(add_right_cancel : Πa b c, add a b = add c b → a = c)
|
||||
definition add_right_cancel_semigroup [class] : Type → Type := right_cancel_semigroup
|
||||
|
||||
definition add_semigroup_of_add_right_cancel_semigroup [reducible] [trans_instance] (A : Type)
|
||||
[H : add_right_cancel_semigroup A] : add_semigroup A :=
|
||||
@right_cancel_semigroup.to_semigroup A H
|
||||
|
||||
definition add.right_cancel [s : add_right_cancel_semigroup A] {a b c : A} :
|
||||
a + b = c + b → a = c :=
|
||||
!add_right_cancel_semigroup.add_right_cancel
|
||||
@mul.right_cancel A s a b c
|
||||
|
||||
abbreviation eq_of_add_eq_add_right := @add.right_cancel
|
||||
|
||||
|
|
@ -112,46 +125,34 @@ structure comm_monoid [class] (A : Type) extends monoid A, comm_semigroup A
|
|||
|
||||
/- additive monoid -/
|
||||
|
||||
structure add_monoid [class] (A : Type) extends add_semigroup A, has_zero A :=
|
||||
(zero_add : Πa, add zero a = a) (add_zero : Πa, add a zero = a)
|
||||
definition add_monoid [class] : Type → Type := monoid
|
||||
|
||||
definition zero_add [s : add_monoid A] (a : A) : 0 + a = a := !add_monoid.zero_add
|
||||
definition add_semigroup_of_add_monoid [reducible] [trans_instance] (A : Type)
|
||||
[H : add_monoid A] : add_semigroup A :=
|
||||
@monoid.to_semigroup A H
|
||||
|
||||
definition add_zero [s : add_monoid A] (a : A) : a + 0 = a := !add_monoid.add_zero
|
||||
definition has_zero_of_add_monoid [reducible] [trans_instance] (A : Type)
|
||||
[H : add_monoid A] : has_zero A :=
|
||||
has_zero.mk (@one A (@monoid.to_has_one A H))
|
||||
|
||||
structure add_comm_monoid [class] (A : Type) extends add_monoid A, add_comm_semigroup A
|
||||
definition zero_add [s : add_monoid A] (a : A) : 0 + a = a := @monoid.one_mul A s a
|
||||
|
||||
definition add_monoid.to_monoid {A : Type} [s : add_monoid A] : monoid A :=
|
||||
⦃ monoid,
|
||||
mul := add_monoid.add,
|
||||
mul_assoc := add_monoid.add_assoc,
|
||||
one := add_monoid.zero A,
|
||||
mul_one := add_monoid.add_zero,
|
||||
one_mul := add_monoid.zero_add,
|
||||
is_set_carrier := _
|
||||
⦄
|
||||
definition add_zero [s : add_monoid A] (a : A) : a + 0 = a := @monoid.mul_one A s a
|
||||
|
||||
definition add_comm_monoid.to_comm_monoid {A : Type} [s : add_comm_monoid A] : comm_monoid A :=
|
||||
⦃ comm_monoid,
|
||||
add_monoid.to_monoid,
|
||||
mul_comm := add_comm_monoid.add_comm
|
||||
⦄
|
||||
definition add_comm_monoid [class] : Type → Type := comm_monoid
|
||||
|
||||
definition monoid.to_add_monoid {A : Type} [s : monoid A] : add_monoid A :=
|
||||
⦃ add_monoid,
|
||||
add := monoid.mul,
|
||||
add_assoc := monoid.mul_assoc,
|
||||
zero := monoid.one A,
|
||||
add_zero := monoid.mul_one,
|
||||
zero_add := monoid.one_mul,
|
||||
is_set_carrier := _
|
||||
⦄
|
||||
definition add_monoid_of_add_comm_monoid [reducible] [trans_instance] (A : Type)
|
||||
[H : add_comm_monoid A] : add_monoid A :=
|
||||
@comm_monoid.to_monoid A H
|
||||
|
||||
definition comm_monoid.to_add_comm_monoid {A : Type} [s : comm_monoid A] : add_comm_monoid A :=
|
||||
⦃ add_comm_monoid,
|
||||
monoid.to_add_monoid,
|
||||
add_comm := comm_monoid.mul_comm
|
||||
⦄
|
||||
definition add_comm_semigroup_of_add_comm_monoid [reducible] [trans_instance] (A : Type)
|
||||
[H : add_comm_monoid A] : add_comm_semigroup A :=
|
||||
@comm_monoid.to_comm_semigroup A H
|
||||
|
||||
definition add_monoid.to_monoid {A : Type} [s : add_monoid A] : monoid A := s
|
||||
definition add_comm_monoid.to_comm_monoid {A : Type} [s : add_comm_monoid A] : comm_monoid A := s
|
||||
definition monoid.to_add_monoid {A : Type} [s : monoid A] : add_monoid A := s
|
||||
definition comm_monoid.to_add_comm_monoid {A : Type} [s : comm_monoid A] : add_comm_monoid A := s
|
||||
|
||||
section add_comm_monoid
|
||||
variables [s : add_comm_monoid A]
|
||||
|
|
@ -346,23 +347,25 @@ structure comm_group [class] (A : Type) extends group A, comm_monoid A
|
|||
|
||||
/- additive group -/
|
||||
|
||||
structure add_group [class] (A : Type) extends add_monoid A, has_neg A :=
|
||||
(add_left_inv : Πa, add (neg a) a = zero)
|
||||
definition add_group [class] : Type → Type := group
|
||||
|
||||
definition add_group.to_group {A : Type} [s : add_group A] : group A :=
|
||||
⦃ group, add_monoid.to_monoid,
|
||||
mul_left_inv := add_group.add_left_inv ⦄
|
||||
definition add_semigroup_of_add_group [reducible] [trans_instance] (A : Type)
|
||||
[H : add_group A] : add_monoid A :=
|
||||
@group.to_monoid A H
|
||||
|
||||
definition group.to_add_group {A : Type} [s : group A] : add_group A :=
|
||||
⦃ add_group, monoid.to_add_monoid,
|
||||
add_left_inv := group.mul_left_inv ⦄
|
||||
definition has_zero_of_add_group [reducible] [trans_instance] (A : Type)
|
||||
[H : add_group A] : has_neg A :=
|
||||
has_neg.mk (@inv A (@group.to_has_inv A H))
|
||||
|
||||
definition add_group.to_group {A : Type} [s : add_group A] : group A := s
|
||||
definition group.to_add_group {A : Type} [s : group A] : add_group A := s
|
||||
|
||||
section add_group
|
||||
|
||||
variables [s : add_group A]
|
||||
include s
|
||||
|
||||
theorem add.left_inv (a : A) : -a + a = 0 := !add_group.add_left_inv
|
||||
theorem add.left_inv (a : A) : -a + a = 0 := @group.mul_left_inv A s a
|
||||
|
||||
theorem neg_add_cancel_left (a b : A) : -a + (a + b) = b :=
|
||||
by rewrite [-add.assoc, add.left_inv, zero_add]
|
||||
|
|
@ -461,13 +464,13 @@ section add_group
|
|||
... = (c + b) + -b : H
|
||||
... = c : add_neg_cancel_right
|
||||
|
||||
definition add_group.to_left_cancel_semigroup [trans_instance] : add_left_cancel_semigroup A :=
|
||||
⦃ add_left_cancel_semigroup, s,
|
||||
add_left_cancel := @add_left_cancel A s ⦄
|
||||
definition add_group.to_add_left_cancel_semigroup [reducible] [trans_instance] :
|
||||
add_left_cancel_semigroup A :=
|
||||
@group.to_left_cancel_semigroup A s
|
||||
|
||||
definition add_group.to_add_right_cancel_semigroup [trans_instance] : add_right_cancel_semigroup A :=
|
||||
⦃ add_right_cancel_semigroup, s,
|
||||
add_right_cancel := @add_right_cancel A s ⦄
|
||||
definition add_group.to_add_right_cancel_semigroup [reducible] [trans_instance] :
|
||||
add_right_cancel_semigroup A :=
|
||||
@group.to_right_cancel_semigroup A s
|
||||
|
||||
theorem add_neg_eq_neg_add_rev {a b : A} : a + -b = -(b + -a) :=
|
||||
by rewrite [neg_add_rev, neg_neg]
|
||||
|
|
@ -545,15 +548,18 @@ section add_group
|
|||
|
||||
end add_group
|
||||
|
||||
structure add_comm_group [class] (A : Type) extends add_group A, add_comm_monoid A
|
||||
definition add_comm_group [class] : Type → Type := comm_group
|
||||
|
||||
definition add_comm_group.to_comm_group {A : Type} [s : add_comm_group A] : comm_group A :=
|
||||
⦃ comm_group, add_group.to_group,
|
||||
mul_comm := add_comm_group.add_comm ⦄
|
||||
definition add_group_of_add_comm_group [reducible] [trans_instance] (A : Type)
|
||||
[H : add_comm_group A] : add_group A :=
|
||||
@comm_group.to_group A H
|
||||
|
||||
definition comm_group.to_add_comm_group {A : Type} [s : comm_group A] : add_comm_group A :=
|
||||
⦃ add_comm_group, group.to_add_group,
|
||||
add_comm := comm_group.mul_comm ⦄
|
||||
definition add_comm_monoid_of_add_comm_group [reducible] [trans_instance] (A : Type)
|
||||
[H : add_comm_group A] : add_comm_monoid A :=
|
||||
@comm_group.to_comm_monoid A H
|
||||
|
||||
definition add_comm_group.to_comm_group {A : Type} [s : add_comm_group A] : comm_group A := s
|
||||
definition comm_group.to_add_comm_group {A : Type} [s : comm_group A] : add_comm_group A := s
|
||||
|
||||
section add_comm_group
|
||||
variable [s : add_comm_group A]
|
||||
|
|
|
|||
|
|
@ -344,9 +344,9 @@ section linear_ordered_field
|
|||
sigma.mk ((a - b) / (1 + 1))
|
||||
(pair (have H2 : a + a > (b + b) + (a - b), from calc
|
||||
a + a > b + a : add_lt_add_right H
|
||||
... = b + a + b - b : add_sub_cancel
|
||||
... = b + b + a - b : add.right_comm
|
||||
... = (b + b) + (a - b) : add_sub,
|
||||
... = b + a + b - b : by rewrite add_sub_cancel
|
||||
... = b + b + a - b : by rewrite add.right_comm
|
||||
... = (b + b) + (a - b) : by rewrite add_sub,
|
||||
have H3 : (a + a) / 2 > ((b + b) + (a - b)) / 2,
|
||||
from div_lt_div_of_lt_of_pos H2 two_pos,
|
||||
by rewrite [one_add_one_eq_two, sub_eq_add_neg, add_self_div_two at H3, -div_add_div_same at H3, add_self_div_two at H3];
|
||||
|
|
|
|||
|
|
@ -15,12 +15,30 @@ variable {A : Type}
|
|||
/- partially ordered monoids, such as the natural numbers -/
|
||||
|
||||
namespace algebra
|
||||
structure ordered_cancel_comm_monoid [class] (A : Type) extends add_comm_monoid A,
|
||||
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)
|
||||
structure ordered_mul_cancel_comm_monoid [class] (A : Type) extends comm_monoid A,
|
||||
left_cancel_semigroup A, right_cancel_semigroup A, order_pair A :=
|
||||
(mul_le_mul_left : Πa b, le a b → Πc, le (mul c a) (mul c b))
|
||||
(le_of_mul_le_mul_left : Πa b c, le (mul a b) (mul a c) → le b c)
|
||||
(mul_lt_mul_left : Πa b, lt a b → Πc, lt (mul c a) (mul c b))
|
||||
(lt_of_mul_lt_mul_left : Πa b c, lt (mul a b) (mul a c) → lt b c)
|
||||
|
||||
definition ordered_cancel_comm_monoid [class] : Type → Type := ordered_mul_cancel_comm_monoid
|
||||
|
||||
definition add_comm_monoid_of_ordered_cancel_comm_monoid [reducible] [trans_instance]
|
||||
(A : Type) [H : ordered_cancel_comm_monoid A] : add_comm_monoid A :=
|
||||
@ordered_mul_cancel_comm_monoid.to_comm_monoid A H
|
||||
|
||||
definition add_left_cancel_semigroup_of_ordered_cancel_comm_monoid [reducible] [trans_instance]
|
||||
(A : Type) [H : ordered_cancel_comm_monoid A] : add_left_cancel_semigroup A :=
|
||||
@ordered_mul_cancel_comm_monoid.to_left_cancel_semigroup A H
|
||||
|
||||
definition add_right_cancel_semigroup_of_ordered_cancel_comm_monoid [reducible] [trans_instance]
|
||||
(A : Type) [H : ordered_cancel_comm_monoid A] : add_right_cancel_semigroup A :=
|
||||
@ordered_mul_cancel_comm_monoid.to_right_cancel_semigroup A H
|
||||
|
||||
definition order_pair_of_ordered_cancel_comm_monoid [reducible] [trans_instance]
|
||||
(A : Type) [H : ordered_cancel_comm_monoid A] : order_pair A :=
|
||||
@ordered_mul_cancel_comm_monoid.to_order_pair A H
|
||||
|
||||
section
|
||||
variables [s : ordered_cancel_comm_monoid A]
|
||||
|
|
@ -28,7 +46,7 @@ section
|
|||
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
|
||||
@ordered_mul_cancel_comm_monoid.mul_lt_mul_left A s a b H c
|
||||
|
||||
theorem add_lt_add_right (H : a < b) (c : A) : a + c < b + c :=
|
||||
begin
|
||||
|
|
@ -37,7 +55,7 @@ section
|
|||
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
|
||||
@ordered_mul_cancel_comm_monoid.mul_le_mul_left A s a b H c
|
||||
|
||||
theorem add_le_add_right (H : a ≤ b) (c : A) : a + c ≤ b + c :=
|
||||
(add.comm c a) ▸ (add.comm c b) ▸ (add_le_add_left H c)
|
||||
|
|
@ -74,13 +92,13 @@ section
|
|||
|
||||
-- here we start using le_of_add_le_add_left.
|
||||
theorem le_of_add_le_add_left (H : a + b ≤ a + c) : b ≤ c :=
|
||||
!ordered_cancel_comm_monoid.le_of_add_le_add_left H
|
||||
@ordered_mul_cancel_comm_monoid.le_of_mul_le_mul_left A s a b c H
|
||||
|
||||
theorem le_of_add_le_add_right (H : a + b ≤ c + b) : a ≤ c :=
|
||||
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 :=
|
||||
!ordered_cancel_comm_monoid.lt_of_add_lt_add_left H
|
||||
@ordered_mul_cancel_comm_monoid.lt_of_mul_lt_mul_left A s a b c H
|
||||
|
||||
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)
|
||||
|
|
@ -195,27 +213,37 @@ end
|
|||
|
||||
/- partially ordered groups -/
|
||||
|
||||
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))
|
||||
structure ordered_mul_comm_group [class] (A : Type) extends comm_group A, order_pair A :=
|
||||
(mul_le_mul_left : Πa b, le a b → Πc, le (mul c a) (mul c b))
|
||||
(mul_lt_mul_left : Πa b, lt a b → Π c, lt (mul c a) (mul c b))
|
||||
|
||||
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 :=
|
||||
have 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'
|
||||
definition ordered_comm_group [class] : Type → Type := ordered_mul_comm_group
|
||||
|
||||
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 :=
|
||||
have 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 add_comm_group_of_ordered_comm_group [reducible] [trans_instance] (A : Type)
|
||||
[H : ordered_comm_group A] : add_comm_group A :=
|
||||
@ordered_mul_comm_group.to_comm_group A H
|
||||
|
||||
definition ordered_comm_group.to_ordered_cancel_comm_monoid [trans_instance]
|
||||
theorem ordered_mul_comm_group.le_of_mul_le_mul_left [s : ordered_mul_comm_group A] {a b c : A}
|
||||
(H : a * b ≤ a * c) : b ≤ c :=
|
||||
have H' : a⁻¹ * (a * b) ≤ a⁻¹ * (a * c), from ordered_mul_comm_group.mul_le_mul_left _ _ H _,
|
||||
by rewrite *inv_mul_cancel_left at H'; exact H'
|
||||
|
||||
theorem ordered_mul_comm_group.lt_of_mul_lt_mul_left [s : ordered_mul_comm_group A] {a b c : A}
|
||||
(H : a * b < a * c) : b < c :=
|
||||
have H' : a⁻¹ * (a * b) < a⁻¹ * (a * c), from ordered_mul_comm_group.mul_lt_mul_left _ _ H _,
|
||||
by rewrite *inv_mul_cancel_left at H'; exact H'
|
||||
|
||||
definition ordered_mul_comm_group.to_ordered_mul_cancel_comm_monoid [reducible] [trans_instance]
|
||||
[s : ordered_mul_comm_group A] : ordered_mul_cancel_comm_monoid A :=
|
||||
⦃ ordered_mul_cancel_comm_monoid, s,
|
||||
mul_left_cancel := @mul.left_cancel A _,
|
||||
mul_right_cancel := @mul.right_cancel A _,
|
||||
le_of_mul_le_mul_left := @ordered_mul_comm_group.le_of_mul_le_mul_left A _,
|
||||
lt_of_mul_lt_mul_left := @ordered_mul_comm_group.lt_of_mul_lt_mul_left A _⦄
|
||||
|
||||
definition ordered_comm_group.to_ordered_cancel_comm_monoid [reducible] [trans_instance]
|
||||
[s : ordered_comm_group A] : ordered_cancel_comm_monoid A :=
|
||||
⦃ ordered_cancel_comm_monoid, s,
|
||||
add_left_cancel := @add.left_cancel A _,
|
||||
add_right_cancel := @add.right_cancel A _,
|
||||
le_of_add_le_add_left := @ordered_comm_group.le_of_add_le_add_left A _,
|
||||
lt_of_add_lt_add_left := @ordered_comm_group.lt_of_add_lt_add_left A _⦄
|
||||
@ordered_mul_comm_group.to_ordered_mul_cancel_comm_monoid A s
|
||||
|
||||
section
|
||||
variables [s : ordered_comm_group A] (a b c d e : A)
|
||||
|
|
@ -575,19 +603,35 @@ end
|
|||
|
||||
/- linear ordered group with decidable order -/
|
||||
|
||||
structure decidable_linear_ordered_comm_group [class] (A : Type)
|
||||
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))
|
||||
structure decidable_linear_ordered_mul_comm_group [class] (A : Type)
|
||||
extends comm_group A, decidable_linear_order A :=
|
||||
(mul_le_mul_left : Π a b, le a b → Π c, le (mul c a) (mul c b))
|
||||
(mul_lt_mul_left : Π a b, lt a b → Π c, lt (mul c a) (mul c b))
|
||||
|
||||
definition decidable_linear_ordered_comm_group.to_ordered_comm_group
|
||||
[trans_instance]
|
||||
(A : Type) [s : decidable_linear_ordered_comm_group A] : ordered_comm_group A :=
|
||||
⦃ ordered_comm_group, s,
|
||||
definition decidable_linear_ordered_comm_group [class] : Type → Type :=
|
||||
decidable_linear_ordered_mul_comm_group
|
||||
|
||||
definition add_comm_group_of_decidable_linear_ordered_comm_group [reducible] [trans_instance] (A : Type)
|
||||
[H : decidable_linear_ordered_comm_group A] : add_comm_group A :=
|
||||
@decidable_linear_ordered_mul_comm_group.to_comm_group A H
|
||||
|
||||
definition decidable_linear_order_of_decidable_linear_ordered_comm_group [reducible]
|
||||
[trans_instance] (A : Type) [H : decidable_linear_ordered_comm_group A] :
|
||||
decidable_linear_order A :=
|
||||
@decidable_linear_ordered_mul_comm_group.to_decidable_linear_order A H
|
||||
|
||||
definition decidable_linear_ordered_mul_comm_group.to_ordered_mul_comm_group [reducible]
|
||||
[trans_instance] (A : Type) [s : decidable_linear_ordered_mul_comm_group A] :
|
||||
ordered_mul_comm_group A :=
|
||||
⦃ ordered_mul_comm_group, s,
|
||||
le_of_lt := @le_of_lt A _,
|
||||
lt_of_le_of_lt := @lt_of_le_of_lt A _,
|
||||
lt_of_lt_of_le := @lt_of_lt_of_le A _ ⦄
|
||||
|
||||
definition decidable_linear_ordered_comm_group.to_ordered_comm_group [reducible] [trans_instance]
|
||||
(A : Type) [s : decidable_linear_ordered_comm_group A] : ordered_comm_group A :=
|
||||
@decidable_linear_ordered_mul_comm_group.to_ordered_mul_comm_group A s
|
||||
|
||||
section
|
||||
variables [s : decidable_linear_ordered_comm_group A]
|
||||
variables {a b c d e : A}
|
||||
|
|
@ -821,4 +865,5 @@ section
|
|||
|
||||
end
|
||||
end
|
||||
|
||||
end algebra
|
||||
|
|
|
|||
|
|
@ -19,13 +19,29 @@ absurd H (lt.irrefl a)
|
|||
|
||||
/- semiring structures -/
|
||||
|
||||
structure ordered_semiring [class] (A : Type)
|
||||
extends semiring A, ordered_cancel_comm_monoid A :=
|
||||
structure ordered_semiring (A : Type)
|
||||
extends semiring A, ordered_mul_cancel_comm_monoid A renaming
|
||||
mul→add mul_assoc→add_assoc one→zero one_mul→zero_add mul_one→add_zero mul_comm→add_comm
|
||||
mul_left_cancel→add_left_cancel mul_right_cancel→add_right_cancel mul_le_mul_left→add_le_add_left
|
||||
mul_lt_mul_left→add_lt_add_left le_of_mul_le_mul_left→le_of_add_le_add_left
|
||||
lt_of_mul_lt_mul_left→lt_of_add_lt_add_left :=
|
||||
(mul_le_mul_of_nonneg_left: Πa b c, le a b → le zero c → le (mul c a) (mul c b))
|
||||
(mul_le_mul_of_nonneg_right: Πa b c, le a b → le zero c → le (mul a c) (mul b c))
|
||||
(mul_lt_mul_of_pos_left: Πa b c, lt a b → lt zero c → lt (mul c a) (mul c b))
|
||||
(mul_lt_mul_of_pos_right: Πa b c, lt a b → lt zero c → lt (mul a c) (mul b c))
|
||||
|
||||
-- /- we make it a class now (and not as part of the structure) to avoid
|
||||
-- ordered_semiring.to_ordered_mul_cancel_comm_monoid to be an instance -/
|
||||
attribute ordered_semiring [class]
|
||||
|
||||
definition add_comm_group_of_ordered_semiring [trans_instance] [reducible] (A : Type)
|
||||
[H : ordered_semiring A] : semiring A :=
|
||||
@ordered_semiring.to_semiring A H
|
||||
|
||||
definition monoid_of_ordered_semiring [trans_instance] [reducible] (A : Type)
|
||||
[H : ordered_semiring A] : ordered_cancel_comm_monoid A :=
|
||||
@ordered_semiring.to_ordered_mul_cancel_comm_monoid A H
|
||||
|
||||
section
|
||||
variable [s : ordered_semiring A]
|
||||
variables (a b c d e : A)
|
||||
|
|
@ -193,15 +209,34 @@ structure decidable_linear_ordered_semiring [class] (A : Type)
|
|||
|
||||
/- ring structures -/
|
||||
|
||||
structure ordered_ring [class] (A : Type)
|
||||
extends ring A, ordered_comm_group A, zero_ne_one_class A :=
|
||||
structure ordered_ring (A : Type) extends ring A, ordered_mul_comm_group A renaming
|
||||
mul→add mul_assoc→add_assoc one→zero one_mul→zero_add mul_one→add_zero inv→neg
|
||||
mul_left_inv→add_left_inv mul_comm→add_comm mul_le_mul_left→add_le_add_left
|
||||
mul_lt_mul_left→add_lt_add_left,
|
||||
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))
|
||||
|
||||
-- /- we make it a class now (and not as part of the structure) to avoid
|
||||
-- ordered_ring.to_ordered_mul_comm_group to be an instance -/
|
||||
attribute ordered_ring [class]
|
||||
|
||||
definition add_comm_group_of_ordered_ring [reducible] [trans_instance] (A : Type)
|
||||
[H : ordered_ring A] : ring A :=
|
||||
@ordered_ring.to_ring A H
|
||||
|
||||
definition monoid_of_ordered_ring [reducible] [trans_instance] (A : Type)
|
||||
[H : ordered_ring A] : ordered_comm_group A :=
|
||||
@ordered_ring.to_ordered_mul_comm_group A H
|
||||
|
||||
definition zero_ne_one_class_of_ordered_ring [reducible] [trans_instance] (A : Type)
|
||||
[H : ordered_ring A] : zero_ne_one_class A :=
|
||||
@ordered_ring.to_zero_ne_one_class A H
|
||||
|
||||
theorem ordered_ring.mul_le_mul_of_nonneg_left [s : ordered_ring A] {a b c : A}
|
||||
(Hab : a ≤ b) (Hc : 0 ≤ c) : c * a ≤ c * b :=
|
||||
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,
|
||||
begin
|
||||
rewrite mul_sub_left_distrib at H2,
|
||||
exact (iff.mp !sub_nonneg_iff_le H2)
|
||||
|
|
@ -210,7 +245,7 @@ end
|
|||
theorem ordered_ring.mul_le_mul_of_nonneg_right [s : ordered_ring A] {a b c : A}
|
||||
(Hab : a ≤ b) (Hc : 0 ≤ c) : a * c ≤ b * c :=
|
||||
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,
|
||||
begin
|
||||
rewrite mul_sub_right_distrib at H2,
|
||||
exact (iff.mp !sub_nonneg_iff_le H2)
|
||||
|
|
@ -219,7 +254,7 @@ end
|
|||
theorem ordered_ring.mul_lt_mul_of_pos_left [s : ordered_ring A] {a b c : A}
|
||||
(Hab : a < b) (Hc : 0 < c) : c * a < c * b :=
|
||||
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,
|
||||
begin
|
||||
rewrite mul_sub_left_distrib at H2,
|
||||
exact (iff.mp !sub_pos_iff_lt H2)
|
||||
|
|
@ -228,13 +263,14 @@ end
|
|||
theorem ordered_ring.mul_lt_mul_of_pos_right [s : ordered_ring A] {a b c : A}
|
||||
(Hab : a < b) (Hc : 0 < c) : a * c < b * c :=
|
||||
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,
|
||||
begin
|
||||
rewrite mul_sub_right_distrib at H2,
|
||||
exact (iff.mp !sub_pos_iff_lt H2)
|
||||
end
|
||||
|
||||
definition ordered_ring.to_ordered_semiring [trans_instance] [s : ordered_ring A] : ordered_semiring A :=
|
||||
definition ordered_ring.to_ordered_semiring [reducible] [trans_instance] [s : ordered_ring A] :
|
||||
ordered_semiring A :=
|
||||
⦃ ordered_semiring, s,
|
||||
mul_zero := mul_zero,
|
||||
zero_mul := zero_mul,
|
||||
|
|
@ -314,7 +350,8 @@ structure linear_ordered_ring [class] (A : Type)
|
|||
extends ordered_ring A, linear_strong_order_pair A :=
|
||||
(zero_lt_one : lt zero one)
|
||||
|
||||
definition linear_ordered_ring.to_linear_ordered_semiring [trans_instance] [s : linear_ordered_ring A] : linear_ordered_semiring A :=
|
||||
definition linear_ordered_ring.to_linear_ordered_semiring [reducible] [trans_instance]
|
||||
[s : linear_ordered_ring A] : linear_ordered_semiring A :=
|
||||
⦃ linear_ordered_semiring, s,
|
||||
mul_zero := mul_zero,
|
||||
zero_mul := zero_mul,
|
||||
|
|
@ -366,7 +403,7 @@ lt.by_cases
|
|||
end))
|
||||
|
||||
-- Linearity implies no zero divisors. Doesn't need commutativity.
|
||||
definition linear_ordered_comm_ring.to_integral_domain [trans_instance]
|
||||
definition linear_ordered_comm_ring.to_integral_domain [reducible] [trans_instance]
|
||||
[s: linear_ordered_comm_ring A] : integral_domain A :=
|
||||
⦃ integral_domain, s,
|
||||
eq_zero_sum_eq_zero_of_mul_eq_zero :=
|
||||
|
|
@ -449,7 +486,24 @@ end
|
|||
Search on mult_le_cancel_right1 in Rings.thy. -/
|
||||
|
||||
structure decidable_linear_ordered_comm_ring [class] (A : Type) extends linear_ordered_comm_ring A,
|
||||
decidable_linear_ordered_comm_group A
|
||||
decidable_linear_ordered_mul_comm_group A renaming
|
||||
mul→add mul_assoc→add_assoc one→zero one_mul→zero_add mul_one→add_zero inv→neg
|
||||
mul_left_inv→add_left_inv mul_comm→add_comm mul_le_mul_left→add_le_add_left
|
||||
mul_lt_mul_left→add_lt_add_left
|
||||
|
||||
-- /- we make it a class now (and not as part of the structure) to avoid
|
||||
-- ordered_semiring.to_ordered_mul_cancel_comm_monoid to be an instance -/
|
||||
attribute decidable_linear_ordered_comm_ring [class]
|
||||
|
||||
definition linear_ordered_comm_ring_of_decidable_linear_ordered_comm_ring [reducible]
|
||||
[trans_instance] (A : Type) [H : decidable_linear_ordered_comm_ring A] :
|
||||
linear_ordered_comm_ring A :=
|
||||
@decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring A H
|
||||
|
||||
definition decidable_linear_ordered_comm_group_of_decidable_linear_ordered_comm_ring [reducible]
|
||||
[trans_instance] (A : Type) [H : decidable_linear_ordered_comm_ring A] :
|
||||
decidable_linear_ordered_comm_group A :=
|
||||
@decidable_linear_ordered_comm_ring.to_decidable_linear_ordered_mul_comm_group A H
|
||||
|
||||
section
|
||||
variable [s : decidable_linear_ordered_comm_ring A]
|
||||
|
|
|
|||
|
|
@ -38,15 +38,38 @@ structure zero_ne_one_class [class] (A : Type) extends has_zero A, has_one A :=
|
|||
theorem zero_ne_one [s: zero_ne_one_class A] : 0 ≠ (1:A) := @zero_ne_one_class.zero_ne_one A s
|
||||
|
||||
/- semiring -/
|
||||
structure semiring (A : Type) extends comm_monoid A renaming
|
||||
mul→add mul_assoc→add_assoc one→zero one_mul→zero_add mul_one→add_zero mul_comm→add_comm,
|
||||
monoid A, distrib A, mul_zero_class A
|
||||
|
||||
structure semiring [class] (A : Type) extends add_comm_monoid A, monoid A, distrib A,
|
||||
mul_zero_class A
|
||||
/- we make it a class now (and not as part of the structure) to avoid
|
||||
semiring.to_comm_monoid to be an instance -/
|
||||
attribute semiring [class]
|
||||
|
||||
definition add_comm_monoid_of_semiring [reducible] [trans_instance] (A : Type)
|
||||
[H : semiring A] : add_comm_monoid A :=
|
||||
@semiring.to_comm_monoid A H
|
||||
|
||||
definition monoid_of_semiring [reducible] [trans_instance] (A : Type)
|
||||
[H : semiring A] : monoid A :=
|
||||
@semiring.to_monoid A H
|
||||
|
||||
definition distrib_of_semiring [reducible] [trans_instance] (A : Type)
|
||||
[H : semiring A] : distrib A :=
|
||||
@semiring.to_distrib A H
|
||||
|
||||
definition mul_zero_class_of_semiring [reducible] [trans_instance] (A : Type)
|
||||
[H : semiring A] : mul_zero_class A :=
|
||||
@semiring.to_mul_zero_class A H
|
||||
|
||||
section semiring
|
||||
variables [s : semiring A] (a b c : A)
|
||||
include s
|
||||
|
||||
theorem one_add_one_eq_two : 1 + 1 = (2:A) :=
|
||||
theorem As {a b c : A} : a + b + c = a + (b + c) :=
|
||||
!add.assoc
|
||||
|
||||
theorem one_add_one_eq_two : 1 + 1 = 2 :> A :=
|
||||
by unfold bit0
|
||||
|
||||
theorem ne_zero_of_mul_ne_zero_right {a b : A} (H : a * b ≠ 0) : a ≠ 0 :=
|
||||
|
|
@ -163,7 +186,25 @@ end comm_semiring
|
|||
|
||||
/- ring -/
|
||||
|
||||
structure ring [class] (A : Type) extends add_comm_group A, monoid A, distrib A
|
||||
structure ring (A : Type) extends comm_group A renaming mul→add mul_assoc→add_assoc
|
||||
one→zero one_mul→zero_add mul_one→add_zero inv→neg mul_left_inv→add_left_inv mul_comm→add_comm,
|
||||
monoid A, distrib A
|
||||
|
||||
/- we make it a class now (and not as part of the structure) to avoid
|
||||
ring.to_comm_group to be an instance -/
|
||||
attribute ring [class]
|
||||
|
||||
definition add_comm_group_of_ring [reducible] [trans_instance] (A : Type)
|
||||
[H : ring A] : add_comm_group A :=
|
||||
@ring.to_comm_group A H
|
||||
|
||||
definition monoid_of_ring [reducible] [trans_instance] (A : Type)
|
||||
[H : ring A] : monoid A :=
|
||||
@ring.to_monoid A H
|
||||
|
||||
definition distrib_of_ring [reducible] [trans_instance] (A : Type)
|
||||
[H : ring A] : distrib A :=
|
||||
@ring.to_distrib A H
|
||||
|
||||
theorem ring.mul_zero [s : ring A] (a : A) : a * 0 = 0 :=
|
||||
have a * 0 + 0 = a * 0 + a * 0, from calc
|
||||
|
|
@ -179,7 +220,7 @@ have 0 * a + 0 = 0 * a + 0 * a, from calc
|
|||
... = 0 * a + 0 * a : by rewrite {_*a}ring.right_distrib,
|
||||
show 0 * a = 0, from (add.left_cancel this)⁻¹
|
||||
|
||||
definition ring.to_semiring [trans_instance] [s : ring A] : semiring A :=
|
||||
definition ring.to_semiring [reducible] [trans_instance] [s : ring A] : semiring A :=
|
||||
⦃ semiring, s,
|
||||
mul_zero := ring.mul_zero,
|
||||
zero_mul := ring.zero_mul ⦄
|
||||
|
|
@ -249,7 +290,7 @@ section
|
|||
have a + a * -1 = 0, from calc
|
||||
a + a * -1 = a * 1 + a * -1 : mul_one
|
||||
... = a * (1 + -1) : left_distrib
|
||||
... = a * 0 : add.right_inv
|
||||
... = a * 0 : by rewrite add.right_inv
|
||||
... = 0 : mul_zero,
|
||||
symm (neg_eq_of_add_eq_zero this)
|
||||
|
||||
|
|
@ -267,7 +308,8 @@ end
|
|||
|
||||
structure comm_ring [class] (A : Type) extends ring A, comm_semigroup A
|
||||
|
||||
definition comm_ring.to_comm_semiring [trans_instance] [s : comm_ring A] : comm_semiring A :=
|
||||
definition comm_ring.to_comm_semiring [reducible] [trans_instance] [s : comm_ring A] :
|
||||
comm_semiring A :=
|
||||
⦃ comm_semiring, s,
|
||||
mul_zero := mul_zero,
|
||||
zero_mul := zero_mul ⦄
|
||||
|
|
|
|||
|
|
@ -27,7 +27,9 @@ namespace freudenthal section
|
|||
definition code_merid : A → ptrunc (n + n) A → ptrunc (n + n) A :=
|
||||
begin
|
||||
have is_conn n (ptrunc (n + n) A), from !is_conn_trunc,
|
||||
refine wedge_extension.ext n n (λ x y, ttrunc (n + n) A) _ _ _,
|
||||
refine @wedge_extension.ext _ _ n n _ _ (λ x y, ttrunc (n + n) A) _ _ _ _,
|
||||
{ intros, apply is_trunc_trunc}, -- this subgoal might become unnecessary if
|
||||
-- type class inference catches it
|
||||
{ exact tr},
|
||||
{ exact id},
|
||||
{ reflexivity}
|
||||
|
|
@ -127,8 +129,10 @@ namespace freudenthal section
|
|||
begin
|
||||
apply arrow_pathover_left, intro c, esimp at *,
|
||||
induction c with a',
|
||||
rewrite [↑code, elim_type_merid, ▸*],
|
||||
refine wedge_extension.ext n n _ _ _ _ a a',
|
||||
rewrite [↑code, elim_type_merid],
|
||||
refine @wedge_extension.ext _ _ n n _ _ (λ a a', tr (up a') =[merid a] decode_south
|
||||
(to_fun (code_merid_equiv a) (tr a'))) _ _ _ _ a a',
|
||||
{ intros, apply is_trunc_pathover, apply is_trunc_succ, apply is_trunc_trunc},
|
||||
{ exact decode_coh_f},
|
||||
{ exact decode_coh_g},
|
||||
{ clear a a', unfold [decode_coh_f, decode_coh_g], refine ap011 concato_eq _ _,
|
||||
|
|
|
|||
|
|
@ -64,12 +64,12 @@ namespace sphere
|
|||
(@pgroup_of_group _ (group_LES_of_homotopy_groups complex_phopf _ _) idp)
|
||||
_,
|
||||
{ rewrite [▸*, LES_of_homotopy_groups_2 _ (n +[ℕ] 2)],
|
||||
have H : 1 ≤[ℕ] n + 1, from !one_le_succ,
|
||||
apply trivial_ghomotopy_group_of_is_trunc _ _ _ H},
|
||||
have H2 : 1 ≤[ℕ] n + 1, from !one_le_succ,
|
||||
exact @trivial_ghomotopy_group_of_is_trunc _ _ _ H H2},
|
||||
{ refine tr_rev (λx, is_contr (ptrunctype._trans_of_to_pType x))
|
||||
(LES_of_homotopy_groups_2 complex_phopf _) _,
|
||||
have H : 1 ≤[ℕ] n + 2, from !one_le_succ,
|
||||
apply trivial_ghomotopy_group_of_is_trunc _ _ _ H},
|
||||
have H2 : 1 ≤[ℕ] n + 2, from !one_le_succ,
|
||||
apply trivial_ghomotopy_group_of_is_trunc _ _ _ H2},
|
||||
{ exact homomorphism.struct (homomorphism_LES_of_homotopy_groups_fun _ (n+2, 0))}}},
|
||||
{ exact homomorphism.struct (homomorphism_LES_of_homotopy_groups_fun _ (n+2, 0))}
|
||||
end
|
||||
|
|
|
|||
|
|
@ -300,7 +300,7 @@ lemma madd_left_inv : Π i : fin (succ n), madd (minv i) i = fin.zero n
|
|||
rewrite [val_madd, ↑minv, mod_add_mod, nat.sub_add_cancel (le_of_lt ilt), mod_self])
|
||||
|
||||
definition madd_is_comm_group [instance] : add_comm_group (fin (succ n)) :=
|
||||
add_comm_group.mk madd _ madd_assoc (fin.zero n) zero_madd madd_zero minv madd_left_inv madd_comm
|
||||
comm_group.mk madd _ madd_assoc (fin.zero n) zero_madd madd_zero minv madd_left_inv madd_comm
|
||||
|
||||
definition gfin (n : ℕ) [H : is_succ n] : AddCommGroup.{0} :=
|
||||
by induction H with n; exact AddCommGroup.mk (fin (succ n)) _
|
||||
|
|
|
|||
|
|
@ -452,11 +452,11 @@ theorem repr_mul : Π (a b : ℤ), repr (a * b) = pmul (repr a) (repr b)
|
|||
... = (m * 0 + 0 * succ n, m * succ n + 0 * 0) : by rewrite *zero_mul
|
||||
| -[1+ m] (of_nat n) := calc
|
||||
repr (-[1+ m] * (n:int)) = (0 + succ m * 0, succ m * n) : repr_neg_of_nat
|
||||
... = (0 + succ m * 0, 0 + succ m * n) : nat.zero_add
|
||||
... = (0 + succ m * 0, 0 + succ m * n) : by rewrite [zero_add (succ m * n)]
|
||||
... = (0 * n + succ m * 0, 0 + succ m * n) : by rewrite zero_mul
|
||||
| -[1+ m] -[1+ n] := calc
|
||||
(succ m * succ n, 0) = (succ m * succ n, 0 * succ n) : by rewrite zero_mul
|
||||
... = (0 + succ m * succ n, 0 * succ n) : nat.zero_add
|
||||
... = (0 + succ m * succ n, 0 * succ n) : by rewrite nat.zero_add
|
||||
|
||||
theorem equiv_mul_prep {xa ya xb yb xn yn xm ym : ℕ}
|
||||
(H1 : xa + yb = ya + xb) (H2 : xn + ym = yn + xm)
|
||||
|
|
@ -466,7 +466,7 @@ nat.add_right_cancel (calc
|
|||
= xa*xn+ya*yn + (yb*xn+xb*yn) + (xb*ym+yb*xm + (xb*xn+yb*yn)) : by rewrite add.comm4
|
||||
... = xa*xn+ya*yn + (yb*xn+xb*yn) + (xb*xn+yb*yn + (xb*ym+yb*xm)) : by rewrite {xb*ym+yb*xm +_}nat.add_comm
|
||||
... = xa*xn+yb*xn + (ya*yn+xb*yn) + (xb*xn+xb*ym + (yb*yn+yb*xm)) : by exact !congr_arg2 !add.comm4 !add.comm4
|
||||
... = ya*xn+xb*xn + (xa*yn+yb*yn) + (xb*yn+xb*xm + (yb*xn+yb*ym)) : by rewrite[-+left_distrib,-+right_distrib]; exact H1 ▸ H2 ▸ rfl
|
||||
... = ya*xn+xb*xn + (xa*yn+yb*yn) + (xb*yn+xb*xm + (yb*xn+yb*ym)) : by xrewrite[-+left_distrib,-+right_distrib, H1, H2]
|
||||
... = ya*xn+xa*yn + (xb*xn+yb*yn) + (xb*yn+yb*xn + (xb*xm+yb*ym)) : by exact !congr_arg2 !add.comm4 !add.comm4
|
||||
... = xa*yn+ya*xn + (xb*xn+yb*yn) + (xb*yn+yb*xn + (xb*xm+yb*ym)) : by rewrite {xa*yn + _}nat.add_comm
|
||||
... = xa*yn+ya*xn + (xb*xn+yb*yn) + (yb*xn+xb*yn + (xb*xm+yb*ym)) : by rewrite {xb*yn + _}nat.add_comm
|
||||
|
|
@ -496,9 +496,9 @@ private theorem pmul_assoc_prep {p1 p2 q1 q2 r1 r2 : ℕ} :
|
|||
(p1*(q1*r1+q2*r2)+p2*(q1*r2+q2*r1), p1*(q1*r2+q2*r1)+p2*(q1*r1+q2*r2)) :=
|
||||
begin
|
||||
rewrite [+left_distrib, +right_distrib, *mul.assoc],
|
||||
rewrite (add.comm4 (p1 * (q1 * r1)) (p2 * (q2 * r1)) (p1 * (q2 * r2)) (p2 * (q1 * r2))),
|
||||
xrewrite (add.comm4 (p1 * (q1 * r1)) (p2 * (q2 * r1)) (p1 * (q2 * r2)) (p2 * (q1 * r2))),
|
||||
rewrite (add.comm (p2 * (q2 * r1)) (p2 * (q1 * r2))),
|
||||
rewrite (add.comm4 (p1 * (q1 * r2)) (p2 * (q2 * r2)) (p1 * (q2 * r1)) (p2 * (q1 * r1))),
|
||||
xrewrite (add.comm4 (p1 * (q1 * r2)) (p2 * (q2 * r2)) (p1 * (q2 * r1)) (p2 * (q1 * r1))),
|
||||
rewrite (add.comm (p2 * (q2 * r2)) (p2 * (q1 * r1)))
|
||||
end
|
||||
|
||||
|
|
@ -591,7 +591,7 @@ begin
|
|||
end
|
||||
|
||||
theorem neg_succ_of_nat_eq' (m : ℕ) : -[1+ m] = -m - 1 :=
|
||||
by rewrite [neg_succ_of_nat_eq, neg_add]
|
||||
by xrewrite [neg_succ_of_nat_eq, neg_add]
|
||||
|
||||
definition succ (a : ℤ) := a + (succ zero)
|
||||
definition pred (a : ℤ) := a - (succ zero)
|
||||
|
|
|
|||
|
|
@ -54,7 +54,7 @@ nat.rec_on m
|
|||
(take k : ℕ,
|
||||
assume IH : n + k - k = n,
|
||||
calc
|
||||
n + succ k - succ k = succ (n + k) - succ k : add_succ
|
||||
n + succ k - succ k = succ (n + k) - succ k : by rewrite add_succ
|
||||
... = n + k - k : succ_sub_succ
|
||||
... = n : IH)
|
||||
|
||||
|
|
@ -77,7 +77,7 @@ nat.rec_on k
|
|||
theorem succ_sub_sub_succ (n m k : ℕ) : succ n - m - succ k = n - m - k :=
|
||||
calc
|
||||
succ n - m - succ k = succ n - (m + succ k) : nat.sub_sub
|
||||
... = succ n - succ (m + k) : add_succ
|
||||
... = succ n - succ (m + k) : by rewrite add_succ
|
||||
... = n - (m + k) : succ_sub_succ
|
||||
... = n - m - k : nat.sub_sub
|
||||
|
||||
|
|
@ -113,7 +113,7 @@ nat.rec_on n
|
|||
calc
|
||||
pred (succ k) * m = k * m : pred_succ
|
||||
... = k * m + m - m : nat.add_sub_cancel
|
||||
... = succ k * m - m : succ_mul)
|
||||
... = succ k * m - m : by rewrite succ_mul)
|
||||
|
||||
theorem mul_pred_right (n m : ℕ) : n * pred m = n * m - n :=
|
||||
calc
|
||||
|
|
@ -134,7 +134,7 @@ nat.rec_on m
|
|||
... = (n - l) * k - k : mul_pred_left
|
||||
... = n * k - l * k - k : IH
|
||||
... = n * k - (l * k + k) : nat.sub_sub
|
||||
... = n * k - (succ l * k) : succ_mul)
|
||||
... = n * k - (succ l * k) : by rewrite succ_mul)
|
||||
|
||||
protected theorem mul_sub_left_distrib (n m k : ℕ) : n * (m - k) = n * m - n * k :=
|
||||
calc
|
||||
|
|
@ -144,8 +144,11 @@ calc
|
|||
... = n * m - n * k : {!mul.comm}
|
||||
|
||||
protected theorem mul_self_sub_mul_self_eq (a b : nat) : a * a - b * b = (a + b) * (a - b) :=
|
||||
by rewrite [nat.mul_sub_left_distrib, *right_distrib, mul.comm b a, add.comm (a*a) (a*b),
|
||||
nat.add_sub_add_left]
|
||||
begin
|
||||
rewrite [nat.mul_sub_left_distrib, *right_distrib, mul.comm b a],
|
||||
xrewrite [add.comm (a*a) (a*b)],
|
||||
rewrite nat.add_sub_add_left
|
||||
end
|
||||
|
||||
theorem succ_mul_succ_eq (a : nat) : succ a * succ a = a*a + a + a + 1 :=
|
||||
calc succ a * succ a = (a+1)*(a+1) : by rewrite [add_one]
|
||||
|
|
@ -207,7 +210,7 @@ theorem exists_sub_eq_of_le {n m : ℕ} (H : n ≤ m) : Σk, m - k = n :=
|
|||
obtain (k : ℕ) (Hk : n + k = m), from le.elim H,
|
||||
sigma.mk k
|
||||
(calc
|
||||
m - k = n + k - k : by rewrite Hk
|
||||
m - k = n + k - k : by xrewrite Hk
|
||||
... = n : nat.add_sub_cancel)
|
||||
|
||||
protected theorem add_sub_assoc {m k : ℕ} (H : k ≤ m) (n : ℕ) : n + m - k = n + (m - k) :=
|
||||
|
|
@ -223,7 +226,7 @@ have l1 : k ≤ m → n + m - k = n + (m - k), from
|
|||
assume IH : k ≤ m → n + m - k = n + (m - k),
|
||||
take H : succ k ≤ succ m,
|
||||
calc
|
||||
n + succ m - succ k = succ (n + m) - succ k : add_succ
|
||||
n + succ m - succ k = succ (n + m) - succ k : by rewrite add_succ
|
||||
... = n + m - k : succ_sub_succ
|
||||
... = n + (m - k) : IH (le_of_succ_le_succ H)
|
||||
... = n + (succ m - succ k) : succ_sub_succ),
|
||||
|
|
@ -270,7 +273,7 @@ sum.elim !le.total
|
|||
n - k + l = l + (n - k) : add.comm
|
||||
... = l + n - k : nat.add_sub_assoc H2 l
|
||||
... = n + l - k : add.comm
|
||||
... = m - k : Hl,
|
||||
... = m - k : by xrewrite Hl,
|
||||
le.intro H3)
|
||||
|
||||
protected theorem sub_le_sub_left {n m : ℕ} (H : n ≤ m) (k : ℕ) : k - m ≤ k - n :=
|
||||
|
|
@ -285,7 +288,7 @@ sub.cases
|
|||
m' + l + n = n + (m' + l) : add.comm
|
||||
... = n + (l + m') : add.comm
|
||||
... = n + l + m' : add.assoc
|
||||
... = m + m' : Hl
|
||||
... = m + m' : by xrewrite Hl
|
||||
... = k : Hm
|
||||
... = k - n + n : nat.sub_add_cancel H3,
|
||||
le.intro (add.right_cancel H4))
|
||||
|
|
|
|||
|
|
@ -438,7 +438,8 @@ section add_group
|
|||
have a + b + -b = a, by inst_simp,
|
||||
by inst_simp
|
||||
|
||||
definition add_group.to_left_cancel_semigroup [trans_instance] : add_left_cancel_semigroup A :=
|
||||
definition add_group.to_add_left_cancel_semigroup [trans_instance] :
|
||||
add_left_cancel_semigroup A :=
|
||||
⦃ add_left_cancel_semigroup, s,
|
||||
add_left_cancel := @add_left_cancel A s ⦄
|
||||
|
||||
|
|
|
|||
Loading…
Reference in a new issue