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

comparison ordinal-definable.agda @ 60:6a1f67a4cc6e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
dead end
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 29 May 2019 12:06:43 +0900
parents d13d1351a1fa
children f2cb756084e0
comparison
equal deleted inserted replaced
59:d13d1351a1fa 60:6a1f67a4cc6e
67 oiso : {n : Level} {x : OD {n}} → ord→od ( od→ord x ) ≡ x 67 oiso : {n : Level} {x : OD {n}} → ord→od ( od→ord x ) ≡ x
68 diso : {n : Level} {x : Ordinal {n}} → od→ord ( ord→od x ) ≡ x 68 diso : {n : Level} {x : Ordinal {n}} → od→ord ( ord→od x ) ≡ x
69 sup-od : {n : Level } → ( OD {n} → OD {n}) → OD {n} 69 sup-od : {n : Level } → ( OD {n} → OD {n}) → OD {n}
70 sup-c< : {n : Level } → ( ψ : OD {n} → OD {n}) → ∀ {x : OD {n}} → ψ x c< sup-od ψ 70 sup-c< : {n : Level } → ( ψ : OD {n} → OD {n}) → ∀ {x : OD {n}} → ψ x c< sup-od ψ
71 ∅-base-def : {n : Level} → def ( ord→od (o∅ {n}) ) ≡ def (od∅ {n}) 71 ∅-base-def : {n : Level} → def ( ord→od (o∅ {n}) ) ≡ def (od∅ {n})
72
73 congf : {n : Level} {x y : OD {n}} → { f g : OD {n} → OD {n} } → x ≡ y → f ≡ g → f x ≡ g y
74 congf refl refl = refl
72 75
73 o∅→od∅ : {n : Level} → ord→od (o∅ {n}) ≡ od∅ {n} 76 o∅→od∅ : {n : Level} → ord→od (o∅ {n}) ≡ od∅ {n}
74 o∅→od∅ {n} = cong ( λ k → record { def = k }) ( ∅-base-def ) 77 o∅→od∅ {n} = cong ( λ k → record { def = k }) ( ∅-base-def )
75 78
76 ∅1 : {n : Level} → ( x : OD {n} ) → ¬ ( x c< od∅ {n} ) 79 ∅1 : {n : Level} → ( x : OD {n} ) → ¬ ( x c< od∅ {n} )
231 234
232 ∅0 : {n : Level} → { x : Ordinal {n} } → o∅ {n} o< x → ¬ ( ord→od x == od∅ {n} ) 235 ∅0 : {n : Level} → { x : Ordinal {n} } → o∅ {n} o< x → ¬ ( ord→od x == od∅ {n} )
233 ∅0 {n} {x} lt record { eq→ = eq→ ; eq← = eq← } with ominimal x lt 236 ∅0 {n} {x} lt record { eq→ = eq→ ; eq← = eq← } with ominimal x lt
234 ... | min with eq→ (o<→c< (Minimumo.min<x min)) 237 ... | min with eq→ (o<→c< (Minimumo.min<x min))
235 ... | () 238 ... | ()
239
240 ∅< : {n : Level} → { x y : OD {n} } → def x (od→ord y ) → ¬ ( x == od∅ {n} )
241 ∅< {n} {x} {y} d eq with eq→ eq d
242 ∅< {n} {x} {y} d eq | lift ()
236 243
237 244
238 is-od∅ : {n : Level} → ( x : OD {suc n} ) → Dec ( x == od∅ {suc n} ) 245 is-od∅ : {n : Level} → ( x : OD {suc n} ) → Dec ( x == od∅ {suc n} )
239 is-od∅ {n} x with trio< {n} (od→ord x) (o∅ {suc n}) 246 is-od∅ {n} x with trio< {n} (od→ord x) (o∅ {suc n})
240 is-od∅ {n} x | tri≈ ¬a b ¬c = yes ( ∅7 (orefl b) ) 247 is-od∅ {n} x | tri≈ ¬a b ¬c = yes ( ∅7 (orefl b) )
257 264
258 ∅9 : {n : Level} → {x : OD {n} } → ¬ x == od∅ → o∅ o< od→ord x 265 ∅9 : {n : Level} → {x : OD {n} } → ¬ x == od∅ → o∅ o< od→ord x
259 ∅9 {_} {x} not = ∅5 lemma where 266 ∅9 {_} {x} not = ∅5 lemma where
260 lemma : ¬ od→ord x ≡ o∅ 267 lemma : ¬ od→ord x ≡ o∅
261 lemma eq = not ( ∅7 eq ) 268 lemma eq = not ( ∅7 eq )
269
270 ∅10 : {n : Level} → {ox : Ordinal {n}} → {x : OD{n}} → ( x ≡ ord→od ox ) → (not : ¬ (x == od∅)) → o∅ o< ox
271 ∅10 {n} {ox} {x} refl not = subst (λ k → o∅ o< k) diso (∅9 not)
262 272
263 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 273 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
264 274
265 OD→ZF : {n : Level} → ZF {suc (suc n)} {suc n} 275 OD→ZF : {n : Level} → ZF {suc (suc n)} {suc n}
266 OD→ZF {n} = record { 276 OD→ZF {n} = record {
331 selection : {ψ : OD → Set (suc n)} {X y : OD} → ((X ∋ y) ∧ ψ y) ⇔ (Select X ψ ∋ y) 341 selection : {ψ : OD → Set (suc n)} {X y : OD} → ((X ∋ y) ∧ ψ y) ⇔ (Select X ψ ∋ y)
332 selection {ψ} {X} {y} = record { 342 selection {ψ} {X} {y} = record {
333 proj1 = λ cond → record { proj1 = proj1 cond ; proj2 = ψiso {ψ} (proj2 cond) (sym oiso) } 343 proj1 = λ cond → record { proj1 = proj1 cond ; proj2 = ψiso {ψ} (proj2 cond) (sym oiso) }
334 ; proj2 = λ select → record { proj1 = proj1 select ; proj2 = ψiso {ψ} (proj2 select) oiso } 344 ; proj2 = λ select → record { proj1 = proj1 select ; proj2 = ψiso {ψ} (proj2 select) oiso }
335 } 345 }
346 ∅-iso : {x : OD} → ¬ (x == od∅) → ¬ ((ord→od (od→ord x)) == od∅)
347 ∅-iso {x} neq = subst (λ k → ¬ k) (=-iso {n} ) neq
336 minord : (x : OD {suc n} ) → ¬ (x == od∅ )→ Minimumo (od→ord x) 348 minord : (x : OD {suc n} ) → ¬ (x == od∅ )→ Minimumo (od→ord x)
337 minord x not = ominimal (od→ord x) (∅9 not) 349 minord x not = ominimal (od→ord x) (∅9 not)
338 minimul : (x : OD {suc n} ) → ¬ (x == od∅ )→ OD {suc n} 350 minimul : (x : OD {suc n} ) → ¬ (x == od∅ )→ OD {suc n}
339 minimul x not = ord→od ( mino (minord x not)) 351 minimul x not = ord→od ( mino (minord x not))
340 minimul<x : (x : OD {suc n} ) → (not : ¬ x == od∅ ) → x ∋ minimul x not 352 minimul<x : (x : OD {suc n} ) → (not : ¬ x == od∅ ) → x ∋ minimul x not
341 minimul<x x not = lemma0 (min<x (minord x not)) where 353 minimul<x x not = lemma0 (min<x (minord x not)) where
342 lemma0 : mino (minord x not) o< (od→ord x) → def x (od→ord (ord→od (mino (minord x not)))) 354 lemma0 : mino (minord x not) o< (od→ord x) → def x (od→ord (ord→od (mino (minord x not))))
343 lemma0 m<x = def-subst {suc n} {ord→od (od→ord x)} {od→ord (ord→od (mino (minord x not)))} (o<→c< m<x) oiso refl 355 lemma0 m<x = def-subst {suc n} {ord→od (od→ord x)} {od→ord (ord→od (mino (minord x not)))} (o<→c< m<x) oiso refl
344 regularity-ord : (x : Ordinal ) (not : ¬ (ord→od x == od∅)) →
345 (ord→od x ∋ minimul (ord→od x) not) ∧ (Select (minimul (ord→od x) not) (λ x₁ → (minimul (ord→od x) not ∋ x₁) ∧ ((ord→od x) ∋ x₁)) == od∅)
346 proj1 ( regularity-ord x not ) = minimul<x (ord→od x) not
347 proj2 ( regularity-ord x not ) = reg1 where
348 reg2 : {y : Ordinal} → ( def (minimul (ord→od x) not) y ∧ (minimul (ord→od x) not ∋ ord→od y) ∧ ((ord→od x) ∋ ord→od y) ) → ⊥
349 reg2 {y} t with proj1 t | proj1 (proj2 t) | proj2 (proj2 t)
350 ... | p1 | p2 | p3 with is-∋ (ord→od x) ( ord→od y)
351 reg2 {y} t | p1 | p2 | p3 | no ¬p = ⊥-elim (¬p p3 ) -- ¬ x ∋ ord→od y empty x case
352 reg2 {y} t | p1 | p2 | p3 | yes p with is-∋ (minimul (ord→od x) not) (ord→od y)
353 reg2 {y} t | p1 | p2 | p3 | yes p | no ¬p = ⊥-elim (¬p p2 ) -- minimum contains nothing q.e.d.
354 reg2 {y} t | p1 | p2 | p3 | yes p | yes p₁ = {!!}
355 reg0 : {y : Ordinal {suc n}} → def (Select (minimul (ord→od x) not) (λ z → (minimul (ord→od x) not ∋ z) ∧ ((ord→od x) ∋ z))) y → def od∅ y
356 reg0 {y} t with trio< y (mino (minord (ord→od x) not))
357 reg0 {y} t | tri< a ¬b ¬c with reg2 {y} t
358 ... | ()
359 reg0 {y} t | tri≈ ¬a refl ¬c = lemma y ( mino (minord (ord→od x) not) ) refl
360 (def-subst {suc n} {ord→od y} {mino (minord (ord→od x) not)} (proj1 t) refl (sym diso))
361 where
362 lemma : ( ox oy : Ordinal {suc n} ) → ox ≡ oy → ord→od ox c< ord→od oy → Lift (suc n) ⊥
363 lemma ox oy refl lt = lift ( o≡→¬c< {suc n} {ord→od oy} {ord→od oy} refl lt )
364 reg0 {y} t | tri> ¬a ¬b c with o<> y (mino (minord (ord→od x) not)) (lemma {!!}) c where
365 lemma : def (ord→od (mino (minord (ord→od x) not))) y → y o< mino (minord (ord→od x) not)
366 lemma d with c<→o< {suc n} {ord→od y} {ord→od (mino (minord (ord→od x) not))}
367 (def-subst {suc n} {ord→od (mino (minord (ord→od x) not))} {y} {!!} refl (sym diso))
368 lemma d | clt = o<-subst clt ord-iso ord-iso
369 ... | ()
370 reg1 : Select (minimul (ord→od x) not) (λ x₁ → (minimul (ord→od x) not ∋ x₁) ∧ ((ord→od x) ∋ x₁)) == od∅
371 reg1 = record { eq→ = reg0 ; eq← = λ () } where
372 ∅-iso : {x : OD} → ¬ (x == od∅) → ¬ ((ord→od (od→ord x)) == od∅)
373 ∅-iso {x} neq = subst (λ k → ¬ k) (=-iso {n} ) neq
374 regularity : (x : OD) (not : ¬ (x == od∅)) → 356 regularity : (x : OD) (not : ¬ (x == od∅)) →
375 (x ∋ minimul x not) ∧ (Select (minimul x not) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁)) == od∅) 357 (x ∋ minimul x not) ∧ (Select (minimul x not) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁)) == od∅)
376 regularity x not = 358 regularity x not = regularity-ord (od→ord x) x (sym oiso ) not where
377 subst₂ ( λ x min → (x ∋ min) ∧ (Select min (λ x₁ → (min ∋ x₁) ∧ (x ∋ x₁)) == od∅) ) 359 regularity-ord : (ox : Ordinal ) → (x : OD) → ( x ≡ ord→od ox ) → (not : ¬ (x == od∅))
378 oiso lemma ( regularity-ord (od→ord x) (subst (λ k → ¬ (k == od∅) ) (sym oiso) not )) where 360 → (x ∋ minimul x not) ∧ (Select (minimul x not) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁)) == od∅)
379 lemma : minimul (ord→od (od→ord x)) (subst (λ k → ¬ (k == od∅)) (sym oiso) not) ≡ minimul x not 361 regularity-ord ox x refl not = record { proj1 = minimul<x x not ; proj2 = record {eq→ = reg0 ; eq← = λ () } } where
380 lemma = cong₂ (λ x not → minimul x not ) oiso {!!} 362 noto : o∅ o< (od→ord (ord→od ox))
381 363 noto = lemma {ox} {od→ord (ord→od ox)} diso (∅10 refl not) where
382 364 lemma : { ox oy : Ordinal {suc n}} → oy ≡ ox → o∅ o< ox → o∅ o< oy
383 365 lemma refl lt = lt
384 366 Min : Minimumo ox
385 367 Min = ominimal ox (∅10 refl not)
386 368 Mino : Minimumo (od→ord (ord→od ox ))
369 Mino = ominimal (od→ord (ord→od ox )) noto
370 m=mo : ox ≡ od→ord (ord→od ox ) → mino Mino ≡ mino Min
371 m=mo eq with ox
372 ... | xx = ?
373 reg0 : {y : Ordinal {suc n}} → def (Select (minimul x not) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁))) y → def od∅ y
374 reg0 {y} t with trio< y ( mino Mino )
375 reg0 {y} t | tri< a ¬b ¬c = {!!}
376 reg0 {y} t | tri≈ ¬a refl ¬c with o≡→¬c< {suc n} {ord→od (mino Mino)} refl lemma where
377 lemma : ord→od y c< ord→od (mino Mino)
378 lemma = subst (λ k → k c< ord→od (mino Mino) ) oiso {!!} -- (proj1 t)
379 reg0 {y} t | tri≈ ¬a b ¬c | ()
380 reg0 {y} t | tri> ¬a ¬b c with o<> y (mino Mino) lemma c where
381 lemma : y o< mino Mino
382 lemma = {!!}
383 reg0 {y} t | tri> ¬a ¬b c | ()