feat(library/algebra/ordered_ring): start on ordered_ring, and minor changes elsewhere
This commit is contained in:
Jeremy Avigad
Leonardo de Moura
parent
c9365db41b
commit
6f775be1b6
5 changed files with 500 additions and 81 deletions
|
|
@ -81,7 +81,7 @@ theorem le.antisym [s : weak_order A] {a b : A} : a ≤ b → b ≤ a → a = b
|
|||
structure linear_weak_order [class] (A : Type) extends weak_order A :=
|
||||
(le_total : ∀a b, le a b ∨ le b a)
|
||||
|
||||
theorem le.total [s : linear_weak_order A] {a b : A} : a ≤ b ∨ b ≤ a :=
|
||||
theorem le.total [s : linear_weak_order A] (a b : A) : a ≤ b ∨ b ≤ a :=
|
||||
!linear_weak_order.le_total
|
||||
|
||||
|
||||
|
|
@ -122,62 +122,82 @@ wf.rec_on x H
|
|||
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))
|
||||
|
||||
theorem lt_iff_le_and_ne [s : order_pair A] {a b : A} : a < b ↔ (a ≤ b ∧ a ≠ b) :=
|
||||
!order_pair.lt_iff_le_ne
|
||||
section
|
||||
|
||||
theorem le_of_lt [s : order_pair A] {a b : A} (H : a < b) : a ≤ b :=
|
||||
and.elim_left (iff.mp lt_iff_le_and_ne H)
|
||||
variable [s : order_pair A]
|
||||
variables {a b c : A}
|
||||
include s
|
||||
|
||||
theorem lt_of_le_of_ne [s : order_pair A] {a b : A} (H1 : a ≤ b) (H2 : a ≠ b) : a < b :=
|
||||
iff.mp (iff.symm lt_iff_le_and_ne) (and.intro H1 H2)
|
||||
theorem lt_iff_le_and_ne : a < b ↔ (a ≤ b ∧ a ≠ b) :=
|
||||
!order_pair.lt_iff_le_ne
|
||||
|
||||
definition order_pair.to_strict_order [instance] [s : order_pair A] : strict_order A :=
|
||||
strict_order.mk
|
||||
order_pair.lt
|
||||
(show ∀a, ¬ a < a, from
|
||||
take a,
|
||||
assume H : a < a,
|
||||
have H1 : a ≠ a, from and.elim_right (iff.mp !lt_iff_le_and_ne H),
|
||||
H1 rfl)
|
||||
(show ∀a b c, a < b → b < c → a < c, from
|
||||
take a b c,
|
||||
assume lt_ab : a < b,
|
||||
have le_ab : a ≤ b, from le_of_lt lt_ab,
|
||||
assume lt_bc : b < c,
|
||||
have le_bc : b ≤ c, from le_of_lt lt_bc,
|
||||
have le_ac : a ≤ c, from le.trans le_ab le_bc,
|
||||
have ne_ac : a ≠ c, from
|
||||
assume eq_ac : a = c,
|
||||
have le_ba : b ≤ a, from eq_ac⁻¹ ▸ le_bc,
|
||||
have eq_ab : a = b, from le.antisym 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)
|
||||
theorem le_of_lt (H : a < b) : a ≤ b :=
|
||||
and.elim_left (iff.mp lt_iff_le_and_ne H)
|
||||
|
||||
theorem lt_of_lt_of_le [s : order_pair A] {a b c : A} : a < b → b ≤ c → a < c :=
|
||||
assume lt_ab : a < b,
|
||||
assume le_bc : b ≤ c,
|
||||
have le_ac : a ≤ c, from le.trans (le_of_lt lt_ab) le_bc,
|
||||
have ne_ac : a ≠ c, from
|
||||
assume eq_ac : a = c,
|
||||
have le_ba : b ≤ a, from eq_ac⁻¹ ▸ le_bc,
|
||||
have eq_ab : a = b, from le.antisym (le_of_lt lt_ab) le_ba,
|
||||
show false, from lt.ne lt_ab eq_ab,
|
||||
show a < c, from lt_of_le_of_ne le_ac ne_ac
|
||||
theorem lt_of_le_of_ne (H1 : a ≤ b) (H2 : a ≠ b) : a < b :=
|
||||
iff.mp (iff.symm lt_iff_le_and_ne) (and.intro H1 H2)
|
||||
|
||||
theorem lt_of_le_of_lt [s : order_pair A] {a b c : A} : a ≤ b → b < c → a < c :=
|
||||
assume le_ab : a ≤ b,
|
||||
assume lt_bc : b < c,
|
||||
have le_ac : a ≤ c, from le.trans le_ab (le_of_lt lt_bc),
|
||||
have ne_ac : a ≠ c, from
|
||||
assume eq_ac : a = c,
|
||||
have le_cb : c ≤ b, from eq_ac ▸ le_ab,
|
||||
have eq_bc : b = c, from le.antisym (le_of_lt lt_bc) le_cb,
|
||||
show false, from lt.ne lt_bc eq_bc,
|
||||
show a < c, from lt_of_le_of_ne le_ac ne_ac
|
||||
definition order_pair.to_strict_order [instance] [s : order_pair A] : strict_order A :=
|
||||
strict_order.mk
|
||||
order_pair.lt
|
||||
(show ∀a, ¬ a < a, from
|
||||
take a,
|
||||
assume H : a < a,
|
||||
have H1 : a ≠ a, from and.elim_right (iff.mp !lt_iff_le_and_ne H),
|
||||
H1 rfl)
|
||||
(show ∀a b c, a < b → b < c → a < c, from
|
||||
take a b c,
|
||||
assume lt_ab : a < b,
|
||||
have le_ab : a ≤ b, from le_of_lt lt_ab,
|
||||
assume lt_bc : b < c,
|
||||
have le_bc : b ≤ c, from le_of_lt lt_bc,
|
||||
have le_ac : a ≤ c, from le.trans le_ab le_bc,
|
||||
have ne_ac : a ≠ c, from
|
||||
assume eq_ac : a = c,
|
||||
have le_ba : b ≤ a, from eq_ac⁻¹ ▸ le_bc,
|
||||
have eq_ab : a = b, from le.antisym 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)
|
||||
|
||||
calc_trans lt_of_lt_of_le
|
||||
calc_trans lt_of_le_of_lt
|
||||
theorem lt_of_lt_of_le : a < b → b ≤ c → a < c :=
|
||||
assume lt_ab : a < b,
|
||||
assume le_bc : b ≤ c,
|
||||
have le_ac : a ≤ c, from le.trans (le_of_lt lt_ab) le_bc,
|
||||
have ne_ac : a ≠ c, from
|
||||
assume eq_ac : a = c,
|
||||
have le_ba : b ≤ a, from eq_ac⁻¹ ▸ le_bc,
|
||||
have eq_ab : a = b, from le.antisym (le_of_lt lt_ab) le_ba,
|
||||
show false, from lt.ne 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 :=
|
||||
assume le_ab : a ≤ b,
|
||||
assume lt_bc : b < c,
|
||||
have le_ac : a ≤ c, from le.trans le_ab (le_of_lt lt_bc),
|
||||
have ne_ac : a ≠ c, from
|
||||
assume eq_ac : a = c,
|
||||
have le_cb : c ≤ b, from eq_ac ▸ le_ab,
|
||||
have eq_bc : b = c, from le.antisym (le_of_lt lt_bc) le_cb,
|
||||
show false, from lt.ne lt_bc eq_bc,
|
||||
show a < c, from lt_of_le_of_ne le_ac ne_ac
|
||||
|
||||
calc_trans lt_of_lt_of_le
|
||||
calc_trans lt_of_le_of_lt
|
||||
|
||||
theorem not_le_of_lt (H : a < b) : ¬ b ≤ a :=
|
||||
assume H1 : b ≤ a,
|
||||
lt.irrefl _ (lt_of_lt_of_le H H1)
|
||||
|
||||
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 :=
|
||||
(le_iff_lt_or_eq : ∀a b, le a b ↔ lt a b ∨ a = b)
|
||||
|
|
@ -194,9 +214,11 @@ 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] : strong_order_pair A :=
|
||||
definition strict_order_with_le.to_order_pair [instance] [s : strict_order_with_le A] :
|
||||
strong_order_pair A :=
|
||||
strong_order_pair.mk strict_order_with_le.le
|
||||
(take a, show a ≤ a, from iff.mp (iff.symm !strict_order_with_le.le_iff_lt_or_eq) (or.intro_right _ rfl))
|
||||
(take a,
|
||||
show a ≤ a, from iff.mp (iff.symm !strict_order_with_le.le_iff_lt_or_eq) (or.intro_right _ rfl))
|
||||
(take a b c,
|
||||
assume le_ab : a ≤ b,
|
||||
assume le_bc : b ≤ c,
|
||||
|
|
@ -205,7 +227,8 @@ strong_order_pair.mk strict_order_with_le.le
|
|||
(assume lt_ab : a < b,
|
||||
or.elim (iff.mp !strict_order_with_le.le_iff_lt_or_eq le_bc)
|
||||
(assume lt_bc : b < c,
|
||||
iff.elim_right !strict_order_with_le.le_iff_lt_or_eq (or.intro_left _ (lt.trans lt_ab lt_bc)))
|
||||
iff.elim_right
|
||||
!strict_order_with_le.le_iff_lt_or_eq (or.intro_left _ (lt.trans lt_ab lt_bc)))
|
||||
(assume eq_bc : b = c, eq_bc ▸ le_ab))
|
||||
(assume eq_ab : a = b,
|
||||
eq_ab⁻¹ ▸ le_bc))
|
||||
|
|
@ -223,19 +246,59 @@ strong_order_pair.mk strict_order_with_le.le
|
|||
(take a b,
|
||||
iff.intro
|
||||
(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),
|
||||
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))
|
||||
(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),
|
||||
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 (A : Type) extends order_pair A, linear_weak_order A
|
||||
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)
|
||||
|
||||
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_or_eq_or_lt_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'))
|
||||
|
||||
definition linear_strong_order_pair.to_linear_order_pair [instance] [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.lt_iff_le_ne
|
||||
(take a b : A,
|
||||
lt_or_eq_or_lt_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')
|
||||
|
||||
definition lt_of_not_le {a b : A} (H : ¬ a ≤ b) : b < a :=
|
||||
lt_or_eq_or_lt_cases
|
||||
(assume H', absurd (le_of_lt H') H)
|
||||
(assume H', absurd (H' ▸ !le.refl) H)
|
||||
(assume H', H')
|
||||
|
||||
end
|
||||
|
||||
|
||||
|
||||
|
||||
structure linear_strong_order_pair (A : Type) extends strong_order_pair A :=
|
||||
(trichotomy : ∀a b, lt a b ∨ a = b ∨ lt b a)
|
||||
|
||||
end algebra
|
||||
|
|
|
|||
|
|
@ -21,8 +21,8 @@ variable {A : Type}
|
|||
|
||||
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 c, le a b → le (add c a) (add c b))
|
||||
(le_of_add_le_add_left : ∀a b c, le (add c a) (add c b) → le a b)
|
||||
(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
|
||||
|
||||
|
|
@ -30,7 +30,7 @@ section
|
|||
include s
|
||||
|
||||
theorem add_le_add_left {a b : A} (H : a ≤ b) (c : A) : c + a ≤ c + b :=
|
||||
!ordered_cancel_comm_monoid.add_le_add_left H
|
||||
!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 :=
|
||||
(add.comm c a) ▸ (add.comm c b) ▸ (add_le_add_left H c)
|
||||
|
|
@ -189,7 +189,7 @@ end
|
|||
-- but it is not clear whether it provides any further useful generality.
|
||||
|
||||
structure ordered_comm_group [class] (A : Type) extends add_comm_group A, order_pair A :=
|
||||
(add_le_add_left : ∀a b c, le a b → le (add c a) (add c b))
|
||||
(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)
|
||||
[s : ordered_comm_group A] : ordered_cancel_comm_monoid A :=
|
||||
|
|
@ -200,8 +200,8 @@ ordered_cancel_comm_monoid.mk ordered_comm_group.add ordered_comm_group.add_asso
|
|||
has_lt.lt (@lt_iff_le_and_ne _ _) ordered_comm_group.add_le_add_left
|
||||
proof
|
||||
take a b c : A,
|
||||
assume H : c + a ≤ c + b,
|
||||
have H' : -c + (c + a) ≤ -c + (c + b), from ordered_comm_group.add_le_add_left _ _ _ H,
|
||||
assume H : a + b ≤ a + c,
|
||||
have H' : -a + (a + b) ≤ -a + (a + c), from ordered_comm_group.add_le_add_left _ _ H _,
|
||||
!neg_add_cancel_left ▸ !neg_add_cancel_left ▸ H'
|
||||
qed
|
||||
|
||||
|
|
|
|||
355
library/algebra/ordered_ring.lean
Normal file
355
library/algebra/ordered_ring.lean
Normal file
|
|
@ -0,0 +1,355 @@
|
|||
/-
|
||||
Copyright (c) 2014 Jeremy Avigad. All rights reserved.
|
||||
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.
|
||||
-/
|
||||
|
||||
import logic.eq data.unit data.sigma data.prod
|
||||
import algebra.function algebra.binary algebra.ordered_group algebra.ring
|
||||
|
||||
open eq eq.ops
|
||||
|
||||
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))
|
||||
|
||||
section
|
||||
|
||||
variable [s : ordered_semiring A]
|
||||
variables (a b c d e : A)
|
||||
include 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
|
||||
|
||||
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
|
||||
|
||||
-- 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) :
|
||||
a * b ≤ c * d :=
|
||||
calc
|
||||
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 :=
|
||||
have H : 0 * b ≤ a * b, from mul_le_mul_of_nonneg_right Ha Hb,
|
||||
!zero_mul_eq ▸ H
|
||||
|
||||
theorem mul_nonpos_of_nonneg_of_nonpos {a b : A} (Ha : a ≥ 0) (Hb : b ≤ 0) : a * b ≤ 0 :=
|
||||
have H : a * b ≤ a * 0, from mul_le_mul_of_nonneg_left Hb Ha,
|
||||
!mul_zero_eq ▸ H
|
||||
|
||||
theorem mul_nonpos_of_nonpos_of_nonneg {a b : A} (Ha : a ≤ 0) (Hb : b ≥ 0) : a * b ≤ 0 :=
|
||||
have H : a * b ≤ 0 * b, from mul_le_mul_of_nonneg_right Ha Hb,
|
||||
!zero_mul_eq ▸ 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
|
||||
|
||||
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
|
||||
|
||||
-- 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) :
|
||||
a * b < c * d :=
|
||||
calc
|
||||
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 :=
|
||||
have H : 0 * b < a * b, from mul_lt_mul_of_pos_right Ha Hb,
|
||||
!zero_mul_eq ▸ H
|
||||
|
||||
theorem mul_neg_of_pos_of_neg {a b : A} (Ha : a > 0) (Hb : b < 0) : a * b < 0 :=
|
||||
have H : a * b < a * 0, from mul_lt_mul_of_pos_left Hb Ha,
|
||||
!mul_zero_eq ▸ H
|
||||
|
||||
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_eq ▸ 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)
|
||||
include s
|
||||
|
||||
theorem lt_of_mul_lt_mul_left {a b c : A} (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 :=
|
||||
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 :=
|
||||
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 :=
|
||||
le_of_not_lt
|
||||
(assume H1 : b < a,
|
||||
have H2 : b * c < a * c, from mul_lt_mul_of_pos_right H1 Hc,
|
||||
not_le_of_lt H2 H)
|
||||
|
||||
theorem pos_of_mul_pos_left (H : 0 < a * b) (H1 : 0 ≤ a) : 0 < b :=
|
||||
lt_of_not_le
|
||||
(assume H2 : b ≤ 0,
|
||||
have H3 : a * b ≤ 0, from mul_nonpos_of_nonneg_of_nonpos H1 H2,
|
||||
not_lt_of_le H3 H)
|
||||
|
||||
theorem pos_of_mul_pos_right (H : 0 < a * b) (H1 : 0 ≤ b) : 0 < a :=
|
||||
lt_of_not_le
|
||||
(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))
|
||||
|
||||
definition ordered_ring.to_ordered_semiring [instance] [s : ordered_ring A] : ordered_semiring A :=
|
||||
ordered_semiring.mk ordered_ring.add ordered_ring.add_assoc !ordered_ring.zero
|
||||
ordered_ring.add_left_id ordered_ring.add_right_id ordered_ring.add_comm ordered_ring.mul
|
||||
ordered_ring.mul_assoc !ordered_ring.one ordered_ring.mul_left_id ordered_ring.mul_right_id
|
||||
ordered_ring.left_distrib ordered_ring.right_distrib
|
||||
zero_mul_eq mul_zero_eq !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.lt ordered_ring.lt_iff_le_ne ordered_ring.add_le_add_left
|
||||
(@le_of_add_le_add_left A _)
|
||||
(take a b c,
|
||||
assume Hab : a ≤ b,
|
||||
assume Hc : 0 ≤ c,
|
||||
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,
|
||||
iff.mp !sub_nonneg_iff_le (!mul_sub_left_distrib ▸ H2)
|
||||
qed)
|
||||
(take a b c,
|
||||
assume Hab : a ≤ b,
|
||||
assume Hc : 0 ≤ c,
|
||||
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,
|
||||
iff.mp !sub_nonneg_iff_le (!mul_sub_right_distrib ▸ H2)
|
||||
qed)
|
||||
(take a b c,
|
||||
assume Hab : a < b,
|
||||
assume Hc : 0 < c,
|
||||
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,
|
||||
iff.mp !sub_pos_iff_lt (!mul_sub_left_distrib ▸ H2)
|
||||
qed)
|
||||
(take a b c,
|
||||
assume Hab : a < b,
|
||||
assume Hc : 0 < c,
|
||||
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,
|
||||
iff.mp !sub_pos_iff_lt (!mul_sub_right_distrib ▸ H2)
|
||||
qed)
|
||||
|
||||
section
|
||||
|
||||
variable [s : ordered_ring A]
|
||||
variables (a b c : A)
|
||||
include s
|
||||
|
||||
theorem mul_le_mul_of_nonpos_left {a b c : A} (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 :=
|
||||
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 :=
|
||||
!zero_mul_eq ▸ 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 :=
|
||||
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 :=
|
||||
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 :=
|
||||
!zero_mul_eq ▸ 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
|
||||
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
|
||||
|
||||
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_of_nonpos_of_nonpos H H)
|
||||
|
||||
theorem zero_le_one : 0 ≤ 1 := mul.left_id 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.right_id ▸ add_lt_add_left H a
|
||||
theorem lt_add_of_pos_left {a b : A} (H : b > 0) : a < b + a := !add.left_id ▸ add_lt_add_right H a
|
||||
theorem le_add_of_nonneg_right {a b : A} (H : b ≥ 0) : a ≤ a + b := !add.right_id ▸ add_le_add_left H a
|
||||
theorem le_add_of_nonneg_left {a b : A} (H : b ≥ 0) : a ≤ b + a := !add.left_id ▸ add_le_add_right H a
|
||||
|
||||
/- 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_eq ▸ 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) :
|
||||
(a > 0 ∧ b > 0) ∨ (a < 0 ∧ b < 0) :=
|
||||
lt_or_eq_or_lt_cases
|
||||
-- @lt_or_eq_or_lt_cases A s 0 a ((a > 0 ∧ b > 0) ∨ (a < 0 ∧ b < 0))
|
||||
(assume Ha : 0 < a,
|
||||
proof
|
||||
lt_or_eq_or_lt_cases
|
||||
-- @lt_or_eq_or_lt_cases A s 0 b ((a > 0 ∧ b > 0) ∨ (a < 0 ∧ b < 0))
|
||||
(assume Hb : 0 < b, or.inl (and.intro Ha Hb))
|
||||
(assume Hb : 0 = b,
|
||||
have H : 0 > 0, from !mul_zero_eq ▸ Hb⁻¹ ▸ Hab,
|
||||
absurd H (lt.irrefl 0))
|
||||
(assume Hb : b < 0,
|
||||
have Hab' : a * b < 0, from mul_neg_of_pos_of_neg Ha Hb,
|
||||
absurd Hab (not_lt_of_lt Hab'))
|
||||
qed)
|
||||
(assume Ha : 0 = a,
|
||||
proof
|
||||
have H : 0 > 0, from !zero_mul_eq ▸ Ha⁻¹ ▸ Hab,
|
||||
absurd H (lt.irrefl 0)
|
||||
qed)
|
||||
(assume Ha : a < 0,
|
||||
proof
|
||||
lt_or_eq_or_lt_cases
|
||||
-- @lt_or_eq_or_lt_cases A s 0 b ((a > 0 ∧ b > 0) ∨ (a < 0 ∧ b < 0))
|
||||
(assume Hb : 0 < b,
|
||||
have Hab' : a * b < 0, from mul_neg_of_neg_of_pos Ha Hb,
|
||||
absurd Hab (not_lt_of_lt Hab'))
|
||||
(assume Hb : 0 = b,
|
||||
have H : 0 > 0, from !mul_zero_eq ▸ Hb⁻¹ ▸ Hab,
|
||||
absurd H (lt.irrefl 0))
|
||||
(assume Hb : b < 0, or.inr (and.intro Ha Hb))
|
||||
qed)
|
||||
|
||||
/-
|
||||
This version, with tactics, is also slow.
|
||||
Also, I do not understand why I cannot succesfully return to "proof mode"
|
||||
in the proof below. I think "s" is not visible there. Can I make it visible?
|
||||
|
||||
Here is the really strange thing: compiling the file with both proofs seems faster than
|
||||
compiling the file with just one of them.
|
||||
-/
|
||||
theorem pos_and_pos_or_neg_and_neg_of_mul_pos' (Hab : a * b > 0) :
|
||||
(a > 0 ∧ b > 0) ∨ (a < 0 ∧ b < 0) :=
|
||||
begin
|
||||
apply (@lt_or_eq_or_lt_cases _ _ 0 a),
|
||||
intro Ha,
|
||||
apply (@lt_or_eq_or_lt_cases _ _ 0 b),
|
||||
intro Hb, apply (or.inl (and.intro Ha Hb)),
|
||||
intro Hb,
|
||||
/-
|
||||
proof -- gives invalid local context
|
||||
have H : 0 > 0, from !mul_zero_eq ▸ (eq.symm Hb) ▸ Hab,
|
||||
absurd H (lt.irrefl 0)
|
||||
qed
|
||||
-/
|
||||
apply (absurd (!mul_zero_eq ▸ (eq.symm Hb) ▸ Hab) (lt.irrefl 0)),
|
||||
intro Hb,
|
||||
apply (absurd Hab (not_lt_of_lt (mul_neg_of_pos_of_neg Ha Hb))),
|
||||
intro Ha,
|
||||
apply (absurd (!zero_mul_eq ▸ Ha⁻¹ ▸ Hab) (lt.irrefl 0)),
|
||||
intro Ha,
|
||||
apply (@lt_or_eq_or_lt_cases _ _ 0 b),
|
||||
intro Hb,
|
||||
apply (absurd Hab (not_lt_of_lt (mul_neg_of_neg_of_pos Ha Hb))),
|
||||
intro Hb,
|
||||
apply (absurd (!mul_zero_eq ▸ (eq.symm Hb) ▸ Hab) (lt.irrefl 0)),
|
||||
intro Hb, apply (or.inr (and.intro Ha Hb))
|
||||
end
|
||||
|
||||
-- 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
|
||||
|
||||
/-
|
||||
Still left to do:
|
||||
|
||||
Isabelle's library has all kinds of cancelation rules for the simplifier, search on
|
||||
mult_le_cancel_right1 in Rings.thy.
|
||||
|
||||
Properties of abs, sgn, and dvd.
|
||||
|
||||
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
|
||||
|
|
@ -43,11 +43,14 @@ 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 := @zero_ne_one_class.zero_ne_one A s
|
||||
|
||||
/- semiring -/
|
||||
|
||||
structure semiring [class] (A : Type) extends add_comm_monoid A, monoid A, distrib A, mul_zero A,
|
||||
zero_ne_one_class A
|
||||
|
||||
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.
|
||||
|
||||
/- abstract divisibility -/
|
||||
|
||||
structure has_dvd [class] (A : Type) extends has_mul A :=
|
||||
|
|
@ -147,7 +150,7 @@ semiring.mk ring.add ring.add_assoc !ring.zero ring.add_left_id
|
|||
ring.add_comm ring.mul ring.mul_assoc !ring.one ring.mul_left_id ring.mul_right_id
|
||||
ring.left_distrib ring.right_distrib
|
||||
(take a,
|
||||
have H : 0 * a + 0 = 0 * a + 0 * a, from
|
||||
have H : 0 * a + 0 = 0 * a + 0 * a, from
|
||||
calc
|
||||
0 * a + 0 = 0 * a : add.right_id
|
||||
... = (0 + 0) * a : {(add.right_id 0)⁻¹}
|
||||
|
|
@ -159,7 +162,7 @@ semiring.mk ring.add ring.add_assoc !ring.zero ring.add_left_id
|
|||
a * 0 + 0 = a * 0 : add.right_id
|
||||
... = a * (0 + 0) : {(add.right_id 0)⁻¹}
|
||||
... = a * 0 + a * 0 : ring.left_distrib,
|
||||
show a * 0 = 0, from (add.left_cancel H)⁻¹)
|
||||
show a * 0 = 0, from (add.left_cancel H)⁻¹)
|
||||
!ring.zero_ne_one
|
||||
|
||||
section
|
||||
|
|
|
|||
|
|
@ -2,13 +2,13 @@
|
|||
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Module: init.logic
|
||||
Authors: Leonardo de Moura, Jeremy Avigad, Floris van Doorn
|
||||
-/
|
||||
prelude
|
||||
import init.datatypes init.reserved_notation
|
||||
|
||||
-- implication
|
||||
-- -----------
|
||||
/- implication -/
|
||||
|
||||
definition trivial := true.intro
|
||||
|
||||
|
|
@ -18,14 +18,12 @@ prefix `¬` := not
|
|||
definition absurd {a : Prop} {b : Type} (H1 : a) (H2 : ¬a) : b :=
|
||||
false.rec b (H2 H1)
|
||||
|
||||
-- not
|
||||
-- ---
|
||||
/- not -/
|
||||
|
||||
theorem not_false : ¬false :=
|
||||
assume H : false, H
|
||||
|
||||
-- eq
|
||||
-- --
|
||||
/- eq -/
|
||||
|
||||
notation a = b := eq a b
|
||||
definition rfl {A : Type} {a : A} := eq.refl a
|
||||
|
|
@ -71,8 +69,7 @@ calc_refl eq.refl
|
|||
calc_trans eq.trans
|
||||
calc_symm eq.symm
|
||||
|
||||
-- ne
|
||||
-- --
|
||||
/- ne -/
|
||||
|
||||
definition ne {A : Type} (a b : A) := ¬(a = b)
|
||||
notation a ≠ b := ne a b
|
||||
|
|
@ -153,8 +150,7 @@ calc_trans heq.of_heq_of_eq
|
|||
calc_trans heq.of_eq_of_heq
|
||||
calc_symm heq.symm
|
||||
|
||||
-- and
|
||||
-- ---
|
||||
/- and -/
|
||||
|
||||
notation a /\ b := and a b
|
||||
notation a ∧ b := and a b
|
||||
|
|
@ -164,8 +160,8 @@ variables {a b c d : Prop}
|
|||
theorem and.elim (H₁ : a ∧ b) (H₂ : a → b → c) : c :=
|
||||
and.rec H₂ H₁
|
||||
|
||||
-- or
|
||||
-- --
|
||||
/- or -/
|
||||
|
||||
notation a `\/` b := or a b
|
||||
notation a ∨ b := or a b
|
||||
|
||||
|
|
@ -180,8 +176,8 @@ namespace or
|
|||
rec H₂ H₃ H₁
|
||||
end or
|
||||
|
||||
-- iff
|
||||
-- ---
|
||||
/- iff -/
|
||||
|
||||
definition iff (a b : Prop) := (a → b) ∧ (b → a)
|
||||
|
||||
notation a <-> b := iff a b
|
||||
|
|
@ -202,6 +198,8 @@ namespace iff
|
|||
definition elim_right (H : a ↔ b) : b → a :=
|
||||
elim (assume H₁ H₂, H₂) H
|
||||
|
||||
definition mp' := @elim_right
|
||||
|
||||
definition flip_sign (H₁ : a ↔ b) : ¬a ↔ ¬b :=
|
||||
intro
|
||||
(assume (Hna : ¬ a) (Hb : b), absurd (elim_right H₁ Hb) Hna)
|
||||
|
|
|
|||
Loading…
Reference in a new issue