Mercurial > hg > Members > kono > Proof > ZF-in-agda
view Ordinals.agda @ 220:95a26d1698f4
try to separate Ordinals
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Wed, 07 Aug 2019 10:28:33 +0900 |
parents | ordinal.agda@eee983e4b402 |
children | 1709c80b7275 |
line wrap: on
line source
open import Level module Ordinals where 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 open import logic open import nat open import Data.Unit using ( ⊤ ) open import Relation.Nullary open import Relation.Binary open import Relation.Binary.Core record IsOrdinal {n : Level} (Ord : Set n) (_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<_ record Ordinal {n : Level} : Set (suc n) where field ord : Set n O< : ord → ord → Set n isOrdinal : IsOrdinal ord O< open Ordinal _o<_ : {n : Level} ( x y : Ordinal {n}) → Set n _o<_ x y = O< x {!!} {!!} -- (ord x) (ord y) o<-dom : {n : Level} { x y : Ordinal {n}} → x o< y → Ordinal o<-dom {n} {x} _ = x o<-cod : {n : Level} { x y : Ordinal {n}} → x o< y → Ordinal o<-cod {n} {_} {y} _ = y 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∅ : {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 = {!!} osucc : {n : Level} {ox oy : Ordinal {n}} → oy o< ox → osuc oy o< osuc ox osucc = {!!} o<¬≡ : {n : Level } { ox oy : Ordinal {suc n}} → ox ≡ oy → ox o< oy → ⊥ o<¬≡ = {!!} ¬x<0 : {n : Level} → { x : Ordinal {suc n} } → ¬ ( x o< o∅ {suc n} ) ¬x<0 = {!!} o<> : {n : Level} → {x y : Ordinal {n} } → y o< x → x o< y → ⊥ 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 ) 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< = {!!} 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 ) ) 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 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 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 -- -- max ( osuc x , osuc y ) -- 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 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 ) 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 ) 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 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 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 _∧_ 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) 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 } } TransFinite : {n m : Level} → { ψ : Ordinal {suc n} → Set m } → {!!} → {!!} → ∀ (x : Ordinal) → ψ x TransFinite {n} {m} {ψ} = {!!} -- 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 )