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

changeset 115:277c2f3b8acb

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Select declaration
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 25 Jun 2019 22:47:17 +0900
parents 89204edb71fa
children 47541e86c6ac
files HOD.agda ordinal-definable.agda zf.agda
diffstat 3 files changed, 21 insertions(+), 19 deletions(-) [+]
line wrap: on
line diff
--- a/HOD.agda	Tue Jun 25 21:05:07 2019 +0900
+++ b/HOD.agda	Tue Jun 25 22:47:17 2019 +0900
@@ -3,7 +3,6 @@
 
 open import zf
 open import ordinal
-
 open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ) 
 open import  Relation.Binary.PropositionalEquality
 open import Data.Nat.Properties 
@@ -246,12 +245,13 @@
  } where
     Replace : HOD {suc n} → (HOD {suc n} → HOD {suc n} ) → HOD {suc n}
     Replace X ψ = sup-od ψ
-    Select : (X : HOD {suc n} ) → ((x : HOD {suc n} ) → X ∋ x → Set (suc n) ) → HOD {suc n}
-    Select X ψ = record { def = λ x → (d : def X x)  → f x d ; otrans = λ {x} g {y} d1 → {!!} }  where
-       f : (x : Ordinal {suc n}) → (d : def X x ) → Set (suc n) 
-       f x d = ψ (ord→od x)  (subst (λ k → def X k ) (sym diso) d)
-       ftrans' : {x : Ordinal} ( g : (x : Ordinal {suc n} ) (d : def X x ) → f x d ) → {y : Ordinal} → y o< x → (d : def X y) → f y d
-       ftrans' {x} g {y} y<x d = g y d
+    Select : (X : HOD {suc n} ) → ((x : HOD {suc n} ) → Set (suc n) ) → HOD {suc n}
+    Select X ψ = record { def = λ x → ((y : Ordinal {suc n} ) → y o< od→ord X  → ψ (ord→od y)) ∧ (X ∋ ord→od x )  ; otrans = lemma } where
+       lemma :  {x : Ordinal} → ((y : Ordinal) → y o< od→ord X → ψ (ord→od y)) ∧ (X ∋ ord→od x) →
+            {y : Ordinal} → y o< x → ((y₁ : Ordinal) → y₁ o< od→ord X → ψ (ord→od y₁)) ∧ (X ∋ ord→od y)
+       lemma {x} select {y} y<x = record { proj1 = proj1 select ; proj2 = y<X } where
+           y<X : X ∋ ord→od y
+           y<X = otrans X (proj2 select) (o<-subst y<x (sym diso) (sym diso)  )
     _,_ : HOD {suc n} → HOD {suc n} → HOD {suc n}
     x , y = Ord (omax (od→ord x) (od→ord y))
     Union : HOD {suc n} → HOD {suc n}
@@ -265,7 +265,7 @@
     _⊆_ : ( A B : ZFSet  ) → ∀{ x : ZFSet } →  Set (suc n)
     _⊆_ A B {x} = A ∋ x →  B ∋ x
     _∩_ : ( A B : ZFSet  ) → ZFSet
-    A ∩ B = Select (A , B) (  λ x d → ( A ∋ x ) ∧ (B ∋ x) )
+    A ∩ B = Select (A , B) (  λ x → ( A ∋ x ) ∧ (B ∋ x) )
     -- _∪_ : ( A B : ZFSet  ) → ZFSet
     -- A ∪ B = Select (A , B) (  λ x → (A ∋ x)  ∨ ( B ∋ x ) )
     ｛_｝ : ZFSet → ZFSet
@@ -349,8 +349,10 @@
          union← X z X∋z = record { proj1 = def-subst {suc n} {_} {_} {X} {od→ord (csuc z )} {!!} oiso (sym diso) ; proj2 = union-lemma-u X∋z } 
          ψiso :  {ψ : HOD {suc n} → Set (suc n)} {x y : HOD {suc n}} → ψ x → x ≡ y   → ψ y
          ψiso {ψ} t refl = t
-         selection : {X : HOD } {ψ : (x : HOD ) →  x ∈ X  → Set (suc n)} {y : HOD} → ((d : X ∋ y ) → ψ y d ) ⇔ (Select X ψ ∋ y)
-         selection {ψ} {X} {y} =  {!!}
+         selection : {X : HOD } {ψ : (x : HOD ) → Set (suc n)} {y : HOD} → (( X ∋ y ) ∧ ψ y ) ⇔ (Select X ψ ∋ y)
+         selection {X} {ψ} {y} =  record { proj1 = λ s → record {
+            proj1 = λ y → {!!}  ; proj2 = def-subst {suc n} {_} {_} {X} {od→ord (ord→od (od→ord y))} (proj1 s) refl (sym diso) } ;
+            proj2 = {!!} }
          replacement : {ψ : HOD → HOD} (X x : HOD) → Replace X ψ ∋ ψ x
          replacement {ψ} X x = sup-c< ψ {x}
          ∅-iso :  {x : HOD} → ¬ (x == od∅) → ¬ ((ord→od (od→ord x)) == od∅) 
@@ -358,10 +360,10 @@
          minimul : (x : HOD {suc n} ) → ¬ (x == od∅ )→ HOD {suc n} 
          minimul x  not = {!!}
          regularity :  (x : HOD) (not : ¬ (x == od∅)) →
-            (x ∋ minimul x not) ∧ (Select (minimul x not) (λ x₁ d → (minimul x not ∋ x₁) ∧ (x ∋ x₁)) == od∅)
+            (x ∋ minimul x not) ∧ (Select (minimul x not) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁)) == od∅)
          proj1 (regularity x not ) = {!!}
          proj2 (regularity x not ) = record { eq→ = reg ; eq← = {!!} } where
-            reg : {y : Ordinal} → def (Select (minimul x not) (λ x₂ d → (minimul x not ∋ x₂) ∧ (x ∋ x₂))) y → def od∅ y
+            reg : {y : Ordinal} → def (Select (minimul x not) (λ x₂ → (minimul x not ∋ x₂) ∧ (x ∋ x₂))) y → def od∅ y
             reg {y} t = {!!}
          extensionality : {A B : HOD {suc n}} → ((z : HOD) → (A ∋ z) ⇔ (B ∋ z)) → A == B
          eq→ (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {A} {B} (sym diso) (proj1 (eq (ord→od x))) d  
--- a/ordinal-definable.agda	Tue Jun 25 21:05:07 2019 +0900
+++ b/ordinal-definable.agda	Tue Jun 25 22:47:17 2019 +0900
@@ -307,7 +307,7 @@
     ; _,_ = _,_
     ; Union = Union
     ; Power = Power
-    ; Select = {!!}
+    ; Select = Select
     ; Replace = Replace
     ; infinite = ord→od ( record { lv = Suc Zero ; ord = Φ 1 } )
     ; isZF = isZF 
@@ -335,7 +335,7 @@
     infixr  200 _∈_
     -- infixr  230 _∩_ _∪_
     infixr  220 _⊆_
-    isZF : IsZF (OD {suc n})  _∋_  _==_ od∅ _,_ Union Power {!!} Replace (ord→od ( record { lv = Suc Zero ; ord = Φ 1} ))
+    isZF : IsZF (OD {suc n})  _∋_  _==_ od∅ _,_ Union Power Select Replace (ord→od ( record { lv = Suc Zero ; ord = Φ 1} ))
     isZF = record {
            isEquivalence  = record { refl = eq-refl ; sym = eq-sym; trans = eq-trans }
        ;   pair  = pair
@@ -350,7 +350,7 @@
        ;   regularity = regularity
        ;   infinity∅ = infinity∅
        ;   infinity = λ _ → infinity
-       ;   selection = λ {ψ} {X} {y} → {!!}
+       ;   selection = λ {X} {ψ} {y} → selection {ψ} {X} {y} 
        ;   replacement = replacement
      } where
          open _∧_ 
--- a/zf.agda	Tue Jun 25 21:05:07 2019 +0900
+++ b/zf.agda	Tue Jun 25 22:47:17 2019 +0900
@@ -36,7 +36,7 @@
      (_,_ : ( A B : ZFSet  ) → ZFSet)
      (Union : ( A : ZFSet  ) → ZFSet)
      (Power : ( A : ZFSet  ) → ZFSet)
-     (Select :  (X : ZFSet  ) → ( ψ : (x : ZFSet ) →  X ∋ x → Set m ) → ZFSet ) 
+     (Select :  (X : ZFSet  ) → ( ψ : (x : ZFSet ) → Set m ) → ZFSet ) 
      (Replace : ZFSet → ( ZFSet → ZFSet ) → ZFSet )
      (infinite : ZFSet)
        : Set (suc (n ⊔ m)) where
@@ -53,7 +53,7 @@
   _⊆_ : ( A B : ZFSet  ) → ∀{ x : ZFSet } →  Set m
   _⊆_ A B {x} = A ∋ x →  B ∋ x
   _∩_ : ( A B : ZFSet  ) → ZFSet
-  A ∩ B = Select A (  λ x d → ( A ∋ x ) ∧ ( B ∋ x )  )
+  A ∩ B = Select A (  λ x → ( A ∋ x ) ∧ ( B ∋ x )  )
   _∪_ : ( A B : ZFSet  ) → ZFSet
   A ∪ B = Union (A , B)    -- Select A (  λ x → ( A ∋ x ) ∨ ( B ∋ x )  ) is easer
   ｛_｝ : ZFSet → ZFSet
@@ -74,7 +74,7 @@
      -- infinity : ∃ A ( ∅ ∈ A ∧ ∀ x ∈ A ( x ∪ { x } ∈ A ) )
      infinity∅ :  ∅ ∈ infinite
      infinity :  ∀( X x : ZFSet  ) → x ∈ infinite →  ( x ∪ ｛ x ｝) ∈ infinite 
-     selection : ∀ { X : ZFSet  } →  { ψ : (x : ZFSet ) →  x ∈ X → Set m } → ∀ {  y : ZFSet  } →  ( ( d : y ∈ X ) → ψ y d ) ⇔ (y ∈  Select X ψ ) 
+     selection : ∀ { X : ZFSet  } →  { ψ : (x : ZFSet ) →  Set m } → ∀ {  y : ZFSet  } →  ( ( y ∈ X ) ∧ ψ y ) ⇔ (y ∈  Select X ψ ) 
      -- replacement : ∀ x ∀ y ∀ z ( ( ψ ( x , y ) ∧ ψ ( x , z ) ) → y = z ) → ∀ X ∃ A ∀ y ( y ∈ A ↔ ∃ x ∈ X ψ ( x , y ) )
      replacement : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet  ) →  ( ψ x ∈  Replace X ψ )  
    -- -- ∀ z [ ∀ x ( x ∈ z  → ¬ ( x ≈ ∅ ) )  ∧ ∀ x ∀ y ( x , y ∈ z ∧ ¬ ( x ≈ y )  → x ∩ y ≈ ∅  ) → ∃ u ∀ x ( x ∈ z → ∃ t ( u ∩ x) ≈ ｛ t ｝) ]
@@ -94,7 +94,7 @@
      _,_ : ( A B : ZFSet  ) → ZFSet
      Union : ( A : ZFSet  ) → ZFSet
      Power : ( A : ZFSet  ) → ZFSet
-     Select :  (X : ZFSet  ) → ( ψ : (x : ZFSet ) →  X ∋ x → Set m ) → ZFSet 
+     Select :  (X : ZFSet  ) → ( ψ : (x : ZFSet ) → Set m ) → ZFSet 
      Replace : ZFSet → ( ZFSet → ZFSet ) → ZFSet
      infinite : ZFSet
      isZF : IsZF ZFSet _∋_ _≈_ ∅ _,_ Union Power Select Replace infinite