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

refactor(library/algebra/order): cleanup, and remove unused class

Browse source
This commit is contained in:
Jeremy Avigad 2015-06-28 14:23:45 +10:00
parent 0fc2efe88e
commit 0d25831111
1 changed files with 42 additions and 144 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

186
library/algebra/order.lean
View file

@ -3,16 +3,8 @@ Copyright (c) 2014 Jeremy Avigad. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE. Released under Apache 2.0 license as described in the file LICENSE.
Author: Jeremy Avigad Author: Jeremy Avigad
Various types of orders. We develop weak orders "≤" and strict orders "<" separately. We also Weak orders "≤", strict orders "<", and structures that include both.
consider structures with both, where the two are related by
x < y ↔ (x ≤ y ∧ x ≠ y) (order_pair)
x ≤ y ↔ (x < y ∨ x = y) (strong_order_pair)
These might not hold constructively in some applications, but we can define additional structures
with both < and ≤ as needed.
-/ -/
import logic.eq logic.connectives import logic.eq logic.connectives
open eq eq.ops open eq eq.ops
@ -28,7 +20,7 @@ structure has_le [class] (A : Type) :=
structure has_lt [class] (A : Type) := structure has_lt [class] (A : Type) :=
(lt : A → A → Prop) (lt : A → A → Prop)
infixl `<=` := has_le.le infixl `<=` := has_le.le
infixl `≤` := has_le.le infixl `≤` := has_le.le
infixl `<` := has_lt.lt infixl `<` := has_lt.lt
@ -58,7 +50,7 @@ section
theorem le.antisymm {a b : A} : a ≤ b → b ≤ a → a = b := !weak_order.le_antisymm theorem le.antisymm {a b : A} : a ≤ b → b ≤ a → a = b := !weak_order.le_antisymm
-- Alternate syntax. A definition does not migrate well. -- Alternate syntax. (Abbreviations do not migrate well.)
theorem eq_of_le_of_ge {a b : A} : a ≤ b → b ≤ a → a = b := !le.antisymm theorem eq_of_le_of_ge {a b : A} : a ≤ b → b ≤ a → a = b := !le.antisymm
end end
@ -100,8 +92,6 @@ end
/- well-founded orders -/ /- well-founded orders -/
-- TODO: do these duplicate what Leo has done? if so, eliminate
structure wf_strict_order [class] (A : Type) extends strict_order A := structure wf_strict_order [class] (A : Type) extends strict_order A :=
(wf_rec : ∀P : A → Type, (∀x, (∀y, lt y x → P y) → P x) → ∀x, P x) (wf_rec : ∀P : A → Type, (∀x, (∀y, lt y x → P y) → P x) → ∀x, P x)
@ -120,7 +110,6 @@ structure order_pair [class] (A : Type) extends weak_order A, has_lt A :=
(lt_of_lt_of_le : ∀ a b c, lt a b → le b c → lt a c) (lt_of_lt_of_le : ∀ a b c, lt a b → le b c → lt a c)
(lt_of_le_of_lt : ∀ a b c, le a b → lt b c → lt a c) (lt_of_le_of_lt : ∀ a b c, le a b → lt b c → lt a c)
(lt_irrefl : ∀ a, ¬ lt a a) (lt_irrefl : ∀ a, ¬ lt a a)
--lt_iff_le_and_ne : a < b ↔ (a ≤ b ∧ a ≠ b)
section section
variable [s : order_pair A] variable [s : order_pair A]
@ -141,7 +130,6 @@ section
definition order_pair.to_strict_order [trans-instance] [coercion] [reducible] : strict_order A := definition order_pair.to_strict_order [trans-instance] [coercion] [reducible] : strict_order A :=
⦃ strict_order, s, lt_irrefl := lt_irrefl s, lt_trans := lt_trans s ⦄ ⦃ strict_order, s, lt_irrefl := lt_irrefl s, lt_trans := lt_trans s ⦄
theorem gt_of_gt_of_ge [trans] (H1 : a > b) (H2 : b ≥ c) : a > c := lt_of_le_of_lt H2 H1 theorem gt_of_gt_of_ge [trans] (H1 : a > b) (H2 : b ≥ c) : a > c := lt_of_le_of_lt H2 H1
theorem gt_of_ge_of_gt [trans] (H1 : a ≥ b) (H2 : b > c) : a > c := lt_of_lt_of_le H2 H1 theorem gt_of_ge_of_gt [trans] (H1 : a ≥ b) (H2 : b > c) : a > c := lt_of_lt_of_le H2 H1
@ -155,7 +143,7 @@ section
lt.irrefl _ (lt_of_le_of_lt H H1) lt.irrefl _ (lt_of_le_of_lt H H1)
end end
structure strong_order_pair [class] (A : Type) extends weak_order A, has_lt A := --order_pair A := structure strong_order_pair [class] (A : Type) extends weak_order A, has_lt A :=
(le_iff_lt_or_eq : ∀a b, le a b ↔ lt a b ∨ a = b) (le_iff_lt_or_eq : ∀a b, le a b ↔ lt a b ∨ a = b)
(lt_irrefl : ∀ a, ¬ lt a a) (lt_irrefl : ∀ a, ¬ lt a a)
@ -166,147 +154,57 @@ theorem lt_or_eq_of_le [s : strong_order_pair A] {a b : A} (le_ab : a ≤ b) : a
iff.mp le_iff_lt_or_eq le_ab iff.mp le_iff_lt_or_eq le_ab
theorem le_of_lt_or_eq [s : strong_order_pair A] {a b : A} (lt_or_eq : a < b ∨ a = b) : a ≤ b := theorem le_of_lt_or_eq [s : strong_order_pair A] {a b : A} (lt_or_eq : a < b ∨ a = b) : a ≤ b :=
iff.mp' le_iff_lt_or_eq lt_or_eq iff.mp' le_iff_lt_or_eq lt_or_eq
private theorem lt_irrefl' [s : strong_order_pair A] (a : A) : ¬ a < a := private theorem lt_irrefl' [s : strong_order_pair A] (a : A) : ¬ a < a :=
!strong_order_pair.lt_irrefl !strong_order_pair.lt_irrefl
private theorem le_of_lt' [s : strong_order_pair A] (a b : A) : a < b → a ≤ b := private theorem le_of_lt' [s : strong_order_pair A] (a b : A) : a < b → a ≤ b :=
take Hlt, le_of_lt_or_eq (or.inl Hlt) take Hlt, le_of_lt_or_eq (or.inl Hlt)
private theorem lt_iff_le_and_ne [s : strong_order_pair A] {a b : A} : a < b ↔ (a ≤ b ∧ a ≠ b) := private theorem lt_iff_le_and_ne [s : strong_order_pair A] {a b : A} : a < b ↔ (a ≤ b ∧ a ≠ b) :=
iff.intro iff.intro
(take Hlt, and.intro (le_of_lt_or_eq (or.inl Hlt)) (take Hab, absurd (Hab ▸ Hlt) !lt_irrefl')) (take Hlt, and.intro (le_of_lt_or_eq (or.inl Hlt)) (take Hab, absurd (Hab ▸ Hlt) !lt_irrefl'))
(take Hand, (take Hand,
have Hor : a < b ∨ a = b, from lt_or_eq_of_le (and.left Hand), have Hor : a < b ∨ a = b, from lt_or_eq_of_le (and.left Hand),
or_resolve_left Hor (and.right Hand)) or_resolve_left Hor (and.right Hand))
theorem lt_of_le_of_ne [s : strong_order_pair A] {a b : A} : a ≤ b → a ≠ b → a < b := theorem lt_of_le_of_ne [s : strong_order_pair A] {a b : A} : a ≤ b → a ≠ b → a < b :=
take H1 H2, iff.mp' lt_iff_le_and_ne (and.intro H1 H2) take H1 H2, iff.mp' lt_iff_le_and_ne (and.intro H1 H2)
private theorem ne_of_lt' [s : strong_order_pair A] {a b : A} (H : a < b) : a ≠ b := private theorem ne_of_lt' [s : strong_order_pair A] {a b : A} (H : a < b) : a ≠ b :=
and.right ((iff.mp lt_iff_le_and_ne) H) and.right ((iff.mp lt_iff_le_and_ne) H)
private theorem lt_of_lt_of_le' [s : strong_order_pair A] (a b c : A) : a < b → b ≤ c → a < c := private theorem lt_of_lt_of_le' [s : strong_order_pair A] (a b c : A) : a < b → b ≤ c → a < c :=
assume lt_ab : a < b, assume lt_ab : a < b,
assume le_bc : b ≤ c, assume le_bc : b ≤ c,
have le_ac : a ≤ c, from le.trans (le_of_lt' _ _ lt_ab) le_bc, have le_ac : a ≤ c, from le.trans (le_of_lt' _ _ lt_ab) le_bc,
have ne_ac : a ≠ c, from have ne_ac : a ≠ c, from
assume eq_ac : a = c, assume eq_ac : a = c,
have le_ba : b ≤ a, from eq_ac⁻¹ ▸ le_bc, have le_ba : b ≤ a, from eq_ac⁻¹ ▸ le_bc,
have eq_ab : a = b, from le.antisymm (le_of_lt' _ _ lt_ab) le_ba, 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 false, from ne_of_lt' lt_ab eq_ab,
show a < c, from iff.mp' (lt_iff_le_and_ne) (and.intro le_ac ne_ac) show a < c, from iff.mp' (lt_iff_le_and_ne) (and.intro le_ac ne_ac)
theorem lt_of_le_of_lt' [s : strong_order_pair A] (a b c : A) : a ≤ b → b < c → a < c := theorem lt_of_le_of_lt' [s : strong_order_pair A] (a b c : A) : a ≤ b → b < c → a < c :=
assume le_ab : a ≤ b, assume le_ab : a ≤ b,
assume lt_bc : b < c, assume lt_bc : b < c,
have le_ac : a ≤ c, from le.trans le_ab (le_of_lt' _ _ lt_bc), have le_ac : a ≤ c, from le.trans le_ab (le_of_lt' _ _ lt_bc),
have ne_ac : a ≠ c, from have ne_ac : a ≠ c, from
assume eq_ac : a = c, assume eq_ac : a = c,
have le_cb : c ≤ b, from eq_ac ▸ le_ab, have le_cb : c ≤ b, from eq_ac ▸ le_ab,
have eq_bc : b = c, from le.antisymm (le_of_lt' _ _ lt_bc) le_cb, 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 false, from ne_of_lt' lt_bc eq_bc,
show a < c, from iff.mp' (lt_iff_le_and_ne) (and.intro le_ac ne_ac) show a < c, from iff.mp' (lt_iff_le_and_ne) (and.intro le_ac ne_ac)
definition strong_order_pair.to_order_pair [trans-instance] [coercion] [reducible] [s : strong_order_pair A]
: order_pair A :=
⦃ order_pair, s,
lt_irrefl := lt_irrefl',
le_of_lt := le_of_lt',
lt_of_le_of_lt := lt_of_le_of_lt',
lt_of_lt_of_le := lt_of_lt_of_le'
⦄
-- We can also construct a strong order pair by defining a strict order, and then defining
-- x ≤ y ↔ x < y ∨ x = y
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)
private theorem le_refl (s : strict_order_with_le A) (a : A) : a ≤ a :=
iff.mp (iff.symm !strict_order_with_le.le_iff_lt_or_eq) (or.intro_right _ rfl)
private theorem le_trans (s : strict_order_with_le A) (a b c : A) (le_ab : a ≤ b) (le_bc : b ≤ c) : a ≤ c :=
or.elim (iff.mp !strict_order_with_le.le_iff_lt_or_eq le_ab)
(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)))
(assume eq_bc : b = c, eq_bc ▸ le_ab))
(assume eq_ab : a = b,
eq_ab⁻¹ ▸ le_bc)
private theorem le_antisymm (s : strict_order_with_le A) (a b : A) (le_ab : a ≤ b) (le_ba : b ≤ a) : a = b :=
or.elim (iff.mp !strict_order_with_le.le_iff_lt_or_eq le_ab)
(assume lt_ab : a < b,
or.elim (iff.mp !strict_order_with_le.le_iff_lt_or_eq le_ba)
(assume lt_ba : b < a, absurd (lt.trans lt_ab lt_ba) (lt.irrefl a))
(assume eq_ba : b = a, eq_ba⁻¹))
(assume eq_ab : a = b, eq_ab)
private theorem lt_iff_le_ne (s : strict_order_with_le A) (a b : A) : a < b ↔ a ≤ b ∧ 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),
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))
private theorem le_of_lt' (s : strict_order_with_le A) (a b : A) : a < b → a ≤ b :=
take Hlt, and.left (iff.mp (lt_iff_le_ne s _ _) Hlt)
private theorem lt_trans (s : strict_order_with_le A) (a b c: A) (lt_ab : a < b) (lt_bc : b < c) : a < c :=
have le_ab : a ≤ b, from le_of_lt' s _ _ lt_ab,
have le_bc : b ≤ c, from le_of_lt' s _ _ lt_bc,
have le_ac : a ≤ c, from le_trans s _ _ _ le_ab le_bc,
have ne_ac : a ≠ c, from
assume eq_ac : a = c,
have le_ba : b ≤ a, from eq_ac⁻¹ ▸ le_bc,
have eq_ab : a = b, from le_antisymm s a b le_ab le_ba,
have ne_ab : a ≠ b, from and.elim_right ((iff.mp (lt_iff_le_ne s a b)) lt_ab),
ne_ab eq_ab,
show a < c, from (iff.mp' !lt_iff_le_ne) (and.intro le_ac ne_ac)
theorem lt_of_lt_of_le' (s : strict_order_with_le A) (a b c : A) : a < b → b ≤ c → a < c :=
assume lt_ab : a < b,
assume le_bc : b ≤ c,
have le_ac : a ≤ c, from le_trans s _ _ _ (le_of_lt' s _ _ lt_ab) le_bc,
have ne_ac : a ≠ c, from
assume eq_ac : a = c,
have le_ba : b ≤ a, from eq_ac⁻¹ ▸ le_bc,
have eq_ab : a = b, from le_antisymm s _ _ (le_of_lt' s _ _ lt_ab) le_ba,
show false, from ne_of_lt lt_ab eq_ab,
show a < c, from iff.mp' (lt_iff_le_ne s _ _) (and.intro le_ac ne_ac)
theorem lt_of_le_of_lt'' (s : strict_order_with_le A) (a b c : A) : a ≤ b → b < c → a < c :=
assume le_ab : a ≤ b,
assume lt_bc : b < c,
have le_ac : a ≤ c, from le_trans s _ _ _ le_ab (le_of_lt' s _ _ lt_bc),
have ne_ac : a ≠ c, from
assume eq_ac : a = c,
have le_cb : c ≤ b, from eq_ac ▸ le_ab,
have eq_bc : b = c, from le_antisymm s _ _ (le_of_lt' s _ _ lt_bc) le_cb,
show false, from ne_of_lt lt_bc eq_bc,
show a < c, from iff.mp' (lt_iff_le_ne s _ _) (and.intro le_ac ne_ac)
definition strict_order_with_le.to_order_pair [trans-instance] [coercion] [reducible] [s : strict_order_with_le A] :
strong_order_pair A :=
⦃ strong_order_pair, s,
le_refl := le_refl s,
le_trans := le_trans s,
le_antisymm := le_antisymm s ⦄
--le_of_lt := le_of_lt' s,
--lt_of_le_of_lt := lt_of_le_of_lt' s,
--lt_of_lt_of_le := lt_of_lt_of_le' s ⦄
--lt_iff_le_and_ne := lt_iff_le_ne s ⦄
definition strong_order_pair.to_order_pair [trans-instance] [coercion] [reducible]
[s : strong_order_pair A] : order_pair A :=
⦃ order_pair, s,
lt_irrefl := lt_irrefl',
le_of_lt := le_of_lt',
lt_of_le_of_lt := lt_of_le_of_lt',
lt_of_lt_of_le := lt_of_lt_of_le'
⦄
/- linear orders -/ /- linear orders -/
@ -317,7 +215,7 @@ structure linear_strong_order_pair [class] (A : Type) extends strong_order_pair
definition linear_strong_order_pair.to_linear_order_pair [trans-instance] [coercion] [reducible] definition linear_strong_order_pair.to_linear_order_pair [trans-instance] [coercion] [reducible]
[s : linear_strong_order_pair A] : linear_order_pair A := [s : linear_strong_order_pair A] : linear_order_pair A :=
⦃ linear_order_pair, s, strong_order_pair.to_order_pair⦄ ⦃ linear_order_pair, s, strong_order_pair.to_order_pair⦄
section section
variable [s : linear_strong_order_pair A] variable [s : linear_strong_order_pair A]