Members/kono/Proof/ZF-in-agda: src/zorn.agda comparison

comparison src/zorn.agda @ 741:adbe43c07ce7

...

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Thu, 21 Jul 2022 03:56:54 +0900
parents	11f46927e3f7
children	de9d9c70a0d7

comparison

equal deleted inserted replaced

-:11f46927e3f7
+:adbe43c07ce7
 field
 sup : HOD
 A∋maximal : A ∋ sup
 x<sup : {x : HOD} → B ∋ x → (x ≡ sup ) ∨ (x < sup )   -- B is Total, use positive
-record IsSup>b (A : HOD) (b : Ordinal) (p : Ordinal) : Set n where
-field
-x2 : Ordinal
-ax2 : odef A x2
-b<x2 : b o< x2
-is-sup>b : IsSup A (* p) ax2
 --
 --  sup and its fclosure is in a chain HOD
 --    chain HOD is sorted by sup as Ordinal and <-ordered
 --    whole chain is a union of separated Chain
 --    minimum index is y not ϕ
 record ChainP (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal) (u z : Ordinal) : Set n where
 field
 fcy<sup  : {z : Ordinal } → FClosure A f y z → z << supf u
 csupz    : FClosure A f (supf u) z
 order    : {sup1 z1 : Ordinal} → (lt : sup1 o< u ) → FClosure A f (supf sup1 ) z1 → z1 << supf u
--- u>0      : o∅ o< u    -- ¬ ch-init
--- supf=u   : supf u ≡ u
--- supf-mono  : {a b : Ordinal } → a o≤ b → supf a o≤ supf b
--- supf-<  : {a b : Ordinal } → a o≤ b → (supf a ≡ supf b) ∨ (supf a << supf b)
--- au       : odef A u
--- ¬u=fx    : {x : Ordinal} → ¬ ( u ≡ f x )
--- asup     : (x : Ordinal) → odef A (supf x)
 data Chain (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal) : Ordinal →  Ordinal → Set n where
 ch-init    : (z : Ordinal) → FClosure A f y z  → Chain A f mf  ay supf o∅ z
 ch-is-sup : {sup z : Ordinal }
 → ( is-sup : ChainP A f mf ay supf sup z)
 chain⊆A : chain ⊆' A
 chain∋init : odef chain init
 initial : {y : Ordinal } → odef chain y → * init ≤ * y
 f-next : {a : Ordinal } → odef chain a → odef chain (f a)
 f-total : IsTotalOrderSet chain
-sup=u : {b : Ordinal} → (ab : odef A b)  → IsSup A chain ab → supf b ≡ b
+sup=u : {b : Ordinal} → {ab : odef A b}  → b o< z → IsSup A chain ab → supf b ≡ b
--- chain<A : {z : Ordinal } → UnionCF A f mf ay supf z ⊆' UnionCF A f mf ay supf (& A)
+order : {sup1 b z1 : Ordinal} → b o< z → sup1 o< b → FClosure A f (supf sup1) z1 → z1 << supf b
 record ZChain1 ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f)
 {init : Ordinal} (ay : odef A init)  (zc : ZChain A f mf ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where
 field
 chain-mono2 : { a b c : Ordinal }  →
 a o≤ b → b o≤ z → odef (UnionCF A f mf ay (ZChain.supf zc) a) c → odef (UnionCF A f mf ay (ZChain.supf zc) b) c
 is-max :  {a b : Ordinal } → (ca : odef (UnionCF A f mf ay (ZChain.supf zc) z) a ) →  b o< z  → (ab : odef A b)
 → HasPrev A (UnionCF A f mf ay (ZChain.supf zc) z) ab f ∨  IsSup A (UnionCF A f mf ay (ZChain.supf zc) z) ab
 → * a < * b  → odef ((UnionCF A f mf ay (ZChain.supf zc) z)) b
+fcy<sup  : {u w : Ordinal } → u o< z  → FClosure A f init w → w << (ZChain.supf zc) u
 record Maximal ( A : HOD )  : Set (Level.suc n) where
 field
 maximal : HOD
 A∋maximal : A ∋ maximal
 is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a →
 b o< x → (ab : odef A b) →
 HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) ab f ∨ IsSup A (UnionCF A f mf ay (ZChain.supf zc) x) ab →
 * a < * b → odef (UnionCF A f mf ay (ZChain.supf zc) x) b
 is-max {a} {b} ua b<x ab (case1 has-prev) a<b = is-max-hp x {a} {b} ua b<x ab has-prev a<b
-is-max {a} {b} ua b<x ab (case2 is-sup) a<b = chain-mono2 x ? o≤-refl m04 where
+is-max {a} {b} ua b<x ab (case2 is-sup) a<b = chain-mono2 x (o<→≤ ob<x) o≤-refl m04 where
-m12 : {sup1 z1 : Ordinal} → sup1 o< b → FClosure A f (ZChain.supf zc sup1) z1 → odef (UnionCF A f mf ay (ZChain.supf zc) x) z1
+ob<x : osuc b o< x
-m12 = ?
+ob<x with trio< (osuc b) x
-m11 : {sup1 z1 : Ordinal} → sup1 o< b → FClosure A f (ZChain.supf zc sup1) z1 → z1 << ZChain.supf zc b
+... | tri< a ¬b ¬c = a
-m11 {sup1} {z1} s<b fc with IsSup.x<sup is-sup (m12 s<b fc)
+... | tri≈ ¬a ob=x ¬c = ⊥-elim ( lim record { op = b ; oprev=x = ob=x }  )
-... | t = ?
+... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ b<x , c ⟫ )
 m07 : {z : Ordinal} → FClosure A f y z → z << ZChain.supf zc b
-m07 {y} (init ay1) = ?
+m07 {z} fc = ZChain1.fcy<sup (prev (osuc b) ob<x) <-osuc fc
-m07 {.(f x)} (fsuc x fc) with proj1 (mf x (A∋fc y f mf  fc))
+m08 : {sup1 z1 : Ordinal} → sup1 o< b → FClosure A f (ZChain.supf zc sup1) z1 → z1 << ZChain.supf zc b
-... | case1 eq = subst ( λ k → k << ZChain.supf zc b) (subst₂ (λ j k → j ≡ k) &iso  &iso (cong (&) eq))  (m07 fc)
+m08 = ?
-... | case2 lt  with ODC.p∨¬p O ( f x << ZChain.supf zc b )
-... | case1 p = p
-... | case2 np = ? where
-m08 : x <<　ZChain.supf zc b
-m08 = m07 fc
-m09 : ⊥
-m09 = fcn-imm y f mf ? ? ⟪ m08 , ?  ⟫
-m10 : ? ∨ ( ? <<  b )
-m10 = IsSup.x<sup is-sup ? -- (proj2 (mf x (A∋fc y f mf  fc)))
 m05 : b ≡ ZChain.supf zc b
-m10 : {sup1 z1 : Ordinal} → sup1 o< b → FClosure A f (ZChain.supf zc sup1) z1 → z1 << ZChain.supf zc b
+m05 = sym (ZChain.sup=u zc {_} {ab} ?
-m05 = sym (ZChain.sup=u ? ab is-sup)   -- ZChain on x
+record { x<sup = λ lt → IsSup.x<sup is-sup (chain-mono2 x (o<→≤ ob<x) o≤-refl ? )} )   -- ZChain on x
 m06 : ChainP A f mf ay (ZChain.supf zc) b b
-m06 = record { fcy<sup = ? ; csupz = subst (λ k →  FClosure A f k b ) m05 (init ab) ; order = ? }
+m06 = record { fcy<sup = m07 ; csupz = subst (λ k →  FClosure A f k b ) m05 (init ab) ; order = m08 }
 m04 : odef (UnionCF A f mf ay (ZChain.supf zc) (osuc b)) b
 m04 = ⟪ ab , record { u = b ; u<x = case1 <-osuc ; uchain = ch-is-sup m06 (subst (λ k → FClosure A f k b) m05 (init ab)) } ⟫
 ---
 --- the maximum chain  has fix point of any ≤-monotonic function

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

comparison src/zorn.agda @ 741:adbe43c07ce7