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

changeset 161:4c704b7a62e4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
ininite done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 15 Jul 2019 18:26:56 +0900
parents ebac6fa116fa
children b06f5d2f34b1
files HOD.agda
diffstat 1 files changed, 26 insertions(+), 45 deletions(-) [+]
line wrap: on
line diff
--- a/HOD.agda	Mon Jul 15 15:54:59 2019 +0900
+++ b/HOD.agda	Mon Jul 15 18:26:56 2019 +0900
@@ -247,9 +247,6 @@
 omega : { n : Level } → Ordinal {n}
 omega = record { lv = Suc Zero ; ord = Φ 1 }
 
-od-infinite : {n : Level} → OD {suc n}
-od-infinite = record { def = λ x → x o< sup-o ( λ y → od→ord (Ord y)) }
-
 OD→ZF : {n : Level} → ZF {suc (suc n)} {suc n}
 OD→ZF {n}  = record { 
     ZFSet = OD {suc n}
@@ -261,7 +258,7 @@
     ; Power = Power
     ; Select = Select
     ; Replace = Replace
-    ; infinite = od-infinite
+    ; infinite = infinite
     ; isZF = isZF 
  } where
     ZFSet = OD {suc n}
@@ -284,10 +281,18 @@
     ｛_｝ : ZFSet → ZFSet
     ｛ x ｝ = ( x ,  x )
 
+    data infinite-d  : ( x : Ordinal {suc n} ) → Set (suc n) where
+        iφ :  infinite-d o∅
+        isuc : {x : Ordinal {suc n} } →   infinite-d  x  →
+                infinite-d  (od→ord ( Union (ord→od x , (ord→od x , ord→od x ) ) ))
+
+    infinite : OD {suc n}
+    infinite = record { def = λ x → infinite-d x }
+
     infixr  200 _∈_
     -- infixr  230 _∩_ _∪_
     infixr  220 _⊆_
-    isZF : IsZF (OD {suc n})  _∋_  _==_ od∅ _,_ Union Power Select Replace od-infinite
+    isZF : IsZF (OD {suc n})  _∋_  _==_ od∅ _,_ Union Power Select Replace infinite
     isZF = record {
            isEquivalence  = record { refl = eq-refl ; sym = eq-sym; trans = eq-trans }
        ;   pair  = pair
@@ -465,47 +470,23 @@
          eq→ (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {A} {B} (sym diso) (proj1 (eq (ord→od x))) d  
          eq← (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {B} {A} (sym diso) (proj2 (eq (ord→od x))) d  
 
-         uxxx-ord : {x  : OD {suc n}} → {y : Ordinal {suc n}} → def (Union (x , (x , x))) y ⇔ ( y o< osuc (od→ord x) )
-         uxxx-ord {x} {y} = subst (λ k → def (Union (k , (k , k))) y ⇔ ( y o< osuc (od→ord x) ) ) oiso lemma where
-              ordΦ  : {lx : Nat } → Ordinal {suc n}
-              ordΦ  {lx} = record { lv = lx ; ord = Φ lx }
-              odΦ  : {lx : Nat } → OD {suc n}
-              odΦ  {lx} = ord→od ordΦ
-              xord  : {lx : Nat } → { ox : OrdinalD {suc n} lx } → Ordinal {suc n}
-              xord  {lx} {ox} = record { lv = lx ; ord = ox }
-              xod  : {lx : Nat } → { ox : OrdinalD {suc n} lx } → OD {suc n}
-              xod  {lx} {ox} = ord→od (xord {lx} {ox})
-              lemmaφ :  (lx : Nat) → def (Union (odΦ {lx} , (odΦ {lx} , odΦ {lx} ))) y ⇔ (y o< osuc (record { lv = lx ; ord = Φ lx }))
-              proj1 (lemmaφ lx) df = TransFiniteExists _ df lemma where
-                  lemma : {y1 : Ordinal} → def (odΦ {lx} , (odΦ {lx} , odΦ {lx} )) y1 ∧ def (ord→od y1) y → y o< xord {lx} {OSuc lx (Φ lx)}
-                  lemma {y1} xx with proj1 xx | c<→o< {suc n} {ord→od y} {ord→od y1} (def-subst {suc n} {ord→od y1} {y} (proj2 xx) refl (sym diso))
-                  --  x : lv y1 < lx ,  x₁ : lv (od→ord (ord→od y) < lv y1  -> lv y < lx
-                  lemma {y1} xx | case1 x | case1 x₁ =
-                      case1 ( <-trans  (subst (λ k → lv k < lv (od→ord (ord→od y1))) diso x₁) (subst (λ k → lv k < lx ) (sym diso) {!!}) )
-                  lemma {y1} xx | case1 x | case2 x₁ with d<→lv x₁
-                  ... | eq = case1 {!!}
-                  lemma {y1} xx | case2 x | lt = {!!}
-              proj2 (lemmaφ lx) lt not = not (ordΦ {lx}){!!}
-              lemma-suc : (lx : Nat) (ox : OrdinalD lx) →
-                    def (Union (xod {lx} {ox} , (xod {lx} {ox} , xod {lx} {ox} ))) y ⇔ (y o< osuc (xord {lx} {ox})) →
-                    def (Union (xod {lx} {OSuc lx ox} , (xod {lx} {OSuc lx ox} , xod {lx} {OSuc lx ox} ))) y
-                        ⇔ (y o< osuc (xord  {lx} {OSuc lx ox}))
-              proj1 (lemma-suc lx ox prev) df =  TransFiniteExists _ df {!!}
-              proj2 (lemma-suc lx ox prev) lt not = not (xord {lx} {ox}) {!!}
-              lemma = TransFinite {suc n} {λ ox → def (Union (ord→od ox , (ord→od ox , ord→od ox))) y ⇔ ( y o< osuc ox ) }
-                  lemmaφ lemma-suc (od→ord x) where
 
-         infinity∅ : od-infinite  ∋ od∅ {suc n}
-         infinity∅ = {!!} -- o<-subst (case1 (s≤s z≤n) ) (sym ord-od∅) refl
-         infinity : (x : OD) → od-infinite ∋ x → od-infinite ∋ Union (x , (x , x ))
-         infinity x lt = {!!} where
-              lemma : (ox : Ordinal {suc n} ) → ox o< omega → osuc ox o< omega 
-              lemma record { lv = Zero ; ord = (Φ .0) } (case1 (s≤s x)) = case1 (s≤s z≤n)
-              lemma record { lv = Zero ; ord = (OSuc .0 ord₁) } (case1 (s≤s x)) = case1 (s≤s z≤n)
-              lemma record { lv = (Suc lv₁) ; ord = (Φ .(Suc lv₁)) } (case1 (s≤s ()))
-              lemma record { lv = (Suc lv₁) ; ord = (OSuc .(Suc lv₁) ord₁) } (case1 (s≤s ()))
-              lemma record { lv = 1 ; ord = (Φ 1) } (case2 c2) with d<→lv c2
-              lemma record { lv = (Suc Zero) ; ord = (Φ .1) } (case2 ()) | refl
+         infinity∅ : infinite  ∋ od∅ {suc n}
+         infinity∅ = def-subst {suc n} {_} {_} {infinite} {od→ord (od∅ {suc n})} iφ refl lemma where
+              lemma : o∅ ≡ od→ord od∅
+              lemma =  let open ≡-Reasoning in begin
+                    o∅
+                 ≡⟨ sym diso ⟩
+                    od→ord ( ord→od o∅ )
+                 ≡⟨ cong ( λ k → od→ord k ) o∅≡od∅ ⟩
+                    od→ord od∅
+                 ∎
+         infinity : (x : OD) → infinite ∋ x → infinite ∋ Union (x , (x , x ))
+         infinity x lt = def-subst {suc n} {_} {_} {infinite} {od→ord (Union (x , (x , x )))} ( isuc {od→ord x} lt ) refl lemma where
+               lemma :  od→ord (Union (ord→od (od→ord x) , (ord→od (od→ord x) , ord→od (od→ord x))))
+                    ≡ od→ord (Union (x , (x , x)))
+               lemma = cong (λ k → od→ord (Union ( k , ( k , k ) ))) oiso 
+
          -- ∀ X [ ∅ ∉ X → (∃ f : X → ⋃ X ) → ∀ A ∈ X ( f ( A ) ∈ A ) ] -- this form is no good since X is a transitive set
          -- ∀ z [ ∀ x ( x ∈ z  → ¬ ( x ≈ ∅ ) )  ∧ ∀ x ∀ y ( x , y ∈ z ∧ ¬ ( x ≈ y )  → x ∩ y ≈ ∅  ) → ∃ u ∀ x ( x ∈ z → ∃ t ( u ∩ x) ≈ ｛ t ｝) ]
          record Choice (z : OD {suc n}) : Set (suc (suc n)) where