Mercurial > hg > Members > kono > Proof > ZF-in-agda
annotate src/BAlgebra.agda @ 1489:0dbbae768c90 default tip
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Mon, 01 Jul 2024 23:04:17 +0900 |
parents | 5dacb669f13b |
children |
rev | line source |
---|---|
1464 | 1 {-# OPTIONS --cubical-compatible --safe #-} |
431 | 2 open import Level |
3 open import Ordinals | |
1464 | 4 import HODBase |
5 import OD | |
1466 | 6 open import Relation.Nullary |
1464 | 7 module BAlgebra {n : Level } (O : Ordinals {n} ) (HODAxiom : HODBase.ODAxiom O) (ho< : OD.ODAxiom-ho< O HODAxiom ) |
1466 | 8 (L : HODBase.HOD O) (∋-p : (P : HODBase.HOD O) → OD._⊆_ O HODAxiom P L → (x : HODBase.HOD O) → Dec ( OD._∈_ O HODAxiom x P )) where |
431 | 9 |
1464 | 10 open import Relation.Binary.PropositionalEquality hiding ( [_] ) |
11 open import Data.Empty | |
12 | |
431 | 13 import OrdUtil |
14 | |
15 open Ordinals.Ordinals O | |
16 open Ordinals.IsOrdinals isOrdinal | |
1466 | 17 import ODUtil |
18 | |
19 open import logic | |
20 open import nat | |
21 | |
431 | 22 open OrdUtil O |
1466 | 23 open ODUtil O HODAxiom ho< |
431 | 24 |
25 open _∧_ | |
26 open _∨_ | |
27 open Bool | |
28 | |
1464 | 29 open HODBase._==_ |
30 | |
1466 | 31 open HODBase.ODAxiom HODAxiom |
1464 | 32 open OD O HODAxiom |
33 | |
34 | |
1466 | 35 L\L=0 : (L \ L) =h= od∅ |
36 L\L=0 = record { eq→ = lem0 ; eq← = lem1 } where | |
1123 | 37 lem0 : {x : Ordinal} → odef (L \ L) x → odef od∅ x |
38 lem0 {x} ⟪ lx , ¬lx ⟫ = ⊥-elim (¬lx lx) | |
39 lem1 : {x : Ordinal} → odef od∅ x → odef (L \ L) x | |
40 lem1 {x} lt = ⊥-elim ( ¬∅∋ (subst (λ k → odef od∅ k) (sym &iso) lt )) | |
41 | |
1485 | 42 \-cong : (P R Q S : HOD) → P =h= R → Q =h= S → (P \ Q) =h= (R \ S) |
43 eq→ (\-cong P R Q S p=r q=s) {x} ⟪ px , npq ⟫ = ⟪ eq→ p=r px , (λ lt → npq (eq← q=s lt) ) ⟫ | |
44 eq← (\-cong P R Q S p=r q=s ) {x} ⟪ rx , nrs ⟫ = ⟪ eq← p=r rx , (λ lt → nrs (eq→ q=s lt) ) ⟫ | |
1484 | 45 |
1466 | 46 L\Lx=x : {x : HOD} → x ⊆ L → (L \ ( L \ x )) =h= x |
47 L\Lx=x {x} x⊆L = record { eq→ = lem03 ; eq← = lem04 } where | |
1465 | 48 lem03 : {z : Ordinal} → odef (L \ (L \ x)) z → odef x z |
1466 | 49 lem03 {z} ⟪ Lz , Lxz ⟫ with ∋-p x x⊆L (* z) |
1465 | 50 ... | yes y = subst (λ k → odef x k ) &iso y |
1151
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
51 ... | no n = ⊥-elim ( Lxz ⟪ Lz , ( subst (λ k → ¬ odef x k ) &iso n ) ⟫ ) |
1465 | 52 lem04 : {z : Ordinal} → odef x z → odef (L \ (L \ x)) z |
1466 | 53 lem04 {z} xz with ∋-p L (λ x → x) (* z) |
1151
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
54 ... | yes y = ⟪ subst (λ k → odef L k ) &iso y , ( λ p → proj2 p xz ) ⟫ |
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
55 ... | no n = ⊥-elim ( n (subst (λ k → odef L k ) (sym &iso) ( x⊆L xz) )) |
1465 | 56 |
1466 | 57 L\0=L : (L \ od∅) =h= L |
58 L\0=L = record { eq→ = lem05 ; eq← = lem06 } where | |
1151
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
59 lem05 : {x : Ordinal} → odef (L \ od∅) x → odef L x |
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
60 lem05 {x} ⟪ Lx , _ ⟫ = Lx |
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
61 lem06 : {x : Ordinal} → odef L x → odef (L \ od∅) x |
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
62 lem06 {x} Lx = ⟪ Lx , (λ lt → ¬x<0 lt) ⟫ |
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
63 |
1466 | 64 ∨L\X : { X : HOD } → {x : Ordinal } → odef L x → odef X x ∨ odef (L \ X) x |
65 ∨L\X {X} {x} Lx with ∋-p (X ∩ L) (λ lt → proj2 lt ) (* x) | |
66 ... | yes y = case1 ( subst (λ k → odef X k ) &iso (proj1 y) ) | |
67 ... | no n = case2 ⟪ Lx , subst (λ k → ¬ odef X k) &iso (λ lt → ⊥-elim ( n ⟪ lt , subst (λ k → odef L k) (sym &iso) Lx ⟫ ) ) ⟫ | |
1182 | 68 |
1466 | 69 \-⊆ : { A B : HOD } → A ⊆ L → ( A ⊆ B → ( L \ B ) ⊆ ( L \ A )) ∧ (( L \ B ) ⊆ ( L \ A ) → A ⊆ B ) |
70 \-⊆ {A} {B} A⊆L = ⟪ ( λ a<b {x} pbx → ⟪ proj1 pbx , (λ ax → proj2 pbx (a<b ax)) ⟫ ) , lem07 ⟫ where | |
71 lem07 : (L \ B) ⊆ (L \ A) → A ⊆ B | |
72 lem07 pba {x} ax with ∋-p (B ∩ L) proj2 (* x) | |
73 ... | yes bx = subst (λ k → odef B k ) &iso (proj1 bx) | |
74 ... | no ¬bx = ⊥-elim ( proj2 ( pba ⟪ A⊆L ax , (λ bx → ¬bx ⟪ d→∋ B bx , subst (λ k → odef L k) (sym &iso) ( A⊆L ax) ⟫) ⟫ ) ax ) | |
1151
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
75 |
1466 | 76 RC\ : RCod (Power (Union L)) (λ z → L \ z ) |
77 RC\ = record { ≤COD = λ {x} lt z xz → lemm {x} lt z xz ; ψ-eq = λ {x} {y} → wdf {x} {y} } where | |
1293 | 78 lemm : {x : HOD} → (L \ x) ⊆ Power (Union L ) |
79 lemm {x} ⟪ Ly , nxy ⟫ z xz = record { owner = _ ; ao = Ly ; ox = xz } | |
1466 | 80 wdf : {x y : HOD} → x =h= y → (L \ x) =h= (L \ y) |
1465 | 81 wdf {x} {y} x=y = record { eq→ = λ {p} lxp → ⟪ proj1 lxp , (λ yp → proj2 lxp (eq← x=y yp) ) ⟫ |
1464 | 82 ; eq← = λ {p} lxp → ⟪ proj1 lxp , (λ yp → proj2 lxp (eq→ x=y yp) ) ⟫ } |
1293 | 83 |
84 | |
1464 | 85 [a-b]∩b=0 : { A B : HOD } → ((A \ B) ∩ B) =h= od∅ |
86 [a-b]∩b=0 {A} {B} = record { eq← = λ lt → ⊥-elim ( ¬∅∋ (subst (λ k → odef od∅ k) (sym &iso) lt )) | |
451 | 87 ; eq→ = λ {x} lt → ⊥-elim (proj2 (proj1 lt ) (proj2 lt)) } |
88 | |
1466 | 89 U-F=∅→F⊆U : {F U : HOD} → U ⊆ L → ((x : Ordinal) → ¬ ( odef F x ∧ ( ¬ odef U x ))) → F ⊆ U |
90 U-F=∅→F⊆U {F} {U} U⊆L not = gt02 where | |
480 | 91 gt02 : { x : Ordinal } → odef F x → odef U x |
1466 | 92 gt02 {x} fx with ∋-p U U⊆L (* x) |
480 | 93 ... | yes y = subst (λ k → odef U k ) &iso y |
94 ... | no n = ⊥-elim ( not x ⟪ fx , subst (λ k → ¬ odef U k ) &iso n ⟫ ) | |
95 | |
1464 | 96 ∪-Union : { A B : HOD } → Union (A , B) =h= ( A ∪ B ) |
1465 | 97 ∪-Union {A} {B} = ( record { eq→ = lemma4 ; eq← = lemma2 } ) where |
98 lemma4 : {x : Ordinal} → odef (Union (A , B)) x → odef (A ∪ B) x | |
1469 | 99 lemma4 {x} record { owner = owner ; ao = (case1 refl) ; ox = ox } = case1 (eq← (==-sym *iso) ox) |
100 lemma4 {x} record { owner = owner ; ao = (case2 refl) ; ox = ox } = case2 (eq← (==-sym *iso) ox) | |
431 | 101 lemma2 : {x : Ordinal} → odef (A ∪ B) x → odef (Union (A , B)) x |
1284 | 102 lemma2 {x} (case1 A∋x) = subst (λ k → odef (Union (A , B)) k) &iso ( union→ (A , B) (* x) A |
431 | 103 ⟪ case1 refl , d→∋ A A∋x ⟫ ) |
1284 | 104 lemma2 {x} (case2 B∋x) = subst (λ k → odef (Union (A , B)) k) &iso ( union→ (A , B) (* x) B |
431 | 105 ⟪ case2 refl , d→∋ B B∋x ⟫ ) |
106 | |
1465 | 107 open import zf |
108 | |
109 pred-in : (A B : HOD ) → ZPred HOD _∋_ _=h=_ (λ x → (A ∋ x) ∧ (B ∋ x)) | |
110 pred-in A B = record { ψ-cong = wdf } where | |
111 wdf : (x y : HOD) → x =h= y → ((A ∋ x) ∧ (B ∋ x)) ⇔ ((A ∋ y) ∧ (B ∋ y)) | |
112 wdf = λ x y x=y | |
113 → ⟪ (λ p → ⟪ subst (λ k → odef A k) (==→o≡ x=y) (proj1 p) | |
114 , subst (λ k → odef B k) (==→o≡ x=y) (proj2 p) ⟫ ) | |
115 , (λ p → ⟪ subst (λ k → odef A k) (sym (==→o≡ x=y)) (proj1 p) | |
116 , subst (λ k → odef B k) (sym (==→o≡ x=y)) (proj2 p) ⟫ ) ⟫ | |
117 | |
118 ∩-Select : { A B : HOD } → Select A ( λ x → ( A ∋ x ) ∧ ( B ∋ x )) (pred-in A B) =h= ( A ∩ B ) | |
1464 | 119 ∩-Select {A} {B} = record { eq→ = lemma1 ; eq← = lemma2 } where |
1465 | 120 lemma1 : {x : Ordinal} → odef (Select A (λ x₁ → (A ∋ x₁) ∧ (B ∋ x₁)) (pred-in A B) ) x → odef (A ∩ B) x |
431 | 121 lemma1 {x} lt = ⟪ proj1 lt , subst (λ k → odef B k ) &iso (proj2 (proj2 lt)) ⟫ |
1465 | 122 lemma2 : {x : Ordinal} → odef (A ∩ B) x → odef (Select A (λ x₁ → (A ∋ x₁) ∧ (B ∋ x₁)) (pred-in A B) ) x |
431 | 123 lemma2 {x} lt = ⟪ proj1 lt , ⟪ d→∋ A (proj1 lt) , d→∋ B (proj2 lt) ⟫ ⟫ |
124 | |
1464 | 125 dist-ord : {p q r : HOD } → (p ∩ ( q ∪ r )) =h= ( ( p ∩ q ) ∪ ( p ∩ r )) |
126 dist-ord {p} {q} {r} = record { eq→ = lemma1 ; eq← = lemma2 } where | |
431 | 127 lemma1 : {x : Ordinal} → odef (p ∩ (q ∪ r)) x → odef ((p ∩ q) ∪ (p ∩ r)) x |
128 lemma1 {x} lt with proj2 lt | |
1465 | 129 lemma1 {x} lt | case1 q∋x = case1 ⟪ proj1 lt , q∋x ⟫ |
130 lemma1 {x} lt | case2 r∋x = case2 ⟪ proj1 lt , r∋x ⟫ | |
431 | 131 lemma2 : {x : Ordinal} → odef ((p ∩ q) ∪ (p ∩ r)) x → odef (p ∩ (q ∪ r)) x |
1465 | 132 lemma2 {x} (case1 p∩q) = ⟪ proj1 p∩q , case1 (proj2 p∩q ) ⟫ |
133 lemma2 {x} (case2 p∩r) = ⟪ proj1 p∩r , case2 (proj2 p∩r ) ⟫ | |
431 | 134 |
1464 | 135 dist-ord2 : {p q r : HOD } → (p ∪ ( q ∩ r )) =h= ( ( p ∪ q ) ∩ ( p ∪ r )) |
136 dist-ord2 {p} {q} {r} = record { eq→ = lemma1 ; eq← = lemma2 } where | |
431 | 137 lemma1 : {x : Ordinal} → odef (p ∪ (q ∩ r)) x → odef ((p ∪ q) ∩ (p ∪ r)) x |
138 lemma1 {x} (case1 cp) = ⟪ case1 cp , case1 cp ⟫ | |
139 lemma1 {x} (case2 cqr) = ⟪ case2 (proj1 cqr) , case2 (proj2 cqr) ⟫ | |
140 lemma2 : {x : Ordinal} → odef ((p ∪ q) ∩ (p ∪ r)) x → odef (p ∪ (q ∩ r)) x | |
141 lemma2 {x} lt with proj1 lt | proj2 lt | |
142 lemma2 {x} lt | case1 cp | _ = case1 cp | |
1465 | 143 lemma2 {x} lt | _ | case1 cp = case1 cp |
144 lemma2 {x} lt | case2 cq | case2 cr = case2 ⟪ cq , cr ⟫ | |
1466 | 145 record PowerP (P : HOD) : Set (suc n) where |
146 constructor ⟦_,_⟧ | |
147 field | |
148 hod : HOD | |
149 x⊆P : hod ⊆ P | |
150 | |
431 | 151 |
1464 | 152 record IsBooleanAlgebra {n m : Level} ( L : Set n) |
1465 | 153 ( _≈_ : L → L → Set m ) |
431 | 154 ( b1 : L ) |
155 ( b0 : L ) | |
156 ( -_ : L → L ) | |
157 ( _+_ : L → L → L ) | |
1464 | 158 ( _x_ : L → L → L ) : Set (n ⊔ m) where |
431 | 159 field |
1465 | 160 +-assoc : {a b c : L } → (a + ( b + c )) ≈ ((a + b) + c) |
161 x-assoc : {a b c : L } → (a x ( b x c )) ≈ ((a x b) x c) | |
162 +-sym : {a b : L } → (a + b) ≈ (b + a) | |
163 x-sym : {a b : L } → (a x b) ≈ (b x a) | |
164 +-aab : {a b : L } → (a + ( a x b )) ≈ a | |
165 x-aab : {a b : L } → (a x ( a + b )) ≈ a | |
166 +-dist : {a b c : L } → (a + ( b x c )) ≈ (( a + b ) x ( a + c )) | |
167 x-dist : {a b c : L } → (a x ( b + c )) ≈ (( a x b ) + ( a x c )) | |
168 a+0 : {a : L } → (a + b0) ≈ a | |
169 ax1 : {a : L } → (a x b1) ≈ a | |
170 a+-a1 : {a : L } → (a + ( - a )) ≈ b1 | |
171 ax-a0 : {a : L } → (a x ( - a )) ≈ b0 | |
431 | 172 |
1464 | 173 record BooleanAlgebra {n m : Level} ( L : Set n) : Set (n ⊔ suc m) where |
431 | 174 field |
1465 | 175 _≈_ : L → L → Set m |
431 | 176 b1 : L |
177 b0 : L | |
1465 | 178 -_ : L → L |
431 | 179 _+_ : L → L → L |
180 _x_ : L → L → L | |
1465 | 181 isBooleanAlgebra : IsBooleanAlgebra L _≈_ b1 b0 -_ _+_ _x_ |
1280 | 182 |
183 | |
1466 | 184 HODBA : (P : HODBase.HOD O) (∋-p : (Q : HODBase.HOD O) → OD._⊆_ O HODAxiom Q P → ( x : HODBase.HOD O ) → Dec ( OD._∈_ O HODAxiom x Q )) |
185 → BooleanAlgebra (PowerP P) | |
186 HODBA P ∋-p = record { _≈_ = λ x y → hod x =h= hod y ; b1 = ⟦ P , (λ x → x) ⟧ ; b0 = ⟦ od∅ , (λ x → ⊥-elim (¬x<0 x)) ⟧ | |
1280 | 187 ; -_ = λ x → ⟦ P \ hod x , proj1 ⟧ |
1465 | 188 ; _+_ = λ x y → ⟦ hod x ∪ hod y , ba00 x y ⟧ ; _x_ = λ x y → ⟦ hod x ∩ hod y , (λ lt → x⊆P x (proj1 lt)) ⟧ |
1280 | 189 ; isBooleanAlgebra = record { |
1464 | 190 +-assoc = λ {a} {b} {c} → record { eq→ = ba01 a b c ; eq← = ba02 a b c } |
1465 | 191 ; x-assoc = λ {a} {b} {c} → |
192 record { eq→ = λ lt → ⟪ ⟪ proj1 lt , proj1 (proj2 lt) ⟫ , proj2 (proj2 lt) ⟫ | |
193 ; eq← = λ lt → ⟪ proj1 (proj1 lt) , ⟪ proj2 (proj1 lt) , proj2 lt ⟫ ⟫ } | |
1464 | 194 ; +-sym = λ {a} {b} → record { eq→ = λ {x} lt → ba05 {hod a} {hod b} lt ; eq← = ba05 {hod b} {hod a} } |
195 ; x-sym = λ {a} {b} → record { eq→ = λ lt → ⟪ proj2 lt , proj1 lt ⟫ ; eq← = λ lt → ⟪ proj2 lt , proj1 lt ⟫ } | |
196 ; +-aab = λ {a} {b} → record { eq→ = ba03 a b ; eq← = case1 } | |
197 ; x-aab = λ {a} {b} → record { eq→ = proj1 ; eq← = λ ax → ⟪ ax , case1 ax ⟫ } | |
1465 | 198 ; +-dist = λ {p} {q} {r} → dist-ord2 {hod p} {hod q} {hod r} |
199 ; x-dist = λ {p} {q} {r} → dist-ord {hod p} {hod q} {hod r} | |
1464 | 200 ; a+0 = λ {a} → record { eq→ = ba04 (hod a) ; eq← = case1 } |
201 ; ax1 = λ {a} → record { eq→ = proj1 ; eq← = λ ax → ⟪ ax , x⊆P a ax ⟫ } | |
202 ; a+-a1 = λ {a} → record { eq→ = ba06 a ; eq← = ba07 a } | |
203 ; ax-a0 = λ {a} → record { eq→ = ba08 a ; eq← = λ lt → ⊥-elim (¬x<0 lt) } | |
1281 | 204 } } where |
1466 | 205 open PowerP |
1281 | 206 ba00 : (x y : PowerP P ) → (hod x ∪ hod y) ⊆ P |
207 ba00 x y (case1 px) = x⊆P x px | |
208 ba00 x y (case2 py) = x⊆P y py | |
209 ba01 : (a b c : PowerP P) → {x : Ordinal} → odef (hod a) x ∨ odef (hod b ∪ hod c) x → | |
210 odef (hod a ∪ hod b) x ∨ odef (hod c) x | |
211 ba01 a b c {x} (case1 ax) = case1 (case1 ax) | |
212 ba01 a b c {x} (case2 (case1 bx)) = case1 (case2 bx) | |
213 ba01 a b c {x} (case2 (case2 cx)) = case2 cx | |
214 ba02 : (a b c : PowerP P) → {x : Ordinal} → odef (hod a ∪ hod b) x ∨ odef (hod c) x | |
1465 | 215 → odef (hod a) x ∨ odef (hod b ∪ hod c) x |
1281 | 216 ba02 a b c {x} (case1 (case1 ax)) = case1 ax |
217 ba02 a b c {x} (case1 (case2 bx)) = case2 (case1 bx) | |
218 ba02 a b c {x} (case2 cx) = case2 (case2 cx) | |
219 ba03 : (a b : PowerP P) → {x : Ordinal} → | |
1466 | 220 odef (hod a) x ∨ odef (hod a ∩ hod b) x → odef (hod a) x |
1281 | 221 ba03 a b (case1 ax) = ax |
222 ba03 a b (case2 ab) = proj1 ab | |
223 ba04 : (a : HOD) → {x : Ordinal} → odef a x ∨ odef od∅ x → odef a x | |
224 ba04 a (case1 ax) = ax | |
225 ba04 a (case2 x) = ⊥-elim (¬x<0 x) | |
1282 | 226 ba05 : {a b : HOD} {x : Ordinal} → odef a x ∨ odef b x → odef b x ∨ odef a x |
227 ba05 (case1 x) = case2 x | |
228 ba05 (case2 x) = case1 x | |
1466 | 229 ba06 : (a : PowerP P ) → { x : Ordinal} → odef (hod a) x ∨ odef (P \ hod a) x → odef P x |
1282 | 230 ba06 a {x} (case1 ax) = x⊆P a ax |
231 ba06 a {x} (case2 nax) = proj1 nax | |
1466 | 232 ba07 : (a : PowerP P ) → { x : Ordinal} → odef P x → odef (hod a) x ∨ odef (P \ hod a) x |
233 ba07 a {x} px with ∋-p (hod a) (x⊆P a) (* x) | |
1282 | 234 ... | yes y = case1 (subst (λ k → odef (hod a) k) &iso y) |
235 ... | no n = case2 ⟪ px , subst (λ k → ¬ odef (hod a) k) &iso n ⟫ | |
1466 | 236 ba08 : (a : PowerP P) → {x : Ordinal} → odef (hod a ∩ (P \ hod a)) x → odef od∅ x |
1282 | 237 ba08 a {x} ⟪ ax , ⟪ px , nax ⟫ ⟫ = ⊥-elim ( nax ax ) |
238 |