Members/kono/Proof/ZF-in-agda: src/zorn.agda comparison

comparison src/zorn.agda @ 865:b095c84310df

...

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Sat, 10 Sep 2022 18:20:24 +0900
parents	06f692bf7a97
children	8a49ab1dcbd0

comparison

equal deleted inserted replaced

-:06f692bf7a97
+:b095c84310df
 ... | tri≈ ¬a refl ¬c = ⊥-elim ( o<¬≡ (cong supf refl) sx<sy )
 ... | tri> ¬a ¬b y<x with osuc-≡< (supf-mono (o<→≤ y<x) )
 ... | case1 eq = ⊥-elim ( o<¬≡ (sym eq) sx<sy )
 ... | case2 lt = ⊥-elim ( o<> sx<sy lt )
+record Zsupf ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f)
+{y : Ordinal} (ay : odef A y)  ( z : Ordinal ) : Set (Level.suc n) where
+field
+s : Ordinal
+s=z : odef A z → s ≡ z
+as : odef A s
+sup : SUP A (UnionCF A f mf ay (λ _ → s) z)
 record ZChain ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f)
 {y : Ordinal} (ay : odef A y)  ( z : Ordinal ) : Set (Level.suc n) where
 field
 supf :  Ordinal → Ordinal
 chain : HOD
 chain = UnionCF A f mf ay supf z
 chain⊆A : chain ⊆' A
 chain⊆A = λ lt → proj1 lt
 field
-supf-max : {x : Ordinal } → z o≤ x  → supf z ≡ supf x
 sup : {x : Ordinal } → x o≤ z  → SUP A (UnionCF A f mf ay supf x)
 sup=u : {b : Ordinal} → (ab : odef A b) → b o≤ z
 → 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 } → z o< x  → supf (osuc z) ≡ supf x
 csupf : {b : Ordinal } → b o≤ z → odef (UnionCF A f mf ay supf (supf b)) (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)
 supfx : {z : Ordinal } → x o≤ z →  supf0 px ≡ supf0 z
 supfx {z} x≤z with trio< z px
 ... | tri< a ¬b ¬c = ⊥-elim ( o≤> x≤z (subst (λ k → z o< k ) (Oprev.oprev=x op) (ordtrans a <-osuc )))
 ... | tri≈ ¬a b ¬c = ⊥-elim ( o≤> x≤z (subst (λ k → k o< x ) (sym b) (pxo<x op)))
-... | tri> ¬a ¬b c = ZChain.supf-max zc (o<→≤ c)
+... | tri> ¬a ¬b c = ? --  ZChain.supf-max zc (o<→≤ c)
 supf∈A : {b : Ordinal} → b o≤ x → odef A (supf0 b)
 supf∈A {b} b≤z with trio< b px
 ... | tri< a ¬b ¬c = proj1 ( ZChain.csupf zc (o<→≤ a ))
 ... | tri≈ ¬a b ¬c = proj1 ( ZChain.csupf zc (o≤-refl0 b ))
-... | tri> ¬a ¬b c = subst (λ k → odef A k ) (ZChain.supf-max zc (o<→≤ c)) (proj1 ( ZChain.csupf zc o≤-refl))
+... | tri> ¬a ¬b c = ? -- subst (λ k → odef A k ) (ZChain.supf-max zc (o<→≤ c)) ? -- (proj1 ( ZChain.csupf zc o≤-refl))
 supf-mono : {a b : Ordinal } → a o≤ b → supf0 a o≤ supf0 b
 supf-mono = ZChain.supf-mono zc
 supf-max : {z : Ordinal} → x o≤ z → supf0 x ≡ supf0 z
 supf-max {z} z≤x = trans ( sym zc02) zc01 where
 zc02 : supf0 px ≡ supf0 x
-zc02 = ZChain.supf-max zc (o<→≤ (pxo<x op))
+zc02 = ? -- ZChain.supf-max zc (o<→≤ (pxo<x op))
 zc01 : supf0 px ≡ supf0 z
-zc01 = ZChain.supf-max zc (OrdTrans (o<→≤ (pxo<x op)) z≤x)
+zc01 = ? -- ZChain.supf-max zc (OrdTrans (o<→≤ (pxo<x op)) z≤x)
 zc04 : {b : Ordinal} → b o≤ x → (b o≤ px ) ∨ (b ≡ x )
 zc04 {b} b≤x with trio< b px
 ... | tri< a ¬b ¬c = case1 (o<→≤ a)
 ... | tri≈ ¬a b ¬c = case1 (o≤-refl0 b)
 ... | tri> ¬a ¬b px<b with osuc-≡< b≤x
 --    UninCF supf0 x   supf0 px is included
 --           supf0 px ≡ px
 --           supf0 px ≡ supf0 x
 no-extension : ( (¬ xSUP (UnionCF A f mf ay supf0 px) x ) ∨  HasPrev A pchain x f) → ZChain A f mf ay x
-no-extension P = record { supf = supf0 ;  sup = λ lt → STMP.tsup (sup lt ) ; supf-mono = supf-mono ; supf-max = supf-max
+no-extension P = record { supf = supf0 ;  sup = λ lt → STMP.tsup (sup lt ) ; supf-mono = supf-mono ; supf-max = ?
 ; sup=u = sup=u ; supf-is-sup = λ lt → STMP.tsup=sup (sup lt) ; csupf = csupf }  where
 zc10 :  {z : Ordinal} → OD.def (od pchain) z → OD.def (od pchain1) 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)) u1-is-sup  fc  ⟫
 zc11 : (¬ xSUP (UnionCF A f mf ay supf0 px) x ) ∨  (HasPrev A pchain x f )
 tsup=sup : supf0 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 = ZChain.sup zc (o<→≤ a)  ; tsup=sup = ZChain.supf-is-sup zc (o<→≤ a) }
 ... | tri≈ ¬a b ¬c = record { tsup = ZChain.sup zc (o≤-refl0 b)  ; tsup=sup = ZChain.supf-is-sup zc (o≤-refl0 b) }
-... | tri> ¬a ¬b px<z = record { tsup = record { sup = SUP.sup zc32 ; as = SUP.as zc32 ; x<sup = zc34 } ; tsup=sup = zc33  } where
+... | tri> ¬a ¬b px<z = zc35 where
-zc32 = ZChain.sup zc o≤-refl
 zc30 : z ≡ x
 zc30 with osuc-≡< z≤x
 ... | case1 eq = eq
 ... | case2 z<x = ⊥-elim (¬p<x<op ⟪ px<z , subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) z<x ⟫ )
-zc34 : {w : HOD} → UnionCF A f mf ay supf0 z ∋ w → (w ≡ SUP.sup zc32) ∨ (w < SUP.sup zc32)
+zc32 = ZChain.sup zc o≤-refl
-zc34 {w} lt with zc11 P (subst (λ k → odef (UnionCF A f mf ay supf0 k) (& w)) zc30 lt)
+zc34 : ¬ (supf0 px ≡ px) → {w : HOD} → UnionCF A f mf ay supf0 z ∋ w → (w ≡ SUP.sup zc32) ∨ (w < SUP.sup zc32)
+zc34 ne {w} lt with zc11 P (subst (λ k → odef (UnionCF A f mf ay supf0 k) (& w)) zc30 lt)
 ... | case1 lt = SUP.x<sup zc32 lt
-... | case2 P = ?
+... | case2 ⟪ spx=px  , fc ⟫ = ⊥-elim ( ne spx=px )
---  FClosure A f px z
--- where
---    zc35 : odef (UnionCF A f mf ay supf0 x) (& w)
---     zc35 =
 zc33 : supf0 z ≡ & (SUP.sup zc32)
 zc33 = trans (sym (supfx (o≤-refl0 (sym zc30)))) ( ZChain.supf-is-sup zc o≤-refl  )
+zc36 : ¬ (supf0 px ≡ px) → STMP z≤x
+zc36 ne = record { tsup = record { sup = SUP.sup zc32 ; as = SUP.as zc32 ; x<sup = zc34 ne } ; tsup=sup = zc33  }
+zc35 : STMP z≤x
+zc35 with trio< (supf0 px) px
+... | tri< a ¬b ¬c = zc36 ¬b
+... | tri> ¬a ¬b c = zc36 ¬b
+... | tri≈ ¬a b ¬c = record { tsup = zc37 ; tsup=sup = ?  } where
+zc37 : SUP A (UnionCF A f mf ay supf0 z)
+zc37 = record { sup = ? ; as = ? ; x<sup = ? }
 sup=u : {b : Ordinal} (ab : odef A b) →
 b o≤ x → IsSup A (UnionCF A f mf ay supf0 b) ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf0 b) b f ) → supf0 b ≡ b
 sup=u {b} ab b≤x is-sup with trio< b px
 ... | tri< a ¬b ¬c = ZChain.sup=u zc ab (o<→≤ a) ⟪ record { x<sup = λ lt → IsSup.x<sup (proj1 is-sup) lt } , proj2 is-sup ⟫
 ... | tri≈ ¬a b ¬c = ZChain.sup=u zc ab (o≤-refl0 b) ⟪ record { x<sup = λ lt → IsSup.x<sup (proj1 is-sup) lt } , proj2 is-sup ⟫
 zc31 (case2 hasPrev ) with zc30
 ... | refl = ⊥-elim ( proj2 is-sup record { ax = HasPrev.ax hasPrev ; y = HasPrev.y hasPrev
 ; ay = zc10 (HasPrev.ay hasPrev) ; x=fy = HasPrev.x=fy hasPrev } )
 csupf :  {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay supf0 (supf0 b)) (supf0 b)
 csupf {b} b≤x with zc04 b≤x
-... | case2 b=x = subst (λ k → odef (UnionCF A f mf ay supf0 k) k) (ZChain.supf-max zc zc05 ) ( ZChain.csupf zc o≤-refl ) where
+... | case2 b=x = subst (λ k → odef (UnionCF A f mf ay supf0 k) k) ? ( ZChain.csupf zc o≤-refl ) where
 zc05 : px o≤ b
 zc05 = subst (λ k → px o≤ k) (sym b=x) (o<→≤ (pxo<x op) )
 ... | case1 b≤px = ZChain.csupf zc b≤px
 zc4 : ZChain A f mf ay x

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

comparison src/zorn.agda @ 865:b095c84310df