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

changeset 512:7cf24b846920

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, 16 Apr 2022 00:26:38 +0900
parents 361021fe53aa
children 5077d708f32f
files src/zorn.agda
diffstat 1 files changed, 28 insertions(+), 29 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Fri Apr 15 20:02:12 2022 +0900
+++ b/src/zorn.agda	Sat Apr 16 00:26:38 2022 +0900
@@ -145,6 +145,9 @@
 IChainSet {A} ax = record { od = record { def = λ y → odef A y ∧ IChained A (& (elm ax)) y }
     ; odmax = & A ; <odmax = λ {y} lt → subst (λ k → k o< & A) &iso (c<→o< (subst (λ k → odef A k) (sym &iso) (proj1 lt))) } 
 
+IChainSet⊆A :  {A : HOD} → (x : Element A ) → IChainSet x ⊆ A
+IChainSet⊆A {A} x = record { incl = λ {oy} y → proj1 y }
+
 -- there is a y, & y > & x
 
 record OSup> (A : HOD) {x : Ordinal} (ax : A ∋ * x) : Set n where
@@ -176,23 +179,29 @@
 
 data Chain (A : HOD) (next : (x : Ordinal ) → odef A x → Ordinal ) : ( x : Ordinal  ) → Set n where
      cfirst : (x : Ordinal ) → odef A x → Chain A next x
-     csuc : (x : Ordinal ) → (ax : odef A x ) → Chain A next x → Chain A next (next x ax )
+     csuc : (x : Ordinal ) → (ax : odef A x ) → Chain A next x → odef A (next x ax) → Chain A next (next x ax )
+
+ct∈A : (A : HOD )  → (next : (x : Ordinal ) → odef A x → Ordinal ) → {x : Ordinal} → Chain A next x → odef A x
+ct∈A A next {x} (cfirst .x x₁) = x₁ 
+ct∈A A next {.(next x ax)} (csuc x ax t anx) = anx
 
 ChainClosure : (A : HOD) →  (next : (x : Ordinal ) → odef A x → Ordinal ) → HOD
-ChainClosure A  next = record { od = record { def = λ x → Chain A next x } ; odmax = {!!} ; <odmax = {!!} }
+ChainClosure A  next = record { od = record { def = λ x → Chain A next x } ; odmax = & A ; <odmax = {!!} }
 
 cton0 : (A : HOD )  → (next : (x : Ordinal ) → odef A x → Ordinal )  {y : Ordinal } → Chain A next y → ℕ
 cton0 A next (cfirst _ x) = zero
-cton0 A next (csuc x ax z) = suc (cton0 A next z)
+cton0 A next (csuc x ax z _) = suc (cton0 A next z) 
 cton : (A : HOD )  → (next : (x : Ordinal ) → odef A x → Ordinal ) → Element (ChainClosure A next) → ℕ
 cton A next y = cton0 A next (is-elm y)
-ct∈A : (A : HOD )  → (next : (x : Ordinal ) → odef A x → Ordinal ) → {x : Ordinal} → Chain A next x → odef A x
-ct∈A = {!!}
 
 InFCSet : (A : HOD) → {x : Ordinal}  (ax : A ∋ * x)
      → (ifc : InFiniteIChain A ax ) → HOD
 InFCSet A ax ifc =  ChainClosure (IChainSet {A} (me ax)) (λ y ay → IChainSup>.y ( InFiniteIChain.c-infinite ifc y ay ) ) 
 
+InFCSet⊆A : (A : HOD) → {x : Ordinal}  (ax : A ∋ * x) →  (ifc : InFiniteIChain A ax ) → InFCSet A ax ifc ⊆ A
+InFCSet⊆A A {x} ax ifc = record { incl = λ {y} lt → incl (IChainSet⊆A (me ax)) (
+     ct∈A (IChainSet {A} (me ax)) (λ y ay → IChainSup>.y ( InFiniteIChain.c-infinite ifc y ay ) ) lt ) }
+
 ChainClosure-is-total : (A : HOD) → {x : Ordinal}  (ax : A ∋ * x)
      → IsPartialOrderSet A 
      → (ifc : InFiniteIChain A ax )
@@ -200,16 +209,20 @@
 ChainClosure-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 = λ {x} lt → {!!} } PO
+    IPO = ⊆-IsPartialOrderSet record { incl = λ {y} lt → incl (InFCSet⊆A A {x} ax ifc) lt} PO
     B = IChainSet {A} (me ax)
     cnext :  (y : Ordinal ) → odef B y → Ordinal
     cnext y ay = IChainSup>.y ( InFiniteIChain.c-infinite ifc y ay  )
+    ct02 : {ox : Ordinal} → (x : Chain B cnext ox ) → A ∋ * ox 
+    ct02 x = incl (IChainSet⊆A {A} (me ax)) (subst (λ k → odef (IChainSet (me ax)) k) (sym &iso) (ct∈A B cnext x) ) 
     ct-monotonic : {ox oy : Ordinal} → (x : Chain B cnext ox ) → (y : Chain B cnext oy )
        → (cton0 B cnext x) Data.Nat.< (cton0 B cnext y) → * ox < * oy
-    ct-monotonic x (csuc oy ax y) (s≤s lt) with NP.<-cmp ( cton0 B cnext x ) ( cton0 B cnext y )
-    ... | tri< a ¬b ¬c = IsStrictPartialOrder.trans PO {me {!!}} {me {!!}} (ct-monotonic x y a ) ct01  where
-        ct01 : * oy < * ( IChainSup>.y (InFiniteIChain.c-infinite ifc oy ax) )
-        ct01 = (IChainSup>.y>x (InFiniteIChain.c-infinite ifc oy ax))
+    ct-monotonic {ox} {oy} x (csuc oy1 ay y _) (s≤s lt) with NP.<-cmp ( cton0 B cnext x ) ( cton0 B cnext y )
+    ... | tri< a ¬b ¬c = IsStrictPartialOrder.trans PO {me (ct02 x) } {me (ct02 y)} {me ct03} (ct-monotonic x y a ) ct01  where
+        ct03 : A ∋ * (IChainSup>.y (InFiniteIChain.c-infinite ifc oy1 ay))
+        ct03 = subst (λ k → odef A k ) (sym &iso) (IChainSup>.A∋y (InFiniteIChain.c-infinite ifc oy1 ay))
+        ct01 : * oy1 < * ( IChainSup>.y (InFiniteIChain.c-infinite ifc oy1 ay) )
+        ct01 = (IChainSup>.y>x (InFiniteIChain.c-infinite ifc oy1 ay))
     ... | tri≈ ¬a b ¬c = {!!}
     ... | tri> ¬a ¬b c = {!!}
     cmp : Trichotomous _ _ 
@@ -307,24 +320,6 @@
      -- ZChain is not compatible with the SUP condition
      ind : (x : Ordinal) → ((y : Ordinal) → y o< x →  ZChain A y ∨ Maximal A )
          →  ZChain A x ∨ Maximal A 
-     --     has previous ordinal
-     --        has maximal          use this
-     --        else has chain
-     --        & A < y              A is a counter example of assumption
-     --          chack y is maximal 
-     --          y < max              use previous chain
-     --          y = max  (  y > max  cannot happen )
-     --              ¬ A ∋ y           use previous chain
-     --              A ∋ y is use oridinaly min of y or previous
-     --     y is limit ordinal    
-     --        has maximal in some lower   use this
-     --        no maximal in all lower
-     --          & A < y              A is a counter example of assumption
-     --          A ∋ y is maximal      use this            
-     --          ¬ A ∋ y           use previous chain
-     --          check some y ≤ max 
-     --              if none A < y is the counter example
-     --              else use the ordinaly smallest max as next chain
      ind x prev with Oprev-p x
      ... | yes op with ODC.∋-p O A (* x)
      ... | no ¬Ax = zc1 where
@@ -359,7 +354,11 @@
               B⊆A : (ifc : InFiniteIChain A ax)  →   B ifc ⊆ A
               B⊆A = {!!}
               ifc : InFiniteIChain A (subst (OD.def (od A)) (sym &iso) ax) → InFiniteIChain A ax
-              ifc record { chain<x = chain<x ; c-infinite = c-infinite } = record { chain<x = ? ; c-infinite = ? } 
+              ifc record { chain<x = chain<x ; c-infinite = c-infinite } = record { chain<x = {!!} ; c-infinite = {!!} }  where
+                  ifc01 : {!!} -- me (subst (OD.def (od A)) (sym &iso) ax)
+                  ifc01 = {!!}
+               -- (y : Ordinal) → odef (IChainSet (me (subst (OD.def (od A)) (sym &iso) ax))) y → y o< & (* x₁)
+               --  (y : Ordinal) → odef (IChainSet (me ax)) y → y o< x₁
               zc5 : InFiniteIChain A (subst (OD.def (od A)) (sym &iso) ax) → ⊥
               zc5 x = zc6 (ifc x) ( supP (B (ifc x)) (B⊆A (ifc x)) (FC-is-total (ifc x) ))
      ind x prev | no ¬ox with trio< (& A) x   --- limit ordinal case