Mercurial > hg > Members > kono > Proof > ZF-in-agda
annotate partfunc.agda @ 424:cc7909f86841
remvoe TransFinifte1
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sat, 01 Aug 2020 23:37:10 +0900 |
parents | 9984cdd88da3 |
children |
rev | line source |
---|---|
387 | 1 {-# OPTIONS --allow-unsolved-metas #-} |
190 | 2 open import Level |
387 | 3 open import Relation.Nullary |
4 open import Relation.Binary.PropositionalEquality | |
236 | 5 open import Ordinals |
387 | 6 module partfunc {n : Level } (O : Ordinals {n}) where |
236 | 7 |
8 open import logic | |
363 | 9 open import Relation.Binary |
10 open import Data.Empty | |
392 | 11 open import Data.List hiding (filter) |
387 | 12 open import Data.Maybe |
190 | 13 open import Relation.Binary |
14 open import Relation.Binary.Core | |
191
9eb6a8691f02
choice function cannot jump between ordinal level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
190
diff
changeset
|
15 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) |
387 | 16 open import filter O |
294
4340ffcfa83d
ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
17 |
236 | 18 open _∧_ |
19 open _∨_ | |
20 open Bool | |
21 | |
423 | 22 ---- |
23 -- | |
24 -- Partial Function without ZF | |
25 -- | |
295 | 26 |
387 | 27 record PFunc (Dom : Set n) (Cod : Set n) : Set (suc n) where |
269
30e419a2be24
disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
28 field |
387 | 29 dom : Dom → Set n |
30 pmap : (x : Dom ) → dom x → Cod | |
31 meq : {x : Dom } → { p q : dom x } → pmap x p ≡ pmap x q | |
371 | 32 |
423 | 33 ---- |
34 -- | |
35 -- PFunc (Lift n Nat) Cod is equivalent to List (Maybe Cod) | |
36 -- | |
374 | 37 |
387 | 38 data Findp : {Cod : Set n} → List (Maybe Cod) → (x : Nat) → Set where |
39 v0 : {Cod : Set n} → {f : List (Maybe Cod)} → ( v : Cod ) → Findp ( just v ∷ f ) Zero | |
40 vn : {Cod : Set n} → {f : List (Maybe Cod)} {d : Maybe Cod} → {x : Nat} → Findp f x → Findp (d ∷ f) (Suc x) | |
379 | 41 |
42 open PFunc | |
43 | |
387 | 44 find : {Cod : Set n} → (f : List (Maybe Cod) ) → (x : Nat) → Findp f x → Cod |
45 find (just v ∷ _) 0 (v0 v) = v | |
46 find (_ ∷ n) (Suc i) (vn p) = find n i p | |
381 | 47 |
387 | 48 findpeq : {Cod : Set n} → (f : List (Maybe Cod)) → {x : Nat} {p q : Findp f x } → find f x p ≡ find f x q |
49 findpeq n {0} {v0 _} {v0 _} = refl | |
50 findpeq [] {Suc x} {()} | |
51 findpeq (just x₁ ∷ n) {Suc x} {vn p} {vn q} = findpeq n {x} {p} {q} | |
52 findpeq (nothing ∷ n) {Suc x} {vn p} {vn q} = findpeq n {x} {p} {q} | |
381 | 53 |
387 | 54 List→PFunc : {Cod : Set n} → List (Maybe Cod) → PFunc (Lift n Nat) Cod |
55 List→PFunc fp = record { dom = λ x → Lift n (Findp fp (lower x)) | |
56 ; pmap = λ x y → find fp (lower x) (lower y) | |
57 ; meq = λ {x} {p} {q} → findpeq fp {lower x} {lower p} {lower q} | |
58 } | |
423 | 59 ---- |
60 -- | |
61 -- to List (Maybe Two) is a Latice | |
62 -- | |
381 | 63 |
387 | 64 _3⊆b_ : (f g : List (Maybe Two)) → Bool |
381 | 65 [] 3⊆b [] = true |
387 | 66 [] 3⊆b (nothing ∷ g) = [] 3⊆b g |
381 | 67 [] 3⊆b (_ ∷ g) = true |
387 | 68 (nothing ∷ f) 3⊆b [] = f 3⊆b [] |
69 (nothing ∷ f) 3⊆b (_ ∷ g) = f 3⊆b g | |
70 (just i0 ∷ f) 3⊆b (just i0 ∷ g) = f 3⊆b g | |
71 (just i1 ∷ f) 3⊆b (just i1 ∷ g) = f 3⊆b g | |
381 | 72 _ 3⊆b _ = false |
73 | |
387 | 74 _3⊆_ : (f g : List (Maybe Two)) → Set |
381 | 75 f 3⊆ g = (f 3⊆b g) ≡ true |
76 | |
387 | 77 _3∩_ : (f g : List (Maybe Two)) → List (Maybe Two) |
78 [] 3∩ (nothing ∷ g) = nothing ∷ ([] 3∩ g) | |
381 | 79 [] 3∩ g = [] |
387 | 80 (nothing ∷ f) 3∩ [] = nothing ∷ f 3∩ [] |
381 | 81 f 3∩ [] = [] |
387 | 82 (just i0 ∷ f) 3∩ (just i0 ∷ g) = just i0 ∷ ( f 3∩ g ) |
83 (just i1 ∷ f) 3∩ (just i1 ∷ g) = just i1 ∷ ( f 3∩ g ) | |
84 (_ ∷ f) 3∩ (_ ∷ g) = nothing ∷ ( f 3∩ g ) | |
381 | 85 |
387 | 86 3∩⊆f : { f g : List (Maybe Two) } → (f 3∩ g ) 3⊆ f |
381 | 87 3∩⊆f {[]} {[]} = refl |
387 | 88 3∩⊆f {[]} {just _ ∷ g} = refl |
89 3∩⊆f {[]} {nothing ∷ g} = 3∩⊆f {[]} {g} | |
90 3∩⊆f {just _ ∷ f} {[]} = refl | |
91 3∩⊆f {nothing ∷ f} {[]} = 3∩⊆f {f} {[]} | |
92 3∩⊆f {just i0 ∷ f} {just i0 ∷ g} = 3∩⊆f {f} {g} | |
93 3∩⊆f {just i1 ∷ f} {just i1 ∷ g} = 3∩⊆f {f} {g} | |
94 3∩⊆f {just i0 ∷ f} {just i1 ∷ g} = 3∩⊆f {f} {g} | |
95 3∩⊆f {just i1 ∷ f} {just i0 ∷ g} = 3∩⊆f {f} {g} | |
96 3∩⊆f {nothing ∷ f} {just _ ∷ g} = 3∩⊆f {f} {g} | |
97 3∩⊆f {just i0 ∷ f} {nothing ∷ g} = 3∩⊆f {f} {g} | |
98 3∩⊆f {just i1 ∷ f} {nothing ∷ g} = 3∩⊆f {f} {g} | |
99 3∩⊆f {nothing ∷ f} {nothing ∷ g} = 3∩⊆f {f} {g} | |
381 | 100 |
387 | 101 3∩sym : { f g : List (Maybe Two) } → (f 3∩ g ) ≡ (g 3∩ f ) |
381 | 102 3∩sym {[]} {[]} = refl |
387 | 103 3∩sym {[]} {just _ ∷ g} = refl |
104 3∩sym {[]} {nothing ∷ g} = cong (λ k → nothing ∷ k) (3∩sym {[]} {g}) | |
105 3∩sym {just _ ∷ f} {[]} = refl | |
106 3∩sym {nothing ∷ f} {[]} = cong (λ k → nothing ∷ k) (3∩sym {f} {[]}) | |
107 3∩sym {just i0 ∷ f} {just i0 ∷ g} = cong (λ k → just i0 ∷ k) (3∩sym {f} {g}) | |
108 3∩sym {just i0 ∷ f} {just i1 ∷ g} = cong (λ k → nothing ∷ k) (3∩sym {f} {g}) | |
109 3∩sym {just i1 ∷ f} {just i0 ∷ g} = cong (λ k → nothing ∷ k) (3∩sym {f} {g}) | |
110 3∩sym {just i1 ∷ f} {just i1 ∷ g} = cong (λ k → just i1 ∷ k) (3∩sym {f} {g}) | |
111 3∩sym {just i0 ∷ f} {nothing ∷ g} = cong (λ k → nothing ∷ k) (3∩sym {f} {g}) | |
112 3∩sym {just i1 ∷ f} {nothing ∷ g} = cong (λ k → nothing ∷ k) (3∩sym {f} {g}) | |
113 3∩sym {nothing ∷ f} {just i0 ∷ g} = cong (λ k → nothing ∷ k) (3∩sym {f} {g}) | |
114 3∩sym {nothing ∷ f} {just i1 ∷ g} = cong (λ k → nothing ∷ k) (3∩sym {f} {g}) | |
115 3∩sym {nothing ∷ f} {nothing ∷ g} = cong (λ k → nothing ∷ k) (3∩sym {f} {g}) | |
381 | 116 |
387 | 117 3⊆-[] : { h : List (Maybe Two) } → [] 3⊆ h |
381 | 118 3⊆-[] {[]} = refl |
387 | 119 3⊆-[] {just _ ∷ h} = refl |
120 3⊆-[] {nothing ∷ h} = 3⊆-[] {h} | |
381 | 121 |
387 | 122 3⊆trans : { f g h : List (Maybe Two) } → f 3⊆ g → g 3⊆ h → f 3⊆ h |
381 | 123 3⊆trans {[]} {[]} {[]} f<g g<h = refl |
387 | 124 3⊆trans {[]} {[]} {just _ ∷ h} f<g g<h = refl |
125 3⊆trans {[]} {[]} {nothing ∷ h} f<g g<h = 3⊆trans {[]} {[]} {h} refl g<h | |
126 3⊆trans {[]} {nothing ∷ g} {[]} f<g g<h = refl | |
127 3⊆trans {[]} {just _ ∷ g} {just _ ∷ h} f<g g<h = refl | |
128 3⊆trans {[]} {nothing ∷ g} {just _ ∷ h} f<g g<h = refl | |
129 3⊆trans {[]} {nothing ∷ g} {nothing ∷ h} f<g g<h = 3⊆trans {[]} {g} {h} f<g g<h | |
130 3⊆trans {nothing ∷ f} {[]} {[]} f<g g<h = f<g | |
131 3⊆trans {nothing ∷ f} {[]} {just _ ∷ h} f<g g<h = 3⊆trans {f} {[]} {h} f<g (3⊆-[] {h}) | |
132 3⊆trans {nothing ∷ f} {[]} {nothing ∷ h} f<g g<h = 3⊆trans {f} {[]} {h} f<g g<h | |
133 3⊆trans {nothing ∷ f} {nothing ∷ g} {[]} f<g g<h = 3⊆trans {f} {g} {[]} f<g g<h | |
134 3⊆trans {nothing ∷ f} {nothing ∷ g} {just _ ∷ h} f<g g<h = 3⊆trans {f} {g} {h} f<g g<h | |
135 3⊆trans {nothing ∷ f} {nothing ∷ g} {nothing ∷ h} f<g g<h = 3⊆trans {f} {g} {h} f<g g<h | |
136 3⊆trans {[]} {just i0 ∷ g} {[]} f<g () | |
137 3⊆trans {[]} {just i1 ∷ g} {[]} f<g () | |
138 3⊆trans {[]} {just x ∷ g} {nothing ∷ h} f<g g<h = 3⊆-[] {h} | |
139 3⊆trans {just i0 ∷ f} {[]} {h} () g<h | |
140 3⊆trans {just i1 ∷ f} {[]} {h} () g<h | |
141 3⊆trans {just x ∷ f} {just i0 ∷ g} {[]} f<g () | |
142 3⊆trans {just x ∷ f} {just i1 ∷ g} {[]} f<g () | |
143 3⊆trans {just i0 ∷ f} {just i0 ∷ g} {just i0 ∷ h} f<g g<h = 3⊆trans {f} {g} {h} f<g g<h | |
144 3⊆trans {just i1 ∷ f} {just i1 ∷ g} {just i1 ∷ h} f<g g<h = 3⊆trans {f} {g} {h} f<g g<h | |
145 3⊆trans {just x ∷ f} {just i0 ∷ g} {nothing ∷ h} f<g () | |
146 3⊆trans {just x ∷ f} {just i1 ∷ g} {nothing ∷ h} f<g () | |
147 3⊆trans {just i0 ∷ f} {nothing ∷ g} {_} () g<h | |
148 3⊆trans {just i1 ∷ f} {nothing ∷ g} {_} () g<h | |
149 3⊆trans {nothing ∷ f} {just i0 ∷ g} {[]} f<g () | |
150 3⊆trans {nothing ∷ f} {just i1 ∷ g} {[]} f<g () | |
151 3⊆trans {nothing ∷ f} {just i0 ∷ g} {just i0 ∷ h} f<g g<h = 3⊆trans {f} {g} {h} f<g g<h | |
152 3⊆trans {nothing ∷ f} {just i1 ∷ g} {just i1 ∷ h} f<g g<h = 3⊆trans {f} {g} {h} f<g g<h | |
153 3⊆trans {nothing ∷ f} {just i0 ∷ g} {nothing ∷ h} f<g () | |
154 3⊆trans {nothing ∷ f} {just i1 ∷ g} {nothing ∷ h} f<g () | |
379 | 155 |
387 | 156 3⊆∩f : { f g h : List (Maybe Two) } → f 3⊆ g → f 3⊆ h → f 3⊆ (g 3∩ h ) |
381 | 157 3⊆∩f {[]} {[]} {[]} f<g f<h = refl |
158 3⊆∩f {[]} {[]} {x ∷ h} f<g f<h = 3⊆-[] {[] 3∩ (x ∷ h)} | |
159 3⊆∩f {[]} {x ∷ g} {h} f<g f<h = 3⊆-[] {(x ∷ g) 3∩ h} | |
387 | 160 3⊆∩f {nothing ∷ f} {[]} {[]} f<g f<h = 3⊆∩f {f} {[]} {[]} f<g f<h |
161 3⊆∩f {nothing ∷ f} {[]} {just _ ∷ h} f<g f<h = f<g | |
162 3⊆∩f {nothing ∷ f} {[]} {nothing ∷ h} f<g f<h = 3⊆∩f {f} {[]} {h} f<g f<h | |
163 3⊆∩f {just i0 ∷ f} {just i0 ∷ g} {just i0 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h | |
164 3⊆∩f {just i1 ∷ f} {just i1 ∷ g} {just i1 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h | |
165 3⊆∩f {nothing ∷ f} {just _ ∷ g} {[]} f<g f<h = f<h | |
166 3⊆∩f {nothing ∷ f} {just i0 ∷ g} {just i0 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h | |
167 3⊆∩f {nothing ∷ f} {just i0 ∷ g} {just i1 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h | |
168 3⊆∩f {nothing ∷ f} {just i1 ∷ g} {just i0 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h | |
169 3⊆∩f {nothing ∷ f} {just i1 ∷ g} {just i1 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h | |
170 3⊆∩f {nothing ∷ f} {just i0 ∷ g} {nothing ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h | |
171 3⊆∩f {nothing ∷ f} {just i1 ∷ g} {nothing ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h | |
172 3⊆∩f {nothing ∷ f} {nothing ∷ g} {[]} f<g f<h = 3⊆∩f {f} {g} {[]} f<g f<h | |
173 3⊆∩f {nothing ∷ f} {nothing ∷ g} {just _ ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h | |
174 3⊆∩f {nothing ∷ f} {nothing ∷ g} {nothing ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h | |
381 | 175 |
387 | 176 3↑22 : (f : Nat → Two) (i j : Nat) → List (Maybe Two) |
382 | 177 3↑22 f Zero j = [] |
387 | 178 3↑22 f (Suc i) j = just (f j) ∷ 3↑22 f i (Suc j) |
382 | 179 |
387 | 180 _3↑_ : (Nat → Two) → Nat → List (Maybe Two) |
384 | 181 _3↑_ f i = 3↑22 f i 0 |
381 | 182 |
384 | 183 3↑< : {f : Nat → Two} → { x y : Nat } → x ≤ y → (_3↑_ f x) 3⊆ (_3↑_ f y) |
184 3↑< {f} {x} {y} x<y = lemma x y 0 x<y where | |
383 | 185 lemma : (x y i : Nat) → x ≤ y → (3↑22 f x i ) 3⊆ (3↑22 f y i ) |
186 lemma 0 y i z≤n with f i | |
187 lemma Zero Zero i z≤n | i0 = refl | |
188 lemma Zero (Suc y) i z≤n | i0 = 3⊆-[] {3↑22 f (Suc y) i} | |
189 lemma Zero Zero i z≤n | i1 = refl | |
190 lemma Zero (Suc y) i z≤n | i1 = 3⊆-[] {3↑22 f (Suc y) i} | |
384 | 191 lemma (Suc x) (Suc y) i (s≤s x<y) with f i |
192 lemma (Suc x) (Suc y) i (s≤s x<y) | i0 = lemma x y (Suc i) x<y | |
193 lemma (Suc x) (Suc y) i (s≤s x<y) | i1 = lemma x y (Suc i) x<y | |
383 | 194 |
387 | 195 Finite3b : (p : List (Maybe Two) ) → Bool |
381 | 196 Finite3b [] = true |
387 | 197 Finite3b (just _ ∷ f) = Finite3b f |
198 Finite3b (nothing ∷ f) = false | |
381 | 199 |
387 | 200 finite3cov : (p : List (Maybe Two) ) → List (Maybe Two) |
381 | 201 finite3cov [] = [] |
387 | 202 finite3cov (just y ∷ x) = just y ∷ finite3cov x |
203 finite3cov (nothing ∷ x) = just i0 ∷ finite3cov x | |
381 | 204 |
387 | 205 Dense-3 : F-Dense (List (Maybe Two) ) (λ x → One) _3⊆_ _3∩_ |
381 | 206 Dense-3 = record { |
207 dense = λ x → Finite3b x ≡ true | |
208 ; d⊆P = OneObj | |
209 ; dense-f = λ x → finite3cov x | |
210 ; dense-d = λ {p} d → lemma1 p | |
211 ; dense-p = λ {p} d → lemma2 p | |
212 } where | |
387 | 213 lemma1 : (p : List (Maybe Two) ) → Finite3b (finite3cov p) ≡ true |
381 | 214 lemma1 [] = refl |
387 | 215 lemma1 (just i0 ∷ p) = lemma1 p |
216 lemma1 (just i1 ∷ p) = lemma1 p | |
217 lemma1 (nothing ∷ p) = lemma1 p | |
218 lemma2 : (p : List (Maybe Two)) → p 3⊆ finite3cov p | |
381 | 219 lemma2 [] = refl |
387 | 220 lemma2 (just i0 ∷ p) = lemma2 p |
221 lemma2 (just i1 ∷ p) = lemma2 p | |
222 lemma2 (nothing ∷ p) = lemma2 p | |
381 | 223 |
388 | 224 -- min = Data.Nat._⊓_ |
381 | 225 -- m≤m⊔n = Data.Nat._⊔_ |
388 | 226 -- open import Data.Nat.Properties |
381 | 227 |