comparison filter.agda @ 329:5544f4921a44

...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 05 Jul 2020 12:32:09 +0900
parents b012a915bbb5
children 12071f79f3cf
comparison
equal deleted inserted replaced
328:72f3e3b44c27 329:5544f4921a44
27 open _∧_ 27 open _∧_
28 open _∨_ 28 open _∨_
29 open Bool 29 open Bool
30 30
31 -- Kunen p.76 and p.53, we use ⊆ 31 -- Kunen p.76 and p.53, we use ⊆
32 record Filter ( L : OD ) : Set (suc n) where 32 record Filter ( L : HOD ) : Set (suc n) where
33 field 33 field
34 filter : OD 34 filter : HOD
35 f⊆PL : filter ⊆ Power L 35 f⊆PL : filter ⊆ Power L
36 filter1 : { p q : OD } → q ⊆ L → filter ∋ p → p ⊆ q → filter ∋ q 36 filter1 : { p q : HOD } → q ⊆ L → filter ∋ p → p ⊆ q → filter ∋ q
37 filter2 : { p q : OD } → filter ∋ p → filter ∋ q → filter ∋ (p ∩ q) 37 filter2 : { p q : HOD } → filter ∋ p → filter ∋ q → filter ∋ (p ∩ q)
38 38
39 open Filter 39 open Filter
40 40
41 record prime-filter { L : OD } (P : Filter L) : Set (suc (suc n)) where 41 record prime-filter { L : HOD } (P : Filter L) : Set (suc (suc n)) where
42 field 42 field
43 proper : ¬ (filter P ∋ od∅) 43 proper : ¬ (filter P ∋ od∅)
44 prime : {p q : OD } → filter P ∋ (p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q ) 44 prime : {p q : HOD } → filter P ∋ (p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q )
45 45
46 record ultra-filter { L : OD } (P : Filter L) : Set (suc (suc n)) where 46 record ultra-filter { L : HOD } (P : Filter L) : Set (suc (suc n)) where
47 field 47 field
48 proper : ¬ (filter P ∋ od∅) 48 proper : ¬ (filter P ∋ od∅)
49 ultra : {p : OD } → p ⊆ L → ( filter P ∋ p ) ∨ ( filter P ∋ ( L \ p) ) 49 ultra : {p : HOD } → p ⊆ L → ( filter P ∋ p ) ∨ ( filter P ∋ ( L \ p) )
50 50
51 open _⊆_ 51 open _⊆_
52 52
53 trans-⊆ : { A B C : OD} → A ⊆ B → B ⊆ C → A ⊆ C 53 trans-⊆ : { A B C : HOD} → A ⊆ B → B ⊆ C → A ⊆ C
54 trans-⊆ A⊆B B⊆C = record { incl = λ x → incl B⊆C (incl A⊆B x) } 54 trans-⊆ A⊆B B⊆C = record { incl = λ x → incl B⊆C (incl A⊆B x) }
55 55
56 power→⊆ : ( A t : OD) → Power A ∋ t → t ⊆ A 56 power→⊆ : ( A t : HOD) → Power A ∋ t → t ⊆ A
57 power→⊆ A t PA∋t = record { incl = λ {x} t∋x → ODC.double-neg-eilm O (t1 t∋x) } where 57 power→⊆ A t PA∋t = record { incl = λ {x} t∋x → HODC.double-neg-eilm O (t1 t∋x) } where
58 t1 : {x : OD } → t ∋ x → ¬ ¬ (A ∋ x) 58 t1 : {x : HOD } → t ∋ x → ¬ ¬ (A ∋ x)
59 t1 = zf.IsZF.power→ isZF A t PA∋t 59 t1 = zf.IsZF.power→ isZF A t PA∋t
60 60
61 ∈-filter : {L p : OD} → (P : Filter L ) → filter P ∋ p → p ⊆ L 61 ∈-filter : {L p : HOD} → (P : Filter L ) → filter P ∋ p → p ⊆ L
62 ∈-filter {L} {p} P lt = power→⊆ L p ( incl (f⊆PL P) lt ) 62 ∈-filter {L} {p} P lt = power→⊆ L p ( incl (f⊆PL P) lt )
63 63
64 ∪-lemma1 : {L p q : OD } → (p ∪ q) ⊆ L → p ⊆ L 64 ∪-lemma1 : {L p q : HOD } → (p ∪ q) ⊆ L → p ⊆ L
65 ∪-lemma1 {L} {p} {q} lt = record { incl = λ {x} p∋x → incl lt (case1 p∋x) } 65 ∪-lemma1 {L} {p} {q} lt = record { incl = λ {x} p∋x → incl lt (case1 p∋x) }
66 66
67 ∪-lemma2 : {L p q : OD } → (p ∪ q) ⊆ L → q ⊆ L 67 ∪-lemma2 : {L p q : HOD } → (p ∪ q) ⊆ L → q ⊆ L
68 ∪-lemma2 {L} {p} {q} lt = record { incl = λ {x} p∋x → incl lt (case2 p∋x) } 68 ∪-lemma2 {L} {p} {q} lt = record { incl = λ {x} p∋x → incl lt (case2 p∋x) }
69 69
70 q∩q⊆q : {p q : OD } → (q ∩ p) ⊆ q 70 q∩q⊆q : {p q : HOD } → (q ∩ p) ⊆ q
71 q∩q⊆q = record { incl = λ lt → proj1 lt } 71 q∩q⊆q = record { incl = λ lt → proj1 lt }
72 72
73 ----- 73 -----
74 -- 74 --
75 -- ultra filter is prime 75 -- ultra filter is prime
76 -- 76 --
77 77
78 filter-lemma1 : {L : OD} → (P : Filter L) → ∀ {p q : OD } → ultra-filter P → prime-filter P 78 filter-lemma1 : {L : HOD} → (P : Filter L) → ∀ {p q : HOD } → ultra-filter P → prime-filter P
79 filter-lemma1 {L} P u = record { 79 filter-lemma1 {L} P u = record {
80 proper = ultra-filter.proper u 80 proper = ultra-filter.proper u
81 ; prime = lemma3 81 ; prime = lemma3
82 } where 82 } where
83 lemma3 : {p q : OD} → filter P ∋ (p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q ) 83 lemma3 : {p q : HOD} → filter P ∋ (p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q )
84 lemma3 {p} {q} lt with ultra-filter.ultra u (∪-lemma1 (∈-filter P lt) ) 84 lemma3 {p} {q} lt with ultra-filter.ultra u (∪-lemma1 (∈-filter P lt) )
85 ... | case1 p∈P = case1 p∈P 85 ... | case1 p∈P = case1 p∈P
86 ... | case2 ¬p∈P = case2 (filter1 P {q ∩ (L \ p)} (∪-lemma2 (∈-filter P lt)) lemma7 lemma8) where 86 ... | case2 ¬p∈P = case2 (filter1 P {q ∩ (L \ p)} (∪-lemma2 (∈-filter P lt)) lemma7 lemma8) where
87 lemma5 : ((p ∪ q ) ∩ (L \ p)) == (q ∩ (L \ p)) 87 lemma5 : ((p ∪ q ) ∩ (L \ p)) == (q ∩ (L \ p))
88 lemma5 = record { eq→ = λ {x} lt → record { proj1 = lemma4 x lt ; proj2 = proj2 lt } 88 lemma5 = record { eq→ = λ {x} lt → record { proj1 = lemma4 x lt ; proj2 = proj2 lt }
102 ----- 102 -----
103 -- 103 --
104 -- if Filter contains L, prime filter is ultra 104 -- if Filter contains L, prime filter is ultra
105 -- 105 --
106 106
107 filter-lemma2 : {L : OD} → (P : Filter L) → filter P ∋ L → prime-filter P → ultra-filter P 107 filter-lemma2 : {L : HOD} → (P : Filter L) → filter P ∋ L → prime-filter P → ultra-filter P
108 filter-lemma2 {L} P f∋L prime = record { 108 filter-lemma2 {L} P f∋L prime = record {
109 proper = prime-filter.proper prime 109 proper = prime-filter.proper prime
110 ; ultra = λ {p} p⊆L → prime-filter.prime prime (lemma p p⊆L) 110 ; ultra = λ {p} p⊆L → prime-filter.prime prime (lemma p p⊆L)
111 } where 111 } where
112 open _==_ 112 open _==_
113 p+1-p=1 : {p : OD} → p ⊆ L → L == (p ∪ (L \ p)) 113 p+1-p=1 : {p : HOD} → p ⊆ L → L == (p ∪ (L \ p))
114 eq→ (p+1-p=1 {p} p⊆L) {x} lt with ODC.decp O (def p x) 114 eq→ (p+1-p=1 {p} p⊆L) {x} lt with HODC.decp O (def p x)
115 eq→ (p+1-p=1 {p} p⊆L) {x} lt | yes p∋x = case1 p∋x 115 eq→ (p+1-p=1 {p} p⊆L) {x} lt | yes p∋x = case1 p∋x
116 eq→ (p+1-p=1 {p} p⊆L) {x} lt | no ¬p = case2 (record { proj1 = lt ; proj2 = ¬p }) 116 eq→ (p+1-p=1 {p} p⊆L) {x} lt | no ¬p = case2 (record { proj1 = lt ; proj2 = ¬p })
117 eq← (p+1-p=1 {p} p⊆L) {x} ( case1 p∋x ) = subst (λ k → def L k ) diso (incl p⊆L ( subst (λ k → def p k) (sym diso) p∋x )) 117 eq← (p+1-p=1 {p} p⊆L) {x} ( case1 p∋x ) = subst (λ k → def L k ) diso (incl p⊆L ( subst (λ k → def p k) (sym diso) p∋x ))
118 eq← (p+1-p=1 {p} p⊆L) {x} ( case2 ¬p ) = proj1 ¬p 118 eq← (p+1-p=1 {p} p⊆L) {x} ( case2 ¬p ) = proj1 ¬p
119 lemma : (p : OD) → p ⊆ L → filter P ∋ (p ∪ (L \ p)) 119 lemma : (p : HOD) → p ⊆ L → filter P ∋ (p ∪ (L \ p))
120 lemma p p⊆L = subst (λ k → filter P ∋ k ) (==→o≡ (p+1-p=1 p⊆L)) f∋L 120 lemma p p⊆L = subst (λ k → filter P ∋ k ) (==→o≡ (p+1-p=1 p⊆L)) f∋L
121 121
122 record Dense (P : OD ) : Set (suc n) where 122 record Dense (P : HOD ) : Set (suc n) where
123 field 123 field
124 dense : OD 124 dense : HOD
125 incl : dense ⊆ P 125 incl : dense ⊆ P
126 dense-f : OD → OD 126 dense-f : HOD → HOD
127 dense-d : { p : OD} → P ∋ p → dense ∋ dense-f p 127 dense-d : { p : HOD} → P ∋ p → dense ∋ dense-f p
128 dense-p : { p : OD} → P ∋ p → p ⊆ (dense-f p) 128 dense-p : { p : HOD} → P ∋ p → p ⊆ (dense-f p)
129 129
130 -- the set of finite partial functions from ω to 2 130 -- the set of finite partial functions from ω to 2
131 -- 131 --
132 -- ph2 : Nat → Set → 2 132 -- ph2 : Nat → Set → 2
133 -- ph2 : Nat → Maybe 2 133 -- ph2 : Nat → Maybe 2
134 -- 134 --
135 -- Hω2 : Filter (Power (Power infinite)) 135 -- Hω2 : Filter (Power (Power infinite))
136 136
137 record Ideal ( L : OD ) : Set (suc n) where 137 record Ideal ( L : HOD ) : Set (suc n) where
138 field 138 field
139 ideal : OD 139 ideal : HOD
140 i⊆PL : ideal ⊆ Power L 140 i⊆PL : ideal ⊆ Power L
141 ideal1 : { p q : OD } → q ⊆ L → ideal ∋ p → q ⊆ p → ideal ∋ q 141 ideal1 : { p q : HOD } → q ⊆ L → ideal ∋ p → q ⊆ p → ideal ∋ q
142 ideal2 : { p q : OD } → ideal ∋ p → ideal ∋ q → ideal ∋ (p ∪ q) 142 ideal2 : { p q : HOD } → ideal ∋ p → ideal ∋ q → ideal ∋ (p ∪ q)
143 143
144 open Ideal 144 open Ideal
145 145
146 proper-ideal : {L : OD} → (P : Ideal L ) → {p : OD} → Set n 146 proper-ideal : {L : HOD} → (P : Ideal L ) → {p : HOD} → Set n
147 proper-ideal {L} P {p} = ideal P ∋ od∅ 147 proper-ideal {L} P {p} = ideal P ∋ od∅
148 148
149 prime-ideal : {L : OD} → Ideal L → ∀ {p q : OD } → Set n 149 prime-ideal : {L : HOD} → Ideal L → ∀ {p q : HOD } → Set n
150 prime-ideal {L} P {p} {q} = ideal P ∋ ( p ∩ q) → ( ideal P ∋ p ) ∨ ( ideal P ∋ q ) 150 prime-ideal {L} P {p} {q} = ideal P ∋ ( p ∩ q) → ( ideal P ∋ p ) ∨ ( ideal P ∋ q )
151 151