Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff Ordinals.agda @ 221:1709c80b7275
fix Ordinals
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 08 Aug 2019 17:32:21 +0900 |
| parents | 95a26d1698f4 |
| children | 59771eb07df0 |
line wrap: on
line diff
--- a/Ordinals.agda Wed Aug 07 10:28:33 2019 +0900 +++ b/Ordinals.agda Thu Aug 08 17:32:21 2019 +0900 @@ -15,175 +15,184 @@ -record IsOrdinal {n : Level} (Ord : Set n) (_O<_ : Ord → Ord → Set n) : Set n where +record IsOrdinals {n : Level} (ord : Set n) (o∅ : ord ) (osuc : ord → ord ) (_o<_ : ord → ord → Set n) : Set n where field - Otrans : {x y z : Ord } → x O< y → y O< z → x O< z - OTri : Trichotomous {n} _≡_ _O<_ + Otrans : {x y z : ord } → x o< y → y o< z → x o< z + OTri : Trichotomous {n} _≡_ _o<_ + ¬x<0 : { x : ord } → ¬ ( x o< o∅ ) + <-osuc : { x : ord } → x o< osuc x + osuc-≡< : { a x : ord } → x o< osuc a → (x ≡ a ) ∨ (x o< a) -record Ordinal {n : Level} : Set (suc n) where +record Ordinals {n : Level} : Set (suc n) where field ord : Set n - O< : ord → ord → Set n - isOrdinal : IsOrdinal ord O< + o∅ : ord + osuc : ord → ord + _o<_ : ord → ord → Set n + isOrdinal : IsOrdinals ord o∅ osuc _o<_ -open Ordinal - -_o<_ : {n : Level} ( x y : Ordinal {n}) → Set n -_o<_ x y = O< x {!!} {!!} -- (ord x) (ord y) +module inOrdinal {n : Level} (O : Ordinals {n} ) where -o<-dom : {n : Level} { x y : Ordinal {n}} → x o< y → Ordinal -o<-dom {n} {x} _ = x + Ordinal : Set n + Ordinal = Ordinals.ord O + + _o<_ : Ordinal → Ordinal → Set n + _o<_ = Ordinals._o<_ O -o<-cod : {n : Level} { x y : Ordinal {n}} → x o< y → Ordinal -o<-cod {n} {_} {y} _ = y + osuc : Ordinal → Ordinal + osuc = Ordinals.osuc O -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 + o∅ : Ordinal + o∅ = Ordinals.o∅ O -o∅ : {n : Level} → Ordinal {n} -o∅ = {!!} - -osuc : {n : Level} ( x : Ordinal {n} ) → Ordinal {n} -osuc = {!!} - -<-osuc : {n : Level} { x : Ordinal {n} } → x o< osuc x -<-osuc = {!!} + ¬x<0 = IsOrdinals.¬x<0 (Ordinals.isOrdinal O) + osuc-≡< = IsOrdinals.osuc-≡< (Ordinals.isOrdinal O) + <-osuc = IsOrdinals.<-osuc (Ordinals.isOrdinal O) + + o<-dom : { x y : Ordinal } → x o< y → Ordinal + o<-dom {x} _ = x -osucc : {n : Level} {ox oy : Ordinal {n}} → oy o< ox → osuc oy o< osuc ox -osucc = {!!} + o<-cod : { x y : Ordinal } → x o< y → Ordinal + o<-cod {_} {y} _ = y -o<¬≡ : {n : Level } { ox oy : Ordinal {suc n}} → ox ≡ oy → ox o< oy → ⊥ -o<¬≡ = {!!} + o<-subst : {Z X z x : Ordinal } → Z o< X → Z ≡ z → X ≡ x → z o< x + o<-subst df refl refl = df -¬x<0 : {n : Level} → { x : Ordinal {suc n} } → ¬ ( x o< o∅ {suc n} ) -¬x<0 = {!!} + ordtrans : {x y z : Ordinal } → x o< y → y o< z → x o< z + ordtrans = IsOrdinals.Otrans (Ordinals.isOrdinal O) -o<> : {n : Level} → {x y : Ordinal {n} } → y o< x → x o< y → ⊥ -o<> = {!!} + trio< : Trichotomous _≡_ _o<_ + trio< = IsOrdinals.OTri (Ordinals.isOrdinal O) -osuc-≡< : {n : Level} { a x : Ordinal {n} } → x o< osuc a → (x ≡ a ) ∨ (x o< a) -osuc-≡< = {!!} - -osuc-< : {n : Level} { x y : Ordinal {n} } → y o< osuc x → x o< y → ⊥ -osuc-< = {!!} - -_o≤_ : {n : Level} → Ordinal → Ordinal → Set (suc n) -a o≤ b = (a ≡ b) ∨ ( a o< b ) + o<¬≡ : { ox oy : Ordinal } → ox ≡ oy → ox o< oy → ⊥ + o<¬≡ {ox} {oy} eq lt with trio< ox oy + o<¬≡ {ox} {oy} eq lt | tri< a ¬b ¬c = ¬b eq + o<¬≡ {ox} {oy} eq lt | tri≈ ¬a b ¬c = ¬a lt + o<¬≡ {ox} {oy} eq lt | tri> ¬a ¬b c = ¬b eq -ordtrans : {n : Level} {x y z : Ordinal {n} } → x o< y → y o< z → x o< z -ordtrans = {!!} - -trio< : {n : Level } → Trichotomous {suc n} _≡_ _o<_ -trio< = {!!} + o<> : {x y : Ordinal } → y o< x → x o< y → ⊥ + o<> {ox} {oy} lt tl with trio< ox oy + o<> {ox} {oy} lt tl | tri< a ¬b ¬c = ¬c lt + o<> {ox} {oy} lt tl | tri≈ ¬a b ¬c = ¬a tl + o<> {ox} {oy} lt tl | tri> ¬a ¬b c = ¬a tl -xo<ab : {n : Level} {oa ob : Ordinal {suc n}} → ( {ox : Ordinal {suc n}} → ox o< oa → ox o< ob ) → oa o< osuc ob -xo<ab {n} {oa} {ob} a→b with trio< oa ob -xo<ab {n} {oa} {ob} a→b | tri< a ¬b ¬c = ordtrans a <-osuc -xo<ab {n} {oa} {ob} a→b | tri≈ ¬a refl ¬c = <-osuc -xo<ab {n} {oa} {ob} a→b | tri> ¬a ¬b c = ⊥-elim ( o<¬≡ refl (a→b c ) ) + osuc-< : { x y : Ordinal } → y o< osuc x → x o< y → ⊥ + osuc-< {x} {y} y<ox x<y with osuc-≡< y<ox + osuc-< {x} {y} y<ox x<y | case1 refl = o<¬≡ refl x<y + osuc-< {x} {y} y<ox x<y | case2 y<x = o<> x<y y<x -maxα : {n : Level} → Ordinal {suc n} → Ordinal → Ordinal -maxα x y with trio< x y -maxα x y | tri< a ¬b ¬c = y -maxα x y | tri> ¬a ¬b c = x -maxα x y | tri≈ ¬a refl ¬c = x + osucc : {ox oy : Ordinal } → oy o< ox → osuc oy o< osuc ox + ---- y < osuc y < x < osuc x + ---- y < osuc y = x < osuc x + ---- y < osuc y > x < osuc x -> y = x ∨ x < y → ⊥ + osucc {ox} {oy} oy<ox with trio< (osuc oy) ox + osucc {ox} {oy} oy<ox | tri< a ¬b ¬c = ordtrans a <-osuc + osucc {ox} {oy} oy<ox | tri≈ ¬a refl ¬c = <-osuc + osucc {ox} {oy} oy<ox | tri> ¬a ¬b c with osuc-≡< c + osucc {ox} {oy} oy<ox | tri> ¬a ¬b c | case1 eq = ⊥-elim (o<¬≡ (sym eq) oy<ox) + osucc {ox} {oy} oy<ox | tri> ¬a ¬b c | case2 lt = ⊥-elim (o<> lt oy<ox) + + open _∧_ -minα : {n : Level} → Ordinal {n} → Ordinal → Ordinal -minα {n} x y with trio< {n} x y -minα x y | tri< a ¬b ¬c = x -minα x y | tri> ¬a ¬b c = y -minα x y | tri≈ ¬a refl ¬c = x + osuc2 : ( x y : Ordinal ) → ( osuc x o< osuc (osuc y )) ⇔ (x o< osuc y) + proj2 (osuc2 x y) lt = osucc lt + proj1 (osuc2 x y) ox<ooy with osuc-≡< ox<ooy + proj1 (osuc2 x y) ox<ooy | case1 ox=oy = o<-subst <-osuc refl ox=oy + proj1 (osuc2 x y) ox<ooy | case2 ox<oy = ordtrans <-osuc ox<oy -min1 : {n : Level} → {x y z : Ordinal {n} } → z o< x → z o< y → z o< minα x y -min1 {n} {x} {y} {z} z<x z<y with trio< {n} x y -min1 {n} {x} {y} {z} z<x z<y | tri< a ¬b ¬c = z<x -min1 {n} {x} {y} {z} z<x z<y | tri≈ ¬a refl ¬c = z<x -min1 {n} {x} {y} {z} z<x z<y | tri> ¬a ¬b c = z<y + _o≤_ : Ordinal → Ordinal → Set n + a o≤ b = (a ≡ b) ∨ ( a o< b ) + --- --- max ( osuc x , osuc y ) --- + xo<ab : {oa ob : Ordinal } → ( {ox : Ordinal } → ox o< oa → ox o< ob ) → oa o< osuc ob + xo<ab {oa} {ob} a→b with trio< oa ob + xo<ab {oa} {ob} a→b | tri< a ¬b ¬c = ordtrans a <-osuc + xo<ab {oa} {ob} a→b | tri≈ ¬a refl ¬c = <-osuc + xo<ab {oa} {ob} a→b | tri> ¬a ¬b c = ⊥-elim ( o<¬≡ refl (a→b c ) ) -omax : {n : Level} ( x y : Ordinal {suc n} ) → Ordinal {suc n} -omax {n} x y with trio< x y -omax {n} x y | tri< a ¬b ¬c = osuc y -omax {n} x y | tri> ¬a ¬b c = osuc x -omax {n} x y | tri≈ ¬a refl ¬c = osuc x + maxα : Ordinal → Ordinal → Ordinal + maxα x y with trio< x y + maxα x y | tri< a ¬b ¬c = y + maxα x y | tri> ¬a ¬b c = x + maxα x y | tri≈ ¬a refl ¬c = x -omax< : {n : Level} ( x y : Ordinal {suc n} ) → x o< y → osuc y ≡ omax x y -omax< {n} x y lt with trio< x y -omax< {n} x y lt | tri< a ¬b ¬c = refl -omax< {n} x y lt | tri≈ ¬a b ¬c = ⊥-elim (¬a lt ) -omax< {n} x y lt | tri> ¬a ¬b c = ⊥-elim (¬a lt ) + minα : Ordinal → Ordinal → Ordinal + minα x y with trio< x y + minα x y | tri< a ¬b ¬c = x + minα x y | tri> ¬a ¬b c = y + minα x y | tri≈ ¬a refl ¬c = x -omax≡ : {n : Level} ( x y : Ordinal {suc n} ) → x ≡ y → osuc y ≡ omax x y -omax≡ {n} x y eq with trio< x y -omax≡ {n} x y eq | tri< a ¬b ¬c = ⊥-elim (¬b eq ) -omax≡ {n} x y eq | tri≈ ¬a refl ¬c = refl -omax≡ {n} x y eq | tri> ¬a ¬b c = ⊥-elim (¬b eq ) + min1 : {x y z : Ordinal } → z o< x → z o< y → z o< minα x y + min1 {x} {y} {z} z<x z<y with trio< x y + min1 {x} {y} {z} z<x z<y | tri< a ¬b ¬c = z<x + min1 {x} {y} {z} z<x z<y | tri≈ ¬a refl ¬c = z<x + min1 {x} {y} {z} z<x z<y | tri> ¬a ¬b c = z<y -omax-x : {n : Level} ( x y : Ordinal {suc n} ) → x o< omax x y -omax-x {n} x y with trio< x y -omax-x {n} x y | tri< a ¬b ¬c = ordtrans a <-osuc -omax-x {n} x y | tri> ¬a ¬b c = <-osuc -omax-x {n} x y | tri≈ ¬a refl ¬c = <-osuc + -- + -- max ( osuc x , osuc y ) + -- + + omax : ( x y : Ordinal ) → Ordinal + omax x y with trio< x y + omax x y | tri< a ¬b ¬c = osuc y + omax x y | tri> ¬a ¬b c = osuc x + omax x y | tri≈ ¬a refl ¬c = osuc x -omax-y : {n : Level} ( x y : Ordinal {suc n} ) → y o< omax x y -omax-y {n} x y with trio< x y -omax-y {n} x y | tri< a ¬b ¬c = <-osuc -omax-y {n} x y | tri> ¬a ¬b c = ordtrans c <-osuc -omax-y {n} x y | tri≈ ¬a refl ¬c = <-osuc + omax< : ( x y : Ordinal ) → x o< y → osuc y ≡ omax x y + omax< x y lt with trio< x y + omax< x y lt | tri< a ¬b ¬c = refl + omax< x y lt | tri≈ ¬a b ¬c = ⊥-elim (¬a lt ) + omax< x y lt | tri> ¬a ¬b c = ⊥-elim (¬a lt ) -omxx : {n : Level} ( x : Ordinal {suc n} ) → omax x x ≡ osuc x -omxx {n} x with trio< x x -omxx {n} x | tri< a ¬b ¬c = ⊥-elim (¬b refl ) -omxx {n} x | tri> ¬a ¬b c = ⊥-elim (¬b refl ) -omxx {n} x | tri≈ ¬a refl ¬c = refl - -omxxx : {n : Level} ( x : Ordinal {suc n} ) → omax x (omax x x ) ≡ osuc (osuc x) -omxxx {n} x = trans ( cong ( λ k → omax x k ) (omxx x )) (sym ( omax< x (osuc x) <-osuc )) - -open _∧_ + omax≡ : ( x y : Ordinal ) → x ≡ y → osuc y ≡ omax x y + omax≡ x y eq with trio< x y + omax≡ x y eq | tri< a ¬b ¬c = ⊥-elim (¬b eq ) + omax≡ x y eq | tri≈ ¬a refl ¬c = refl + omax≡ x y eq | tri> ¬a ¬b c = ⊥-elim (¬b eq ) -osuc2 : {n : Level} ( x y : Ordinal {suc n} ) → ( osuc x o< osuc (osuc y )) ⇔ (x o< osuc y) -osuc2 = {!!} - -OrdTrans : {n : Level} → Transitive {suc n} _o≤_ -OrdTrans (case1 refl) (case1 refl) = case1 refl -OrdTrans (case1 refl) (case2 lt2) = case2 lt2 -OrdTrans (case2 lt1) (case1 refl) = case2 lt1 -OrdTrans (case2 x) (case2 y) = case2 (ordtrans x y) + omax-x : ( x y : Ordinal ) → x o< omax x y + omax-x x y with trio< x y + omax-x x y | tri< a ¬b ¬c = ordtrans a <-osuc + omax-x x y | tri> ¬a ¬b c = <-osuc + omax-x x y | tri≈ ¬a refl ¬c = <-osuc -OrdPreorder : {n : Level} → Preorder (suc n) (suc n) (suc n) -OrdPreorder {n} = record { Carrier = Ordinal - ; _≈_ = _≡_ - ; _∼_ = _o≤_ - ; isPreorder = record { - isEquivalence = record { refl = refl ; sym = sym ; trans = trans } - ; reflexive = case1 - ; trans = OrdTrans - } - } + omax-y : ( x y : Ordinal ) → y o< omax x y + omax-y x y with trio< x y + omax-y x y | tri< a ¬b ¬c = <-osuc + omax-y x y | tri> ¬a ¬b c = ordtrans c <-osuc + omax-y x y | tri≈ ¬a refl ¬c = <-osuc + + omxx : ( x : Ordinal ) → omax x x ≡ osuc x + omxx x with trio< x x + omxx x | tri< a ¬b ¬c = ⊥-elim (¬b refl ) + omxx x | tri> ¬a ¬b c = ⊥-elim (¬b refl ) + omxx x | tri≈ ¬a refl ¬c = refl + + omxxx : ( x : Ordinal ) → omax x (omax x x ) ≡ osuc (osuc x) + omxxx x = trans ( cong ( λ k → omax x k ) (omxx x )) (sym ( omax< x (osuc x) <-osuc )) + + open _∧_ -TransFinite : {n m : Level} → { ψ : Ordinal {suc n} → Set m } - → {!!} - → {!!} - → ∀ (x : Ordinal) → ψ x -TransFinite {n} {m} {ψ} = {!!} + OrdTrans : Transitive _o≤_ + OrdTrans (case1 refl) (case1 refl) = case1 refl + OrdTrans (case1 refl) (case2 lt2) = case2 lt2 + OrdTrans (case2 lt1) (case1 refl) = case2 lt1 + OrdTrans (case2 x) (case2 y) = case2 (ordtrans x y) --- we cannot prove this in intutionistic logic --- (¬ (∀ y → ¬ ( ψ y ))) → (ψ y → p ) → p --- postulate --- TransFiniteExists : {n m l : Level} → ( ψ : Ordinal {n} → Set m ) --- → (exists : ¬ (∀ y → ¬ ( ψ y ) )) --- → {p : Set l} ( P : { y : Ordinal {n} } → ψ y → p ) --- → p --- --- Instead we prove --- -TransFiniteExists : {n m l : Level} → ( ψ : Ordinal {n} → Set m ) - → {p : Set l} ( P : { y : Ordinal {n} } → ψ y → ¬ p ) - → (exists : ¬ (∀ y → ¬ ( ψ y ) )) - → ¬ p -TransFiniteExists {n} {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p ) + OrdPreorder : Preorder n n n + OrdPreorder = record { Carrier = Ordinal + ; _≈_ = _≡_ + ; _∼_ = _o≤_ + ; isPreorder = record { + isEquivalence = record { refl = refl ; sym = sym ; trans = trans } + ; reflexive = case1 + ; trans = OrdTrans + } + } + TransFiniteExists : {m l : Level} → ( ψ : Ordinal → Set m ) + → {p : Set l} ( P : { y : Ordinal } → ψ y → ¬ p ) + → (exists : ¬ (∀ y → ¬ ( ψ y ) )) + → ¬ p + TransFiniteExists {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p ) +