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

changeset 509:72ea26339f66

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
chain closure
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 15 Apr 2022 16:46:54 +0900
parents d0ae1e3288f2
children ec84dce16697
files src/zorn.agda
diffstat 1 files changed, 30 insertions(+), 63 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Fri Apr 15 12:24:38 2022 +0900
+++ b/src/zorn.agda	Fri Apr 15 16:46:54 2022 +0900
@@ -47,12 +47,13 @@
 
 open Element
 
+_<A_ : {A : HOD} → (x y : Element A ) → Set n
+x <A y = elm x < elm y
+_≡A_ : {A : HOD} → (x y : Element A ) → Set (Level.suc n)
+x ≡A y = elm x ≡ elm y
+
 IsPartialOrderSet : ( A : HOD ) → Set (Level.suc n)
-IsPartialOrderSet A = IsStrictPartialOrder _≡A_ _<A_  where
-   _<A_ : (x y : Element A ) → Set n
-   x <A y = elm x < elm y
-   _≡A_ : (x y : Element A ) → Set (Level.suc n)
-   x ≡A y = elm x ≡ elm y
+IsPartialOrderSet A = IsStrictPartialOrder (_≡A_ {A}) _<A_  
 
 open _==_
 open _⊆_
@@ -79,11 +80,7 @@
 -- open import Relation.Binary.Properties.Poset as Poset
 
 IsTotalOrderSet : ( A : HOD ) →  Set (Level.suc n)
-IsTotalOrderSet A = IsStrictTotalOrder  _≡A_ _<A_ where
-   _<A_ : (x y : Element A ) → Set n
-   x <A y = elm x < elm y
-   _≡A_ : (x y : Element A ) → Set (Level.suc n)
-   x ≡A y = elm x ≡ elm y
+IsTotalOrderSet A = IsStrictTotalOrder  (_≡A_ {A}) _<A_ 
 
 me : { A a : HOD } → A ∋ a → Element A
 me {A} {a} lt = record { elm = a ; is-elm = lt }
@@ -148,59 +145,6 @@
 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))) } 
 
-open import Data.Nat hiding (_<_) 
-import Data.Nat.Properties as NP
-open import nat
-
---   x < ... < y
---   x < ... < y  ... < z
-
-iclen : (A : HOD) → {y : Ordinal} → IChain A y → ℕ
-iclen A {y} (ifirst x) = zero
-iclen A {y} (inext {ox} x x₁ ic) = suc ( iclen A {ox} ic )
-
-ic-1 : (A : HOD) → {x y1 y : Ordinal} → (cy : IChain A y ) → { ay1 : odef A y1 } → { y<y1 : * y < * y1 }
-     → ic-connect x (inext {A} {y} {y1} ay1 y<y1 cy) → (x ≡ y ) ∨ ic-connect x cy
-ic-1 A {x} {y1} {.x} cy {ay1} {y<y1} (case1 refl) = case1 refl
-ic-1 A {x} {y1} {y} cy {ay1} {y<y1} (case2 icy) = case2 icy
-
-ic-0 : (A : HOD) → {s x y : Ordinal} → {cx : IChain A x } {cy : IChain A y }
-    → ic-connect s cx → ¬ ic-connect x cy → ¬ ic-connect s cy
-ic-0 = {!!}
-
-ic-∨ : (A : HOD) → {s x y : Ordinal} → {cx : IChain A x } {cy : IChain A y }
-    → ic-connect s cx → ic-connect s cy
-    → ic-connect x cy ∨ ic-connect y cx
-ic-∨ = {!!}
-
-iclen-monotonic : (A : HOD) → IsPartialOrderSet A → {s x y : Ordinal} → {cx : IChain A x } {cy : IChain A y }
-    → ic-connect s cx → ic-connect s cy
-    → iclen A cx Data.Nat.≤ iclen A cy → (x ≡ y) ∨ ( (* x) < (* y) )
-iclen-monotonic A PO {s} {x} {y} {cx} {inext x₁ x₂ cy} ix (case1 s=ox ) le = {!!}
-iclen-monotonic A PO {s} {x} {y} {inext {ox} {x} x₃ x₄ cx} {inext {oy} {y} x₁ x₂ cy} ix (case2 icy) (s≤s le) = ic02 where
-     ic02 : (x ≡ y) ∨ (* x < * y)
-     ic02 with NP.<-cmp (iclen A (inext x₃ x₄ cx)) (suc ( iclen A cy ))
-     ... | tri< a ¬b ¬c =  ic03 where
-        ic01 : (x ≡ oy) ∨ ( (* x) < (* oy ))
-        ic01 = iclen-monotonic A PO {s} {x} {oy} {inext x₃ x₄ cx} {cy} ix icy {!!}
-        ic03 : (x ≡ y) ∨ ( (* x) < (* y ))
-        ic03 with ic01
-        ... | case1 x=oy = {!!}
-        ... | case2 x<oy =  case2 ( IsStrictPartialOrder.trans PO {!!} {!!} )
-     ... | tri≈ ¬a b ¬c = case2 ( subst (λ k → * k < * y) {!!} x₂ ) -- suc (iclen A cx) ≡ suc (iclen A cy) → → oy ≡ x
-     ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> (s≤s le) c )
-
-IC-is-total : {A : HOD} → (ax : Element A ) → IsPartialOrderSet A → IsTotalOrderSet (IChainSet {A} ax)
-IC-is-total {A} ax PO = record { isEquivalence = IsStrictPartialOrder.isEquivalence IPO
-   ; trans = λ {x} {y} {z} → IsStrictPartialOrder.trans IPO {x} {y} {z}  ; compare = cmp } where
-    IPO : IsPartialOrderSet (IChainSet {A} ax)
-    IPO = ⊆-IsPartialOrderSet record { incl = λ {x} lt → proj1 lt } PO
-    cmp : Trichotomous _ _ 
-    cmp x y with iclen A (IChained.iy (proj2 (is-elm x))) | iclen A (IChained.iy (proj2 (is-elm y)))
-    ... | zero | zero = {!!}
-    ... | zero | suc t = {!!}
-    ... | suc s | zero = {!!}
-    ... | suc s | suc t = {!!}
 -- there is a y, & y > & x
 
 record OSup> (A : HOD) {x : Ordinal} (ax : A ∋ * x) : Set n where
@@ -222,6 +166,29 @@
       chain<x : (y : Ordinal ) → odef (IChainSet {A} (me ax)) y →  y o< x
       c-infinite : (y : Ordinal ) → (cy : odef (IChainSet {A} (me ax)) y  )
           → IChainSup> A ax
+
+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 )
+
+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 = {!!} }
+
+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 ) ) 
+
+ChainClosure-is-total : (A : HOD) → {x : Ordinal}  (ax : A ∋ * x)
+     → IsPartialOrderSet A 
+     → (ifc : InFiniteIChain A ax )
+     → IsTotalOrderSet ( InFCSet A ax ifc )
+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
+    cmp : Trichotomous _ _ 
+    cmp x y = {!!}
+
       
 record IsFC (A : HOD) {x : Ordinal}  (ax : A ∋ * x) (y : Ordinal) : Set n where
    field