Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1096:55ab5de1ae02
recovery
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 23 Dec 2022 12:54:05 +0900 |
| parents | 08b6aa6870d9 |
| children | 40345abc0949 |
| files | src/BAlgbra.agda src/LEMC.agda src/OD.agda src/ODC.agda src/ODUtil.agda src/OPair.agda src/PFOD.agda src/filter.agda src/generic-filter.agda src/partfunc.agda src/zorn.agda |
| diffstat | 11 files changed, 96 insertions(+), 110 deletions(-) [+] |
line wrap: on
line diff
--- a/src/BAlgbra.agda Thu Dec 22 15:10:31 2022 +0900 +++ b/src/BAlgbra.agda Fri Dec 23 12:54:05 2022 +0900 @@ -58,7 +58,7 @@ ; eq→ = λ {x} lt → ⊥-elim (proj2 (proj1 lt ) (proj2 lt)) } U-F=∅→F⊆U : {F U : HOD} → ((x : Ordinal) → ¬ ( odef F x ∧ ( ¬ odef U x ))) → F ⊆ U -U-F=∅→F⊆U {F} {U} not = record { incl = gt02 } where +U-F=∅→F⊆U {F} {U} not = gt02 where gt02 : { x : Ordinal } → odef F x → odef U x gt02 {x} fx with ODC.∋-p O U (* x) ... | yes y = subst (λ k → odef U k ) &iso y @@ -67,13 +67,12 @@ ∪-Union : { A B : HOD } → Union (A , B) ≡ ( A ∪ B ) ∪-Union {A} {B} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where lemma1 : {x : Ordinal} → odef (Union (A , B)) x → odef (A ∪ B) x - lemma1 {x} lt = lemma3 lt where - lemma4 : {y : Ordinal} → odef (A , B) y ∧ odef (* y) x → ¬ (¬ ( odef A x ∨ odef B x) ) - lemma4 {y} z with proj1 z - lemma4 {y} z | case1 refl = double-neg (case1 ( subst (λ k → odef k x ) *iso (proj2 z)) ) - lemma4 {y} z | case2 refl = double-neg (case2 ( subst (λ k → odef k x ) *iso (proj2 z)) ) - lemma3 : (((u : Ordinal ) → ¬ odef (A , B) u ∧ odef (* u) x) → ⊥) → odef (A ∪ B) x - lemma3 not = ODC.double-neg-eilm O (FExists _ lemma4 not) -- choice + lemma1 {x} record { owner = owner ; ao = abo ; ox = ox } with pair=∨ (subst₂ (λ j k → odef (j , k ) owner) (sym *iso) (sym *iso) abo ) + ... | case1 a=o = case1 (subst (λ k → odef k x ) ( begin + * owner ≡⟨ cong (*) (sym a=o) ⟩ + * (& A) ≡⟨ *iso ⟩ + A ∎ ) ox ) where open ≡-Reasoning + ... | case2 b=o = case2 (subst (λ k → odef k x ) (trans (cong (*) (sym b=o)) *iso ) ox) lemma2 : {x : Ordinal} → odef (A ∪ B) x → odef (Union (A , B)) x lemma2 {x} (case1 A∋x) = subst (λ k → odef (Union (A , B)) k) &iso ( IsZF.union→ isZF (A , B) (* x) A ⟪ case1 refl , d→∋ A A∋x ⟫ )
--- a/src/LEMC.agda Thu Dec 22 15:10:31 2022 +0900 +++ b/src/LEMC.agda Fri Dec 23 12:54:05 2022 +0900 @@ -32,8 +32,6 @@ open HOD -open _⊆_ - decp : ( p : Set n ) → Dec p -- assuming axiom of choice decp p with p∨¬p p decp p | case1 x = yes x @@ -50,8 +48,8 @@ ... | no ¬p = ⊥-elim ( notnot ¬p ) power→⊆ : ( A t : HOD) → Power A ∋ t → t ⊆ A -power→⊆ A t PA∋t = record { incl = λ {x} t∋x → double-neg-eilm (λ not → t1 t∋x (λ x → not x) ) } where - t1 : {x : HOD } → t ∋ x → ¬ ¬ (A ∋ x) +power→⊆ A t PA∋t t∋x = subst (λ k → odef A k ) &iso ( t1 (subst (λ k → odef t k ) (sym &iso) t∋x)) where + t1 : {x : HOD } → t ∋ x → A ∋ x t1 = power→ A t PA∋t --- With assuption of HOD is ordered, p ∨ ( ¬ p ) <=> axiom of choice
--- a/src/OD.agda Thu Dec 22 15:10:31 2022 +0900 +++ b/src/OD.agda Fri Dec 23 12:54:05 2022 +0900 @@ -265,11 +265,9 @@ A ∩ B = record { od = record { def = λ x → odef A x ∧ odef B x } ; odmax = omin (odmax A) (odmax B) ; <odmax = λ y → min1 (<odmax A (proj1 y)) (<odmax B (proj2 y))} -record _⊆_ ( A B : HOD ) : Set (suc n) where - field - incl : { x : HOD } → A ∋ x → B ∋ x +_⊆_ : ( A B : HOD) → Set n +_⊆_ A B = { x : Ordinal } → odef A x → odef B x -open _⊆_ infixr 220 _⊆_ -- if we have & (x , x) ≡ osuc (& x), ⊆→o≤ → c<→o< @@ -298,28 +296,6 @@ ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (* oy) ε-induction-ord ox {oy} lt = TransFinite {λ oy → ψ (* oy)} induction oy -record OSUP (A x : Ordinal ) ( ψ : ( x : Ordinal ) → odef (* A) x → Ordinal ) : Set n where - field - sup-o' : Ordinal - sup-o≤' : {z : Ordinal } → z o< x → (lt : odef (* A) z ) → ψ z lt o≤ sup-o' - --- o<-sup : ( A x : Ordinal) { ψ : ( x : Ordinal ) → odef (* A) x → Ordinal } → OSUP A x ψ --- o<-sup A x {ψ} = ? where --- m00 : (x : Ordinal ) → OSUP A x ψ --- m00 x = Ordinals.inOrdinal.TransFinite0 O ind x where --- ind : (x : Ordinal) → ((z : Ordinal) → z o< x → OSUP A z ψ ) → OSUP A x ψ --- ind x prev = ? where --- if has prev , od01 is empty use prev (cannot be odef (* A) x) --- not empty, take larger --- limit ordinal, take address of Union --- --- od01 : HOD --- od01 = record { od = record { def = λ z → odef A z ∧ ( z ≡ & x ) } ; odmax = & A ; <odmax = odef∧< } --- m01 : OSUP A x ψ --- m01 with is-o∅ (& od01 ) --- ... | case1 t=0 = record { sup-o' = prevjjk --- ... | case2 t>0 = ? - -- Open supreme upper bound leads a contradition, so we use domain restriction on sup ¬open-sup : ( sup-o : (Ordinal → Ordinal ) → Ordinal) → ((ψ : Ordinal → Ordinal ) → (x : Ordinal) → ψ x o< sup-o ψ ) → ⊥ ¬open-sup sup-o sup-o< = o<> <-osuc (sup-o< next-ord (sup-o next-ord)) where @@ -468,13 +444,13 @@ pair← x y t (case2 t=h=y) = case2 (cong (λ k → & k ) (==→o≡ t=h=y)) o<→c< : {x y : Ordinal } → x o< y → (Ord x) ⊆ (Ord y) -o<→c< lt = record { incl = λ z → ordtrans z lt } +o<→c< lt {z} ox = ordtrans ox lt ⊆→o< : {x y : Ordinal } → (Ord x) ⊆ (Ord y) → x o< osuc y ⊆→o< {x} {y} lt with trio< x y ⊆→o< {x} {y} lt | tri< a ¬b ¬c = ordtrans a <-osuc ⊆→o< {x} {y} lt | tri≈ ¬a b ¬c = subst ( λ k → k o< osuc y) (sym b) <-osuc -⊆→o< {x} {y} lt | tri> ¬a ¬b c with (incl lt) (o<-subst c (sym &iso) refl ) +⊆→o< {x} {y} lt | tri> ¬a ¬b c with lt (o<-subst c (sym &iso) refl ) ... | ttt = ⊥-elim ( o<¬≡ refl (o<-subst ttt &iso refl )) ψiso : {ψ : HOD → Set n} {x y : HOD } → ψ x → x ≡ y → ψ y
--- a/src/ODC.agda Thu Dec 22 15:10:31 2022 +0900 +++ b/src/ODC.agda Fri Dec 23 12:54:05 2022 +0900 @@ -95,17 +95,13 @@ or-exclude {A} {B} (case2 b) | case1 a = case1 a or-exclude {A} {B} (case2 b) | case2 ¬a = case2 ⟪ ¬a , b ⟫ -open _⊆_ - power→⊆ : ( A t : HOD) → Power A ∋ t → t ⊆ A -power→⊆ A t PA∋t = record { incl = λ {x} t∋x → double-neg-eilm (t1 t∋x) } where - t1 : {x : HOD } → t ∋ x → ¬ ¬ (A ∋ x) - t1 = power→ A t PA∋t +power→⊆ A t PA∋t tx = subst (λ k → odef A k ) &iso ( power→ A t PA∋t (subst (λ k → odef t k) (sym &iso) tx ) ) power-∩ : { A x y : HOD } → Power A ∋ x → Power A ∋ y → Power A ∋ ( x ∩ y ) power-∩ {A} {x} {y} ax ay = power← A (x ∩ y) p01 where p01 : {z : HOD} → (x ∩ y) ∋ z → A ∋ z - p01 {z} xyz = double-neg-eilm ( power→ A x ax (proj1 xyz )) + p01 {z} xyz = power→ A x ax (proj1 xyz ) OrdP : ( x : Ordinal ) ( y : HOD ) → Dec ( Ord x ∋ y ) OrdP x y with trio< x (& y)
--- a/src/ODUtil.agda Thu Dec 22 15:10:31 2022 +0900 +++ b/src/ODUtil.agda Fri Dec 23 12:54:05 2022 +0900 @@ -26,7 +26,6 @@ open ODAxiom odAxiom open HOD -open _⊆_ open _∧_ open _==_ @@ -58,25 +57,25 @@ lemmab1 = ho< trans-⊆ : { A B C : HOD} → A ⊆ B → B ⊆ C → A ⊆ C -trans-⊆ A⊆B B⊆C = record { incl = λ x → incl B⊆C (incl A⊆B x) } +trans-⊆ A⊆B B⊆C ab = B⊆C (A⊆B ab) refl-⊆ : {A : HOD} → A ⊆ A -refl-⊆ {A} = record { incl = λ x → x } +refl-⊆ x = x od⊆→o≤ : {x y : HOD } → x ⊆ y → & x o< osuc (& y) -od⊆→o≤ {x} {y} lt = ⊆→o≤ {x} {y} (λ {z} x>z → subst (λ k → def (od y) k ) &iso (incl lt (d→∋ x x>z))) +od⊆→o≤ {x} {y} lt = ⊆→o≤ {x} {y} (λ {z} x>z → subst (λ k → def (od y) k ) &iso (lt (d→∋ x x>z))) ⊆→= : {F U : HOD} → F ⊆ U → U ⊆ F → F =h= U -⊆→= {F} {U} FU UF = record { eq→ = λ {x} lt → subst (λ k → odef U k) &iso (incl FU (subst (λ k → odef F k) (sym &iso) lt) ) - ; eq← = λ {x} lt → subst (λ k → odef F k) &iso (incl UF (subst (λ k → odef U k) (sym &iso) lt) ) } +⊆→= {F} {U} FU UF = record { eq→ = λ {x} lt → subst (λ k → odef U k) &iso (FU (subst (λ k → odef F k) (sym &iso) lt) ) + ; eq← = λ {x} lt → subst (λ k → odef F k) &iso (UF (subst (λ k → odef U k) (sym &iso) lt) ) } ¬A∋x→A≡od∅ : (A : HOD) → {x : HOD} → A ∋ x → ¬ ( & A ≡ o∅ ) ¬A∋x→A≡od∅ A {x} ax a=0 = ¬x<0 ( subst (λ k → & x o< k) a=0 (c<→o< ax )) subset-lemma : {A x : HOD } → ( {y : HOD } → x ∋ y → (A ∩ x ) ∋ y ) ⇔ ( x ⊆ A ) subset-lemma {A} {x} = record { - proj1 = λ lt → record { incl = λ x∋z → proj1 (lt x∋z) } - ; proj2 = λ x⊆A lt → ⟪ incl x⊆A lt , lt ⟫ + proj1 = λ lt x∋z → subst (λ k → odef A k ) &iso ( proj1 (lt (subst (λ k → odef x k) (sym &iso) x∋z ) )) + ; proj2 = λ x⊆A lt → ⟪ x⊆A lt , lt ⟫ } ω<next-o∅ : {y : Ordinal} → infinite-d y → y o< next o∅ @@ -109,20 +108,34 @@ single (case1 eq) = ==→o≡ ( ord→== (sym eq) ) single (case2 eq) = ==→o≡ ( ord→== (sym eq) ) +single& : {x y : Ordinal } → odef (* x , * x ) y → x ≡ y +single& (case1 eq) = sym (trans eq &iso) +single& (case2 eq) = sym (trans eq &iso) + open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) -- postulate f-extensionality : { n m : Level} → HE.Extensionality n m +pair=∨ : {a b c : Ordinal } → odef (* a , * b) c → ( a ≡ c ) ∨ ( b ≡ c ) +pair=∨ {a} {b} {c} (case1 c=a) = case1 ( sym (trans c=a &iso)) +pair=∨ {a} {b} {c} (case2 c=b) = case2 ( sym (trans c=b &iso)) + ω-prev-eq1 : {x y : Ordinal} → & (Union (* y , (* y , * y))) ≡ & (Union (* x , (* x , * x))) → ¬ (x o< y) -ω-prev-eq1 {x} {y} eq x<y = eq→ (ord→== eq) {& (* y)} (λ not2 → not2 (& (* y , * y)) - ⟪ case2 refl , subst (λ k → odef k (& (* y))) (sym *iso) (case1 refl)⟫ ) (λ u → lemma u ) where - lemma : (u : Ordinal) → ¬ def (od (* x , (* x , * x))) u ∧ def (od (* u)) (& (* y)) - lemma u t with proj1 t - lemma u t | case1 u=x = o<> (c<→o< {* y} {* u} (proj2 t)) (subst₂ (λ j k → j o< k ) - (trans (sym &iso) (trans (sym u=x) (sym &iso)) ) (sym &iso) x<y ) -- x ≡ & (* u) - lemma u t | case2 u=xx = o<¬≡ (lemma1 (subst (λ k → odef k (& (* y)) ) (trans (cong (λ k → * k ) u=xx) *iso ) (proj2 t))) x<y where - lemma1 : {x y : Ordinal } → (* x , * x ) ∋ * y → x ≡ y -- y = x ∈ ( x , x ) = u - lemma1 (case1 eq) = subst₂ (λ j k → j ≡ k ) &iso &iso (sym eq) - lemma1 (case2 eq) = subst₂ (λ j k → j ≡ k ) &iso &iso (sym eq) +ω-prev-eq1 {x} {y} eq x<y with eq→ (ord→== eq) record { owner = & (* y , * y) ; ao = case2 refl + ; ox = subst (λ k → odef k (& (* y))) (sym *iso) (case1 refl) } -- (* x , (* x , * x)) ∋ * y +... | record { owner = u ; ao = xxx∋u ; ox = uy } with xxx∋u +... | case1 u=x = ⊥-elim ( o<> x<y (osucprev (begin + osuc y ≡⟨ sym (cong osuc &iso) ⟩ + osuc (& (* y)) ≤⟨ osucc (c<→o< {* y} {* u} uy) ⟩ -- * x ≡ * u ∋ * y + & (* u) ≡⟨ &iso ⟩ + u ≡⟨ u=x ⟩ + & (* x) ≡⟨ &iso ⟩ + x ∎ ))) where open o≤-Reasoning O +... | case2 u=xx = ⊥-elim (o<¬≡ ( begin + x ≡⟨ single& (subst₂ (λ j k → odef j k ) (begin + * u ≡⟨ cong (*) u=xx ⟩ + * (& (* x , * x)) ≡⟨ *iso ⟩ + (* x , * x ) ∎ ) &iso uy ) ⟩ -- (* x , * x ) ∋ * y + y ∎ ) x<y) where open ≡-Reasoning ω-prev-eq : {x y : Ordinal} → & (Union (* y , (* y , * y))) ≡ & (Union (* x , (* x , * x))) → x ≡ y ω-prev-eq {x} {y} eq with trio< x y @@ -131,7 +144,7 @@ ω-prev-eq {x} {y} eq | tri> ¬a ¬b c = ⊥-elim (ω-prev-eq1 (sym eq) c) ω-∈s : (x : HOD) → Union ( x , (x , x)) ∋ x -ω-∈s x not = not (& (x , x)) ⟪ case2 refl , subst (λ k → odef k (& x) ) (sym *iso) (case1 refl) ⟫ +ω-∈s x = record { owner = & ( x , x ) ; ao = case2 refl ; ox = subst₂ (λ j k → odef j k ) (sym *iso) refl (case2 refl) } ωs≠0 : (x : HOD) → ¬ ( Union ( x , (x , x)) ≡ od∅ ) ωs≠0 y eq = ⊥-elim ( ¬x<0 (subst (λ k → & y o< k ) ord-od∅ (c<→o< (subst (λ k → odef k (& y )) eq (ω-∈s y) ))) ) @@ -154,8 +167,8 @@ ∎ where open ≡-Reasoning lemma0 : x ∋ * x₁ - lemma0 = subst (λ k → odef k (& (* x₁))) (trans (sym *iso) ox=x) (λ not → not - (& (* x₁ , * x₁)) ⟪ pair2 , subst (λ k → odef k (& (* x₁))) (sym *iso) pair1 ⟫ ) + lemma0 = subst (λ k → odef k (& (* x₁))) (trans (sym *iso) ox=x) + record { owner = & ( * x₁ , * x₁ ) ; ao = case2 refl ; ox = subst (λ k → odef k (& (* x₁))) (sym *iso) (case1 refl) } lemma1 : infinite ∋ * x₁ lemma1 = subst (λ k → odef infinite k) (sym &iso) ltd lemma3 : {x y : Ordinal} → (ltd : infinite-d x ) (ltd1 : infinite-d y ) → y ≡ x → ltd ≅ ltd1
--- a/src/OPair.agda Thu Dec 22 15:10:31 2022 +0900 +++ b/src/OPair.agda Fri Dec 23 12:54:05 2022 +0900 @@ -166,8 +166,7 @@ A ⊗ B = Union ( Replace B (λ b → Replace A (λ a → < a , b > ) )) product→ : {A B a b : HOD} → A ∋ a → B ∋ b → ( A ⊗ B ) ∋ < a , b > -product→ {A} {B} {a} {b} A∋a B∋b = λ t → t (& (Replace A (λ a → < a , b >))) - ⟪ lemma1 , subst (λ k → odef k (& < a , b >)) (sym *iso) lemma2 ⟫ where +product→ {A} {B} {a} {b} A∋a B∋b = record { owner = _ ; ao = lemma1 ; ox = subst (λ k → odef k _) (sym *iso) lemma2 } where lemma1 : odef (Replace B (λ b₁ → Replace A (λ a₁ → < a₁ , b₁ >))) (& (Replace A (λ a₁ → < a₁ , b >))) lemma1 = replacement← B b B∋b lemma2 : odef (Replace A (λ a₁ → < a₁ , b >)) (& < a , b >)
--- a/src/PFOD.agda Thu Dec 22 15:10:31 2022 +0900 +++ b/src/PFOD.agda Fri Dec 23 12:54:05 2022 +0900 @@ -130,8 +130,6 @@ ω→2f≡i1 X i iω lt eq with ODC.∋-p O X (nat→ω (ω→nat i iω)) ω→2f≡i1 X i iω lt eq | yes p = subst (λ k → X ∋ k ) (nat→ω-iso iω) p -open _⊆_ - -- someday ... -- postulate -- ω→2f-iso : (X : HOD) → ( lt : ω→2 ∋ X ) → fω→2 ( ω→2f X lt ) =h= X
--- a/src/filter.agda Thu Dec 22 15:10:31 2022 +0900 +++ b/src/filter.agda Fri Dec 23 12:54:05 2022 +0900 @@ -57,22 +57,20 @@ proper : ¬ (filter F ∋ od∅) ultra : {p : HOD } → L ∋ p → L ∋ ( P ＼ p) → ( filter F ∋ p ) ∨ ( filter F ∋ ( P ＼ p) ) -open _⊆_ - ∈-filter : {L P p : HOD} → {LP : L ⊆ Power P} → (F : Filter LP ) → filter F ∋ p → L ∋ p -∈-filter {L} {p} {LP} F lt = incl ( f⊆L F) lt +∈-filter {L} {p} {LP} F lt = ( f⊆L F) lt ⊆-filter : {L P p q : HOD } → {LP : L ⊆ Power P } → (F : Filter LP) → L ∋ q → q ⊆ P -⊆-filter {L} {P} {p} {q} {LP} F lt = power→⊆ P q ( incl LP lt ) +⊆-filter {L} {P} {p} {q} {LP} F lt = power→⊆ P q ( LP lt ) ∪-lemma1 : {L p q : HOD } → (p ∪ q) ⊆ L → p ⊆ L -∪-lemma1 {L} {p} {q} lt = record { incl = λ {x} p∋x → incl lt (case1 p∋x) } +∪-lemma1 {L} {p} {q} lt p∋x = lt (case1 p∋x) ∪-lemma2 : {L p q : HOD } → (p ∪ q) ⊆ L → q ⊆ L -∪-lemma2 {L} {p} {q} lt = record { incl = λ {x} p∋x → incl lt (case2 p∋x) } +∪-lemma2 {L} {p} {q} lt p∋x = lt (case2 p∋x) q∩q⊆q : {p q : HOD } → (q ∩ p) ⊆ q -q∩q⊆q = record { incl = λ lt → proj1 lt } +q∩q⊆q lt = proj1 lt open HOD @@ -120,16 +118,16 @@ → (F : Filter LP) → filter F ∋ P → prime-filter F → ultra-filter F filter-lemma2 {P} {L} LP Lm F f∋P prime = record { proper = prime-filter.proper prime - ; ultra = λ {p} L∋p _ → prime-filter.prime prime L∋p (Lm L∋p) (lemma10 L∋p (incl (f⊆L F) f∋P) ) (lemma p (p⊆L L∋p )) + ; ultra = λ {p} L∋p _ → prime-filter.prime prime L∋p (Lm L∋p) (lemma10 L∋p ((f⊆L F) f∋P) ) (lemma p (p⊆L L∋p )) } where open _==_ p⊆L : {p : HOD} → L ∋ p → p ⊆ P - p⊆L {p} lt = power→⊆ P p ( incl LP lt ) + p⊆L {p} lt = power→⊆ P p ( LP lt ) p+1-p=1 : {p : HOD} → p ⊆ P → P =h= (p ∪ (P ＼ p)) eq→ (p+1-p=1 {p} p⊆P) {x} lt with ODC.decp O (odef p x) eq→ (p+1-p=1 {p} p⊆P) {x} lt | yes p∋x = case1 p∋x eq→ (p+1-p=1 {p} p⊆P) {x} lt | no ¬p = case2 ⟪ lt , ¬p ⟫ - eq← (p+1-p=1 {p} p⊆P) {x} ( case1 p∋x ) = subst (λ k → odef P k ) &iso (incl p⊆P ( subst (λ k → odef p k) (sym &iso) p∋x )) + eq← (p+1-p=1 {p} p⊆P) {x} ( case1 p∋x ) = subst (λ k → odef P k ) &iso (p⊆P ( subst (λ k → odef p k) (sym &iso) p∋x )) eq← (p+1-p=1 {p} p⊆P) {x} ( case2 ¬p ) = proj1 ¬p lemma : (p : HOD) → p ⊆ P → filter F ∋ (p ∪ (P ＼ p)) lemma p p⊆P = subst (λ k → filter F ∋ k ) (==→o≡ (p+1-p=1 {p} p⊆P)) f∋P @@ -187,7 +185,7 @@ ... | yes y = case1 y ... | no np with ∋-p (filter mf) (P ＼ p) ... | yes y = case2 y - ... | no n-p = ⊥-elim (MaximumFilter.is-maximum mx FisFilter FisProper {!!} record { incl = FisGreater } ) where + ... | no n-p = ⊥-elim (MaximumFilter.is-maximum mx FisFilter FisProper {!!} ? ) where Y : (y : Ordinal) → (my : odef (filter mf) y ) → HOD Y y my = record { od = record { def = λ x → (x ≡ y) ∨ (x ≡ & p) } ; odmax = & L ; <odmax = {!!} } F : HOD @@ -225,21 +223,18 @@ F∋p : filter F ∋ p F∋p = proj1 (ODC.x∋minimal O GT GT≠∅) F∋-p : filter F ∋ ( P ＼ p ) - F∋-p = incl U⊆F U∋-p + F∋-p = U⊆F U∋-p f0 : filter F ∋ od∅ f0 = subst (λ k → odef (filter F) k ) (trans (cong (&) ∩-comm) (cong (&) [a-b]∩b=0 ) ) ( filter2 F F∋p F∋-p ( CAP {!!} {!!}) ) -_⊆'_ : ( A B : HOD ) → Set n -_⊆'_ A B = {x : Ordinal } → odef A x → odef B x - import zorn -open zorn O _⊆'_ hiding ( _⊆'_ ) +open zorn O _⊆_ open import Relation.Binary.Structures MaximumSubset : {L P : HOD} - → o∅ o< & L → o∅ o< & P → P ⊆' L - → (PO : IsStrictPartialOrder _≡_ _⊆'_ ) + → o∅ o< & L → o∅ o< & P → P ⊆ L + → (PO : IsStrictPartialOrder _≡_ _⊆_ ) → ( (B : HOD) → B ⊆ P → IsTotalOrderSet PO B → SUP PO P B ) → Maximal PO P MaximumSubset {L} {P} 0<L 0<P P⊆L PO C = Zorn-lemma PO 0<P {!!}
--- a/src/generic-filter.agda Thu Dec 22 15:10:31 2022 +0900 +++ b/src/generic-filter.agda Fri Dec 23 12:54:05 2022 +0900 @@ -125,36 +125,35 @@ open import Data.Nat.Properties open import nat -open _⊆_ p-monotonic1 : (L p : HOD ) (C : CountableModel ) → {n : Nat} → (* (find-p L C (Suc n) (& p))) ⊆ (* (find-p L C n (& p))) -p-monotonic1 L p C {n} with is-o∅ (& (PGHOD n L C (find-p L C n (& p)))) -... | yes y = refl-⊆ -... | no not = record { incl = λ {x} lt → proj2 (proj2 fmin∈PGHOD) (& x) lt } where +p-monotonic1 L p C {n} {x} with is-o∅ (& (PGHOD n L C (find-p L C n (& p)))) +... | yes y = refl-⊆ {* (find-p L C n (& p))} +... | no not = λ lt → proj2 (proj2 fmin∈PGHOD) _ lt where fmin : HOD fmin = ODC.minimal O (PGHOD n L C (find-p L C n (& p))) (λ eq → not (=od∅→≡o∅ eq)) fmin∈PGHOD : PGHOD n L C (find-p L C n (& p)) ∋ fmin fmin∈PGHOD = ODC.x∋minimal O (PGHOD n L C (find-p L C n (& p))) (λ eq → not (=od∅→≡o∅ eq)) p-monotonic : (L p : HOD ) (C : CountableModel ) → {n m : Nat} → n ≤ m → (* (find-p L C m (& p))) ⊆ (* (find-p L C n (& p))) -p-monotonic L p C {Zero} {Zero} n≤m = refl-⊆ -p-monotonic L p C {Zero} {Suc m} z≤n = trans-⊆ (p-monotonic1 L p C {m} ) (p-monotonic L p C {Zero} {m} z≤n ) +p-monotonic L p C {Zero} {Zero} n≤m = refl-⊆ {* (find-p L C Zero (& p))} +p-monotonic L p C {Zero} {Suc m} z≤n lt = (p-monotonic L p C {Zero} {m} z≤n ) (p-monotonic1 L p C {m} lt ) p-monotonic L p C {Suc n} {Suc m} (s≤s n≤m) with <-cmp n m -... | tri< a ¬b ¬c = trans-⊆ (p-monotonic1 L p C {m}) (p-monotonic L p C {Suc n} {m} a) -... | tri≈ ¬a refl ¬c = refl-⊆ +... | tri< a ¬b ¬c = λ lt → (p-monotonic L p C {Suc n} {m} a) (p-monotonic1 L p C {m} lt ) +... | tri≈ ¬a refl ¬c = λ x → x ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> n≤m c ) -P-GenericFilter : (P L p0 : HOD ) → (LP : L ⊆ Power P) → L ∋ p0 → (C : CountableModel ) → GenericFilter LP ( ctl-M C ) +P-GenericFilter : (P L p0 : HOD ) → (LP : L ⊆ Power P) → L ∋ p0 → (C : CountableModel ) → GenericFilter {L} {P} LP ( ctl-M C ) P-GenericFilter P L p0 L⊆PP Lp0 C = record { genf = record { filter = PDHOD L p0 C ; f⊆L = f⊆PL ; filter1 = λ L∋q PD∋p p⊆q → f1 L∋q PD∋p p⊆q ; filter2 = f2 } ; generic = fdense } where f⊆PL : PDHOD L p0 C ⊆ L - f⊆PL = record { incl = λ {x} lt → x∈PP lt } + f⊆PL lt = x∈PP lt f1 : {p q : HOD} → L ∋ q → PDHOD L p0 C ∋ p → p ⊆ q → PDHOD L p0 C ∋ q f1 {p} {q} L∋q PD∋p p⊆q = record { gr = gr PD∋p ; pn<gr = f04 ; x∈PP = L∋q } where f04 : (y : Ordinal) → odef (* (find-p L C (gr PD∋p) (& p0))) y → odef (* (& q)) y - f04 y lt1 = subst₂ (λ j k → odef j k ) (sym *iso) &iso (incl p⊆q (subst₂ (λ j k → odef k j ) (sym &iso) *iso ( pn<gr PD∋p y lt1 ))) + f04 y lt1 = subst₂ (λ j k → odef j k ) (sym *iso) &iso (p⊆q (subst₂ (λ j k → odef k j ) (sym &iso) *iso ( pn<gr PD∋p y lt1 ))) -- odef (* (find-p P C (gr PD∋p) (& p0))) y → odef (* (& q)) y f2 : {p q : HOD} → PDHOD L p0 C ∋ p → PDHOD L p0 C ∋ q → L ∋ (p ∩ q) → PDHOD L p0 C ∋ (p ∩ q) f2 {p} {q} PD∋p PD∋q L∋pq with <-cmp (gr PD∋q) (gr PD∋p) @@ -162,7 +161,7 @@ f3 : (y : Ordinal) → odef (* (find-p L C (gr PD∋p) (& p0))) y → odef (p ∩ q) y f3 y lt = ⟪ subst (λ k → odef k y) *iso (pn<gr PD∋p y lt) , subst (λ k → odef k y) *iso (pn<gr PD∋q y (f5 lt)) ⟫ where f5 : odef (* (find-p L C (gr PD∋p) (& p0))) y → odef (* (find-p L C (gr PD∋q) (& p0))) y - f5 lt = subst (λ k → odef (* (find-p L C (gr PD∋q) (& p0))) k ) &iso ( incl (p-monotonic L p0 C {gr PD∋q} {gr PD∋p} (<to≤ a)) + f5 lt = subst (λ k → odef (* (find-p L C (gr PD∋q) (& p0))) k ) &iso ( (p-monotonic L p0 C {gr PD∋q} {gr PD∋p} (<to≤ a)) (subst (λ k → odef (* (find-p L C (gr PD∋p) (& p0))) k ) (sym &iso) lt) ) ... | tri≈ ¬a refl ¬c = record { gr = gr PD∋p ; pn<gr = λ y lt → subst (λ k → odef k y ) (sym *iso) (f4 y lt) ; x∈PP = L∋pq } where f4 : (y : Ordinal) → odef (* (find-p L C (gr PD∋p) (& p0))) y → odef (p ∩ q) y @@ -171,7 +170,7 @@ f3 : (y : Ordinal) → odef (* (find-p L C (gr PD∋q) (& p0))) y → odef (p ∩ q) y f3 y lt = ⟪ subst (λ k → odef k y) *iso (pn<gr PD∋p y (f5 lt)), subst (λ k → odef k y) *iso (pn<gr PD∋q y lt) ⟫ where f5 : odef (* (find-p L C (gr PD∋q) (& p0))) y → odef (* (find-p L C (gr PD∋p) (& p0))) y - f5 lt = subst (λ k → odef (* (find-p L C (gr PD∋p) (& p0))) k ) &iso ( incl (p-monotonic L p0 C {gr PD∋p} {gr PD∋q} (<to≤ c)) + f5 lt = subst (λ k → odef (* (find-p L C (gr PD∋p) (& p0))) k ) &iso ( (p-monotonic L p0 C {gr PD∋p} {gr PD∋q} (<to≤ c)) (subst (λ k → odef (* (find-p L C (gr PD∋q) (& p0))) k ) (sym &iso) lt) ) fdense : (D : Dense L⊆PP ) → (ctl-M C ) ∋ Dense.dense D → ¬ (filter.Dense.dense D ∩ PDHOD L p0 C) ≡ od∅ fdense D MD eq0 = ⊥-elim ( ∅< {Dense.dense D ∩ PDHOD L p0 C} fd01 (≡od∅→=od∅ eq0 )) where @@ -204,11 +203,11 @@ fd11 : Ordinal fd11 = & ( dense-f D fd12 ) fd13 : L ∋ ( dense-f D fd12 ) - fd13 = incl (d⊆P D) ( dense-d D fd12 ) + fd13 = (d⊆P D) ( dense-d D fd12 ) fd14 : (* (ctl→ C an)) ∋ ( dense-f D fd12 ) fd14 = subst (λ k → odef k (& ( dense-f D fd12 ) )) d=an ( dense-d D fd12 ) fd15 : (y : Ordinal) → odef (* (& (dense-f D fd12))) y → odef (* (find-p L C an (& p0))) y - fd15 y lt = subst (λ k → odef (* (find-p L C an (& p0))) k ) &iso ( incl (dense-p D fd12 ) fd16 ) where + fd15 y lt = subst (λ k → odef (* (find-p L C an (& p0))) k ) &iso ( (dense-p D fd12 ) fd16 ) where fd16 : odef (dense-f D fd12) (& ( * y)) fd16 = subst₂ (λ j k → odef j k ) (*iso) (sym &iso) lt fd10 : PGHOD an L C (find-p L C an (& p0)) =h= od∅ @@ -243,7 +242,7 @@ -- val x G = { val y G | ∃ p → G ∋ p → x ∋ < y , p > } -- -record valR (x : HOD) {P L : HOD} {LP : L ⊆ Power P} (C : CountableModel ) (G : GenericFilter LP (ctl-M C) ) : Set (suc n) where +record valR (x : HOD) {P L : HOD} {LP : L ⊆ Power P} (C : CountableModel ) (G : GenericFilter {L} {P} LP (ctl-M C) ) : Set (suc n) where field valx : HOD @@ -254,7 +253,7 @@ is-val : odef (* ox) ( & < * oy , * op > ) val : (x : HOD) {P L : HOD } {LP : L ⊆ Power P} - → (G : GenericFilter LP {!!} ) + → (G : GenericFilter {L} {P} LP {!!} ) → HOD val x G = TransFinite {λ x → HOD } ind (& x) where ind : (x : Ordinal) → ((y : Ordinal) → y o< x → HOD) → HOD
--- a/src/partfunc.agda Thu Dec 22 15:10:31 2022 +0900 +++ b/src/partfunc.agda Fri Dec 23 12:54:05 2022 +0900 @@ -202,6 +202,22 @@ finite3cov (just y ∷ x) = just y ∷ finite3cov x finite3cov (nothing ∷ x) = just i0 ∷ finite3cov x +record F-Filter {n : Level} (L : Set n) (PL : (L → Set n) → Set n) ( _⊆_ : L → L → Set n) (_∩_ : L → L → L ) : Set (suc n) where + field + filter : L → Set n + f⊆P : PL filter + filter1 : { p q : L } → PL (λ x → q ⊆ x ) → filter p → p ⊆ q → filter q + filter2 : { p q : L } → filter p → filter q → filter (p ∩ q) + +record F-Dense {n : Level} (L : Set n) (PL : (L → Set n) → Set n) ( _⊆_ : L → L → Set n) (_∩_ : L → L → L ) : Set (suc n) where + field + dense : L → Set n + d⊆P : PL dense + dense-f : L → L + dense-d : { p : L} → PL (λ x → p ⊆ x ) → dense ( dense-f p ) + dense-p : { p : L} → PL (λ x → p ⊆ x ) → p ⊆ (dense-f p) + + Dense-3 : F-Dense (List (Maybe Two) ) (λ x → One) _3⊆_ _3∩_ Dense-3 = record { dense = λ x → Finite3b x ≡ true
--- a/src/zorn.agda Thu Dec 22 15:10:31 2022 +0900 +++ b/src/zorn.agda Fri Dec 23 12:54:05 2022 +0900 @@ -4,7 +4,7 @@ open import Relation.Binary open import Relation.Binary.Core open import Relation.Binary.PropositionalEquality -import OD hiding ( _⊆_ ) +import OD module zorn {n : Level } (O : Ordinals {n}) (_<_ : (x y : OD.HOD O ) → Set n ) (PO : IsStrictPartialOrder _≡_ _<_ ) where -- @@ -218,9 +218,6 @@ IsTotalOrderSet : ( A : HOD ) → Set (Level.suc n) IsTotalOrderSet A = {a b : HOD} → odef A (& a) → odef A (& b) → Tri (a < b) (a ≡ b) (b < a ) -_⊆_ : ( A B : HOD ) → Set n -_⊆_ A B = {x : Ordinal } → odef A x → odef B x - ⊆-IsTotalOrderSet : { A B : HOD } → B ⊆ A → IsTotalOrderSet A → IsTotalOrderSet B ⊆-IsTotalOrderSet {A} {B} B⊆A T ax ay = T (B⊆A ax) (B⊆A ay)