1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
|
/-
Copyright (c) 2017 Johannes Hölzl. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johannes Hölzl
Zorn's lemmas.
Ported from Isabelle/HOL (written by Jacques D. Fleuriot, Tobias Nipkow, and Christian Sternagel).
-/
import data.set.lattice
noncomputable theory
universes u
open set classical
local attribute [instance] decidable_inhabited
local attribute [instance] prop_decidable
namespace zorn
section chain
parameters {α : Type u} {r : α → α → Prop}
local infix ` ≺ `:50 := r
def chain (c : set α) := pairwise_on c (λx y, x ≺ y ∨ y ≺ x)
theorem chain_insert {c : set α} {a : α} (hc : chain c) (ha : ∀b∈c, b ≠ a → a ≺ b ∨ b ≺ a) :
chain (insert a c) :=
forall_insert_of_forall
(assume x hx, forall_insert_of_forall (hc x hx) (assume hneq, (ha x hx hneq).symm))
(forall_insert_of_forall (assume x hx hneq, ha x hx $ assume h', hneq h'.symm) (assume h, (h rfl).rec _))
def super_chain (c₁ c₂ : set α) := chain c₂ ∧ c₁ ⊂ c₂
def is_max_chain (c : set α) := chain c ∧ ¬ (∃c', super_chain c c')
def succ_chain (c : set α) :=
if h : ∃c', chain c ∧ super_chain c c' then some h else c
theorem succ_spec {c : set α} (h : ∃c', chain c ∧ super_chain c c') :
super_chain c (succ_chain c) :=
let ⟨c', hc'⟩ := h in
have chain c ∧ super_chain c (some h),
from @some_spec _ (λc', chain c ∧ super_chain c c') _,
by simp [succ_chain, dif_pos, h, this.right]
theorem chain_succ {c : set α} (hc : chain c) : chain (succ_chain c) :=
if h : ∃c', chain c ∧ super_chain c c' then
(succ_spec h).left
else
by simp [succ_chain, dif_neg, h]; exact hc
theorem super_of_not_max {c : set α} (hc₁ : chain c) (hc₂ : ¬ is_max_chain c) :
super_chain c (succ_chain c) :=
begin
simp [is_max_chain, not_and_iff, not_not_iff] at hc₂,
exact have ∃c', super_chain c c', from hc₂.neg_resolve_left hc₁,
let ⟨c', hc'⟩ := this in
show super_chain c (succ_chain c),
from succ_spec ⟨c', hc₁, hc'⟩
end
theorem succ_increasing {c : set α} : c ⊆ succ_chain c :=
if h : ∃c', chain c ∧ super_chain c c' then
have super_chain c (succ_chain c), from succ_spec h,
this.right.left
else by simp [succ_chain, dif_neg, h, subset.refl]
inductive chain_closure : set α → Prop
| succ : ∀{s}, chain_closure s → chain_closure (succ_chain s)
| union : ∀{s}, (∀a∈s, chain_closure a) → chain_closure (⋃₀ s)
theorem chain_closure_empty : chain_closure ∅ :=
have chain_closure (⋃₀ ∅),
from chain_closure.union $ assume a h, h.rec _,
by simp at this; assumption
theorem chain_closure_closure : chain_closure (⋃₀ chain_closure) :=
chain_closure.union $ assume s hs, hs
variables {c c₁ c₂ c₃ : set α}
private lemma chain_closure_succ_total_aux (hc₁ : chain_closure c₁) (hc₂ : chain_closure c₂)
(h : ∀{c₃}, chain_closure c₃ → c₃ ⊆ c₂ → c₂ = c₃ ∨ succ_chain c₃ ⊆ c₂) :
c₁ ⊆ c₂ ∨ succ_chain c₂ ⊆ c₁ :=
begin
induction hc₁,
case _root_.zorn.chain_closure.succ c₃ hc₃ ih {
cases ih with ih ih,
{ have h := h hc₃ ih,
cases h with h h,
{ exact or.inr (h ▸ subset.refl _) },
{ exact or.inl h } },
{ exact or.inr (subset.trans ih succ_increasing) } },
case _root_.zorn.chain_closure.union s hs ih {
refine (or_of_not_implies' $ λ hn, sUnion_subset $ λ a ha, _),
apply (ih a ha).resolve_right,
apply mt (λ h, _) hn,
exact subset.trans h (subset_sUnion_of_mem ha) }
end
private lemma chain_closure_succ_total (hc₁ : chain_closure c₁) (hc₂ : chain_closure c₂) (h : c₁ ⊆ c₂) :
c₂ = c₁ ∨ succ_chain c₁ ⊆ c₂ :=
begin
induction hc₂ generalizing c₁ hc₁ h,
case _root_.zorn.chain_closure.succ c₂ hc₂ ih {
have h₁ : c₁ ⊆ c₂ ∨ @succ_chain α r c₂ ⊆ c₁ :=
(chain_closure_succ_total_aux hc₁ hc₂ $ assume c₁, ih),
cases h₁ with h₁ h₁,
{ have h₂ := ih hc₁ h₁,
cases h₂ with h₂ h₂,
{ exact (or.inr $ h₂ ▸ subset.refl _) },
{ exact (or.inr $ subset.trans h₂ succ_increasing) } },
{ exact (or.inl $ subset.antisymm h₁ h) } },
case _root_.zorn.chain_closure.union s hs ih {
apply or.imp (assume h', subset.antisymm h' h) id,
apply classical.by_contradiction,
simp [not_or_iff, sUnion_subset_iff, classical.not_forall_iff, not_implies_iff],
intro h, cases h with h₁ h₂, cases h₂ with c₃ h₂, cases h₂ with h₂ hc₃,
have h := chain_closure_succ_total_aux hc₁ (hs c₃ hc₃) (assume c₄, ih _ hc₃),
cases h with h h,
{ have h' := ih c₃ hc₃ hc₁ h,
cases h' with h' h',
{ exact (h₂ $ h' ▸ subset.refl _) },
{ exact (h₁ $ subset.trans h' $ subset_sUnion_of_mem hc₃) } },
{ exact (h₂ $ subset.trans succ_increasing h) } }
end
theorem chain_closure_total (hc₁ : chain_closure c₁) (hc₂ : chain_closure c₂) : c₁ ⊆ c₂ ∨ c₂ ⊆ c₁ :=
have c₁ ⊆ c₂ ∨ succ_chain c₂ ⊆ c₁,
from chain_closure_succ_total_aux hc₁ hc₂ $ assume c₃ hc₃, chain_closure_succ_total hc₃ hc₂,
or.imp_right (assume : succ_chain c₂ ⊆ c₁, subset.trans succ_increasing this) this
theorem chain_closure_succ_fixpoint (hc₁ : chain_closure c₁) (hc₂ : chain_closure c₂)
(h_eq : succ_chain c₂ = c₂) : c₁ ⊆ c₂ :=
begin
induction hc₁,
case _root_.zorn.chain_closure.succ c₁ hc₁ h {
exact or.elim (chain_closure_succ_total hc₁ hc₂ h)
(assume h, h ▸ h_eq.symm ▸ subset.refl c₂) id },
case _root_.zorn.chain_closure.union s hs ih {
exact (sUnion_subset $ assume c₁ hc₁, ih c₁ hc₁) }
end
theorem chain_closure_succ_fixpoint_iff (hc : chain_closure c) :
succ_chain c = c ↔ c = ⋃₀ chain_closure :=
⟨assume h, subset.antisymm
(subset_sUnion_of_mem hc)
(chain_closure_succ_fixpoint chain_closure_closure hc h),
assume : c = ⋃₀{c : set α | chain_closure c},
subset.antisymm
(calc succ_chain c ⊆ ⋃₀{c : set α | chain_closure c} :
subset_sUnion_of_mem $ chain_closure.succ hc
... = c : this.symm)
succ_increasing⟩
theorem chain_chain_closure (hc : chain_closure c) : chain c :=
begin
induction hc,
case _root_.zorn.chain_closure.succ c hc h {
exact chain_succ h },
case _root_.zorn.chain_closure.union s hs h {
have h : ∀c∈s, zorn.chain c := h,
exact assume c₁ ⟨t₁, ht₁, (hc₁ : c₁ ∈ t₁)⟩ c₂ ⟨t₂, ht₂, (hc₂ : c₂ ∈ t₂)⟩ hneq,
have t₁ ⊆ t₂ ∨ t₂ ⊆ t₁, from chain_closure_total (hs _ ht₁) (hs _ ht₂),
or.elim this
(assume : t₁ ⊆ t₂, h t₂ ht₂ c₁ (this hc₁) c₂ hc₂ hneq)
(assume : t₂ ⊆ t₁, h t₁ ht₁ c₁ hc₁ c₂ (this hc₂) hneq) }
end
def max_chain := ⋃₀ chain_closure
/-- Hausdorff's maximality principle
There exists a maximal totally ordered subset of `α`.
Note that we do not require `α` to be partially ordered by `r`. -/
theorem max_chain_spec : is_max_chain max_chain :=
classical.by_contradiction $
assume : ¬ is_max_chain (⋃₀ chain_closure),
have super_chain (⋃₀ chain_closure) (succ_chain (⋃₀ chain_closure)),
from super_of_not_max (chain_chain_closure chain_closure_closure) this,
let ⟨h₁, h₂, (h₃ : (⋃₀ chain_closure) ≠ succ_chain (⋃₀ chain_closure))⟩ := this in
have succ_chain (⋃₀ chain_closure) = (⋃₀ chain_closure),
from (chain_closure_succ_fixpoint_iff chain_closure_closure).mpr rfl,
h₃ this.symm
/-- Zorn's lemma
If every chain has an upper bound, then there is a maximal element -/
theorem zorn (h : ∀c, chain c → ∃ub, ∀a∈c, a ≺ ub) (trans : ∀{a b c}, a ≺ b → b ≺ c → a ≺ c) :
∃m, ∀a, m ≺ a → a ≺ m :=
have ∃ub, ∀a∈max_chain, a ≺ ub,
from h _ $ max_chain_spec.left,
let ⟨ub, (hub : ∀a∈max_chain, a ≺ ub)⟩ := this in
⟨ub, assume a ha,
have chain (insert a max_chain),
from chain_insert max_chain_spec.left $ assume b hb _, or.inr $ trans (hub b hb) ha,
have a ∈ max_chain, from
classical.by_contradiction $ assume h : a ∉ max_chain,
max_chain_spec.right $ ⟨insert a max_chain, this, ssubset_insert h⟩,
hub a this⟩
end chain
theorem zorn_weak_order {α : Type u} [weak_order α]
(h : ∀c:set α, @chain α (≤) c → ∃ub, ∀a∈c, a ≤ ub) : ∃m:α, ∀a, m ≤ a → a = m :=
let ⟨m, hm⟩ := @zorn α (≤) h (assume a b c, le_trans) in
⟨m, assume a ha, le_antisymm (hm a ha) ha⟩
end zorn
-- other bits of tricky syntax
@[to_additive "See note [foo]"]
lemma mul_one : sorry := sorry
|
