Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 783:195c3c7de021
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 01 Aug 2022 10:37:39 +0900 |
| parents | e8cf9c453431 |
| children | d83b0f7ece32 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 41 insertions(+), 39 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Mon Aug 01 09:38:00 2022 +0900 +++ b/src/zorn.agda Mon Aug 01 10:37:39 2022 +0900 @@ -105,19 +105,19 @@ ≤-monotonic-f A f = (x : Ordinal ) → odef A x → ( * x ≤ * (f x) ) ∧ odef A (f x ) data FClosure (A : HOD) (f : Ordinal → Ordinal ) (s : Ordinal) : Ordinal → Set n where - init : odef A s → FClosure A f s s + init : {s1 : Ordinal } → odef A s → s ≡ s1 → FClosure A f s s1 fsuc : (x : Ordinal) ( p : FClosure A f s x ) → FClosure A f s (f x) A∋fc : {A : HOD} (s : Ordinal) {y : Ordinal } (f : Ordinal → Ordinal) (mf : ≤-monotonic-f A f) → (fcy : FClosure A f s y ) → odef A y -A∋fc {A} s f mf (init as) = as +A∋fc {A} s f mf (init as refl ) = as A∋fc {A} s f mf (fsuc y fcy) = proj2 (mf y ( A∋fc {A} s f mf fcy ) ) A∋fcs : {A : HOD} (s : Ordinal) {y : Ordinal } (f : Ordinal → Ordinal) (mf : ≤-monotonic-f A f) → (fcy : FClosure A f s y ) → odef A s -A∋fcs {A} s f mf (init as) = as +A∋fcs {A} s f mf (init as refl) = as A∋fcs {A} s f mf (fsuc y fcy) = A∋fcs {A} s f mf fcy s≤fc : {A : HOD} (s : Ordinal ) {y : Ordinal } (f : Ordinal → Ordinal) (mf : ≤-monotonic-f A f) → (fcy : FClosure A f s y ) → * s ≤ * y -s≤fc {A} s {.s} f mf (init x) = case1 refl +s≤fc {A} s {.s} f mf (init x refl ) = case1 refl s≤fc {A} s {.(f x)} f mf (fsuc x fcy) with proj1 (mf x (A∋fc s f mf fcy ) ) ... | case1 x=fx = subst (λ k → * s ≤ * k ) (*≡*→≡ x=fx) ( s≤fc {A} s f mf fcy ) ... | case2 x<fx with s≤fc {A} s f mf fcy @@ -125,7 +125,7 @@ ... | case2 s<x = case2 ( IsStrictPartialOrder.trans PO s<x x<fx ) fcn : {A : HOD} (s : Ordinal) { x : Ordinal} {f : Ordinal → Ordinal} → (mf : ≤-monotonic-f A f) → FClosure A f s x → ℕ -fcn s mf (init as) = zero +fcn s mf (init as refl) = zero fcn {A} s {x} {f} mf (fsuc y p) with proj1 (mf y (A∋fc s f mf p)) ... | case1 eq = fcn s mf p ... | case2 y<fy = suc (fcn s mf p ) @@ -134,11 +134,11 @@ → (cx : FClosure A f s x ) (cy : FClosure A f s y ) → fcn s mf cx ≡ fcn s mf cy → * x ≡ * y fcn-inject {A} s {x} {y} {f} mf cx cy eq = fc00 (fcn s mf cx) (fcn s mf cy) eq cx cy refl refl where fc00 : (i j : ℕ ) → i ≡ j → {x y : Ordinal } → (cx : FClosure A f s x ) (cy : FClosure A f s y ) → i ≡ fcn s mf cx → j ≡ fcn s mf cy → * x ≡ * y - fc00 zero zero refl (init _) (init x₁) i=x i=y = refl - fc00 zero zero refl (init as) (fsuc y cy) i=x i=y with proj1 (mf y (A∋fc s f mf cy ) ) - ... | case1 y=fy = subst (λ k → * s ≡ k ) y=fy ( fc00 zero zero refl (init as) cy i=x i=y ) - fc00 zero zero refl (fsuc x cx) (init as) i=x i=y with proj1 (mf x (A∋fc s f mf cx ) ) - ... | case1 x=fx = subst (λ k → k ≡ * s ) x=fx ( fc00 zero zero refl cx (init as) i=x i=y ) + fc00 zero zero refl (init _ refl) (init x₁ refl) i=x i=y = refl + fc00 zero zero refl (init as refl) (fsuc y cy) i=x i=y with proj1 (mf y (A∋fc s f mf cy ) ) + ... | case1 y=fy = subst (λ k → * s ≡ k ) y=fy ( fc00 zero zero refl (init as refl) cy i=x i=y ) + fc00 zero zero refl (fsuc x cx) (init as refl) i=x i=y with proj1 (mf x (A∋fc s f mf cx ) ) + ... | case1 x=fx = subst (λ k → k ≡ * s ) x=fx ( fc00 zero zero refl cx (init as refl) i=x i=y ) fc00 zero zero refl (fsuc x cx) (fsuc y cy) i=x i=y with proj1 (mf x (A∋fc s f mf cx ) ) | proj1 (mf y (A∋fc s f mf cy ) ) ... | case1 x=fx | case1 y=fy = subst₂ (λ j k → j ≡ k ) x=fx y=fy ( fc00 zero zero refl cx cy i=x i=y ) fc00 (suc i) (suc j) i=j {.(f x)} {.(f y)} (fsuc x cx) (fsuc y cy) i=x j=y with proj1 (mf x (A∋fc s f mf cx ) ) | proj1 (mf y (A∋fc s f mf cy ) ) @@ -211,7 +211,7 @@ cxx : FClosure A f s (f x) cxx = fsuc x cx fc16 : (x : Ordinal ) → (cx : FClosure A f s x) → (fcn s mf cx ≡ fcn s mf (fsuc x cx)) ∨ ( suc (fcn s mf cx ) ≡ fcn s mf (fsuc x cx)) - fc16 x (init as) with proj1 (mf s as ) + fc16 x (init as refl) with proj1 (mf s as ) ... | case1 _ = case1 refl ... | case2 _ = case2 refl fc16 .(f x) (fsuc x cx ) with proj1 (mf (f x) (A∋fc s f mf (fsuc x cx)) ) @@ -230,8 +230,8 @@ → {p0 p1 : Ordinal → Ordinal} → p0 u ≡ p1 u → FClosure A f (p0 u) b → FClosure A f (p1 u) b -fc-conv A f {.(p0 u)} {u} {p0} {p1} p0u=p1u (init ap0u) = subst (λ k → FClosure A f (p1 u) k) (sym p0u=p1u) - ( init (subst (λ k → odef A k) p0u=p1u ap0u )) +fc-conv A f {.(p0 u)} {u} {p0} {p1} p0u=p1u (init ap0u refl) = subst (λ k → FClosure A f (p1 u) k) (sym p0u=p1u) + ( init (subst (λ k → odef A k) p0u=p1u ap0u ) refl) fc-conv A f {_} {u} {p0} {p1} p0u=p1u (fsuc z fc) = fsuc z (fc-conv A f {_} {u} {p0} {p1} p0u=p1u fc) -- open import Relation.Binary.Properties.Poset as Poset @@ -298,15 +298,15 @@ = record { od = record { def = λ z → odef A z ∧ UChain A f mf ay supf x z } ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy } record ZChain ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) - {init : Ordinal} (ay : odef A init) ( z : Ordinal ) : Set (Level.suc n) where + {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 field chain⊆A : chain ⊆' A - chain∋init : odef chain init - initial : {y : Ordinal } → odef chain y → * init ≤ * y + chain∋init : odef chain y + initial : {z : Ordinal } → odef chain z → * y ≤ * z f-next : {a : Ordinal } → odef chain a → odef chain (f a) f-total : IsTotalOrderSet chain @@ -315,29 +315,31 @@ 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 csupf : (z : Ordinal ) → odef chain (supf z) csupf' : {b : Ordinal } → b o≤ z → odef (UnionCF A f mf ay supf b) (supf 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 + fcy<sup : {u w : Ordinal } → u o< z → FClosure A f y w → (w ≡ supf u ) ∨ ( w << supf u ) -- different from order because y o< supf 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) supf∈A : {u : Ordinal } → odef A (supf u) supf∈A = ? - 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 - fcy<sup' {u} {w} u<z fc with SUP.x<sup (sup ?) ⟪ subst (λ k → odef A k ) (sym &iso) (A∋fc {A} init f mf fc) , ? ⟫ + fcy<sup' : {u w : Ordinal } → u o< z → FClosure A f y w → (w ≡ supf u ) ∨ ( w << supf u ) -- different from order because y o< supf + fcy<sup' {u} {w} u<z fc with SUP.x<sup (sup (o<→≤ u<z)) ⟪ subst (λ k → odef A k ) (sym &iso) (A∋fc {A} y f mf fc) , ? ⟫ ... | case1 eq = ? ... | case2 lt = ? fc∈A : {s z1 : Ordinal} → FClosure A f (supf s) z1 → odef chain z1 fc∈A {s} (fsuc x fc) = f-next (fc∈A {s} fc ) -- (supf s) ≡ z1 → init (supf s) 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' {b} {s} {z1} b<z sf<sb fc with SUP.x<sup (sup (o<→≤ b<z)) (subst (λ k → odef (UnionCF A f mf ay supf b) k) (sym &iso) ( csupf' (o<→≤ b<z)) ) - ... | case1 eq = case1 (begin - ? ≡⟨ ? ⟩ - ? ∎ ) where open ≡-Reasoning - ... | case2 lt = case2 ? where - zc00 : ? - zc00 = ? - -- case2 ( subst (λ k → * z1 < k ) (subst₂ (λ j k → j ≡ k ) *iso ? (cong (*) (sym supf-is-sup))) lt ) + order' {b} {s} {.(f x)} b<z sf<sb (fsuc x fc) with proj1 (mf x (A∋fc _ f mf fc)) | order' b<z sf<sb fc + ... | case1 eq | t = ? + ... | case2 lt | t = ? + order' {b} {s} {z1} b<z sf<sb (init x refl) = ? where + zc01 : s o≤ z + zc01 = ? + zc00 : ( * (supf s) ≡ SUP.sup (sup (o<→≤ b<z ))) ∨ ( * (supf s) < SUP.sup ( sup (o<→≤ b<z )) ) + zc00 with csupf' zc01 + ... | ⟪ ss , ch-init fc ⟫ = SUP.x<sup (sup (o<→≤ b<z)) ⟪ ? , ch-init ? ⟫ + ... | ⟪ ss , ch-is-sup us is-sup fc ⟫ = SUP.x<sup (sup (o<→≤ b<z)) ⟪ ? , ch-is-sup us ? ? ⟫ 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 + {y : Ordinal} (ay : odef A y) (zc : ZChain A f mf ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where field is-max : {a b : Ordinal } → (ca : odef (UnionCF A f mf ay (ZChain.supf zc) z) a ) → b o< z → (ab : odef A b) → HasPrev A (UnionCF A f mf ay (ZChain.supf zc) z) ab f ∨ IsSup A (UnionCF A f mf ay (ZChain.supf zc) z) ab @@ -442,7 +444,7 @@ init-uchain : (A : HOD) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal } → (ay : odef A y ) { supf : Ordinal → Ordinal } { x : Ordinal } → odef (UnionCF A f mf ay supf x) y -init-uchain A f mf ay = ⟪ ay , ch-init (init ay) ⟫ +init-uchain A f mf ay = ⟪ ay , ch-init (init ay refl) ⟫ ChainP-next : (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal ) → {x z : Ordinal } → ChainP A f mf ay supf x z → ChainP A f mf ay supf x (f z ) @@ -559,7 +561,7 @@ 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-mono1 x lt) } ) a<b - ... | tri≈ ¬a b=px ¬c = ⟪ ab , ch-is-sup b m06 (subst (λ k → FClosure A f k b) m05 (init ab)) ⟫ where + ... | tri≈ ¬a b=px ¬c = ⟪ ab , ch-is-sup b m06 (subst (λ k → FClosure A f k b) m05 (init ab refl)) ⟫ where b<A : b o< & A b<A = z09 ab m05 : b ≡ ZChain.supf zc b @@ -595,7 +597,7 @@ m06 : ChainP A f mf ay (ZChain.supf zc) b b m06 = record { fcy<sup = m07 ; order = m08 } 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)) ⟫ + m04 = ⟪ ab , ch-is-sup b m06 (subst (λ k → FClosure A f k b) m05 (init ab refl)) ⟫ --- --- the maximum chain has fix point of any ≤-monotonic function @@ -684,9 +686,9 @@ sp = ysup f mf ay asi = SUP.A∋maximal sp cy : odef (UnionCF A f mf ay isupf o∅) y - cy = ⟪ ay , ch-init (init ay) ⟫ + cy = ⟪ ay , ch-init (init ay refl) ⟫ y<sup : * y ≤ SUP.sup (ysup f mf ay) - y<sup = SUP.x<sup (ysup f mf ay) (subst (λ k → FClosure A f y k ) (sym &iso) (init ay)) + y<sup = SUP.x<sup (ysup f mf ay) (subst (λ k → FClosure A f y k ) (sym &iso) (init ay refl)) isy : {z : Ordinal } → odef (UnionCF A f mf ay isupf o∅) z → * y ≤ * z isy {z} ⟪ az , uz ⟫ with uz ... | ch-init fc = s≤fc y f mf fc @@ -701,7 +703,7 @@ uz01 = chain-total A f mf ay isupf (proj2 ca) (proj2 cb) csupf : (z : Ordinal) → odef (UnionCF A f mf ay isupf o∅) (isupf z) - csupf z = ⟪ asi , ch-is-sup spi uz02 (init asi) ⟫ where + csupf z = ⟪ asi , ch-is-sup spi uz02 (init asi refl) ⟫ where uz03 : {z : Ordinal } → FClosure A f y z → (z ≡ isupf spi) ∨ (z << isupf spi) uz03 {z} fc with SUP.x<sup sp (subst (λ k → FClosure A f y k ) (sym &iso) fc ) ... | case1 eq = case1 ( begin @@ -750,9 +752,9 @@ ... | ch-init fc = s≤fc y f mf fc ... | ch-is-sup u is-sup fc = ≤-ftrans (<=to≤ zc7) (s≤fc _ f mf fc) where zc7 : y <= (ZChain.supf zc) u - zc7 = ChainP.fcy<sup is-sup (init ay) + zc7 = ChainP.fcy<sup is-sup (init ay refl) pcy : odef pchain y - pcy = ⟪ ay , ch-init (init ay) ⟫ + pcy = ⟪ ay , ch-init (init ay refl) ⟫ supf0 = ZChain.supf zc @@ -863,7 +865,7 @@ zc12 : odef A (ZChain.supf ozc z) ∧ UChain A f mf ay (ZChain.supf ozc) (osuc z) (ZChain.supf ozc z) zc12 = ZChain.csupf ozc z zc11 : odef A (ZChain.supf ozc z) ∧ UChain A f mf ay psupf x (ZChain.supf ozc z) - zc11 = ⟪ az , ch-is-sup z cp1 (subst (λ k → FClosure A f k _) (sym eq1) (init az) ) ⟫ where + zc11 = ⟪ az , ch-is-sup z cp1 (subst (λ k → FClosure A f k _) (sym eq1) (init az refl) ) ⟫ where az : odef A ( ZChain.supf ozc z ) az = proj1 zc12 zc20 : {z1 : Ordinal} → FClosure A f y z1 → (z1 ≡ psupf z) ∨ (z1 << psupf z) @@ -898,9 +900,9 @@ ... | ch-init fc = s≤fc y f mf fc ... | ch-is-sup u is-sup fc = ≤-ftrans (<=to≤ zc7) (s≤fc _ f mf fc) where zc7 : y <= psupf _ - zc7 = ChainP.fcy<sup is-sup (init ay) + zc7 = ChainP.fcy<sup is-sup (init ay refl) pcy : odef pchain y - pcy = ⟪ ay , ch-init (init ay) ⟫ + pcy = ⟪ ay , ch-init (init ay refl) ⟫ ptotal : IsTotalOrderSet pchain ptotal {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) )