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

comparison filter.agda @ 270:fc3d4bc1dc5e

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 Mon, 07 Oct 2019 01:28:11 +0900
parents 30e419a2be24
children 2169d948159b
comparison
equal deleted inserted replaced
269:30e419a2be24 270:fc3d4bc1dc5e
26 A ∩ B = record { def = λ x → def A x ∧ def B x } 26 A ∩ B = record { def = λ x → def A x ∧ def B x }
27 27
28 _∪_ : ( A B : OD ) → OD 28 _∪_ : ( A B : OD ) → OD
29 A ∪ B = record { def = λ x → def A x ∨ def B x } 29 A ∪ B = record { def = λ x → def A x ∨ def B x }
30 30
31 _＼_ : ( A B : OD ) → OD
32 A ＼ B = record { def = λ x → def A x ∧ ( ¬ ( def B x ) ) }
33
31 ∪-Union : { A B : OD } → Union (A , B) ≡ ( A ∪ B ) 34 ∪-Union : { A B : OD } → Union (A , B) ≡ ( A ∪ B )
32 ∪-Union {A} {B} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where 35 ∪-Union {A} {B} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where
33 lemma1 : {x : Ordinal} → def (Union (A , B)) x → def (A ∪ B) x 36 lemma1 : {x : Ordinal} → def (Union (A , B)) x → def (A ∪ B) x
34 lemma1 {x} lt = lemma3 lt where 37 lemma1 {x} lt = lemma3 lt where
35 lemma4 : {y : Ordinal} → def (A , B) y ∧ def (ord→od y) x → ¬ (¬ ( def A x ∨ def B x) ) 38 lemma4 : {y : Ordinal} → def (A , B) y ∧ def (ord→od y) x → ¬ (¬ ( def A x ∨ def B x) )
36 lemma4 {y} z with proj1 z 39 lemma4 {y} z with proj1 z
37 lemma4 {y} z | case1 refl = double-neg (case1 ( subst (λ k → def k x ) oiso (proj2 z)) ) 40 lemma4 {y} z | case1 refl = double-neg (case1 ( subst (λ k → def k x ) oiso (proj2 z)) )
38 lemma4 {y} z | case2 refl = double-neg (case2 ( subst (λ k → def k x ) oiso (proj2 z)) ) 41 lemma4 {y} z | case2 refl = double-neg (case2 ( subst (λ k → def k x ) oiso (proj2 z)) )
39 lemma3 : (((u : Ordinals.ord O) → ¬ def (A , B) u ∧ def (ord→od u) x) → ⊥) → def (A ∪ B) x 42 lemma3 : (((u : Ordinals.ord O) → ¬ def (A , B) u ∧ def (ord→od u) x) → ⊥) → def (A ∪ B) x
40 lemma3 not = double-neg-eilm (FExists _ lemma4 not) 43 lemma3 not = double-neg-eilm (FExists _ lemma4 not) -- choice
41 lemma2 : {x : Ordinal} → def (A ∪ B) x → def (Union (A , B)) x 44 lemma2 : {x : Ordinal} → def (A ∪ B) x → def (Union (A , B)) x
42 lemma2 {x} (case1 A∋x) = subst (λ k → def (Union (A , B)) k) diso ( IsZF.union→ isZF (A , B) (ord→od x) A 45 lemma2 {x} (case1 A∋x) = subst (λ k → def (Union (A , B)) k) diso ( IsZF.union→ isZF (A , B) (ord→od x) A
43 (record { proj1 = case1 refl ; proj2 = subst (λ k → def A k) (sym diso) A∋x})) 46 (record { proj1 = case1 refl ; proj2 = subst (λ k → def A k) (sym diso) A∋x}))
44 lemma2 {x} (case2 B∋x) = subst (λ k → def (Union (A , B)) k) diso ( IsZF.union→ isZF (A , B) (ord→od x) B 47 lemma2 {x} (case2 B∋x) = subst (λ k → def (Union (A , B)) k) diso ( IsZF.union→ isZF (A , B) (ord→od x) B
45 (record { proj1 = case2 refl ; proj2 = subst (λ k → def B k) (sym diso) B∋x})) 48 (record { proj1 = case2 refl ; proj2 = subst (λ k → def B k) (sym diso) B∋x}))
71 lemma2 {x} lt with proj1 lt | proj2 lt 74 lemma2 {x} lt with proj1 lt | proj2 lt
72 lemma2 {x} lt | case1 cp | _ = case1 cp 75 lemma2 {x} lt | case1 cp | _ = case1 cp
73 lemma2 {x} lt | _ | case1 cp = case1 cp 76 lemma2 {x} lt | _ | case1 cp = case1 cp
74 lemma2 {x} lt | case2 cq | case2 cr = case2 ( record { proj1 = cq ; proj2 = cr } ) 77 lemma2 {x} lt | case2 cq | case2 cr = case2 ( record { proj1 = cq ; proj2 = cr } )
75 78
79 record IsBooleanAlgebra ( L : Set n)
80 ( b1 : L )
81 ( b0 : L )
82 ( -_ : L → L )
83 ( _+_ : L → L → L )
84 ( _*_ : L → L → L ) : Set (suc n) where
85 field
86 +-assoc : {a b c : L } → a + ( b + c ) ≡ (a + b) + c
87 *-assoc : {a b c : L } → a * ( b * c ) ≡ (a * b) * c
88 +-sym : {a b : L } → a + b ≡ b + a
89 -sym : {a b : L } → a * b ≡ b * a
90 -aab : {a b : L } → a + ( a * b ) ≡ a
91 *-aab : {a b : L } → a * ( a + b ) ≡ a
92 -dist : {a b c : L } → a + ( b * c ) ≡ ( a * b ) + ( a * c )
93 *-dist : {a b c : L } → a * ( b + c ) ≡ ( a + b ) * ( a + c )
94 a+0 : {a : L } → a + b0 ≡ a
95 a*1 : {a : L } → a * b1 ≡ a
96 a+-a1 : {a : L } → a + ( - a ) ≡ b1
97 a*-a0 : {a : L } → a * ( - a ) ≡ b0
98
99 record BooleanAlgebra ( L : Set n) : Set (suc n) where
100 field
101 b1 : L
102 b0 : L
103 -_ : L → L
104 _++_ : L → L → L
105 _**_ : L → L → L
106 isBooleanAlgebra : IsBooleanAlgebra L b1 b0 -_ _++_ _**_
107
108
76 record Filter ( L : OD ) : Set (suc n) where 109 record Filter ( L : OD ) : Set (suc n) where
77 field 110 field
78 F1 : { p q : OD } → L ∋ p → ({ x : OD} → _⊆_ p q {x} ) → L ∋ q 111 filter : OD
79 F2 : { p q : OD } → L ∋ p → L ∋ q → L ∋ (p ∩ q) 112 proper : ¬ ( filter ∋ od∅ )
113 inL : { x : OD} → _⊆_ filter L {x}
114 filter1 : { p q : OD } → ( {x : OD} → _⊆_ q L {x} ) → filter ∋ p → ({ x : OD} → _⊆_ p q {x} ) → filter ∋ q
115 filter2 : { p q : OD } → filter ∋ p → filter ∋ q → filter ∋ (p ∩ q)
80 116
81 open Filter 117 open Filter
82 118
83 proper-filter : {L : OD} → Filter L → Set n 119 L-filter : {L : OD} → (P : Filter L ) → {p : OD} → filter P ∋ p → filter P ∋ L
84 proper-filter {L} P = ¬ ( L ∋ od∅ ) 120 L-filter {L} P {p} lt = filter1 P {p} {L} {!!} lt {!!}
85 121
86 prime-filter : {L : OD} → Filter L → {p q : OD } → Set n 122 prime-filter : {L : OD} → Filter L → ∀ {p q : OD } → Set n
87 prime-filter {L} P {p} {q} = L ∋ ( p ∪ q) → ( L ∋ p ) ∨ ( L ∋ q ) 123 prime-filter {L} P {p} {q} = filter P ∋ ( p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q )
88 124
89 ultra-filter : {L : OD} → Filter L → {p : OD } → Set n 125 ultra-filter : {L : OD} → Filter L → ∀ {p : OD } → Set n
90 ultra-filter {L} P {p} = ( L ∋ p ) ∨ ( ¬ ( L ∋ p )) 126 ultra-filter {L} P {p} = L ∋ p → ( filter P ∋ p ) ∨ ( filter P ∋ ( L ＼ p) )
91 127
92 128
93 filter-lemma1 : {L : OD} → (P : Filter L) → {p q : OD } → ( (p : OD ) → ultra-filter {L} P {p} ) → prime-filter {L} P {p} {q} 129 filter-lemma1 : {L : OD} → (P : Filter L) → ∀ {p q : OD } → ( ∀ (p : OD ) → ultra-filter {L} P {p} ) → prime-filter {L} P {p} {q}
94 filter-lemma1 {L} P {p} {q} u lt with u p | u q 130 filter-lemma1 {L} P {p} {q} u lt = {!!}
95 filter-lemma1 {L} P {p} {q} u lt | case1 x | case1 y = case1 x 131
96 filter-lemma1 {L} P {p} {q} u lt | case1 x | case2 y = case1 x 132 filter-lemma2 : {L : OD} → (P : Filter L) → ( ∀ {p q : OD } → prime-filter {L} P {p} {q}) → ∀ (p : OD ) → ultra-filter {L} P {p}
97 filter-lemma1 {L} P {p} {q} u lt | case2 x | case1 y = case2 y 133 filter-lemma2 {L} P prime p with prime {!!}
98 filter-lemma1 {L} P {p} {q} u lt | case2 x | case2 y = ⊥-elim (lemma (record { proj1 = x ; proj2 = y })) where 134 ... | t = {!!}
99 lemma : ¬ ( ¬ ( L ∋ p ) ) ∧ ( ¬ ( L ∋ q ))
100 lemma = {!!}
101 135
102 generated-filter : {L : OD} → Filter L → (p : OD ) → Filter ( record { def = λ x → def L x ∨ (x ≡ od→ord p) } ) 136 generated-filter : {L : OD} → Filter L → (p : OD ) → Filter ( record { def = λ x → def L x ∨ (x ≡ od→ord p) } )
103 generated-filter {L} P p = record { 137 generated-filter {L} P p = record {
104 F1 = {!!} ; F2 = {!!} 138 filter = {!!} ; inL = {!!} ;
139 filter1 = {!!} ; filter2 = {!!}
105 } 140 }
106 141
107 record Dense (P : OD ) : Set (suc n) where 142 record Dense (P : OD ) : Set (suc n) where
108 field 143 field
109 dense : OD 144 dense : OD
120 import ordinal 155 import ordinal
121 156
122 open ordinal.C-Ordinal-with-choice 157 open ordinal.C-Ordinal-with-choice
123 158
124 Hω2 : Filter (Power (Power infinite)) 159 Hω2 : Filter (Power (Power infinite))
125 Hω2 = record { F1 = {!!} ; F2 = {!!} } 160 Hω2 = {!!}
126 161