Mercurial > hg > Members > kono > Proof > ZF-in-agda
view filter.agda @ 371:e75402b1f7d4
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 19 Jul 2020 16:19:24 +0900 |
parents | 1425104bb5d8 |
children | 8c3b59f583f2 |
line wrap: on
line source
open import Level open import Ordinals module filter {n : Level } (O : Ordinals {n}) where open import zf open import logic import OD open import Relation.Nullary open import Relation.Binary open import Data.Empty open import Relation.Binary open import Relation.Binary.Core open import Relation.Binary.PropositionalEquality open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) import BAlgbra open BAlgbra O open inOrdinal O open OD O open OD.OD open ODAxiom odAxiom import ODC open _∧_ open _∨_ open Bool -- Kunen p.76 and p.53, we use ⊆ record Filter ( L : HOD ) : Set (suc n) where field filter : HOD f⊆PL : filter ⊆ Power L filter1 : { p q : HOD } → q ⊆ L → filter ∋ p → p ⊆ q → filter ∋ q filter2 : { p q : HOD } → filter ∋ p → filter ∋ q → filter ∋ (p ∩ q) open Filter record prime-filter { L : HOD } (P : Filter L) : Set (suc (suc n)) where field proper : ¬ (filter P ∋ od∅) prime : {p q : HOD } → filter P ∋ (p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q ) record ultra-filter { L : HOD } (P : Filter L) : Set (suc (suc n)) where field proper : ¬ (filter P ∋ od∅) ultra : {p : HOD } → p ⊆ L → ( filter P ∋ p ) ∨ ( filter P ∋ ( L \ p) ) open _⊆_ 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) } power→⊆ : ( A t : HOD) → Power A ∋ t → t ⊆ A power→⊆ A t PA∋t = record { incl = λ {x} t∋x → ODC.double-neg-eilm O (t1 t∋x) } where t1 : {x : HOD } → t ∋ x → ¬ ¬ (A ∋ x) t1 = zf.IsZF.power→ isZF A t PA∋t ∈-filter : {L p : HOD} → (P : Filter L ) → filter P ∋ p → p ⊆ L ∈-filter {L} {p} P lt = power→⊆ L p ( incl (f⊆PL P) 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) } ∪-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) } q∩q⊆q : {p q : HOD } → (q ∩ p) ⊆ q q∩q⊆q = record { incl = λ lt → proj1 lt } open HOD ----- -- -- ultra filter is prime -- filter-lemma1 : {L : HOD} → (P : Filter L) → ∀ {p q : HOD } → ultra-filter P → prime-filter P filter-lemma1 {L} P u = record { proper = ultra-filter.proper u ; prime = lemma3 } where lemma3 : {p q : HOD} → filter P ∋ (p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q ) lemma3 {p} {q} lt with ultra-filter.ultra u (∪-lemma1 (∈-filter P lt) ) ... | case1 p∈P = case1 p∈P ... | case2 ¬p∈P = case2 (filter1 P {q ∩ (L \ p)} (∪-lemma2 (∈-filter P lt)) lemma7 lemma8) where lemma5 : ((p ∪ q ) ∩ (L \ p)) =h= (q ∩ (L \ p)) lemma5 = record { eq→ = λ {x} lt → record { proj1 = lemma4 x lt ; proj2 = proj2 lt } ; eq← = λ {x} lt → record { proj1 = case2 (proj1 lt) ; proj2 = proj2 lt } } where lemma4 : (x : Ordinal ) → odef ((p ∪ q) ∩ (L \ p)) x → odef q x lemma4 x lt with proj1 lt lemma4 x lt | case1 px = ⊥-elim ( proj2 (proj2 lt) px ) lemma4 x lt | case2 qx = qx lemma6 : filter P ∋ ((p ∪ q ) ∩ (L \ p)) lemma6 = filter2 P lt ¬p∈P lemma7 : filter P ∋ (q ∩ (L \ p)) lemma7 = subst (λ k → filter P ∋ k ) (==→o≡ lemma5 ) lemma6 lemma8 : (q ∩ (L \ p)) ⊆ q lemma8 = q∩q⊆q ----- -- -- if Filter contains L, prime filter is ultra -- filter-lemma2 : {L : HOD} → (P : Filter L) → filter P ∋ L → prime-filter P → ultra-filter P filter-lemma2 {L} P f∋L prime = record { proper = prime-filter.proper prime ; ultra = λ {p} p⊆L → prime-filter.prime prime (lemma p p⊆L) } where open _==_ p+1-p=1 : {p : HOD} → p ⊆ L → L =h= (p ∪ (L \ p)) eq→ (p+1-p=1 {p} p⊆L) {x} lt with ODC.decp O (odef p x) eq→ (p+1-p=1 {p} p⊆L) {x} lt | yes p∋x = case1 p∋x eq→ (p+1-p=1 {p} p⊆L) {x} lt | no ¬p = case2 (record { proj1 = lt ; proj2 = ¬p }) eq← (p+1-p=1 {p} p⊆L) {x} ( case1 p∋x ) = subst (λ k → odef L k ) diso (incl p⊆L ( subst (λ k → odef p k) (sym diso) p∋x )) eq← (p+1-p=1 {p} p⊆L) {x} ( case2 ¬p ) = proj1 ¬p lemma : (p : HOD) → p ⊆ L → filter P ∋ (p ∪ (L \ p)) lemma p p⊆L = subst (λ k → filter P ∋ k ) (==→o≡ (p+1-p=1 p⊆L)) f∋L record Dense (P : HOD ) : Set (suc n) where field dense : HOD incl : dense ⊆ Power P dense-f : HOD → HOD dense-d : { p : HOD} → p ⊆ P → dense ∋ dense-f p dense-p : { p : HOD} → p ⊆ P → p ⊆ (dense-f p) record Ideal ( L : HOD ) : Set (suc n) where field ideal : HOD i⊆PL : ideal ⊆ Power L ideal1 : { p q : HOD } → q ⊆ L → ideal ∋ p → q ⊆ p → ideal ∋ q ideal2 : { p q : HOD } → ideal ∋ p → ideal ∋ q → ideal ∋ (p ∪ q) open Ideal proper-ideal : {L : HOD} → (P : Ideal L ) → {p : HOD} → Set n proper-ideal {L} P {p} = ideal P ∋ od∅ prime-ideal : {L : HOD} → Ideal L → ∀ {p q : HOD } → Set n prime-ideal {L} P {p} {q} = ideal P ∋ ( p ∩ q) → ( ideal P ∋ p ) ∨ ( ideal P ∋ q ) ------- -- the set of finite partial functions from ω to 2 -- -- import OPair open OPair O data Two : Set n where i0 : Two i1 : Two record PFunc : Set (suc n) where field restrict : Nat → Set n map : (x : Nat ) → restrict x → Two open PFunc record _f⊆_ (f g : PFunc) : Set (suc n) where field extend : (x : Nat) → (fr : restrict f x ) → restrict g x feq : (x : Nat) → (fr : restrict f x ) → map f x fr ≡ map g x (extend x fr) record _f∩_ (f g : PFunc) : Set (suc n) where field pf : PFunc f< : f f⊆ pf g< : g f⊆ pf full-func : Set n full-func = Nat → Two full→PF : (Nat → Two) → PFunc full→PF f = record { restrict = λ x → One ; map = λ x _ → f x } _↑_ : (Nat → Two) → Nat → PFunc f ↑ i = record { restrict = λ x → Lift n (x ≤ i) ; map = λ x _ → f x } record gf-filter (f : Nat → Two) (p : PFunc ) : Set (suc n) where field gn : Nat f<n : p f⊆ (f ↑ gn) record F-Filter (L : Set (suc n)) (PL : (L → Set (suc n)) → Set n) ( _⊆_ : L → L → Set (suc n)) (_∩_ : L → L → L ) : Set (suc (suc n)) where field filter : L → Set (suc n) f⊆P : PL filter filter1 : { p q : L } → filter p → p ⊆ q → filter q filter2 : { p q : L } → filter p → filter q → filter (p ∩ q) GF : (Nat → Two ) → F-Filter PFunc (λ x → One) _f⊆_ {!!} GF f = record { filter = λ p → gf-filter f p ; f⊆P = OneObj ; filter1 = λ {p} {q} fp p⊆q → record { gn = {!!} ; f<n = {!!} } ; filter2 = λ {p} {q} fp fq → record { gn = {!!} ; f<n = {!!} } } ODSuc : (y : HOD) → infinite ∋ y → HOD ODSuc y lt = Union (y , (y , y)) data Hω2 : (i : Nat) ( x : Ordinal ) → Set n where hφ : Hω2 0 o∅ h0 : {i : Nat} {x : Ordinal } → Hω2 i x → Hω2 (Suc i) (od→ord (Union ((< nat→ω i , nat→ω 0 >) , ord→od x ))) h1 : {i : Nat} {x : Ordinal } → Hω2 i x → Hω2 (Suc i) (od→ord (Union ((< nat→ω i , nat→ω 1 >) , ord→od x ))) he : {i : Nat} {x : Ordinal } → Hω2 i x → Hω2 (Suc i) x record Hω2r (x : Ordinal) : Set n where field count : Nat hω2 : Hω2 count x open Hω2r HODω2 : HOD HODω2 = record { od = record { def = λ x → Hω2r x } ; odmax = next o∅ ; <odmax = odmax0 } where ω<next : {y : Ordinal} → infinite-d y → y o< next o∅ ω<next = ω<next-o∅ ho< lemma : {i j : Nat} {x : Ordinal } → od→ord (Union (< nat→ω i , nat→ω j > , ord→od x)) o< next x lemma = {!!} odmax0 : {y : Ordinal} → Hω2r y → y o< next o∅ odmax0 {y} r with hω2 r ... | hφ = x<nx ... | h0 {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) (lemma {i} {0} {x}) ... | h1 {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) (lemma {i} {1} {x}) ... | he {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) x<nx ω→2 : HOD ω→2 = Replace (Power infinite) (λ p p⊆i → Replace infinite (λ x i∋x → < x , repl p x > )) where repl : HOD → HOD → HOD repl p x with ODC.∋-p O p x ... | yes _ = nat→ω 1 ... | no _ = nat→ω 0 record _↑n (f : HOD) (ω→2∋f : ω→2 ∋ f ) : Set n where -- field -- n : HOD -- ? : Select f (λ x f∋x → ω→nat (π1 f∋x) < ω→nat n Gf : {f : HOD} → ω→2 ∋ f → HOD Gf {f} lt = Select HODω2 (λ x H∋x → {!!} ) G : (Nat → Two) → Filter HODω2 G f = record { filter = {!!} ; f⊆PL = {!!} ; filter1 = {!!} ; filter2 = {!!} } where filter0 : HOD filter0 = {!!} f⊆PL1 : filter0 ⊆ Power HODω2 f⊆PL1 = {!!} filter11 : { p q : HOD } → q ⊆ HODω2 → filter0 ∋ p → p ⊆ q → filter0 ∋ q filter11 = {!!} filter12 : { p q : HOD } → filter0 ∋ p → filter0 ∋ q → filter0 ∋ (p ∩ q) filter12 = {!!} -- the set of finite partial functions from ω to 2 Hω2f : Set (suc n) Hω2f = (Nat → Set n) → Two Hω2f→Hω2 : Hω2f → HOD Hω2f→Hω2 p = record { od = record { def = λ x → (p {!!} ≡ i0 ) ∨ (p {!!} ≡ i1 )}; odmax = {!!} ; <odmax = {!!} }