Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 883:b7fb839cdcd0
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 01 Oct 2022 19:34:04 +0900 |
| parents | 1a84433ebc1b |
| children | 36a50c66a00d |
| files | src/zorn.agda |
| diffstat | 1 files changed, 91 insertions(+), 56 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Fri Sep 30 17:48:11 2022 +0900 +++ b/src/zorn.agda Sat Oct 01 19:34:04 2022 +0900 @@ -829,16 +829,15 @@ ... | case1 eq = case2 eq ... | case2 b<x = ⊥-elim ( ¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ ) - -- if previous chain satisfies maximality, we caan reuse it - -- - -- UninCF supf0 px previous chain u o< px, supf0 px is not included - -- UninCF supf0 x supf0 px is included - -- supf0 px ≡ px - -- supf0 px ≡ supf0 x - zc4 : ZChain A f mf ay x zc4 with osuc-≡< (ZChain.x≤supfx zc ) - ... | case1 sfpx=px = ? where + ... | case1 sfpx=px = record { supf = supf1 ; sup=u = ? ; asupf = asupf1 ; supf-mono = supf-mono1 ; supf-< = supf-<1 + ; x≤supfx = ? ; minsup = ? ; supf-is-sup = ? ; csupf = ? } where + + -- we are going to determine (supf x), which is not specified in previous zc + -- case1 : supf px ≡ px + -- supf px is MinSUP of previous chain , supf x ≡ MinSUP of Union of UChain and FClosure px + pchainpx : HOD pchainpx = record { od = record { def = λ z → (odef A z ∧ UChain A f mf ay supf0 px z ) ∨ FClosure A f px z } ; odmax = & A ; <odmax = zc00 } where zc00 : {z : Ordinal } → (odef A z ∧ UChain A f mf ay supf0 px z ) ∨ FClosure A f px z → z o< & A @@ -890,20 +889,44 @@ supf1 z with trio< z px ... | tri< a ¬b ¬c = supf0 z ... | tri≈ ¬a b ¬c = px --- supf px ≡ px - ... | tri> ¬a ¬b c = sp1 + ... | tri> ¬a ¬b c = sp1 --- this may equal or larger then x, and sp1 ≡ supf x, is not included in UniofCF - pchainp : HOD - pchainp = UnionCF A f mf ay supf1 x + asupf1 : {z : Ordinal } → odef A (supf1 z ) + asupf1 {z} with trio< z px + ... | tri< a ¬b ¬c = ZChain.asupf zc + ... | tri≈ ¬a b ¬c = subst (λ k → odef A k ) (trans (cong supf0 b) (sym sfpx=px)) ( ZChain.asupf zc ) + ... | tri> ¬a ¬b c = MinSUP.asm sup1 - zc16 : {z : Ordinal } → z o< px → supf1 z ≡ supf0 z + -- ch1x=pchainpx : UnionCF A f mf ay supf1 x ≡ pchainpx + -- ch1x=pchainpx = ? + + -- UnionCF A f mf ay supf0 x ⊆ UnionCF A f mf ay supf1 x + + zc16 : {z : Ordinal } → z o≤ px → supf1 z ≡ supf0 z zc16 {z} z<px with trio< z px ... | tri< a ¬b ¬c = refl - ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬a z<px ) - ... | tri> ¬a ¬b c = ⊥-elim ( ¬a z<px ) + ... | tri≈ ¬a b ¬c = trans sfpx=px (cong supf0 (sym b)) + ... | tri> ¬a ¬b c = ⊥-elim ( o≤> z<px c ) + + record STMP {z : Ordinal} (z≤x : z o≤ x ) : Set (Level.suc n) where + field + tsup : MinSUP A (UnionCF A f mf ay supf1 z) + tsup=sup : supf1 z ≡ MinSUP.sup tsup + + sup : {z : Ordinal} → (z≤x : z o≤ x ) → STMP z≤x + sup {z} z≤x with trio< z px + ... | tri< a ¬b ¬c = record { tsup = record { sup = MinSUP.sup m ; asm = MinSUP.asm m + ; x<sup = ? ; minsup = ? } ; tsup=sup = trans (zc16 (o<→≤ a)) (ZChain.supf-is-minsup zc (o<→≤ a)) } where + m = ZChain.minsup zc (o<→≤ a) + ... | tri≈ ¬a b ¬c = record { tsup = record { sup = MinSUP.sup m ; asm = MinSUP.asm m + ; x<sup = ? ; minsup = ? } ; tsup=sup = trans (zc16 (o≤-refl0 b)) (ZChain.supf-is-minsup zc (o≤-refl0 b)) } where + m = ZChain.minsup zc (o≤-refl0 b) + ... | tri> ¬a ¬b px<z = record { tsup = record { sup = sp1 ; asm = MinSUP.asm sup1 + ; x<sup = ? ; minsup = ? } ; tsup=sup = ? } where supf-mono1 : {z w : Ordinal } → z o≤ w → supf1 z o≤ supf1 w supf-mono1 {z} {w} z≤w with trio< w px - ... | tri< a ¬b ¬c = subst₂ (λ j k → j o≤ k ) (sym (zc16 (ordtrans≤-< z≤w a))) refl ( supf-mono z≤w ) + ... | tri< a ¬b ¬c = subst₂ (λ j k → j o≤ k ) (sym (zc16 (o<→≤ (ordtrans≤-< z≤w a)))) refl ( supf-mono z≤w ) ... | tri≈ ¬a refl ¬c with osuc-≡< z≤w ... | case1 refl = o≤-refl0 zc17 where zc17 : supf1 px ≡ px @@ -911,60 +934,68 @@ ... | tri< a ¬b ¬c = ⊥-elim ( ¬b refl ) ... | tri≈ ¬a b ¬c = refl ... | tri> ¬a ¬b c = ⊥-elim ( ¬b refl ) - ... | case2 lt = subst₂ (λ j k → j o≤ k ) (sym (zc16 lt)) (sym sfpx=px) ( supf-mono z≤w ) + ... | case2 lt = subst₂ (λ j k → j o≤ k ) (sym (zc16 (o<→≤ lt))) (sym sfpx=px) ( supf-mono z≤w ) supf-mono1 {z} {w} z≤w | tri> ¬a ¬b c with trio< z px ... | tri< a ¬b ¬c = zc19 where zc21 : MinSUP A (UnionCF A f mf ay supf0 z) zc21 = ZChain.minsup zc (o<→≤ a) - zc23 : odef A sp1 - zc23 = MinSUP.asm sup1 zc24 : {x₁ : Ordinal} → odef (UnionCF A f mf ay supf0 z) x₁ → (x₁ ≡ sp1) ∨ (x₁ << sp1) - zc24 {x₁} ux = MinSUP.x<sup sup1 ? + zc24 {x₁} ux = MinSUP.x<sup sup1 (case1 (chain-mono f mf ay supf0 (o<→≤ a) ux)) zc19 : supf0 z o≤ sp1 - zc19 = subst (λ k → k o≤ sp1) (sym (ZChain.supf-is-minsup zc (o<→≤ a))) ( MinSUP.minsup zc21 zc23 zc24 ) + zc19 = subst (λ k → k o≤ sp1) (sym (ZChain.supf-is-minsup zc (o<→≤ a))) ( MinSUP.minsup zc21 (MinSUP.asm sup1) zc24 ) ... | tri≈ ¬a b ¬c = zc18 where zc21 : MinSUP A (UnionCF A f mf ay supf0 z) zc21 = ZChain.minsup zc (o≤-refl0 b) + zc20 : MinSUP.sup zc21 ≡ px + zc20 = begin + MinSUP.sup zc21 ≡⟨ sym (ZChain.supf-is-minsup zc (o≤-refl0 b)) ⟩ + supf0 z ≡⟨ cong supf0 b ⟩ + supf0 px ≡⟨ sym sfpx=px ⟩ + px ∎ where open ≡-Reasoning + zc24 : {x₁ : Ordinal} → odef (UnionCF A f mf ay supf0 z) x₁ → (x₁ ≡ sp1) ∨ (x₁ << sp1) + zc24 {x₁} ux = MinSUP.x<sup sup1 (case1 (chain-mono f mf ay supf0 (o≤-refl0 b) ux)) zc18 : px o≤ sp1 -- supf0 z ≡ px - zc18 = ? + zc18 = subst (λ k → k o≤ sp1) zc20 ( MinSUP.minsup zc21 (MinSUP.asm sup1) zc24 ) ... | tri> ¬a ¬b c = o≤-refl - zc10 : {z : Ordinal} → OD.def (od pchain) z → OD.def (od pchainp) z - zc10 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ - zc10 {z} ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ = ⟪ az , ch-is-sup u1 (ordtrans u1<x (pxo<x op)) zc15 zc14 ⟫ where - zc14 : FClosure A f (supf1 u1) z - zc14 = subst (λ k → FClosure A f k z) (sym (zc16 u1<x)) fc - zc15 : ChainP A f mf ay supf1 u1 - zc15 = record { fcy<sup = λ {z} fcy → subst (λ k → (z ≡ k) ∨ ( z << k ) ) (sym (zc16 u1<x)) (ChainP.fcy<sup u1-is-sup fcy) - ; order = λ {s} {z1} lt fc1 → subst (λ k → (z1 ≡ k) ∨ ( z1 << k ) ) (sym (zc16 u1<x)) ( - ChainP.order u1-is-sup (subst₂ (λ j k → j o< k) (zc17 u1<x lt) (zc16 u1<x) lt) (subst (λ k → FClosure A f k z1) (zc17 u1<x lt) fc1) ) - ; supu=u = trans (zc16 u1<x) (ChainP.supu=u u1-is-sup) } where - zc17 : {s u : Ordinal } → u o< px → supf1 s o< supf1 u → supf1 s ≡ supf0 s - zc17 u1<x lt = zc16 (ordtrans ( supf-inject0 supf-mono1 lt) u1<x) - - zc11 : {z : Ordinal} → z o< px → OD.def (od pchainp) z → OD.def (od pchain) z - zc11 {z} z<px ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ - zc11 {z} z<px ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ = ⟪ az , ch-is-sup u1 (ordtrans u1<x ?) ? ? ⟫ + supf-<1 : {z0 z1 : Ordinal} → supf1 z0 o< supf1 z1 → supf1 z0 << supf1 z1 + supf-<1 {z0} {z1} sz0<sz1 = zc21 where + z0<z1 : z0 o< z1 + z0<z1 = supf-inject0 supf-mono1 sz0<sz1 + zc26 : supf0 px <= sp1 + zc26 with MinSUP.x<sup sup1 (case2 (init (subst (λ k → odef A k) (sym sfpx=px) (ZChain.asupf zc) ) refl )) + ... | case1 eq = case1 (trans (sym sfpx=px) eq ) + ... | case2 lt = case2 (subst (λ k → k << sp1 ) sfpx=px lt) + zc22 : ¬ px ≡ sp1 → supf0 px << sp1 + zc22 not with MinSUP.x<sup sup1 (case2 (init (subst (λ k → odef A k) (sym sfpx=px) (ZChain.asupf zc) ) refl )) + ... | case1 eq = ⊥-elim ( not eq ) -- px ≡ sp1 + ... | case2 lt = subst (λ k → k << sp1 ) sfpx=px lt + zc21 : supf1 z0 << supf1 z1 + zc21 with trio< z1 px + ... | tri< a ¬b ¬c = subst (λ k → k << supf0 z1) (sym (zc16 (o<→≤ (ordtrans z0<z1 a)))) + ( ZChain.supf-< zc (subst (λ k → k o< supf0 z1) (zc16 (o<→≤ (ordtrans z0<z1 a))) sz0<sz1 )) + ... | tri≈ ¬a b ¬c = subst₂ (λ j k → j << k ) (sym (zc16 (o<→≤ (subst (λ k → z0 o< k) b z0<z1 )))) (sym sfpx=px) + ( ZChain.supf-< zc (subst₂ (λ j k → j o< k ) (zc16 (o<→≤ (subst (λ k → z0 o< k) b z0<z1 ))) sfpx=px sz0<sz1 )) + ... | tri> ¬a ¬b px<z1 with trio< z0 px --- supf1 z1 ≡ sp1 + ... | tri< a ¬b ¬c = zc23 where + zc23 : supf0 z0 << sp1 + zc23 with osuc-≡< ( ZChain.supf-mono zc (o<→≤ a) ) + ... | case1 eq = subst (λ k → k << sp1 ) (sym eq) (zc22 zc24) where + zc25 : px ≡ sp1 → supf0 z0 ≡ sp1 + zc25 px=sp1 = begin supf0 z0 ≡⟨ eq ⟩ + supf0 px ≡⟨ sym ( sfpx=px ) ⟩ + px ≡⟨ px=sp1 ⟩ + sp1 ∎ where open ≡-Reasoning + zc24 : ¬ px ≡ sp1 + zc24 eq1 = ⊥-elim (o<¬≡ (zc25 eq1) sz0<sz1 ) + ... | case2 lt with zc26 + ... | case1 eq = subst (λ k → supf0 z0 << k ) eq (ZChain.supf-< zc lt) + ... | case2 lt1 = ptrans (ZChain.supf-< zc lt) lt1 + ... | tri≈ ¬a b ¬c = subst (λ k → k << sp1 ) (sym sfpx=px) (zc22 zc23 ) where + zc23 : ¬ px ≡ sp1 + zc23 eq = ⊥-elim (o<¬≡ eq sz0<sz1 ) + ... | tri> ¬a ¬b c = ⊥-elim ( o<¬≡ refl sz0<sz1 ) - zc12 : {z : Ordinal} → OD.def (od pchainp) z → OD.def (od pchainpx) z - zc12 {z} ⟪ az , ch-init fc ⟫ = case1 ⟪ az , ch-init fc ⟫ - zc12 {z} ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ = ? - - zc13 : {z : Ordinal} → OD.def (od pchainpx) z → OD.def (od pchainp) z - zc13 {z} (case1 ⟪ az , ch-init fc ⟫ ) = ⟪ az , ch-init fc ⟫ - zc13 {z} (case1 ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ ) = ⟪ az , ch-is-sup u1 (ordtrans u1<x (pxo<x op)) ? ? ⟫ - zc13 {z} (case2 fc) = ⟪ ? , ch-is-sup ? ? ? ? ⟫ - - record STMP {z : Ordinal} (z≤x : z o≤ x ) : Set (Level.suc n) where - field - tsup : SUP A (UnionCF A f mf ay supf1 z) - tsup=sup : supf1 z ≡ & (SUP.sup tsup ) - - sup : {z : Ordinal} → (z≤x : z o≤ x ) → STMP z≤x - sup {z} z≤x with trio< z px - ... | tri< a ¬b ¬c = record { tsup = ? ; tsup=sup = ? } - ... | tri≈ ¬a b ¬c = record { tsup = ? ; tsup=sup = ? } - ... | tri> ¬a ¬b px<z = record { tsup = ? ; tsup=sup = ? } csupf1 : {b : Ordinal } → supf1 b o< x → odef (UnionCF A f mf ay supf1 x) (supf1 b) csupf1 {b} sb<z = ⟪ asb , ch-is-sup (supf1 b) sb<z @@ -985,6 +1016,10 @@ ... | case2 lt = ? ... | case2 px<spfx = ? where + + -- case2 : px o< supf px + -- supf px is not MinSUP of previous chain , supf x ≡ supf px + -- record { supf = supf0 ; asupf = ZChain.asupf zc ; sup = λ lt → STMP.tsup (sup lt ) ; supf-mono = supf-mono -- ; supf-< = ? ; sup=u = sup=u ; supf-is-sup = λ lt → STMP.tsup=sup (sup lt) } where supf1 : Ordinal → Ordinal