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

comparison src/zorn.agda @ 769:34678c0ad278

...

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Mon, 25 Jul 2022 23:38:38 +0900
parents	67c7d4b43844
children	798d8b8c36b1

comparison

equal deleted inserted replaced

-:67c7d4b43844
+:34678c0ad278
 record ChainP (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal) (u z : Ordinal) : Set n where
 field
 csupz    : FClosure A f (supf u) z
 supfu=u  : supf u ≡ u
 fcy<sup  : {z : Ordinal } → FClosure A f y z → (z ≡ supf u) ∨ ( z << supf u )
-order    : {sup1 z1 : Ordinal} → (lt : sup1 o< u ) → FClosure A f (supf sup1 ) z1 → (z1 ≡ supf u ) ∨ ( z1 << supf u )
+order    : {sup1 z1 : Ordinal} → (lt : supf sup1 o< supf u ) → FClosure A f (supf sup1 ) z1 → (z1 ≡ supf u ) ∨ ( z1 << supf u )
 -- Union of supf z which o< x
 --
 data UChain  ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {y : Ordinal } (ay : odef A y )
 chain∋init : odef chain init
 initial : {y : Ordinal } → odef chain y → * init ≤ * y
 f-next : {a : Ordinal } → odef chain a → odef chain (f a)
 f-total : IsTotalOrderSet chain
+supf-mono : { a b : Ordinal } → a o< b → supf a o≤ supf b
 csupf : {z : Ordinal } → odef chain (supf z)
 sup=u : {b : Ordinal} → (ab : odef A b) → b o< z  → IsSup A (UnionCF A f mf ay supf (osuc b)) ab → supf b ≡ b
 fcy<sup  : {u w : Ordinal } → u o< z  → FClosure A f init w → (w ≡ supf u ) ∨ ( w << supf u ) -- different from order because y o< supf
-order : {b sup1 z1 : Ordinal} → b o< z → sup1 o< b → FClosure A f (supf sup1) z1 → (z1 ≡ supf b) ∨ (z1 << supf b)
+order : {b sup1 z1 : Ordinal} → b o< z → supf sup1 o< supf b → FClosure A f (supf sup1) z1 → (z1 ≡ supf b) ∨ (z1 << supf b)
 record ZChain1 ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f)
 {init : Ordinal} (ay : odef A init)  (zc : ZChain A f mf ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where
 field
 ct00 = lt
 ct01 : * b < * a
 ct01 with s≤fc (supf ua) f mf fca
 ... | case1 eq =  subst (λ k → * b < k ) eq ct00
 ... | case2 lt =  IsStrictPartialOrder.trans POO ct00 lt
-ct-ind xa xb {a} {b} (ch-is-sup ua supa fca) (ch-is-sup ub supb fcb) with trio< ua ub
+ct-ind xa xb {a} {b} (ch-is-sup ua supa fca) (ch-is-sup ub supb fcb) with trio< (supf ua) (supf ub)
 ... | tri< a₁ ¬b ¬c with ChainP.order supb  a₁ (ChainP.csupz supa)
 ... | case1 eq with s≤fc (supf ub) f mf fcb
 ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00  (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
 ct00 : * a ≡ * b
 ct00 = trans (cong (*) eq) eq1
 ct03 = lt
 ct02 : * a < * b
 ct02 with s≤fc (supf ub) f mf fcb
 ... | case1 eq =  subst (λ k → * a < k ) eq ct03
 ... | case2 lt =  IsStrictPartialOrder.trans POO ct03 lt
-ct-ind xa xb {a} {b} (ch-is-sup ua supa fca) (ch-is-sup ub supb fcb) | tri≈ ¬a  refl ¬c = fcn-cmp (supf ua) f mf fca fcb
+ct-ind xa xb {a} {b} (ch-is-sup ua supa fca) (ch-is-sup ub supb fcb) | tri≈ ¬a  eq ¬c
+= fcn-cmp (supf ua) f mf fca (subst (λ k → FClosure A f k b ) (sym eq) fcb )
 ct-ind xa xb {a} {b} (ch-is-sup ua supa fca) (ch-is-sup ub supb fcb) | tri> ¬a ¬b c with ChainP.order supa c (ChainP.csupz supb)
 ... | case1 eq with s≤fc (supf ua) f mf fca
 ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00  (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
 ct00 : * a ≡ * b
 ct00 = sym (trans (cong (*) eq) eq1)
 m07 = osucc (ordtrans b<px px<x )
 fcb : FClosure A f (ZChain.supf zc b) b
 fcb = subst (λ k → FClosure A f k b ) (sym (ZChain.sup=u zc ab (z09 ab)
 (record {x<sup = λ {z} lt → IsSup.x<sup is-sup (chain-mono2 x m07 o≤-refl lt)  } ) )) ( init ab )
 m08 :  odef (UnionCF A f mf ay (ZChain.supf zc) px) a
-m08 with subst (λ k → b <= k ) su=u ( ZChain.order zc u<A (ordtrans b<px c)  fcb )
+m08 with osuc-≡<  (ZChain.supf-mono zc (ordtrans b<px c))
+... | case1 eq = ?
+... | case2 lt  with subst (λ k → b <= k ) su=u ( ZChain.order zc u<A lt fcb )
 ... | case2 b<u = ⊥-elim (<-irr u≤a (ptrans a<b b<u ) )
 ... | case1 eq = ⊥-elim ( <-irr (s≤fc u f mf (subst (λ k → FClosure A f k a ) su=u fc )) (subst (λ k → * a < * k) eq a<b ))
 m04 : odef (UnionCF A f mf ay (ZChain.supf zc) px) b
 m04 = ZChain1.is-max (prev px px<x) m03 b<px ab
 (case2 record {x<sup = λ {z} lt → IsSup.x<sup is-sup (chain-mono2 x ( o<→≤  (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ))  o≤-refl lt)  } ) a<b
 m05 : b ≡ ZChain.supf zc b
 m05 = sym ( ZChain.sup=u zc ab (z09 ab)
 record { x<sup = λ {z} uz → IsSup.x<sup is-sup (chain-mono2 x (osucc b<x) o≤-refl uz )  }  )
 m08 : {z : Ordinal} → (fcz : FClosure A f y z ) → z <= ZChain.supf zc b
 m08 {z} fcz = ZChain.fcy<sup zc b<A fcz
-m09 : {sup1 z1 : Ordinal} → sup1 o< b → FClosure A f (ZChain.supf zc sup1) z1 → z1 <= ZChain.supf zc b
+m09 : {sup1 z1 : Ordinal} → (ZChain.supf zc sup1) o< (ZChain.supf zc b)
-m09 {sup1} {z} s<b fcz = ZChain.order zc b<A s<b fcz
+→ FClosure A f (ZChain.supf zc sup1) z1 → z1 <= ZChain.supf zc b
+m09 {sup1} {z} s<b fcz = ZChain.order zc b<A ? fcz
 m06 : ChainP A f mf ay (ZChain.supf zc) b b
 m06 = record { csupz = subst (λ k → FClosure A f k b) m05 (init ab) ; supfu=u = sym m05
 ; fcy<sup = m08  ; order = m09 }
 ... | no lim = record { is-max = is-max }  where
 is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a →
 b o< x → (ab : odef A b) →
 HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) ab f ∨ IsSup A (UnionCF A f mf ay (ZChain.supf zc) x) ab →
 * a < * b → odef (UnionCF A f mf ay (ZChain.supf zc) x) b
 ... | case2 y<b = chain-mono2 x (o<→≤ (ob<x lim b<x) ) o≤-refl m04 where
 m09 : b o< & A
 m09 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab))
 m07 : {z : Ordinal} → FClosure A f y z → z <= ZChain.supf zc b
 m07 {z} fc = ZChain.fcy<sup zc m09 fc
-m08 : {sup1 z1 : Ordinal} → sup1 o< b → FClosure A f (ZChain.supf zc sup1) z1 → z1 <= ZChain.supf zc b
+m08 : {sup1 z1 : Ordinal} → (ZChain.supf zc sup1) o< (ZChain.supf zc b)
+→ FClosure A f (ZChain.supf zc sup1) z1 → z1 <= ZChain.supf zc b
 m08 {sup1} {z1} s<b fc = ZChain.order zc m09 s<b fc
 m05 : b ≡ ZChain.supf zc b
 m05 = sym (ZChain.sup=u zc ab m09
 record { x<sup = λ lt → IsSup.x<sup is-sup (chain-mono2 x (o<→≤ (ob<x lim b<x)) o≤-refl lt )} )   -- ZChain on x
 m06 : ChainP A f mf ay (ZChain.supf zc) b b
 m06 = record { fcy<sup = m07 ; csupz = subst (λ k →  FClosure A f k b ) m05 (init ab) ; order = m08
 ; supfu=u = sym m05 }
 m04 : odef (UnionCF A f mf ay (ZChain.supf zc) (osuc b)) b
 m04 = ⟪ ab , ch-is-sup b  m06 (subst (λ k → FClosure A f k b) m05 (init ab))  ⟫
 ---
 ... | case1 eq = case1 ( begin
 z ≡⟨ sym &iso  ⟩
 & (* z) ≡⟨ cong (&) eq  ⟩
 spi  ∎ ) where open ≡-Reasoning
 ... | case2 lt = case2 (subst (λ k → * z < k ) (sym *iso) lt )
-uz04 : {sup1 z1 : Ordinal} → sup1 o< spi → FClosure A f (isupf sup1) z1 → (z1 ≡ isupf spi) ∨ (z1 << isupf spi)
+uz04 : {sup1 z1 : Ordinal} → isupf sup1 o< isupf spi → FClosure A f (isupf sup1) z1 → (z1 ≡ isupf spi) ∨ (z1 << isupf spi)
-uz04 {s} {z} s<spi fcz = ?
+uz04 {s} {z} s<spi fcz = ⊥-elim ( o<¬≡ refl s<spi )
 uz02 :  ChainP A f mf ay isupf spi (isupf z)
-uz02 = record { csupz = init asi ; supfu=u = refl ; fcy<sup = uz03 ; order = ? }
+uz02 = record { csupz = init asi ; supfu=u = refl ; fcy<sup = uz03 ; order = λ {s} {z} → uz04 {s} {z} }
 --
 -- create all ZChains under o< x
 --

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

comparison src/zorn.agda @ 769:34678c0ad278