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

comparison src/OPair.agda @ 431:a5f8084b8368

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
reorganiztion for apkg
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 21 Dec 2020 10:23:37 +0900
parents
children 55ab5de1ae02
comparison
equal deleted inserted replaced
430:28c7be8f252c 431:a5f8084b8368
1 {-# OPTIONS --allow-unsolved-metas #-}
2
3 open import Level
4 open import Ordinals
5 module OPair {n : Level } (O : Ordinals {n}) where
6
7 open import zf
8 open import logic
9 import OD
10 import ODUtil
11 import OrdUtil
12
13 open import Relation.Nullary
14 open import Relation.Binary
15 open import Data.Empty
16 open import Relation.Binary
17 open import Relation.Binary.Core
18 open import Relation.Binary.PropositionalEquality
19 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ )
20
21 open OD O
22 open OD.OD
23 open OD.HOD
24 open ODAxiom odAxiom
25
26 open Ordinals.Ordinals O
27 open Ordinals.IsOrdinals isOrdinal
28 open Ordinals.IsNext isNext
29 open OrdUtil O
30 open ODUtil O
31
32 open _∧_
33 open _∨_
34 open Bool
35
36 open _==_
37
38 <_,_> : (x y : HOD) → HOD
39 < x , y > = (x , x ) , (x , y )
40
41 exg-pair : { x y : HOD } → (x , y ) =h= ( y , x )
42 exg-pair {x} {y} = record { eq→ = left ; eq← = right } where
43 left : {z : Ordinal} → odef (x , y) z → odef (y , x) z
44 left (case1 t) = case2 t
45 left (case2 t) = case1 t
46 right : {z : Ordinal} → odef (y , x) z → odef (x , y) z
47 right (case1 t) = case2 t
48 right (case2 t) = case1 t
49
50 ord≡→≡ : { x y : HOD } → & x ≡ & y → x ≡ y
51 ord≡→≡ eq = subst₂ (λ j k → j ≡ k ) *iso *iso ( cong ( λ k → * k ) eq )
52
53 od≡→≡ : { x y : Ordinal } → * x ≡ * y → x ≡ y
54 od≡→≡ eq = subst₂ (λ j k → j ≡ k ) &iso &iso ( cong ( λ k → & k ) eq )
55
56 eq-prod : { x x' y y' : HOD } → x ≡ x' → y ≡ y' → < x , y > ≡ < x' , y' >
57 eq-prod refl refl = refl
58
59 xx=zy→x=y : {x y z : HOD } → ( x , x ) =h= ( z , y ) → x ≡ y
60 xx=zy→x=y {x} {y} eq with trio< (& x) (& y)
61 xx=zy→x=y {x} {y} eq | tri< a ¬b ¬c with eq← eq {& y} (case2 refl)
62 xx=zy→x=y {x} {y} eq | tri< a ¬b ¬c | case1 s = ⊥-elim ( o<¬≡ (sym s) a )
63 xx=zy→x=y {x} {y} eq | tri< a ¬b ¬c | case2 s = ⊥-elim ( o<¬≡ (sym s) a )
64 xx=zy→x=y {x} {y} eq | tri≈ ¬a b ¬c = ord≡→≡ b
65 xx=zy→x=y {x} {y} eq | tri> ¬a ¬b c with eq← eq {& y} (case2 refl)
66 xx=zy→x=y {x} {y} eq | tri> ¬a ¬b c | case1 s = ⊥-elim ( o<¬≡ s c )
67 xx=zy→x=y {x} {y} eq | tri> ¬a ¬b c | case2 s = ⊥-elim ( o<¬≡ s c )
68
69 prod-eq : { x x' y y' : HOD } → < x , y > =h= < x' , y' > → (x ≡ x' ) ∧ ( y ≡ y' )
70 prod-eq {x} {x'} {y} {y'} eq = ⟪ lemmax , lemmay ⟫ where
71 lemma2 : {x y z : HOD } → ( x , x ) =h= ( z , y ) → z ≡ y
72 lemma2 {x} {y} {z} eq = trans (sym (xx=zy→x=y lemma3 )) ( xx=zy→x=y eq ) where
73 lemma3 : ( x , x ) =h= ( y , z )
74 lemma3 = ==-trans eq exg-pair
75 lemma1 : {x y : HOD } → ( x , x ) =h= ( y , y ) → x ≡ y
76 lemma1 {x} {y} eq with eq← eq {& y} (case2 refl)
77 lemma1 {x} {y} eq | case1 s = ord≡→≡ (sym s)
78 lemma1 {x} {y} eq | case2 s = ord≡→≡ (sym s)
79 lemma4 : {x y z : HOD } → ( x , y ) =h= ( x , z ) → y ≡ z
80 lemma4 {x} {y} {z} eq with eq← eq {& z} (case2 refl)
81 lemma4 {x} {y} {z} eq | case1 s with ord≡→≡ s -- x ≡ z
82 ... | refl with lemma2 (==-sym eq )
83 ... | refl = refl
84 lemma4 {x} {y} {z} eq | case2 s = ord≡→≡ (sym s) -- y ≡ z
85 lemmax : x ≡ x'
86 lemmax with eq→ eq {& (x , x)} (case1 refl)
87 lemmax | case1 s = lemma1 (ord→== s ) -- (x,x)≡(x',x')
88 lemmax | case2 s with lemma2 (ord→== s ) -- (x,x)≡(x',y') with x'≡y'
89 ... | refl = lemma1 (ord→== s )
90 lemmay : y ≡ y'
91 lemmay with lemmax
92 ... | refl with lemma4 eq -- with (x,y)≡(x,y')
93 ... | eq1 = lemma4 (ord→== (cong (λ k → & k ) eq1 ))
94
95 --
96 -- unlike ordered pair, ZFProduct is not a HOD
97
98 data ord-pair : (p : Ordinal) → Set n where
99 pair : (x y : Ordinal ) → ord-pair ( & ( < * x , * y > ) )
100
101 ZFProduct : OD
102 ZFProduct = record { def = λ x → ord-pair x }
103
104 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
105 -- eq-pair : { x x' y y' : Ordinal } → x ≡ x' → y ≡ y' → pair x y ≅ pair x' y'
106 -- eq-pair refl refl = HE.refl
107
108 pi1 : { p : Ordinal } → ord-pair p → Ordinal
109 pi1 ( pair x y) = x
110
111 π1 : { p : HOD } → def ZFProduct (& p) → HOD
112 π1 lt = * (pi1 lt )
113
114 pi2 : { p : Ordinal } → ord-pair p → Ordinal
115 pi2 ( pair x y ) = y
116
117 π2 : { p : HOD } → def ZFProduct (& p) → HOD
118 π2 lt = * (pi2 lt )
119
120 op-cons : { ox oy : Ordinal } → def ZFProduct (& ( < * ox , * oy > ))
121 op-cons {ox} {oy} = pair ox oy
122
123 def-subst : {Z : OD } {X : Ordinal }{z : OD } {x : Ordinal }→ def Z X → Z ≡ z → X ≡ x → def z x
124 def-subst df refl refl = df
125
126 p-cons : ( x y : HOD ) → def ZFProduct (& ( < x , y >))
127 p-cons x y = def-subst {_} {_} {ZFProduct} {& (< x , y >)} (pair (& x) ( & y )) refl (
128 let open ≡-Reasoning in begin
129 & < * (& x) , * (& y) >
130 ≡⟨ cong₂ (λ j k → & < j , k >) *iso *iso ⟩
131 & < x , y >
132 ∎ )
133
134 op-iso : { op : Ordinal } → (q : ord-pair op ) → & < * (pi1 q) , * (pi2 q) > ≡ op
135 op-iso (pair ox oy) = refl
136
137 p-iso : { x : HOD } → (p : def ZFProduct (& x) ) → < π1 p , π2 p > ≡ x
138 p-iso {x} p = ord≡→≡ (op-iso p)
139
140 p-pi1 : { x y : HOD } → (p : def ZFProduct (& < x , y >) ) → π1 p ≡ x
141 p-pi1 {x} {y} p = proj1 ( prod-eq ( ord→== (op-iso p) ))
142
143 p-pi2 : { x y : HOD } → (p : def ZFProduct (& < x , y >) ) → π2 p ≡ y
144 p-pi2 {x} {y} p = proj2 ( prod-eq ( ord→== (op-iso p)))
145
146 ω-pair : {x y : HOD} → {m : Ordinal} → & x o< next m → & y o< next m → & (x , y) o< next m
147 ω-pair lx ly = next< (omax<nx lx ly ) ho<
148
149 ω-opair : {x y : HOD} → {m : Ordinal} → & x o< next m → & y o< next m → & < x , y > o< next m
150 ω-opair {x} {y} {m} lx ly = lemma0 where
151 lemma0 : & < x , y > o< next m
152 lemma0 = osucprev (begin
153 osuc (& < x , y >)
154 <⟨ osuc<nx ho< ⟩
155 next (omax (& (x , x)) (& (x , y)))
156 ≡⟨ cong (λ k → next k) (sym ( omax≤ _ _ pair-xx<xy )) ⟩
157 next (osuc (& (x , y)))
158 ≡⟨ sym (nexto≡) ⟩
159 next (& (x , y))
160 ≤⟨ x<ny→≤next (ω-pair lx ly) ⟩
161 next m
162 ∎ ) where
163 open o≤-Reasoning O
164
165 _⊗_ : (A B : HOD) → HOD
166 A ⊗ B = Union ( Replace B (λ b → Replace A (λ a → < a , b > ) ))
167
168 product→ : {A B a b : HOD} → A ∋ a → B ∋ b → ( A ⊗ B ) ∋ < a , b >
169 product→ {A} {B} {a} {b} A∋a B∋b = λ t → t (& (Replace A (λ a → < a , b >)))
170 ⟪ lemma1 , subst (λ k → odef k (& < a , b >)) (sym *iso) lemma2 ⟫ where
171 lemma1 : odef (Replace B (λ b₁ → Replace A (λ a₁ → < a₁ , b₁ >))) (& (Replace A (λ a₁ → < a₁ , b >)))
172 lemma1 = replacement← B b B∋b
173 lemma2 : odef (Replace A (λ a₁ → < a₁ , b >)) (& < a , b >)
174 lemma2 = replacement← A a A∋a
175
176 x<nextA : {A x : HOD} → A ∋ x → & x o< next (odmax A)
177 x<nextA {A} {x} A∋x = ordtrans (c<→o< {x} {A} A∋x) ho<
178
179 A<Bnext : {A B x : HOD} → & A o< & B → A ∋ x → & x o< next (odmax B)
180 A<Bnext {A} {B} {x} lt A∋x = osucprev (begin
181 osuc (& x)
182 <⟨ osucc (c<→o< A∋x) ⟩
183 osuc (& A)
184 <⟨ osucc lt ⟩
185 osuc (& B)
186 <⟨ osuc<nx ho< ⟩
187 next (odmax B)
188 ∎ ) where open o≤-Reasoning O
189
190 ZFP : (A B : HOD) → HOD
191 ZFP A B = record { od = record { def = λ x → ord-pair x ∧ ((p : ord-pair x ) → odef A (pi1 p) ∧ odef B (pi2 p) )} ;
192 odmax = omax (next (odmax A)) (next (odmax B)) ; <odmax = λ {y} px → lemma y px }
193 where
194 lemma : (y : Ordinal) → ( ord-pair y ∧ ((p : ord-pair y) → odef A (pi1 p) ∧ odef B (pi2 p))) → y o< omax (next (odmax A)) (next (odmax B))
195 lemma y lt with proj1 lt
196 lemma p lt | pair x y with trio< (& A) (& B)
197 lemma p lt | pair x y | tri< a ¬b ¬c = ordtrans (ω-opair (A<Bnext a (subst (λ k → odef A k ) (sym &iso)
198 (proj1 (proj2 lt (pair x y))))) (lemma1 (proj2 (proj2 lt (pair x y))))) (omax-y _ _ ) where
199 lemma1 : odef B y → & (* y) o< next (HOD.odmax B)
200 lemma1 lt = x<nextA {B} (d→∋ B lt)
201 lemma p lt | pair x y | tri≈ ¬a b ¬c = ordtrans (ω-opair (x<nextA {A} (d→∋ A ((proj1 (proj2 lt (pair x y)))))) lemma2 ) (omax-x _ _ ) where
202 lemma2 : & (* y) o< next (HOD.odmax A)
203 lemma2 = ordtrans ( subst (λ k → & (* y) o< k ) (sym b) (c<→o< (d→∋ B ((proj2 (proj2 lt (pair x y))))))) ho<
204 lemma p lt | pair x y | tri> ¬a ¬b c = ordtrans (ω-opair (x<nextA {A} (d→∋ A ((proj1 (proj2 lt (pair x y))))))
205 (A<Bnext c (subst (λ k → odef B k ) (sym &iso) (proj2 (proj2 lt (pair x y)))))) (omax-x _ _ )
206
207 ZFP⊆⊗ : {A B : HOD} {x : Ordinal} → odef (ZFP A B) x → odef (A ⊗ B) x
208 ZFP⊆⊗ {A} {B} {px} ⟪ (pair x y) , p2 ⟫ = product→ (d→∋ A (proj1 (p2 (pair x y) ))) (d→∋ B (proj2 (p2 (pair x y) )))
209
210 -- axiom of choice required
211 -- ⊗⊆ZFP : {A B x : HOD} → ( A ⊗ B ) ∋ x → def ZFProduct (& x)
212 -- ⊗⊆ZFP {A} {B} {x} lt = subst (λ k → ord-pair (& k )) {!!} op-cons
213