Mercurial > hg > Members > kono > Proof > ZF-in-agda

comparison src/zorn.agda @ 491:646831f6b06d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 08 Apr 2022 22:19:05 +0900
parents 00c71d1dc316
children e28b1da1b58d
comparison
equal deleted inserted replaced
490:00c71d1dc316 491:646831f6b06d
45 elm : HOD 45 elm : HOD
46 is-elm : A ∋ elm 46 is-elm : A ∋ elm
47 47
48 open Element 48 open Element
49 49
50 TotalOrderSet : ( A : HOD ) → (_<_ : (x y : HOD) → Set n ) → Set (suc n)
51 TotalOrderSet A _<_ = Trichotomous (λ (x : Element A) y → elm x ≡ elm y ) (λ x y → elm x < elm y )
52
53 PartialOrderSet : ( A : HOD ) → (_<_ : (x y : HOD) → Set n ) → Set (suc n)
54 PartialOrderSet A _<_ = (a b : Element A)
55 → (elm a < elm b → ((¬ elm b < elm a) ∧ (¬ (elm a ≡ elm b) ))) ∧ (elm a ≡ elm b → (¬ elm a < elm b) ∧ (¬ elm b < elm a))
56
57 IsPartialOrderSet : ( A : HOD ) → (_<_ : (x y : HOD) → Set n ) → Set (suc n) 50 IsPartialOrderSet : ( A : HOD ) → (_<_ : (x y : HOD) → Set n ) → Set (suc n)
58 IsPartialOrderSet A _<_ = IsPartialOrder _<A_ _≡A_ where 51 IsPartialOrderSet A _<_ = IsPartialOrder _<A_ _≡A_ where
59 _<A_ : (x y : Element A ) → Set n 52 _<A_ : (x y : Element A ) → Set n
60 x <A y = elm x < elm y 53 x <A y = elm x < elm y
61 _≡A_ : (x y : Element A ) → Set (suc n) 54 _≡A_ : (x y : Element A ) → Set (suc n)
86 open _==_ 79 open _==_
87 open _⊆_ 80 open _⊆_
88 81
89 record ZChain ( A : HOD ) (y : Ordinal) (_<_ : (x y : HOD) → Set n ) : Set (suc n) where 82 record ZChain ( A : HOD ) (y : Ordinal) (_<_ : (x y : HOD) → Set n ) : Set (suc n) where
90 field 83 field
91 fb : (x : Ordinal ) → x o< y → HOD 84 fb : (x : Ordinal ) → HOD
92 A∋fb : (ox : Ordinal ) → (x<y : ox o< y ) → A ∋ fb ox x<y 85 A∋fb : (ox : Ordinal ) → ox o< y → A ∋ fb ox
93 monotonic : {ox oz : Ordinal } → (x<y : ox o< y ) → (z<y : oz o< y ) → ox o< oz → fb ox x<y < fb oz z<y 86 total : {ox oz : Ordinal } → (x<y : ox o< y ) → (z<y : oz o< y ) → ( ox ≡ oz ) ∨ ( fb ox < fb oz ) ∨ ( fb oz < fb ox )
87 monotonic : {ox oz : Ordinal } → (x<y : ox o< y ) → (z<y : oz o< y ) → ox o< oz → fb ox < fb oz
94 88
95 Zorn-lemma : { A : HOD } → { _<_ : (x y : HOD) → Set n } 89 Zorn-lemma : { A : HOD } → { _<_ : (x y : HOD) → Set n }
96 → o∅ o< & A 90 → o∅ o< & A
97 → PartialOrderSet A _<_ 91 → IsPartialOrderSet A _<_
98 → ( ( B : HOD) → (B⊆A : B ⊆ A) → TotalOrderSet B _<_ → SUP A B _<_ ) -- SUP condition 92 → ( ( B : HOD) → (B⊆A : B ⊆ A) → IsTotalOrderSet B _<_ → SUP A B _<_ ) -- SUP condition
99 → Maximal A _<_ 93 → Maximal A _<_
100 Zorn-lemma {A} {_<_} 0<A PO supP = zorn00 where 94 Zorn-lemma {A} {_<_} 0<A PO supP = zorn00 where
101 someA : HOD 95 someA : HOD
102 someA = ODC.minimal O A (λ eq → ¬x<0 ( subst (λ k → o∅ o< k ) (=od∅→≡o∅ eq) 0<A )) 96 someA = ODC.minimal O A (λ eq → ¬x<0 ( subst (λ k → o∅ o< k ) (=od∅→≡o∅ eq) 0<A ))
103 isSomeA : A ∋ someA 97 isSomeA : A ∋ someA
111 Gtx : { x : HOD} → A ∋ x → HOD 105 Gtx : { x : HOD} → A ∋ x → HOD
112 Gtx {x} ax = record { od = record { def = λ y → odef A y ∧ (x < (* y)) } ; odmax = & A ; <odmax = z09 } where 106 Gtx {x} ax = record { od = record { def = λ y → odef A y ∧ (x < (* y)) } ; odmax = & A ; <odmax = z09 } where
113 z09 : {y : Ordinal} → (odef A y ∧ (x < (* y))) → y o< & A 107 z09 : {y : Ordinal} → (odef A y ∧ (x < (* y))) → y o< & A
114 z09 {y} P = subst (λ k → k o< & A) &iso (c<→o< {* y} (subst (λ k → odef A k) (sym &iso) (proj1 P))) 108 z09 {y} P = subst (λ k → k o< & A) &iso (c<→o< {* y} (subst (λ k → odef A k) (sym &iso) (proj1 P)))
115 z01 : {a b : HOD} → A ∋ a → A ∋ b → (a ≡ b ) ∨ (a < b ) → b < a → ⊥ 109 z01 : {a b : HOD} → A ∋ a → A ∋ b → (a ≡ b ) ∨ (a < b ) → b < a → ⊥
116 z01 {a} {b} A∋a A∋b (case1 a=b) b<a = proj1 (proj2 (PO (me A∋b) (me A∋a)) (sym a=b)) b<a 110 z01 {a} {b} A∋a A∋b (case1 a=b) b<a = {!!} -- proj1 (proj2 (PO (me A∋b) (me A∋a)) (sym a=b)) b<a
117 z01 {a} {b} A∋a A∋b (case2 a<b) b<a = proj1 (proj1 (PO (me A∋b) (me A∋a)) b<a) a<b 111 z01 {a} {b} A∋a A∋b (case2 a<b) b<a = {!!} -- proj1 (proj1 (PO (me A∋b) (me A∋a)) b<a) a<b
118 -- ZChain is not compatible with the SUP condition 112 -- ZChain is not compatible with the SUP condition
119 record BX (x y : Ordinal) (fb : ( x : Ordinal ) → (x o< y ) → HOD ) : Set n where 113 record BX (x y : Ordinal) (fb : ( x : Ordinal ) → HOD ) : Set n where
120 field 114 field
121 bx : Ordinal 115 bx : Ordinal
122 bx<y : bx o< y 116 bx<y : bx o< y
123 is-fb : x ≡ & (fb bx bx<y ) 117 is-fb : x ≡ & (fb bx )
124 bx<A : (z : ZChain A (& A) _<_ ) → {x : Ordinal } → (bx : BX x (& A) ( ZChain.fb z )) → BX.bx bx o< & A 118 bx<A : (z : ZChain A (& A) _<_ ) → {x : Ordinal } → (bx : BX x (& A) ( ZChain.fb z )) → BX.bx bx o< & A
125 bx<A z {x} bx = BX.bx<y bx 119 bx<A z {x} bx = BX.bx<y bx
126 B : (z : ZChain A (& A) _<_ ) → HOD 120 B : (z : ZChain A (& A) _<_ ) → HOD
127 B z = record { od = record { def = λ x → BX x (& A) ( ZChain.fb z ) } ; odmax = & A ; <odmax = {!!} } 121 B z = record { od = record { def = λ x → BX x (& A) ( ZChain.fb z ) } ; odmax = & A ; <odmax = {!!} }
128 z11 : (z : ZChain A (& A) _<_ ) → (x : Element (B z)) → elm x ≡ ZChain.fb z (BX.bx (is-elm x)) (bx<A z (is-elm x)) 122 z11 : (z : ZChain A (& A) _<_ ) → (x : Element (B z)) → elm x ≡ ZChain.fb z ?
129 z11 z x = subst₂ (λ j k → j ≡ k ) *iso *iso ( cong (*) (BX.is-fb (is-elm x)) ) 123 z11 z x = subst₂ (λ j k → j ≡ k ) *iso *iso ( cong (*) (BX.is-fb (is-elm x)) )
130 obx : (z : ZChain A (& A) _<_ ) → {x : HOD} → B z ∋ x → Ordinal 124 obx : (z : ZChain A (& A) _<_ ) → {x : HOD} → B z ∋ x → Ordinal
131 obx z {x} bx = BX.bx bx 125 obx z {x} bx = BX.bx bx
132 obx=fb : (z : ZChain A (& A) _<_ ) → {x : HOD} → (bx : B z ∋ x ) → x ≡ ZChain.fb z ( obx z bx ) (bx<A z bx ) 126 obx=fb : (z : ZChain A (& A) _<_ ) → {x : HOD} → (bx : B z ∋ x ) → x ≡ ZChain.fb z {!!}
133 obx=fb z {x} bx = subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) (BX.is-fb bx)) 127 obx=fb z {x} bx = subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) (BX.is-fb bx))
134 B⊆A : (z : ZChain A (& A) _<_ ) → B z ⊆ A 128 B⊆A : (z : ZChain A (& A) _<_ ) → B z ⊆ A
135 B⊆A z = record { incl = λ {x} bx → subst (λ k → odef A k ) (sym (BX.is-fb bx)) (ZChain.A∋fb z (BX.bx bx) (BX.bx<y bx) ) } 129 B⊆A z = record { incl = λ {x} bx → subst (λ k → odef A k ) (sym (BX.is-fb bx)) (ZChain.A∋fb z (BX.bx bx) (BX.bx<y bx) ) }
136 PO-B : (z : ZChain A (& A) _<_ ) → PartialOrderSet (B z) _<_ 130 PO-B : (z : ZChain A (& A) _<_ ) → IsPartialOrderSet (B z) _<_
137 PO-B z a b = PO record { elm = elm a ; is-elm = incl ( B⊆A z) (is-elm a) } record { elm = elm b ; is-elm = incl ( B⊆A z) (is-elm b) } 131 PO-B z = ? -- a b = {!!} -- PO record { elm = elm a ; is-elm = incl ( B⊆A z) (is-elm a) } record { elm = elm b ; is-elm = incl ( B⊆A z) (is-elm b) }
138 bx-monotonic : (z : ZChain A (& A) _<_ ) → {x y : Element (B z)} → obx z (is-elm x) o< obx z (is-elm y) → elm x < elm y 132 bx-monotonic : (z : ZChain A (& A) _<_ ) → {x y : Element (B z)} → obx z (is-elm x) o< obx z (is-elm y) → elm x < elm y
139 bx-monotonic z {x} {y} a = subst₂ (λ j k → j < k ) (sym (z11 z x)) (sym (z11 z y)) (ZChain.monotonic z (bx<A z (is-elm x)) (bx<A z (is-elm y)) a ) 133 bx-monotonic z {x} {y} a = subst₂ (λ j k → j < k ) (sym (z11 z x)) (sym (z11 z y)) (ZChain.monotonic z (bx<A z (is-elm x)) (bx<A z (is-elm y)) a )
140 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 134 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
141 z12 : (z : ZChain A (& A) _<_ ) → {a b : HOD } → (x : BX (& a) (& A) (ZChain.fb z)) (y : BX (& b) (& A) (ZChain.fb z)) 135 z12 : (z : ZChain A (& A) _<_ ) → {a b : HOD } → (x : BX (& a) (& A) (ZChain.fb z)) (y : BX (& b) (& A) (ZChain.fb z))
142 → obx z x ≡ obx z y → bx<A z x ≅ bx<A z y 136 → obx z x ≡ obx z y → bx<A z x ≅ bx<A z y
145 bx-inject z {x} {y} eq = begin 139 bx-inject z {x} {y} eq = begin
146 elm x ≡⟨ {!!} ⟩ 140 elm x ≡⟨ {!!} ⟩
147 {!!} ≡⟨ cong (λ k → {!!} ) {!!} ⟩ 141 {!!} ≡⟨ cong (λ k → {!!} ) {!!} ⟩
148 {!!} ≡⟨ {!!} ⟩ 142 {!!} ≡⟨ {!!} ⟩
149 elm y ∎ where open ≡-Reasoning 143 elm y ∎ where open ≡-Reasoning
150 B-is-total : (z : ZChain A (& A) _<_ ) → TotalOrderSet (B z) _<_ 144 B-is-total : (z : ZChain A (& A) _<_ ) → IsTotalOrderSet (B z) _<_
151 B-is-total z x y with trio< (obx z (is-elm x)) (obx z (is-elm y)) 145 B-is-total = ?
152 ... | tri< a ¬b ¬c = tri< z10 (λ eq → proj1 (proj2 (PO-B z x y) eq ) z10) (λ ¬c → proj1 (proj1 (PO-B z y x) ¬c ) z10) where 146 B-Tri : (z : ZChain A (& A) _<_ ) → Trichotomous (λ (x : Element A) y → elm x ≡ elm y ) (λ x y → elm x < elm y )
147 B-Tri z x y with trio< (obx z ?) (obx z ?)
148 ... | tri< a ¬b ¬c = ? where -- tri< z10 (λ eq → proj1 (proj2 (PO-B z x y) eq ) z10) (λ ¬c → proj1 (proj1 (PO-B z y x) ¬c ) z10) where
153 z10 : elm x < elm y 149 z10 : elm x < elm y
154 z10 = bx-monotonic z {x} {y} a 150 z10 = ? -- bx-monotonic z {x} {y} a
155 ... | tri≈ ¬a b ¬c = tri≈ {!!} (bx-inject z {x} {y} b) {!!} 151 ... | tri≈ ¬a b ¬c = ? -- tri≈ {!!} (bx-inject z {x} {y} b) {!!}
156 ... | tri> ¬a ¬b c = tri> (λ ¬a → proj1 (proj1 (PO-B z x y) ¬a ) (bx-monotonic z {y} {x} c) ) (λ eq → proj2 (proj2 (PO-B z x y) eq ) (bx-monotonic z {y} {x} c)) (bx-monotonic z {y} {x} c) 152 ... | tri> ¬a ¬b c = ? -- tri> (λ ¬a → proj1 (proj1 (PO-B z x y) ¬a ) (bx-monotonic z {y} {x} c) ) (λ eq → proj2 (proj2 (PO-B z x y) eq ) (bx-monotonic z {y} {x} c)) (bx-monotonic z {y} {x} c)
157 ZChain→¬SUP : (z : ZChain A (& A) _<_ ) → ¬ (SUP A (B z) _<_ ) 153 ZChain→¬SUP : (z : ZChain A (& A) _<_ ) → ¬ (SUP A (B z) _<_ )
158 ZChain→¬SUP z sp = ⊥-elim {!!} where 154 ZChain→¬SUP z sp = ⊥-elim {!!} where
159 z03 : & (SUP.sup sp) o< osuc (& A) 155 z03 : & (SUP.sup sp) o< osuc (& A)
160 z03 = ordtrans (c<→o< (SUP.A∋maximal sp)) <-osuc 156 z03 = ordtrans (c<→o< (SUP.A∋maximal sp)) <-osuc
161 z02 : (x : HOD) → B z ∋ x → SUP.sup sp < x → ⊥ 157 z02 : (x : HOD) → B z ∋ x → SUP.sup sp < x → ⊥
221 _⊆'_ : ( A B : HOD ) → Set n 217 _⊆'_ : ( A B : HOD ) → Set n
222 _⊆'_ A B = (x : Ordinal ) → odef A x → odef B x 218 _⊆'_ A B = (x : Ordinal ) → odef A x → odef B x
223 219
224 MaximumSubset : {L P : HOD} 220 MaximumSubset : {L P : HOD}
225 → o∅ o< & L → o∅ o< & P → P ⊆ L 221 → o∅ o< & L → o∅ o< & P → P ⊆ L
226 → PartialOrderSet P _⊆'_ 222 → IsPartialOrderSet P _⊆'_
227 → ( (B : HOD) → B ⊆ P → TotalOrderSet B _⊆'_ → SUP P B _⊆'_ ) 223 → ( (B : HOD) → B ⊆ P → IsTotalOrderSet B _⊆'_ → SUP P B _⊆'_ )
228 → Maximal P (_⊆'_) 224 → Maximal P (_⊆'_)
229 MaximumSubset {L} {P} 0<L 0<P P⊆L PO SP = Zorn-lemma {P} {_⊆'_} 0<P PO SP 225 MaximumSubset {L} {P} 0<L 0<P P⊆L PO SP = Zorn-lemma {P} {_⊆'_} 0<P PO SP