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

comparison src/zorn.agda @ 779:9e34893d9a03

...

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Fri, 29 Jul 2022 02:38:37 +0900
parents	6aafa22c951a
children	10a036aeb688

comparison

equal deleted inserted replaced

-:6aafa22c951a
+:9e34893d9a03
 ≤-ftrans {x} {y} {z} (case1 refl ) (case1 refl ) = case1 refl
 ≤-ftrans {x} {y} {z} (case1 refl ) (case2 y<z) = case2 y<z
 ≤-ftrans {x} {_} {z} (case2 x<y ) (case1 refl ) = case2 x<y
 ≤-ftrans {x} {y} {z} (case2 x<y) (case2 y<z) = case2 ( IsStrictPartialOrder.trans PO x<y y<z )
+<-ftrans : {x y z : Ordinal } →  x <=  y →  y <=  z →  x <=  z
+<-ftrans {x} {y} {z} (case1 refl ) (case1 refl ) = case1 refl
+<-ftrans {x} {y} {z} (case1 refl ) (case2 y<z) = case2 y<z
+<-ftrans {x} {_} {z} (case2 x<y ) (case1 refl ) = case2 x<y
+<-ftrans {x} {y} {z} (case2 x<y) (case2 y<z) = case2 ( IsStrictPartialOrder.trans PO x<y y<z )
 <=to≤ : {x y : Ordinal } → x <= y → * x ≤ * y
 <=to≤ (case1 eq) = case1 (cong (*) eq)
 <=to≤ (case2 lt) = case2 lt
+≤to<= : {x y : Ordinal } → * x ≤ * y → x <= y
+≤to<= (case1 eq) = case1 ( subst₂ (λ j k → j ≡ k ) &iso &iso  (cong (&) eq) )
+≤to<= (case2 lt) = case2 lt
 <-irr : {a b : HOD} → (a ≡ b ) ∨ (a < b ) → b < a → ⊥
 <-irr {a} {b} (case1 a=b) b<a = IsStrictPartialOrder.irrefl PO   (sym a=b) b<a
 <-irr {a} {b} (case2 a<b) b<a = IsStrictPartialOrder.irrefl PO   refl
 (IsStrictPartialOrder.trans PO     b<a a<b)
 ay : odef B y
 x=fy :  x ≡ f y
 record IsSup (A B : HOD) {x : Ordinal } (xa : odef A x)     : Set n where
 field
-x<sup : {y : Ordinal} → odef B y → (y ≡ x ) ∨ (y << x )
+x<sup   : {y : Ordinal} → odef B y → (y ≡ x ) ∨ (y << x )
 record SUP ( A B : HOD )  : Set (Level.suc n) where
 field
 sup : HOD
 A∋maximal : A ∋ sup
 x<sup : {x : HOD} → B ∋ x → (x ≡ sup ) ∨ (x < sup )   -- B is Total, use positive
+min-sup : {z : HOD } → B ∋ z → ( {x : HOD } → B ∋ x → (x ≡ z ) ∨ (x < z ) )
+→ (z ≡ sup ) ∨ (sup < z )
 --
 --  sup and its fclosure is in a chain HOD
 --    chain HOD is sorted by sup as Ordinal and <-ordered
 --    whole chain is a union of separated Chain
 --
 -- create all ZChains under o< x
 --
+record FChain (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) (x : Ordinal) : Set n where
+field
+supf     : Ordinal → Ordinal
+fcy<sup : { z : Ordinal ) → FClosure A f y z → z <= supf x
+is-sup : ( z : Ordinal ) → (z<x : z o< x ) → { z1 : Ordinal } → FClosure A f (supf z) z1 → z1 <= supf x
+is-minsup : ( x1 : Ordinal ) →
+(( z : Ordinal ) → (z<x : z o< x ) → { z1 : Ordinal } → FClosure A f (supf z) z1 → z1 <= x1 ) → supf x <= x1
+order : {b s z1 : Ordinal} → b o< z → supf s o< supf b → FClosure A f (supf s) z1 → (z1 ≡ supf b) ∨ (z1 << supf b)
+order = ?
+fsupf : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (x : Ordinal ) → FChain A f mf ay x
+fsupf f mf {y} ay x = TransFinite0 find x where
+find : (x : Ordinal ) →  (( z : Ordinal ) → z o< x → FChain A f mf ay z ) → FChain A f mf ay x
+find x prev with trio< o∅ x
+... | tri< a ¬b ¬c = ?
+... | tri≈ ¬a b ¬c = ?
+... | tri> ¬a ¬b c = ?
 ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (x : Ordinal)
 → ((z : Ordinal) → z o< x → ZChain A f mf ay z) → ZChain A f mf ay x
 ind f mf {y} ay x prev with Oprev-p x
 ... | yes op = zc4 where
 --
 ptotal0 : IsTotalOrderSet pchain0
 ptotal0 {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where
 uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
 uz01 = chain-total A f mf ay psupf0 ( (proj2 ca)) ( (proj2 cb))
 usup : SUP A pchain0
 usup = supP pchain0 (λ lt → proj1 lt) ptotal0
 spu = & (SUP.sup usup)
-record Usupf ( w : Ordinal ) : Set n where
-field
-supf : Ordinal → Ordinal
-uniq-supf : {z w1 : Ordinal } → z o< w1 → (w<x : w o< x) → (w1<w : w1 o< w)
-→  supf z ≡ ZChain.supf (prev w1 (ordtrans w1<w w<x )) z
-US : (w1 : Ordinal) → w1 o< x → Usupf w1
-US w1 w1<x = TransFinite0 uind w1 where
-uind :  (w : Ordinal) → ((z : Ordinal) → z o< w → Usupf z ) → Usupf w
-uind w uprev with Oprev-p x
-... | yes op = record { supf = ? ; uniq-supf = ? } where
-px = Oprev.oprev op
-zc : ZChain A f mf ay (Oprev.oprev op)
-zc = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc )
-supf : Ordinal → Ordinal
-supf z with trio< z w
-... | tri< a ¬b ¬c = ZChain.supf (prev _ ?) z
-... | tri≈ ¬a b ¬c = ZChain.supf zc z
-... | tri> ¬a ¬b c = ZChain.supf zc z
-us : {z : Ordinal } → z o< w → (w<x : w o< x) → supf z ≡ ZChain.supf (prev _ w<x) z
-us {z} z<w w<x with trio< z w
-... | tri< a ¬b ¬c = u01 where
-u02 :  ? ≡ Usupf.supf (uprev z a) z
-u02 = ?
-u01 : ZChain.supf (prev ? ?) z ≡ ZChain.supf (prev w w<x) z
-u01 = ? -- subst (λ k → k ≡ _ ) ? ( Usupf.uniq-supf (uprev _ ?) ? ? )
-... | tri≈ ¬a b ¬c = ?
-... | tri> ¬a ¬b c = ?
-... | no wlim = record { supf = supf ; uniq-supf = ? } where
-supf : Ordinal → Ordinal
-supf z with trio< (osuc z) w
-... | tri< a ¬b ¬c = Usupf.supf ( uprev (osuc z) a ) z
-... | tri≈ ¬a b ¬c = spu
-... | tri> ¬a ¬b c = spu
-us : {z : Ordinal} {w2 : Ordinal} → z o< w2
-→ (w<x : w o< x) (w2<w : w2 o< w) → supf z ≡ ZChain.supf (prev w2 (ordtrans w2<w w<x)) z
-us {z} {w2} z<w2 w<x w2<w with trio< (osuc z) w
-... | tri< a ¬b ¬c = ? where
-u00 =  Usupf.uniq-supf (uprev (osuc z) ?)  ? ? ?
-u01 =  Usupf.uniq-supf (uprev w2 ?)  ? ? ?
-... | tri≈ ¬a b ¬c = ?
-... | tri> ¬a ¬b c = ?
 psupf : Ordinal → Ordinal
 psupf z with trio< z x
 ... | tri< a ¬b ¬c = ZChain.supf (pzc (osuc z) (ob<x lim a)) z
 ... | tri≈ ¬a b ¬c = spu              -- ^^ this z dependcy have to be removed
 zc20 : {z : Ordinal } → z ≡ x → spu ≡ psupf x
 zc20 {z} z=x with trio< z x | inspect psupf z
 ... | tri< a ¬b ¬c | _ = ⊥-elim ( ¬b z=x)
 ... | tri≈ ¬a b ¬c | record { eq = eq1 } = subst (λ k → spu ≡ psupf k) b (sym eq1)
 ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬b z=x)
+order :  {b sup1 z1 : Ordinal} → b o< x →
+psupf sup1 o< psupf b →
+FClosure A f (psupf sup1) z1 → (z1 ≡ psupf b) ∨ (z1 << psupf b)
+order {b} {s} {z1}  b<x ps<pb fc = ?
 csupf : (z : Ordinal) → odef (UnionCF A f mf ay psupf x) (psupf z)
 csupf z with trio< z x | inspect psupf z
 ... | tri< z<x ¬b ¬c | record { eq = eq1 } = zc11 where
 ozc = pzc (osuc z) (ob<x lim z<x)
 az = proj1 zc12
 zc20 : {z1  : Ordinal} → FClosure A f y z1 → (z1 ≡ psupf z) ∨ (z1 << psupf z)
 zc20 {z1} fc with ZChain.fcy<sup ozc <-osuc fc
 ... | case1 eq = case1 (trans eq (sym eq1) )
 ... | case2 lt = case2 (subst ( λ k → z1 << k ) (sym eq1) lt)
-zc21 :  {sup1 z1 : Ordinal} → psupf sup1 o< psupf z → FClosure A f (psupf sup1) z1 → (z1 ≡ psupf z) ∨ (z1 << psupf z)
-zc21 {s} {z1} s<z fc = zc22 where
-zc25 : psupf z ≡ ZChain.supf ozc z
-zc25 = psupf<z z<x
-s<x : s o< x
-s<x = {!!}
-zc26 : psupf s ≡ ZChain.supf (pzc (osuc s) (ob<x lim s<x))  s
-zc26 = psupf<z s<x
-zc23 : ZChain.supf ozc s o< ZChain.supf ozc z
-zc23 = {!!}
-zc24 : FClosure A f (ZChain.supf ozc s) z1
-zc24 with trio< s x
-... | t = {!!}
-zc22 : (z1 ≡ psupf z) ∨ (z1 << psupf z)
-zc22 with ZChain.order ozc <-osuc zc23 zc24
-... | case1 eq = case1 (trans eq (sym eq1) )
-... | case2 lt = case2 (subst ( λ k → z1 << k ) (sym eq1) lt)
 cp1 : ChainP A f mf ay psupf z (ZChain.supf ozc z)
-cp1 = record {  fcy<sup = zc20   ; order = zc21 }
+cp1 = record {  fcy<sup = zc20   ; order = order z<x  }
 ---  u = supf u = supf z
 ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ sa , ch-is-sup {!!} {!!} {!!} ⟫ where
 sa = SUP.A∋maximal usup
 ... | tri> ¬a ¬b c | record { eq = eq1 } = {!!}

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

comparison src/zorn.agda @ 779:9e34893d9a03