Mercurial > hg > Members > kono > Proof > ZF-in-agda
annotate partfunc.agda @ 414:aa306f5dab9b
add VL
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 30 Jul 2020 16:06:36 +0900 |
| parents | 55f44ec2a0c6 |
| children | 9984cdd88da3 |
| 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 | |
| 295 | 22 |
| 387 | 23 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
|
24 field |
| 387 | 25 dom : Dom → Set n |
| 26 pmap : (x : Dom ) → dom x → Cod | |
| 27 meq : {x : Dom } → { p q : dom x } → pmap x p ≡ pmap x q | |
| 371 | 28 |
| 374 | 29 |
| 387 | 30 data Findp : {Cod : Set n} → List (Maybe Cod) → (x : Nat) → Set where |
| 31 v0 : {Cod : Set n} → {f : List (Maybe Cod)} → ( v : Cod ) → Findp ( just v ∷ f ) Zero | |
| 32 vn : {Cod : Set n} → {f : List (Maybe Cod)} {d : Maybe Cod} → {x : Nat} → Findp f x → Findp (d ∷ f) (Suc x) | |
| 379 | 33 |
| 34 open PFunc | |
| 35 | |
| 387 | 36 find : {Cod : Set n} → (f : List (Maybe Cod) ) → (x : Nat) → Findp f x → Cod |
| 37 find (just v ∷ _) 0 (v0 v) = v | |
| 38 find (_ ∷ n) (Suc i) (vn p) = find n i p | |
| 381 | 39 |
| 387 | 40 findpeq : {Cod : Set n} → (f : List (Maybe Cod)) → {x : Nat} {p q : Findp f x } → find f x p ≡ find f x q |
| 41 findpeq n {0} {v0 _} {v0 _} = refl | |
| 42 findpeq [] {Suc x} {()} | |
| 43 findpeq (just x₁ ∷ n) {Suc x} {vn p} {vn q} = findpeq n {x} {p} {q} | |
| 44 findpeq (nothing ∷ n) {Suc x} {vn p} {vn q} = findpeq n {x} {p} {q} | |
| 381 | 45 |
| 387 | 46 List→PFunc : {Cod : Set n} → List (Maybe Cod) → PFunc (Lift n Nat) Cod |
| 47 List→PFunc fp = record { dom = λ x → Lift n (Findp fp (lower x)) | |
| 48 ; pmap = λ x y → find fp (lower x) (lower y) | |
| 49 ; meq = λ {x} {p} {q} → findpeq fp {lower x} {lower p} {lower q} | |
| 50 } | |
| 381 | 51 |
| 387 | 52 _3⊆b_ : (f g : List (Maybe Two)) → Bool |
| 381 | 53 [] 3⊆b [] = true |
| 387 | 54 [] 3⊆b (nothing ∷ g) = [] 3⊆b g |
| 381 | 55 [] 3⊆b (_ ∷ g) = true |
| 387 | 56 (nothing ∷ f) 3⊆b [] = f 3⊆b [] |
| 57 (nothing ∷ f) 3⊆b (_ ∷ g) = f 3⊆b g | |
| 58 (just i0 ∷ f) 3⊆b (just i0 ∷ g) = f 3⊆b g | |
| 59 (just i1 ∷ f) 3⊆b (just i1 ∷ g) = f 3⊆b g | |
| 381 | 60 _ 3⊆b _ = false |
| 61 | |
| 387 | 62 _3⊆_ : (f g : List (Maybe Two)) → Set |
| 381 | 63 f 3⊆ g = (f 3⊆b g) ≡ true |
| 64 | |
| 387 | 65 _3∩_ : (f g : List (Maybe Two)) → List (Maybe Two) |
| 66 [] 3∩ (nothing ∷ g) = nothing ∷ ([] 3∩ g) | |
| 381 | 67 [] 3∩ g = [] |
| 387 | 68 (nothing ∷ f) 3∩ [] = nothing ∷ f 3∩ [] |
| 381 | 69 f 3∩ [] = [] |
| 387 | 70 (just i0 ∷ f) 3∩ (just i0 ∷ g) = just i0 ∷ ( f 3∩ g ) |
| 71 (just i1 ∷ f) 3∩ (just i1 ∷ g) = just i1 ∷ ( f 3∩ g ) | |
| 72 (_ ∷ f) 3∩ (_ ∷ g) = nothing ∷ ( f 3∩ g ) | |
| 381 | 73 |
| 387 | 74 3∩⊆f : { f g : List (Maybe Two) } → (f 3∩ g ) 3⊆ f |
| 381 | 75 3∩⊆f {[]} {[]} = refl |
| 387 | 76 3∩⊆f {[]} {just _ ∷ g} = refl |
| 77 3∩⊆f {[]} {nothing ∷ g} = 3∩⊆f {[]} {g} | |
| 78 3∩⊆f {just _ ∷ f} {[]} = refl | |
| 79 3∩⊆f {nothing ∷ f} {[]} = 3∩⊆f {f} {[]} | |
| 80 3∩⊆f {just i0 ∷ f} {just i0 ∷ g} = 3∩⊆f {f} {g} | |
| 81 3∩⊆f {just i1 ∷ f} {just i1 ∷ g} = 3∩⊆f {f} {g} | |
| 82 3∩⊆f {just i0 ∷ f} {just i1 ∷ g} = 3∩⊆f {f} {g} | |
| 83 3∩⊆f {just i1 ∷ f} {just i0 ∷ g} = 3∩⊆f {f} {g} | |
| 84 3∩⊆f {nothing ∷ f} {just _ ∷ g} = 3∩⊆f {f} {g} | |
| 85 3∩⊆f {just i0 ∷ f} {nothing ∷ g} = 3∩⊆f {f} {g} | |
| 86 3∩⊆f {just i1 ∷ f} {nothing ∷ g} = 3∩⊆f {f} {g} | |
| 87 3∩⊆f {nothing ∷ f} {nothing ∷ g} = 3∩⊆f {f} {g} | |
| 381 | 88 |
| 387 | 89 3∩sym : { f g : List (Maybe Two) } → (f 3∩ g ) ≡ (g 3∩ f ) |
| 381 | 90 3∩sym {[]} {[]} = refl |
| 387 | 91 3∩sym {[]} {just _ ∷ g} = refl |
| 92 3∩sym {[]} {nothing ∷ g} = cong (λ k → nothing ∷ k) (3∩sym {[]} {g}) | |
| 93 3∩sym {just _ ∷ f} {[]} = refl | |
| 94 3∩sym {nothing ∷ f} {[]} = cong (λ k → nothing ∷ k) (3∩sym {f} {[]}) | |
| 95 3∩sym {just i0 ∷ f} {just i0 ∷ g} = cong (λ k → just i0 ∷ k) (3∩sym {f} {g}) | |
| 96 3∩sym {just i0 ∷ f} {just i1 ∷ g} = cong (λ k → nothing ∷ k) (3∩sym {f} {g}) | |
| 97 3∩sym {just i1 ∷ f} {just i0 ∷ g} = cong (λ k → nothing ∷ k) (3∩sym {f} {g}) | |
| 98 3∩sym {just i1 ∷ f} {just i1 ∷ g} = cong (λ k → just i1 ∷ k) (3∩sym {f} {g}) | |
| 99 3∩sym {just i0 ∷ f} {nothing ∷ g} = cong (λ k → nothing ∷ k) (3∩sym {f} {g}) | |
| 100 3∩sym {just i1 ∷ f} {nothing ∷ g} = cong (λ k → nothing ∷ k) (3∩sym {f} {g}) | |
| 101 3∩sym {nothing ∷ f} {just i0 ∷ g} = cong (λ k → nothing ∷ k) (3∩sym {f} {g}) | |
| 102 3∩sym {nothing ∷ f} {just i1 ∷ g} = cong (λ k → nothing ∷ k) (3∩sym {f} {g}) | |
| 103 3∩sym {nothing ∷ f} {nothing ∷ g} = cong (λ k → nothing ∷ k) (3∩sym {f} {g}) | |
| 381 | 104 |
| 387 | 105 3⊆-[] : { h : List (Maybe Two) } → [] 3⊆ h |
| 381 | 106 3⊆-[] {[]} = refl |
| 387 | 107 3⊆-[] {just _ ∷ h} = refl |
| 108 3⊆-[] {nothing ∷ h} = 3⊆-[] {h} | |
| 381 | 109 |
| 387 | 110 3⊆trans : { f g h : List (Maybe Two) } → f 3⊆ g → g 3⊆ h → f 3⊆ h |
| 381 | 111 3⊆trans {[]} {[]} {[]} f<g g<h = refl |
| 387 | 112 3⊆trans {[]} {[]} {just _ ∷ h} f<g g<h = refl |
| 113 3⊆trans {[]} {[]} {nothing ∷ h} f<g g<h = 3⊆trans {[]} {[]} {h} refl g<h | |
| 114 3⊆trans {[]} {nothing ∷ g} {[]} f<g g<h = refl | |
| 115 3⊆trans {[]} {just _ ∷ g} {just _ ∷ h} f<g g<h = refl | |
| 116 3⊆trans {[]} {nothing ∷ g} {just _ ∷ h} f<g g<h = refl | |
| 117 3⊆trans {[]} {nothing ∷ g} {nothing ∷ h} f<g g<h = 3⊆trans {[]} {g} {h} f<g g<h | |
| 118 3⊆trans {nothing ∷ f} {[]} {[]} f<g g<h = f<g | |
| 119 3⊆trans {nothing ∷ f} {[]} {just _ ∷ h} f<g g<h = 3⊆trans {f} {[]} {h} f<g (3⊆-[] {h}) | |
| 120 3⊆trans {nothing ∷ f} {[]} {nothing ∷ h} f<g g<h = 3⊆trans {f} {[]} {h} f<g g<h | |
| 121 3⊆trans {nothing ∷ f} {nothing ∷ g} {[]} f<g g<h = 3⊆trans {f} {g} {[]} f<g g<h | |
| 122 3⊆trans {nothing ∷ f} {nothing ∷ g} {just _ ∷ h} f<g g<h = 3⊆trans {f} {g} {h} f<g g<h | |
| 123 3⊆trans {nothing ∷ f} {nothing ∷ g} {nothing ∷ h} f<g g<h = 3⊆trans {f} {g} {h} f<g g<h | |
| 124 3⊆trans {[]} {just i0 ∷ g} {[]} f<g () | |
| 125 3⊆trans {[]} {just i1 ∷ g} {[]} f<g () | |
| 126 3⊆trans {[]} {just x ∷ g} {nothing ∷ h} f<g g<h = 3⊆-[] {h} | |
| 127 3⊆trans {just i0 ∷ f} {[]} {h} () g<h | |
| 128 3⊆trans {just i1 ∷ f} {[]} {h} () g<h | |
| 129 3⊆trans {just x ∷ f} {just i0 ∷ g} {[]} f<g () | |
| 130 3⊆trans {just x ∷ f} {just i1 ∷ g} {[]} f<g () | |
| 131 3⊆trans {just i0 ∷ f} {just i0 ∷ g} {just i0 ∷ h} f<g g<h = 3⊆trans {f} {g} {h} f<g g<h | |
| 132 3⊆trans {just i1 ∷ f} {just i1 ∷ g} {just i1 ∷ h} f<g g<h = 3⊆trans {f} {g} {h} f<g g<h | |
| 133 3⊆trans {just x ∷ f} {just i0 ∷ g} {nothing ∷ h} f<g () | |
| 134 3⊆trans {just x ∷ f} {just i1 ∷ g} {nothing ∷ h} f<g () | |
| 135 3⊆trans {just i0 ∷ f} {nothing ∷ g} {_} () g<h | |
| 136 3⊆trans {just i1 ∷ f} {nothing ∷ g} {_} () g<h | |
| 137 3⊆trans {nothing ∷ f} {just i0 ∷ g} {[]} f<g () | |
| 138 3⊆trans {nothing ∷ f} {just i1 ∷ g} {[]} f<g () | |
| 139 3⊆trans {nothing ∷ f} {just i0 ∷ g} {just i0 ∷ h} f<g g<h = 3⊆trans {f} {g} {h} f<g g<h | |
| 140 3⊆trans {nothing ∷ f} {just i1 ∷ g} {just i1 ∷ h} f<g g<h = 3⊆trans {f} {g} {h} f<g g<h | |
| 141 3⊆trans {nothing ∷ f} {just i0 ∷ g} {nothing ∷ h} f<g () | |
| 142 3⊆trans {nothing ∷ f} {just i1 ∷ g} {nothing ∷ h} f<g () | |
| 379 | 143 |
| 387 | 144 3⊆∩f : { f g h : List (Maybe Two) } → f 3⊆ g → f 3⊆ h → f 3⊆ (g 3∩ h ) |
| 381 | 145 3⊆∩f {[]} {[]} {[]} f<g f<h = refl |
| 146 3⊆∩f {[]} {[]} {x ∷ h} f<g f<h = 3⊆-[] {[] 3∩ (x ∷ h)} | |
| 147 3⊆∩f {[]} {x ∷ g} {h} f<g f<h = 3⊆-[] {(x ∷ g) 3∩ h} | |
| 387 | 148 3⊆∩f {nothing ∷ f} {[]} {[]} f<g f<h = 3⊆∩f {f} {[]} {[]} f<g f<h |
| 149 3⊆∩f {nothing ∷ f} {[]} {just _ ∷ h} f<g f<h = f<g | |
| 150 3⊆∩f {nothing ∷ f} {[]} {nothing ∷ h} f<g f<h = 3⊆∩f {f} {[]} {h} f<g f<h | |
| 151 3⊆∩f {just i0 ∷ f} {just i0 ∷ g} {just i0 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h | |
| 152 3⊆∩f {just i1 ∷ f} {just i1 ∷ g} {just i1 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h | |
| 153 3⊆∩f {nothing ∷ f} {just _ ∷ g} {[]} f<g f<h = f<h | |
| 154 3⊆∩f {nothing ∷ f} {just i0 ∷ g} {just i0 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h | |
| 155 3⊆∩f {nothing ∷ f} {just i0 ∷ g} {just i1 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h | |
| 156 3⊆∩f {nothing ∷ f} {just i1 ∷ g} {just i0 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h | |
| 157 3⊆∩f {nothing ∷ f} {just i1 ∷ g} {just i1 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h | |
| 158 3⊆∩f {nothing ∷ f} {just i0 ∷ g} {nothing ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h | |
| 159 3⊆∩f {nothing ∷ f} {just i1 ∷ g} {nothing ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h | |
| 160 3⊆∩f {nothing ∷ f} {nothing ∷ g} {[]} f<g f<h = 3⊆∩f {f} {g} {[]} f<g f<h | |
| 161 3⊆∩f {nothing ∷ f} {nothing ∷ g} {just _ ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h | |
| 162 3⊆∩f {nothing ∷ f} {nothing ∷ g} {nothing ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h | |
| 381 | 163 |
| 387 | 164 3↑22 : (f : Nat → Two) (i j : Nat) → List (Maybe Two) |
| 382 | 165 3↑22 f Zero j = [] |
| 387 | 166 3↑22 f (Suc i) j = just (f j) ∷ 3↑22 f i (Suc j) |
| 382 | 167 |
| 387 | 168 _3↑_ : (Nat → Two) → Nat → List (Maybe Two) |
| 384 | 169 _3↑_ f i = 3↑22 f i 0 |
| 381 | 170 |
| 384 | 171 3↑< : {f : Nat → Two} → { x y : Nat } → x ≤ y → (_3↑_ f x) 3⊆ (_3↑_ f y) |
| 172 3↑< {f} {x} {y} x<y = lemma x y 0 x<y where | |
| 383 | 173 lemma : (x y i : Nat) → x ≤ y → (3↑22 f x i ) 3⊆ (3↑22 f y i ) |
| 174 lemma 0 y i z≤n with f i | |
| 175 lemma Zero Zero i z≤n | i0 = refl | |
| 176 lemma Zero (Suc y) i z≤n | i0 = 3⊆-[] {3↑22 f (Suc y) i} | |
| 177 lemma Zero Zero i z≤n | i1 = refl | |
| 178 lemma Zero (Suc y) i z≤n | i1 = 3⊆-[] {3↑22 f (Suc y) i} | |
| 384 | 179 lemma (Suc x) (Suc y) i (s≤s x<y) with f i |
| 180 lemma (Suc x) (Suc y) i (s≤s x<y) | i0 = lemma x y (Suc i) x<y | |
| 181 lemma (Suc x) (Suc y) i (s≤s x<y) | i1 = lemma x y (Suc i) x<y | |
| 383 | 182 |
| 387 | 183 Finite3b : (p : List (Maybe Two) ) → Bool |
| 381 | 184 Finite3b [] = true |
| 387 | 185 Finite3b (just _ ∷ f) = Finite3b f |
| 186 Finite3b (nothing ∷ f) = false | |
| 381 | 187 |
| 387 | 188 finite3cov : (p : List (Maybe Two) ) → List (Maybe Two) |
| 381 | 189 finite3cov [] = [] |
| 387 | 190 finite3cov (just y ∷ x) = just y ∷ finite3cov x |
| 191 finite3cov (nothing ∷ x) = just i0 ∷ finite3cov x | |
| 381 | 192 |
| 387 | 193 Dense-3 : F-Dense (List (Maybe Two) ) (λ x → One) _3⊆_ _3∩_ |
| 381 | 194 Dense-3 = record { |
| 195 dense = λ x → Finite3b x ≡ true | |
| 196 ; d⊆P = OneObj | |
| 197 ; dense-f = λ x → finite3cov x | |
| 198 ; dense-d = λ {p} d → lemma1 p | |
| 199 ; dense-p = λ {p} d → lemma2 p | |
| 200 } where | |
| 387 | 201 lemma1 : (p : List (Maybe Two) ) → Finite3b (finite3cov p) ≡ true |
| 381 | 202 lemma1 [] = refl |
| 387 | 203 lemma1 (just i0 ∷ p) = lemma1 p |
| 204 lemma1 (just i1 ∷ p) = lemma1 p | |
| 205 lemma1 (nothing ∷ p) = lemma1 p | |
| 206 lemma2 : (p : List (Maybe Two)) → p 3⊆ finite3cov p | |
| 381 | 207 lemma2 [] = refl |
| 387 | 208 lemma2 (just i0 ∷ p) = lemma2 p |
| 209 lemma2 (just i1 ∷ p) = lemma2 p | |
| 210 lemma2 (nothing ∷ p) = lemma2 p | |
| 381 | 211 |
| 388 | 212 -- min = Data.Nat._⊓_ |
| 381 | 213 -- m≤m⊔n = Data.Nat._⊔_ |
| 388 | 214 -- open import Data.Nat.Properties |
| 381 | 215 |