Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff ordinal.agda @ 74:819da8c08f05
ordinal atomical successor?
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 01 Jun 2019 19:19:40 +0900 |
| parents | dd430a95610f |
| children | 714470702a8b |
line wrap: on
line diff
--- a/ordinal.agda Sat Jun 01 18:17:24 2019 +0900 +++ b/ordinal.agda Sat Jun 01 19:19:40 2019 +0900 @@ -41,12 +41,6 @@ o<-subst : {n : Level } {Z X z x : Ordinal {n}} → Z o< X → Z ≡ z → X ≡ x → z o< x o<-subst df refl refl = df -osuc : {n : Level} ( x : Ordinal {n} ) → Ordinal {n} -osuc record { lv = 0 ; ord = (Φ lv) } = record { lv = 0 ; ord = OSuc 0 (Φ lv) } -osuc record { lv = Suc lx ; ord = (Φ (Suc lv)) } = record { lv = Suc lx ; ord = ℵ lv } -osuc record { lv = lx ; ord = (OSuc lx ox ) } = record { lv = lx ; ord = OSuc lx (OSuc lx ox) } -osuc record { lv = Suc lx ; ord = ℵ lx } = record { lv = Suc lx ; ord = OSuc (Suc lx) (ℵ lx) } - open import Data.Nat.Properties open import Data.Empty open import Data.Unit using ( ⊤ ) @@ -63,36 +57,6 @@ s<refl {n} {lv} {OSuc lv x} = s< s<refl s<refl {n} {Suc lv} {ℵ lv} = ℵs< -<-osuc : {n : Level} { x : Ordinal {n} } → x o< osuc x -<-osuc {n} { record { lv = 0 ; ord = Φ 0 } } = case2 Φ< -<-osuc {n} { record { lv = (Suc lv) ; ord = Φ (Suc lv) } } = case2 ℵΦ< -<-osuc {n} {record { lv = Zero ; ord = OSuc .0 ox }} = case2 ( s< s<refl ) -<-osuc {n} {record { lv = Suc lv₁ ; ord = OSuc .(Suc lv₁) ox }} = case2 ( s< s<refl ) -<-osuc {n} { record { lv = .(Suc lv₁) ; ord = (ℵ lv₁) } } = case2 ℵs< - -osuc-lveq : {n : Level} { x : Ordinal {n} } → lv x ≡ lv ( osuc x ) -osuc-lveq {n} {record { lv = 0 ; ord = Φ 0 }} = refl -osuc-lveq {n} {record { lv = Suc lv ; ord = Φ (Suc lv) }} = refl -osuc-lveq {n} {record { lv = Zero ; ord = OSuc .0 ord₁ }} = refl -osuc-lveq {n} {record { lv = Suc lv₁ ; ord = OSuc .(Suc lv₁) ord₁ }} = refl -osuc-lveq {n} {record { lv = .(Suc lv₁) ; ord = ℵ lv₁ }} = refl - -nat-<> : { x y : Nat } → x < y → y < x → ⊥ -nat-<> (s≤s x<y) (s≤s y<x) = nat-<> x<y y<x - -osuc-< : {n : Level} { x y : Ordinal {n} } → y o< osuc x → x o< y → ⊥ -osuc-< {n} {record { lv = .0 ; ord = Φ .0 }} {record { lv = .(Suc _) ; ord = ord }} (case1 ()) (case1 (s≤s z≤n)) -osuc-< {n} {record { lv = .0 ; ord = OSuc .0 ord₁ }} {record { lv = .(Suc _) ; ord = ord }} (case1 ()) (case1 (s≤s z≤n)) -osuc-< {n} {record { lv = lx ; ord = xo }} {record { lv = ly ; ord = yo }} (case1 lt1) (case1 lt2) with osuc-lveq {n} {record { lv = lx ; ord = xo }} -osuc-< {n} {record { lv = Zero ; ord = Φ .0 }} {record { lv = ly ; ord = yo }} (case1 lt1) (case1 lt2) | eq = nat-<> lt1 lt2 -osuc-< {n} {record { lv = Suc lx ; ord = Φ .(Suc lx) }} {record { lv = ly ; ord = yo }} (case1 lt1) (case1 lt2) | eq = nat-<> lt1 lt2 -osuc-< {n} {record { lv = Zero ; ord = OSuc .0 xo }} {record { lv = ly ; ord = yo }} (case1 lt1) (case1 lt2) | eq = nat-<> lt1 lt2 -osuc-< {n} {record { lv = Suc lx ; ord = OSuc .(Suc lx) xo }} {record { lv = ly ; ord = yo }} (case1 lt1) (case1 lt2) | eq = nat-<> lt1 lt2 -osuc-< {n} {record { lv = .(Suc lv₁) ; ord = ℵ lv₁ }} {record { lv = ly ; ord = yo }} (case1 lt1) (case1 lt2) | refl = nat-<> lt1 lt2 -osuc-< {n} {x} {y} (case1 x₁) (case2 x₂) = {!!} -osuc-< {n} {x} {y} (case2 x₁) (case1 x₂) = {!!} -osuc-< {n} {x} {y} (case2 x₁) (case2 x₂) = {!!} - open import Relation.Binary.HeterogeneousEquality using (_≅_;refl) ordinal-cong : {n : Level} {x y : Ordinal {n}} → @@ -160,6 +124,61 @@ d<→lv ℵs< = refl d<→lv (ℵss< _) = refl +osuc : {n : Level} ( x : Ordinal {n} ) → Ordinal {n} +osuc record { lv = 0 ; ord = (Φ lv) } = record { lv = 0 ; ord = OSuc 0 (Φ lv) } +osuc record { lv = Suc lx ; ord = (Φ (Suc lv)) } = record { lv = Suc lx ; ord = ℵ lv } +osuc record { lv = 0 ; ord = (OSuc 0 ox ) } = record { lv = 0 ; ord = OSuc 0 (OSuc 0 ox) } +osuc record { lv = Suc lx ; ord = (OSuc (Suc lx) ox ) } = record { lv = Suc lx ; ord = OSuc (Suc lx) (OSuc (Suc lx) ox) } +osuc record { lv = Suc lx ; ord = ℵ lx } = record { lv = Suc lx ; ord = OSuc (Suc lx) (ℵ lx) } + +<-osuc : {n : Level} { x : Ordinal {n} } → x o< osuc x +<-osuc {n} { record { lv = 0 ; ord = Φ 0 } } = case2 Φ< +<-osuc {n} { record { lv = (Suc lv) ; ord = Φ (Suc lv) } } = case2 ℵΦ< +<-osuc {n} {record { lv = Zero ; ord = OSuc .0 ox }} = case2 ( s< s<refl ) +<-osuc {n} {record { lv = Suc lv₁ ; ord = OSuc .(Suc lv₁) ox }} = case2 ( s< s<refl ) +<-osuc {n} { record { lv = .(Suc lv₁) ; ord = (ℵ lv₁) } } = case2 ℵs< + +osuc-lveq : {n : Level} { x : Ordinal {n} } → lv x ≡ lv ( osuc x ) +osuc-lveq {n} {record { lv = 0 ; ord = Φ 0 }} = refl +osuc-lveq {n} {record { lv = Suc lv ; ord = Φ (Suc lv) }} = refl +osuc-lveq {n} {record { lv = Zero ; ord = OSuc .0 ord₁ }} = refl +osuc-lveq {n} {record { lv = Suc lv₁ ; ord = OSuc .(Suc lv₁) ord₁ }} = refl +osuc-lveq {n} {record { lv = .(Suc lv₁) ; ord = ℵ lv₁ }} = refl + +nat-<> : { x y : Nat } → x < y → y < x → ⊥ +nat-<> (s≤s x<y) (s≤s y<x) = nat-<> x<y y<x + +nat-<≡ : { x : Nat } → x < x → ⊥ +nat-<≡ (s≤s lt) = nat-<≡ lt + +osuc-< : {n : Level} { x y : Ordinal {n} } → y o< osuc x → x o< y → ⊥ +osuc-< {n} {record { lv = .0 ; ord = Φ .0 }} {record { lv = .(Suc _) ; ord = ord }} (case1 ()) (case1 (s≤s z≤n)) +osuc-< {n} {record { lv = .0 ; ord = OSuc .0 ord₁ }} {record { lv = .(Suc _) ; ord = ord }} (case1 ()) (case1 (s≤s z≤n)) +osuc-< {n} {record { lv = Suc lx ; ord = Φ .(Suc lx) }} {record { lv = ly ; ord = yo }} (case1 lt1) (case1 lt2) = nat-<> lt1 lt2 +osuc-< {n} {record { lv = Suc lx ; ord = OSuc .(Suc lx) xo }} {record { lv = ly ; ord = yo }} (case1 lt1) (case1 lt2) = nat-<> lt1 lt2 +osuc-< {n} {record { lv = .(Suc lv₁) ; ord = ℵ lv₁ }} {record { lv = ly ; ord = yo }} (case1 lt1) (case1 lt2) = nat-<> lt1 lt2 +osuc-< {n} {x} {y} (case1 x₁) (case2 x₂) with d<→lv x₂ | osuc-lveq {n} {x} +... | refl | eq = {!!} +osuc-< {n} {x} {y} (case2 x₁) (case1 x₂) with d<→lv x₁ | osuc-lveq {n} {x} +... | refl | eq = {!!} +osuc-< {n} {record { lv = Zero ; ord = Φ .0 }} {record { lv = Zero ; ord = Φ .0 }} (case2 Φ<) (case2 ()) +osuc-< {n} {record { lv = Suc lv₁ ; ord = Φ .(Suc lv₁) }} {record { lv = Zero ; ord = Φ .0 }} (case2 ()) (case2 x₂) +osuc-< {n} {record { lv = lv₁ ; ord = Φ .lv₁ }} {record { lv = Suc lv₂ ; ord = Φ .(Suc lv₂) }} (case2 x₁) (case2 ()) +osuc-< {n} {record { lv = .0 ; ord = Φ .0 }} {record { lv = Zero ; ord = OSuc .0 ord₁ }} (case2 (s< ())) (case2 Φ<) +osuc-< {n} {record { lv = .1 ; ord = ℵ Zero }} {record { lv = .1 ; ord = ℵ Zero }} (case2 ℵs<) (case2 ()) +osuc-< {n} {record { lv = .1 ; ord = ℵ Zero }} {record { lv = .1 ; ord = ℵ Zero }} (case2 (ℵss< x₁)) (case2 ()) +osuc-< {n} {record { lv = .1 ; ord = ℵ Zero }} {record { lv = .(Suc (Suc lv₂)) ; ord = ℵ Suc lv₂ }} (case2 ()) (case2 x₂) +osuc-< {n} {record { lv = .(Suc (Suc lv₁)) ; ord = ℵ Suc lv₁ }} {record { lv = .(Suc (Suc lv₁)) ; ord = ℵ .(Suc lv₁) }} (case2 ℵs<) (case2 ()) +osuc-< {n} {record { lv = .(Suc (Suc lv₁)) ; ord = ℵ Suc lv₁ }} {record { lv = .(Suc (Suc lv₁)) ; ord = ℵ .(Suc lv₁) }} (case2 (ℵss< x₁)) (case2 ()) +osuc-< {n} {record { lv = Suc lv₁ ; ord = .(Φ (Suc lv₁)) }} {record { lv = .(Suc lv₁) ; ord = (OSuc (Suc lv₁) y) }} (case2 (ℵ< x)) (case2 Φ<) = {!!} +osuc-< {n} {record { lv = Zero ; ord = (OSuc 0 ox) }} {record { lv = .0 ; ord = (OSuc 0 oy) }} (case2 (s< c1)) (case2 (s< c2)) = + osuc-< {n} {record { lv = Zero ; ord = ox }} {record { lv = 0 ; ord = oy }} (case2 {!!}) (case2 c2) +osuc-< {n} {record { lv = Suc lv₁ ; ord = .(OSuc (Suc lv₁) _) }} {record { lv = .(Suc lv₁) ; ord = .(OSuc (Suc lv₁) _) }} (case2 (s< c1)) (case2 (s< c2)) = {!!} +osuc-< {n} {record { lv = .(Suc _) ; ord = .(OSuc (Suc _) _) }} {record { lv = .(Suc _) ; ord = .(ℵ _) }} (case2 (ℵss< c1)) (case2 (ℵ< x)) = {!!} +osuc-< {n} {record { lv = .(Suc _) ; ord = .(ℵ _) }} {record { lv = .(Suc _) ; ord = .(OSuc (Suc _) (ℵ _)) }} (case2 (s< c1)) (case2 ℵs<) = {!!} +osuc-< {n} {record { lv = .(Suc _) ; ord = .(ℵ _) }} {record { lv = .(Suc _) ; ord = .(OSuc (Suc _) _) }} (case2 (s< c1)) (case2 (ℵss< c2)) = {!!} + + xsyℵ : {n : Level} {lx : Nat} {x y : OrdinalD {n} lx } → x d< y → ¬ℵ y → ¬ℵ x xsyℵ {_} {_} {Φ lv₁} {y} x<y t = ¬ℵΦ xsyℵ {_} {_} {OSuc lv₁ x} {OSuc lv₁ y} (s< x<y) (¬ℵs t) = ¬ℵs ( xsyℵ x<y t)