diff ordinal.agda @ 29:fce60b99dc55

posturate OD is isomorphic to Ordinal
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 20 May 2019 18:18:43 +0900
parents constructible-set.agda@f36e40d5d2c3
children 3b0fdb95618e
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ordinal.agda	Mon May 20 18:18:43 2019 +0900
@@ -0,0 +1,179 @@
+open import Level
+module ordinal where
+
+open import zf
+
+open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ) 
+
+open import  Relation.Binary.PropositionalEquality
+
+data OrdinalD {n : Level} :  (lv : Nat) → Set n where
+   Φ : (lv : Nat) → OrdinalD  lv
+   OSuc : (lv : Nat) → OrdinalD {n} lv → OrdinalD lv
+   ℵ_ :  (lv : Nat) → OrdinalD (Suc lv)
+
+record Ordinal {n : Level} : Set n where
+   field
+     lv : Nat
+     ord : OrdinalD {n} lv
+
+data _d<_ {n : Level} :   {lx ly : Nat} → OrdinalD {n} lx  →  OrdinalD {n} ly  → Set n where
+   Φ<  : {lx : Nat} → {x : OrdinalD {n} lx}  →  Φ lx d< OSuc lx x
+   s<  : {lx : Nat} → {x y : OrdinalD {n} lx}  →  x d< y  → OSuc  lx x d< OSuc  lx y
+   ℵΦ< : {lx : Nat} → {x : OrdinalD {n} (Suc lx) } →  Φ  (Suc lx) d< (ℵ lx) 
+   ℵ<  : {lx : Nat} → {x : OrdinalD {n} (Suc lx) } →  OSuc  (Suc lx) x d< (ℵ lx) 
+
+open Ordinal
+
+_o<_ : {n : Level} ( x y : Ordinal ) → Set n
+_o<_ x y =  (lv x < lv y )  ∨ ( ord x d< ord y )
+
+open import Data.Nat.Properties 
+open import Data.Empty
+open import Relation.Nullary
+
+open import Relation.Binary
+open import Relation.Binary.Core
+
+o∅ : {n : Level} → Ordinal {n}
+o∅  = record { lv = Zero ; ord = Φ Zero }
+
+
+≡→¬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<≡ : {n : Level} →  {lx : Nat} {x  : OrdinalD {n} lx } { y : OrdinalD  lx }  → x ≡ y  → x d< y → ⊥
+trio<≡ refl = ≡→¬d<
+
+trio>≡ : {n : Level} →  {lx : Nat} {x  : OrdinalD {n} lx } { y : OrdinalD  lx }  → x ≡ y  → y d< x → ⊥
+trio>≡ refl = ≡→¬d<
+
+triO : {n : Level} →  {lx ly : Nat} → OrdinalD {n} lx  →  OrdinalD {n} ly  → Tri (lx < ly) ( lx ≡ ly ) ( lx > ly )
+triO  {n} {lx} {ly} x y = <-cmp lx ly
+
+triOrdd : {n : Level} →  {lx : Nat}   → Trichotomous  _≡_ ( _d<_  {n} {lx} {lx} )
+triOrdd  {_} {lv} (Φ lv) (Φ lv) = tri≈ ≡→¬d< refl ≡→¬d<
+triOrdd  {_} {Suc lv} (ℵ lv) (ℵ lv) = tri≈ ≡→¬d< refl ≡→¬d<
+triOrdd  {_} {lv} (Φ lv) (OSuc lv y) = tri< Φ< (λ ()) ( λ lt → trio<> lt Φ< )
+triOrdd  {_} {.(Suc lv)} (Φ (Suc lv)) (ℵ lv) = tri<  (ℵΦ<  {_} {lv} {Φ (Suc lv)} ) (λ ()) ( λ lt → trio<> lt ((ℵΦ< {_} {lv} {Φ (Suc lv)} )) )
+triOrdd  {_} {Suc lv} (ℵ lv) (Φ (Suc lv)) = tri> ( λ lt → trio<> lt (ℵΦ< {_} {lv} {Φ (Suc lv)} ) ) (λ ()) (ℵΦ<  {_} {lv} {Φ (Suc lv)} )
+triOrdd  {_} {Suc lv} (ℵ lv) (OSuc (Suc lv) y) = tri> ( λ lt → trio<> lt (ℵ< {_} {lv} {y} )  ) (λ ()) (ℵ< {_} {lv} {y} )
+triOrdd  {_} {lv} (OSuc lv x) (Φ lv) = tri> (λ lt → trio<> lt Φ<) (λ ()) Φ<
+triOrdd  {_} {.(Suc lv)} (OSuc (Suc lv) x) (ℵ lv) = tri< ℵ< (λ ()) (λ lt → trio<> lt ℵ< )
+triOrdd  {_} {lv} (OSuc lv x) (OSuc lv y) with triOrdd x y
+triOrdd  {_} {lv} (OSuc lv x) (OSuc lv y) | tri< a ¬b ¬c = tri< (s< a) (λ tx=ty → trio<≡ tx=ty (s< a) )  (  λ lt → trio<> lt (s< a) )
+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
+
+orddtrans : {n : Level} {lx : Nat} {x y z : OrdinalD {n}  lx }   → x d< y → y d< z → x d< z
+orddtrans {_} {lx} {.(Φ lx)} {.(OSuc lx _)} {.(OSuc lx _)} Φ< (s< y<z) = Φ< 
+orddtrans {_} {Suc lx} {Φ (Suc lx)} {OSuc (Suc lx) y} {ℵ lx} Φ< ℵ< = ℵΦ< {_} {lx} {y}
+orddtrans {_} {lx} {.(OSuc lx _)} {.(OSuc lx _)} {.(OSuc lx _)} (s< x<y) (s< y<z) = s< ( orddtrans x<y y<z )
+orddtrans {_} {Suc lx} {.(OSuc (Suc lx) _)} {.(OSuc (Suc lx) _)} {.(ℵ _)} (s< x<y) ℵ< = ℵ<
+orddtrans {_} {Suc lx} {Φ (Suc lx)} {.(ℵ _)} {z} ℵΦ< ()
+orddtrans {_} {Suc lx} {OSuc (Suc lx) _} {.(ℵ _)} {z} ℵ< ()
+
+max : (x y : Nat) → Nat
+max Zero Zero = Zero
+max Zero (Suc x) = (Suc x)
+max (Suc x) Zero = (Suc x)
+max (Suc x) (Suc y) = Suc ( max x y )
+
+maxαd : {n : Level} → { lx : Nat } → OrdinalD {n} lx  →  OrdinalD  lx  →  OrdinalD  lx
+maxαd x y with triOrdd x y
+maxαd x y | tri< a ¬b ¬c = y
+maxαd x y | tri≈ ¬a b ¬c = x
+maxαd x y | tri> ¬a ¬b c = x
+
+maxα : {n : Level} →  Ordinal {n} →  Ordinal  → Ordinal
+maxα x y with <-cmp (lv x) (lv y)
+maxα x y | tri< a ¬b ¬c = x
+maxα x y | tri> ¬a ¬b c = y
+maxα x y | tri≈ ¬a refl ¬c = record { lv = lv x ; ord = maxαd (ord x) (ord y) }
+
+_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 {n} {x} {y} {z} (case1 x₁) (case1 x₂) = case1 ( <-trans x₁ x₂ )
+ordtrans {n} {x} {y} {z} (case1 x₁) (case2 x₂) with d<→lv x₂
+... | refl = case1 x₁
+ordtrans {n} {x} {y} {z} (case2 x₁) (case1 x₂) with d<→lv x₁
+... | refl = case1 x₂
+ordtrans {n} {x} {y} {z} (case2 x₁) (case2 x₂) with d<→lv x₁ | d<→lv x₂
+... | refl | refl = case2 ( orddtrans x₁ x₂ )
+
+
+trio< : {n : Level } → Trichotomous {suc n} _≡_  _o<_ 
+trio< a b with <-cmp (lv a) (lv b)
+trio< a b | tri< a₁ ¬b ¬c = tri< (case1  a₁) (λ refl → ¬b (cong ( λ x → lv x ) refl ) ) lemma1 where
+   lemma1 : ¬ (Suc (lv b) ≤ lv a) ∨ (ord b d< ord a)
+   lemma1 (case1 x) = ¬c x
+   lemma1 (case2 x) with d<→lv x
+   lemma1 (case2 x) | refl = ¬b refl
+trio< a b | tri> ¬a ¬b c = tri> lemma1 (λ refl → ¬b (cong ( λ x → lv x ) refl ) ) (case1 c) where
+   lemma1 : ¬ (Suc (lv a) ≤ lv b) ∨ (ord a d< ord b)
+   lemma1 (case1 x) = ¬a x
+   lemma1 (case2 x) with d<→lv x
+   lemma1 (case2 x) | refl = ¬b refl
+trio< a b | tri≈ ¬a refl ¬c with triOrdd ( ord a ) ( ord b )
+trio< record { lv = .(lv b) ; ord = x } b | tri≈ ¬a refl ¬c | tri< a ¬b ¬c₁ = tri< (case2 a) (λ refl → ¬b (lemma1 refl )) lemma2 where
+   lemma1 :  (record { lv = _ ; ord = x }) ≡ b →  x ≡ ord b
+   lemma1 refl = refl
+   lemma2 : ¬ (Suc (lv b) ≤ lv b) ∨ (ord b d< x)
+   lemma2 (case1 x) = ¬a x
+   lemma2 (case2 x) = trio<> x a
+trio< record { lv = .(lv b) ; ord = x } b | tri≈ ¬a refl ¬c | tri> ¬a₁ ¬b c = tri> lemma2 (λ refl → ¬b (lemma1 refl )) (case2 c) where
+   lemma1 :  (record { lv = _ ; ord = x }) ≡ b →  x ≡ ord b
+   lemma1 refl = refl
+   lemma2 : ¬ (Suc (lv b) ≤ lv b) ∨ (x d< ord b)
+   lemma2 (case1 x) = ¬a x
+   lemma2 (case2 x) = trio<> x c
+trio< record { lv = .(lv b) ; ord = x } b | tri≈ ¬a refl ¬c | tri≈ ¬a₁ refl ¬c₁ = tri≈ lemma1 refl lemma1 where
+   lemma1 : ¬ (Suc (lv b) ≤ lv b) ∨ (ord b d< ord b)
+   lemma1 (case1 x) = ¬a x
+   lemma1 (case2 x) = ≡→¬d< x
+
+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 (case1 x)) (case2 (case1 y)) = case2 (case1 ( <-trans x y ) )
+OrdTrans (case2 (case1 x)) (case2 (case2 y)) with d<→lv y
+OrdTrans (case2 (case1 x)) (case2 (case2 y)) | refl = case2 (case1 x )
+OrdTrans (case2 (case2 x)) (case2 (case1 y)) with d<→lv x
+OrdTrans (case2 (case2 x)) (case2 (case1 y)) | refl = case2 (case1 y)
+OrdTrans (case2 (case2 x)) (case2 (case2 y)) with d<→lv x | d<→lv y
+OrdTrans (case2 (case2 x)) (case2 (case2 y)) | refl | refl = case2 (case2 (orddtrans 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 : Level} → ( ψ : Ordinal {n} → Set n ) 
+  → ( ∀ (lx : Nat ) → ψ ( record { lv = Suc lx ; ord = ℵ lx } )) 
+  → ( ∀ (lx : Nat ) → ψ ( record { lv = lx ; ord = Φ lx } ) )
+  → ( ∀ (lx : Nat ) → (x : OrdinalD lx )  → ψ ( record { lv = lx ; ord = x } ) → ψ ( record { lv = lx ; ord = OSuc lx x } ) )
+  →  ∀ (x : Ordinal)  → ψ x
+TransFinite ψ caseℵ caseΦ caseOSuc record { lv = lv ; ord = Φ lv } = caseΦ lv
+TransFinite ψ caseℵ caseΦ caseOSuc record { lv = lv ; ord = OSuc lv ord₁ } = caseOSuc lv ord₁
+    ( TransFinite ψ caseℵ caseΦ caseOSuc (record { lv = lv ; ord = ord₁ } ))
+TransFinite ψ caseℵ caseΦ caseOSuc record { lv = Suc lv₁ ; ord = ℵ lv₁ } = caseℵ lv₁
+