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

comparison ordinal.agda @ 213:22d435172d1a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
separate logic and nat
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 02 Aug 2019 12:17:10 +0900
parents d4802eb159ff
children eee983e4b402
comparison
equal deleted inserted replaced
212:0a1804cc9d0a 213:22d435172d1a
5 open import zf 5 open import zf
6 6
7 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) 7 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ )
8 open import Data.Empty 8 open import Data.Empty
9 open import Relation.Binary.PropositionalEquality 9 open import Relation.Binary.PropositionalEquality
10 open import logic
11 open import nat
10 12
11 data OrdinalD {n : Level} : (lv : Nat) → Set n where 13 data OrdinalD {n : Level} : (lv : Nat) → Set n where
12 Φ : (lv : Nat) → OrdinalD lv 14 Φ : (lv : Nat) → OrdinalD lv
13 OSuc : (lv : Nat) → OrdinalD {n} lv → OrdinalD lv 15 OSuc : (lv : Nat) → OrdinalD {n} lv → OrdinalD lv
14 16
97 99
98 osucc : {n : Level} {ox oy : Ordinal {n}} → oy o< ox → osuc oy o< osuc ox 100 osucc : {n : Level} {ox oy : Ordinal {n}} → oy o< ox → osuc oy o< osuc ox
99 osucc {n} {ox} {oy} (case1 x) = case1 x 101 osucc {n} {ox} {oy} (case1 x) = case1 x
100 osucc {n} {ox} {oy} (case2 x) with d<→lv x 102 osucc {n} {ox} {oy} (case2 x) with d<→lv x
101 ... | refl = case2 (s< x) 103 ... | refl = case2 (s< x)
102
103 nat-<> : { x y : Nat } → x < y → y < x → ⊥
104 nat-<> (s≤s x<y) (s≤s y<x) = nat-<> x<y y<x
105
106 nat-<≡ : { x : Nat } → x < x → ⊥
107 nat-<≡ (s≤s lt) = nat-<≡ lt
108
109 nat-≡< : { x y : Nat } → x ≡ y → x < y → ⊥
110 nat-≡< refl lt = nat-<≡ lt
111
112 ¬a≤a : {la : Nat} → Suc la ≤ la → ⊥
113 ¬a≤a (s≤s lt) = ¬a≤a lt
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
119 =→¬< : {x : Nat } → ¬ ( x < x )
120 =→¬< {Zero} ()
121 =→¬< {Suc x} (s≤s lt) = =→¬< lt
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 104
131 case12-⊥ : {n : Level} {x y : Ordinal {suc n}} → lv x < lv y → ord x d< ord y → ⊥ 105 case12-⊥ : {n : Level} {x y : Ordinal {suc n}} → lv x < lv y → ord x d< ord y → ⊥
132 case12-⊥ {x} {y} lt1 lt2 with d<→lv lt2 106 case12-⊥ {x} {y} lt1 lt2 with d<→lv lt2
133 ... | refl = nat-≡< refl lt1 107 ... | refl = nat-≡< refl lt1
134 108
342 lemma1 x (case2 ()) 316 lemma1 x (case2 ())
343 TransFinite1 (Suc lx) (Φ (Suc lx)) = record { proj1 = caseΦ (Suc lx) (λ x → lemma (lv x) (ord x)) ; proj2 = (λ x → lemma (lv x) (ord x)) } where 317 TransFinite1 (Suc lx) (Φ (Suc lx)) = record { proj1 = caseΦ (Suc lx) (λ x → lemma (lv x) (ord x)) ; proj2 = (λ x → lemma (lv x) (ord x)) } where
344 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)
345 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
346 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)
347 lemma lx1 ox1 (case1 lt) with <-∨ lt 321 lemma lx1 ox1 (case1 lt) with <-∨ lt
348 lemma lx (Φ lx) (case1 lt) | case1 refl = proj1 ( TransFinite1 lx (Φ lx) ) 322 lemma lx (Φ lx) (case1 lt) | case1 refl = proj1 ( TransFinite1 lx (Φ lx) )
349 lemma lx (OSuc lx ox1) (case1 lt) | case1 refl = caseOSuc lx ox1 ( lemma lx ox1 (case1 a<sa)) 323 lemma lx (Φ lx) (case1 lt) | case2 (s≤s lt1) = lemma0 lx (Φ lx) (case1 (s≤s lt1))
350 lemma lx (Φ lx) (case1 lt) | case2 (s≤s lt1) = lemma0 lx (Φ lx) (case1 (s≤s lt1)) 324 lemma lx (OSuc lx ox1) (case1 lt) | case1 refl = caseOSuc lx ox1 ( lemma lx ox1 (case1 a<sa))
351 lemma lx1 (OSuc lx1 ox1) (case1 lt) | case2 lt1 = caseOSuc lx1 ox1 ( lemma lx1 ox1 (case1 (<-trans lt1 a<sa ))) 325 lemma lx1 (OSuc lx1 ox1) (case1 lt) | case2 lt1 = caseOSuc lx1 ox1 ( lemma lx1 ox1 (case1 (<-trans lt1 a<sa )))
352 TransFinite1 lx (OSuc lx ox) = record { proj1 = caseOSuc lx ox (proj1 (TransFinite1 lx ox )) ; proj2 = proj2 (TransFinite1 lx ox )} 326 TransFinite1 lx (OSuc lx ox) = record { proj1 = caseOSuc lx ox (proj1 (TransFinite1 lx ox )) ; proj2 = proj2 (TransFinite1 lx ox )}
353 327
354 -- we cannot prove this in intutionistic logic 328 -- we cannot prove this in intutionistic logic
355 -- (¬ (∀ y → ¬ ( ψ y ))) → (ψ y → p ) → p 329 -- (¬ (∀ y → ¬ ( ψ y ))) → (ψ y → p ) → p
356 -- postulate 330 -- postulate