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

changeset 658:a7a0df28086d

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 Sat, 02 Jul 2022 18:50:11 +0900
parents 5e056537807d
children b8dca06b6372
files src/zorn.agda
diffstat 1 files changed, 35 insertions(+), 38 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Sat Jul 02 10:51:48 2022 +0900
+++ b/src/zorn.agda	Sat Jul 02 18:50:11 2022 +0900
@@ -26,7 +26,6 @@
 open import Data.Nat.Properties 
 open import nat 
 
-
 open inOrdinal O
 open OD O
 open OD.OD
@@ -38,16 +37,11 @@
 open Ordinals.IsNext isNext
 open OrdUtil O
 open ODUtil O
-
-
 import ODC
 
-
 open _∧_
 open _∨_
 open Bool
-
-
 open HOD
 
 --
@@ -140,7 +134,6 @@
                fc05 = fc00 i j (cong pred i=j) cx cy1 (cong pred i=x) (cong pred j=y1)
      ... | case2 x₁ | case2 x₂ = subst₂ (λ j k → * (f j) ≡ * (f k) ) &iso &iso (cong (λ k → * (f (& k))) (fc00 i j (cong pred i=j) cx cy (cong pred i=x) (cong pred j=y)))
 
-
 fcn-< : {A : HOD} (s : Ordinal ) { x y : Ordinal} {f : Ordinal → Ordinal} → (mf : ≤-monotonic-f A f)
     → (cx : FClosure A f s x ) (cy : FClosure A f s y ) → fcn s mf cx Data.Nat.< fcn s mf cy  → * x < * y
 fcn-< {A} s {x} {y} {f} mf cx cy x<y = fc01 (fcn s mf cy) cx cy refl x<y where
@@ -169,14 +162,13 @@
       fc12 : * y < * x
       fc12 = fcn-< {A} s {y} {x} {f} mf cy cx c
 
-
 fcn-imm : {A : HOD} (s : Ordinal) { x y : Ordinal } (f : Ordinal → Ordinal) (mf : ≤-monotonic-f A f) 
     → (cx : FClosure A f s x) → (cy : FClosure A f s y ) → ¬ ( ( * x < * y ) ∧ ( * y < * (f x )) ) 
 fcn-imm {A} s {x} {y} f mf cx cy ⟪ x<y , y<fx ⟫ = fc21 where
       fc20 : fcn s mf cy Data.Nat.< suc (fcn s mf cx) → (fcn s mf cy ≡ fcn s mf cx) ∨ ( fcn s mf cy Data.Nat.< fcn s mf cx )
       fc20 y<sx with <-cmp ( fcn s mf cy ) (fcn s mf cx )
       ... | tri< a ¬b ¬c = case2 a
-      ... | tri≈ ¬a b ¬c = case1 b
+      ... | tri≈ ¬a b ¬c = case1 b 
       ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> y<sx (s≤s c))
       fc17 : {x y : Ordinal } → (cx : FClosure A f s x) → (cy : FClosure A f s y ) → suc (fcn s mf cx) ≡ fcn s mf cy → * (f x ) ≡ * y
       fc17 {x} {y} cx cy sx=y = fc18 (fcn s mf cy) cx cy refl sx=y  where
@@ -239,12 +231,12 @@
       A∋maximal : A ∋ sup
       x<sup : {x : HOD} → B ∋ x → (x ≡ sup ) ∨ (x < sup )   -- B is Total, use positive
 
-record UChain (chain : Ordinal → HOD) (x : Ordinal) (z : Ordinal) : Set n where 
+record UChain (x : Ordinal) (chain : (z : Ordinal ) → z o< x → HOD)  (z : Ordinal) : Set n where 
    -- Union of supf z which o< x
    field
       u : Ordinal
       u<x : u o< x
-      chain∋z : odef (chain u) z
+      chain∋z : odef (chain u u<x ) z
 
 ∈∧P→o< :  {A : HOD } {y : Ordinal} → {P : Set n} → odef A y ∧ P → y o< & A
 ∈∧P→o< {A } {y} p = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) (proj1 p )))
@@ -259,9 +251,9 @@
     ch-skip : {x : Ordinal } { chain : HOD } ( op : Oprev Ordinal osuc x ) ( ax : odef A x ) 
         ( c : Chain A f ay (Oprev.oprev op) chain) ( nh : ¬  HasPrev A chain ax f ) ( nsup : ¬ IsSup A chain ax ) → Chain A f ay x chain
     ch-union : {x : Ordinal } { chain : HOD } ( nop : ¬ Oprev Ordinal osuc x ) ( ax : odef A x ) 
-         → ( chainf : Ordinal → HOD ) → ( lt : ( z : Ordinal ) → z o< x → Chain A f ay z ( chainf z ))
+         → ( chainf : ( z : Ordinal ) → z o< x → HOD )
          → Chain A f ay x 
-             record { od = record { def = λ z → odef A z ∧ (UChain chainf x z ∨ FClosure A f y z ) } 
+             record { od = record { def = λ z → odef A z ∧ (UChain x chainf z ∨ FClosure A f y z ) } 
                 ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy }
 
 record ZChain ( A : HOD )    ( f : Ordinal → Ordinal ) {init : Ordinal} (ay : odef A init) ( z : Ordinal ) : Set (Level.suc n) where
@@ -304,7 +296,7 @@
      as0 : odef A  (& s  )
      as0 =  subst (λ k → odef A k ) &iso as
      s<A : & s o< & A
-     s<A = c<→o< (subst (λ k → odef A (& k) ) *iso as )
+     s<A = c<→o< (subst (λ k → odef A (& k) ) *iso as ) 
      HasMaximal : HOD
      HasMaximal = record { od = record { def = λ x → odef A x ∧ ( (m : Ordinal) →  odef A m → ¬ (* x < * m)) }  ; odmax = & A ; <odmax = z07 } 
      no-maximum : HasMaximal =h= od∅ → (x : Ordinal) → odef A x ∧ ((m : Ordinal) →  odef A m →  odef A x ∧ (¬ (* x < * m) )) →  ⊥
@@ -321,7 +313,7 @@
 
      -- Uncountable ascending chain by axiom of choice
      cf : ¬ Maximal A → Ordinal → Ordinal
-     cf  nmx x with ODC.∋-p O A (* x)
+     cf  nmx x with ODC.∋-p O A (* x) 
      ... | no _ = o∅
      ... | yes ax with is-o∅ (& ( Gtx ax ))
      ... | yes nogt = -- no larger element, so it is maximal
@@ -394,7 +386,6 @@
                z17 with z15
                ... | case1 eq = ¬b eq
                ... | case2 lt = ¬a lt
-
      -- ZChain contradicts ¬ Maximal
      --
      -- ZChain forces fix point on any ≤-monotonic function (fixpoint)
@@ -412,7 +403,6 @@
      --
      -- create all ZChains under o< x
      --
-
      ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (x : Ordinal) 
          → ((z : Ordinal) → z o< x → ZChain A f ay z) → ZChain A f ay x
      ind f mf {y} ay x prev with Oprev-p x
@@ -436,13 +426,13 @@
                     HasPrev A (ZChain.chain zc) ab f ∨  IsSup A (ZChain.chain zc) ab →
                             * a < * b → odef (ZChain.chain zc) b ) → ZChain A f ay  x
           no-extenion is-max = record { 
-                       chainf = {!!}
-                     ; chain-uniq = {!!}
-                     ; chain⊆A = {!!} -- subst (λ k → k ⊆' A ) {!!} (ZChain.chain⊆A zc)
+                       chainf = ?
+                     ; chain-uniq = ?
+                     ; chain⊆A = ? -- subst (λ k → k ⊆' A ) {!!} (ZChain.chain⊆A zc)
                      ; chain∋init  = subst (λ k → odef k y ) {!!} (ZChain.chain∋init  zc) 
                      ; initial = subst (λ k →  {y₁ : Ordinal} → odef k y₁ → * y ≤ * y₁ ) {!!} (ZChain.initial zc)
                      ; f-next =  subst (λ k → {a : Ordinal} → odef k a → odef k (f a) ) {!!} (ZChain.f-next zc) 
-                     ; f-total = {!!} 
+                     ; f-total = ?   
                      ; is-max = subst (λ k → {a b : Ordinal} → odef k a → b o< osuc x → (ab : odef A b) →
                                  HasPrev A k ab f ∨  IsSup A k ab → * a < * b → odef k b  ) {!!} is-max } where
                 supf0 : Ordinal → HOD
@@ -462,7 +452,7 @@
                 ... | tri> ¬a ¬b c  = ⊥-elim (¬a  b<x )
 
           zc4 : ZChain A f ay x 
-          zc4 with ODC.∋-p O A (* x)
+          zc4 with ODC.∋-p O A (* x) 
           ... | no noax = no-extenion zc1  where -- ¬ A ∋ p, just skip
                 zc1 : {a b : Ordinal} → odef (ZChain.chain zc) a → b o< osuc x → (ab : odef A b) →
                     HasPrev A (ZChain.chain zc) ab f ∨  IsSup A (ZChain.chain zc) ab →
@@ -590,32 +580,39 @@
                 ... | case1 pr = ⊥-elim ( ¬fy<x record {y = HasPrev.y pr ; ay = HasPrev.ay pr ; x=fy = trans (trans &iso (sym b=x) ) (HasPrev.x=fy pr ) } )
                 ... | case2 b=sup = ⊥-elim ( ¬x=sup record { 
                       x<sup = λ {y} zy → subst (λ k → (y ≡ k) ∨ (y << k)) (trans b=x (sym &iso)) (IsSup.x<sup b=sup zy)  } ) 
-     ... | no ¬ox = record { chain⊆A = {!!} ; f-next = {!!} ; f-total = {!!}
+     ... | no ¬ox = record { chainf = supf0 ; chain⊆A = {!!} ; f-next = {!!} ; f-total = ? ; chain-uniq = ?
                      ; initial = {!!} ; chain∋init  = {!!} ; is-max = {!!} }   where --- limit ordinal case
-         supf : Ordinal → HOD
-         supf = {!!}
-         uzc : {z : Ordinal} → (u : UChain supf x z) → ZChain A f ay (UChain.u u)
+         supf : (z : Ordinal ) → z o< x → HOD
+         supf z z<x = ZChain.chainf (prev z z<x ) z
+         uzc : {z : Ordinal} → (u : UChain x supf z) → ZChain A f ay (UChain.u u)
          uzc {z} u =  prev (UChain.u u) (UChain.u<x u) 
          Uz : HOD
-         Uz = record { od = record { def = λ z → odef A z ∧ ( UChain supf z x ∨ FClosure A f y z ) } ; odmax = & A ; <odmax = {!!}  }
-         u-next : {z : Ordinal} → odef Uz z → odef Uz (f z)
-         u-next {z} = {!!}
+         Uz = record { od = record { def = λ z → odef A z ∧ ( UChain x supf z ∨ FClosure A f y z ) } ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy  }
+         supf0 : Ordinal → HOD
+         supf0 z with trio< z x
+         ... | tri< a ¬b ¬c = supf z a
+         ... | tri≈ ¬a b ¬c = Uz 
+         ... | tri> ¬a ¬b c = Uz
+         u-next : {a : Ordinal} → odef (supf0 x) a → odef (supf0 x) (f a)
+         u-next {z} = ?
          -- (case1 u) = case1 record { u = UChain.u u ; u<x = UChain.u<x u ; chain∋z = ZChain.f-next ( uzc u ) (UChain.chain∋z u)  }
          -- u-next {z} (case2 u) = case2 ( fsuc _ u )
-         u-initial :  {z : Ordinal} → odef Uz z → * y ≤ * z 
-         u-initial {z} = {!!}
+         u-initial :  {z : Ordinal} → odef (supf0 x) z → * y ≤ * z
+         u-initial {z} = ?
          -- (case1 u) = ZChain.initial ( uzc u )  (UChain.chain∋z u)
          -- u-initial {z} (case2 u) = s≤fc _ f mf u
          u-chain∋init :  odef Uz y
-         u-chain∋init = {!!} -- case2 ( init ay )
-         supf0 : Ordinal → HOD
-         supf0 z with trio< z x
-         ... | tri< a ¬b ¬c = {!!}
-         ... | tri≈ ¬a b ¬c = Uz 
-         ... | tri> ¬a ¬b c = Uz
+         u-chain∋init = ? -- case2 ( init ay )
+         u-mono-ind : (z : Ordinal) {cz : HOD} (Cz : Chain A f ay z cz)  (x : Ordinal) →
+            ((w : Ordinal) → w o< x → z o≤ w → {cw : HOD} → Chain A f ay w cw → cw ⊆' cz) →
+            z o≤ x → {cx : HOD} → Chain A f ay x cx → cx ⊆' cz
+         u-mono-ind z {cz} Cz x prev z≤x {cx} Cx = ?
+         u-mono-chain :  {x z : Ordinal}  → z o≤ x → { cx cz : HOD } → (Cx : Chain A f ay x cx ) ( Cz : Chain A f ay z cz ) → cx ⊆' cz
+         u-mono-chain {x} {z}  z≤x {cx} {cz} Cx Cz = TransFinite 
+              {λ x → z o≤ x → { cx : HOD } → (Cx : Chain A f ay x cx )  → cx ⊆' cz } (u-mono-ind z Cz) x z≤x Cx 
          u-mono :  {z : Ordinal} {w : Ordinal} → z o≤ w → w o≤ x → supf0 z ⊆' supf0 w
          u-mono {z} {w} z≤w w≤x {i} with trio< z x | trio< w x
-         ... | s | t = {!!}
+         ... | s | t = ?
          
      SZ : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → ZChain A f ay (& A)
      SZ f mf {y} ay = TransFinite {λ z → ZChain A f ay   z  } (λ x → ind f mf ay x ) (& A)