Mercurial > hg > Members > kono > Proof > ZF-in-agda

changeset 70:cd9cf8b09610

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Union needs +1 space
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 01 Jun 2019 10:01:38 +0900
parents 93abc0133b8a
children d088eb66564e
files ordinal-definable.agda ordinal.agda zf.agda
diffstat 3 files changed, 29 insertions(+), 13 deletions(-) [+]
line wrap: on
line diff
--- a/ordinal-definable.agda	Fri May 31 22:30:23 2019 +0900
+++ b/ordinal-definable.agda	Sat Jun 01 10:01:38 2019 +0900
@@ -332,7 +332,8 @@
            isEquivalence  = record { refl = eq-refl ; sym = eq-sym; trans = eq-trans }
        ;   pair  = pair
        ;   union-u = {!!}
-       ;   union-iso = {!!}
+       ;   union→ = {!!}
+       ;   union← = {!!}
        ;   empty = empty
        ;   power→ = {!!}
        ;   power← = {!!}
@@ -351,18 +352,29 @@
          proj2 (pair A B ) =  case2 refl 
          empty : (x : OD {suc n} ) → ¬  (od∅ ∋ x)
          empty x ()
+         union-u : (X z : OD {suc n}) → Union X ∋ z → OD {suc n}
+         union-u X z U>z with od→ord X | od→ord z 
+         union-u X z (case1 (s≤s x)) | record { lv = Suc lX ; ord = oX } | record { lv = lz ; ord = oz } = ord→od (mid (Suc lX) lz oX oz (s≤s x) )  where
+             mid : (lX lz : Nat) → (oX : OrdinalD {suc n} lX ) → (oz : OrdinalD {suc n} lz ) → lX > lz  → Ordinal {suc n}
+             mid (Suc lX) 0 oX oz (s≤s z≤n) = record { lv = 0 ; ord = OSuc 0 oz }
+             mid (Suc (Suc lX)) (Suc lz) (Φ (Suc (Suc lX))) (Φ (Suc lz)) (s≤s (s≤s lt)) = record { lv = Suc lz ; ord = OSuc (Suc lz) (Φ (Suc lz) ) }
+             mid (Suc (Suc lX)) (Suc lz) (Φ (Suc (Suc lX))) (OSuc (Suc lz) oz) (s≤s (s≤s lt)) = record { lv = Suc lz ; ord = OSuc (Suc lz) (OSuc (Suc lz) oz) }
+             mid (Suc (Suc lX)) (Suc lz) (Φ (Suc (Suc lX))) (ℵ lz) (s≤s (s≤s lt)) = record { lv = (Suc (Suc lX)) ; ord = OSuc (Suc (Suc lX)) (ℵ (Suc lX)) }
+             mid (Suc (Suc lX)) (Suc lz) (OSuc (Suc (Suc lX)) oX) oz (s≤s (s≤s lt)) = record { lv = Suc (Suc lX) ; ord = oX }
+             mid (Suc (Suc lX)) (Suc lz) (ℵ (Suc lX)) oz (s≤s (s≤s lt)) = record { lv = Suc (Suc lX) ; ord = OSuc (Suc (Suc lX)) (Φ (Suc (Suc lX))) }
+         union-u X z (case2 Φ<) | record { lv = Zero ; ord = (OSuc 0 oX) } | record { lv = .0 ; ord = .(Φ 0) } =
+             ord→od (record { lv = Zero ; ord = oX }) -- this case contains X = odΦ
+         union-u X z (case2 Φ<) | record { lv = Suc lv₁ ; ord = (OSuc (Suc lv₁) oX) } | record { lv = .(Suc lv₁) ; ord = .(Φ (Suc lv₁)) } =  ord→od (record { lv = Suc lv₁ ; ord = oX } )
+         union-u X z (case2 (s< x)) | record { lv = lv₁ ; ord = .(OSuc lv₁ _) } | record { lv = .lv₁ ; ord = .(OSuc lv₁ _) } = {!!}
+         union-u X z (case2 ℵΦ<) | record { lv = Suc lX ; ord = .(ℵ _) } | record { lv = .(Suc _) ; ord = .(Φ (Suc _)) } =  ord→od ( record { lv = Suc lX ; ord = OSuc (Suc lX ) (Φ (Suc lX))} )
+         union-u X z (case2 (ℵ< x)) | record { lv = Suc lX ; ord = .(ℵ _) } | record { lv = .(Suc _) ; ord = OSuc (Suc _) oz } =
+              ord→od ( record { lv = Suc lX ; ord = OSuc (Suc lX ) (OSuc (Suc lX) (OSuc (Suc lX) oz ))} )
+         union-u X z (case2 ℵs<) | record { lv = Suc lX ; ord = OSuc (Suc lX) (ℵ lX) } | record { lv = Suc lX ; ord = ℵ lX } = {!!}
+         union-u X z (case2 (ℵss< x)) | record { lv = .(Suc _) ; ord = .(OSuc (Suc _) _) } | record { lv = .(Suc _) ; ord = .(ℵ _) } = {!!}
          union→ :  (X x y : OD {suc n}) → X ∋ x → x ∋ y → Union X ∋ y
          union→ X x y X∋x x∋y =  c<→o<  (transitive {n} {X} {x} {y} X∋x x∋y  )
-         union-u : (X z : OD {suc n}) → OD {suc n}
-         union-u X z = record { def =  ( λ u → (u o< od→ord X)  ∧ (od→ord z o< u) ) }
-         union-iso :  (X z : OD {suc n}) → (Union X ∋ z) ⇔ ((Union X ∋ union-u X z ) ∧ (union-u X z ∋ z))
-         --    ((x : OD) →  (z ∋ x → y ∋ x)) → y ∋ z 
-         proj1 ( union-iso X z ) U∋z = record { proj1 = U∋u ;  proj2 = u∋z } where
-             U∋u : Union X ∋ union-u X z
-             U∋u = {!!}
-             u∋z : union-u X z ∋ z
-             u∋z = {!!}
-         proj2 (union-iso X z ) U∋u∧U∋z  = transitive {n} {!!} {!!} -- (proj1 U∋u∧U∋z ) (proj2 U∋u∧U∋z )
+         union← :  (X z : OD {suc n}) → (X∋z : Union X ∋ z) → ((Union X ∋ union-u X z X∋z) ∧ (union-u X z X∋z ∋ z))
+         union← = {!!}
          ψiso :  {ψ : OD {suc n} → Set (suc n)} {x y : OD {suc n}} → ψ x → x ≡ y   → ψ y
          ψiso {ψ} t refl = t
          selection : {ψ : OD → Set (suc n)} {X y : OD} → ((X ∋ y) ∧ ψ y) ⇔ (Select X ψ ∋ y)
--- a/ordinal.agda	Fri May 31 22:30:23 2019 +0900
+++ b/ordinal.agda	Sat Jun 01 10:01:38 2019 +0900
@@ -22,6 +22,9 @@
     ¬ℵΦ : ¬ℵ (Φ lx) 
     ¬ℵs : {x : OrdinalD {n} lx } → ¬ℵ x → ¬ℵ (OSuc lx x) 
 
+--
+--    Φ (Suc lv) < ℵ lv < OSuc (Suc lv) (ℵ lv) < OSuc ... < OSuc (Suc lv) (Φ (Suc lv)) < OSuc ...  < ℵ (Suc 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
--- a/zf.agda	Fri May 31 22:30:23 2019 +0900
+++ b/zf.agda	Sat Jun 01 10:01:38 2019 +0900
@@ -50,8 +50,9 @@
      -- ∀ x ∀ y ∃ z(x ∈ z ∧ y ∈ z)
      pair : ( A B : ZFSet  ) →  ( (A , B)  ∋ A ) ∧ ( (A , B)  ∋ B  )
      -- ∀ x ∃ y ∀ z (z ∈ y ⇔ ∃ u ∈ x  ∧ (z ∈ u))
-     union-u : ( y z : ZFSet  ) → ZFSet
-     union-iso : ( X z : ZFSet ) → (Union X ∋ z ) ⇔ ((Union X ∋ union-u X z )  ∧ (union-u X z ∋ z ))
+     union-u : ( X z : ZFSet  ) → Union X ∋ z → ZFSet
+     union→ : ( X z u : ZFSet ) → ((Union X ∋ u )  ∧ (u ∋ z )) → Union X ∋ z
+     union← : ( X z : ZFSet ) → (X∋z : Union X ∋ z ) → (Union X ∋ union-u X z X∋z)  ∧ (union-u X z X∋z ∋ z )
   _∈_ : ( A B : ZFSet  ) → Set m
   A ∈ B = B ∋ A
   _⊆_ : ( A B : ZFSet  ) → ∀{ x : ZFSet } →  Set m