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

changeset 874:852bdf4a2df3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 17 Sep 2022 10:11:54 +0900
parents 27bab3f65064
children 7f03e1d24961
files src/zorn.agda
diffstat 1 files changed, 63 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Fri Sep 16 23:06:10 2022 +0900
+++ b/src/zorn.agda	Sat Sep 17 10:11:54 2022 +0900
@@ -373,8 +373,9 @@
            → IsSup A (UnionCF A f mf ay supf b) ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf b) b f) → supf b ≡ b 
       supf-is-sup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ & (SUP.sup (sup x≤z) )
       supf-mono : {x y : Ordinal } → x o≤  y → supf x o≤ supf y
+      supf-max : {x : Ordinal } → supf x o≤ supf z
       supf-< : {x y : Ordinal } → supf x o< supf  y → supf x << supf y
-      csupf : {b : Ordinal } → supf b o≤ z → odef (UnionCF A f mf ay supf z) (supf b) 
+      csupf : {b : Ordinal } → supf b o< z → odef (UnionCF A f mf ay supf z) (supf b) 
    chain∋init : odef chain y
    chain∋init = ⟪ ay , ch-init (init ay refl)    ⟫
    f-next : {a : Ordinal} → odef chain a → odef chain (f a)
@@ -421,6 +422,9 @@
    ... | case1 eq = case1 (subst (λ k → k ≡ supf u ) &iso  (trans (cong (&) eq) (sym (supf-is-sup u≤z ) ) ))
    ... | case2 lt = case2 (subst (λ k → * w < k ) (subst (λ k → k ≡ _ ) *iso (cong (*) (sym (supf-is-sup u≤z ))) ) lt )
 
+   csupf1 : {b : Ordinal } → supf b o< z → odef (UnionCF A f mf ay supf z) (supf b) 
+   csupf1 {b} sb<z = ⟪ ? , ch-is-sup (supf b) ? record { fcy<sup = fcy<sup ? ; order = ? ; supu=u = ? }  (init ? ? ) ⟫
+
    -- ordering is not proved here but in ZChain1 
 
 record ZChain1 ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) 
@@ -540,7 +544,7 @@
                 s≤<z : s o≤ & A
                 s≤<z = ordtrans s<b b≤z
                 zc04 : odef (UnionCF A f mf ay supf (& A))  (supf s)
-                zc04 = ZChain.csupf zc (o<→≤ (z09 (ZChain.asupf zc)))
+                zc04 = ZChain.csupf zc (z09 (ZChain.asupf zc))
                 zc05 : odef (UnionCF A f mf ay supf b)  (supf s)
                 zc05 with zc04
                 ... | ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc  ⟫ 
@@ -816,9 +820,44 @@
                  pchainp : HOD
                  pchainp = 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 )
+
+                 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 refl ¬c with osuc-≡< z≤w 
+                 ... | case1 refl = o≤-refl0 zc17 where
+                       zc17 : supf1 px ≡ px
+                       zc17 with trio< px px
+                       ... | 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 )
+                 supf-mono1 {z} {w} z≤w | tri> ¬a ¬b c with trio< z px
+                 ... | tri< a ¬b ¬c = zc19 where
+                       zc19 : supf0 z o≤ sp1
+                       zc19 = ?
+                 ... | tri≈ ¬a b ¬c = zc18 where
+                       zc18 : px o≤ sp1
+                       zc18 = ?
+                 ... | 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)) ?  ?  ⟫
+                 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 ⟫ 
@@ -853,6 +892,27 @@
                  ... | 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
+                 ... | tri< a ¬b ¬c = refl
+                 ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬a z<px )
+                 ... | tri> ¬a ¬b c = ⊥-elim ( ¬a z<px )
+
+                 zc17 : {z : Ordinal } → supf0 z o≤ supf0 px
+                 zc17 = ? -- px o< z, px o< supf0 px
+
+                 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 refl ¬c with trio< z px
+                 ... | tri< a ¬b ¬c = zc17
+                 ... | tri≈ ¬a refl ¬c = o≤-refl
+                 ... | tri> ¬a ¬b c = o≤-refl
+                 supf-mono1 {z} {w} z≤w | tri> ¬a ¬b c with trio< z px
+                 ... | tri< a ¬b ¬c = zc17
+                 ... | tri≈ ¬a b ¬c = o≤-refl
+                 ... | tri> ¬a ¬b c = o≤-refl
+
                  pchain1 : HOD
                  pchain1 = UnionCF A f mf ay supf1 x