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

comparison HOD.agda @ 123:0c2cbf37e002

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 Sun, 30 Jun 2019 20:31:10 +0900
parents 4d2434513228
children 55c6e1ddc739
comparison
equal deleted inserted replaced
122:4d2434513228 123:0c2cbf37e002
76 -- sup-lb : {n : Level } → ( ψ : Ordinal {n} → Ordinal {n}) → ( ∀ {x : Ordinal {n}} → ψx o< z ) → z o< osuc ( sup-o ψ ) 76 -- sup-lb : {n : Level } → ( ψ : Ordinal {n} → Ordinal {n}) → ( ∀ {x : Ordinal {n}} → ψx o< z ) → z o< osuc ( sup-o ψ )
77 minimul : {n : Level } → (x : HOD {suc n} ) → ¬ (x == od∅ )→ HOD {suc n} 77 minimul : {n : Level } → (x : HOD {suc n} ) → ¬ (x == od∅ )→ HOD {suc n}
78 -- this should be ¬ (x == od∅ )→ ∃ ox → x ∋ Ord ox ( minimum of x ) 78 -- this should be ¬ (x == od∅ )→ ∃ ox → x ∋ Ord ox ( minimum of x )
79 x∋minimul : {n : Level } → (x : HOD {suc n} ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimul x ne ) ) 79 x∋minimul : {n : Level } → (x : HOD {suc n} ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimul x ne ) )
80 minimul-1 : {n : Level } → (x : HOD {suc n} ) → ( ne : ¬ (x == od∅ ) ) → (y : HOD {suc n}) → ¬ ( def (minimul x ne) (od→ord y)) ∧ (def x (od→ord y) ) 80 minimul-1 : {n : Level } → (x : HOD {suc n} ) → ( ne : ¬ (x == od∅ ) ) → (y : HOD {suc n}) → ¬ ( def (minimul x ne) (od→ord y)) ∧ (def x (od→ord y) )
81 -- we should prove this in agda, but simply put here
82 ===-≡ : {n : Level} { x y : HOD {suc n}} → x == y → x ≡ y
83
84 Ord-ord : {n : Level } {ox : Ordinal {suc n}} → Ord ox ≡ ord→od ox
85 Ord-ord {n} {px} = trans (sym oiso) (cong ( λ k → ord→od k ) (sym ord-Ord))
81 86
82 _∋_ : { n : Level } → ( a x : HOD {n} ) → Set n 87 _∋_ : { n : Level } → ( a x : HOD {n} ) → Set n
83 _∋_ {n} a x = def a ( od→ord x ) 88 _∋_ {n} a x = def a ( od→ord x )
84 89
85 _c<_ : { n : Level } → ( x a : HOD {n} ) → Set n 90 _c<_ : { n : Level } → ( x a : HOD {n} ) → Set n
105 sup-c< : {n : Level } → ( ψ : HOD {n} → HOD {n}) → ∀ {x : HOD {n}} → def ( sup-od ψ ) (od→ord ( ψ x )) 110 sup-c< : {n : Level } → ( ψ : HOD {n} → HOD {n}) → ∀ {x : HOD {n}} → def ( sup-od ψ ) (od→ord ( ψ x ))
106 sup-c< {n} ψ {x} = def-subst {n} {_} {_} {Ord ( sup-o ( λ x → od→ord (ψ (ord→od x ))) )} {od→ord ( ψ x )} 111 sup-c< {n} ψ {x} = def-subst {n} {_} {_} {Ord ( sup-o ( λ x → od→ord (ψ (ord→od x ))) )} {od→ord ( ψ x )}
107 lemma refl (cong ( λ k → od→ord (ψ k) ) oiso) where 112 lemma refl (cong ( λ k → od→ord (ψ k) ) oiso) where
108 lemma : od→ord (ψ (ord→od (od→ord x))) o< sup-o (λ x → od→ord (ψ (ord→od x))) 113 lemma : od→ord (ψ (ord→od (od→ord x))) o< sup-o (λ x → od→ord (ψ (ord→od x)))
109 lemma = subst₂ (λ j k → j o< k ) refl diso (o<-subst sup-o< refl (sym diso) ) 114 lemma = subst₂ (λ j k → j o< k ) refl diso (o<-subst sup-o< refl (sym diso) )
115
116 o<→o> : {n : Level} → { x y : Ordinal {n} } → (Ord x == Ord y) → x o< y → ⊥
117 o<→o> {n} {x} {y} record { eq→ = xy ; eq← = yx } (case1 lt) with o<-subst (yx (case1 lt)) ord-Ord refl
118 ... | oyx with o<¬≡ refl (c<→o< {n} {Ord x} oyx )
119 ... | ()
120 o<→o> {n} {x} {y} record { eq→ = xy ; eq← = yx } (case2 lt) with o<-subst (yx (case2 lt)) ord-Ord refl
121 ... | oyx with o<¬≡ refl (c<→o< {n} {Ord x} oyx )
122 ... | ()
123
124 Ord==→≡ : {n : Level} { x y : Ordinal {suc n}} → Ord x == Ord y → x ≡ y
125 Ord==→≡ {n} {x} {y} eq with trio< x y
126 Ord==→≡ {n} {x} {y} eq | tri< a ¬b ¬c = ⊥-elim ( o<→o> eq a )
127 Ord==→≡ {n} {x} {y} eq | tri≈ ¬a b ¬c = b
128 Ord==→≡ {n} {x} {y} eq | tri> ¬a ¬b c = ⊥-elim ( o<→o> (eq-sym eq) c )
129
110 130
111 ∅3 : {n : Level} → { x : Ordinal {n}} → ( ∀(y : Ordinal {n}) → ¬ (y o< x ) ) → x ≡ o∅ {n} 131 ∅3 : {n : Level} → { x : Ordinal {n}} → ( ∀(y : Ordinal {n}) → ¬ (y o< x ) ) → x ≡ o∅ {n}
112 ∅3 {n} {x} = TransFinite {n} c2 c3 x where 132 ∅3 {n} {x} = TransFinite {n} c2 c3 x where
113 c0 : Nat → Ordinal {n} → Set n 133 c0 : Nat → Ordinal {n} → Set n
114 c0 lx x = (∀(y : Ordinal {n}) → ¬ (y o< x)) → x ≡ o∅ {n} 134 c0 lx x = (∀(y : Ordinal {n}) → ¬ (y o< x)) → x ≡ o∅ {n}
232 L {n} record { lv = Zero ; ord = (Φ .0) } = od∅ 252 L {n} record { lv = Zero ; ord = (Φ .0) } = od∅
233 L {n} record { lv = lx ; ord = (OSuc lv ox) } = Def ( L {n} ( record { lv = lx ; ord = ox } ) ) 253 L {n} record { lv = lx ; ord = (OSuc lv ox) } = Def ( L {n} ( record { lv = lx ; ord = ox } ) )
234 L {n} record { lv = (Suc lx) ; ord = (Φ (Suc lx)) } = -- Union ( L α ) 254 L {n} record { lv = (Suc lx) ; ord = (Φ (Suc lx)) } = -- Union ( L α )
235 cseq ( Ord (od→ord (L {n} (record { lv = lx ; ord = Φ lx })))) 255 cseq ( Ord (od→ord (L {n} (record { lv = lx ; ord = Φ lx }))))
236 256
237 LS : {n : Level} → {la : Nat } → {oa : OrdinalD {suc n} la } 257 L00 : {n : Level} → (ox : Ordinal {suc n}) → ox o< sup-o ( λ x → od→ord ( ZFSubset (Ord ox) (ord→od x )))
238 → L {n} (record { lv = la; ord = OSuc la oa }) ∋ L {n} (record { lv = la; ord = oa }) 258 L00 {n} ox = o<-subst {suc n} {_} {_} {ox} {sup-o ( λ x → od→ord ( ZFSubset (Ord ox) (ord→od x )))}
239 LS {n} {la} {oa} = {!!} where 259 (sup-o< {suc n} {λ x → od→ord ( ZFSubset (Ord ox) (ord→od x ))} {ox} ) (lemma0 ox) refl where
260 lemma1 : {n : Level } {ox z : Ordinal {suc n}} → ( def (Ord ox) z ∧ def (ord→od ox) z ) ⇔ def ( Ord ox ) z
261 lemma1 {n} {ox} {z} = record { proj1 = proj1 ; proj2 = λ t → record { proj1 = t ; proj2 = subst (λ k → def k z ) Ord-ord t }}
240 lemma0 : {n : Level} → (ox : Ordinal {suc n}) → od→ord (ZFSubset (Ord ox) (ord→od ox)) ≡ ox 262 lemma0 : {n : Level} → (ox : Ordinal {suc n}) → od→ord (ZFSubset (Ord ox) (ord→od ox)) ≡ ox
241 lemma0 = {!!} 263 lemma0 {n} ox = trans (cong (λ k → od→ord k) (===-≡ (⇔→== lemma1) )) (sym ord-Ord)
242 lemma : {n : Level} → (ox : Ordinal {suc n}) → ox o< sup-o ( λ x → od→ord ( ZFSubset (Ord ox) (ord→od x ))) 264
243 lemma {n} ox = o<-subst {suc n} {_} {_} {ox} {sup-o ( λ x → od→ord ( ZFSubset (Ord ox) (ord→od x )))} 265 -- L0 : {n : Level} → (α : Ordinal {suc n}) → α o< β → L (osuc α) ∋ L α
244 (sup-o< {suc n} {λ x → od→ord ( ZFSubset (Ord ox) (ord→od x ))} {ox} ) (lemma0 ox) refl 266 -- L1 : {n : Level} → (α β : Ordinal {suc n}) → α o< β → ∀ (x : HOD {suc n}) → L α ∋ x → L β ∋ x
245
246 L0 : {n : Level} → {la : Nat } → {oa : OrdinalD {suc n} (Suc la) }{ob : OrdinalD {suc n} la }
247 → L (record { lv = Suc la; ord = oa }) ∋ L (record { lv = la; ord = ob })
248 L0 = {!!}
249
250 L1 : {n : Level} → (α β : Ordinal {suc n}) → α o< β → ∀ (x : HOD {suc n}) → L α ∋ x → L β ∋ x
251 L1 {n} record { lv = .0 ; ord = (Φ .0) } record { lv = .(Suc _) ; ord = ord₁ } (case1 (s≤s z≤n)) x (case1 ())
252 L1 {n} record { lv = .0 ; ord = (Φ .0) } record { lv = .(Suc _) ; ord = ord₁ } (case1 (s≤s z≤n)) x (case2 ())
253 L1 {n} record { lv = .0 ; ord = (OSuc .0 ord₂) } record { lv = (Suc lx) ; ord = ord₁ } (case1 (s≤s z≤n)) x α∋x = lemma α∋x where
254 lemma : (od→ord x) o< (sup-o (λ x₁ → od→ord (ZFSubset (L (record { lv = 0 ; ord = ord₂ })) (ord→od x₁))))
255 → L (record { lv = Suc lx ; ord = ord₁ }) ∋ x
256 lemma lt = {!!}
257 L1 {n} record { lv = (Suc _) ; ord = ord₂ } record { lv = (Suc (Suc _)) ; ord = ord₁ } (case1 (s≤s (s≤s x₁))) x α∋x = {!!}
258 L1 {n} record { lv = lx ; ord = (Φ lx) } record { lv = lx ; ord = (OSuc lx _) } (case2 Φ<) x α∋x = {!!}
259 L1 {n} record { lv = lx ; ord = (OSuc lx _) } record { lv = lx ; ord = (OSuc lx _) } (case2 (s< x₁)) x α∋x = {!!}
260 267
261 omega : { n : Level } → Ordinal {n} 268 omega : { n : Level } → Ordinal {n}
262 omega = record { lv = Suc Zero ; ord = Φ 1 } 269 omega = record { lv = Suc Zero ; ord = Φ 1 }
263 270
264 HOD→ZF : {n : Level} → ZF {suc (suc n)} {suc n} 271 HOD→ZF : {n : Level} → ZF {suc (suc n)} {suc n}