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

changeset 656:db9477c80dce

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
data Chain
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 02 Jul 2022 07:52:05 +0900
parents b602e3f070df
children 5e056537807d 9142e834c4c6
files src/zorn.agda
diffstat 1 files changed, 39 insertions(+), 14 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Fri Jul 01 14:36:38 2022 +0900
+++ b/src/zorn.agda	Sat Jul 02 07:52:05 2022 +0900
@@ -233,6 +233,12 @@
    field
       x<sup : {y : Ordinal} → odef B y → (y ≡ x ) ∨ (y << x )
 
+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 UChain (chain : Ordinal → HOD) (x : Ordinal) (z : Ordinal) : Set n where 
    -- Union of supf z which o< x
    field
@@ -240,6 +246,24 @@
       u<x : u o< x
       chain∋z : odef (chain u) 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 )))
+
+data Chain (A : HOD ) ( f : Ordinal → Ordinal ) {y : Ordinal} (ay : odef A y) : Ordinal →  HOD  → Set (Level.suc n) where
+    ch-noax    : {x : Ordinal } { chain : HOD } ( op : Oprev Ordinal osuc x ) (noax : ¬ odef A x ) (c : Chain A f ay (Oprev.oprev op) chain) → Chain A f ay x chain
+    ch-hasprev : {x : Ordinal } { chain : HOD } ( op : Oprev Ordinal osuc x ) (ax : odef A x ) 
+        ( c : Chain A f ay (Oprev.oprev op) chain) ( h :  HasPrev A chain ax f ) → Chain A f ay x chain
+    ch-is-sup : {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 ) ( sup : IsSup A chain   ax ) → Chain A f ay x 
+            record { od = record { def = λ x → odef A x ∧ (odef chain x ∨ (FClosure A f y x)) } ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy }
+    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 ))
+         → Chain A f ay x 
+             record { od = record { def = λ z → odef A z ∧ (UChain chainf x z ∨ FClosure A f y z ) } 
+                ; odmax = & A ; <odmax = λ {y} sy → {!!}   }
+
 Chain-uniq : (A : HOD ) ( f : Ordinal → Ordinal ) → {y : Ordinal} (ay : odef A y) → (x : Ordinal)
      → ( Ordinal → HOD ) → Set (Level.suc n)
 Chain-uniq A f {y} ay x chain  with Oprev-p x
@@ -255,7 +279,7 @@
             schain : HOD
             schain = record { od = record { def = λ x → odef (chain px) x ∨ (FClosure A f y x) } ; odmax = & A ; <odmax = λ {y} sy → {!!}  }
       ... | case2 ¬x=sup = chain x ≡ chain px
-... | no ¬ox = chain x ≡ record { od = record { def = λ z → odef A z ∧ ( UChain chain z x ∨ FClosure A f y z ) ; odmax = & A ; <odmax = λ {y} sy → {!!}  } }
+... | no ¬ox = chain x ≡ record { od = record { def = λ z → odef A z ∧ ( UChain chain x z ∨ FClosure A f y z ) } ; odmax = & A ; <odmax = λ {y} sy → {!!}   }
 
 record ZChain1 ( A : HOD )    ( f : Ordinal → Ordinal ) {y : Ordinal } (ay : odef A y ) ( z : Ordinal ) : Set (Level.suc n) where
    field
@@ -282,12 +306,6 @@
       A∋maximal : A ∋ maximal
       ¬maximal<x : {x : HOD} → A ∋ x  → ¬ maximal < x       -- A is Partial, use negative
 
-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
-
 SupCond : ( A B : HOD) → (B⊆A : B ⊆ A) → IsTotalOrderSet B → Set (Level.suc n)
 SupCond A B _ _ = SUP A B  
 
@@ -296,8 +314,6 @@
     → ( ( B : HOD) → (B⊆A : B ⊆' A) → IsTotalOrderSet B → SUP A B   ) -- SUP condition
     → Maximal A 
 Zorn-lemma {A}  0<A supP = zorn00 where
-     supO : (C : HOD ) → C ⊆' A → IsTotalOrderSet C → Ordinal
-     supO C C⊆A TC = & ( SUP.sup ( supP  C  C⊆A TC ))
      <-irr0 : {a b : HOD} → A ∋ a → A ∋ b  → (a ≡ b ) ∨ (a < b ) → b < a → ⊥
      <-irr0 {a} {b} A∋a A∋b = <-irr
      z07 :   {y : Ordinal} → {P : Set n} → odef A y ∧ P → y o< & A
@@ -424,13 +440,22 @@
      ... | yes op = sc4 where
           open ZChain1
           px = Oprev.oprev op
+          px<x : px o< x
+          px<x = subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc 
           sc : ZChain1 A f ay px
-          sc = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) 
+          sc = prev px px<x
           no-ext : ZChain1 A f ay x
-          no-ext = record { chain = s01 ; chain-mono = ? ; chain-uniq = ? } where
+          no-ext = record { chain = s01 ; chain-mono = ? ; chain-uniq = s02 } where
                 s01 : Ordinal → HOD
-                s01 z = chain (prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc )) z
-
+                s01 z with trio< z x
+                ... | tri< a ¬b ¬c = chain (prev z a ) z
+                ... | tri≈ ¬a b ¬c = chain (prev px px<x ) px
+                ... | tri> ¬a ¬b c = chain (prev px px<x ) px
+                s02 : Chain-uniq A f ay x s01
+                s02 with trio< x x
+                ... | tri< a ¬b ¬c = ?
+                ... | tri≈ ¬a refl ¬c = ?
+                ... | tri> ¬a ¬b c = ?
           sc4 : ZChain1 A f ay x
           sc4 with ODC.∋-p O A (* x)
           ... | no noax = {!!}
@@ -452,7 +477,7 @@
           ... | case2 ¬x=sup = {!!}
      ... | no ¬ox = ? where
           sc5 : HOD
-          sc5 = record { od = record { def = λ z → odef A z ∧ UChain ? x z } ; odmax = & A ; <odmax = λ {y} sy → {!!}  }
+          sc5 = record { od = record { def = λ z → odef A z ∧ (UChain ? x z ∨ FClosure A f y z)} ; odmax = & A ; <odmax = λ {y} sy → {!!}  }
 
      ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (x : Ordinal) → (zc0 : ZChain1 A f ay (& A)) 
          → ((z : Ordinal) → z o< x → ZChain A f ay zc0 z) → ZChain A f ay zc0 x