Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison BAlgbra.agda @ 272:985a1af11bce
separate ordered pair and Boolean Algebra
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 31 Dec 2019 11:22:52 +0900 |
parents | |
children | 6f10c47e4e7a |
comparison
equal
deleted
inserted
replaced
271:2169d948159b | 272:985a1af11bce |
---|---|
1 open import Level | |
2 open import Ordinals | |
3 module BAlgbra {n : Level } (O : Ordinals {n}) where | |
4 | |
5 open import zf | |
6 open import logic | |
7 import OD | |
8 | |
9 open import Relation.Nullary | |
10 open import Relation.Binary | |
11 open import Data.Empty | |
12 open import Relation.Binary | |
13 open import Relation.Binary.Core | |
14 open import Relation.Binary.PropositionalEquality | |
15 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) | |
16 | |
17 open inOrdinal O | |
18 open OD O | |
19 open OD.OD | |
20 | |
21 open _∧_ | |
22 open _∨_ | |
23 open Bool | |
24 | |
25 _∩_ : ( A B : OD ) → OD | |
26 A ∩ B = record { def = λ x → def A x ∧ def B x } | |
27 | |
28 _∪_ : ( A B : OD ) → OD | |
29 A ∪ B = record { def = λ x → def A x ∨ def B x } | |
30 | |
31 _\_ : ( A B : OD ) → OD | |
32 A \ B = record { def = λ x → def A x ∧ ( ¬ ( def B x ) ) } | |
33 | |
34 ∪-Union : { A B : OD } → Union (A , B) ≡ ( A ∪ B ) | |
35 ∪-Union {A} {B} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where | |
36 lemma1 : {x : Ordinal} → def (Union (A , B)) x → def (A ∪ B) x | |
37 lemma1 {x} lt = lemma3 lt where | |
38 lemma4 : {y : Ordinal} → def (A , B) y ∧ def (ord→od y) x → ¬ (¬ ( def A x ∨ def B x) ) | |
39 lemma4 {y} z with proj1 z | |
40 lemma4 {y} z | case1 refl = double-neg (case1 ( 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)) ) | |
42 lemma3 : (((u : Ordinals.ord O) → ¬ def (A , B) u ∧ def (ord→od u) x) → ⊥) → def (A ∪ B) x | |
43 lemma3 not = double-neg-eilm (FExists _ lemma4 not) -- choice | |
44 lemma2 : {x : Ordinal} → def (A ∪ B) x → def (Union (A , B)) x | |
45 lemma2 {x} (case1 A∋x) = subst (λ k → def (Union (A , B)) k) diso ( IsZF.union→ isZF (A , B) (ord→od x) A | |
46 (record { proj1 = case1 refl ; proj2 = subst (λ k → def A k) (sym diso) A∋x})) | |
47 lemma2 {x} (case2 B∋x) = subst (λ k → def (Union (A , B)) k) diso ( IsZF.union→ isZF (A , B) (ord→od x) B | |
48 (record { proj1 = case2 refl ; proj2 = subst (λ k → def B k) (sym diso) B∋x})) | |
49 | |
50 ∩-Select : { A B : OD } → Select A ( λ x → ( A ∋ x ) ∧ ( B ∋ x ) ) ≡ ( A ∩ B ) | |
51 ∩-Select {A} {B} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where | |
52 lemma1 : {x : Ordinal} → def (Select A (λ x₁ → (A ∋ x₁) ∧ (B ∋ x₁))) x → def (A ∩ B) x | |
53 lemma1 {x} lt = record { proj1 = proj1 lt ; proj2 = subst (λ k → def B k ) diso (proj2 (proj2 lt)) } | |
54 lemma2 : {x : Ordinal} → def (A ∩ B) x → def (Select A (λ x₁ → (A ∋ x₁) ∧ (B ∋ x₁))) x | |
55 lemma2 {x} lt = record { proj1 = proj1 lt ; proj2 = | |
56 record { proj1 = subst (λ k → def A k) (sym diso) (proj1 lt) ; proj2 = subst (λ k → def B k ) (sym diso) (proj2 lt) } } | |
57 | |
58 dist-ord : {p q r : OD } → p ∩ ( q ∪ r ) ≡ ( p ∩ q ) ∪ ( p ∩ r ) | |
59 dist-ord {p} {q} {r} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where | |
60 lemma1 : {x : Ordinal} → def (p ∩ (q ∪ r)) x → def ((p ∩ q) ∪ (p ∩ r)) x | |
61 lemma1 {x} lt with proj2 lt | |
62 lemma1 {x} lt | case1 q∋x = case1 ( record { proj1 = proj1 lt ; proj2 = q∋x } ) | |
63 lemma1 {x} lt | case2 r∋x = case2 ( record { proj1 = proj1 lt ; proj2 = r∋x } ) | |
64 lemma2 : {x : Ordinal} → def ((p ∩ q) ∪ (p ∩ r)) x → def (p ∩ (q ∪ r)) x | |
65 lemma2 {x} (case1 p∩q) = record { proj1 = proj1 p∩q ; proj2 = case1 (proj2 p∩q ) } | |
66 lemma2 {x} (case2 p∩r) = record { proj1 = proj1 p∩r ; proj2 = case2 (proj2 p∩r ) } | |
67 | |
68 dist-ord2 : {p q r : OD } → p ∪ ( q ∩ r ) ≡ ( p ∪ q ) ∩ ( p ∪ r ) | |
69 dist-ord2 {p} {q} {r} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where | |
70 lemma1 : {x : Ordinal} → def (p ∪ (q ∩ r)) x → def ((p ∪ q) ∩ (p ∪ r)) x | |
71 lemma1 {x} (case1 cp) = record { proj1 = case1 cp ; proj2 = case1 cp } | |
72 lemma1 {x} (case2 cqr) = record { proj1 = case2 (proj1 cqr) ; proj2 = case2 (proj2 cqr) } | |
73 lemma2 : {x : Ordinal} → def ((p ∪ q) ∩ (p ∪ r)) x → def (p ∪ (q ∩ r)) x | |
74 lemma2 {x} lt with proj1 lt | proj2 lt | |
75 lemma2 {x} lt | case1 cp | _ = case1 cp | |
76 lemma2 {x} lt | _ | case1 cp = case1 cp | |
77 lemma2 {x} lt | case2 cq | case2 cr = case2 ( record { proj1 = cq ; proj2 = cr } ) | |
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 |