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

changeset 104:d92411bed18c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 16 Jun 2019 02:06:09 +0900
parents c8b79d303867
children ec6235ce0215
files ordinal-definable.agda
diffstat 1 files changed, 92 insertions(+), 50 deletions(-) [+]
line wrap: on
line diff
--- a/ordinal-definable.agda	Wed Jun 12 10:45:00 2019 +0900
+++ b/ordinal-definable.agda	Sun Jun 16 02:06:09 2019 +0900
@@ -57,15 +57,60 @@
   -- a contra-position of minimality of supermum 
   sup-x  : {n : Level } → ( Ordinal {n} → Ordinal {n}) →  Ordinal {n}
   sup-lb : {n : Level } → { ψ : Ordinal {n} →  Ordinal {n}} → {z : Ordinal {n}}  →  z o< sup-o ψ → z o< osuc (ψ (sup-x ψ))
+-- sup-min : {n : Level } → ( ψ : Ordinal {n} →  Ordinal {n}) → {z : Ordinal {n}}  →  ψ z  o<  z  →   sup-o ψ  o< osuc z
+  minimul : {n : Level } → (x : OD {suc n} ) → ¬ (x == od∅ )→ OD {suc n} 
+  x∋minimul : {n : Level } → (x : OD {suc n} ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimul x ne ) )
+  minimul-1 : {n : Level } → (x : OD {suc n} ) → ( ne : ¬ (x == od∅ ) ) → (y : OD {suc n}) → ¬ ( def (minimul x ne) (od→ord y)) ∧ (def x (od→ord  y) )
+
 
 _∋_ : { n : Level } → ( a x : OD {n} ) → Set n
 _∋_ {n} a x  = def a ( od→ord x )
 
-_c<_ : { n : Level } → ( x a : OD {n} ) → Set n
-x c< a =  od→ord x o< od→ord a
+Ord : { n : Level } → ( a : Ordinal {suc n} ) → OD {suc n}
+Ord {n} a = record { def = λ y → y o< a } 
+
+_c<_ : { n : Level } → ( x a : Ordinal {n} ) → Set n
+x c< a = Ord a ∋ Ord x
+
+c<→o< : { n : Level } → { x a : OD {n} } → record { def = λ y → y o< od→ord a } ∋ x → od→ord x o< od→ord a
+c<→o< lt = lt
+
+o<→c< : { n : Level } → { x a : OD {n} } → od→ord x o< od→ord a → record { def = λ y → y o< od→ord a } ∋ x 
+o<→c< lt = lt
+
+==→o≡' : {n : Level} →  { x y : Ordinal {suc n} } →  Ord x == Ord y →  x ≡ y 
+==→o≡' {n} {x} {y} eq with trio< {n} x y
+==→o≡' {n} {x} {y} eq | tri< a ¬b ¬c with eq← eq {x} a
+... | t = ⊥-elim ( o<¬≡ x x refl t )
+==→o≡' {n} {x} {y} eq | tri≈ ¬a refl ¬c = refl
+==→o≡' {n} {x} {y} eq | tri> ¬a ¬b c  with eq→ eq {y} c
+... | t = ⊥-elim ( o<¬≡ y y refl t )
 
-postulate      
-   o<→c<  : {n : Level} {x y : Ordinal {n} } → x o< y  → ord→od x c< ord→od y
+∅∨ : { n : Level } → { x y : Ordinal {suc n} } → ( Ord {n} x == Ord y ) ∨ ( ¬ ( Ord x == Ord y ) )
+∅∨ {n} {x} {y} with trio< x y
+∅∨ {n} {x} {y} | tri< a ¬b ¬c = case2 ( λ eq → ¬b ( ==→o≡' eq ) )
+∅∨ {n} {x} {y} | tri≈ ¬a refl ¬c = case1 ( record { eq→ =  id ; eq← = id } ) 
+∅∨ {n} {x} {y} | tri> ¬a ¬b c = case2 ( λ eq → ¬b ( ==→o≡' eq ) )
+
+¬x∋x' : { n : Level } → { x  : Ordinal {n} } → ¬ ( record { def = λ y → y o< x } ∋ record { def = λ y → y o< x } )
+¬x∋x' {n} {record { lv = Zero ; ord = ord }} (case1 ())
+¬x∋x' {n} {record { lv = Suc lx ; ord = Φ .(Suc lx) }} (case1 (s≤s x)) = ¬x∋x' {n} {record { lv = lx ; ord = Φ lx }} (case1 {!!}) 
+¬x∋x' {n} {record { lv = Suc lx ; ord = OSuc (Suc lx) ox }} (case1 (s≤s x)) = ¬x∋x' {n} {record { lv = Suc lx ; ord = ox}}  (case1 {!!}) 
+¬x∋x' {n} {record { lv = lv ; ord = Φ (lv) }} (case2 ())
+¬x∋x' {n} {record { lv = lv ; ord = OSuc (lv) ox }} (case2 x) = 
+   ¬x∋x' {n} {record { lv = lv ; ord = ox }} (case2 {!!}) 
+
+¬x∋x : { n : Level } → { x  : OD {n} } → ¬ x ∋ x
+¬x∋x = {!!}
+
+oc-lemma : { n : Level } → { x : OD {n} } → { oa : Ordinal {n} } → def (record { def = λ y → y o< oa }) oa → ⊥
+oc-lemma {n} {x} {oa} lt = o<¬≡ oa oa refl lt
+
+oc-lemma1 : { n : Level } → { x : OD {n} } → { oa : Ordinal {n} } → od→ord (record { def = λ y → y o< oa }) o< oa → ⊥
+oc-lemma1 {n} {x} {oa} lt = ¬x∋x' {n}   lt -- lt : def (record { def = λ y → y o< oa }) (record { def = λ y → y o< oa })
+
+oc-lemma2 : { n : Level } → { x a : OD {n} } → { oa : Ordinal {n} } → oa o< od→ord (record { def = λ y → y o< oa }) → ⊥
+oc-lemma2 {n} {x} {oa} lt = {!!} 
 
 _c≤_ : {n : Level} →  OD {n} →  OD {n} → Set (suc n)
 a c≤ b  = (a ≡ b)  ∨ ( b ∋ a )
@@ -73,7 +118,11 @@
 def-subst : {n : Level } {Z : OD {n}} {X : Ordinal {n} }{z : OD {n}} {x : Ordinal {n} }→ def Z X → Z ≡ z  →  X ≡ x  →  def z x
 def-subst df refl refl = df
 
--- sup-min : {n : Level } → ( ψ : Ordinal {n} →  Ordinal {n}) → {z : Ordinal {n}}  →  ψ z  o<  z  →   sup-o ψ  o< osuc z
+o<-def : {n : Level } {x y : Ordinal {n} } → x o< y  →  def (record { def = λ x → x o< y }) x
+o<-def x<y = x<y
+
+def-o< : {n : Level } {x y : Ordinal {n} } → def (record { def = λ x → x o< y }) x → x o< y    
+def-o< x<y = x<y
 
 sup-od : {n : Level } → ( OD {n} → OD {n}) →  OD {n}
 sup-od ψ = ord→od ( sup-o ( λ x → od→ord (ψ (ord→od x ))) )
@@ -82,8 +131,16 @@
 sup-c< {n} ψ {x} = def-subst {n} {_} {_} {sup-od ψ} {od→ord ( ψ x )}
         {!!} refl (cong ( λ k → od→ord (ψ k) ) oiso)
 
-∅1 : {n : Level} →  ( x : OD {n} )  → ¬ ( x c< od∅ {n} )
-∅1 {n} x = {!!}
+od∅' : {n : Level} →  OD {n}
+od∅' = record { def = λ x → x o< o∅ }
+
+∅0 : {n : Level} →  od∅ {suc n} == record { def = λ x → x o< o∅ }
+eq→ ∅0 {w} (lift ())
+eq← ∅0 {w} (case1 ())
+eq← ∅0 {w} (case2 ())
+
+∅1 : {n : Level} →  ( x : Ordinal {n} )  → ¬ ( x c< o∅ {n} )
+∅1 {n} x lt = {!!}
 
 ∅3 : {n : Level} →  { x : Ordinal {n}}  → ( ∀(y : Ordinal {n}) → ¬ (y o< x ) ) → x ≡ o∅ {n}
 ∅3 {n} {x} = TransFinite {n} c2 c3 x where
@@ -102,14 +159,6 @@
    ... | t with t (case2 (s< s<refl ) )
    c3 lx (OSuc .lx x₁) d not | t | ()
 
-transitive : {n : Level } { z y x : OD {suc n} } → z ∋ y → y ∋ x → z  ∋ x
-transitive  {n} {z} {y} {x} z∋y x∋y  with  ordtrans {!!} {!!} 
-... | t = lemma0 (lemma t) where
-   lemma : ( od→ord x ) o< ( od→ord z ) → def ( ord→od ( od→ord z )) ( od→ord x)
-   lemma xo<z = {!!}
-   lemma0 :  def ( ord→od ( od→ord z )) ( od→ord x) →  def z (od→ord x)
-   lemma0 dz  = def-subst {suc n} { ord→od ( od→ord z )} { od→ord x} dz (oiso)  refl
-
 ∅5 : {n : Level} →  { x : Ordinal {n} }  → ¬ ( x  ≡ o∅ {n} ) → o∅ {n} o< x
 ∅5 {n} {record { lv = Zero ; ord = (Φ .0) }} not = ⊥-elim (not refl) 
 ∅5 {n} {record { lv = Zero ; ord = (OSuc .0 ord) }} not = case2 Φ<
@@ -166,10 +215,11 @@
 ≡-def : {n : Level} →  { x : Ordinal {suc n} } → x ≡ od→ord (record { def = λ z → z o< x } )
 ≡-def {n} {x} = ==→o≡ {n} (subst (λ k → ord→od x == k ) (sym oiso) lemma ) where
     lemma :  ord→od x == record { def = λ z → z o< x }
-    eq→ lemma {w} z = subst₂ (λ k j → k o< j ) diso refl (subst (λ k → (od→ord ( ord→od w)) o< k ) diso t ) where 
-        t : (od→ord ( ord→od w)) o< (od→ord (ord→od x))
-        t = {!!}
-    eq← lemma {w} z = def-subst {suc n} {_} {_} {ord→od x} {w} {!!} refl refl
+    eq→ lemma {w} lt = {!!}
+        -- ?subst₂ (λ k j → k o< j ) diso refl (subst (λ k → (od→ord ( ord→od w)) o< k ) diso t ) where 
+        --t : (od→ord ( ord→od w)) o< (od→ord (ord→od x))
+        --t = o<-subst lt ? ?
+    eq← lemma {w} lt = def-subst {suc n} {_} {_} {ord→od x} {w} {!!} refl refl
 
 od≡-def : {n : Level} →  { x : Ordinal {suc n} } → ord→od x ≡ record { def = λ z → z o< x } 
 od≡-def {n} {x} = subst (λ k  → ord→od x ≡ k ) oiso (cong ( λ k → ord→od k ) (≡-def {n} {x} ))
@@ -193,11 +243,11 @@
          t : def (ord→od (od→ord a)) (od→ord x)
          t = {!!}
 
-o∅≡od∅ : {n : Level} → ord→od (o∅ {suc n}) ≡ od∅ {suc n}
-o∅≡od∅ {n} with trio< {n} (o∅ {suc n}) (od→ord (od∅ {suc n} ))
+o∅≡od∅ : {n : Level} → ord→od (o∅ {suc n}) ≡ od∅' {suc n}
+o∅≡od∅ {n} with trio< {n} (o∅ {suc n}) (od→ord (od∅' {suc n} ))
 o∅≡od∅ {n} | tri< a ¬b ¬c = ⊥-elim (lemma a) where
-    lemma :  o∅ {suc n } o< (od→ord (od∅ {suc n} )) → ⊥
-    lemma lt with def-subst {!!} oiso refl
+    lemma :  o∅ {suc n } o< (od→ord (od∅' {suc n} )) → ⊥
+    lemma lt with  def-subst {suc n} {_} {_} {_} {_} ( o<→c< ( o<-subst lt (sym diso) refl ) ) refl diso
     lemma lt | t = {!!}
 o∅≡od∅ {n} | tri≈ ¬a b ¬c = trans (cong (λ k → ord→od k ) b ) oiso
 o∅≡od∅ {n} | tri> ¬a ¬b c = ⊥-elim (¬x<0 c)
@@ -205,22 +255,22 @@
 o<→¬== : {n : Level} →  { x y : OD {n} } → (od→ord x ) o< ( od→ord y) →  ¬ (x == y )
 o<→¬== {n} {x} {y} lt eq = o<→o> eq lt
 
-o<→¬c> : {n : Level} →  { x y : OD {n} } → (od→ord x ) o< ( od→ord y) →  ¬ (y c< x )
+o<→¬c> : {n : Level} →  { x y : Ordinal {n} } → x o< y →  ¬ (y c< x )
 o<→¬c> {n} {x} {y} olt clt = o<> olt {!!} where
 
-o≡→¬c< : {n : Level} →  { x y : OD {n} } →  (od→ord x ) ≡ ( od→ord y) →   ¬ x c< y
-o≡→¬c< {n} {x} {y} oeq lt  = o<¬≡ (od→ord x) (od→ord y) (orefl oeq ) lt  
+o≡→¬c< : {n : Level} →  { x y : Ordinal {n} } →  x ≡ y →   ¬ x c< y
+o≡→¬c< {n} {x} {y} oeq lt  = o<¬≡ x y {!!} {!!}  
 
-tri-c< : {n : Level} →  Trichotomous _==_ (_c<_ {suc n})
-tri-c< {n} x y with trio< {n} (od→ord x) (od→ord y) 
-tri-c< {n} x y | tri< a ¬b ¬c = tri< (def-subst {!!} oiso refl) (o<→¬== a) ( o<→¬c> a )
-tri-c< {n} x y | tri≈ ¬a b ¬c = tri≈ (o≡→¬c< b) (ord→== b) (o≡→¬c< (sym b))
-tri-c< {n} x y | tri> ¬a ¬b c = tri>  ( o<→¬c> c) (λ eq → o<→¬== c (eq-sym eq ) ) (def-subst {!!} oiso refl)
+tri-c< : {n : Level} →  Trichotomous _≡_ (_c<_ {suc n})
+tri-c< {n} x y with trio< {n} x y 
+tri-c< {n} x y | tri< a ¬b ¬c = tri< (def-subst {!!} oiso refl) {!!} ( o<→¬c> a )
+tri-c< {n} x y | tri≈ ¬a b ¬c = tri≈ (o≡→¬c< b) {!!} (o≡→¬c< (sym b))
+tri-c< {n} x y | tri> ¬a ¬b c = tri>  ( o<→¬c> c) (λ eq → {!!} ) (def-subst {!!} oiso refl)
 
-c<> : {n : Level } { x y : OD {suc n}} → x c<  y  → y c< x  →  ⊥
+c<> : {n : Level } { x y : Ordinal {suc n}} → x c<  y  → y c< x  →  ⊥
 c<> {n} {x} {y} x<y y<x with tri-c< x y
 c<> {n} {x} {y} x<y y<x | tri< a ¬b ¬c = ¬c y<x
-c<> {n} {x} {y} x<y y<x | tri≈ ¬a b ¬c = o<→o> b x<y 
+c<> {n} {x} {y} x<y y<x | tri≈ ¬a b ¬c = o<→o> {!!} {!!}
 c<> {n} {x} {y} x<y y<x | tri> ¬a ¬b c = ¬a x<y
 
 ∅< : {n : Level} →  { x y : OD {n} } → def x (od→ord y ) → ¬ (  x  == od∅ {n} )
@@ -228,17 +278,11 @@
 ∅< {n} {x} {y} d eq | lift ()
        
 ∅6 : {n : Level} →  { x : OD {suc n} }  → ¬ ( x ∋ x )    --  no Russel paradox
-∅6 {n} {x} x∋x = c<> {n} {x} {x} {!!} {!!}
+∅6 {n} {x} x∋x = c<> {n} {{!!}} {{!!}} {!!} {!!}
 
 def-iso : {n : Level} {A B : OD {n}} {x y : Ordinal {n}} → x ≡ y  → (def A y → def B y)  → def A x → def B x
 def-iso refl t = t
 
-is-∋ : {n : Level} →  ( x y : OD {suc n} ) → Dec ( x ∋ y )
-is-∋ {n} x y with tri-c< x y
-is-∋ {n} x y | tri< a ¬b ¬c = no {!!}
-is-∋ {n} x y | tri≈ ¬a b ¬c = no {!!}
-is-∋ {n} x y | tri> ¬a ¬b c = yes {!!}
-
 is-o∅ : {n : Level} →  ( x : Ordinal {suc n} ) → Dec ( x ≡ o∅ {suc n} )
 is-o∅ {n} record { lv = Zero ; ord = (Φ .0) } = yes refl
 is-o∅ {n} record { lv = Zero ; ord = (OSuc .0 ord₁) } = no ( λ () )
@@ -252,9 +296,9 @@
      lemma ox ne with is-o∅ ox
      lemma ox ne | yes refl with ne ( ord→== lemma1 ) where
          lemma1 : od→ord (ord→od o∅) ≡ od→ord od∅
-         lemma1 = cong ( λ k → od→ord k ) o∅≡od∅
+         lemma1 = cong ( λ k → od→ord k ) {!!}
      lemma o∅ ne | yes refl | ()
-     lemma ox ne | no ¬p = subst ( λ k → def (ord→od ox) (od→ord k) ) o∅≡od∅ {!!}
+     lemma ox ne | no ¬p = subst ( λ k → def (ord→od ox) (od→ord k) ) {!!} {!!}
 
 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
 -- postulate f-extensionality : { n : Level}  → Relation.Binary.PropositionalEquality.Extensionality (suc n) (suc (suc n))
@@ -268,14 +312,14 @@
 ZFSubset A x =  record { def = λ y → def A y ∧  def x y }  
 
 Def :  {n : Level} → (A :  OD {suc n}) → OD {suc n}
-Def {n} A = ord→od ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) )  
+Def {n} A = record { def = λ y → y o< ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )))) }
 
 -- Constructible Set on α
 L : {n : Level} → (α : Ordinal {suc n}) → OD {suc n}
 L {n}  record { lv = Zero ; ord = (Φ .0) } = od∅
 L {n}  record { lv = lx ; ord = (OSuc lv ox) } = Def ( L {n} ( record { lv = lx ; ord = ox } ) ) 
 L {n}  record { lv = (Suc lx) ; ord = (Φ (Suc lx)) } = -- Union ( L α )
-    record { def = λ y → osuc y o< (od→ord (L {n}  (record { lv = lx ; ord = Φ lx }) )) }
+       record { def = λ y → osuc y o< (od→ord (L {n}  (record { lv = lx ; ord = Φ lx }) )) }
 
 OD→ZF : {n : Level} → ZF {suc (suc n)} {suc n}
 OD→ZF {n}  = record { 
@@ -396,15 +440,13 @@
          replacement {ψ} X x = sup-c< ψ {x}
          ∅-iso :  {x : OD} → ¬ (x == od∅) → ¬ ((ord→od (od→ord x)) == od∅) 
          ∅-iso {x} neq = subst (λ k → ¬ k) (=-iso {n} ) neq  
-         minimul : (x : OD {suc n} ) → ¬ (x == od∅ )→ OD {suc n} 
-         minimul x  not = od∅   
          regularity :  (x : OD) (not : ¬ (x == od∅)) →
             (x ∋ minimul x not) ∧ (Select (minimul x not) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁)) == od∅)
-         proj1 (regularity x not ) = ¬∅=→∅∈ not 
+         proj1 (regularity x not ) = x∋minimul x not
          proj2 (regularity x not ) = record { eq→ = reg ; eq← = λ () } where
             reg : {y : Ordinal} → def (Select (minimul x not) (λ x₂ → (minimul x not ∋ x₂) ∧ (x ∋ x₂))) y → def od∅ y
-            reg {y} t with proj1 t
-            ... | x∈∅ = x∈∅
+            reg {y} t  with minimul-1 x not (ord→od y) (proj2 t ) 
+            ... | t1 = lift t1
          extensionality : {A B : OD {suc n}} → ((z : OD) → (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  
          eq← (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {B} {A} (sym diso) (proj2 (eq (ord→od x))) d  
@@ -432,7 +474,7 @@
          infinite = ord→od ( omega )
          infinity∅ : ord→od ( omega ) ∋ od∅ {suc n}
          infinity∅ = def-subst {suc n} {_} {o∅} {infinite} {od→ord od∅}
-              {!!}  refl (subst ( λ k → ( k ≡ od→ord od∅ )) diso (cong (λ k →  od→ord k) o∅≡od∅ ))
+              {!!}  refl (subst ( λ k → ( k ≡ od→ord od∅ )) diso (cong (λ k →  od→ord k) {!!} ))
          infinite∋x : (x : OD) → infinite ∋ x → od→ord x o< omega
          infinite∋x x lt = subst (λ k → od→ord x o< k ) diso t where
               t  : od→ord x o< od→ord (ord→od (omega))