Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison partfunc.agda @ 387:8b0715e28b33
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sat, 25 Jul 2020 09:09:00 +0900 |
parents | filter.agda@24a66a246316 |
children | 19687f3304c9 |
comparison
equal
deleted
inserted
replaced
386:24a66a246316 | 387:8b0715e28b33 |
---|---|
1 {-# OPTIONS --allow-unsolved-metas #-} | |
2 open import Level | |
3 open import Relation.Nullary | |
4 open import Relation.Binary.PropositionalEquality | |
5 open import Ordinals | |
6 module partfunc {n : Level } (O : Ordinals {n}) where | |
7 | |
8 open import logic | |
9 open import Relation.Binary | |
10 open import Data.Empty | |
11 open import Data.List | |
12 open import Data.Maybe | |
13 open import Relation.Binary | |
14 open import Relation.Binary.Core | |
15 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) | |
16 open import filter O | |
17 | |
18 open _∧_ | |
19 open _∨_ | |
20 open Bool | |
21 | |
22 | |
23 record PFunc (Dom : Set n) (Cod : Set n) : Set (suc n) where | |
24 field | |
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 | |
28 | |
29 | |
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) | |
33 | |
34 open PFunc | |
35 | |
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 | |
39 | |
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} | |
45 | |
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 } | |
51 | |
52 _3⊆b_ : (f g : List (Maybe Two)) → Bool | |
53 [] 3⊆b [] = true | |
54 [] 3⊆b (nothing ∷ g) = [] 3⊆b g | |
55 [] 3⊆b (_ ∷ g) = true | |
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 | |
60 _ 3⊆b _ = false | |
61 | |
62 _3⊆_ : (f g : List (Maybe Two)) → Set | |
63 f 3⊆ g = (f 3⊆b g) ≡ true | |
64 | |
65 _3∩_ : (f g : List (Maybe Two)) → List (Maybe Two) | |
66 [] 3∩ (nothing ∷ g) = nothing ∷ ([] 3∩ g) | |
67 [] 3∩ g = [] | |
68 (nothing ∷ f) 3∩ [] = nothing ∷ f 3∩ [] | |
69 f 3∩ [] = [] | |
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 ) | |
73 | |
74 3∩⊆f : { f g : List (Maybe Two) } → (f 3∩ g ) 3⊆ f | |
75 3∩⊆f {[]} {[]} = refl | |
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} | |
88 | |
89 3∩sym : { f g : List (Maybe Two) } → (f 3∩ g ) ≡ (g 3∩ f ) | |
90 3∩sym {[]} {[]} = refl | |
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}) | |
104 | |
105 3⊆-[] : { h : List (Maybe Two) } → [] 3⊆ h | |
106 3⊆-[] {[]} = refl | |
107 3⊆-[] {just _ ∷ h} = refl | |
108 3⊆-[] {nothing ∷ h} = 3⊆-[] {h} | |
109 | |
110 3⊆trans : { f g h : List (Maybe Two) } → f 3⊆ g → g 3⊆ h → f 3⊆ h | |
111 3⊆trans {[]} {[]} {[]} f<g g<h = refl | |
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 () | |
143 | |
144 3⊆∩f : { f g h : List (Maybe Two) } → f 3⊆ g → f 3⊆ h → f 3⊆ (g 3∩ h ) | |
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} | |
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 | |
163 | |
164 3↑22 : (f : Nat → Two) (i j : Nat) → List (Maybe Two) | |
165 3↑22 f Zero j = [] | |
166 3↑22 f (Suc i) j = just (f j) ∷ 3↑22 f i (Suc j) | |
167 | |
168 _3↑_ : (Nat → Two) → Nat → List (Maybe Two) | |
169 _3↑_ f i = 3↑22 f i 0 | |
170 | |
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 | |
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} | |
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 | |
182 | |
183 Finite3b : (p : List (Maybe Two) ) → Bool | |
184 Finite3b [] = true | |
185 Finite3b (just _ ∷ f) = Finite3b f | |
186 Finite3b (nothing ∷ f) = false | |
187 | |
188 finite3cov : (p : List (Maybe Two) ) → List (Maybe Two) | |
189 finite3cov [] = [] | |
190 finite3cov (just y ∷ x) = just y ∷ finite3cov x | |
191 finite3cov (nothing ∷ x) = just i0 ∷ finite3cov x | |
192 | |
193 Dense-3 : F-Dense (List (Maybe Two) ) (λ x → One) _3⊆_ _3∩_ | |
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 | |
201 lemma1 : (p : List (Maybe Two) ) → Finite3b (finite3cov p) ≡ true | |
202 lemma1 [] = refl | |
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 | |
207 lemma2 [] = refl | |
208 lemma2 (just i0 ∷ p) = lemma2 p | |
209 lemma2 (just i1 ∷ p) = lemma2 p | |
210 lemma2 (nothing ∷ p) = lemma2 p | |
211 | |
212 record 3Gf (f : Nat → Two) (p : List (Maybe Two)) : Set where | |
213 field | |
214 3gn : Nat | |
215 3f<n : p 3⊆ (f 3↑ 3gn) | |
216 | |
217 open 3Gf | |
218 | |
219 min = Data.Nat._⊓_ | |
220 -- m≤m⊔n = Data.Nat._⊔_ | |
221 open import Data.Nat.Properties | |
222 | |
223 3GF : {n : Level } → (Nat → Two ) → F-Filter (List (Maybe Two)) (λ x → One) _3⊆_ _3∩_ | |
224 3GF {n} f = record { | |
225 filter = λ p → 3Gf f p | |
226 ; f⊆P = OneObj | |
227 ; filter1 = λ {p} {q} _ fp p⊆q → lemma1 p q fp p⊆q | |
228 ; filter2 = λ {p} {q} fp fq → record { 3gn = min (3gn fp) (3gn fq) ; 3f<n = lemma2 p q fp fq } | |
229 } where | |
230 lemma1 : (p q : List (Maybe Two) ) → (fp : 3Gf f p) → (p⊆q : p 3⊆ q) → 3Gf f q | |
231 lemma1 p q fp p⊆q = record { 3gn = 3gn fp ; 3f<n = {!!} } | |
232 lemma2 : (p q : List (Maybe Two) ) → (fp : 3Gf f p) → (fq : 3Gf f q) → (p 3∩ q) 3⊆ (f 3↑ min (3gn fp) (3gn fq)) | |
233 lemma2 p q fp fq = ? |