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

comparison src/filter.agda @ 457:5f8243d1d41b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 17 Mar 2022 16:40:54 +0900
parents 9207b0c3cfe9
children 882c24efdc3f
comparison
equal deleted inserted replaced
456:9207b0c3cfe9 457:5f8243d1d41b
1 {-# OPTIONS --allow-unsolved-metas #-}
2
1 open import Level 3 open import Level
2 open import Ordinals 4 open import Ordinals
3 module filter {n : Level } (O : Ordinals {n}) where 5 module filter {n : Level } (O : Ordinals {n}) where
4 6
5 open import zf 7 open import zf
57 ultra : {p : HOD } → L ∋ p → ( filter F ∋ p ) ∨ ( filter F ∋ ( P ＼ p) ) 59 ultra : {p : HOD } → L ∋ p → ( filter F ∋ p ) ∨ ( filter F ∋ ( P ＼ p) )
58 60
59 open _⊆_ 61 open _⊆_
60 62
61 ∈-filter : {L p : HOD} → (F : Filter L ) → filter F ∋ p → L ∋ p 63 ∈-filter : {L p : HOD} → (F : Filter L ) → filter F ∋ p → L ∋ p
62 ∈-filter {L} {p} F lt = {!!} -- power→⊆ L p ( incl ? lt ) 64 ∈-filter {L} {p} F lt = incl ( f⊆L F) lt
63 65
64 ∪-lemma1 : {L p q : HOD } → (p ∪ q) ⊆ L → p ⊆ L 66 ∪-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) } 67 ∪-lemma1 {L} {p} {q} lt = record { incl = λ {x} p∋x → incl lt (case1 p∋x) }
66 68
67 ∪-lemma2 : {L p q : HOD } → (p ∪ q) ⊆ L → q ⊆ L 69 ∪-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) } 70 ∪-lemma2 {L} {p} {q} lt = record { incl = λ {x} p∋x → incl lt (case2 p∋x) }
71
72 ∪-lemma3 : {L P p q : HOD } → L ⊆ Power P → L ∋ (p ∪ q) → L ∋ p
73 ∪-lemma3 = {!!}
74
75 ∪-lemma4 : {L P p q : HOD } → L ⊆ Power P → L ∋ (p ∪ q) → L ∋ q
76 ∪-lemma4 = {!!}
69 77
70 q∩q⊆q : {p q : HOD } → (q ∩ p) ⊆ q 78 q∩q⊆q : {p q : HOD } → (q ∩ p) ⊆ q
71 q∩q⊆q = record { incl = λ lt → proj1 lt } 79 q∩q⊆q = record { incl = λ lt → proj1 lt }
72 80
73 open HOD 81 open HOD
81 filter-lemma1 {P} {L} F u = record { 89 filter-lemma1 {P} {L} F u = record {
82 proper = ultra-filter.proper u 90 proper = ultra-filter.proper u
83 ; prime = lemma3 91 ; prime = lemma3
84 } where 92 } where
85 lemma3 : {p q : HOD} → filter F ∋ (p ∪ q) → ( filter F ∋ p ) ∨ ( filter F ∋ q ) 93 lemma3 : {p q : HOD} → filter F ∋ (p ∪ q) → ( filter F ∋ p ) ∨ ( filter F ∋ q )
86 lemma3 {p} {q} lt with ultra-filter.ultra u {!!} -- (∪-lemma1 (∈-filter P lt) ) 94 lemma3 {p} {q} lt with ultra-filter.ultra u (∈-filter F lt)
87 ... | case1 p∈P = case1 p∈P 95 ... | case1 p∈P = case1 {!!} -- (∪-lemma3 (ultra-filter.L⊆PP u) ? ) -- : OD.def (od (filter F)) (& p)
88 ... | case2 ¬p∈P = case2 (filter1 F {q ∩ (L ＼ p)} {!!} lemma7 lemma8) where 96 ... | case2 ¬p∈P = case2 (filter1 F {q ∩ (L ＼ p)} {!!} lemma7 lemma8) where
89 lemma5 : ((p ∪ q ) ∩ (L ＼ p)) =h= (q ∩ (L ＼ p)) 97 lemma5 : ((p ∪ q ) ∩ (L ＼ p)) =h= (q ∩ (L ＼ p))
90 lemma5 = record { eq→ = λ {x} lt → ⟪ lemma4 x lt , proj2 lt ⟫ 98 lemma5 = record { eq→ = λ {x} lt → ⟪ lemma4 x lt , proj2 lt ⟫
91 ; eq← = λ {x} lt → ⟪ case2 (proj1 lt) , proj2 lt ⟫ 99 ; eq← = λ {x} lt → ⟪ case2 (proj1 lt) , proj2 lt ⟫
92 } where 100 } where
93 lemma4 : (x : Ordinal ) → odef ((p ∪ q) ∩ (L ＼ p)) x → odef q x 101 lemma4 : (x : Ordinal ) → odef ((p ∪ q) ∩ (L ＼ p)) x → odef q x
94 lemma4 x lt with proj1 lt 102 lemma4 x lt with proj1 lt
95 lemma4 x lt | case1 px = ⊥-elim ( proj2 (proj2 lt) px ) 103 lemma4 x lt | case1 px = ⊥-elim ( proj2 (proj2 lt) px )
96 lemma4 x lt | case2 qx = qx 104 lemma4 x lt | case2 qx = qx
97 lemma6 : filter F ∋ ((p ∪ q ) ∩ (P ＼ p)) 105 lemma6 : filter F ∋ ((p ∪ q ) ∩ (P ＼ p))
98 lemma6 = filter2 F lt ¬p∈P 106 lemma6 = {!!} -- filter2 F lt ¬p∈P
99 lemma7 : filter F ∋ (q ∩ (L ＼ p)) 107 lemma7 : filter F ∋ (q ∩ (L ＼ p))
100 lemma7 = subst (λ k → filter F ∋ k ) (==→o≡ lemma5 ) {!!} 108 lemma7 = subst (λ k → filter F ∋ k ) (==→o≡ lemma5 ) {!!}
101 lemma8 : (q ∩ (L ＼ p)) ⊆ q 109 lemma8 : (q ∩ (L ＼ p)) ⊆ q
102 lemma8 = q∩q⊆q 110 lemma8 = q∩q⊆q
103 111