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

comparison ordinal.agda @ 222:59771eb07df0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
TransFinite induction fixed
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 09 Aug 2019 16:54:30 +0900
parents 95a26d1698f4
children afc864169325
comparison
equal deleted inserted replaced
221:1709c80b7275 222:59771eb07df0
301 } 301 }
302 } 302 }
303 303
304 TransFinite : {n m : Level} → { ψ : Ordinal {suc n} → Set m } 304 TransFinite : {n m : Level} → { ψ : Ordinal {suc n} → Set m }
305 → ( ∀ (lx : Nat ) → ( (x : Ordinal {suc n} ) → x o< ordinal lx (Φ lx) → ψ x ) → ψ ( record { lv = lx ; ord = Φ lx } ) ) 305 → ( ∀ (lx : Nat ) → ( (x : Ordinal {suc n} ) → x o< ordinal lx (Φ lx) → ψ x ) → ψ ( record { lv = lx ; ord = Φ lx } ) )
306 → ( ∀ (lx : Nat ) → (x : OrdinalD lx ) → ψ ( record { lv = lx ; ord = x } ) → ψ ( record { lv = lx ; ord = OSuc lx x } ) ) 306 → ( ∀ (lx : Nat ) → (x : OrdinalD lx ) → ( (y : Ordinal {suc n} ) → y o< ordinal lx (OSuc lx x) → ψ y ) → ψ ( record { lv = lx ; ord = OSuc lx x } ) )
307 → ∀ (x : Ordinal) → ψ x 307 → ∀ (x : Ordinal) → ψ x
308 TransFinite {n} {m} {ψ} caseΦ caseOSuc x = proj1 (TransFinite1 (lv x) (ord x) ) where 308 TransFinite {n} {m} {ψ} caseΦ caseOSuc x = proj1 (TransFinite1 (lv x) (ord x) ) where
309 TransFinite1 : (lx : Nat) (ox : OrdinalD lx ) → ψ (ordinal lx ox) ∧ ( ( (x : Ordinal {suc n} ) → x o< ordinal lx (Φ lx) → ψ x ) ) 309 TransFinite1 : (lx : Nat) (ox : OrdinalD lx ) → ψ (ordinal lx ox) ∧ ( ( (x : Ordinal {suc n} ) → x o< ordinal lx ox → ψ x ) )
310 TransFinite1 Zero (Φ 0) = record { proj1 = caseΦ Zero lemma ; proj2 = lemma1 } where 310 TransFinite1 Zero (Φ 0) = record { proj1 = caseΦ Zero lemma ; proj2 = lemma1 } where
311 lemma : (x : Ordinal) → x o< ordinal Zero (Φ Zero) → ψ x 311 lemma : (x : Ordinal) → x o< ordinal Zero (Φ Zero) → ψ x
312 lemma x (case1 ()) 312 lemma x (case1 ())
313 lemma x (case2 ()) 313 lemma x (case2 ())
314 lemma1 : (x : Ordinal) → x o< ordinal Zero (Φ Zero) → ψ x 314 lemma1 : (x : Ordinal) → x o< ordinal Zero (Φ Zero) → ψ x
318 lemma0 : (ly : Nat) (oy : OrdinalD ly ) → ordinal ly oy o< ordinal lx (Φ lx) → ψ (ordinal ly oy) 318 lemma0 : (ly : Nat) (oy : OrdinalD ly ) → ordinal ly oy o< ordinal lx (Φ lx) → ψ (ordinal ly oy)
319 lemma0 ly oy lt = proj2 ( TransFinite1 lx (Φ lx) ) (ordinal ly oy) lt 319 lemma0 ly oy lt = proj2 ( TransFinite1 lx (Φ lx) ) (ordinal ly oy) lt
320 lemma : (ly : Nat) (oy : OrdinalD ly ) → ordinal ly oy o< ordinal (Suc lx) (Φ (Suc lx)) → ψ (ordinal ly oy) 320 lemma : (ly : Nat) (oy : OrdinalD ly ) → ordinal ly oy o< ordinal (Suc lx) (Φ (Suc lx)) → ψ (ordinal ly oy)
321 lemma lx1 ox1 (case1 lt) with <-∨ lt 321 lemma lx1 ox1 (case1 lt) with <-∨ lt
322 lemma lx (Φ lx) (case1 lt) | case1 refl = proj1 ( TransFinite1 lx (Φ lx) ) 322 lemma lx (Φ lx) (case1 lt) | case1 refl = proj1 ( TransFinite1 lx (Φ lx) )
323 lemma lx (Φ lx) (case1 lt) | case2 (s≤s lt1) = lemma0 lx (Φ lx) (case1 (s≤s lt1)) 323 lemma lx (Φ lx) (case1 lt) | case2 lt1 = lemma0 lx (Φ lx) (case1 lt1)
324 lemma lx (OSuc lx ox1) (case1 lt) | case1 refl = caseOSuc lx ox1 ( lemma lx ox1 (case1 a<sa)) 324 lemma lx (OSuc lx ox1) (case1 lt) | case1 refl = caseOSuc lx ox1 lemma2 where
325 lemma lx1 (OSuc lx1 ox1) (case1 lt) | case2 lt1 = caseOSuc lx1 ox1 ( lemma lx1 ox1 (case1 (<-trans lt1 a<sa ))) 325 lemma2 : (y : Ordinal) → (Suc (lv y) ≤ lx) ∨ (ord y d< OSuc lx ox1) → ψ y
326 TransFinite1 lx (OSuc lx ox) = record { proj1 = caseOSuc lx ox (proj1 (TransFinite1 lx ox )) ; proj2 = proj2 (TransFinite1 lx ox )} 326 lemma2 y lt1 with osuc-≡< lt1
327 lemma2 y lt1 | case1 refl = lemma lx ox1 (case1 a<sa)
328 lemma2 y lt1 | case2 t = proj2 (TransFinite1 lx ox1) y t
329 lemma lx1 (OSuc lx1 ox1) (case1 lt) | case2 lt1 = caseOSuc lx1 ox1 lemma2 where
330 lemma2 : (y : Ordinal) → (Suc (lv y) ≤ lx1) ∨ (ord y d< OSuc lx1 ox1) → ψ y
331 lemma2 y lt2 with osuc-≡< lt2
332 lemma2 y lt2 | case1 refl = lemma lx1 ox1 (ordtrans lt2 (case1 lt))
333 lemma2 y lt2 | case2 (case1 lt3) = proj2 (TransFinite1 lx (Φ lx)) y (case1 (<-trans lt3 lt1 ))
334 lemma2 y lt2 | case2 (case2 lt3) with d<→lv lt3
335 ... | refl = proj2 (TransFinite1 lx (Φ lx)) y (case1 lt1)
336 TransFinite1 lx (OSuc lx ox) = record { proj1 = caseOSuc lx ox lemma ; proj2 = lemma } where
337 lemma : (y : Ordinal) → y o< ordinal lx (OSuc lx ox) → ψ y
338 lemma y lt with osuc-≡< lt
339 lemma y lt | case1 refl = proj1 ( TransFinite1 lx ox )
340 lemma y lt | case2 lt1 = proj2 ( TransFinite1 lx ox ) y lt1
327 341
328 -- we cannot prove this in intutionistic logic 342 -- we cannot prove this in intutionistic logic
329 -- (¬ (∀ y → ¬ ( ψ y ))) → (ψ y → p ) → p 343 -- (¬ (∀ y → ¬ ( ψ y ))) → (ψ y → p ) → p
330 -- postulate 344 -- postulate
331 -- TransFiniteExists : {n m l : Level} → ( ψ : Ordinal {n} → Set m ) 345 -- TransFiniteExists : {n m l : Level} → ( ψ : Ordinal {n} → Set m )
339 → {p : Set l} ( P : { y : Ordinal {n} } → ψ y → ¬ p ) 353 → {p : Set l} ( P : { y : Ordinal {n} } → ψ y → ¬ p )
340 → (exists : ¬ (∀ y → ¬ ( ψ y ) )) 354 → (exists : ¬ (∀ y → ¬ ( ψ y ) ))
341 → ¬ p 355 → ¬ p
342 TransFiniteExists {n} {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p ) 356 TransFiniteExists {n} {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p )
343 357
358 open import Ordinals
359
360 C-Ordinal : {n : Level } → Ordinals {suc n}
361 C-Ordinal {n} = record {
362 ord = Ordinal {suc n}
363 ; o∅ = o∅
364 ; osuc = osuc
365 ; _o<_ = _o<_
366 ; isOrdinal = record {
367 Otrans = ordtrans
368 ; OTri = trio<
369 ; ¬x<0 = ¬x<0
370 ; <-osuc = <-osuc
371 ; osuc-≡< = osuc-≡<
372 ; TransFinite = TransFinite1
373 }
374 } where
375 ord1 : Set (suc n)
376 ord1 = Ordinal {suc n}
377 TransFinite1 : { ψ : ord1 → Set (suc (suc n)) }
378 → ( (x : ord1) → ( (y : ord1 ) → y o< x → ψ y ) → ψ x )
379 → ∀ (x : ord1) → ψ x
380 TransFinite1 {ψ} lt x = TransFinite {n} {suc (suc n)} {ψ} caseΦ caseOSuc x where
381 caseΦ : (lx : Nat) → ((x₁ : Ordinal) → x₁ o< ordinal lx (Φ lx) → ψ x₁) →
382 ψ (record { lv = lx ; ord = Φ lx })
383 caseΦ lx prev = lt (ordinal lx (Φ lx) ) prev
384 caseOSuc : (lx : Nat) (x₁ : OrdinalD lx) → ((y : Ordinal) → y o< ordinal lx (OSuc lx x₁) → ψ y) →
385 ψ (record { lv = lx ; ord = OSuc lx x₁ })
386 caseOSuc lx ox prev = lt (ordinal lx (OSuc lx ox)) prev