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

changeset 527:634c4a66cfcf

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 Tue, 19 Apr 2022 11:24:55 +0900
parents 7e59e0aeaa73
children 8facdd7cc65a
files src/zorn.agda
diffstat 1 files changed, 31 insertions(+), 65 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Mon Apr 18 23:52:31 2022 +0900
+++ b/src/zorn.agda	Tue Apr 19 11:24:55 2022 +0900
@@ -107,7 +107,7 @@
 -- El-irr : {A : HOD} → {x y : Element A } → elm x ≡ elm y → x ≡ y
 -- El-irr {A} {x} {y} eq = El-irr2 A eq ( is-elm-irr A eq ) 
 
-record Set≈ (A B : Ordinal ) : Set n where
+record _Set≈_ (A B : Ordinal ) : Set n where
    field
        fun←  : {x : Ordinal } → odef (* A)  x → Ordinal
        fun→  : {x : Ordinal } → odef (* B)  x → Ordinal
@@ -116,10 +116,10 @@
        fiso← : {x : Ordinal } → ( lt : odef (* B)  x ) → fun←  ( funA lt ) ≡ x
        fiso→ : {x : Ordinal } → ( lt : odef (* A)  x ) → fun→  ( funB lt ) ≡ x
 
-open Set≈
-record OS≈ {A B : HOD} (TA : IsTotalOrderSet A ) (TB : IsTotalOrderSet B ) : Set (Level.suc n) where
+open _Set≈_
+record _OS≈_ {A B : HOD} (TA : IsTotalOrderSet A ) (TB : IsTotalOrderSet B ) : Set (Level.suc n) where
    field
-      iso : Set≈ (& A) (& B)
+      iso : (& A ) Set≈  (& B)
       fmap : {x y : Ordinal} → (ax : odef A x) → (ay : odef A y) → * x < * y
           → * (fun← iso (subst (λ k → odef k x) (sym *iso) ax)) < * (fun← iso (subst (λ k → odef k y) (sym *iso) ay))
 
@@ -127,13 +127,18 @@
 Cut<  A x = record { od = record { def = λ y → ( odef A y ) ∧ ( x < * y ) } ; odmax = & A
     ; <odmax = λ lt → subst (λ k → k o< & A) &iso (c<→o< (subst (λ k → odef A k ) (sym &iso) (proj1 lt))) }
 
-Cut<TA : {A : HOD}   → (TA : IsTotalOrderSet A ) ( x : HOD )→  IsTotalOrderSet ( Cut< A x )
-Cut<TA {A} TA x =  record { isEquivalence = record { refl = refl ; trans = trans ; sym = sym }
+Cut<T : {A : HOD}   → (TA : IsTotalOrderSet A ) ( x : HOD )→  IsTotalOrderSet ( Cut< A x )
+Cut<T {A} TA x =  record { isEquivalence = record { refl = refl ; trans = trans ; sym = sym }
    ; trans = λ {x} {y} {z} → IsStrictTotalOrder.trans TA {me (proj1 (is-elm x))} {me (proj1 (is-elm y))} {me (proj1 (is-elm z))} ;
-        compare = λ x y → IsStrictTotalOrder.compare TA (me (proj1 (is-elm x))) (me (proj1 (is-elm y)))  }
+         compare = λ x y → IsStrictTotalOrder.compare TA (me (proj1 (is-elm x))) (me (proj1 (is-elm y)))  }
 
-triTO : {A B : HOD} (TA : IsTotalOrderSet A ) (TB : IsTotalOrderSet B ) → {!!}
-triTO = {!!}
+record _OS<_ {A B : HOD} (TA : IsTotalOrderSet A ) (TB : IsTotalOrderSet B ) : Set (Level.suc n) where
+   field
+      x : HOD
+      iso : TA OS≈ (Cut<T TA x) 
+
+OS<-cmp : {x : HOD} → Trichotomous {_} {IsTotalOrderSet x} _OS≈_ _OS<_ 
+OS<-cmp A B = {!!}
 
 record ZChain ( A : HOD ) (y : Ordinal)   : Set (Level.suc n) where
    field
@@ -223,15 +228,15 @@
 --
 -- extract single chain from countable infinite chains
 --
-ChainClosure : (A : HOD) (s : Ordinal) →  (next : Ordinal → Ordinal ) → HOD
-ChainClosure A s next = record { od = record { def = λ x → Chain A s next x } ; odmax = & A ; <odmax = cc01 } where
+TransitiveClosure : (A : HOD) (s : Ordinal) →  (next : Ordinal → Ordinal ) → HOD
+TransitiveClosure A s next = record { od = record { def = λ x → Chain A s next x } ; odmax = & A ; <odmax = cc01 } where
     cc01 : {y : Ordinal} → Chain A s next y → y o< & A
     cc01 {y} cy = subst (λ k → k o< & A ) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso) ( ct∈A A s next cy ) ) )
 
 cton0 : (A : HOD ) (s : Ordinal) → (next : Ordinal  → Ordinal )  {y : Ordinal } → Chain A s next y → ℕ
 cton0 A s next (cfirst _)  = zero
 cton0 A s next (csuc x ax z _) = suc (cton0 A s next z) 
-cton : (A : HOD ) (s : Ordinal)   → (next : Ordinal → Ordinal ) → Element (ChainClosure A s next) → ℕ
+cton : (A : HOD ) (s : Ordinal)   → (next : Ordinal → Ordinal ) → Element (TransitiveClosure A s next) → ℕ
 cton A s next y = cton0 A s next (is-elm y)
 
 cinext :  (A : HOD) {x max : Ordinal } → (ax : A ∋ * x ) → (ifc : InfiniteChain A max ax ) → Ordinal  →  Ordinal
@@ -241,7 +246,7 @@
 
 InFCSet : (A : HOD) → {x max : Ordinal}  (ax : A ∋ * x)
      → (ifc : InfiniteChain A max ax ) → HOD
-InFCSet A {x} ax ifc =  ChainClosure (IChainSet A ax) x (cinext A ax ifc ) 
+InFCSet A {x} ax ifc =  TransitiveClosure (IChainSet A ax) x (cinext A ax ifc ) 
 
 InFCSet⊆A : (A : HOD) → {x max : Ordinal}  (ax : A ∋ * x) →  (ifc : InfiniteChain A max ax ) → InFCSet A ax ifc ⊆ A
 InFCSet⊆A A {x} ax ifc = record { incl = λ {y} lt → incl (IChainSet⊆A ax) (
@@ -253,11 +258,11 @@
 ... | no not = ⊥-elim ( not ay )
 ... | yes ay1 = InfiniteChain.c-infinite ifc y (subst (λ k → odef (IChainSet A ax) k) &iso ay )
 
-ChainClosure-is-total : (A : HOD) → {x max : Ordinal}  (ax : A ∋ * x)
+TransitiveClosure-is-total : (A : HOD) → {x max : Ordinal}  (ax : A ∋ * x)
      → IsPartialOrderSet A 
      → (ifc : InfiniteChain A max ax )
      → IsTotalOrderSet ( InFCSet A ax ifc )
-ChainClosure-is-total A {x} ax PO ifc = record { isEquivalence = IsStrictPartialOrder.isEquivalence IPO
+TransitiveClosure-is-total A {x} ax PO ifc = record { isEquivalence = IsStrictPartialOrder.isEquivalence IPO
    ; trans = λ {x} {y} {z} → IsStrictPartialOrder.trans IPO {x} {y} {z}  ; compare = cmp } where
     IPO : IsPartialOrderSet (InFCSet A ax ifc )
     IPO = ⊆-IsPartialOrderSet record { incl = λ {y} lt → incl (InFCSet⊆A A {x} ax ifc) lt} PO
@@ -294,11 +299,11 @@
               ct011 :  * oy1 < * ( IChainSup>.y (InfiniteChain.c-infinite ifc oy1 (subst (λ k → odef (IChainSet A ax) k) &iso ay1 )) )
               ct011 = IChainSup>.y>x (InfiniteChain.c-infinite ifc oy1 (subst (λ k → odef (IChainSet A ax) k) &iso ay1 )) 
     ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> lt c ) 
-    ct12 : {y z : Element (ChainClosure B x cnext) } → elm y ≡ elm z → elm y < elm z → ⊥ 
+    ct12 : {y z : Element (TransitiveClosure B x cnext) } → elm y ≡ elm z → elm y < elm z → ⊥ 
     ct12 {y} {z} y=z y<z = IsStrictPartialOrder.irrefl IPO {y} {z} y=z y<z
-    ct13 : {y z : Element (ChainClosure B x cnext) } → elm y < elm z → elm z < elm y → ⊥ 
+    ct13 : {y z : Element (TransitiveClosure B x cnext) } → elm y < elm z → elm z < elm y → ⊥ 
     ct13 {y} {z} y<z y>z = IsStrictPartialOrder.irrefl IPO {y} {y} refl ( IsStrictPartialOrder.trans IPO {y} {z} {y} y<z y>z )
-    ct17 : (x1 : Element (ChainClosure B x cnext)) → Chain B x cnext (& (elm x1))
+    ct17 : (x1 : Element (TransitiveClosure B x cnext)) → Chain B x cnext (& (elm x1))
     ct17 x1 = is-elm x1
     cmp : Trichotomous _ _ 
     cmp x1 y with NP.<-cmp (cton B x cnext x1) (cton B x cnext y)
@@ -320,6 +325,12 @@
         ct15 : ¬ (elm x1 <  elm y)
         ct15 lt = ct13 {x1} {y} lt (subst₂ (λ j k → j < k ) *iso *iso (ct-monotonic (is-elm y) (is-elm x1) c )  )
 
+extendInfiniteChain : (A : HOD) → {x mx y my : Ordinal}  (ax : A ∋ * x) (ay : A ∋ * y)
+     → IsPartialOrderSet A 
+     → (ifcx : InfiniteChain A mx ax ) → (ifcy : InfiniteChain A my ay )
+     → * mx < * my
+     → InfiniteChain A my ax 
+extendInfiniteChain = ?
       
 record IsFC (A : HOD) {x : Ordinal}  (ax : A ∋ * x) (y : Ordinal) : Set n where
    field
@@ -423,57 +434,12 @@
              y<z  = ic→< {A} PO y (subst (λ k → odef A k) &iso ay) (IChained.iy (proj2 icy))
                (subst (λ k → ic-connect k (IChained.iy (proj2 icy))) &iso (IChained.ic (proj2 icy)))
 
-
-record Indirect<  {x z : HOD} (x<z : x < z ) : Set (Level.suc n) where
-   field
-      y y1 : HOD
-      =∨< : ( y ≡ y1 ) ∨ ( y < y1 )
-      dirct : ¬ ( (x < y ) ∧ ( y1 < z ))
-
-record NChain ( A : HOD ) (f : { x : HOD} → A ∋ x → HOD) (min : HOD) : Set (Level.suc n) where
-   field
-      N : HOD
-      N⊆A : N ⊆ A
-      nmin : N ∋ min
-      is-min : (x : HOD) → N ∋ x → ( min ≡ x ) ∨ ( min < x )
-      total : IsTotalOrderSet N
-      A∋fx : { x : HOD} → (ax : A ∋ x ) → A ∋ f ax
-      atomic : { x y : HOD } → (nx : N ∋ x)  → (x<y : x < y)  → ¬ Indirect< x<y → y ≡ f (incl N⊆A nx )
-
 record SUP ( A B : HOD )  : Set (Level.suc n) where
    field
       sup : HOD
       A∋maximal : A ∋ sup
       x<sup : {x : HOD} → B ∋ x → (x ≡ sup ) ∨ (x < sup )   -- B is Total, use positive
 
-record Zfixpoint (A : HOD ) (f : { x : HOD} → A ∋ x → HOD) : Set (Level.suc n) where
-   field
-      fx  : HOD
-      afx : A ∋ fx 
-      is-fx : fx ≡ f afx 
-
-Zorn-fixpoint : { A : HOD } 
-    → o∅ o< & A 
-    → IsPartialOrderSet A 
-    → ( ( B : HOD) → (B⊆A : B ⊆ A) → IsTotalOrderSet B → SUP A B   ) -- SUP condition
-    → (f : { x : HOD} → A ∋ x → HOD ) → ( A∋fx : {x : HOD}   (ax : A ∋ x ) → A ∋ f ax )
-    → (f≤ : {x : HOD} → (ax : A ∋ x ) → (x ≡ f ax ) ∨ (x < f ax ))
-    → Zfixpoint A f
-Zorn-fixpoint  = {!!}
-
-record Zmono (A : HOD ) : Set (Level.suc n) where
-   field
-      f : { x : HOD} → A ∋ x → HOD
-      A∋fx : { x : HOD} → (ax : A ∋ x ) → A ∋ f ax
-      monotonic : { x y : HOD} → (ax : A ∋ x )  → x < f ax
-
-Zorn-monotonic : { A : HOD } 
-    → o∅ o< & A 
-    → IsPartialOrderSet A 
-    → ¬ ( Maximal A )
-    → Zmono A
-Zorn-monotonic = {!!}
-
 Zorn-lemma : { A : HOD } 
     → o∅ o< & A 
     → IsPartialOrderSet A 
@@ -503,7 +469,7 @@
               nxa : A ∋ * nx
               nxa = {!!} -- cinext∈A A ax ifc (& (SUP.sup sup)) {!!}
           zc5 : InfiniteChain A max ax → ⊥
-          zc5 ifc = zc6 ifc ( supP (InFCSet A ax ifc) (InFCSet⊆A A {x} ax ifc) (  ChainClosure-is-total  A {x} ax PO ifc ))
+          zc5 ifc = zc6 ifc ( supP (InFCSet A ax ifc) (InFCSet⊆A A {x} ax ifc) (  TransitiveClosure-is-total  A {x} ax PO ifc ))
      z03 : {x : Ordinal } → (ax : A ∋ * x ) → InfiniteChain A (& A)  ax  → ⊥
      z03 {x}  ax ifc = {!!}
      -- ZChain is not compatible with the SUP condition
@@ -539,7 +505,7 @@
               zc6 :  (ifc : InfiniteChain A x ax ) → ¬ SUP A (B ifc)
               zc6 = {!!}
               FC-is-total : (ifc : InfiniteChain A x ax)  → IsTotalOrderSet (B ifc)
-              FC-is-total ifc = ChainClosure-is-total A ax PO ifc 
+              FC-is-total ifc = TransitiveClosure-is-total A ax PO ifc 
               B⊆A : (ifc : InfiniteChain A x ax)  →   B ifc ⊆ A
               B⊆A = {!!}
               ifc : InfiniteChain A x (subst (OD.def (od A)) (sym &iso) ax) → InfiniteChain A x ax