# HG changeset patch # User Shinji KONO # Date 1650387297 -32400 # Node ID 8facdd7cc65a9ef954f7f1b4e64d6f61c0fbbfc2 # Parent 634c4a66cfcf3de97256fa26b568f66a6fbbeb31 TransitiveClosure with x <= f x is possible diff -r 634c4a66cfcf -r 8facdd7cc65a src/zorn.agda --- a/src/zorn.agda Tue Apr 19 11:24:55 2022 +0900 +++ b/src/zorn.agda Wed Apr 20 01:54:57 2022 +0900 @@ -40,6 +40,9 @@ open HOD +_≤_ : (x y : HOD) → Set (Level.suc n) +x ≤ y = ( x ≡ y ) ∨ ( x < y ) + record Element (A : HOD) : Set (Level.suc n) where field elm : HOD @@ -213,7 +216,7 @@ c-infinite : (y : Ordinal ) → (cy : odef (IChainSet A ax) y ) → IChainSup> A (ic→A∋y A ax cy) -open import Data.Nat hiding (_<_) +open import Data.Nat hiding (_<_ ; _≤_ ) import Data.Nat.Properties as NP open import nat @@ -267,7 +270,7 @@ IPO : IsPartialOrderSet (InFCSet A ax ifc ) IPO = ⊆-IsPartialOrderSet record { incl = λ {y} lt → incl (InFCSet⊆A A {x} ax ifc) lt} PO B = IChainSet A ax - cnext = cinext A ax ifc + cnext = {!!} -- cinext A ax ifc ct02 : {oy : Ordinal} → (y : Chain B x cnext oy ) → A ∋ * oy ct02 y = incl (IChainSet⊆A {A} ax) (subst (λ k → odef (IChainSet A ax) k) (sym &iso) (ct∈A B x cnext y) ) ct-inject : {ox oy : Ordinal} → (x1 : Chain B x cnext ox ) → (y : Chain B x cnext oy ) @@ -285,7 +288,7 @@ ct07 : * ox < * (cnext oy1) ct07 with ODC.∋-p O (IChainSet A ax) (* oy1) ... | no not = ⊥-elim ( not (subst (λ k → odef (IChainSet A ax) k ) (sym &iso) ay ) ) - ... | yes ay1 = IsStrictPartialOrder.trans PO {me (ct02 x1) } {me (ct02 y)} {me ct031 } (ct-monotonic x1 y a ) ct011 where + ... | yes ay1 = {!!} where -- IsStrictPartialOrder.trans PO {me (ct02 x1) } {me (ct02 y)} {me ct031 } (ct-monotonic x1 y a ) ct011 where ct031 : A ∋ * (IChainSup>.y (InfiniteChain.c-infinite ifc oy1 (subst (λ k → odef (IChainSet A ax) k) &iso ay1 ) )) ct031 = subst (λ k → odef A k ) (sym &iso) ( IChainSup>.A∋y (InfiniteChain.c-infinite ifc oy1 (subst (λ k → odef (IChainSet A ax) k) &iso ay1 )) ) @@ -295,7 +298,7 @@ ct11 : * ox < * (cnext oy1) ct11 with ODC.∋-p O (IChainSet A ax) (* oy1) ... | no not = ⊥-elim ( not (subst (λ k → odef (IChainSet A ax) k ) (sym &iso) ay ) ) - ... | yes ay1 = subst (λ k → * k < _) (sym (ct-inject _ _ b)) ct011 where + ... | yes ay1 = subst (λ k → * k < _) (sym (ct-inject _ _ b)) {!!} where 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 ) @@ -328,9 +331,13 @@ 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 = ? + → * y ≤ * mx + → InfiniteChain A (maxα mx my) ax +extendInfiniteChain A {x} {mx} {y} {my} ax ay PO ifcx ifcy y A (ic→A∋y A ax cy) + eic01 z cy = {!!} record IsFC (A : HOD) {x : Ordinal} (ax : A ∋ * x) (y : Ordinal) : Set n where field @@ -470,61 +477,12 @@ 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) ( TransitiveClosure-is-total A {x} ax PO ifc )) - z03 : {x : Ordinal } → (ax : A ∋ * x ) → InfiniteChain A (& A) ax → ⊥ - z03 {x} ax ifc = {!!} + -- z03 : {x : Ordinal } → (ax : A ∋ * x ) → InfiniteChain A (& A) ax → ⊥ + -- z03 {x} ax ifc = {!!} -- 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 - ind x prev with Oprev-p x - ... | yes op with ODC.∋-p O A (* x) - ... | no ¬Ax = zc1 where - -- we have previous ordinal and ¬ A ∋ x, use previous Zchain - px = Oprev.oprev op - zc1 : ZChain A x ∨ Maximal A - zc1 with prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc) - ... | case2 x = case2 x -- we have the Maximal - ... | case1 z with trio< x (& (ZChain.max z)) - ... | tri< a ¬b ¬c = case1 record { max = ZChain.max z ; y ¬a ¬b c = {!!} -- can't happen - ... | yes ax = zc4 where -- we have previous ordinal and A ∋ x - px = Oprev.oprev op - zc1 : OSup> A (subst (OD.def (od A)) (sym &iso) ax) → ZChain A x ∨ Maximal A - zc1 os with prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc) - ... | case2 x = case2 x - ... | case1 x = {!!} - zc4 : ZChain A x ∨ Maximal A - zc4 with Zorn-lemma-3case 0x = zc1 {!!} - ... | case2 (case1 x) = case2 x - ... | case2 (case2 ex) = ⊥-elim (zc5 {!!} ) where - FC : HOD - FC = IChainSet A ax - B : InfiniteChain A x ax → HOD - B ifc = InFCSet A ax ifc - 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 = 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 - ifc record { c-infinite = c-infinite } = record { 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 : InfiniteChain A x (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 - ... | tri< a ¬b ¬c = {!!} where - zc1 : ZChain A (& A) - zc1 with prev (& A) a - ... | t = {!!} - ... | tri≈ ¬a b ¬c = {!!} where - ... | tri> ¬a ¬b c with ODC.∋-p O A (* x) - ... | no ¬Ax = {!!} where - ... | yes ax = {!!} + ind x prev = {!!} zorn03 : (x : Ordinal) → ZChain A x ∨ Maximal A zorn03 x = TransFinite ind x zorn04 : Maximal A