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