Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 75:714470702a8b
Union done
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 02 Jun 2019 10:53:52 +0900 |
| parents | 819da8c08f05 |
| children | 8e8f54e7a030 |
| files | ordinal.agda |
| diffstat | 1 files changed, 68 insertions(+), 68 deletions(-) [+] |
line wrap: on
line diff
--- a/ordinal.agda Sat Jun 01 19:19:40 2019 +0900 +++ b/ordinal.agda Sun Jun 02 10:53:52 2019 +0900 @@ -5,7 +5,7 @@ open import zf open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) - +open import Data.Empty open import Relation.Binary.PropositionalEquality data OrdinalD {n : Level} : (lv : Nat) → Set n where @@ -38,11 +38,34 @@ _o<_ : {n : Level} ( x y : Ordinal ) → Set n _o<_ x y = (lv x < lv y ) ∨ ( ord x d< ord y ) +s<refl : {n : Level } {lx : Nat } { x : OrdinalD {n} lx } → x d< OSuc lx x +s<refl {n} {lv} {Φ lv} = Φ< +s<refl {n} {lv} {OSuc lv x} = s< s<refl +s<refl {n} {Suc lv} {ℵ lv} = ℵs< + +trio<> : {n : Level} → {lx : Nat} {x : OrdinalD {n} lx } { y : OrdinalD lx } → y d< x → x d< y → ⊥ +trio<> {n} {lx} {.(OSuc lx _)} {.(OSuc lx _)} (s< s) (s< t) = trio<> s t +trio<> {_} {.(Suc _)} {.(OSuc (Suc _) (ℵ _))} {.(ℵ _)} ℵs< (ℵ< {_} {.(ℵ _)} ()) +trio<> {_} {.(Suc _)} {.(ℵ _)} {.(OSuc (Suc _) (ℵ _))} (ℵ< ()) ℵs< +trio<> {n} {lx} {.(OSuc lx _)} {.(Φ lx)} Φ< () +trio<> {n} {.(Suc _)} {.(ℵ _)} {.(Φ (Suc _))} ℵΦ< () +trio<> {n} {.(Suc _)} {.(ℵ _)} {.(OSuc (Suc _) (Φ (Suc _)))} (ℵ< ¬ℵΦ) (ℵss< ()) +trio<> {n} {.(Suc _)} {.(ℵ _)} {.(OSuc (Suc _) (OSuc (Suc _) _))} (ℵ< (¬ℵs x)) (ℵss< x<y) = trio<> (ℵ< x) x<y +trio<> {n} {.(Suc _)} {.(OSuc (Suc _) (Φ (Suc _)))} {.(ℵ _)} (ℵss< ()) (ℵ< ¬ℵΦ) +trio<> {n} {.(Suc _)} {.(OSuc (Suc _) (OSuc (Suc _) _))} {.(ℵ _)} (ℵss< y<x) (ℵ< (¬ℵs x)) = trio<> y<x (ℵ< x) + +d<→lv : {n : Level} {x y : Ordinal {n}} → ord x d< ord y → lv x ≡ lv y +d<→lv Φ< = refl +d<→lv (s< lt) = refl +d<→lv ℵΦ< = refl +d<→lv (ℵ< _) = refl +d<→lv ℵs< = refl +d<→lv (ℵss< _) = refl + 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 open import Data.Nat.Properties -open import Data.Empty open import Data.Unit using ( ⊤ ) open import Relation.Nullary @@ -52,11 +75,6 @@ o∅ : {n : Level} → Ordinal {n} o∅ = record { lv = Zero ; ord = Φ Zero } -s<refl : {n : Level } {lx : Nat } { x : OrdinalD {n} lx } → x d< OSuc lx x -s<refl {n} {lv} {Φ lv} = Φ< -s<refl {n} {lv} {OSuc lv x} = s< s<refl -s<refl {n} {Suc lv} {ℵ lv} = ℵs< - open import Relation.Binary.HeterogeneousEquality using (_≅_;refl) ordinal-cong : {n : Level} {x y : Ordinal {n}} → @@ -72,17 +90,6 @@ ≡→¬d< : {n : Level} → {lv : Nat} → {x : OrdinalD {n} lv } → x d< x → ⊥ ≡→¬d< {n} {lx} {OSuc lx y} (s< t) = ≡→¬d< t -trio<> : {n : Level} → {lx : Nat} {x : OrdinalD {n} lx } { y : OrdinalD lx } → y d< x → x d< y → ⊥ -trio<> {n} {lx} {.(OSuc lx _)} {.(OSuc lx _)} (s< s) (s< t) = trio<> s t -trio<> {_} {.(Suc _)} {.(OSuc (Suc _) (ℵ _))} {.(ℵ _)} ℵs< (ℵ< {_} {.(ℵ _)} ()) -trio<> {_} {.(Suc _)} {.(ℵ _)} {.(OSuc (Suc _) (ℵ _))} (ℵ< ()) ℵs< -trio<> {n} {lx} {.(OSuc lx _)} {.(Φ lx)} Φ< () -trio<> {n} {.(Suc _)} {.(ℵ _)} {.(Φ (Suc _))} ℵΦ< () -trio<> {n} {.(Suc _)} {.(ℵ _)} {.(OSuc (Suc _) (Φ (Suc _)))} (ℵ< ¬ℵΦ) (ℵss< ()) -trio<> {n} {.(Suc _)} {.(ℵ _)} {.(OSuc (Suc _) (OSuc (Suc _) _))} (ℵ< (¬ℵs x)) (ℵss< x<y) = trio<> (ℵ< x) x<y -trio<> {n} {.(Suc _)} {.(OSuc (Suc _) (Φ (Suc _)))} {.(ℵ _)} (ℵss< ()) (ℵ< ¬ℵΦ) -trio<> {n} {.(Suc _)} {.(OSuc (Suc _) (OSuc (Suc _) _))} {.(ℵ _)} (ℵss< y<x) (ℵ< (¬ℵs x)) = trio<> y<x (ℵ< x) - trio<≡ : {n : Level} → {lx : Nat} {x : OrdinalD {n} lx } { y : OrdinalD lx } → x ≡ y → x d< y → ⊥ trio<≡ refl = ≡→¬d< @@ -116,34 +123,16 @@ triOrdd {_} {lv} (OSuc lv x) (OSuc lv x) | tri≈ ¬a refl ¬c = tri≈ ≡→¬d< refl ≡→¬d< triOrdd {_} {lv} (OSuc lv x) (OSuc lv y) | tri> ¬a ¬b c = tri> ( λ lt → trio<> lt (s< c) ) (λ tx=ty → trio>≡ tx=ty (s< c) ) (s< c) -d<→lv : {n : Level} {x y : Ordinal {n}} → ord x d< ord y → lv x ≡ lv y -d<→lv Φ< = refl -d<→lv (s< lt) = refl -d<→lv ℵΦ< = refl -d<→lv (ℵ< _) = refl -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 record { lv = lx ; ord = ox } = record { lv = lx ; ord = OSuc lx ox } <-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 {n} {record { lv = lx ; ord = Φ .lx }} = case2 Φ< +<-osuc {n} {record { lv = lx ; ord = OSuc .lx ox }} = case2 ( s< s<refl ) +<-osuc {n} {record { lv = (Suc lx) ; ord = ℵ lx }} = 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 +osuc-lveq {n} = refl nat-<> : { x y : Nat } → x < y → y < x → ⊥ nat-<> (s≤s x<y) (s≤s y<x) = nat-<> x<y y<x @@ -151,33 +140,8 @@ 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)) = {!!} - +¬a≤a : {la : Nat} → Suc la ≤ la → ⊥ +¬a≤a (s≤s lt) = ¬a≤a lt xsyℵ : {n : Level} {lx : Nat} {x y : OrdinalD {n} lx } → x d< y → ¬ℵ y → ¬ℵ x xsyℵ {_} {_} {Φ lv₁} {y} x<y t = ¬ℵΦ @@ -208,6 +172,42 @@ orddtrans (ℵss< (ℵss< x<y)) (ℵ< (¬ℵs x)) = orddtrans (ℵss< x<y) ( ℵ< x ) orddtrans {n} {Suc lx} {x} {y} {z} ℵs< (s< (ℵss< {lx} {ss} y<z)) = ℵss< ( ℵss< y<z ) +osuc-≡< : {n : Level} { a x : Ordinal {n} } → x o< osuc a → (x ≡ a ) ∨ (x o< a) +osuc-≡< {n} {a} {x} (case1 lt) = case2 (case1 lt) +osuc-≡< {n} {record { lv = lv₁ ; ord = Φ .lv₁ }} {record { lv = .lv₁ ; ord = .(Φ lv₁) }} (case2 Φ<) = case1 refl +osuc-≡< {n} {record { lv = lv₁ ; ord = OSuc .lv₁ ord₁ }} {record { lv = .lv₁ ; ord = .(Φ lv₁) }} (case2 Φ<) = case2 (case2 Φ<) +osuc-≡< {n} {record { lv = .(Suc lv₁) ; ord = ℵ lv₁ }} {record { lv = .(Suc lv₁) ; ord = .(Φ (Suc lv₁)) }} (case2 Φ<) = case2 (case2 ℵΦ<) +osuc-≡< {n} {record { lv = lv₁ ; ord = Φ .lv₁ }} {record { lv = .lv₁ ; ord = .(OSuc lv₁ _) }} (case2 (s< ())) +osuc-≡< {n} {record { lv = la ; ord = OSuc la oa }} {record { lv = la ; ord = (OSuc la ox) }} (case2 (s< lt)) with + osuc-≡< {n} {record { lv = la ; ord = oa }} {record { lv = la ; ord = ox }} (case2 lt ) +... | case1 refl = case1 refl +... | case2 (case2 x) = case2 (case2( s< x) ) +... | case2 (case1 x) = ⊥-elim (¬a≤a x) where +osuc-≡< {n} {record { lv = .(Suc lv₁) ; ord = ℵ lv₁ }} {record { lv = .(Suc lv₁) ; ord = .(OSuc (Suc lv₁) (Φ (Suc lv₁))) }} (case2 (s< ℵΦ<)) = case2 (case2 (ℵ< ¬ℵΦ )) +osuc-≡< {n} {record { lv = (Suc lx) ; ord = ℵ lx }} {record { lv = (Suc lx) ; ord = (OSuc (Suc lx) (OSuc (Suc lx) ox)) }} (case2 (s< (ℵ< x))) with + osuc-≡< {n} {record { lv = (Suc lx) ; ord = ℵ lx }} {record { lv = (Suc lx) ; ord = (OSuc (Suc lx) ox) }} (case2 (lemma (ℵ< x)) ) where + lemma : OSuc (Suc lx) ox d< (ℵ lx) → OSuc (Suc lx) ox d< ord (osuc (record { lv = Suc lx ; ord = ℵ lx })) + lemma lt = orddtrans lt s<refl +... | case1 () +... | case2 ttt = case2 ( case2 (ℵ< (¬ℵs x) )) +osuc-≡< {n} {record { lv = .(Suc _) ; ord = .(ℵ _) }} {record { lv = .(Suc _) ; ord = .(ℵ _) }} (case2 ℵs<) = case1 refl +osuc-≡< {n} {record { lv = .(Suc _) ; ord = Φ .(Suc _) }} {record { lv = .(Suc _) ; ord = .(ℵ _) }} (case2 (ℵss< lt)) = case2 (case2 lt) +osuc-≡< {n} {record { lv = .(Suc _) ; ord = OSuc .(Suc _) ord₁ }} {record { lv = .(Suc _) ; ord = .(ℵ _) }} (case2 (ℵss< lt)) = case2 (case2 lt) +osuc-≡< {n} {record { lv = .(Suc lv₁) ; ord = ℵ lv₁ }} {record { lv = .(Suc lv₁) ; ord = .(ℵ lv₁) }} (case2 (ℵss< lt)) = case1 refl + +osuc-< : {n : Level} { x y : Ordinal {n} } → y o< osuc x → x o< y → ⊥ +osuc-< {n} {x} {y} y<ox x<y with osuc-≡< y<ox +osuc-< {n} {x} {x} y<ox (case1 x₁) | case1 refl = ⊥-elim (¬a≤a x₁) +osuc-< {n} {x} {x} (case1 x₂) (case2 x₁) | case1 refl = ⊥-elim (¬a≤a x₂) +osuc-< {n} {x} {x} (case2 x₂) (case2 x₁) | case1 refl = ≡→¬d< x₁ +osuc-< {n} {x} {y} y<ox (case1 x₂) | case2 (case1 x₁) = nat-<> x₁ x₂ +osuc-< {n} {x} {y} y<ox (case2 x₂) | case2 (case1 x₁) with d<→lv x₂ +... | refl = ⊥-elim (¬a≤a x₁) +osuc-< {n} {x} {y} y<ox (case1 x₁) | case2 (case2 y<x) with d<→lv y<x +... | refl = ⊥-elim (¬a≤a x₁) +osuc-< {n} {x} {y} y<ox (case2 x<y) | case2 (case2 y<x) with d<→lv y<x | d<→lv x<y +... | refl | refl = trio<> y<x x<y + max : (x y : Nat) → Nat max Zero Zero = Zero max Zero (Suc x) = (Suc x)