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

comparison ordinal.agda @ 256:6e1c60866788 release

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
orderd pair and product
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 29 Aug 2019 16:18:37 +0900
parents c10048d69614
children d9d178d1457c
comparison
equal deleted inserted replaced
232:fe8392f527eb 256:6e1c60866788
1 {-# OPTIONS --allow-unsolved-metas #-}
2 open import Level 1 open import Level
3 module ordinal where 2 module ordinal where
4 3
5 open import zf 4 open import zf
6 5
202 lemma : (y : Ordinal) → y o< ordinal lx (OSuc lx ox) → ψ y 201 lemma : (y : Ordinal) → y o< ordinal lx (OSuc lx ox) → ψ y
203 lemma y lt with osuc-≡< lt 202 lemma y lt with osuc-≡< lt
204 lemma y lt | case1 refl = proj1 ( TransFinite1 lx ox ) 203 lemma y lt | case1 refl = proj1 ( TransFinite1 lx ox )
205 lemma y lt | case2 lt1 = proj2 ( TransFinite1 lx ox ) y lt1 204 lemma y lt | case2 lt1 = proj2 ( TransFinite1 lx ox ) y lt1
206 205
207 -- we cannot prove this in intutionistic logic
208 -- (¬ (∀ y → ¬ ( ψ y ))) → (ψ y → p ) → p
209 -- postulate
210 -- TransFiniteExists : {n m l : Level} → ( ψ : Ordinal {n} → Set m )
211 -- → (exists : ¬ (∀ y → ¬ ( ψ y ) ))
212 -- → {p : Set l} ( P : { y : Ordinal {n} } → ψ y → p )
213 -- → p
214 --
215 -- Instead we prove
216 --
217 TransFiniteExists : {n m l : Level} → ( ψ : Ordinal {n} → Set m )
218 → {p : Set l} ( P : { y : Ordinal {n} } → ψ y → ¬ p )
219 → (exists : ¬ (∀ y → ¬ ( ψ y ) ))
220 → ¬ p
221 TransFiniteExists {n} {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p )
222 206
223 open import Ordinals 207 open import Ordinals
224 208
225 C-Ordinal : {n : Level} → Ordinals {suc n} 209 C-Ordinal : {n : Level} → Ordinals {suc n}
226 C-Ordinal {n} = record { 210 C-Ordinal {n} = record {
320 dz : lv (od→ord z) ≡ lx → OrdinalD lx 304 dz : lv (od→ord z) ≡ lx → OrdinalD lx
321 dz refl = OSuc lx (ord (od→ord z)) 305 dz refl = OSuc lx (ord (od→ord z))
322 dz<dz : (z=x : lv (od→ord z) ≡ lx ) → ord (od→ord z) d< dz z=x 306 dz<dz : (z=x : lv (od→ord z) ≡ lx ) → ord (od→ord z) d< dz z=x
323 dz<dz refl = s<refl 307 dz<dz refl = s<refl
324 308
325 ---
326 --- With assuption of OD is ordered, p ∨ ( ¬ p ) <=> axiom of choice
327 ---
328 record choiced ( X : OD) : Set (suc (suc n)) where
329 field
330 a-choice : OD
331 is-in : X ∋ a-choice
332
333 choice-func' : (X : OD ) → (p∨¬p : { n : Level } → ( p : Set (suc n) ) → p ∨ ( ¬ p )) → ¬ ( X == od∅ ) → choiced X
334 choice-func' X p∨¬p not = have_to_find where
335 ψ : ( ox : Ordinal {suc n}) → Set (suc (suc n))
336 ψ ox = (( x : Ordinal {suc n}) → x o< ox → ( ¬ def X x )) ∨ choiced X
337 lemma-ord : ( ox : Ordinal {suc n} ) → ψ ox
338 lemma-ord ox = TransFinite {n} {suc (suc n)} {ψ} caseΦ caseOSuc1 ox where
339 ∋-p' : (A x : OD ) → Dec ( A ∋ x )
340 ∋-p' A x with p∨¬p ( A ∋ x )
341 ∋-p' A x | case1 t = yes t
342 ∋-p' A x | case2 t = no t
343 ∀-imply-or : {n : Level} {A : Ordinal {suc n} → Set (suc n) } {B : Set (suc (suc n)) }
344 → ((x : Ordinal {suc n}) → A x ∨ B) → ((x : Ordinal {suc n}) → A x) ∨ B
345 ∀-imply-or {n} {A} {B} ∀AB with p∨¬p ((x : Ordinal {suc n}) → A x)
346 ∀-imply-or {n} {A} {B} ∀AB | case1 t = case1 t
347 ∀-imply-or {n} {A} {B} ∀AB | case2 x = case2 (lemma x) where
348 lemma : ¬ ((x : Ordinal {suc n}) → A x) → B
349 lemma not with p∨¬p B
350 lemma not | case1 b = b
351 lemma not | case2 ¬b = ⊥-elim (not (λ x → dont-orb (∀AB x) ¬b ))
352 caseΦ : (lx : Nat) → ( (x : Ordinal {suc n} ) → x o< ordinal lx (Φ lx) → ψ x) → ψ (ordinal lx (Φ lx) )
353 caseΦ lx prev with ∋-p' X ( ord→od (ordinal lx (Φ lx) ))
354 caseΦ lx prev | yes p = case2 ( record { a-choice = ord→od (ordinal lx (Φ lx)) ; is-in = p } )
355 caseΦ lx prev | no ¬p = lemma where
356 lemma1 : (x : Ordinal) → (((Suc (lv x) ≤ lx) ∨ (ord x d< Φ lx) → def X x → ⊥) ∨ choiced X)
357 lemma1 x with trio< x (ordinal lx (Φ lx))
358 lemma1 x | tri< a ¬b ¬c with prev (osuc x) (lemma2 a) where
359 lemma2 : x o< (ordinal lx (Φ lx)) → osuc x o< ordinal lx (Φ lx)
360 lemma2 (case1 lt) = case1 lt
361 lemma1 x | tri< a ¬b ¬c | case2 found = case2 found
362 lemma1 x | tri< a ¬b ¬c | case1 not_found = case1 ( λ lt df → not_found x <-osuc df )
363 lemma1 x | tri≈ ¬a refl ¬c = case1 ( λ lt → ⊥-elim (o<¬≡ refl lt ))
364 lemma1 x | tri> ¬a ¬b c = case1 ( λ lt → ⊥-elim (o<> lt c ))
365 lemma : ((x : Ordinal) → (Suc (lv x) ≤ lx) ∨ (ord x d< Φ lx) → def X x → ⊥) ∨ choiced X
366 lemma = ∀-imply-or lemma1
367 caseOSuc : (lx : Nat) (x : OrdinalD lx) → ψ ( ordinal lx x ) → ψ ( ordinal lx (OSuc lx x) )
368 caseOSuc lx x prev with ∋-p' X (ord→od record { lv = lx ; ord = x } )
369 caseOSuc lx x prev | yes p = case2 (record { a-choice = ord→od record { lv = lx ; ord = x } ; is-in = p })
370 caseOSuc lx x (case1 not_found) | no ¬p = case1 lemma where
371 lemma : (y : Ordinal) → (Suc (lv y) ≤ lx) ∨ (ord y d< OSuc lx x) → def X y → ⊥
372 lemma y lt with trio< y (ordinal lx x )
373 lemma y lt | tri< a ¬b ¬c = not_found y a
374 lemma y lt | tri≈ ¬a refl ¬c = subst (λ k → def X k → ⊥ ) diso ¬p
375 lemma y lt | tri> ¬a ¬b c with osuc-≡< lt
376 lemma y lt | tri> ¬a ¬b c | case1 refl = ⊥-elim ( ¬b refl )
377 lemma y lt | tri> ¬a ¬b c | case2 lt1 = ⊥-elim (o<> c lt1 )
378 caseOSuc lx x (case2 found) | no ¬p = case2 found
379 caseOSuc1 : (lx : Nat) (x : OrdinalD lx) → ((y : Ordinal) → y o< ordinal lx (OSuc lx x) → ψ y) →
380 ψ (record { lv = lx ; ord = OSuc lx x })
381 caseOSuc1 lx x lt = caseOSuc lx x (lt ( ordinal lx x ) (case2 s<refl))
382 have_to_find : choiced X
383 have_to_find with lemma-ord (od→ord X )
384 have_to_find | t = dont-or t ¬¬X∋x where
385 ¬¬X∋x : ¬ ((x : Ordinal) → (Suc (lv x) ≤ lv (od→ord X)) ∨ (ord x d< ord (od→ord X)) → def X x → ⊥)
386 ¬¬X∋x nn = not record {
387 eq→ = λ {x} lt → ⊥-elim (nn x (def→o< lt) lt)
388 ; eq← = λ {x} lt → ⊥-elim ( ¬x<0 lt )
389 }
390