Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 886:7c4b65fcba97
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 02 Oct 2022 19:30:19 +0900 |
| parents | d1a850b5d8e4 |
| children | 09915b6b4212 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 69 insertions(+), 30 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Sun Oct 02 16:13:32 2022 +0900 +++ b/src/zorn.agda Sun Oct 02 19:30:19 2022 +0900 @@ -900,15 +900,15 @@ ... | 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 - zc16 {z} z<px with trio< z px + sf1=sf0 : {z : Ordinal } → z o≤ px → supf1 z ≡ supf0 z + sf1=sf0 {z} z<px with trio< z px ... | tri< a ¬b ¬c = refl ... | tri≈ ¬a b ¬c = trans sfpx=px (cong supf0 (sym b)) ... | tri> ¬a ¬b c = ⊥-elim ( o≤> z<px c ) 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 (o<→≤ (ordtrans≤-< z≤w a)))) refl ( supf-mono z≤w ) + ... | tri< a ¬b ¬c = subst₂ (λ j k → j o≤ k ) (sym (sf1=sf0 (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 @@ -916,7 +916,7 @@ ... | 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 (o<→≤ lt))) (sym sfpx=px) ( supf-mono z≤w ) + ... | case2 lt = subst₂ (λ j k → j o≤ k ) (sym (sf1=sf0 (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) @@ -954,10 +954,10 @@ ... | 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 ¬c = subst (λ k → k << supf0 z1) (sym (sf1=sf0 (o<→≤ (ordtrans z0<z1 a)))) + ( ZChain.supf-< zc (subst (λ k → k o< supf0 z1) (sf1=sf0 (o<→≤ (ordtrans z0<z1 a))) sz0<sz1 )) + ... | tri≈ ¬a b ¬c = subst₂ (λ j k → j << k ) (sym (sf1=sf0 (o<→≤ (subst (λ k → z0 o< k) b z0<z1 )))) (sym sfpx=px) + ( ZChain.supf-< zc (subst₂ (λ j k → j o< k ) (sf1=sf0 (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 @@ -981,23 +981,32 @@ ch1x=pchainpx : UnionCF A f mf ay supf1 x ≡ pchainpx ch1x=pchainpx = ==→o≡ record { eq→ = zc11 ; eq← = zc12 } where fcup : {u z : Ordinal } → FClosure A f (supf1 u) z → u o≤ px → FClosure A f (supf0 u) z - fcup {u} {z} fc u≤px = subst (λ k → FClosure A f k z ) (zc16 u≤px) fc + fcup {u} {z} fc u≤px = subst (λ k → FClosure A f k z ) (sf1=sf0 u≤px) fc fcpu : {u z : Ordinal } → FClosure A f (supf0 u) z → u o≤ px → FClosure A f (supf1 u) z - fcpu {u} {z} fc u≤px = subst (λ k → FClosure A f k z ) (sym (zc16 u≤px)) fc + fcpu {u} {z} fc u≤px = subst (λ k → FClosure A f k z ) (sym (sf1=sf0 u≤px)) fc zc11 : {z : Ordinal} → odef (UnionCF A f mf ay supf1 x) z → odef pchainpx z zc11 {z} ⟪ az , ch-init fc ⟫ = case1 ⟪ az , ch-init fc ⟫ - zc11 {z} ⟪ az , ch-is-sup u u≤x is-sup fc ⟫ = zc21 fc where + zc11 {z} ⟪ az , ch-is-sup u u<x is-sup fc ⟫ = zc21 fc where zc21 : {z1 : Ordinal } → FClosure A f (supf1 u) z1 → odef pchainpx z1 zc21 {z1} (fsuc z2 fc ) with zc21 fc ... | case1 ⟪ ua1 , ch-init fc₁ ⟫ = case1 ⟪ proj2 ( mf _ ua1) , ch-init (fsuc _ fc₁) ⟫ - ... | case1 ⟪ ua1 , ch-is-sup u u≤x u1-is-sup fc₁ ⟫ = case1 ⟪ proj2 ( mf _ ua1) , ch-is-sup u u≤x u1-is-sup (fsuc _ fc₁) ⟫ - ... | case2 fc = case2 ? + ... | case1 ⟪ ua1 , ch-is-sup u u<x u1-is-sup fc₁ ⟫ = case1 ⟪ proj2 ( mf _ ua1) , ch-is-sup u u<x u1-is-sup (fsuc _ fc₁) ⟫ + ... | case2 fc = case2 (fsuc _ fc) zc21 (init asp refl ) with trio< u px | inspect supf1 u - ... | tri< a ¬b ¬c | _ = case1 ⟪ asp , ch-is-sup u a record {fcy<sup = zc13 ; order = ? ; supu=u = trans (sym (zc16 (o<→≤ a))) (ChainP.supu=u is-sup) } ? ⟫ where - zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf0 u) ∨ ( z << supf0 u ) - zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (zc16 (o<→≤ a)) ( ChainP.fcy<sup is-sup fc ) - ... | tri≈ ¬a b ¬c | _ = case2 ? - ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u≤x ⟫ ) + ... | tri< a ¬b ¬c | _ = case1 ⟪ asp , ch-is-sup u a record {fcy<sup = zc13 ; order = zc17 + ; supu=u = trans (sym (sf1=sf0 (o<→≤ a))) (ChainP.supu=u is-sup) } (init asp refl) ⟫ where + zc17 : {s : Ordinal} {z1 : Ordinal} → supf0 s o< supf0 u → + FClosure A f (supf0 s) z1 → (z1 ≡ supf0 u) ∨ (z1 << supf0 u) + zc17 {s} {z1} ss<spx fc = subst (λ k → (z1 ≡ k) ∨ (z1 << k)) ((sf1=sf0 zc19)) ( ChainP.order is-sup + (subst₂ (λ j k → j o< k ) (sym (sf1=sf0 zc18)) (sym (sf1=sf0 zc19)) ss<spx) (fcpu fc zc18) ) where + zc19 : u o≤ px + zc19 = subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u<x + zc18 : s o≤ px + zc18 = ordtrans (ZChain.supf-inject zc ss<spx) zc19 + zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf0 u) ∨ ( z << supf0 u ) + zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sf1=sf0 (o<→≤ a)) ( ChainP.fcy<sup is-sup fc ) + ... | tri≈ ¬a b ¬c | _ = case2 (init apx refl ) + ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u<x ⟫ ) zc12 : {z : Ordinal} → odef pchainpx z → odef (UnionCF A f mf ay supf1 x) z zc12 {z} (case1 ⟪ az , ch-init fc ⟫ ) = ⟪ az , ch-init fc ⟫ zc12 {z} (case1 ⟪ az , ch-is-sup u u<x is-sup fc ⟫ ) = zc21 fc where @@ -1008,21 +1017,51 @@ zc21 (init asp refl ) with trio< u px | inspect supf1 u ... | tri< a ¬b ¬c | _ = ⟪ asp , ch-is-sup u (subst (λ k → u o< k) (Oprev.oprev=x op) (ordtrans u<x <-osuc )) - record {fcy<sup = zc13 ; order = ? ; supu=u = trans ? (ChainP.supu=u is-sup) } ? ⟫ where + record {fcy<sup = zc13 ; order = zc17 ; supu=u = trans ((sf1=sf0 (o<→≤ u<x))) (ChainP.supu=u is-sup) } zc14 ⟫ where + zc17 : {s : Ordinal} {z1 : Ordinal} → supf1 s o< supf1 u → + FClosure A f (supf1 s) z1 → (z1 ≡ supf1 u) ∨ (z1 << supf1 u) + zc17 {s} {z1} ss<spx fc = subst (λ k → (z1 ≡ k) ∨ (z1 << k)) (sym (sf1=sf0 (o<→≤ u<x))) ( ChainP.order is-sup + (subst₂ (λ j k → j o< k ) (sf1=sf0 s≤px) (sf1=sf0 (o<→≤ u<x)) ss<spx) (fcup fc s≤px) ) where + s≤px : s o≤ px + s≤px = ordtrans ( supf-inject0 supf-mono1 ss<spx ) (o<→≤ u<x) + zc14 : FClosure A f (supf1 u) (supf0 u) + zc14 = init (subst (λ k → odef A k ) (sym (sf1=sf0 (o<→≤ u<x))) asp) (sf1=sf0 (o<→≤ u<x)) zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 u) ∨ ( z << supf1 u ) - zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (zc16 (o<→≤ u<x))) ( ChainP.fcy<sup is-sup fc ) - ... | tri≈ ¬a b ¬c | _ = ? - ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) ? ⟫ ) - + zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (sf1=sf0 (o<→≤ u<x))) ( ChainP.fcy<sup is-sup fc ) + ... | tri≈ ¬a b ¬c | _ = ⟪ asp , ch-is-sup px (pxo<x op) record { fcy<sup = zc13 + ; order = zc17 ; supu=u = zc18 } (init asupf1 (trans (sf1=sf0 o≤-refl ) (cong supf0 (sym b))) ) ⟫ where + zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 px) ∨ ( z << supf1 px ) + zc13 {z} fc = subst (λ k → (z ≡ k) ∨ (z << k)) (trans (cong supf0 b) (sym (sf1=sf0 o≤-refl))) (ChainP.fcy<sup is-sup fc ) + zc18 : supf1 px ≡ px + zc18 = begin + supf1 px ≡⟨ sf1=sf0 o≤-refl ⟩ + supf0 px ≡⟨ cong supf0 (sym b) ⟩ + supf0 u ≡⟨ ChainP.supu=u is-sup ⟩ + u ≡⟨ b ⟩ + px ∎ where open ≡-Reasoning + zc17 : {s : Ordinal} {z1 : Ordinal} → supf1 s o< supf1 px → + FClosure A f (supf1 s) z1 → (z1 ≡ supf1 px) ∨ (z1 << supf1 px) + zc17 {s} {z1} ss<spx fc = subst (λ k → (z1 ≡ k) ∨ (z1 << k)) (trans (cong supf0 b) (sym (sf1=sf0 o≤-refl))) + ( ChainP.order is-sup (subst₂ (λ j k → j o< k) (sf1=sf0 s≤px) ? ss<spx) (fcup fc s≤px) ) where + s≤px : s o≤ px + s≤px = ? + ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ c , (ordtrans u<x <-osuc ) ⟫ ) zc12 {z} (case2 fc) = zc21 fc where zc21 : {z1 : Ordinal } → FClosure A f px z1 → odef (UnionCF A f mf ay supf1 x) z1 zc21 {z1} (fsuc z2 fc ) with zc21 fc ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-init (fsuc _ fc₁) ⟫ ... | ⟪ ua1 , ch-is-sup u u≤x u1-is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-is-sup u u≤x u1-is-sup (fsuc _ fc₁) ⟫ zc21 (init asp refl ) = ⟪ asp , ch-is-sup px (pxo<x op) - record {fcy<sup = zc13 ; order = ? ; supu=u = trans (zc16 o≤-refl ) (sym sfpx=px) } (init ? ? ) ⟫ where + record {fcy<sup = zc13 ; order = zc17 ; supu=u = zc15 } zc14 ⟫ where + zc15 : supf1 px ≡ px + zc15 = trans (sf1=sf0 o≤-refl ) (sym sfpx=px) + zc14 : FClosure A f (supf1 px) px + zc14 = init (subst (λ k → odef A k) (sym zc15) asp) zc15 zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 px ) ∨ ( z << supf1 px ) - zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (zc16 o≤-refl)) ( ZChain.fcy<sup zc o≤-refl fc ) + zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (sf1=sf0 o≤-refl)) ( ZChain.fcy<sup zc o≤-refl fc ) + zc17 : {s : Ordinal} {z1 : Ordinal} → supf1 s o< supf1 px → + FClosure A f (supf1 s) z1 → (z1 ≡ supf1 px) ∨ (z1 << supf1 px) + zc17 {s} {z1} ss<spx fc = ? record STMP {z : Ordinal} (z≤x : z o≤ x ) : Set (Level.suc n) where field @@ -1032,10 +1071,10 @@ 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 + ; x<sup = ? ; minsup = ? } ; tsup=sup = trans (sf1=sf0 (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 + ; x<sup = ? ; minsup = ? } ; tsup=sup = trans (sf1=sf0 (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 = ? } @@ -1072,8 +1111,8 @@ ... | tri≈ ¬a b ¬c = supf0 px ... | tri> ¬a ¬b c = supf0 px - zc16 : {z : Ordinal } → z o< px → supf1 z ≡ supf0 z - zc16 {z} z<px with trio< z px + sf1=sf0 : {z : Ordinal } → z o< px → supf1 z ≡ supf0 z + sf1=sf0 {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 ) @@ -1083,7 +1122,7 @@ 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 (sf1=sf0 (ordtrans≤-< z≤w a))) refl ( supf-mono z≤w ) ... | tri≈ ¬a refl ¬c with trio< z px ... | tri< a ¬b ¬c = zc17 ... | tri≈ ¬a refl ¬c = o≤-refl