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

comparison cardinal.agda @ 249:2ecda48298e3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 28 Aug 2019 20:32:35 +0900
parents 9fd85b954477
children 08428a661677
comparison
equal deleted inserted replaced
248:9fd85b954477 249:2ecda48298e3
25 -- since we use p∨¬p which works only on Level n 25 -- since we use p∨¬p which works only on Level n
26 26
27 <_,_> : (x y : OD) → OD 27 <_,_> : (x y : OD) → OD
28 < x , y > = (x , x ) , (x , y ) 28 < x , y > = (x , x ) , (x , y )
29 29
30 data ord-pair : (p : Ordinal) → Set n where
31 pair : (x y : Ordinal ) → ord-pair ( od→ord ( < ord→od x , ord→od y > ) )
32
33 ZFProduct : OD
34 ZFProduct = record { def = λ x → ord-pair x }
35
36 pi1 : { p : Ordinal } → ord-pair p → Ordinal
37 pi1 ( pair x y ) = x
38
39 π1 : { p : OD } → ZFProduct ∋ p → Ordinal
40 π1 lt = pi1 lt
41
42 pi2 : { p : Ordinal } → ord-pair p → Ordinal
43 pi2 ( pair x y ) = y
44
45 π2 : { p : OD } → ZFProduct ∋ p → Ordinal
46 π2 lt = pi2 lt
47
48 p-cons : ( x y : OD ) → ZFProduct ∋ < x , y >
49 p-cons x y = def-subst {_} {_} {ZFProduct} {od→ord (< x , y >)} (pair (od→ord x) ( od→ord y )) refl (
50 let open ≡-Reasoning in begin
51 od→ord < ord→od (od→ord x) , ord→od (od→ord y) >
52 ≡⟨ cong₂ (λ j k → od→ord < j , k >) oiso oiso ⟩
53 od→ord < x , y >
54 ∎ )
55
56 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 30 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
57 31
58 eq-pair : { x x' y y' : Ordinal } → x ≡ x' → y ≡ y' → pair x y ≅ pair x' y'
59 eq-pair refl refl = HE.refl
60
61 eq-prod : { x x' y y' : OD } → x ≡ x' → y ≡ y' → < x , y > ≡ < x' , y' >
62 eq-prod refl refl = refl
63 32
64 open _==_ 33 open _==_
65 34
66 exg-pair : { x y : OD } → (x , y ) == ( y , x ) 35 exg-pair : { x y : OD } → (x , y ) == ( y , x )
67 exg-pair {x} {y} = record { eq→ = left ; eq← = right } where 36 exg-pair {x} {y} = record { eq→ = left ; eq← = right } where
78 ==-sym : { x y : OD } → x == y → y == x 47 ==-sym : { x y : OD } → x == y → y == x
79 ==-sym x=y = record { eq→ = λ {m} t → eq← x=y t ; eq← = λ {m} t → eq→ x=y t } 48 ==-sym x=y = record { eq→ = λ {m} t → eq← x=y t ; eq← = λ {m} t → eq→ x=y t }
80 49
81 ord≡→≡ : { x y : OD } → od→ord x ≡ od→ord y → x ≡ y 50 ord≡→≡ : { x y : OD } → od→ord x ≡ od→ord y → x ≡ y
82 ord≡→≡ eq = subst₂ (λ j k → j ≡ k ) oiso oiso ( cong ( λ k → ord→od k ) eq ) 51 ord≡→≡ eq = subst₂ (λ j k → j ≡ k ) oiso oiso ( cong ( λ k → ord→od k ) eq )
52
53 eq-prod : { x x' y y' : OD } → x ≡ x' → y ≡ y' → < x , y > ≡ < x' , y' >
54 eq-prod refl refl = refl
83 55
84 prod-eq : { x x' y y' : OD } → < x , y > == < x' , y' > → (x ≡ x' ) ∧ ( y ≡ y' ) 56 prod-eq : { x x' y y' : OD } → < x , y > == < x' , y' > → (x ≡ x' ) ∧ ( y ≡ y' )
85 prod-eq {x} {x'} {y} {y'} eq = record { proj1 = lemmax ; proj2 = lemmay } where 57 prod-eq {x} {x'} {y} {y'} eq = record { proj1 = lemmax ; proj2 = lemmay } where
86 lemma0 : {x y z : OD } → ( x , x ) == ( z , y ) → x ≡ y 58 lemma0 : {x y z : OD } → ( x , x ) == ( z , y ) → x ≡ y
87 lemma0 {x} {y} eq with trio< (od→ord x) (od→ord y) 59 lemma0 {x} {y} eq with trio< (od→ord x) (od→ord y)
114 lemmay : y ≡ y' 86 lemmay : y ≡ y'
115 lemmay with lemmax 87 lemmay with lemmax
116 ... | refl with lemma4 eq -- with (x,y)≡(x,y') 88 ... | refl with lemma4 eq -- with (x,y)≡(x,y')
117 ... | eq1 = lemma4 (ord→== (cong (λ k → od→ord k ) eq1 )) 89 ... | eq1 = lemma4 (ord→== (cong (λ k → od→ord k ) eq1 ))
118 90
119 postulate 91 data ord-pair : (p : Ordinal) → Set n where
120 def-eq : { P Q p q : OD } → P ≡ Q → p ≡ q → (pt : P ∋ p ) → (qt : Q ∋ q ) → pt ≅ qt 92 pair : (x y : Ordinal ) → ord-pair ( od→ord ( < ord→od x , ord→od y > ) )
121 93
122 ∈-to-ord : {p : Ordinal } → ( ZFProduct ∋ ord→od p ) → ord-pair p 94 ZFProduct : OD
123 ∈-to-ord {p} lt = def-subst {ZFProduct} {(od→ord (ord→od p))} {_} {_} lt refl diso 95 ZFProduct = record { def = λ x → ord-pair x }
124 96
125 ord-to-∈ : {p : Ordinal } → ord-pair p → ZFProduct ∋ ord→od p 97 eq-pair : { x x' y y' : Ordinal } → x ≡ x' → y ≡ y' → pair x y ≅ pair x' y'
126 ord-to-∈ {p} lt = def-subst {_} {_} {ZFProduct} {(od→ord (ord→od p))} lt refl (sym diso) 98 eq-pair refl refl = HE.refl
127 99
128 lemma333 : { A a : OD } → { x : A ∋ a } → def-subst {A} {od→ord a} (def-subst {A} {od→ord a} x refl refl ) refl refl ≡ x 100 pi1 : { p : Ordinal } → ord-pair p → Ordinal
129 lemma333 = refl 101 pi1 ( pair x y) = x
130 102
131 lemma334 : { A B : OD } → {a b : Ordinal} → { x : A ∋ ord→od a } → { y : B ∋ ord→od b } → (f1 : A ≡ B) → (f2 : a ≡ b) 103 π1 : { p : OD } → ZFProduct ∋ p → Ordinal
132 → def-subst {B} {od→ord (ord→od b)} (def-subst {A} { od→ord (ord→od a)} x f1 (cong (λ k → od→ord (ord→od k)) f2 )) refl refl ≅ x 104 π1 lt = pi1 lt
133 lemma334 {A} {A} {a} {a} {x} {y} refl refl with def-eq {A} {A} {ord→od a} {ord→od a} refl refl x y 105
134 ... | HE.refl = HE.refl 106 pi2 : { p : Ordinal } → ord-pair p → Ordinal
135 107 pi2 ( pair x y ) = y
136 lemma335 : { A B C : OD } → {a b c : Ordinal} → { x : A ∋ ord→od a } → { y : C ∋ ord→od c } → (f1 : A ≡ B) → (f2 : a ≡ b) → (g1 : B ≡ C) → (g2 : b ≡ c) 108
137 → def-subst {B} {od→ord (ord→od b)} (def-subst {A} { od→ord (ord→od a)} x f1 (cong (λ k → od→ord (ord→od k)) f2 )) g1 (cong (λ k → od→ord (ord→od k)) g2 ) 109 π2 : { p : OD } → ZFProduct ∋ p → Ordinal
138 ≅ def-subst {A} { od→ord (ord→od a)} {C } { od→ord (ord→od c)} x (trans f1 g1) 110 π2 lt = pi2 lt
139 (trans (cong (λ k → od→ord (ord→od k)) f2 ) (cong (λ k → od→ord (ord→od k)) g2 )) 111
140 lemma335 {A} {A} {A} {a} {a} {a} {x} {y} refl refl refl refl with def-eq {A} {A} {ord→od a} {ord→od a} refl refl x y 112 p-cons : ( x y : OD ) → ZFProduct ∋ < x , y >
141 ... | HE.refl = HE.refl 113 p-cons x y = def-subst {_} {_} {ZFProduct} {od→ord (< x , y >)} (pair (od→ord x) ( od→ord y )) refl (
142 114 let open ≡-Reasoning in begin
143 ∈-to-ord-oiso : { p : Ordinal } → { x : ord-pair p } → ∈-to-ord (ord-to-∈ x) ≡ x 115 od→ord < ord→od (od→ord x) , ord→od (od→ord y) >
144 ∈-to-ord-oiso {p} {x} = {!!} where 116 ≡⟨ cong₂ (λ j k → od→ord < j , k >) oiso oiso ⟩
145 lemma : def-subst {_} {_} {ZFProduct} {{!!}} (def-subst {_} {_} {ZFProduct} {{!!}} x refl (sym diso)) refl diso ≡ x 117 od→ord < x , y >
146 lemma = {!!} 118 ∎ )
147 119
148 lemma34 : { p q : Ordinal } → (x : ord-pair p ) → (y : ord-pair q ) → p ≡ q → x ≅ y 120
149 lemma34 {p} {q} x y refl = subst₂ (λ j k → j ≅ k) ∈-to-ord-oiso ∈-to-ord-oiso (HE.cong (λ k → ∈-to-ord k) lemma1 ) where 121 p-iso-1 : { x y : OD } → (p : ZFProduct ∋ < x , y > ) → π1 p ≡ od→ord x
150 lemma : (pt : ZFProduct ∋ ord→od p ) → (qt : ZFProduct ∋ ord→od q ) → p ≡ q → pt ≅ qt 122 p-iso-1 {x} {y} p = lemma1 {od→ord < x , y >} {od→ord x} {od→ord y} p (cong₂ (λ j k → ord-pair (od→ord < j , k >)) (sym oiso) (sym oiso) ) where
151 lemma pt qt eq = def-eq {ZFProduct} {ZFProduct} refl (cong (λ k → ord→od k) eq) pt qt 123 lemma1 : {op ox oy : Ordinal } → ( p : ord-pair op ) → ord-pair op ≡ ord-pair (od→ord ( < ord→od ox , ord→od oy > )) → pi1 p ≡ ox
152 lemma1 : (ord-to-∈ x) ≅ (ord-to-∈ y ) 124 lemma1 (pair ox oy) eq = {!!}
153 lemma1 = lemma (ord-to-∈ x) (ord-to-∈ y ) refl 125 lemma2 : {op ox oy : Ordinal } → ord-pair op ≡ ord-pair (od→ord ( < ord→od ox , ord→od oy > ))
154 126 lemma2 = {!!}
155 π1-cong : { p q : OD } → p ≡ q → (pt : ZFProduct ∋ p ) → (qt : ZFProduct ∋ q ) → π1 pt ≅ π1 qt 127 lemma0 : {op ox oy : Ordinal } → ( p : ord-pair (od→ord ( < ord→od ox , ord→od oy > ))) → pi1 p ≡ ox
156 π1-cong {p} {q} refl s t = HE.cong (λ k → pi1 k ) (def-eq {ZFProduct} {ZFProduct} refl refl s t ) 128 lemma0 = {!!}
157 129 lemma3 : {ox oy : Ordinal } ( p : ord-pair (od→ord ( < ord→od ox , ord→od oy > )) ) → pi1 p ≡ ox
158 π1--iso : { x y : OD } → (p : ZFProduct ∋ < x , y > ) → π1 p ≅ od→ord x 130 lemma3 {ox} {oy} p = {!!}
159 π1--iso {x} {y} p = lemma (od→ord x) (od→ord y) {!!} {!!} refl where 131 lemma4 : {ox oy : Ordinal } → ord-pair (od→ord < ord→od ox , ord→od oy > ) ≡ ZFProduct ∋ < ord→od ox , ord→od oy >
160 lemma1 : ( ox oy op : Ordinal ) → (p : ord-pair op) → op ≡ od→ord ( < ord→od ox , ord→od oy >) → p ≅ pair ox oy 132 lemma4 = refl
161 lemma1 ox oy op (pair x' y') eq = lemma34 {!!} {!!} {!!} 133 lemma : {p : OD } → ord-pair (od→ord p) ≡ ZFProduct ∋ p
162 lemma : ( ox oy op : Ordinal ) → (p : ord-pair op ) → op ≡ od→ord ( < ord→od ox , ord→od oy > ) → pi1 p ≅ ox 134 lemma = refl
163 lemma ox oy op p eq = {!!} -- HE.cong (λ k → pi1 k ) (lemma1 ox oy op p eq ) 135
164 136 p-iso : { x : OD } → (p : ZFProduct ∋ x ) → < ord→od (π1 p) , ord→od (π2 p) > ≡ x
165 p-iso : { x : OD } → {p : ZFProduct ∋ x } → < ord→od (π1 p) , ord→od (π2 p) > ≡ x 137 p-iso {x} p = {!!}
166 p-iso {x} {p} with p-cons (ord→od (π1 p)) (ord→od (π2 p))
167 ... | t = {!!}
168
169 138
170 ∋-p : (A x : OD ) → Dec ( A ∋ x ) 139 ∋-p : (A x : OD ) → Dec ( A ∋ x )
171 ∋-p A x with p∨¬p ( A ∋ x ) 140 ∋-p A x with p∨¬p ( A ∋ x )
172 ∋-p A x | case1 t = yes t 141 ∋-p A x | case1 t = yes t
173 ∋-p A x | case2 t = no t 142 ∋-p A x | case2 t = no t