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

comparison cardinal.agda @ 254:2ea2a19f9cd6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
ordered pair clean up
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 29 Aug 2019 16:16:51 +0900
parents 0446b6c5e7bc
children 53b7acd63481
comparison
equal deleted inserted replaced
253:0446b6c5e7bc 254:2ea2a19f9cd6
18 open OD.OD 18 open OD.OD
19 19
20 open _∧_ 20 open _∧_
21 open _∨_ 21 open _∨_
22 open Bool 22 open Bool
23 open _==_
23 24
24 -- we have to work on Ordinal to keep OD Level n 25 -- we have to work on Ordinal to keep OD Level n
25 -- since we use p∨¬p which works only on Level n 26 -- since we use p∨¬p which works only on Level n
26 27 -- < x , y > = (x , x) , (x , y)
27 <_,_> : (x y : OD) → OD
28 < x , y > = (x , x ) , (x , y )
29
30 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
31
32
33 open _==_
34
35 exg-pair : { x y : OD } → (x , y ) == ( y , x )
36 exg-pair {x} {y} = record { eq→ = left ; eq← = right } where
37 left : {z : Ordinal} → def (x , y) z → def (y , x) z
38 left (case1 t) = case2 t
39 left (case2 t) = case1 t
40 right : {z : Ordinal} → def (y , x) z → def (x , y) z
41 right (case1 t) = case2 t
42 right (case2 t) = case1 t
43
44 ==-trans : { x y z : OD } → x == y → y == z → x == z
45 ==-trans x=y y=z = record { eq→ = λ {m} t → eq→ y=z (eq→ x=y t) ; eq← = λ {m} t → eq← x=y (eq← y=z t) }
46
47 ==-sym : { x y : OD } → x == y → y == x
48 ==-sym x=y = record { eq→ = λ {m} t → eq← x=y t ; eq← = λ {m} t → eq→ x=y t }
49
50 ord≡→≡ : { x y : OD } → od→ord x ≡ od→ord y → x ≡ y
51 ord≡→≡ eq = subst₂ (λ j k → j ≡ k ) oiso oiso ( cong ( λ k → ord→od k ) eq )
52
53 od≡→≡ : { x y : Ordinal } → ord→od x ≡ ord→od y → x ≡ y
54 od≡→≡ eq = subst₂ (λ j k → j ≡ k ) diso diso ( cong ( λ k → od→ord k ) eq )
55
56 eq-prod : { x x' y y' : OD } → x ≡ x' → y ≡ y' → < x , y > ≡ < x' , y' >
57 eq-prod refl refl = refl
58
59 prod-eq : { x x' y y' : OD } → < x , y > == < x' , y' > → (x ≡ x' ) ∧ ( y ≡ y' )
60 prod-eq {x} {x'} {y} {y'} eq = record { proj1 = lemmax ; proj2 = lemmay } where
61 lemma0 : {x y z : OD } → ( x , x ) == ( z , y ) → x ≡ y
62 lemma0 {x} {y} eq with trio< (od→ord x) (od→ord y)
63 lemma0 {x} {y} eq | tri< a ¬b ¬c with eq← eq {od→ord y} (case2 refl)
64 lemma0 {x} {y} eq | tri< a ¬b ¬c | case1 s = ⊥-elim ( o<¬≡ (sym s) a )
65 lemma0 {x} {y} eq | tri< a ¬b ¬c | case2 s = ⊥-elim ( o<¬≡ (sym s) a )
66 lemma0 {x} {y} eq | tri≈ ¬a b ¬c = ord≡→≡ b
67 lemma0 {x} {y} eq | tri> ¬a ¬b c with eq← eq {od→ord y} (case2 refl)
68 lemma0 {x} {y} eq | tri> ¬a ¬b c | case1 s = ⊥-elim ( o<¬≡ s c )
69 lemma0 {x} {y} eq | tri> ¬a ¬b c | case2 s = ⊥-elim ( o<¬≡ s c )
70 lemma2 : {x y z : OD } → ( x , x ) == ( z , y ) → z ≡ y
71 lemma2 {x} {y} {z} eq = trans (sym (lemma0 lemma3 )) ( lemma0 eq ) where
72 lemma3 : ( x , x ) == ( y , z )
73 lemma3 = ==-trans eq exg-pair
74 lemma1 : {x y : OD } → ( x , x ) == ( y , y ) → x ≡ y
75 lemma1 {x} {y} eq with eq← eq {od→ord y} (case2 refl)
76 lemma1 {x} {y} eq | case1 s = ord≡→≡ (sym s)
77 lemma1 {x} {y} eq | case2 s = ord≡→≡ (sym s)
78 lemma4 : {x y z : OD } → ( x , y ) == ( x , z ) → y ≡ z
79 lemma4 {x} {y} {z} eq with eq← eq {od→ord z} (case2 refl)
80 lemma4 {x} {y} {z} eq | case1 s with ord≡→≡ s -- x ≡ z
81 ... | refl with lemma2 (==-sym eq )
82 ... | refl = refl
83 lemma4 {x} {y} {z} eq | case2 s = ord≡→≡ (sym s) -- y ≡ z
84 lemmax : x ≡ x'
85 lemmax with eq→ eq {od→ord (x , x)} (case1 refl)
86 lemmax | case1 s = lemma1 (ord→== s ) -- (x,x)≡(x',x')
87 lemmax | case2 s with lemma2 (ord→== s ) -- (x,x)≡(x',y') with x'≡y'
88 ... | refl = lemma1 (ord→== s )
89 lemmay : y ≡ y'
90 lemmay with lemmax
91 ... | refl with lemma4 eq -- with (x,y)≡(x,y')
92 ... | eq1 = lemma4 (ord→== (cong (λ k → od→ord k ) eq1 ))
93
94 28
95 data ord-pair : (p : Ordinal) → Set n where 29 data ord-pair : (p : Ordinal) → Set n where
96 pair : (x y : Ordinal ) → ord-pair ( od→ord ( < ord→od x , ord→od y > ) ) 30 pair : (x y : Ordinal ) → ord-pair ( od→ord ( < ord→od x , ord→od y > ) )
97 31
98 ZFProduct : OD 32 ZFProduct : OD
99 ZFProduct = record { def = λ x → ord-pair x } 33 ZFProduct = record { def = λ x → ord-pair x }
100 34
101 eq-pair : { x x' y y' : Ordinal } → x ≡ x' → y ≡ y' → pair x y ≅ pair x' y' 35 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
102 eq-pair refl refl = HE.refl 36 -- eq-pair : { x x' y y' : Ordinal } → x ≡ x' → y ≡ y' → pair x y ≅ pair x' y'
37 -- eq-pair refl refl = HE.refl
103 38
104 pi1 : { p : Ordinal } → ord-pair p → Ordinal 39 pi1 : { p : Ordinal } → ord-pair p → Ordinal
105 pi1 ( pair x y) = x 40 pi1 ( pair x y) = x
106 41
107 π1 : { p : OD } → ZFProduct ∋ p → Ordinal 42 π1 : { p : OD } → ZFProduct ∋ p → Ordinal
124 59
125 p-iso1 : { ox oy : Ordinal } → ZFProduct ∋ < ord→od ox , ord→od oy > 60 p-iso1 : { ox oy : Ordinal } → ZFProduct ∋ < ord→od ox , ord→od oy >
126 p-iso1 {ox} {oy} = pair ox oy 61 p-iso1 {ox} {oy} = pair ox oy
127 62
128 p-iso : { x : OD } → (p : ZFProduct ∋ x ) → < ord→od (π1 p) , ord→od (π2 p) > ≡ x 63 p-iso : { x : OD } → (p : ZFProduct ∋ x ) → < ord→od (π1 p) , ord→od (π2 p) > ≡ x
129 p-iso {x} p = ord≡→≡ (lemma2 p) where 64 p-iso {x} p = ord≡→≡ (lemma p) where
130 lemma : { op : Ordinal } → (q : ord-pair op ) → od→ord < ord→od (pi1 q) , ord→od (pi2 q) > ≡ op 65 lemma : { op : Ordinal } → (q : ord-pair op ) → od→ord < ord→od (pi1 q) , ord→od (pi2 q) > ≡ op
131 lemma (pair ox oy) = refl 66 lemma (pair ox oy) = refl
132 lemma2 : { x : OD } → (p : ZFProduct ∋ x ) → od→ord < ord→od (π1 p) , ord→od (π2 p) > ≡ od→ord x
133 lemma2 {x} p = lemma p
134 67
135 68
136 ∋-p : (A x : OD ) → Dec ( A ∋ x ) 69 ∋-p : (A x : OD ) → Dec ( A ∋ x )
137 ∋-p A x with p∨¬p ( A ∋ x ) 70 ∋-p A x with p∨¬p ( A ∋ x )
138 ∋-p A x | case1 t = yes t 71 ∋-p A x | case1 t = yes t