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

refactor(library/data/int,library/algebra): make int an instnance of ordered ring, rename theorems

Browse source
This commit is contained in:
Jeremy Avigad 2014-12-26 16:25:05 -05:00
parent 25394dddb7
commit cecabbb401
9 changed files with 742 additions and 424 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
library/algebra/group.lean
View file

@ -255,7 +255,7 @@ section group
theorem mul_eq_iff_eq_mul_inv (a b c : A) : a * b = c ↔ a = c * b⁻¹ :=
iff.intro eq_mul_inv_of_mul_eq mul_eq_of_eq_mul_inv
definition group.to_left_cancel_semigroup [instance] : left_cancel_semigroup A :=
definition group.to_left_cancel_semigroup [instance] [coercion] : left_cancel_semigroup A :=
left_cancel_semigroup.mk (@group.mul A s) (@group.mul_assoc A s)
(take a b c,
assume H : a * b = a * c,
@ -264,7 +264,7 @@ section group
... = a⁻¹ * (a * c) : H
... = c : inv_mul_cancel_left)
definition group.to_right_cancel_semigroup [instance] : right_cancel_semigroup A :=
definition group.to_right_cancel_semigroup [instance] [coercion] : right_cancel_semigroup A :=
right_cancel_semigroup.mk (@group.mul A s) (@group.mul_assoc A s)
(take a b c,
assume H : a * b = c * b,
@ -383,7 +383,7 @@ section add_group
theorem add_eq_iff_eq_add_neg (a b c : A) : a + b = c ↔ a = c + -b :=
iff.intro eq_add_neg_of_add_eq add_eq_of_eq_add_neg
definition add_group.to_left_cancel_semigroup [instance] :
definition add_group.to_left_cancel_semigroup [instance] [coercion] :
add_left_cancel_semigroup A :=
add_left_cancel_semigroup.mk add_group.add add_group.add_assoc
(take a b c,
@ -393,7 +393,7 @@ section add_group
... = -a + (a + c) : H
... = c : neg_add_cancel_left)
definition add_group.to_add_right_cancel_semigroup [instance] :
definition add_group.to_add_right_cancel_semigroup [instance] [coercion] :
add_right_cancel_semigroup A :=
add_right_cancel_semigroup.mk add_group.add add_group.add_assoc
(take a b c,

102
library/algebra/order.lean
View file

@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Module: algebra.order
Author: Jeremy Avigad
Various types of orders. We develop weak orders (<=) and strict orders (<) separately. We also
Various types of orders. We develop weak orders "≤" and strict orders "<" separately. We also
consider structures with both, where the two are related by
x < y ↔ (x ≤ y ∧ x ≠ y) (order_pair)
@ -16,16 +16,12 @@ with both < and ≤ as needed.
-/
import logic.eq logic.connectives
import data.unit data.sigma data.prod
import algebra.function algebra.binary
open eq eq.ops
namespace algebra
variable {A : Type}
/- overloaded symbols -/
structure has_le [class] (A : Type) :=
@ -62,21 +58,24 @@ calc_trans le_of_le_of_eq
calc_trans lt_of_eq_of_lt
calc_trans lt_of_lt_of_eq
/- weak orders -/
structure weak_order [class] (A : Type) extends has_le A :=
(le_refl : ∀a, le a a)
(le_trans : ∀a b c, le a b → le b c → le a c)
(le_antisym : ∀a b, le a b → le b a → a = b)
(le_antisymm : ∀a b, le a b → le b a → a = b)
theorem le.refl [s : weak_order A] (a : A) : a ≤ a := !weak_order.le_refl
section
variable [s : weak_order A]
include s
theorem le.trans [s : weak_order A] {a b c : A} : a ≤ b → b ≤ c → a ≤ c := !weak_order.le_trans
theorem le.refl (a : A) : a ≤ a := !weak_order.le_refl
calc_trans le.trans
theorem le.trans {a b c : A} : a ≤ b → b ≤ c → a ≤ c := !weak_order.le_trans
calc_trans le.trans
theorem le.antisym [s : weak_order A] {a b : A} : a ≤ b → b ≤ a → a = b := !weak_order.le_antisym
theorem le.antisymm {a b : A} : a ≤ b → b ≤ a → a = b := !weak_order.le_antisymm
end
structure linear_weak_order [class] (A : Type) extends weak_order A :=
(le_total : ∀a b, le a b ∨ le b a)
@ -84,22 +83,28 @@ structure linear_weak_order [class] (A : Type) extends weak_order A :=
theorem le.total [s : linear_weak_order A] (a b : A) : a ≤ b ∨ b ≤ a :=
!linear_weak_order.le_total
/- strict orders -/
structure strict_order [class] (A : Type) extends has_lt A :=
(lt_irrefl : ∀a, ¬ lt a a)
(lt_trans : ∀a b c, lt a b → lt b c → lt a c)
theorem lt.irrefl [s : strict_order A] (a : A) : ¬ a < a := !strict_order.lt_irrefl
section
variable [s : strict_order A]
include s
theorem lt.trans [s : strict_order A] {a b c : A} : a < b → b < c → a < c := !strict_order.lt_trans
theorem lt.irrefl (a : A) : ¬ a < a := !strict_order.lt_irrefl
calc_trans lt.trans
theorem lt.trans {a b c : A} : a < b → b < c → a < c := !strict_order.lt_trans
calc_trans lt.trans
theorem lt.ne [s : strict_order A] {a b : A} : a < b → a ≠ b :=
assume lt_ab : a < b, assume eq_ab : a = b, lt.irrefl a (eq_ab⁻¹ ▸ lt_ab)
theorem ne_of_lt {a b : A} : a < b → a ≠ b :=
assume lt_ab : a < b, assume eq_ab : a = b,
show false, from lt.irrefl b (eq_ab ▸ lt_ab)
theorem lt.asymm {a b : A} (H : a < b) : ¬ b < a :=
assume H1 : b < a, lt.irrefl _ (lt.trans H H1)
end
/- well-founded orders -/
@ -123,7 +128,6 @@ structure order_pair [class] (A : Type) extends weak_order A, has_lt A :=
(lt_iff_le_ne : ∀a b, lt a b ↔ (le a b ∧ a ≠ b))
section
variable [s : order_pair A]
variables {a b c : A}
include s
@ -137,7 +141,7 @@ section
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)
definition order_pair.to_strict_order [instance] [s : order_pair A] : strict_order A :=
definition order_pair.to_strict_order [instance] [coercion] [s : order_pair A] : strict_order A :=
strict_order.mk
order_pair.lt
(show ∀a, ¬ a < a, from
@ -155,7 +159,7 @@ section
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.antisym le_ab le_ba,
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)
@ -167,8 +171,8 @@ section
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.antisym (le_of_lt lt_ab) le_ba,
show false, from lt.ne lt_ab eq_ab,
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 : a ≤ b → b < c → a < c :=
@ -178,8 +182,8 @@ section
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.antisym (le_of_lt lt_bc) le_cb,
show false, from lt.ne lt_bc eq_bc,
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
calc_trans lt_of_lt_of_le
@ -192,11 +196,6 @@ section
theorem not_lt_of_le (H : a ≤ b) : ¬ b < a :=
assume H1 : b < a,
lt.irrefl _ (lt_of_le_of_lt H H1)
theorem not_lt_of_lt (H : a < b) : ¬ b < a :=
assume H1 : b < a,
lt.irrefl _ (lt.trans H1 H)
end
structure strong_order_pair [class] (A : Type) extends order_pair A :=
@ -205,7 +204,7 @@ structure strong_order_pair [class] (A : Type) extends order_pair 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
theorem le_imp_lt_or_eq [s : strong_order_pair A] {a b : A} (le_ab : a ≤ b) : 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
-- We can also construct a strong order pair by defining a strict order, and then defining
@ -214,7 +213,7 @@ iff.mp le_iff_lt_or_eq le_ab
structure strict_order_with_le [class] (A : Type) extends strict_order A, has_le A :=
(le_iff_lt_or_eq : ∀a b, le a b ↔ lt a b ∨ a = b)
definition strict_order_with_le.to_order_pair [instance] [s : strict_order_with_le A] :
definition strict_order_with_le.to_order_pair [instance] [coercion] [s : strict_order_with_le A] :
strong_order_pair A :=
strong_order_pair.mk strict_order_with_le.le
(take a,
@ -248,57 +247,60 @@ strong_order_pair.mk strict_order_with_le.le
(assume lt_ab : a < b,
have le_ab : a ≤ b,
from iff.elim_right !strict_order_with_le.le_iff_lt_or_eq (or.intro_left _ lt_ab),
show a ≤ b ∧ a ≠ b, from and.intro le_ab (lt.ne lt_ab))
show a ≤ b ∧ a ≠ b, from and.intro le_ab (ne_of_lt lt_ab))
(assume H : a ≤ b ∧ a ≠ b,
have H1 : a < b ∨ a = b,
from 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)))
strict_order_with_le.le_iff_lt_or_eq
/- linear orders -/
structure linear_order_pair [class] (A : Type) extends order_pair A, linear_weak_order A
structure linear_strong_order_pair [class] (A : Type) extends strong_order_pair A :=
(lt_or_eq_or_lt : ∀a b, lt a b ∨ a = b ∨ lt b a)
structure linear_strong_order_pair [class] (A : Type) extends strong_order_pair A,
linear_weak_order A
section
variable [s : linear_strong_order_pair A]
variables (a b c : A)
include s
theorem lt_or_eq_or_lt : a < b ∨ a = b ∨ b < a := !linear_strong_order_pair.lt_or_eq_or_lt
theorem lt.trichotomy : a < b ∨ a = b ∨ b < a :=
or.elim (le.total a b)
(assume H : a ≤ b,
or.elim (iff.mp !le_iff_lt_or_eq H) (assume H1, or.inl H1) (assume H1, or.inr (or.inl H1)))
(assume H : b ≤ a,
or.elim (iff.mp !le_iff_lt_or_eq H)
(assume H1, or.inr (or.inr H1))
(assume H1, or.inr (or.inl (H1⁻¹))))
theorem lt_or_eq_or_lt_cases {a b : A} {P : Prop}
theorem lt.by_cases {a b : A} {P : Prop}
(H1 : a < b → P) (H2 : a = b → P) (H3 : b < a → P) : P :=
or.elim !lt_or_eq_or_lt (assume H, H1 H) (assume H, or.elim H (assume H', H2 H') (assume H', H3 H'))
or.elim !lt.trichotomy
(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] [s : linear_strong_order_pair A] :
linear_order_pair A :=
definition linear_strong_order_pair.to_linear_order_pair [instance] [coercion]
[s : linear_strong_order_pair A] : linear_order_pair A :=
linear_order_pair.mk linear_strong_order_pair.le linear_strong_order_pair.le_refl
linear_strong_order_pair.le_trans linear_strong_order_pair.le_antisym linear_strong_order_pair.lt
linear_strong_order_pair.le_trans linear_strong_order_pair.le_antisymm
linear_strong_order_pair.lt
linear_strong_order_pair.lt_iff_le_ne
(take a b : A,
lt_or_eq_or_lt_cases
lt.by_cases
(assume H : a < b, or.inl (le_of_lt H))
(assume H1 : a = b, or.inl (H1 ▸ !le.refl))
(assume H1 : b < a, or.inr (le_of_lt H1)))
definition le_of_not_lt {a b : A} (H : ¬ a < b) : b ≤ a :=
lt_or_eq_or_lt_cases (assume H', absurd H' H) (assume H', H' ▸ !le.refl) (assume H', le_of_lt H')
lt.by_cases (assume H', absurd H' H) (assume H', H' ▸ !le.refl) (assume H', le_of_lt H')
definition lt_of_not_le {a b : A} (H : ¬ a ≤ b) : b < a :=
lt_or_eq_or_lt_cases
lt.by_cases
(assume H', absurd (le_of_lt H') H)
(assume H', absurd (H' ▸ !le.refl) H)
(assume H', H')
end
end algebra

156
library/algebra/ordered_group.lean
View file

@ -5,114 +5,125 @@ Released under Apache 2.0 license as described in the file LICENSE.
Module: algebra.ordered_group
Authors: Jeremy Avigad
Partially ordered additive groups. Modeled on Isabelle's library. The comments below indicate that
we could refine the structures, though we would have to declare more inheritance paths.
Partially ordered additive groups, modeled on Isabelle's library. We could refine the structures,
but we would have to declare more inheritance paths.
-/
import logic.eq data.unit data.sigma data.prod
import algebra.function algebra.binary
import algebra.group algebra.order
open eq eq.ops -- note: ⁻¹ will be overloaded
namespace algebra
variable {A : Type}
/- partially ordered monoids, such as the natural numbers -/
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)
section
variables [s : ordered_cancel_comm_monoid A] (a b c d e : A)
variables [s : ordered_cancel_comm_monoid A]
variables {a b c d e : A}
include s
theorem add_le_add_left {a b : A} (H : a ≤ b) (c : A) : c + a ≤ c + b :=
theorem add_le_add_left (H : a ≤ b) (c : A) : c + a ≤ c + b :=
!ordered_cancel_comm_monoid.add_le_add_left H c
theorem add_le_add_right {a b : A} (H : a ≤ b) (c : A) : a + c ≤ b + 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)
theorem add_le_add {a b c d : A} (Hab : a ≤ b) (Hcd : c ≤ d) : a + c ≤ b + d :=
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 {a b : A} (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,
lt.ne H H4,
ne_of_lt H H4,
lt_of_le_of_ne H1 H2
theorem add_lt_add_right {a b : A} (H : a < b) (c : A) : a + c < b + c :=
theorem add_lt_add_right (H : a < b) (c : A) : a + c < b + c :=
(add.comm c a) ▸ (add.comm c b) ▸ (add_lt_add_left H c)
theorem add_lt_add_of_lt_of_lt {a b c d : A} (Hab : a < b) (Hcd : c < d) : a + c < b + d :=
theorem le_add_of_nonneg_right (H : b ≥ 0) : a ≤ a + b :=
!add_zero ▸ add_le_add_left H a
theorem le_add_of_nonneg_left (H : b ≥ 0) : a ≤ b + a :=
!zero_add ▸ add_le_add_right H a
theorem add_lt_add (Hab : a < b) (Hcd : c < d) : a + c < b + d :=
lt.trans (add_lt_add_right Hab c) (add_lt_add_left Hcd b)
theorem add_lt_add_of_le_of_lt {a b c d : A} (Hab : a ≤ b) (Hcd : c < d) : a + c < b + d :=
theorem add_lt_add_of_le_of_lt (Hab : a ≤ b) (Hcd : c < d) : a + c < b + d :=
lt_of_le_of_lt (add_le_add_right Hab c) (add_lt_add_left Hcd b)
theorem add_lt_add_of_lt_of_le {a b c d : A} (Hab : a < b) (Hcd : c ≤ d) : a + c < b + d :=
theorem add_lt_add_of_lt_of_le (Hab : a < b) (Hcd : c ≤ d) : a + c < b + d :=
lt_of_lt_of_le (add_lt_add_right Hab c) (add_le_add_left Hcd b)
theorem lt_add_of_pos_right (H : b > 0) : a < a + b := !add_zero ▸ add_lt_add_left H a
theorem lt_add_of_pos_left (H : b > 0) : a < b + a := !zero_add ▸ add_lt_add_right H a
-- here we start using le_of_add_le_add_left.
theorem le_of_add_le_add_left {a b c : A} (H : a + b ≤ a + c) : b ≤ c :=
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
theorem le_of_add_le_add_right {a b c : A} (H : a + b ≤ c + b) : a ≤ c :=
theorem le_of_add_le_add_right (H : a + b ≤ c + b) : a ≤ c :=
le_of_add_le_add_left ((add.comm a b) ▸ (add.comm c b) ▸ H)
theorem lt_of_add_lt_add_left {a b c : A} (H : a + b < a + c) : b < c :=
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),
have H2 : b ≠ c, from
assume H3 : b = c, lt.irrefl _ (H3 ▸ H),
lt_of_le_of_ne H1 H2
theorem lt_of_add_lt_add_right {a b c : A} (H : a + b < c + b) : a < c :=
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)
theorem add_le_add_left_iff : a + b ≤ a + c ↔ b ≤ c :=
theorem add_le_add_left_iff (a b c : A) : a + b ≤ a + c ↔ b ≤ c :=
iff.intro le_of_add_le_add_left (assume H, add_le_add_left H _)
theorem add_le_add_right_iff : a + b ≤ c + b ↔ a ≤ c :=
theorem add_le_add_right_iff (a b c : A) : a + b ≤ c + b ↔ a ≤ c :=
iff.intro le_of_add_le_add_right (assume H, add_le_add_right H _)
theorem add_lt_add_left_iff : a + b < a + c ↔ b < c :=
theorem add_lt_add_left_iff (a b c : A) : a + b < a + c ↔ b < c :=
iff.intro lt_of_add_lt_add_left (assume H, add_lt_add_left H _)
theorem add_lt_add_right_iff : a + b < c + b ↔ a < c :=
theorem add_lt_add_right_iff (a b c : A) : a + b < c + b ↔ a < c :=
iff.intro lt_of_add_lt_add_right (assume H, add_lt_add_right H _)
-- here we start using properties of zero.
theorem add_nonneg {a b : A} (Ha : 0 ≤ a) (Hb : 0 ≤ b) : 0 ≤ a + b :=
theorem add_nonneg (Ha : 0 ≤ a) (Hb : 0 ≤ b) : 0 ≤ a + b :=
!zero_add ▸ (add_le_add Ha Hb)
theorem add_pos_of_pos_of_nonneg {a b : A} (Ha : 0 < a) (Hb : 0 ≤ b) : 0 < a + b :=
theorem add_pos (Ha : 0 < a) (Hb : 0 < b) : 0 < a + b :=
!zero_add ▸ (add_lt_add Ha Hb)
theorem add_pos_of_pos_of_nonneg (Ha : 0 < a) (Hb : 0 ≤ b) : 0 < a + b :=
!zero_add ▸ (add_lt_add_of_lt_of_le Ha Hb)
theorem add_pos_of_nonneg_of_pos {a b : A} (Ha : 0 ≤ a) (Hb : 0 < b) : 0 < a + b :=
theorem add_pos_of_nonneg_of_pos (Ha : 0 ≤ a) (Hb : 0 < b) : 0 < a + b :=
!zero_add ▸ (add_lt_add_of_le_of_lt Ha Hb)
theorem add_pos_of_pos_of_pos {a b : A} (Ha : 0 < a) (Hb : 0 < b) : 0 < a + b :=
!zero_add ▸ (add_lt_add_of_lt_of_lt Ha Hb)
theorem add_nonpos {a b : A} (Ha : a ≤ 0) (Hb : b ≤ 0) : a + b ≤ 0 :=
theorem add_nonpos (Ha : a ≤ 0) (Hb : b ≤ 0) : a + b ≤ 0 :=
!zero_add ▸ (add_le_add Ha Hb)
theorem add_neg_of_neg_of_nonpos {a b : A} (Ha : a < 0) (Hb : b ≤ 0) : a + b < 0 :=
theorem add_neg (Ha : a < 0) (Hb : b < 0) : a + b < 0 :=
!zero_add ▸ (add_lt_add Ha Hb)
theorem add_neg_of_neg_of_nonpos (Ha : a < 0) (Hb : b ≤ 0) : a + b < 0 :=
!zero_add ▸ (add_lt_add_of_lt_of_le Ha Hb)
theorem add_neg_of_nonpos_of_neg {a b : A} (Ha : a ≤ 0) (Hb : b < 0) : a + b < 0 :=
theorem add_neg_of_nonpos_of_neg (Ha : a ≤ 0) (Hb : b < 0) : a + b < 0 :=
!zero_add ▸ (add_lt_add_of_le_of_lt Ha Hb)
theorem add_neg_of_neg_of_neg {a b : A} (Ha : a < 0) (Hb : b < 0) : a + b < 0 :=
!zero_add ▸ (add_lt_add_of_lt_of_lt Ha Hb)
-- TODO: add nonpos version (will be easier with simplifier)
theorem add_eq_zero_iff_eq_zero_and_eq_zero_of_nonneg_of_noneng {a b : A}
theorem add_eq_zero_iff_eq_zero_and_eq_zero_of_nonneg_of_nonneg
(Ha : 0 ≤ a) (Hb : 0 ≤ b) : a + b = 0 ↔ a = 0 ∧ b = 0 :=
iff.intro
(assume Hab : a + b = 0,
@ -121,13 +132,13 @@ section
a = a + 0 : add_zero
... ≤ a + b : add_le_add_left Hb
... = 0 : Hab,
have Haz : a = 0, from le.antisym Ha' Ha,
have Haz : a = 0, from le.antisymm Ha' Ha,
have Hb' : b ≤ 0, from
calc
b = 0 + b : zero_add
... ≤ a + b : add_le_add_right Ha
... = 0 : Hab,
have Hbz : b = 0, from le.antisym Hb' Hb,
have Hbz : b = 0, from le.antisymm Hb' Hb,
and.intro Haz Hbz)
(assume Hab : a = 0 ∧ b = 0,
(and.elim_left Hab)⁻¹ ▸ (and.elim_right Hab)⁻¹ ▸ (add_zero 0))
@ -163,10 +174,10 @@ section
!add_zero ▸ add_lt_add_of_lt_of_le Hbc Ha
theorem lt_add_of_pos_of_lt (Ha : 0 < a) (Hbc : b < c) : b < a + c :=
!zero_add ▸ add_lt_add_of_lt_of_lt Ha Hbc
!zero_add ▸ add_lt_add Ha Hbc
theorem lt_add_of_lt_of_pos (Hbc : b < c) (Ha : 0 < a) : b < c + a :=
!add_zero ▸ add_lt_add_of_lt_of_lt Hbc Ha
!add_zero ▸ add_lt_add Hbc Ha
theorem add_lt_of_nonpos_of_lt (Ha : a ≤ 0) (Hbc : b < c) : a + b < c :=
!zero_add ▸ add_lt_add_of_le_of_lt Ha Hbc
@ -175,28 +186,25 @@ section
!add_zero ▸ add_lt_add_of_lt_of_le Hbc Ha
theorem add_lt_of_neg_of_lt (Ha : a < 0) (Hbc : b < c) : a + b < c :=
!zero_add ▸ add_lt_add_of_lt_of_lt Ha Hbc
!zero_add ▸ add_lt_add Ha Hbc
theorem add_lt_of_lt_of_neg (Hbc : b < c) (Ha : a < 0) : b + a < c :=
!add_zero ▸ add_lt_add_of_lt_of_lt Hbc Ha
!add_zero ▸ add_lt_add Hbc Ha
end
-- TODO: there is more we can do if we have max and min (in order.lean as well)
-- TODO: add properties of max and min
-- TODO: there is more we can do if we assume a ≤ b ↔ ∃c. a + c = b.
-- This covers the natural numbers,
-- but it is not clear whether it provides any further useful generality.
/- 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))
definition ordered_comm_group.to_ordered_cancel_comm_monoid [instance] (A : Type)
definition ordered_comm_group.to_ordered_cancel_comm_monoid [instance] [coercion]
[s : ordered_comm_group A] : ordered_cancel_comm_monoid A :=
ordered_cancel_comm_monoid.mk ordered_comm_group.add ordered_comm_group.add_assoc
(@ordered_comm_group.zero A s) zero_add add_zero ordered_comm_group.add_comm
(@add.left_cancel _ _) (@add.right_cancel _ _)
has_le.le le.refl (@le.trans _ _) (@le.antisym _ _)
has_le.le le.refl (@le.trans _ _) (@le.antisymm _ _)
has_lt.lt (@lt_iff_le_and_ne _ _) ordered_comm_group.add_le_add_left
proof
take a b c : A,
@ -206,17 +214,16 @@ proof
qed
section
variables [s : ordered_comm_group A] (a b c d e : A)
include s
theorem neg_le_neg_of_le {a b : A} (H : a ≤ b) : -b ≤ -a :=
theorem neg_le_neg {a b : A} (H : a ≤ b) : -b ≤ -a :=
have H1 : 0 ≤ -a + b, from !add.left_inv ▸ !(add_le_add_left H),
!add_neg_cancel_right ▸ !zero_add ▸ add_le_add_right H1 (-b)
-- !zero_add ▸ !add_neg_cancel_right ▸ add_le_add_right H1 (-b) -- doesn't work?
-- !zero_add ▸ !add_neg_cancel_right ▸ add_le_add_right H1 (-b) -- doesn't work
theorem neg_le_neg_iff_le : -a ≤ -b ↔ b ≤ a :=
iff.intro (take H, neg_neg a ▸ neg_neg b ▸ neg_le_neg_of_le H) neg_le_neg_of_le
iff.intro (take H, neg_neg a ▸ neg_neg b ▸ neg_le_neg H) neg_le_neg
theorem neg_nonpos_iff_nonneg : -a ≤ 0 ↔ 0 ≤ a :=
neg_zero ▸ neg_le_neg_iff_le a 0
@ -224,12 +231,12 @@ section
theorem neg_nonneg_iff_nonpos : 0 ≤ -a ↔ a ≤ 0 :=
neg_zero ▸ neg_le_neg_iff_le 0 a
theorem neg_lt_neg_of_lt {a b : A} (H : a < b) : -b < -a :=
theorem neg_lt_neg {a b : A} (H : a < b) : -b < -a :=
have H1 : 0 < -a + b, from !add.left_inv ▸ !(add_lt_add_left H),
!add_neg_cancel_right ▸ !zero_add ▸ add_lt_add_right H1 (-b)
theorem neg_lt_neg_iff_lt : -a < -b ↔ b < a :=
iff.intro (take H, neg_neg a ▸ neg_neg b ▸ neg_lt_neg_of_lt H) neg_lt_neg_of_lt
iff.intro (take H, neg_neg a ▸ neg_neg b ▸ neg_lt_neg H) neg_lt_neg
theorem neg_neg_iff_pos : -a < 0 ↔ 0 < a :=
neg_zero ▸ neg_lt_neg_iff_lt a 0
@ -275,27 +282,32 @@ section
have H: a ≤ b + c ↔ a - c ≤ b + c - c, from iff.symm (!add_le_add_right_iff),
!add_neg_cancel_right ▸ H
theorem add_lt_add_iff_lt_neg_add : a + b < c ↔ b < -a + c :=
theorem add_lt_iff_lt_neg_add_left : a + b < c ↔ b < -a + c :=
have H: a + b < c ↔ -a + (a + b) < -a + c, from iff.symm (!add_lt_add_left_iff),
!neg_add_cancel_left ▸ H
theorem add_lt_add_iff_lt_sub_left : a + b < c ↔ b < c - a :=
!add.comm ▸ !add_lt_add_iff_lt_neg_add
theorem add_lt_iff_lt_neg_add_right : a + b < c ↔ a < -b + c :=
!add.comm ▸ !add_lt_iff_lt_neg_add_left
theorem add_lt_iff_lt_sub_left : a + b < c ↔ b < c - a :=
!add.comm ▸ !add_lt_iff_lt_neg_add_left
theorem add_lt_add_iff_lt_sub_right : a + b < c ↔ a < c - b :=
have H: a + b < c ↔ a + b - b < c - b, from iff.symm (!add_lt_add_right_iff),
!add_neg_cancel_right ▸ H
theorem lt_add_iff_neg_add_lt_add : a < b + c ↔ -b + a < c :=
theorem lt_add_iff_neg_add_lt_left : a < b + c ↔ -b + a < c :=
have H: a < b + c ↔ -b + a < -b + (b + c), from iff.symm (!add_lt_add_left_iff),
!neg_add_cancel_left ▸ H
theorem lt_add_iff_sub_left_lt : a < b + c ↔ a - b < c :=
!add.comm ▸ !lt_add_iff_neg_add_lt_add
theorem lt_add_iff_neg_add_lt_right : a < b + c ↔ -c + a < b :=
!add.comm ▸ !lt_add_iff_neg_add_lt_left
theorem lt_add_iff_sub_right_lt : a < b + c ↔ a - c < b :=
have H: a < b + c ↔ a - c < b + c - c, from iff.symm (!add_lt_add_right_iff),
!add_neg_cancel_right ▸ H
theorem lt_add_iff_sub_lt_left : a < b + c ↔ a - b < c :=
!add.comm ▸ !lt_add_iff_neg_add_lt_left
theorem lt_add_iff_sub_lt_right : a < b + c ↔ a - c < b :=
!add.comm ▸ !lt_add_iff_sub_lt_left
-- TODO: the Isabelle library has varations on a + b ≤ b ↔ a ≤ 0
@ -312,31 +324,29 @@ section
... ↔ c < d : sub_neg_iff_lt c d
theorem sub_le_sub_left {a b : A} (H : a ≤ b) (c : A) : c - b ≤ c - a :=
add_le_add_left (neg_le_neg_of_le H) c
add_le_add_left (neg_le_neg H) c
theorem sub_le_sub_right {a b : A} (H : a ≤ b) (c : A) : a - c ≤ b - c := add_le_add_right H (-c)
theorem sub_le_sub {a b c d : A} (Hab : a ≤ b) (Hcd : c ≤ d) : a - d ≤ b - c :=
add_le_add Hab (neg_le_neg_of_le Hcd)
add_le_add Hab (neg_le_neg Hcd)
theorem sub_lt_sub_left {a b : A} (H : a < b) (c : A) : c - b < c - a :=
add_lt_add_left (neg_lt_neg_of_lt H) c
add_lt_add_left (neg_lt_neg H) c
theorem sub_lt_sub_right {a b : A} (H : a < b) (c : A) : a - c < b - c := add_lt_add_right H (-c)
theorem sub_lt_sub_of_lt_of_lt {a b c d : A} (Hab : a < b) (Hcd : c < d) : a - d < b - c :=
add_lt_add_of_lt_of_lt Hab (neg_lt_neg_of_lt Hcd)
theorem sub_lt_sub {a b c d : A} (Hab : a < b) (Hcd : c < d) : a - d < b - c :=
add_lt_add Hab (neg_lt_neg Hcd)
theorem sub_lt_sub_of_le_of_lt {a b c d : A} (Hab : a ≤ b) (Hcd : c < d) : a - d < b - c :=
add_lt_add_of_le_of_lt Hab (neg_lt_neg_of_lt Hcd)
add_lt_add_of_le_of_lt Hab (neg_lt_neg Hcd)
theorem sub_lt_sub_of_lt_of_le {a b c d : A} (Hab : a < b) (Hcd : c ≤ d) : a - d < b - c :=
add_lt_add_of_lt_of_le Hab (neg_le_neg_of_le Hcd)
add_lt_add_of_lt_of_le Hab (neg_le_neg Hcd)
end
-- TODO: additional facts if the ordering is a linear ordering (e.g. -a = a ↔ a = 0)
-- TODO: structures with abs
-- TODO: abs and sign
end algebra

185
library/algebra/ordered_ring.lean
View file

@ -5,17 +5,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
Module: algebra.ordered_ring
Authors: Jeremy Avigad
Rather than multiply classes unnecessarily, we are aiming for the ones that are likely to be useful.
We can always split them apart later if necessary. Here an "ordered_ring" is partial ordered ring (which
is ordered with respect to both a weak order and an associated strict order). Our numeric structures will be
instances of "linear_ordered_comm_ring".
This development is modeled after Isabelle's library.
Here an "ordered_ring" is partially ordered ring, which is ordered with respect to both a weak
order and an associated strict order. Our numeric structures (int, rat, and real) will be instances
of "linear_ordered_comm_ring". This development is modeled after Isabelle's library.
-/
import logic.eq data.unit data.sigma data.prod
import algebra.function algebra.binary algebra.ordered_group algebra.ring
import algebra.ordered_group algebra.ring
open eq eq.ops
namespace algebra
@ -23,13 +18,12 @@ namespace algebra
variable {A : Type}
structure ordered_semiring [class] (A : Type) extends semiring A, ordered_cancel_comm_monoid A :=
(mul_le_mul_left: ∀a b c, le a b → le zero c → le (mul c a) (mul c b))
(mul_le_mul_right: ∀a b c, le a b → le zero c → le (mul a c) (mul b c))
(mul_lt_mul_left: ∀a b c, lt a b → lt zero c → lt (mul c a) (mul c b))
(mul_lt_mul_right: ∀a b c, lt a b → lt zero c → lt (mul a c) (mul b c))
(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))
section
variable [s : ordered_semiring A]
variables (a b c d e : A)
include s
@ -43,10 +37,10 @@ section
has_zero.mk (@ordered_semiring.zero A s)
theorem mul_le_mul_of_nonneg_left {a b c : A} (Hab : a ≤ b) (Hc : 0 ≤ c) :
c * a ≤ c * b := !ordered_semiring.mul_le_mul_left Hab Hc
c * a ≤ c * b := !ordered_semiring.mul_le_mul_of_nonneg_left Hab Hc
theorem mul_le_mul_of_nonneg_right {a b c : A} (Hab : a ≤ b) (Hc : 0 ≤ c) :
a * c ≤ b * c := !ordered_semiring.mul_le_mul_right Hab Hc
a * c ≤ b * c := !ordered_semiring.mul_le_mul_of_nonneg_right Hab Hc
-- TODO: there are four variations, depending on which variables we assume to be nonneg
theorem mul_le_mul {a b c d : A} (Hac : a ≤ c) (Hbd : b ≤ d) (nn_b : 0 ≤ b) (nn_c : 0 ≤ c) :
@ -55,7 +49,7 @@ section
a * b ≤ c * b : mul_le_mul_of_nonneg_right Hac nn_b
... ≤ c * d : mul_le_mul_of_nonneg_left Hbd nn_c
theorem mul_nonneg_of_nonneg_of_nonneg {a b : A} (Ha : a ≥ 0) (Hb : b ≥ 0) : a * b ≥ 0 :=
theorem mul_nonneg {a b : A} (Ha : a ≥ 0) (Hb : b ≥ 0) : a * b ≥ 0 :=
have H : 0 * b ≤ a * b, from mul_le_mul_of_nonneg_right Ha Hb,
!zero_mul ▸ H
@ -68,10 +62,10 @@ section
!zero_mul ▸ H
theorem mul_lt_mul_of_pos_left {a b c : A} (Hab : a < b) (Hc : 0 < c) :
c * a < c * b := !ordered_semiring.mul_lt_mul_left Hab Hc
c * a < c * b := !ordered_semiring.mul_lt_mul_of_pos_left Hab Hc
theorem mul_lt_mul_of_pos_right {a b c : A} (Hab : a < b) (Hc : 0 < c) :
a * c < b * c := !ordered_semiring.mul_lt_mul_right Hab Hc
a * c < b * c := !ordered_semiring.mul_lt_mul_of_pos_right Hab Hc
-- TODO: once again, there are variations
theorem mul_lt_mul {a b c d : A} (Hac : a < c) (Hbd : b ≤ d) (pos_b : 0 < b) (nn_c : 0 ≤ c) :
@ -80,7 +74,7 @@ section
a * b < c * b : mul_lt_mul_of_pos_right Hac pos_b
... ≤ c * d : mul_le_mul_of_nonneg_left Hbd nn_c
theorem mul_pos_of_pos_of_pos {a b : A} (Ha : a > 0) (Hb : b > 0) : a * b > 0 :=
theorem mul_pos {a b : A} (Ha : a > 0) (Hb : b > 0) : a * b > 0 :=
have H : 0 * b < a * b, from mul_lt_mul_of_pos_right Ha Hb,
!zero_mul ▸ H
@ -91,16 +85,14 @@ section
theorem mul_neg_of_neg_of_pos {a b : A} (Ha : a < 0) (Hb : b > 0) : a * b < 0 :=
have H : a * b < 0 * b, from mul_lt_mul_of_pos_right Ha Hb,
!zero_mul ▸ H
end
structure linear_ordered_semiring [class] (A : Type)
extends ordered_semiring A, linear_strong_order_pair A
section
variable [s : linear_ordered_semiring A]
variables (a b c : A)
variables {a b c : A}
include s
-- TODO: remove after we short-circuit class-graph
@ -111,25 +103,25 @@ section
definition linear_ordered_semiring.to_zero [instance] [priority 100000] : has_zero A :=
has_zero.mk (@linear_ordered_semiring.zero A s)
theorem lt_of_mul_lt_mul_left {a b c : A} (H : c * a < c * b) (Hc : c ≥ 0) : a < b :=
theorem lt_of_mul_lt_mul_left (H : c * a < c * b) (Hc : c ≥ 0) : a < b :=
lt_of_not_le
(assume H1 : b ≤ a,
have H2 : c * b ≤ c * a, from mul_le_mul_of_nonneg_left H1 Hc,
not_lt_of_le H2 H)
theorem lt_of_mul_lt_mul_right {a b c : A} (H : a * c < b * c) (Hc : c ≥ 0) : a < b :=
theorem lt_of_mul_lt_mul_right (H : a * c < b * c) (Hc : c ≥ 0) : a < b :=
lt_of_not_le
(assume H1 : b ≤ a,
have H2 : b * c ≤ a * c, from mul_le_mul_of_nonneg_right H1 Hc,
not_lt_of_le H2 H)
theorem le_of_mul_le_mul_left {a b c : A} (H : c * a ≤ c * b) (Hc : c > 0) : a ≤ b :=
theorem le_of_mul_le_mul_left (H : c * a ≤ c * b) (Hc : c > 0) : a ≤ b :=
le_of_not_lt
(assume H1 : b < a,
have H2 : c * b < c * a, from mul_lt_mul_of_pos_left H1 Hc,
not_le_of_lt H2 H)
theorem le_of_mul_le_mul_right {a b c : A} (H : a * c ≤ b * c) (Hc : c > 0) : a ≤ b :=
theorem le_of_mul_le_mul_right (H : a * c ≤ b * c) (Hc : c > 0) : a ≤ b :=
le_of_not_lt
(assume H1 : b < a,
have H2 : b * c < a * c, from mul_lt_mul_of_pos_right H1 Hc,
@ -146,21 +138,21 @@ section
(assume H2 : a ≤ 0,
have H3 : a * b ≤ 0, from mul_nonpos_of_nonpos_of_nonneg H2 H1,
not_lt_of_le H3 H)
end
structure ordered_ring [class] (A : Type) extends ring A, ordered_comm_group A :=
(mul_nonneg_of_nonneg_of_nonneg : ∀a b, le zero a → le zero b → le zero (mul a b))
(mul_pos_of_pos_of_pos : ∀a b, lt zero a → lt zero b → lt zero (mul a b))
(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))
definition ordered_ring.to_ordered_semiring [instance] [s : ordered_ring A] : ordered_semiring A :=
definition ordered_ring.to_ordered_semiring [instance] [coercion] [s : ordered_ring A] :
ordered_semiring A :=
ordered_semiring.mk ordered_ring.add ordered_ring.add_assoc !ordered_ring.zero
ordered_ring.zero_add ordered_ring.add_zero ordered_ring.add_comm ordered_ring.mul
ordered_ring.mul_assoc !ordered_ring.one ordered_ring.one_mul ordered_ring.mul_one
ordered_ring.left_distrib ordered_ring.right_distrib
zero_mul mul_zero !ordered_ring.zero_ne_one
(@add.left_cancel A _) (@add.right_cancel A _)
ordered_ring.le ordered_ring.le_refl ordered_ring.le_trans ordered_ring.le_antisym
ordered_ring.le ordered_ring.le_refl ordered_ring.le_trans ordered_ring.le_antisymm
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,
@ -169,7 +161,7 @@ ordered_semiring.mk ordered_ring.add ordered_ring.add_assoc !ordered_ring.zero
show c * a ≤ c * b,
proof
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_of_nonneg_of_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)
qed)
(take a b c,
@ -178,7 +170,7 @@ ordered_semiring.mk ordered_ring.add ordered_ring.add_assoc !ordered_ring.zero
show a * c ≤ b * c,
proof
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_of_nonneg_of_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)
qed)
(take a b c,
@ -187,7 +179,7 @@ ordered_semiring.mk ordered_ring.add ordered_ring.add_assoc !ordered_ring.zero
show c * a < c * b,
proof
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_of_pos_of_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)
qed)
(take a b c,
@ -196,14 +188,13 @@ ordered_semiring.mk ordered_ring.add ordered_ring.add_assoc !ordered_ring.zero
show a * c < b * c,
proof
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_of_pos_of_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)
qed)
section
variable [s : ordered_ring A]
variables (a b c : A)
variables {a b c : A}
include s
-- TODO: remove after we short-circuit class-graph
@ -214,65 +205,107 @@ section
definition ordered_ring.to_zero [instance] [priority 100000] : has_zero A :=
has_zero.mk (@ordered_ring.zero A s)
theorem mul_le_mul_of_nonpos_left {a b c : A} (H : b ≤ a) (Hc : c ≤ 0) : c * a ≤ c * b :=
theorem mul_le_mul_of_nonpos_left (H : b ≤ a) (Hc : c ≤ 0) : c * a ≤ c * b :=
have Hc' : -c ≥ 0, from iff.mp' !neg_nonneg_iff_nonpos Hc,
have H1 : -c * b ≤ -c * a, from mul_le_mul_of_nonneg_left H Hc',
have H2 : -(c * b) ≤ -(c * a), from !neg_mul_eq_neg_mul⁻¹ ▸ !neg_mul_eq_neg_mul⁻¹ ▸ H1,
iff.mp !neg_le_neg_iff_le H2
theorem mul_le_mul_of_nonpos_right {a b c : A} (H : b ≤ a) (Hc : c ≤ 0) : a * c ≤ b * c :=
theorem mul_le_mul_of_nonpos_right (H : b ≤ a) (Hc : c ≤ 0) : a * c ≤ b * c :=
have Hc' : -c ≥ 0, from iff.mp' !neg_nonneg_iff_nonpos Hc,
have H1 : b * -c ≤ a * -c, from mul_le_mul_of_nonneg_right H Hc',
have H2 : -(b * c) ≤ -(a * c), from !neg_mul_eq_mul_neg⁻¹ ▸ !neg_mul_eq_mul_neg⁻¹ ▸ H1,
iff.mp !neg_le_neg_iff_le H2
theorem mul_nonneg_of_nonpos_of_nonpos {a b : A} (Ha : a ≤ 0) (Hb : b ≤ 0) : 0 ≤ a * b :=
theorem mul_nonneg_of_nonpos_of_nonpos (Ha : a ≤ 0) (Hb : b ≤ 0) : 0 ≤ a * b :=
!zero_mul ▸ mul_le_mul_of_nonpos_right Ha Hb
theorem mul_lt_mul_of_neg_left {a b c : A} (H : b < a) (Hc : c < 0) : c * a < c * b :=
theorem mul_lt_mul_of_neg_left (H : b < a) (Hc : c < 0) : c * a < c * b :=
have Hc' : -c > 0, from iff.mp' !neg_pos_iff_neg Hc,
have H1 : -c * b < -c * a, from mul_lt_mul_of_pos_left H Hc',
have H2 : -(c * b) < -(c * a), from !neg_mul_eq_neg_mul⁻¹ ▸ !neg_mul_eq_neg_mul⁻¹ ▸ H1,
iff.mp !neg_lt_neg_iff_lt H2
theorem mul_lt_mul_of_neg_right {a b c : A} (H : b < a) (Hc : c < 0) : a * c < b * c :=
theorem mul_lt_mul_of_neg_right (H : b < a) (Hc : c < 0) : a * c < b * c :=
have Hc' : -c > 0, from iff.mp' !neg_pos_iff_neg Hc,
have H1 : b * -c < a * -c, from mul_lt_mul_of_pos_right H Hc',
have H2 : -(b * c) < -(a * c), from !neg_mul_eq_mul_neg⁻¹ ▸ !neg_mul_eq_mul_neg⁻¹ ▸ H1,
iff.mp !neg_lt_neg_iff_lt H2
theorem mul_pos_of_neg_of_neg {a b : A} (Ha : a < 0) (Hb : b < 0) : 0 < a * b :=
theorem mul_pos_of_neg_of_neg (Ha : a < 0) (Hb : b < 0) : 0 < a * b :=
!zero_mul ▸ mul_lt_mul_of_neg_right Ha Hb
end
-- TODO: we can eliminate mul_pos_of_pos, but now it is not worth the effort to redeclare the class instance
-- 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
-- TODO: after we break out definition of divides, show that this is an instance of integral domain,
-- i.e no zero divisors
-- print fields linear_ordered_semiring
definition linear_ordered_ring.to_linear_ordered_semiring [instance] [coercion]
[s : linear_ordered_ring A] :
linear_ordered_semiring A :=
linear_ordered_semiring.mk linear_ordered_ring.add linear_ordered_ring.add_assoc
(@linear_ordered_ring.zero _ _) linear_ordered_ring.zero_add linear_ordered_ring.add_zero
linear_ordered_ring.add_comm linear_ordered_ring.mul linear_ordered_ring.mul_assoc
(@linear_ordered_ring.one _ _) linear_ordered_ring.one_mul linear_ordered_ring.mul_one
linear_ordered_ring.left_distrib linear_ordered_ring.right_distrib
zero_mul mul_zero !ordered_ring.zero_ne_one
(@add.left_cancel A _) (@add.right_cancel A _)
linear_ordered_ring.le linear_ordered_ring.le_refl linear_ordered_ring.le_trans
linear_ordered_ring.le_antisymm
linear_ordered_ring.lt linear_ordered_ring.lt_iff_le_ne linear_ordered_ring.add_le_add_left
(@le_of_add_le_add_left A _)
(@mul_le_mul_of_nonneg_left A _) (@mul_le_mul_of_nonneg_right A _)
(@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
-- Linearity implies no zero divisors. Doesn't need commutativity.
definition linear_ordered_comm_ring.to_integral_domain [instance] [coercion]
[s: linear_ordered_comm_ring A] :
integral_domain A :=
integral_domain.mk linear_ordered_comm_ring.add linear_ordered_comm_ring.add_assoc
(@linear_ordered_comm_ring.zero _ _)
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,
show a = 0 ∨ b = 0, from
lt.by_cases
(assume Ha : 0 < a,
lt.by_cases
(assume Hb : 0 < b, absurd (H ▸ mul_pos Ha Hb) (lt.irrefl 0))
(assume Hb : 0 = b, or.inr (Hb⁻¹))
(assume Hb : 0 > b, absurd (H ▸ mul_neg_of_pos_of_neg Ha Hb) (lt.irrefl 0)))
(assume Ha : 0 = a, or.inl (Ha⁻¹))
(assume Ha : 0 > a,
lt.by_cases
(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, absurd (H ▸ mul_pos_of_neg_of_neg Ha Hb) (lt.irrefl 0))))
section
variable [s : linear_ordered_ring A]
variables (a b c : A)
include s
theorem mul_self_nonneg : a * a ≥ 0 :=
or.elim (le.total 0 a)
(assume H : a ≥ 0, mul_nonneg_of_nonneg_of_nonneg H H)
(assume H : a ≥ 0, mul_nonneg H H)
(assume H : a ≤ 0, mul_nonneg_of_nonpos_of_nonpos H H)
theorem zero_le_one : 0 ≤ 1 := one_mul 1 ▸ mul_self_nonneg 1
theorem zero_lt_one : 0 < 1 := lt_of_le_of_ne zero_le_one zero_ne_one
-- TODO: move these to ordered_group.lean
theorem lt_add_of_pos_right {a b : A} (H : b > 0) : a < a + b := !add_zero ▸ add_lt_add_left H a
theorem lt_add_of_pos_left {a b : A} (H : b > 0) : a < b + a := !zero_add ▸ add_lt_add_right H a
theorem le_add_of_nonneg_right {a b : A} (H : b ≥ 0) : a ≤ a + b := !add_zero ▸ add_le_add_left H a
theorem le_add_of_nonneg_left {a b : A} (H : b ≥ 0) : a ≤ b + a := !zero_add ▸ add_le_add_right H a
-- TODO: remove after we short-circuit class-graph
definition linear_ordered_ring.to_mul [instance] [priority 100000] : has_mul A :=
has_mul.mk (@linear_ordered_ring.mul A s)
@ -281,49 +314,25 @@ section
definition linear_ordered_ring.to_zero [instance] [priority 100000] : has_zero A :=
has_zero.mk (@linear_ordered_ring.zero A s)
/- TODO: a good example of a performance bottleneck.
Without any of the "proof ... qed" pairs, it exceeds the unifier maximum number of steps.
It works with at least one "proof ... qed", but takes about two seconds on my laptop. I do not
know where the bottleneck is.
Adding the explicit arguments to lt_or_eq_or_lt_cases does not seem to help at all. (The proof
still works if all the instances are replaced by "lt_or_eq_or_lt_cases" alone.)
Adding an extra "proof ... qed" around "!mul_zero ▸ Hb⁻¹ ▸ Hab" fails with "value has
metavariables". I am not sure why.
-/
theorem pos_and_pos_or_neg_and_neg_of_mul_pos (Hab : a * b > 0) :
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) :=
lt_or_eq_or_lt_cases
lt.by_cases
(assume Ha : 0 < a,
lt_or_eq_or_lt_cases
lt.by_cases
(assume Hb : 0 < b, or.inl (and.intro Ha Hb))
(assume Hb : 0 = b,
absurd (!mul_zero ▸ Hb⁻¹ ▸ Hab) (lt.irrefl 0))
(assume Hb : b < 0,
absurd Hab (not_lt_of_lt (mul_neg_of_pos_of_neg Ha Hb))))
absurd Hab (lt.asymm (mul_neg_of_pos_of_neg Ha Hb))))
(assume Ha : 0 = a,
absurd (!zero_mul ▸ Ha⁻¹ ▸ Hab) (lt.irrefl 0))
(assume Ha : a < 0,
lt_or_eq_or_lt_cases
lt.by_cases
(assume Hb : 0 < b,
absurd Hab (not_lt_of_lt (mul_neg_of_neg_of_pos Ha Hb)))
absurd Hab (lt.asymm (mul_neg_of_neg_of_pos Ha Hb)))
(assume Hb : 0 = b,
absurd (!mul_zero ▸ Hb⁻¹ ▸ Hab) (lt.irrefl 0))
(assume Hb : b < 0, or.inr (and.intro Ha Hb)))
set_option pp.coercions true
set_option pp.implicit true
set_option pp.notation false
-- print definition pos_and_pos_or_neg_and_neg_of_mul_pos
-- TODO: use previous and integral domain
theorem noneg_and_nonneg_or_nonpos_and_nonpos_of_mul_nonneg (Hab : a * b ≥ 0) :
(a ≥ 0 ∧ b ≥ 0) ∨ (a ≤ 0 ∧ b ≤ 0) :=
sorry
end
/-
@ -337,6 +346,4 @@ end
Multiplication and one, starting with mult_right_le_one_le.
-/
structure linear_ordered_comm_ring [class] (A : Type) extends linear_ordered_ring A, comm_monoid A
end algebra

32
library/algebra/ring.lean
View file

@ -11,7 +11,6 @@ The development is modeled after Isabelle's library.
import logic.eq logic.connectives data.unit data.sigma data.prod
import algebra.function algebra.binary algebra.group
open eq eq.ops
namespace algebra
@ -48,7 +47,6 @@ structure semiring [class] (A : Type) extends add_comm_monoid A, monoid A, distr
mul_zero_class A, zero_ne_one_class A
section semiring
variables [s : semiring A] (a b c : A)
include s
@ -61,17 +59,15 @@ section semiring
assume H1 : b = 0,
have H2 : a * b = 0, from H1⁻¹ ▸ mul_zero a,
H H2
end semiring
/- comm semiring -/
structure comm_semiring [class] (A : Type) extends semiring A, comm_semigroup A
-- TODO: we could also define a cancelative comm_semiring, i.e. satisfying c ≠ 0 → c * a = c * b → a = b.
-- TODO: we could also define a cancelative comm_semiring, i.e. satisfying
-- c ≠ 0 → c * a = c * b → a = b.
section comm_semiring
variables [s : comm_semiring A] (a b c : A)
include s
@ -81,6 +77,9 @@ section comm_semiring
theorem dvd.intro {a b c : A} (H : a * b = c) : a | c :=
exists.intro _ H
theorem dvd.intro_right {a b c : A} (H : a * b = c) : b | c :=
dvd.intro (!mul.comm ▸ H)
theorem dvd.ex {a b : A} (H : a | b) : ∃c, a * c = b := H
theorem dvd.elim {P : Prop} {a b : A} (H₁ : a | b) (H₂ : ∀c, a * c = b → P) : P :=
@ -147,15 +146,13 @@ section comm_semiring
dvd.elim Hac
(take e, assume Haec : a * e = c,
dvd.intro (show a * (d + e) = b + c, from Hadb ▸ Haec ▸ left_distrib a d e)))
end comm_semiring
/- ring -/
structure ring [class] (A : Type) extends add_comm_group A, monoid A, distrib A, zero_ne_one_class A
definition ring.to_semiring [instance] [s : ring A] : semiring A :=
definition ring.to_semiring [instance] [coercion] [s : ring A] : semiring A :=
semiring.mk ring.add ring.add_assoc !ring.zero ring.zero_add
add_zero -- note: we've shown that add_zero follows from zero_add in add_comm_group
ring.add_comm ring.mul ring.mul_assoc !ring.one ring.one_mul ring.mul_one
@ -177,7 +174,6 @@ semiring.mk ring.add ring.add_assoc !ring.zero ring.zero_add
!ring.zero_ne_one
section
variables [s : ring A] (a b c d e : A)
include s
@ -225,12 +221,11 @@ section
... ↔ a * e + c - b * e = d : iff.symm !sub_eq_iff_eq_add
... ↔ a * e - b * e + c = d : !sub_add_eq_add_sub ▸ !iff.refl
... ↔ (a - b) * e + c = d : !mul_sub_right_distrib ▸ !iff.refl
end
structure comm_ring [class] (A : Type) extends ring A, comm_semigroup A
definition comm_ring.to_comm_semiring [instance] [s : comm_ring A] : comm_semiring A :=
definition comm_ring.to_comm_semiring [instance] [coercion] [s : comm_ring A] : comm_semiring A :=
comm_semiring.mk comm_ring.add comm_ring.add_assoc (@comm_ring.zero A s)
comm_ring.zero_add comm_ring.add_zero comm_ring.add_comm comm_ring.mul comm_ring.mul_assoc
(@comm_ring.one A s) comm_ring.one_mul comm_ring.mul_one comm_ring.left_distrib
@ -238,7 +233,6 @@ comm_semiring.mk comm_ring.add comm_ring.add_assoc (@comm_ring.zero A s)
comm_ring.mul_comm
section
variables [s : comm_ring A] (a b c d e : A)
include s
@ -248,13 +242,6 @@ section
theorem mul_self_sub_one_eq : a * a - 1 = (a + 1) * (a - 1) :=
mul_one 1 ▸ mul_self_sub_mul_self_eq a 1
end
section
variables [s : comm_ring A] (a b c d e : A)
include s
theorem dvd_neg_iff_dvd : a | -b ↔ a | b :=
iff.intro
(assume H : a | -b,
@ -292,14 +279,10 @@ section
theorem dvd_sub (H₁ : a | b) (H₂ : a | c) : a | (b - c) :=
dvd_add H₁ (iff.elim_right !dvd_neg_iff_dvd H₂)
end
/- integral domains -/
-- TODO: some properties here may extend to cancellative semirings. It is worth the effort?
structure no_zero_divisors [class] (A : Type) extends has_mul A, has_zero A :=
(eq_zero_or_eq_zero_of_mul_eq_zero : ∀a b, mul a b = zero → a = zero ∨ b = zero)
@ -353,7 +336,6 @@ section
have H1 : b * d * a = c * a, from eq.trans !mul.right_comm H,
have H2 : b * d = c, from mul.cancel_right Ha H1,
dvd.intro H2)
end
end algebra

90
library/data/int/basic.lean
View file

@ -6,15 +6,15 @@ Module: int.basic
Authors: Floris van Doorn, Jeremy Avigad
The integers, with addition, multiplication, and subtraction. The representation of the integers is
chosen to compute efficiently; see the examples in the comments at the end of this file.
chosen to compute efficiently.
To faciliate proving things about these operations, we show that the integers are a quotient of
ℕ × ℕ with the usual equivalence relation ≡, and functions
ℕ × ℕ with the usual equivalence relation, ≡, and functions
abstr : ℕ × ℕ → ℤ
repr : ℤ → ℕ × ℕ
satisfying
satisfying:
abstr_repr (a : ℤ) : abstr (repr a) = a
repr_abstr (p : ℕ × ℕ) : repr (abstr p) ≡ p
@ -25,12 +25,12 @@ following:
repr_add (a b : ℤ) : repr (a + b) = padd (repr a) (repr b)
padd_congr (p p' q q' : ℕ × ℕ) (H1 : p ≡ p') (H2 : q ≡ q') : padd p q ≡ p' q'
-/
import data.nat.basic data.nat.order data.nat.sub data.prod
import algebra.relation algebra.binary algebra.ordered_ring
import tools.fake_simplifier
open eq.ops
open prod relation nat
open decidable binary fake_simplifier
@ -54,8 +54,8 @@ nat.cases_on m 0 (take m', neg_succ_of_nat m')
definition sub_nat_nat (m n : ℕ) : ℤ :=
nat.cases_on (n - m)
(of_nat (m - n)) -- m ≥ n
(take k, neg_succ_of_nat k) -- m < n, and n - m = succ k
(of_nat (m - n)) -- m ≥ n
(take k, neg_succ_of_nat k) -- m < n, and n - m = succ k
definition neg (a : ℤ) : ℤ :=
cases_on a
@ -144,11 +144,7 @@ cases_on a
(take m, assume H : nat_abs (of_nat m) = 0, congr_arg of_nat H)
(take m', assume H : nat_abs (neg_succ_of_nat m') = 0, absurd H (succ_ne_zero _))
/-
Show int is a quotient of ordered pairs of natural numbers, with the usual
equivalence relation.
-/
/- int is a quotient of ordered pairs of natural numbers -/
definition equiv (p q : ℕ × ℕ) : Prop := pr1 p + pr2 q = pr2 p + pr1 q
@ -319,7 +315,7 @@ or.elim (cases_of_nat_succ a)
(assume H, obtain (n : ℕ) (H3 : a = -(succ n)), from H, H3⁻¹ ▸ H2 n)
/-
Show int is a ring.
int is a ring
-/
/- addition -/
@ -434,7 +430,7 @@ have H : repr (-a + a) ≡ repr 0, from
... ≡ repr 0 : padd_pneg,
eq_of_repr_equiv_repr H
/- nat -/
/- nat abs -/
definition pabs (p : ℕ × ℕ) : ℕ := dist (pr1 p) (pr2 p)
@ -595,24 +591,27 @@ have H2 : (nat_abs a) * (nat_abs b) = nat.zero, from
(nat_abs a) * (nat_abs b) = (nat_abs (a * b)) : (mul_nat_abs a b)⁻¹
... = (nat_abs 0) : {H}
... = nat.zero : nat_abs_of_nat nat.zero,
have H3 : (nat_abs a) = nat.zero ∨ (nat_abs b) = nat.zero, from eq_zero_or_eq_zero_of_mul_eq_zero H2,
have H3 : (nat_abs a) = nat.zero ∨ (nat_abs b) = nat.zero,
from eq_zero_or_eq_zero_of_mul_eq_zero H2,
or_of_or_of_imp_of_imp H3
(assume H : (nat_abs a) = nat.zero, nat_abs_eq_zero H)
(assume H : (nat_abs b) = nat.zero, nat_abs_eq_zero H)
definition integral_domain : algebra.integral_domain int :=
protected definition integral_domain : algebra.integral_domain int :=
algebra.integral_domain.mk add add.assoc zero zero_add add_zero neg add.left_inv
add.comm mul mul.assoc (of_num 1) one_mul mul_one mul.left_distrib mul.right_distrib
zero_ne_one mul.comm @eq_zero_or_eq_zero_of_mul_eq_zero
/-
Instantiate ring theorems to int
-/
--namespace algebra
-- open algebra -- TODO: why do we have to do this?
-- instance [persistent] int.integral_domain
--end algebra
-- TODO: make this "section" when scoping bug is fixed
context port_algebra
/- instantiate ring theorems to int -/
section port_algebra
open algebra
instance integral_domain
instance int.integral_domain -- TODO: why didn't the setting above persist?
theorem mul.left_comm : ∀a b c : ℤ, a * (b * c) = b * (a * c) := algebra.mul.left_comm
theorem mul.right_comm : ∀a b c : ℤ, (a * b) * c = (a * c) * b := algebra.mul.right_comm
@ -687,6 +686,7 @@ context port_algebra
definition dvd (a b : ℤ) : Prop := algebra.dvd a b
infix `|` := dvd
theorem dvd.intro : ∀{a b c : ℤ} (H : a * b = c), a | c := @algebra.dvd.intro _ _
theorem dvd.intro_right : ∀{a b c : ℤ} (H : a * b = c), b | c := @algebra.dvd.intro_right _ _
theorem dvd.ex : ∀{a b : ℤ} (H : a | b), ∃c, a * c = b := @algebra.dvd.ex _ _
theorem dvd.elim : ∀{P : Prop} {a b : ℤ} (H₁ : a | b) (H₂ : ∀c, a * c = b → P), P :=
@algebra.dvd.elim _ _
@ -741,54 +741,6 @@ context port_algebra
@algebra.dvd_of_mul_dvd_mul_left _ _
theorem dvd_of_mul_dvd_mul_right : ∀{a b c : ℤ}, a ≠ 0 → b * a | c * a → b | c :=
@algebra.dvd_of_mul_dvd_mul_right _ _
end port_algebra
-- TODO: declare appropriate rewrite rules
-- add_rewrite zero_add add_zero
-- add_rewrite add_comm add.assoc add_left_comm
-- add_rewrite sub_def add_inverse_right add_inverse_left
-- add_rewrite neg_add_distr
---- add_rewrite sub_sub_assoc sub_add_assoc add_sub_assoc
---- add_rewrite add_neg_right add_neg_left
---- add_rewrite sub_self
end int
/- tests -/
/- open int
eval -100
eval -(-100)
eval #int (5 + 7)
eval -5 + 7
eval 5 + -7
eval -5 + -7
eval #int 155 + 277
eval -155 + 277
eval 155 + -277
eval -155 + -277
eval #int 155 - 277
eval #int 277 - 155
eval #int 2 * 3
eval -2 * 3
eval 2 * -3
eval -2 * -3
eval 22 * 33
eval -22 * 33
eval 22 * -33
eval -22 * -33
eval #int 22 ≤ 33
eval #int 33 ≤ 22
example : #int 22 ≤ 33 := true.intro
example : #int -5 < 7 := true.intro
-/

586
library/data/int/order.lean
View file

@ -5,10 +5,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
Module: data.int.order
Authors: Floris van Doorn, Jeremy Avigad
The order relation on the integers, and the sign function.
The order relation on the integers. We show that int is an instance of linear_comm_ordered_ring
and transfer the results.
-/
import .basic
import .basic algebra.ordered_ring
open nat
open decidable
@ -17,7 +18,7 @@ open int eq.ops
namespace int
definition nonneg (a : ℤ) : Prop := cases_on a (take n, true) (take n, false)
private definition nonneg (a : ℤ) : Prop := cases_on a (take n, true) (take n, false)
definition le (a b : ℤ) : Prop := nonneg (sub b a)
definition lt (a b : ℤ) : Prop := le (add a 1) b
@ -26,52 +27,88 @@ infix <= := int.le
infix ≤ := int.le
infix < := int.lt
definition decidable_nonneg [instance] (a : ℤ) : decidable (nonneg a) := cases_on a _ _
private definition decidable_nonneg [instance] (a : ℤ) : decidable (nonneg a) := cases_on a _ _
definition decidable_le [instance] (a b : ℤ) : decidable (a ≤ b) := decidable_nonneg _
definition decidable_lt [instance] (a b : ℤ) : decidable (a < b) := decidable_nonneg _
theorem nonneg_elim {a : ℤ} : nonneg a → ∃n : ℕ, a = n :=
private theorem nonneg.elim {a : ℤ} : nonneg a → ∃n : ℕ, a = n :=
cases_on a (take n H, exists.intro n rfl) (take n' H, false.elim H)
theorem le_intro {a b : ℤ} {n : ℕ} (H : a + n = b) : a ≤ b :=
private theorem nonneg_or_nonneg_neg (a : ℤ) : nonneg a ∨ nonneg (-a) :=
cases_on a (take n, or.inl trivial) (take n, or.inr trivial)
theorem le.intro {a b : ℤ} {n : ℕ} (H : a + n = b) : a ≤ b :=
have H1 : b - a = n, from (eq_add_neg_of_add_eq (!add.comm ▸ H))⁻¹,
have H2 : nonneg n, from true.intro,
show nonneg (b - a), from H1⁻¹ ▸ H2
theorem le_elim {a b : ℤ} (H : a ≤ b) : ∃n : ℕ, a + n = b :=
obtain (n : ℕ) (H1 : b - a = n), from nonneg_elim H,
theorem le.elim {a b : ℤ} (H : a ≤ b) : ∃n : ℕ, a + n = b :=
obtain (n : ℕ) (H1 : b - a = n), from nonneg.elim H,
exists.intro n (!add.comm ▸ iff.mp' !add_eq_iff_eq_add_neg (H1⁻¹))
-- ### partial order
theorem le.total (a b : ℤ) : a ≤ b ∨ b ≤ a :=
or.elim (nonneg_or_nonneg_neg (b - a))
(assume H, or.inl H)
(assume H : nonneg (-(b - a)),
have H0 : -(b - a) = a - b, from neg_sub_eq b a,
have H1 : nonneg (a - b), from H0 ▸ H, -- too bad: can't do it in one step
or.inr H1)
theorem le_refl (a : ℤ) : a ≤ a :=
le_intro (add_zero a)
theorem le_of_nat (n m : ℕ) : (of_nat n ≤ of_nat m) ↔ (n ≤ m) :=
theorem of_nat_le_of_nat (n m : ℕ) : of_nat n ≤ of_nat m ↔ n ≤ m :=
iff.intro
(assume H : of_nat n ≤ of_nat m,
obtain (k : ℕ) (Hk : of_nat n + of_nat k = of_nat m), from le_elim H,
obtain (k : ℕ) (Hk : of_nat n + of_nat k = of_nat m), from le.elim H,
have H2 : n + k = m, from of_nat_inj ((add_of_nat n k)⁻¹ ⬝ Hk),
nat.le_intro H2)
(assume H : n ≤ m,
obtain (k : ℕ) (Hk : n + k = m), from nat.le_elim H,
have H2 : of_nat n + of_nat k = of_nat m, from Hk ▸ add_of_nat n k,
le_intro H2)
le.intro H2)
theorem le_trans {a b c : ℤ} (H1 : a ≤ b) (H2 : b ≤ c) : a ≤ c :=
obtain (n : ℕ) (Hn : a + n = b), from le_elim H1,
obtain (m : ℕ) (Hm : b + m = c), from le_elim H2,
theorem lt_add_succ (a : ℤ) (n : ℕ) : a < a + succ n :=
le.intro (show a + 1 + n = a + succ n, from
calc
a + 1 + n = a + (1 + n) : add.assoc
... = a + (n + 1) : add.comm
... = a + succ n : rfl)
theorem lt.intro {a b : ℤ} {n : ℕ} (H : a + succ n = b) : a < b :=
H ▸ lt_add_succ a n
theorem lt.elim {a b : ℤ} (H : a < b) : ∃n : ℕ, a + succ n = b :=
obtain (n : ℕ) (Hn : a + 1 + n = b), from le.elim H,
have H2 : a + succ n = b, from
calc
a + succ n = a + 1 + n : by simp
... = b : Hn,
exists.intro n H2
theorem of_nat_lt_of_nat (n m : ℕ) : of_nat n < of_nat m ↔ n < m :=
calc
of_nat n < of_nat m ↔ of_nat n + 1 ≤ of_nat m : iff.refl
... ↔ of_nat (succ n) ≤ of_nat m : of_nat_succ n ▸ !iff.refl
... ↔ succ n ≤ m : of_nat_le_of_nat
... ↔ n < m : iff.symm (lt_iff_succ_le _ _)
/- show that the integers form an ordered additive group -/
theorem le.refl (a : ℤ) : a ≤ a :=
le.intro (add_zero a)
theorem le.trans {a b c : ℤ} (H1 : a ≤ b) (H2 : b ≤ c) : a ≤ c :=
obtain (n : ℕ) (Hn : a + n = b), from le.elim H1,
obtain (m : ℕ) (Hm : b + m = c), from le.elim H2,
have H3 : a + of_nat (n + m) = c, from
calc
a + of_nat (n + m) = a + (of_nat n + m) : {(add_of_nat n m)⁻¹}
... = a + n + m : (add.assoc a n m)⁻¹
... = b + m : {Hn}
... = c : Hm,
le_intro H3
le.intro H3
theorem le_antisym {a b : ℤ} (H1 : a ≤ b) (H2 : b ≤ a) : a = b :=
obtain (n : ℕ) (Hn : a + n = b), from le_elim H1,
obtain (m : ℕ) (Hm : b + m = a), from le_elim H2,
theorem le.antisymm {a b : ℤ} (H1 : a ≤ b) (H2 : b ≤ a) : a = b :=
obtain (n : ℕ) (Hn : a + n = b), from le.elim H1,
obtain (m : ℕ) (Hm : b + m = a), from le.elim H2,
have H3 : a + of_nat (n + m) = a + 0, from
calc
a + of_nat (n + m) = a + (of_nat n + m) : {(add_of_nat n m)⁻¹}
@ -88,27 +125,388 @@ show a = b, from
... = a + n : {H6⁻¹}
... = b : Hn
-- ### interaction with add
theorem lt.irrefl (a : ℤ) : ¬ a < a :=
(assume H : a < a,
obtain (n : ℕ) (Hn : a + succ n = a), from lt.elim H,
have H2 : a + succ n = a + 0, from
calc
a + succ n = a : Hn
... = a + 0 : by simp,
have H3 : succ n = 0, from add.left_cancel H2,
have H4 : succ n = 0, from of_nat_inj H3,
absurd H4 !succ_ne_zero)
theorem le_add_of_nat_right (a : ℤ) (n : ℕ) : a ≤ a + n :=
le_intro (eq.refl (a + n))
theorem ne_of_lt {a b : ℤ} (H : a < b) : a ≠ b :=
(assume H2 : a = b, absurd (H2 ▸ H) (lt.irrefl b))
theorem le_add_of_nat_left (a : ℤ) (n : ℕ) : a ≤ n + a :=
le_intro (add.comm a n)
theorem succ_le_of_lt {a b : ℤ} (H : a < b) : a + 1 ≤ b := H
theorem add_le_left {a b : ℤ} (H : a ≤ b) (c : ℤ) : c + a ≤ c + b :=
obtain (n : ℕ) (Hn : a + n = b), from le_elim H,
theorem lt_of_le_succ {a b : ℤ} (H : a + 1 ≤ b) : a < b := H
theorem le_of_lt {a b : ℤ} (H : a < b) : a ≤ b :=
obtain (n : ℕ) (Hn : a + succ n = b), from lt.elim H,
le.intro Hn
theorem lt_iff_le_and_ne (a b : ℤ) : a < b ↔ (a ≤ b ∧ a ≠ b) :=
iff.intro
(assume H, and.intro (le_of_lt H) (ne_of_lt H))
(assume H,
have H1 : a ≤ b, from and.elim_left H,
have H2 : a ≠ b, from and.elim_right H,
obtain (n : ℕ) (Hn : a + n = b), from le.elim H1,
have H3 : n ≠ 0, from (assume H' : n = 0, H2 (!add_zero ▸ H' ▸ Hn)),
obtain (k : ℕ) (Hk : n = succ k), from nat.exists_eq_succ_of_ne_zero H3,
lt.intro (Hk ▸ Hn))
theorem le_iff_lt_or_eq (a b : ℤ) : a ≤ b ↔ (a < b ∨ a = b) :=
iff.intro
(assume H,
by_cases
(assume H1 : a = b, or.inr H1)
(assume H1 : a ≠ b,
obtain (n : ℕ) (Hn : a + n = b), from le.elim H,
have H2 : n ≠ 0, from (assume H' : n = 0, H1 (!add_zero ▸ H' ▸ Hn)),
obtain (k : ℕ) (Hk : n = succ k), from nat.exists_eq_succ_of_ne_zero H2,
or.inl (lt.intro (Hk ▸ Hn))))
(assume H,
or.elim H
(assume H1, le_of_lt H1)
(assume H1, H1 ▸ !le.refl))
theorem lt_succ (a : ℤ) : a < a + 1 :=
le.refl (a + 1)
theorem add_le_add_left {a b : ℤ} (H : a ≤ b) (c : ℤ) : c + a ≤ c + b :=
obtain (n : ℕ) (Hn : a + n = b), from le.elim H,
have H2 : c + a + n = c + b, from
calc
c + a + n = c + (a + n) : add.assoc c a n
... = c + b : {Hn},
le_intro H2
le.intro H2
theorem mul_nonneg {a b : ℤ} (Ha : 0 ≤ a) (Hb : 0 ≤ b) : 0 ≤ a * b :=
obtain (n : ℕ) (Hn : 0 + n = a), from le.elim Ha,
obtain (m : ℕ) (Hm : 0 + m = b), from le.elim Hb,
le.intro
(eq.symm
(calc
a * b = (0 + n) * b : Hn
... = n * b : zero_add
... = n * (0 + m) : Hm
... = n * m : zero_add
... = 0 + n * m : zero_add))
theorem mul_pos {a b : ℤ} (Ha : 0 < a) (Hb : 0 < b) : 0 < a * b :=
obtain (n : ℕ) (Hn : 0 + succ n = a), from lt.elim Ha,
obtain (m : ℕ) (Hm : 0 + succ m = b), from lt.elim Hb,
lt.intro
(eq.symm
(calc
a * b = (0 + succ n) * b : Hn
... = succ n * b : zero_add
... = succ n * (0 + succ m) : Hm
... = succ n * succ m : zero_add
... = of_nat (succ n * succ m) : mul_of_nat
... = of_nat (succ n * m + succ n) : nat.mul_succ
... = of_nat (succ (succ n * m + n)) : nat.add_succ
... = 0 + succ (succ n * m + n) : zero_add))
protected definition linear_ordered_comm_ring : algebra.linear_ordered_comm_ring int :=
algebra.linear_ordered_comm_ring.mk add add.assoc zero zero_add add_zero neg add.left_inv
add.comm mul mul.assoc (of_num 1) one_mul mul_one mul.left_distrib mul.right_distrib
zero_ne_one le le.refl @le.trans @le.antisymm lt lt_iff_le_and_ne @add_le_add_left
@mul_nonneg @mul_pos le_iff_lt_or_eq le.total mul.comm
/- instantiate ordered ring theorems to int -/
namespace algebra
open algebra
instance [persistent] int.linear_ordered_comm_ring
end algebra
section port_algebra
open algebra
instance int.linear_ordered_comm_ring
definition ge (a b : ℤ) := algebra.has_le.ge a b
definition gt (a b : ℤ) := algebra.has_lt.gt a b
infix >= := int.ge
infix ≥ := int.ge
infix > := int.gt
definition decidable_ge [instance] (a b : ℤ) : decidable (a ≥ b) := _
definition decidable_gt [instance] (a b : ℤ) : decidable (a > b) := _
theorem le_of_eq_of_le : ∀{a b c : ℤ}, a = b → b ≤ c → a ≤ c := @algebra.le_of_eq_of_le _ _
theorem le_of_le_of_eq : ∀{a b c : ℤ}, a ≤ b → b = c → a ≤ c := @algebra.le_of_le_of_eq _ _
theorem lt_of_eq_of_lt : ∀{a b c : ℤ}, a = b → b < c → a < c := @algebra.lt_of_eq_of_lt _ _
theorem lt_of_lt_of_eq : ∀{a b c : ℤ}, a < b → b = c → a < c := @algebra.lt_of_lt_of_eq _ _
calc_trans int.le_of_eq_of_le
calc_trans int.le_of_le_of_eq
calc_trans int.lt_of_eq_of_lt
calc_trans int.lt_of_lt_of_eq
theorem lt.asymm : ∀{a b : ℤ}, a < b → ¬ b < a := @algebra.lt.asymm _ _
theorem lt_of_le_of_ne : ∀{a b : ℤ}, a ≤ b → a ≠ b → a < b := @algebra.lt_of_le_of_ne _ _
theorem lt_of_lt_of_le : ∀{a b c : ℤ}, a < b → b ≤ c → a < c := @algebra.lt_of_lt_of_le _ _
theorem lt_of_le_of_lt : ∀{a b c : ℤ}, a ≤ b → b < c → a < c := @algebra.lt_of_le_of_lt _ _
theorem not_le_of_lt : ∀{a b : ℤ}, a < b → ¬ b ≤ a := @algebra.not_le_of_lt _ _
theorem not_lt_of_le : ∀{a b : ℤ}, a ≤ b → ¬ b < a := @algebra.not_lt_of_le _ _
theorem lt_or_eq_of_le : ∀{a b : ℤ}, a ≤ b → a < b ∨ a = b := @algebra.lt_or_eq_of_le _ _
theorem lt.trichotomy : ∀a b : ℤ, a < b ∨ a = b ∨ b < a := algebra.lt.trichotomy
theorem lt.by_cases : ∀{a b : ℤ} {P : Prop}, (a < b → P) → (a = b → P) → (b < a → P) → P :=
@algebra.lt.by_cases _ _
definition le_of_not_lt : ∀{a b : ℤ}, ¬ a < b → b ≤ a := @algebra.le_of_not_lt _ _
definition lt_of_not_le : ∀{a b : ℤ}, ¬ a ≤ b → b < a := @algebra.lt_of_not_le _ _
theorem add_le_add_right : ∀{a b : ℤ}, a ≤ b → ∀c : ℤ, a + c ≤ b + c :=
@algebra.add_le_add_right _ _
theorem add_le_add : ∀{a b c d : ℤ}, a ≤ b → c ≤ d → a + c ≤ b + d := @algebra.add_le_add _ _
theorem add_lt_add_left : ∀{a b : ℤ}, a < b → ∀c : ℤ, c + a < c + b :=
@algebra.add_lt_add_left _ _
theorem add_lt_add_right : ∀{a b : ℤ}, a < b → ∀c : ℤ, a + c < b + c :=
@algebra.add_lt_add_right _ _
theorem le_add_of_nonneg_right : ∀{a b : ℤ}, b ≥ 0 → a ≤ a + b :=
@algebra.le_add_of_nonneg_right _ _
theorem le_add_of_nonneg_left : ∀{a b : ℤ}, b ≥ 0 → a ≤ b + a :=
@algebra.le_add_of_nonneg_left _ _
theorem add_lt_add : ∀{a b c d : ℤ}, a < b → c < d → a + c < b + d := @algebra.add_lt_add _ _
theorem add_lt_add_of_le_of_lt : ∀{a b c d : ℤ}, a ≤ b → c < d → a + c < b + d :=
@algebra.add_lt_add_of_le_of_lt _ _
theorem add_lt_add_of_lt_of_le : ∀{a b c d : ℤ}, a < b → c ≤ d → a + c < b + d :=
@algebra.add_lt_add_of_lt_of_le _ _
theorem lt_add_of_pos_right : ∀{a b : ℤ}, b > 0 → a < a + b := @algebra.lt_add_of_pos_right _ _
theorem lt_add_of_pos_left : ∀{a b : ℤ}, b > 0 → a < b + a := @algebra.lt_add_of_pos_left _ _
theorem le_of_add_le_add_left : ∀{a b c : ℤ}, a + b ≤ a + c → b ≤ c :=
@algebra.le_of_add_le_add_left _ _
theorem le_of_add_le_add_right : ∀{a b c : ℤ}, a + b ≤ c + b → a ≤ c :=
@algebra.le_of_add_le_add_right _ _
theorem lt_of_add_lt_add_left : ∀{a b c : ℤ}, a + b < a + c → b < c :=
@algebra.lt_of_add_lt_add_left _ _
theorem lt_of_add_lt_add_right : ∀{a b c : ℤ}, a + b < c + b → a < c :=
@algebra.lt_of_add_lt_add_right _ _
theorem add_le_add_left_iff : ∀a b c : ℤ, a + b ≤ a + c ↔ b ≤ c := algebra.add_le_add_left_iff
theorem add_le_add_right_iff : ∀a b c : ℤ, a + b ≤ c + b ↔ a ≤ c := algebra.add_le_add_right_iff
theorem add_lt_add_left_iff : ∀a b c : ℤ, a + b < a + c ↔ b < c := algebra.add_lt_add_left_iff
theorem add_lt_add_right_iff : ∀a b c : ℤ, a + b < c + b ↔ a < c := algebra.add_lt_add_right_iff
theorem add_nonneg : ∀{a b : ℤ}, 0 ≤ a → 0 ≤ b → 0 ≤ a + b := @algebra.add_nonneg _ _
theorem add_pos : ∀{a b : ℤ}, 0 < a → 0 < b → 0 < a + b := @algebra.add_pos _ _
theorem add_pos_of_pos_of_nonneg : ∀{a b : ℤ}, 0 < a → 0 ≤ b → 0 < a + b :=
@algebra.add_pos_of_pos_of_nonneg _ _
theorem add_pos_of_nonneg_of_pos : ∀{a b : ℤ}, 0 ≤ a → 0 < b → 0 < a + b :=
@algebra.add_pos_of_nonneg_of_pos _ _
theorem add_nonpos : ∀{a b : ℤ}, a ≤ 0 → b ≤ 0 → a + b ≤ 0 :=
@algebra.add_nonpos _ _
theorem add_neg : ∀{a b : ℤ}, a < 0 → b < 0 → a + b < 0 :=
@algebra.add_neg _ _
theorem add_neg_of_neg_of_nonpos : ∀{a b : ℤ}, a < 0 → b ≤ 0 → a + b < 0 :=
@algebra.add_neg_of_neg_of_nonpos _ _
theorem add_neg_of_nonpos_of_neg : ∀{a b : ℤ}, a ≤ 0 → b < 0 → a + b < 0 :=
@algebra.add_neg_of_nonpos_of_neg _ _
theorem add_eq_zero_iff_eq_zero_and_eq_zero_of_nonneg_of_nonneg : ∀{a b : ℤ},
0 ≤ a → 0 ≤ b → a + b = 0 ↔ a = 0 ∧ b = 0 :=
@algebra.add_eq_zero_iff_eq_zero_and_eq_zero_of_nonneg_of_nonneg _ _
theorem le_add_of_nonneg_of_le : ∀{a b c : ℤ}, 0 ≤ a → b ≤ c → b ≤ a + c :=
@algebra.le_add_of_nonneg_of_le _ _
theorem le_add_of_le_of_nonneg : ∀{a b c : ℤ}, b ≤ c → 0 ≤ a → b ≤ c + a :=
@algebra.le_add_of_le_of_nonneg _ _
theorem lt_add_of_pos_of_le : ∀{a b c : ℤ}, 0 < a → b ≤ c → b < a + c :=
@algebra.lt_add_of_pos_of_le _ _
theorem lt_add_of_le_of_pos : ∀{a b c : ℤ}, b ≤ c → 0 < a → b < c + a :=
@algebra.lt_add_of_le_of_pos _ _
theorem add_le_of_nonpos_of_le : ∀{a b c : ℤ}, a ≤ 0 → b ≤ c → a + b ≤ c :=
@algebra.add_le_of_nonpos_of_le _ _
theorem add_le_of_le_of_nonpos : ∀{a b c : ℤ}, b ≤ c → a ≤ 0 → b + a ≤ c :=
@algebra.add_le_of_le_of_nonpos _ _
theorem add_lt_of_neg_of_le : ∀{a b c : ℤ}, a < 0 → b ≤ c → a + b < c :=
@algebra.add_lt_of_neg_of_le _ _
theorem add_lt_of_le_of_neg : ∀{a b c : ℤ}, b ≤ c → a < 0 → b + a < c :=
@algebra.add_lt_of_le_of_neg _ _
theorem lt_add_of_nonneg_of_lt : ∀{a b c : ℤ}, 0 ≤ a → b < c → b < a + c :=
@algebra.lt_add_of_nonneg_of_lt _ _
theorem lt_add_of_lt_of_nonneg : ∀{a b c : ℤ}, b < c → 0 ≤ a → b < c + a :=
@algebra.lt_add_of_lt_of_nonneg _ _
theorem lt_add_of_pos_of_lt : ∀{a b c : ℤ}, 0 < a → b < c → b < a + c :=
@algebra.lt_add_of_pos_of_lt _ _
theorem lt_add_of_lt_of_pos : ∀{a b c : ℤ}, b < c → 0 < a → b < c + a :=
@algebra.lt_add_of_lt_of_pos _ _
theorem add_lt_of_nonpos_of_lt : ∀{a b c : ℤ}, a ≤ 0 → b < c → a + b < c :=
@algebra.add_lt_of_nonpos_of_lt _ _
theorem add_lt_of_lt_of_nonpos : ∀{a b c : ℤ}, b < c → a ≤ 0 → b + a < c :=
@algebra.add_lt_of_lt_of_nonpos _ _
theorem add_lt_of_neg_of_lt : ∀{a b c : ℤ}, a < 0 → b < c → a + b < c :=
@algebra.add_lt_of_neg_of_lt _ _
theorem add_lt_of_lt_of_neg : ∀{a b c : ℤ}, b < c → a < 0 → b + a < c :=
@algebra.add_lt_of_lt_of_neg _ _
theorem neg_le_neg : ∀{a b : ℤ}, a ≤ b → -b ≤ -a := @algebra.neg_le_neg _ _
theorem neg_le_neg_iff_le : ∀a b : ℤ, -a ≤ -b ↔ b ≤ a := algebra.neg_le_neg_iff_le
theorem neg_nonpos_iff_nonneg : ∀a : ℤ, -a ≤ 0 ↔ 0 ≤ a := algebra.neg_nonpos_iff_nonneg
theorem neg_nonneg_iff_nonpos : ∀a : ℤ, 0 ≤ -a ↔ a ≤ 0 := algebra.neg_nonneg_iff_nonpos
theorem neg_lt_neg : ∀{a b : ℤ}, a < b → -b < -a := @algebra.neg_lt_neg _ _
theorem neg_lt_neg_iff_lt : ∀a b : ℤ, -a < -b ↔ b < a := algebra.neg_lt_neg_iff_lt
theorem neg_neg_iff_pos : ∀a : ℤ, -a < 0 ↔ 0 < a := algebra.neg_neg_iff_pos
theorem neg_pos_iff_neg : ∀a : ℤ, 0 < -a ↔ a < 0 := algebra.neg_pos_iff_neg
theorem le_neg_iff_le_neg : ∀a b : ℤ, a ≤ -b ↔ b ≤ -a := algebra.le_neg_iff_le_neg
theorem neg_le_iff_neg_le : ∀a b : ℤ, -a ≤ b ↔ -b ≤ a := algebra.neg_le_iff_neg_le
theorem lt_neg_iff_lt_neg : ∀a b : ℤ, a < -b ↔ b < -a := algebra.lt_neg_iff_lt_neg
theorem neg_lt_iff_neg_lt : ∀a b : ℤ, -a < b ↔ -b < a := algebra.neg_lt_iff_neg_lt
theorem sub_nonneg_iff_le : ∀a b : ℤ, 0 ≤ a - b ↔ b ≤ a := algebra.sub_nonneg_iff_le
theorem sub_nonpos_iff_le : ∀a b : ℤ, a - b ≤ 0 ↔ a ≤ b := algebra.sub_nonpos_iff_le
theorem sub_pos_iff_lt : ∀a b : ℤ, 0 < a - b ↔ b < a := algebra.sub_pos_iff_lt
theorem sub_neg_iff_lt : ∀a b : ℤ, a - b < 0 ↔ a < b := algebra.sub_neg_iff_lt
theorem add_le_iff_le_neg_add : ∀a b c : ℤ, a + b ≤ c ↔ b ≤ -a + c :=
algebra.add_le_iff_le_neg_add
theorem add_le_iff_le_sub_left : ∀a b c : ℤ, a + b ≤ c ↔ b ≤ c - a :=
algebra.add_le_iff_le_sub_left
theorem add_le_iff_le_sub_right : ∀a b c : ℤ, a + b ≤ c ↔ a ≤ c - b :=
algebra.add_le_iff_le_sub_right
theorem le_add_iff_neg_add_le : ∀a b c : ℤ, a ≤ b + c ↔ -b + a ≤ c :=
algebra.le_add_iff_neg_add_le
theorem le_add_iff_sub_left_le : ∀a b c : ℤ, a ≤ b + c ↔ a - b ≤ c :=
algebra.le_add_iff_sub_left_le
theorem le_add_iff_sub_right_le : ∀a b c : ℤ, a ≤ b + c ↔ a - c ≤ b :=
algebra.le_add_iff_sub_right_le
theorem add_lt_iff_lt_neg_add_left : ∀a b c : ℤ, a + b < c ↔ b < -a + c :=
algebra.add_lt_iff_lt_neg_add_left
theorem add_lt_iff_lt_neg_add_right : ∀a b c : ℤ, a + b < c ↔ a < -b + c :=
algebra.add_lt_iff_lt_neg_add_right
theorem add_lt_iff_lt_sub_left : ∀a b c : ℤ, a + b < c ↔ b < c - a :=
algebra.add_lt_iff_lt_sub_left
theorem add_lt_add_iff_lt_sub_right : ∀a b c : ℤ, a + b < c ↔ a < c - b :=
algebra.add_lt_add_iff_lt_sub_right
theorem lt_add_iff_neg_add_lt_left : ∀a b c : ℤ, a < b + c ↔ -b + a < c :=
algebra.lt_add_iff_neg_add_lt_left
theorem lt_add_iff_neg_add_lt_right : ∀a b c : ℤ, a < b + c ↔ -c + a < b :=
algebra.lt_add_iff_neg_add_lt_right
theorem lt_add_iff_sub_lt_left : ∀a b c : ℤ, a < b + c ↔ a - b < c :=
algebra.lt_add_iff_sub_lt_left
theorem lt_add_iff_sub_lt_right : ∀a b c : ℤ, a < b + c ↔ a - c < b :=
algebra.lt_add_iff_sub_lt_right
theorem le_iff_le_of_sub_eq_sub : ∀{a b c d : ℤ}, a - b = c - d → a ≤ b ↔ c ≤ d :=
@algebra.le_iff_le_of_sub_eq_sub _ _
theorem lt_iff_lt_of_sub_eq_sub : ∀{a b c d : ℤ}, a - b = c - d → a < b ↔ c < d :=
@algebra.lt_iff_lt_of_sub_eq_sub _ _
theorem sub_le_sub_left : ∀{a b : ℤ}, a ≤ b → ∀c : ℤ, c - b ≤ c - a :=
@algebra.sub_le_sub_left _ _
theorem sub_le_sub_right : ∀{a b : ℤ}, a ≤ b → ∀c : ℤ, a - c ≤ b - c :=
@algebra.sub_le_sub_right _ _
theorem sub_le_sub : ∀{a b c d : ℤ}, a ≤ b → c ≤ d → a - d ≤ b - c :=
@algebra.sub_le_sub _ _
theorem sub_lt_sub_left : ∀{a b : ℤ}, a < b → ∀c : ℤ, c - b < c - a :=
@algebra.sub_lt_sub_left _ _
theorem sub_lt_sub_right : ∀{a b : ℤ}, a < b → ∀c : ℤ, a - c < b - c :=
@algebra.sub_lt_sub_right _ _
theorem sub_lt_sub : ∀{a b c d : ℤ}, a < b → c < d → a - d < b - c :=
@algebra.sub_lt_sub _ _
theorem sub_lt_sub_of_le_of_lt : ∀{a b c d : ℤ}, a ≤ b → c < d → a - d < b - c :=
@algebra.sub_lt_sub_of_le_of_lt _ _
theorem sub_lt_sub_of_lt_of_le : ∀{a b c d : ℤ}, a < b → c ≤ d → a - d < b - c :=
@algebra.sub_lt_sub_of_lt_of_le _ _
theorem mul_le_mul_of_nonneg_left : ∀{a b c : ℤ}, a ≤ b → 0 ≤ c → c * a ≤ c * b :=
@algebra.mul_le_mul_of_nonneg_left _ _
theorem mul_le_mul_of_nonneg_right : ∀{a b c : ℤ}, a ≤ b → 0 ≤ c → a * c ≤ b * c :=
@algebra.mul_le_mul_of_nonneg_right _ _
theorem mul_le_mul : ∀{a b c d : ℤ}, a ≤ c → b ≤ d → 0 ≤ b → 0 ≤ c → a * b ≤ c * d :=
@algebra.mul_le_mul _ _
theorem mul_nonpos_of_nonneg_of_nonpos : ∀{a b : ℤ}, a ≥ 0 → b ≤ 0 → a * b ≤ 0 :=
@algebra.mul_nonpos_of_nonneg_of_nonpos _ _
theorem mul_nonpos_of_nonpos_of_nonneg : ∀{a b : ℤ}, a ≤ 0 → b ≥ 0 → a * b ≤ 0 :=
@algebra.mul_nonpos_of_nonpos_of_nonneg _ _
theorem mul_lt_mul_of_pos_left : ∀{a b c : ℤ}, a < b → 0 < c → c * a < c * b :=
@algebra.mul_lt_mul_of_pos_left _ _
theorem mul_lt_mul_of_pos_right : ∀{a b c : ℤ}, a < b → 0 < c → a * c < b * c :=
@algebra.mul_lt_mul_of_pos_right _ _
theorem mul_lt_mul : ∀{a b c d : ℤ}, a < c → b ≤ d → 0 < b → 0 ≤ c → a * b < c * d :=
@algebra.mul_lt_mul _ _
theorem mul_neg_of_pos_of_neg : ∀{a b : ℤ}, a > 0 → b < 0 → a * b < 0 :=
@algebra.mul_neg_of_pos_of_neg _ _
theorem mul_neg_of_neg_of_pos : ∀{a b : ℤ}, a < 0 → b > 0 → a * b < 0 :=
@algebra.mul_neg_of_neg_of_pos _ _
theorem lt_of_mul_lt_mul_left : ∀{a b c : ℤ}, c * a < c * b → c ≥ zero → a < b :=
@algebra.lt_of_mul_lt_mul_left int _
theorem lt_of_mul_lt_mul_right : ∀{a b c : ℤ}, a * c < b * c → c ≥ 0 → a < b :=
@algebra.lt_of_mul_lt_mul_right _ _
theorem le_of_mul_le_mul_left : ∀{a b c : ℤ}, c * a ≤ c * b → c > 0 → a ≤ b :=
@algebra.le_of_mul_le_mul_left _ _
theorem le_of_mul_le_mul_right : ∀{a b c : ℤ}, a * c ≤ b * c → c > 0 → a ≤ b :=
@algebra.le_of_mul_le_mul_right _ _
theorem pos_of_mul_pos_left : ∀{a b : ℤ}, 0 < a * b → 0 ≤ a → 0 < b :=
@algebra.pos_of_mul_pos_left _ _
theorem pos_of_mul_pos_right : ∀{a b : ℤ}, 0 < a * b → 0 ≤ b → 0 < a :=
@algebra.pos_of_mul_pos_right _ _
theorem mul_le_mul_of_nonpos_left : ∀{a b c : ℤ}, b ≤ a → c ≤ 0 → c * a ≤ c * b :=
@algebra.mul_le_mul_of_nonpos_left _ _
theorem mul_le_mul_of_nonpos_right : ∀{a b c : ℤ}, b ≤ a → c ≤ 0 → a * c ≤ b * c :=
@algebra.mul_le_mul_of_nonpos_right _ _
theorem mul_nonneg_of_nonpos_of_nonpos : ∀{a b : ℤ}, a ≤ 0 → b ≤ 0 → 0 ≤ a * b :=
@algebra.mul_nonneg_of_nonpos_of_nonpos _ _
theorem mul_lt_mul_of_neg_left : ∀{a b c : ℤ}, b < a → c < 0 → c * a < c * b :=
@algebra.mul_lt_mul_of_neg_left _ _
theorem mul_lt_mul_of_neg_right : ∀{a b c : ℤ}, b < a → c < 0 → a * c < b * c :=
@algebra.mul_lt_mul_of_neg_right _ _
theorem mul_pos_of_neg_of_neg : ∀{a b : ℤ}, a < 0 → b < 0 → 0 < a * b :=
@algebra.mul_pos_of_neg_of_neg _ _
theorem mul_self_nonneg : ∀a : ℤ, a * a ≥ 0 := algebra.mul_self_nonneg
theorem zero_le_one : #int 0 ≤ 1 := @algebra.zero_le_one int int.linear_ordered_comm_ring
theorem zero_lt_one : #int 0 < 1 := @algebra.zero_lt_one int int.linear_ordered_comm_ring
theorem pos_and_pos_or_neg_and_neg_of_mul_pos : ∀{a b : ℤ}, a * b > 0 →
(a > 0 ∧ b > 0) ∨ (a < 0 ∧ b < 0) := @algebra.pos_and_pos_or_neg_and_neg_of_mul_pos _ _
end port_algebra
/- more facts specific to int -/
theorem nonneg_of_nat (n : ℕ) : 0 ≤ of_nat n := trivial
theorem exists_eq_of_nat {a : ℤ} (H : 0 ≤ a) : ∃n : ℕ, a = of_nat n :=
obtain (n : ℕ) (H1 : 0 + of_nat n = a), from le.elim H,
exists.intro n (!zero_add ▸ (H1⁻¹))
theorem exists_eq_neg_of_nat {a : ℤ} (H : a ≤ 0) : ∃n : ℕ, a = -(of_nat n) :=
have H2 : -a ≥ 0, from iff.mp' !neg_nonneg_iff_nonpos H,
obtain (n : ℕ) (Hn : -a = of_nat n), from exists_eq_of_nat H2,
exists.intro n (eq_neg_of_eq_neg (Hn⁻¹))
theorem of_nat_nat_abs_of_nonneg {a : ℤ} (H : a ≥ 0) : of_nat (nat_abs a) = a :=
obtain (n : ℕ) (Hn : a = of_nat n), from exists_eq_of_nat H,
Hn⁻¹ ▸ congr_arg of_nat (nat_abs_of_nat n)
theorem of_nat_nat_abs_of_nonpos {a : ℤ} (H : a ≤ 0) : of_nat (nat_abs a) = -a :=
have H1 : (-a) ≥ 0, from iff.mp' !neg_nonneg_iff_nonpos H,
calc
of_nat (nat_abs a) = of_nat (nat_abs (-a)) : nat_abs_neg
... = -a : of_nat_nat_abs_of_nonneg H1
exit
-- ### interaction with add
theorem le_add_of_nat_right (a : ℤ) (n : ℕ) : a ≤ a + n :=
le.intro (eq.refl (a + n))
theorem le_add_of_nat_left (a : ℤ) (n : ℕ) : a ≤ n + a :=
le.intro (add.comm a n)
theorem add_le_right {a b : ℤ} (H : a ≤ b) (c : ℤ) : a + c ≤ b + c :=
add.comm c b ▸ add.comm c a ▸ add_le_left H c
add.comm c b ▸ add.comm c a ▸ add_le_add_left H c
theorem add_le {a b c d : ℤ} (H1 : a ≤ b) (H2 : c ≤ d) : a + c ≤ b + d :=
le_trans (add_le_right H1 c) (add_le_left H2 b)
le_trans (add_le_right H1 c) (add_le_add_left H2 b)
theorem add_le_cancel_right {a b c : ℤ} (H : a + c ≤ b + c) : a ≤ b :=
have H1 : a + c + -c ≤ b + c + -c, from add_le_right H (-c),
@ -118,7 +516,7 @@ theorem add_le_cancel_left {a b c : ℤ} (H : c + a ≤ c + b) : a ≤ b :=
add_le_cancel_right (add.comm c b ▸ add.comm c a ▸ H)
theorem add_le_inv {a b c d : ℤ} (H1 : a + b ≤ c + d) (H2 : c ≤ a) : b ≤ d :=
obtain (n : ℕ) (Hn : c + n = a), from le_elim H2,
obtain (n : ℕ) (Hn : c + n = a), from le.elim H2,
have H3 : c + (n + b) ≤ c + d, from add.assoc c n b ▸ Hn⁻¹ ▸ H1,
have H4 : n + b ≤ d, from add_le_cancel_left H3,
show b ≤ d, from le_trans (le_add_of_nat_left b n) H4
@ -127,7 +525,7 @@ theorem le_add_of_nat_right_trans {a b : ℤ} (H : a ≤ b) (n : ℕ) : a ≤ b
le_trans H (le_add_of_nat_right b n)
theorem le_imp_succ_le_or_eq {a b : ℤ} (H : a ≤ b) : a + 1 ≤ b ∨ a = b :=
obtain (n : ℕ) (Hn : a + n = b), from le_elim H,
obtain (n : ℕ) (Hn : a + n = b), from le.elim H,
discriminate
(assume H2 : n = 0,
have H3 : a = b, from
@ -143,19 +541,19 @@ discriminate
a + 1 + k = a + succ k : by simp
... = a + n : by simp
... = b : Hn,
or.inl (le_intro H3))
or.inl (le.intro H3))
-- ### interaction with neg and sub
theorem le_neg {a b : ℤ} (H : a ≤ b) : -b ≤ -a :=
obtain (n : ℕ) (Hn : a + n = b), from le_elim H,
obtain (n : ℕ) (Hn : a + n = b), from le.elim H,
have H2 : b - n = a, from (iff.mp !add_eq_iff_eq_add_neg Hn)⁻¹,
have H3 : -b + n = -a, from
calc
-b + n = -b + -(-n) : {(neg_neg n)⁻¹}
... = -(b + -n) : (neg_add_distrib b (-n))⁻¹
... = -a : {H2},
le_intro H3
le.intro H3
theorem neg_le_zero {a : ℤ} (H : 0 ≤ a) : -a ≤ 0 :=
neg_zero ▸ (le_neg H)
@ -167,13 +565,13 @@ theorem le_neg_inv {a b : ℤ} (H : -a ≤ -b) : b ≤ a :=
neg_neg b ▸ neg_neg a ▸ le_neg H
theorem le_sub_of_nat (a : ℤ) (n : ℕ) : a - n ≤ a :=
le_intro (neg_add_cancel_right a n)
le.intro (neg_add_cancel_right a n)
theorem sub_le_right {a b : ℤ} (H : a ≤ b) (c : ℤ) : a - c ≤ b - c :=
add_le_right H _
theorem sub_le_left {a b : ℤ} (H : a ≤ b) (c : ℤ) : c - b ≤ c - a :=
add_le_left (le_neg H) _
add_le_add_left (le_neg H) _
theorem sub_le {a b c d : ℤ} (H1 : a ≤ b) (H2 : d ≤ c) : a - c ≤ b - d :=
add_le H1 (le_neg H2)
@ -213,59 +611,14 @@ iff.refl (n ≥ m)
-- add_rewrite gt_def ge_def --it might be possible to remove this in Lean 0.2
theorem lt_add_succ (a : ℤ) (n : ℕ) : a < a + succ n :=
le_intro (show a + 1 + n = a + succ n, by simp)
theorem lt_intro {a b : ℤ} {n : ℕ} (H : a + succ n = b) : a < b :=
H ▸ lt_add_succ a n
theorem lt_elim {a b : ℤ} (H : a < b) : ∃n : ℕ, a + succ n = b :=
obtain (n : ℕ) (Hn : a + 1 + n = b), from le_elim H,
have H2 : a + succ n = b, from
calc
a + succ n = a + 1 + n : by simp
... = b : Hn,
exists.intro n H2
-- -- ### basic facts
theorem lt_irrefl (a : ℤ) : ¬ a < a :=
(assume H : a < a,
obtain (n : ℕ) (Hn : a + succ n = a), from lt_elim H,
have H2 : a + succ n = a + 0, from
calc
a + succ n = a : Hn
... = a + 0 : by simp,
have H3 : succ n = 0, from add.left_cancel H2,
have H4 : succ n = 0, from of_nat_inj H3,
absurd H4 !succ_ne_zero)
theorem lt_imp_ne {a b : ℤ} (H : a < b) : a ≠ b :=
(assume H2 : a = b, absurd (H2 ▸ H) (lt_irrefl b))
theorem lt_of_nat (n m : ℕ) : (of_nat n < of_nat m) ↔ (n < m) :=
calc
(of_nat n + 1 ≤ of_nat m) ↔ (of_nat (succ n) ≤ of_nat m) : by simp
... ↔ (succ n ≤ m) : le_of_nat (succ n) m
... ↔ (n < m) : iff.symm (nat.lt_def n m)
theorem gt_of_nat (n m : ℕ) : (of_nat n > of_nat m) ↔ (n > m) :=
lt_of_nat m n
of_nat_lt_of_nat m n
-- ### interaction with le
theorem lt_imp_le_succ {a b : ℤ} (H : a < b) : a + 1 ≤ b :=
H
theorem le_succ_imp_lt {a b : ℤ} (H : a + 1 ≤ b) : a < b :=
H
theorem self_lt_succ (a : ℤ) : a < a + 1 :=
le_refl (a + 1)
theorem lt_imp_le {a b : ℤ} (H : a < b) : a ≤ b :=
obtain (n : ℕ) (Hn : a + succ n = b), from lt_elim H,
le_intro Hn
theorem le_imp_lt_or_eq {a b : ℤ} (H : a ≤ b) : a < b ∨ a = b :=
le_imp_succ_le_or_eq H
@ -289,22 +642,22 @@ theorem le_lt_trans {a b c : ℤ} (H1 : a ≤ b) (H2 : b < c) : a < c :=
le_trans (add_le_right H1 1) H2
theorem lt_trans {a b c : ℤ} (H1 : a < b) (H2 : b < c) : a < c :=
lt_le_trans H1 (lt_imp_le H2)
lt_le_trans H1 (le_of_lt H2)
theorem le_imp_not_gt {a b : ℤ} (H : a ≤ b) : ¬ a > b :=
(assume H2 : a > b, absurd (le_lt_trans H H2) (lt_irrefl a))
(assume H2 : a > b, absurd (le_lt_trans H H2) (lt.irrefl a))
theorem lt_imp_not_ge {a b : ℤ} (H : a < b) : ¬ a ≥ b :=
(assume H2 : a ≥ b, absurd (lt_le_trans H H2) (lt_irrefl a))
(assume H2 : a ≥ b, absurd (lt_le_trans H H2) (lt.irrefl a))
theorem lt_antisym {a b : ℤ} (H : a < b) : ¬ b < a :=
le_imp_not_gt (lt_imp_le H)
le_imp_not_gt (le_of_lt H)
-- ### interaction with addition
-- TODO: note: no longer works without the "show"
theorem add_lt_left {a b : ℤ} (H : a < b) (c : ℤ) : c + a < c + b :=
show (c + a) + 1 ≤ c + b, from (add.assoc c a 1)⁻¹ ▸ add_le_left H c
show (c + a) + 1 ≤ c + b, from (add.assoc c a 1)⁻¹ ▸ add_le_add_left H c
theorem add_lt_right {a b : ℤ} (H : a < b) (c : ℤ) : a + c < b + c :=
add.comm c b ▸ add.comm c a ▸ add_lt_left H c
@ -313,10 +666,10 @@ theorem add_le_lt {a b c d : ℤ} (H1 : a ≤ c) (H2 : b < d) : a + b < c + d :=
le_lt_trans (add_le_right H1 b) (add_lt_left H2 c)
theorem add_lt_le {a b c d : ℤ} (H1 : a < c) (H2 : b ≤ d) : a + b < c + d :=
lt_le_trans (add_lt_right H1 b) (add_le_left H2 c)
lt_le_trans (add_lt_right H1 b) (add_le_add_left H2 c)
theorem add_lt {a b c d : ℤ} (H1 : a < c) (H2 : b < d) : a + b < c + d :=
add_lt_le H1 (lt_imp_le H2)
add_lt_le H1 (le_of_lt H2)
theorem add_lt_cancel_left {a b c : ℤ} (H : c + a < c + b) : a < b :=
show a + 1 ≤ b, from add_le_cancel_left (add.assoc c a 1 ▸ H)
@ -342,7 +695,7 @@ theorem lt_neg_inv {a b : ℤ} (H : -a < -b) : b < a :=
neg_neg b ▸ neg_neg a ▸ lt_neg H
theorem lt_sub_of_nat_succ (a : ℤ) (n : ℕ) : a - succ n < a :=
lt_intro (neg_add_cancel_right a (succ n))
lt.intro (neg_add_cancel_right a (succ n))
theorem sub_lt_right {a b : ℤ} (H : a < b) (c : ℤ) : a - c < b - c :=
add_lt_right H _
@ -375,10 +728,15 @@ by_cases_of_nat a
(take n : ℕ,
by_cases_of_nat_succ b
(take m : ℕ,
show of_nat n ≤ m ∨ of_nat n > m, by simp) -- from (by simp) ◂ (le_or_gt n m))
show of_nat n ≤ m ∨ of_nat n > m, from
proof
or.elim (@nat.le_or_gt n m)
(assume H : n ≤ m, or.inl (iff.mp' !of_nat_le_of_nat H))
(assume H : n > m, or.inr (iff.mp' !of_nat_lt_of_nat H))
qed)
(take m : ℕ,
show n ≤ -succ m ∨ n > -succ m, from
have H0 : -succ m < -m, from lt_neg ((of_nat_succ m)⁻¹ ▸ self_lt_succ m),
have H0 : -succ m < -m, from lt_neg ((of_nat_succ m)⁻¹ ▸ lt_succ m),
have H : -succ m < n, from lt_le_trans H0 (neg_le_pos m n),
or.inr H))
(take n : ℕ,
@ -390,9 +748,9 @@ by_cases_of_nat a
show -n ≤ -succ m ∨ -n > -succ m, from
or_of_or_of_imp_of_imp le_or_gt
(assume H : succ m ≤ n,
le_neg (iff.elim_left (iff.symm (le_of_nat (succ m) n)) H))
le_neg (iff.elim_left (iff.symm (of_nat_le_of_nat (succ m) n)) H))
(assume H : succ m > n,
lt_neg (iff.elim_left (iff.symm (lt_of_nat n (succ m))) H))))
lt_neg (iff.elim_left (iff.symm (of_nat_lt_of_nat n (succ m))) H))))
theorem trichotomy_alt (a b : ℤ) : (a < b ∨ a = b) ∨ a > b :=
or_of_or_of_imp_left (le_or_gt a b) (assume H : a ≤ b, le_imp_lt_or_eq H)
@ -401,9 +759,9 @@ theorem trichotomy (a b : ℤ) : a < b ∨ a = b ∨ a > b :=
iff.elim_left or.assoc (trichotomy_alt a b)
theorem le_total (a b : ℤ) : a ≤ b ∨ b ≤ a :=
or_of_or_of_imp_right (le_or_gt a b) (assume H : b < a, lt_imp_le H)
or_of_or_of_imp_right (le_or_gt a b) (assume H : b < a, le_of_lt H)
theorem not_lt_imp_le {a b : ℤ} (H : ¬ a < b) : b ≤ a :=
theorem not_le_of_lt {a b : ℤ} (H : ¬ a < b) : b ≤ a :=
or_resolve_left (le_or_gt b a) H
theorem not_le_imp_lt {a b : ℤ} (H : ¬ a ≤ b) : b < a :=
@ -417,7 +775,7 @@ or_resolve_right (le_or_gt a b) H
-- see also "int_by_cases" and similar theorems
theorem pos_imp_exists_nat {a : ℤ} (H : a ≥ 0) : ∃n : ℕ, a = n :=
obtain (n : ℕ) (Hn : of_nat 0 + n = a), from le_elim H,
obtain (n : ℕ) (Hn : of_nat 0 + n = a), from le.elim H,
exists.intro n (Hn⁻¹ ⬝ zero_add n)
theorem neg_imp_exists_nat {a : ℤ} (H : a ≤ 0) : ∃n : ℕ, a = -n :=
@ -431,7 +789,7 @@ obtain (n : ℕ) (Hn : a = n), from pos_imp_exists_nat H,
Hn⁻¹ ▸ congr_arg of_nat (nat_abs_of_nat n)
theorem of_nat_nonneg (n : ℕ) : of_nat n ≥ 0 :=
iff.mp (iff.symm !le_of_nat) !zero_le
iff.mp (iff.symm !of_nat_le_of_nat) !zero_le
definition ge_decidable [instance] {a b : ℤ} : decidable (a ≥ b) := _
definition lt_decidable [instance] {a b : ℤ} : decidable (a < b) := _
@ -454,14 +812,14 @@ or_of_or_of_imp_of_imp (le_total 0 a)
-- ### interaction of mul with le and lt
theorem mul_le_left_nonneg {a b c : ℤ} (Ha : a ≥ 0) (H : b ≤ c) : a * b ≤ a * c :=
obtain (n : ℕ) (Hn : b + n = c), from le_elim H,
obtain (n : ℕ) (Hn : b + n = c), from le.elim H,
have H2 : a * b + of_nat ((nat_abs a) * n) = a * c, from
calc
a * b + of_nat ((nat_abs a) * n) = a * b + (nat_abs a) * of_nat n : by simp
... = a * b + a * n : {nat_abs_nonneg_eq Ha}
... = a * (b + n) : by simp
... = a * c : by simp,
le_intro H2
le.intro H2
theorem mul_le_right_nonneg {a b c : ℤ} (Hb : b ≥ 0) (H : a ≤ c) : a * b ≤ c * b :=
!mul.comm ▸ !mul.comm ▸ mul_le_left_nonneg Hb H
@ -479,13 +837,13 @@ theorem mul_le_nonneg {a b c d : ℤ} (Ha : a ≥ 0) (Hb : b ≥ 0) (Hc : a ≤
: a * b ≤ c * d :=
le_trans (mul_le_right_nonneg Hb Hc) (mul_le_left_nonneg (le_trans Ha Hc) Hd)
theorem mul_le_nonpos {a b c d : ℤ} (Ha : a ≤ 0) (Hb : b ≤ 0) (Hc : c ≤ a) (Hd : d ≤ b)
theorem mul_le_nonpos {a b c d : ℤ} (Ha : a ≤ 0) (Hb :b ≤ 0) (Hc : c ≤ a) (Hd : d ≤ b)
: a * b ≤ c * d :=
le_trans (mul_le_right_nonpos Hb Hc) (mul_le_left_nonpos (le_trans Hc Ha) Hd)
theorem mul_lt_left_pos {a b c : ℤ} (Ha : a > 0) (H : b < c) : a * b < a * c :=
have H2 : a * b < a * b + a, from add_zero (a * b) ▸ add_lt_left Ha (a * b),
have H3 : a * b + a ≤ a * c, from (by simp) ▸ mul_le_left_nonneg (lt_imp_le Ha) H,
have H3 : a * b + a ≤ a * c, from (by simp) ▸ mul_le_left_nonneg (le_of_lt Ha) H,
lt_le_trans H2 H3
theorem mul_lt_right_pos {a b c : ℤ} (Hb : b > 0) (H : a < c) : a * b < c * b :=
@ -505,11 +863,11 @@ le_lt_trans (mul_le_right_nonneg Hb Hc) (mul_lt_left_pos (lt_le_trans Ha Hc) Hd)
theorem mul_lt_le_pos {a b c d : ℤ} (Ha : a ≥ 0) (Hb : b > 0) (Hc : a < c) (Hd : b ≤ d)
: a * b < c * d :=
lt_le_trans (mul_lt_right_pos Hb Hc) (mul_le_left_nonneg (le_trans Ha (lt_imp_le Hc)) Hd)
lt_le_trans (mul_lt_right_pos Hb Hc) (mul_le_left_nonneg (le_trans Ha (le_of_lt Hc)) Hd)
theorem mul_lt_pos {a b c d : ℤ} (Ha : a > 0) (Hb : b > 0) (Hc : a < c) (Hd : b < d)
: a * b < c * d :=
mul_lt_le_pos (lt_imp_le Ha) Hb Hc (lt_imp_le Hd)
mul_lt_le_pos (le_of_lt Ha) Hb Hc (le_of_lt Hd)
theorem mul_lt_neg {a b c d : ℤ} (Ha : a < 0) (Hb : b < 0) (Hc : c < a) (Hd : d < b)
: a * b < c * d :=
@ -583,13 +941,13 @@ theorem sign_negative {a : ℤ} (H : a < 0) : sign a = - 1 :=
if_neg (lt_antisym H) ⬝ if_pos H
theorem sign_zero : sign 0 = 0 :=
if_neg (lt_irrefl 0) ⬝ if_neg (lt_irrefl 0)
if_neg (lt.irrefl 0) ⬝ if_neg (lt.irrefl 0)
-- add_rewrite sign_negative sign_pos nat_abs_negative nat_abs_nonneg_eq sign_zero mul_nat_abs
theorem mul_sign_nat_abs (a : ℤ) : sign a * (nat_abs a) = a :=
have temp1 : ∀a : ℤ, a < 0 → a ≤ 0, from take a, lt_imp_le,
have temp2 : ∀a : ℤ, a > 0 → a ≥ 0, from take a, lt_imp_le,
have temp1 : ∀a : ℤ, a < 0 → a ≤ 0, from take a, le_of_lt,
have temp2 : ∀a : ℤ, a > 0 → a ≥ 0, from take a, le_of_lt,
or.elim3 (trichotomy a 0)
(assume H : a < 0, by simp)
(assume H : a = 0, by simp)
@ -615,7 +973,7 @@ or.elim (em (a = 0))
mul.cancel_right H3 H))
theorem sign_idempotent (a : ℤ) : sign (sign a) = sign a :=
have temp : of_nat 1 > 0, from iff.elim_left (iff.symm (lt_of_nat 0 1)) !succ_pos,
have temp : of_nat 1 > 0, from iff.elim_left (iff.symm (of_nat_lt_of_nat 0 1)) !succ_pos,
--this should be done with simp
or.elim3 (trichotomy a 0) sorry sorry sorry
-- (by simp)
@ -623,7 +981,7 @@ or.elim3 (trichotomy a 0) sorry sorry sorry
-- (by simp)
theorem sign_succ (n : ℕ) : sign (succ n) = 1 :=
sign_pos (iff.elim_left (iff.symm (lt_of_nat 0 (succ n))) !succ_pos)
sign_pos (iff.elim_left (iff.symm (of_nat_lt_of_nat 0 (succ n))) !succ_pos)
--this should be done with simp
theorem sign_neg (a : ℤ) : sign (-a) = - sign a :=
@ -644,8 +1002,8 @@ or.elim3 (trichotomy a 0) sorry
-- (by simp)
theorem sign_nat_abs (a : ℤ) : sign (nat_abs a) = nat_abs (sign a) :=
have temp1 : ∀a : ℤ, a < 0 → a ≤ 0, from take a, lt_imp_le,
have temp2 : ∀a : ℤ, a > 0 → a ≥ 0, from take a, lt_imp_le,
have temp1 : ∀a : ℤ, a < 0 → a ≤ 0, from take a, le_of_lt,
have temp2 : ∀a : ℤ, a > 0 → a ≥ 0, from take a, le_of_lt,
or.elim3 (trichotomy a 0) sorry sorry sorry
-- (by simp)
-- (by simp)

3
library/data/nat/basic.lean
View file

@ -65,6 +65,9 @@ induction_on n
(take m IH, or.inr
(show succ m = succ (pred (succ m)), from congr_arg succ !pred.succ⁻¹))
theorem exists_eq_succ_of_ne_zero {n : ℕ} (H : n ≠ 0) : ∃k : ℕ, n = succ k :=
exists.intro _ (or_resolve_right !eq_zero_or_eq_succ_pred H)
theorem succ.inj {n m : ℕ} (H : succ n = succ m) : n = m :=
no_confusion H (λe, e)

4
library/data/nat/order.lean
View file

@ -13,6 +13,10 @@ open eq.ops
namespace nat
-- TODO: move this
theorem lt_iff_succ_le (m n : nat) : m < n ↔ succ m ≤ n :=
iff.intro succ_le_of_lt lt_of_succ_le
-- Less than or equal
-- ------------------