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

comparison ordinal.agda @ 203:8edd2a13a7f3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fixing transfinte induction...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 31 Jul 2019 12:40:02 +0900
parents ed88384b5102
children d4802eb159ff
comparison
equal deleted inserted replaced
202:ed88384b5102 203:8edd2a13a7f3
110 nat-≡< refl lt = nat-<≡ lt 110 nat-≡< refl lt = nat-<≡ lt
111 111
112 ¬a≤a : {la : Nat} → Suc la ≤ la → ⊥ 112 ¬a≤a : {la : Nat} → Suc la ≤ la → ⊥
113 ¬a≤a (s≤s lt) = ¬a≤a lt 113 ¬a≤a (s≤s lt) = ¬a≤a lt
114 114
115 a<sa : {la : Nat} → la < Suc la
116 a<sa {Zero} = s≤s z≤n
117 a<sa {Suc la} = s≤s a<sa
118
115 =→¬< : {x : Nat } → ¬ ( x < x ) 119 =→¬< : {x : Nat } → ¬ ( x < x )
116 =→¬< {Zero} () 120 =→¬< {Zero} ()
117 =→¬< {Suc x} (s≤s lt) = =→¬< lt 121 =→¬< {Suc x} (s≤s lt) = =→¬< lt
118 122
123 <-∨ : { x y : Nat } → x < Suc y → ( (x ≡ y ) ∨ (x < y) )
124 <-∨ {Zero} {Zero} (s≤s z≤n) = case1 refl
125 <-∨ {Zero} {Suc y} (s≤s lt) = case2 (s≤s z≤n)
126 <-∨ {Suc x} {Zero} (s≤s ())
127 <-∨ {Suc x} {Suc y} (s≤s lt) with <-∨ {x} {y} lt
128 <-∨ {Suc x} {Suc y} (s≤s lt) | case1 eq = case1 (cong (λ k → Suc k ) eq)
129 <-∨ {Suc x} {Suc y} (s≤s lt) | case2 lt1 = case2 (s≤s lt1)
130
119 case12-⊥ : {n : Level} {x y : Ordinal {suc n}} → lv x < lv y → ord x d< ord y → ⊥ 131 case12-⊥ : {n : Level} {x y : Ordinal {suc n}} → lv x < lv y → ord x d< ord y → ⊥
120 case12-⊥ {x} {y} lt1 lt2 with d<→lv lt2 132 case12-⊥ {x} {y} lt1 lt2 with d<→lv lt2
121 ... | refl = nat-≡< refl lt1 133 ... | refl = nat-≡< refl lt1
122 134
123 case21-⊥ : {n : Level} {x y : Ordinal {suc n}} → lv x < lv y → ord y d< ord x → ⊥ 135 case21-⊥ : {n : Level} {x y : Ordinal {suc n}} → lv x < lv y → ord y d< ord x → ⊥
124 case21-⊥ {x} {y} lt1 lt2 with d<→lv lt2 136 case21-⊥ {x} {y} lt1 lt2 with d<→lv lt2
125 ... | refl = nat-≡< refl lt1 137 ... | refl = nat-≡< refl lt1
126 138
127 o<¬≡ : {n : Level } { ox oy : Ordinal {n}} → ox ≡ oy → ox o< oy → ⊥ 139 o<¬≡ : {n : Level } { ox oy : Ordinal {suc n}} → ox ≡ oy → ox o< oy → ⊥
128 o<¬≡ {_} {ox} {ox} refl (case1 lt) = =→¬< lt 140 o<¬≡ {_} {ox} {ox} refl (case1 lt) = =→¬< lt
129 o<¬≡ {_} {ox} {ox} refl (case2 (s< lt)) = trio<≡ refl lt 141 o<¬≡ {_} {ox} {ox} refl (case2 (s< lt)) = trio<≡ refl lt
130 142
131 ¬x<0 : {n : Level} → { x : Ordinal {suc n} } → ¬ ( x o< o∅ {suc n} ) 143 ¬x<0 : {n : Level} → { x : Ordinal {suc n} } → ¬ ( x o< o∅ {suc n} )
132 ¬x<0 {n} {x} (case1 ()) 144 ¬x<0 {n} {x} (case1 ())
313 ; reflexive = case1 325 ; reflexive = case1
314 ; trans = OrdTrans 326 ; trans = OrdTrans
315 } 327 }
316 } 328 }
317 329
318 TransFinite : {n m : Level} → { ψ : Ordinal {n} → Set m } 330 TransFinite : {n m : Level} → { ψ : Ordinal {suc n} → Set m }
319 → ( ∀ (lx : Nat ) → ψ ( record { lv = lx ; ord = Φ lx } ) ) 331 → ( ∀ (lx : Nat ) → ( (x : Ordinal {suc n} ) → x o< ordinal lx (Φ lx) → ψ x ) → ψ ( record { lv = lx ; ord = Φ lx } ) )
320 → ( ∀ (lx : Nat ) → (x : OrdinalD lx ) → ψ ( record { lv = lx ; ord = x } ) → ψ ( record { lv = lx ; ord = OSuc lx x } ) ) 332 → ( ∀ (lx : Nat ) → (x : OrdinalD lx ) → ψ ( record { lv = lx ; ord = x } ) → ψ ( record { lv = lx ; ord = OSuc lx x } ) )
321 → ∀ (x : Ordinal) → ψ x 333 → ∀ (x : Ordinal) → ψ x
322 TransFinite caseΦ caseOSuc record { lv = lv ; ord = (Φ (lv)) } = caseΦ lv 334 TransFinite {n} {m} {ψ} caseΦ caseOSuc x = TransFinite1 (lv x) (ord x) where
323 TransFinite caseΦ caseOSuc record { lv = lx ; ord = (OSuc lx ox) } = 335 TransFinite1 : (lx : Nat) (ox : OrdinalD lx ) → ψ (ordinal lx ox)
324 caseOSuc lx ox (TransFinite caseΦ caseOSuc record { lv = lx ; ord = ox }) 336 TransFinite1 Zero (Φ 0) = caseΦ Zero lemma where
337 lemma : (x : Ordinal) → x o< ordinal Zero (Φ Zero) → ψ x
338 lemma x (case1 ())
339 lemma x (case2 ())
340 TransFinite1 (Suc lx) (Φ (Suc lx)) = caseΦ (Suc lx) lemma where
341 lemma : (x : Ordinal) → x o< ordinal (Suc lx) (Φ (Suc lx)) → ψ x
342 lemma (ordinal lx1 ox1) (case1 lt) with <-∨ lt
343 lemma (ordinal lx (Φ lx)) (case1 lt) | case1 refl = TransFinite1 lx (Φ lx)
344 lemma (ordinal lx (OSuc lx ox1)) (case1 lt) | case1 refl = caseOSuc lx ox1 ( lemma (ordinal lx ox1) (case1 a<sa))
345 lemma (ordinal Zero (Φ 0)) (case1 lt) | case2 (s≤s lt1) = caseΦ Zero ( λ x lt → ⊥-elim (¬x<0 lt) )
346 lemma (ordinal (Suc lx1) (Φ (Suc lx1))) (case1 lt) | case2 (s≤s lt1) = caseΦ (Suc lx1) lemma2 where
347 lemma2 : (y : Ordinal) → (Suc (lv y) ≤ Suc lx1) ∨ (ord y d< Φ (Suc lx1)) → ψ y
348 lemma2 y (case1 lt2 ) = {!!}
349 lemma (ordinal lx1 (OSuc lx1 ox1)) (case1 lt) | case2 lt1 = caseOSuc lx1 ox1 ( lemma (ordinal lx1 ox1) (case1 (<-trans lt1 a<sa )))
350 TransFinite1 lx (OSuc lx ox) = caseOSuc lx ox (TransFinite1 lx ox )
325 351
326 -- we cannot prove this in intutionistic logic 352 -- we cannot prove this in intutionistic logic
327 -- (¬ (∀ y → ¬ ( ψ y ))) → (ψ y → p ) → p 353 -- (¬ (∀ y → ¬ ( ψ y ))) → (ψ y → p ) → p
328 -- postulate 354 -- postulate
329 -- TransFiniteExists : {n m l : Level} → ( ψ : Ordinal {n} → Set m ) 355 -- TransFiniteExists : {n m l : Level} → ( ψ : Ordinal {n} → Set m )