Mercurial > hg > Members > kono > Proof > ZF-in-agda

comparison filter.agda @ 294:4340ffcfa83d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
ultra-filter P → prime-filter P done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 14 Jun 2020 19:11:38 +0900
parents 9972bd4a0d6f
children 822b50091a26
comparison
equal deleted inserted replaced
293:9972bd4a0d6f 294:4340ffcfa83d
20 open inOrdinal O 20 open inOrdinal O
21 open OD O 21 open OD O
22 open OD.OD 22 open OD.OD
23 open ODAxiom odAxiom 23 open ODAxiom odAxiom
24 24
25 import ODC
26
25 open _∧_ 27 open _∧_
26 open _∨_ 28 open _∨_
27 open Bool 29 open Bool
28 30
29 -- Kunen p.76 and p.53 31 -- Kunen p.76 and p.53
39 -- should use inhabit? 41 -- should use inhabit?
40 proper-filter : {L : OD} → (P : Filter L ) → {p : OD} → Set n 42 proper-filter : {L : OD} → (P : Filter L ) → {p : OD} → Set n
41 proper-filter {L} P {p} = ¬ (filter P ∋ od∅) 43 proper-filter {L} P {p} = ¬ (filter P ∋ od∅)
42 44
43 prime-filter : {L : OD} → Filter L → ∀ {p q : OD } → Set n 45 prime-filter : {L : OD} → Filter L → ∀ {p q : OD } → Set n
44 prime-filter {L} P {p} {q} = filter P ∋ ( p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q ) 46 prime-filter {L} P {p} {q} = filter P ∋ (p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q )
45 47
46 ultra-filter : {L : OD} → Filter L → ∀ {p : OD } → Set (suc n ) 48 open _⊆_
47 ultra-filter {L} P {p} = p ⊆ L → ( filter P ∋ p ) ∨ ( filter P ∋ ( L ＼ p) )
48 49
49 filter-lemma1 : {L : OD} → (P : Filter L) → ∀ {p q : OD } → ( ∀ (p : OD ) → ultra-filter {L} P {p} ) → prime-filter {L} P {p} {q} 50 trans-⊆ : { A B C : OD} → A ⊆ B → B ⊆ C → A ⊆ C
50 filter-lemma1 {L} P {p} {q} u lt with lt 51 trans-⊆ A⊆B B⊆C = record { incl = λ x → incl B⊆C (incl A⊆B x) }
51 ... | t = {!!}
52 52
53 filter-lemma2 : {L : OD} → (P : Filter L) → ( ∀ {p q : OD } → prime-filter {L} P {p} {q}) → ∀ (p : OD ) → ultra-filter {L} P {p} 53 power→⊆ : ( A t : OD) → Power A ∋ t → t ⊆ A
54 power→⊆ A t PA∋t = record { incl = λ {x} t∋x → ODC.double-neg-eilm O (t1 t∋x) } where
55 t1 : {x : OD } → t ∋ x → ¬ ¬ (A ∋ x)
56 t1 = zf.IsZF.power→ isZF A t PA∋t
57
58 ∈-filter : {L p : OD} → (P : Filter L ) → filter P ∋ p → p ⊆ L
59 ∈-filter {L} {p} P lt = power→⊆ L p ( incl (f⊆PL P) lt )
60
61 ∪-lemma1 : {L p q : OD } → (p ∪ q) ⊆ L → p ⊆ L
62 ∪-lemma1 {L} {p} {q} lt = record { incl = λ {x} p∋x → incl lt (case1 p∋x) }
63
64 ∪-lemma2 : {L p q : OD } → (p ∪ q) ⊆ L → q ⊆ L
65 ∪-lemma2 {L} {p} {q} lt = record { incl = λ {x} p∋x → incl lt (case2 p∋x) }
66
67 q∩q⊆q : {p q : OD } → (q ∩ p) ⊆ q
68 q∩q⊆q = record { incl = λ lt → proj1 lt }
69
70 -- is-∅ : ( x : OD ) → Dec ( x ≡ od∅ )
71 -- is-∅ x with is-o∅ (od→ord x)
72 -- ... | yes eq = yes {!!}
73 -- ... | no ne = no {!!}
74
75 record ultra-filter { L : OD } (P : Filter L) : Set (suc (suc n)) where
76 field
77 proper : ¬ (filter P ∋ od∅)
78 ultra : {p : OD } → p ⊆ L → ( filter P ∋ p ) ∨ ( filter P ∋ ( L ＼ p) )
79
80 filter-lemma1 : {L : OD} → (P : Filter L) → ∀ {p q : OD } → ultra-filter P → prime-filter {L} P {p} {q}
81 filter-lemma1 {L} P {p} {q} u lt with ultra-filter.ultra u (∪-lemma1 (∈-filter P lt) )
82 ... | case1 p∈P = case1 p∈P
83 ... | case2 ¬p∈P = case2 (filter1 P {q ∩ (L ＼ p)} (∪-lemma2 (∈-filter P lt)) lemma7 lemma8) where
84 lemma5 : ((p ∪ q ) ∩ (L ＼ p)) == (q ∩ (L ＼ p))
85 lemma5 = record { eq→ = λ {x} lt → record { proj1 = lemma4 x lt ; proj2 = proj2 lt }
86 ; eq← = λ {x} lt → record { proj1 = case2 (proj1 lt) ; proj2 = proj2 lt }
87 } where
88 lemma4 : (x : Ordinal ) → def ((p ∪ q) ∩ (L ＼ p)) x → def q x
89 lemma4 x lt with proj1 lt
90 lemma4 x lt | case1 px = ⊥-elim ( proj2 (proj2 lt) px )
91 lemma4 x lt | case2 qx = qx
92 lemma6 : filter P ∋ ((p ∪ q ) ∩ (L ＼ p))
93 lemma6 = filter2 P lt ¬p∈P
94 lemma7 : filter P ∋ (q ∩ (L ＼ p))
95 lemma7 = subst (λ k → filter P ∋ k ) (==→o≡ lemma5 ) lemma6
96 lemma8 : (q ∩ (L ＼ p)) ⊆ q
97 lemma8 = q∩q⊆q
98
99 filter-lemma2 : {L : OD} → (P : Filter L) → ( ∀ {p q : OD } → prime-filter {L} P {p} {q}) → ∀ (p : OD ) → ultra-filter P
54 filter-lemma2 {L} P prime p = {!!} 100 filter-lemma2 {L} P prime p = {!!}
55 101
56 generated-filter : {L : OD} → Filter L → (p : OD ) → Filter ( record { def = λ x → def L x ∨ (x ≡ od→ord p) } ) 102 generated-filter : {L : OD} → Filter L → (p : OD ) → Filter ( record { def = λ x → def L x ∨ (x ≡ od→ord p) } )
57 generated-filter {L} P p = {!!} 103 generated-filter {L} P p = {!!}
58 104