Mercurial > hg > Members > kono > Proof > ZF-in-agda
annotate BAlgbra.agda @ 423:9984cdd88da3
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sat, 01 Aug 2020 18:05:23 +0900 |
parents | 44a484f17f26 |
children | cc7909f86841 |
rev | line source |
---|---|
272
985a1af11bce
separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
1 open import Level |
985a1af11bce
separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
2 open import Ordinals |
985a1af11bce
separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
3 module BAlgbra {n : Level } (O : Ordinals {n}) where |
985a1af11bce
separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
4 |
985a1af11bce
separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
5 open import zf |
985a1af11bce
separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
6 open import logic |
985a1af11bce
separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
7 import OD |
276 | 8 import ODC |
272
985a1af11bce
separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
9 |
985a1af11bce
separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
10 open import Relation.Nullary |
985a1af11bce
separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
11 open import Relation.Binary |
985a1af11bce
separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
12 open import Data.Empty |
985a1af11bce
separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
13 open import Relation.Binary |
985a1af11bce
separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
14 open import Relation.Binary.Core |
985a1af11bce
separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
15 open import Relation.Binary.PropositionalEquality |
422 | 16 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ; _+_ to _n+_ ) |
272
985a1af11bce
separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
17 |
985a1af11bce
separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
18 open inOrdinal O |
985a1af11bce
separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
19 open OD O |
985a1af11bce
separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
20 open OD.OD |
277
d9d3654baee1
seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
276
diff
changeset
|
21 open ODAxiom odAxiom |
331 | 22 open HOD |
272
985a1af11bce
separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
23 |
985a1af11bce
separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
24 open _∧_ |
985a1af11bce
separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
25 open _∨_ |
985a1af11bce
separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
26 open Bool |
985a1af11bce
separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
27 |
360 | 28 --_∩_ : ( A B : HOD ) → HOD |
29 --A ∩ B = record { od = record { def = λ x → odef A x ∧ odef B x } ; | |
30 -- odmax = omin (odmax A) (odmax B) ; <odmax = λ y → min1 (<odmax A (proj1 y)) (<odmax B (proj2 y)) } | |
272
985a1af11bce
separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
31 |
329 | 32 _∪_ : ( A B : HOD ) → HOD |
331 | 33 A ∪ B = record { od = record { def = λ x → odef A x ∨ odef B x } ; |
34 odmax = omax (odmax A) (odmax B) ; <odmax = lemma } where | |
35 lemma : {y : Ordinal} → odef A y ∨ odef B y → y o< omax (odmax A) (odmax B) | |
36 lemma {y} (case1 a) = ordtrans (<odmax A a) (omax-x _ _) | |
37 lemma {y} (case2 b) = ordtrans (<odmax B b) (omax-y _ _) | |
272
985a1af11bce
separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
38 |
329 | 39 _\_ : ( A B : HOD ) → HOD |
331 | 40 A \ B = record { od = record { def = λ x → odef A x ∧ ( ¬ ( odef B x ) ) }; odmax = odmax A ; <odmax = λ y → <odmax A (proj1 y) } |
272
985a1af11bce
separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
41 |
329 | 42 ∪-Union : { A B : HOD } → Union (A , B) ≡ ( A ∪ B ) |
272
985a1af11bce
separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
43 ∪-Union {A} {B} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where |
331 | 44 lemma1 : {x : Ordinal} → odef (Union (A , B)) x → odef (A ∪ B) x |
272
985a1af11bce
separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
45 lemma1 {x} lt = lemma3 lt where |
422 | 46 lemma4 : {y : Ordinal} → odef (A , B) y ∧ odef (* y) x → ¬ (¬ ( odef A x ∨ odef B x) ) |
272
985a1af11bce
separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
47 lemma4 {y} z with proj1 z |
422 | 48 lemma4 {y} z | case1 refl = double-neg (case1 ( subst (λ k → odef k x ) *iso (proj2 z)) ) |
49 lemma4 {y} z | case2 refl = double-neg (case2 ( subst (λ k → odef k x ) *iso (proj2 z)) ) | |
50 lemma3 : (((u : Ordinals.ord O) → ¬ odef (A , B) u ∧ odef (* u) x) → ⊥) → odef (A ∪ B) x | |
276 | 51 lemma3 not = ODC.double-neg-eilm O (FExists _ lemma4 not) -- choice |
331 | 52 lemma2 : {x : Ordinal} → odef (A ∪ B) x → odef (Union (A , B)) x |
422 | 53 lemma2 {x} (case1 A∋x) = subst (λ k → odef (Union (A , B)) k) &iso ( IsZF.union→ isZF (A , B) (* x) A |
54 ⟪ case1 refl , d→∋ A A∋x ⟫ ) | |
55 lemma2 {x} (case2 B∋x) = subst (λ k → odef (Union (A , B)) k) &iso ( IsZF.union→ isZF (A , B) (* x) B | |
56 ⟪ case2 refl , d→∋ B B∋x ⟫ ) | |
272
985a1af11bce
separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
57 |
376 | 58 ∩-Select : { A B : HOD } → Select A ( λ x → ( A ∋ x ) ∧ ( B ∋ x ) ) ≡ ( A ∩ B ) |
272
985a1af11bce
separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
59 ∩-Select {A} {B} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where |
376 | 60 lemma1 : {x : Ordinal} → odef (Select A (λ x₁ → (A ∋ x₁) ∧ (B ∋ x₁))) x → odef (A ∩ B) x |
422 | 61 lemma1 {x} lt = ⟪ proj1 lt , subst (λ k → odef B k ) &iso (proj2 (proj2 lt)) ⟫ |
376 | 62 lemma2 : {x : Ordinal} → odef (A ∩ B) x → odef (Select A (λ x₁ → (A ∋ x₁) ∧ (B ∋ x₁))) x |
422 | 63 lemma2 {x} lt = ⟪ proj1 lt , ⟪ d→∋ A (proj1 lt) , d→∋ B (proj2 lt) ⟫ ⟫ |
272
985a1af11bce
separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
64 |
329 | 65 dist-ord : {p q r : HOD } → p ∩ ( q ∪ r ) ≡ ( p ∩ q ) ∪ ( p ∩ r ) |
272
985a1af11bce
separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
66 dist-ord {p} {q} {r} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where |
331 | 67 lemma1 : {x : Ordinal} → odef (p ∩ (q ∪ r)) x → odef ((p ∩ q) ∪ (p ∩ r)) x |
272
985a1af11bce
separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
68 lemma1 {x} lt with proj2 lt |
422 | 69 lemma1 {x} lt | case1 q∋x = case1 ⟪ proj1 lt , q∋x ⟫ |
70 lemma1 {x} lt | case2 r∋x = case2 ⟪ proj1 lt , r∋x ⟫ | |
331 | 71 lemma2 : {x : Ordinal} → odef ((p ∩ q) ∪ (p ∩ r)) x → odef (p ∩ (q ∪ r)) x |
422 | 72 lemma2 {x} (case1 p∩q) = ⟪ proj1 p∩q , case1 (proj2 p∩q ) ⟫ |
73 lemma2 {x} (case2 p∩r) = ⟪ proj1 p∩r , case2 (proj2 p∩r ) ⟫ | |
272
985a1af11bce
separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
74 |
329 | 75 dist-ord2 : {p q r : HOD } → p ∪ ( q ∩ r ) ≡ ( p ∪ q ) ∩ ( p ∪ r ) |
272
985a1af11bce
separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
76 dist-ord2 {p} {q} {r} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where |
331 | 77 lemma1 : {x : Ordinal} → odef (p ∪ (q ∩ r)) x → odef ((p ∪ q) ∩ (p ∪ r)) x |
422 | 78 lemma1 {x} (case1 cp) = ⟪ case1 cp , case1 cp ⟫ |
79 lemma1 {x} (case2 cqr) = ⟪ case2 (proj1 cqr) , case2 (proj2 cqr) ⟫ | |
331 | 80 lemma2 : {x : Ordinal} → odef ((p ∪ q) ∩ (p ∪ r)) x → odef (p ∪ (q ∩ r)) x |
272
985a1af11bce
separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
81 lemma2 {x} lt with proj1 lt | proj2 lt |
985a1af11bce
separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
82 lemma2 {x} lt | case1 cp | _ = case1 cp |
985a1af11bce
separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
83 lemma2 {x} lt | _ | case1 cp = case1 cp |
422 | 84 lemma2 {x} lt | case2 cq | case2 cr = case2 ⟪ cq , cr ⟫ |
272
985a1af11bce
separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
85 |
985a1af11bce
separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
86 record IsBooleanAlgebra ( L : Set n) |
985a1af11bce
separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
87 ( b1 : L ) |
985a1af11bce
separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
88 ( b0 : L ) |
985a1af11bce
separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
89 ( -_ : L → L ) |
985a1af11bce
separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
90 ( _+_ : L → L → L ) |
422 | 91 ( _x_ : L → L → L ) : Set (suc n) where |
272
985a1af11bce
separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
92 field |
985a1af11bce
separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
93 +-assoc : {a b c : L } → a + ( b + c ) ≡ (a + b) + c |
422 | 94 x-assoc : {a b c : L } → a x ( b x c ) ≡ (a x b) x c |
272
985a1af11bce
separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
95 +-sym : {a b : L } → a + b ≡ b + a |
422 | 96 -sym : {a b : L } → a x b ≡ b x a |
423 | 97 +-aab : {a b : L } → a + ( a x b ) ≡ a |
422 | 98 x-aab : {a b : L } → a x ( a + b ) ≡ a |
423 | 99 +-dist : {a b c : L } → a + ( b x c ) ≡ ( a x b ) + ( a x c ) |
422 | 100 x-dist : {a b c : L } → a x ( b + c ) ≡ ( a + b ) x ( a + c ) |
272
985a1af11bce
separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
101 a+0 : {a : L } → a + b0 ≡ a |
422 | 102 ax1 : {a : L } → a x b1 ≡ a |
272
985a1af11bce
separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
103 a+-a1 : {a : L } → a + ( - a ) ≡ b1 |
422 | 104 ax-a0 : {a : L } → a x ( - a ) ≡ b0 |
272
985a1af11bce
separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
105 |
985a1af11bce
separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
106 record BooleanAlgebra ( L : Set n) : Set (suc n) where |
985a1af11bce
separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
107 field |
985a1af11bce
separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
108 b1 : L |
985a1af11bce
separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
109 b0 : L |
985a1af11bce
separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
110 -_ : L → L |
422 | 111 _+_ : L → L → L |
112 _x_ : L → L → L | |
113 isBooleanAlgebra : IsBooleanAlgebra L b1 b0 -_ _+_ _x_ | |
272
985a1af11bce
separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
114 |