Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff src/zorn.agda @ 836:d72bcf8552bb
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 23 Aug 2022 15:47:50 +0900 |
| parents | 106492766e36 |
| children | 8ceaf3455601 |
line wrap: on
line diff
--- a/src/zorn.agda Tue Aug 23 15:16:06 2022 +0900 +++ b/src/zorn.agda Tue Aug 23 15:47:50 2022 +0900 @@ -225,8 +225,9 @@ -- tree structure -- -record HasPrev (A B : HOD) {x : Ordinal } (xa : odef A x) ( f : Ordinal → Ordinal ) : Set n where +record HasPrev (A B : HOD) (x : Ordinal ) ( f : Ordinal → Ordinal ) : Set n where field + ax : odef A x y : Ordinal ay : odef B y x=fy : x ≡ f y @@ -346,7 +347,7 @@ {y : Ordinal} (ay : odef A y) (zc : ZChain A f mf ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where field 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 + → HasPrev A (UnionCF A f mf ay (ZChain.supf zc) z) b 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 record Maximal ( A : HOD ) : Set (Level.suc n) where @@ -512,7 +513,7 @@ chain-mono1 {a} {b} {c} a≤b = chain-mono f mf ay (ZChain.supf zc) a≤b is-max-hp : (x : Ordinal) {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 → + HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) b f → * a < * b → odef (UnionCF A f mf ay (ZChain.supf zc) x) b is-max-hp x {a} {b} ua b<x ab has-prev a<b with HasPrev.ay has-prev ... | ⟪ ab0 , ch-init fc ⟫ = ⟪ ab , ch-init ( subst (λ k → FClosure A f y k) (sym (HasPrev.x=fy has-prev)) (fsuc _ fc )) ⟫ @@ -527,7 +528,7 @@ zc-b<x {b} lt = subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) lt 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 → + HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) b 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 @@ -548,7 +549,7 @@ ... | no lim = record { is-max = is-max } where 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 → + HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) b 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 with IsSup.x<sup is-sup (init-uchain A f mf ay ) @@ -579,7 +580,7 @@ chain = ZChain.chain zc sp1 = sp0 f mf zc total z10 : {a b : Ordinal } → (ca : odef chain a ) → b o< & A → (ab : odef A b ) - → HasPrev A chain ab f ∨ IsSup A chain {b} ab -- (supO chain (ZChain.chain⊆A zc) (ZChain.f-total zc) ≡ b ) + → HasPrev A chain b f ∨ IsSup A chain {b} ab -- (supO chain (ZChain.chain⊆A zc) (ZChain.f-total zc) ≡ b ) → * a < * b → odef chain b z10 = ZChain1.is-max (SZ1 f mf as0 zc (& A) ) z11 : & (SUP.sup sp1) o< & A @@ -707,13 +708,12 @@ pchain1 : HOD pchain1 = UnionCF A f mf ay supf1 x - -- if previous chain satisfies maximality, we caan reuse it -- -- supf0 px is sup of UnionCF px , supf0 x is sup of UnionCF x - no-extension : (¬ xSUP (UnionCF A f mf ay supf0 px) x ) ∨ HasPrev A pchain ? f → ZChain A f mf ay x - no-extension ¬sp=x = record { supf = supf0 ; sup = ? ; supf-mono = {!!} + no-extension : (¬ xSUP (UnionCF A f mf ay supf0 px) x ) ∨ HasPrev A pchain x f → ZChain A f mf ay x + no-extension ¬sp=x = record { supf = supf1 ; sup = ? ; supf-mono = {!!} ; initial = ? ; chain∋init = ? ; sup=u = ? ; supf-is-sup = ? ; csupf = {!!} ; chain⊆A = λ lt → proj1 lt ; f-next = ? ; f-total = ? } where pchain0=1 : ? @@ -752,7 +752,7 @@ zc4 : ZChain A f mf ay x zc4 with ODC.∋-p O A (* x) ... | no noax = no-extension {!!} -- ¬ A ∋ p, just skip - ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc ) ax f ) + ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc ) x f ) -- we have to check adding x preserve is-max ZChain A y f mf x ... | case1 pr = no-extension {!!} -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc ) ax ) @@ -790,18 +790,14 @@ ysp = & (SUP.sup (ysup f mf ay)) initial-segment : {a b z : Ordinal } → (a<x : a o< x) ( b<x : b o< x) → a o< b → z o≤ a - → ZChain.supf (pzc (osuc a) (ob<x lim a<x )) z ≡ ZChain.(umax z)) (ob<x lim b<x )) z + → ZChain.supf (pzc (osuc a) (ob<x lim a<x )) z ≡ ZChain.supf (pzc (osuc b) (ob<x lim b<x )) z initial-segment = ? - initial-segment1 : {a b z : Ordinal } → (a<x : a o< x) ( b<x : b o< x) → a o< b → - → ZChain.supf (pzc (osuc a) (ob<x lim a<x )) x ≡ ZChain.(umax z)) (ob<x lim b<x )) x - initial-segment1 = ? - supf0 : Ordinal → Ordinal supf0 z with trio< z x ... | tri< a ¬b ¬c = ZChain.supf (pzc (osuc z) (ob<x lim a)) z - ... | tri≈ ¬a b ¬c = {!!} - ... | tri> ¬a ¬b c = {!!} + ... | tri≈ ¬a b ¬c = ysp + ... | tri> ¬a ¬b c = ysp pchain0 : HOD pchain0 = UnionCF A f mf ay supf0 x @@ -818,8 +814,8 @@ supf1 : Ordinal → Ordinal supf1 z with trio< z x ... | tri< a ¬b ¬c = ZChain.supf (pzc (osuc z) (ob<x lim a)) z - ... | tri≈ ¬a b ¬c = {!!} - ... | tri> ¬a ¬b c = {!!} + ... | tri≈ ¬a b ¬c = spu + ... | tri> ¬a ¬b c = spu pchain : HOD pchain = UnionCF A f mf ay supf1 x @@ -844,7 +840,7 @@ is-max-hp : (supf : Ordinal → Ordinal) (x : Ordinal) {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay supf x) a → b o< x → (ab : odef A b) → - HasPrev A (UnionCF A f mf ay supf x) ab f → + HasPrev A (UnionCF A f mf ay supf x) b f → * a < * b → odef (UnionCF A f mf ay supf x) b is-max-hp supf x {a} {b} ua b<x ab has-prev a<b with HasPrev.ay has-prev ... | ⟪ ab0 , ch-init fc ⟫ = ⟪ ab , ch-init ( subst (λ k → FClosure A f y k) (sym (HasPrev.x=fy has-prev)) (fsuc _ fc )) ⟫ @@ -852,7 +848,7 @@ subst (λ k → UChain A f mf ay supf x k ) (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u u≤x is-sup (fsuc _ fc)) ⟫ - no-extension : ¬ ( xSUP (UnionCF A f mf ay supf1 x) x ) ∨ HasPrev A pchain ? f → ZChain A f mf ay x + no-extension : ¬ ( xSUP (UnionCF A f mf ay supf0 x) x ) ∨ HasPrev A pchain x f → ZChain A f mf ay x no-extension ¬sp=x = record { initial = pinit ; chain∋init = pcy ; supf = supf1 ; sup=u = sup=u ; sup = sup ; supf-is-sup = sis ; supf-mono = {!!} ; csupf = {!!} ; chain⊆A = pchain⊆A ; f-next = pnext ; f-total = ptotal } where @@ -901,7 +897,7 @@ zc5 : ZChain A f mf ay x zc5 with ODC.∋-p O A (* x) ... | no noax = no-extension {!!} -- ¬ A ∋ p, just skip - ... | yes ax with ODC.p∨¬p O ( HasPrev A pchain ax f ) + ... | yes ax with ODC.p∨¬p O ( HasPrev A pchain x f ) -- we have to check adding x preserve is-max ZChain A y f mf x ... | case1 pr = no-extension {!!} ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A pchain ax )