Mercurial > hg > Members > kono > Proof > ZF-in-agda
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 |