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

changeset 159:3675bd617ac8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
infinite continue...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 15 Jul 2019 09:31:32 +0900
parents b97b4ee06f01
children ebac6fa116fa
files HOD.agda ordinal-definable.agda zf.agda
diffstat 3 files changed, 29 insertions(+), 49 deletions(-) [+]
line wrap: on
line diff
--- a/HOD.agda	Sun Jul 14 17:26:57 2019 +0900
+++ b/HOD.agda	Mon Jul 15 09:31:32 2019 +0900
@@ -63,7 +63,8 @@
   -- we should prove this in agda, but simply put here
   ==→o≡ : {n : Level} →  { x y : OD {suc n} } → (x == y) → x ≡ y
   -- next assumption causes ∀ x ∋ ∅ . It menas only an ordinal becomes a set
-  -- o<→c<  : {n : Level} {x y : Ordinal {n} } → x o< y             → def (ord→od y) x 
+  --   o<→c<  : {n : Level} {x y : Ordinal {n} } → x o< y → def (ord→od y) x 
+  --   ord→od x ≡ Ord x results the same
   -- supermum as Replacement Axiom
   sup-o  : {n : Level } → ( Ordinal {n} → Ordinal {n}) →  Ordinal {n}
   sup-o< : {n : Level } → { ψ : Ordinal {n} →  Ordinal {n}} → ∀ {x : Ordinal {n}} →  ψ x  o<  sup-o ψ 
@@ -287,7 +288,6 @@
     isZF = record {
            isEquivalence  = record { refl = eq-refl ; sym = eq-sym; trans = eq-trans }
        ;   pair  = pair
-       ;   union-u = λ X z UX∋z → union-u {X} {z} UX∋z
        ;   union→ = union→
        ;   union← = union←
        ;   empty = empty
@@ -323,39 +323,15 @@
          ⊆→o< {x} {y}  lt | tri> ¬a ¬b c with lt (ord→od y) (o<-subst c (sym diso) refl )
          ... | ttt = ⊥-elim ( o<¬≡ refl (o<-subst ttt diso refl ))
 
-         Union-o : (X : Ordinal {suc n}) → OD {suc n}
-         Union-o X = record { def = λ y → osuc y o< X }
-
-         union-ou : {X z : OD {suc n}} → (U>z : Union X ∋ z ) → OD {suc n}
-         union-ou {X} {z} U>z = ord→od  ( osuc ( od→ord z ) )
-         ord-union→ :  (x : Ordinal) (z u : OD) → (Ord x ∋ u) ∧ (u ∋ z) → Union-o x ∋ z
-         ord-union→ x z u plt with trio< ( od→ord u ) ( osuc ( od→ord z ))
-         ord-union→ X z u xx | tri< a ¬b ¬c with  osuc-< a (c<→o< (proj2 xx))
-         ord-union→ X z u xx | tri< a ¬b ¬c | ()
-         ord-union→ X z u xx | tri≈ ¬a b ¬c = def-subst (c<→o< (proj1 xx )) refl refl where
-         ord-union→ X z u xx | tri> ¬a ¬b c = {!!}
-
-         ord-union← :  (x : Ordinal) (z : OD) (UX∋z : Union-o x ∋ z)
-                 → (Ord x ∋  union-ou {Ord x} {z} {!!} ) ∧ (union-ou {Ord x} {z} {!!} ∋ z )
-         ord-union← x z UX∋z = record { proj1 = lemma ; proj2 = {!!} } where
-             lemma : Ord x ∋ union-ou {Ord x} {z} {!!}
-             lemma = def-subst {suc n} {_} {_} {Ord x} {_} UX∋z refl (sym diso)
-
          union-u : {X z : OD {suc n}} → (U>z : Union X ∋ z ) → OD {suc n}
          union-u {X} {z} U>z = ord→od ( osuc ( od→ord z ) )
          union→ :  (X z u : OD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z
          union→ X z u xx not = ⊥-elim ( not (od→ord u) ( record { proj1 = proj1 xx
               ; proj2 = subst ( λ k → def k (od→ord z)) (sym oiso) (proj2 xx) } ))
 
-         union←' :  (X z : OD) (X∋z : Union X ∋ z) →  ¬  ( (u : OD ) → ¬ ((X ∋  u) ∧ (u ∋ z )))
-         union←' X z UX∋z =  TransFiniteExists _ UX∋z
+         union← :  (X z : OD) (X∋z : Union X ∋ z) →  ¬  ( (u : OD ) → ¬ ((X ∋  u) ∧ (u ∋ z )))
+         union← X z UX∋z =  TransFiniteExists _ UX∋z
              ( λ {y} xx not → not (ord→od y) (record { proj1 = subst ( λ k → def X k ) (sym diso) (proj1 xx ) ; proj2 = proj2 xx } ))
-         union← :  (X z : OD) (X∋z : Union X ∋ z) → (X ∋  union-u {X} {z} X∋z ) ∧ (union-u {X} {z} X∋z ∋ z )
-         union← X z UX∋z = record { proj1 = lemma ; proj2 = lemma2 } where
-             lemma : X ∋ union-u {X} {z} UX∋z
-             lemma = {!!} -- def-subst {suc n} {_} {_} {X} {od→ord (Ord (osuc ( od→ord z )))} UX∋z refl {!!}
-             lemma2 : union-u {X} UX∋z ∋ z
-             lemma2 = {!!}
 
          ψiso :  {ψ : OD {suc n} → Set (suc n)} {x y : OD {suc n}} → ψ x → x ≡ y   → ψ y
          ψiso {ψ} t refl = t
@@ -486,21 +462,28 @@
          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  
 
-         open  import  Relation.Binary.PropositionalEquality
          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 → k ⇔ ( y o< osuc (od→ord x) )) (sym lemma) ( osuc2 y (od→ord x))  where
-              lemma : {y : Ordinal {suc n}} → def (Union (x , (x , x))) y ≡ osuc y o< osuc (osuc (od→ord x)) 
-              lemma {y} = let open ≡-Reasoning in begin
-                   def (Union (x , (x , x))) y  
-                ≡⟨ {!!} ⟩
-                   def ( Ord ( omax (od→ord x) (od→ord (Ord (omax (od→ord x)  (od→ord x)  )) ))) ( osuc y )
-                ≡⟨⟩
-                   osuc y o<  omax (od→ord x) (od→ord (Ord (omax (od→ord x)  (od→ord x)  )) )
-                ≡⟨ cong (λ k → osuc y o<  omax (od→ord x) k ) {!!}  ⟩
-                   osuc y o<  omax (od→ord x) (omax (od→ord x)  (od→ord x)  ) 
-                ≡⟨ cong (λ k → osuc y o<  k ) (omxxx  (od→ord x) )  ⟩
-                   osuc y o< osuc (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) = {!!}
+              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) = {!!}
+              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
+
          infinite : OD {suc n}
          infinite = Ord omega 
          infinity∅ : Ord omega  ∋ od∅ {suc n}
@@ -511,8 +494,6 @@
               eq = let open ≡-Reasoning in begin
                     osuc (od→ord x)
                  ≡⟨ {!!}  ⟩
-                    od→ord (Ord (osuc (od→ord x)))
-                 ≡⟨ cong ( λ k → od→ord  k ) ( sym (==→o≡ ( ⇔→==  uxxx-ord ))) ⟩
                     od→ord (Union (x , (x , x)))
                  ∎
               lemma : (ox : Ordinal {suc n} ) → ox o< omega → osuc ox o< omega 
--- a/ordinal-definable.agda	Sun Jul 14 17:26:57 2019 +0900
+++ b/ordinal-definable.agda	Mon Jul 15 09:31:32 2019 +0900
@@ -337,7 +337,6 @@
     isZF = record {
            isEquivalence  = record { refl = eq-refl ; sym = eq-sym; trans = eq-trans }
        ;   pair  = pair
-       ;   union-u = λ _ z _ → csuc z
        ;   union→ = union→
        ;   union← = union←
        ;   empty = empty
@@ -404,8 +403,9 @@
              lemma : {oX ou ooy : Ordinal {suc n}} →  ou ≡ ooy  → ou o< oX   → ooy  o< oX
              lemma refl lt = lt
          union→ X y u xx | tri> ¬a ¬b c = ordtrans {suc n} {osuc ( od→ord y )} {od→ord u} {od→ord X} c ( c<→o< (proj1 xx )) 
-         union← :  (X z : OD) (X∋z : Union X ∋ z) → (X ∋ csuc z) ∧ (csuc z ∋ z )
-         union← X z X∋z = record { proj1 = def-subst {suc n} {_} {_} {X} {od→ord (csuc z )} (o<→c< X∋z) oiso (sym diso) ; proj2 = union-lemma-u X∋z } 
+         union← :  (X z : OD) (X∋z : Union X ∋ z) →  ¬  ( (u : OD ) → ¬ ((X ∋  u) ∧ (u ∋ z ))) -- (X ∋ csuc z) ∧ (csuc z ∋ z )
+         union← X z X∋z not = not (csuc z) 
+             record { proj1 = def-subst {suc n} {_} {_} {X} {od→ord (csuc z )} (o<→c< X∋z) oiso (sym diso) ; proj2 = union-lemma-u X∋z } 
          ψ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/zf.agda	Sun Jul 14 17:26:57 2019 +0900
+++ b/zf.agda	Mon Jul 15 09:31:32 2019 +0900
@@ -46,9 +46,8 @@
      -- ∀ 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 : ( X z : ZFSet  ) → Union X ∋ z → ZFSet
      union→ : ( X z u : ZFSet ) → ( X ∋ u ) ∧ (u ∋ z ) → Union X ∋ z
-     union← : ( X z : ZFSet ) → (X∋z : Union X ∋ z ) → (X ∋ union-u X z X∋z)  ∧ (union-u X z X∋z ∋ z )
+     union← : ( X z : ZFSet ) → (X∋z : Union X ∋ z ) →  ¬  ( (u : ZFSet ) → ¬ ((X ∋  u) ∧ (u ∋ z )))
   _∈_ : ( A B : ZFSet  ) → Set m
   A ∈ B = B ∋ A
   _⊆_ : ( A B : ZFSet  ) → ∀{ x : ZFSet } →  Set m