|
141
|
1 module FSetUtil where
|
|
|
2
|
|
|
3 open import Data.Nat hiding ( _≟_ )
|
|
|
4 open import Data.Fin renaming ( _<_ to _<<_ ) hiding (_≤_)
|
|
|
5 open import Data.Fin.Properties
|
|
|
6 open import Data.Empty
|
|
|
7 open import Relation.Nullary
|
|
|
8 open import Relation.Binary.Definitions
|
|
|
9 open import Relation.Binary.PropositionalEquality
|
|
|
10 open import logic
|
|
|
11 open import nat
|
|
|
12 open import finiteSet
|
|
|
13 open import Data.Nat.Properties as NatP hiding ( _≟_ )
|
|
|
14 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
|
|
|
15
|
|
|
16 record ISO (A B : Set) : Set where
|
|
|
17 field
|
|
|
18 A←B : B → A
|
|
|
19 B←A : A → B
|
|
|
20 iso← : (q : A) → A←B ( B←A q ) ≡ q
|
|
|
21 iso→ : (f : B) → B←A ( A←B f ) ≡ f
|
|
|
22
|
|
|
23 iso-fin : {A B : Set} → FiniteSet A → ISO A B → FiniteSet B
|
|
|
24 iso-fin {A} {B} fin iso = record {
|
|
|
25 Q←F = λ f → ISO.B←A iso ( FiniteSet.Q←F fin f )
|
|
|
26 ; F←Q = λ b → FiniteSet.F←Q fin ( ISO.A←B iso b )
|
|
|
27 ; finiso→ = finiso→
|
|
|
28 ; finiso← = finiso←
|
|
|
29 } where
|
|
|
30 finiso→ : (q : B) → ISO.B←A iso (FiniteSet.Q←F fin (FiniteSet.F←Q fin (ISO.A←B iso q))) ≡ q
|
|
|
31 finiso→ q = begin
|
|
|
32 ISO.B←A iso (FiniteSet.Q←F fin (FiniteSet.F←Q fin (ISO.A←B iso q)))
|
|
|
33 ≡⟨ cong (λ k → ISO.B←A iso k ) (FiniteSet.finiso→ fin _ ) ⟩
|
|
|
34 ISO.B←A iso (ISO.A←B iso q)
|
|
|
35 ≡⟨ ISO.iso→ iso _ ⟩
|
|
|
36 q
|
|
|
37 ∎ where
|
|
|
38 open ≡-Reasoning
|
|
|
39 finiso← : (f : Fin (FiniteSet.finite fin ))→ FiniteSet.F←Q fin (ISO.A←B iso (ISO.B←A iso (FiniteSet.Q←F fin f))) ≡ f
|
|
|
40 finiso← f = begin
|
|
|
41 FiniteSet.F←Q fin (ISO.A←B iso (ISO.B←A iso (FiniteSet.Q←F fin f)))
|
|
|
42 ≡⟨ cong (λ k → FiniteSet.F←Q fin k ) (ISO.iso← iso _) ⟩
|
|
|
43 FiniteSet.F←Q fin (FiniteSet.Q←F fin f)
|
|
|
44 ≡⟨ FiniteSet.finiso← fin _ ⟩
|
|
|
45 f
|
|
|
46 ∎ where
|
|
|
47 open ≡-Reasoning
|
|
|
48
|
|
|
49 data One : Set where
|
|
|
50 one : One
|
|
|
51
|
|
|
52 fin-∨1 : {B : Set} → (fb : FiniteSet B ) → FiniteSet (One ∨ B)
|
|
|
53 fin-∨1 {B} fb = record {
|
|
|
54 Q←F = Q←F
|
|
|
55 ; F←Q = F←Q
|
|
|
56 ; finiso→ = finiso→
|
|
|
57 ; finiso← = finiso←
|
|
|
58 } where
|
|
|
59 b = FiniteSet.finite fb
|
|
|
60 Q←F : Fin (suc b) → One ∨ B
|
|
|
61 Q←F zero = case1 one
|
|
|
62 Q←F (suc f) = case2 (FiniteSet.Q←F fb f)
|
|
|
63 F←Q : One ∨ B → Fin (suc b)
|
|
|
64 F←Q (case1 one) = zero
|
|
|
65 F←Q (case2 f ) = suc (FiniteSet.F←Q fb f)
|
|
|
66 finiso→ : (q : One ∨ B) → Q←F (F←Q q) ≡ q
|
|
|
67 finiso→ (case1 one) = refl
|
|
|
68 finiso→ (case2 b) = cong (λ k → case2 k ) (FiniteSet.finiso→ fb b)
|
|
|
69 finiso← : (q : Fin (suc b)) → F←Q (Q←F q) ≡ q
|
|
|
70 finiso← zero = refl
|
|
|
71 finiso← (suc f) = cong ( λ k → suc k ) (FiniteSet.finiso← fb f)
|
|
|
72
|
|
|
73
|
|
|
74 fin-∨2 : {B : Set} → ( a : ℕ ) → FiniteSet B → FiniteSet (Fin a ∨ B)
|
|
|
75 fin-∨2 {B} zero fb = iso-fin fb iso where
|
|
|
76 iso : ISO B (Fin zero ∨ B)
|
|
|
77 iso = record {
|
|
|
78 A←B = A←B
|
|
|
79 ; B←A = λ b → case2 b
|
|
|
80 ; iso→ = iso→
|
|
|
81 ; iso← = λ _ → refl
|
|
|
82 } where
|
|
|
83 A←B : Fin zero ∨ B → B
|
|
|
84 A←B (case2 x) = x
|
|
|
85 iso→ : (f : Fin zero ∨ B ) → case2 (A←B f) ≡ f
|
|
|
86 iso→ (case2 x) = refl
|
|
|
87 fin-∨2 {B} (suc a) fb = iso-fin (fin-∨1 (fin-∨2 a fb) ) iso
|
|
|
88 where
|
|
|
89 iso : ISO (One ∨ (Fin a ∨ B) ) (Fin (suc a) ∨ B)
|
|
|
90 ISO.A←B iso (case1 zero) = case1 one
|
|
|
91 ISO.A←B iso (case1 (suc f)) = case2 (case1 f)
|
|
|
92 ISO.A←B iso (case2 b) = case2 (case2 b)
|
|
|
93 ISO.B←A iso (case1 one) = case1 zero
|
|
|
94 ISO.B←A iso (case2 (case1 f)) = case1 (suc f)
|
|
|
95 ISO.B←A iso (case2 (case2 b)) = case2 b
|
|
|
96 ISO.iso← iso (case1 one) = refl
|
|
|
97 ISO.iso← iso (case2 (case1 x)) = refl
|
|
|
98 ISO.iso← iso (case2 (case2 x)) = refl
|
|
|
99 ISO.iso→ iso (case1 zero) = refl
|
|
|
100 ISO.iso→ iso (case1 (suc x)) = refl
|
|
|
101 ISO.iso→ iso (case2 x) = refl
|
|
|
102
|
|
|
103
|
|
|
104 FiniteSet→Fin : {A : Set} → (fin : FiniteSet A ) → ISO (Fin (FiniteSet.finite fin)) A
|
|
|
105 ISO.A←B (FiniteSet→Fin fin) f = FiniteSet.F←Q fin f
|
|
|
106 ISO.B←A (FiniteSet→Fin fin) f = FiniteSet.Q←F fin f
|
|
|
107 ISO.iso← (FiniteSet→Fin fin) = FiniteSet.finiso← fin
|
|
|
108 ISO.iso→ (FiniteSet→Fin fin) = FiniteSet.finiso→ fin
|
|
|
109
|
|
|
110
|
|
|
111 fin-∨ : {A B : Set} → FiniteSet A → FiniteSet B → FiniteSet (A ∨ B)
|
|
|
112 fin-∨ {A} {B} fa fb = iso-fin (fin-∨2 a fb ) iso2 where
|
|
|
113 a = FiniteSet.finite fa
|
|
|
114 ia = FiniteSet→Fin fa
|
|
|
115 iso2 : ISO (Fin a ∨ B ) (A ∨ B)
|
|
|
116 ISO.A←B iso2 (case1 x) = case1 ( ISO.A←B ia x )
|
|
|
117 ISO.A←B iso2 (case2 x) = case2 x
|
|
|
118 ISO.B←A iso2 (case1 x) = case1 ( ISO.B←A ia x )
|
|
|
119 ISO.B←A iso2 (case2 x) = case2 x
|
|
|
120 ISO.iso← iso2 (case1 x) = cong ( λ k → case1 k ) (ISO.iso← ia x)
|
|
|
121 ISO.iso← iso2 (case2 x) = refl
|
|
|
122 ISO.iso→ iso2 (case1 x) = cong ( λ k → case1 k ) (ISO.iso→ ia x)
|
|
|
123 ISO.iso→ iso2 (case2 x) = refl
|
|
|
124
|
|
|
125 open import Data.Product
|
|
|
126
|
|
|
127 fin-× : {A B : Set} → FiniteSet A → FiniteSet B → FiniteSet (A × B)
|
|
|
128 fin-× {A} {B} fa fb with FiniteSet→Fin fa
|
|
|
129 ... | a=f = iso-fin (fin-×-f a ) iso-1 where
|
|
|
130 a = FiniteSet.finite fa
|
|
|
131 b = FiniteSet.finite fb
|
|
|
132 iso-1 : ISO (Fin a × B) ( A × B )
|
|
|
133 ISO.A←B iso-1 x = ( FiniteSet.F←Q fa (proj₁ x) , proj₂ x)
|
|
|
134 ISO.B←A iso-1 x = ( FiniteSet.Q←F fa (proj₁ x) , proj₂ x)
|
|
|
135 ISO.iso← iso-1 x = lemma where
|
|
|
136 lemma : (FiniteSet.F←Q fa (FiniteSet.Q←F fa (proj₁ x)) , proj₂ x) ≡ ( proj₁ x , proj₂ x )
|
|
|
137 lemma = cong ( λ k → ( k , proj₂ x ) ) (FiniteSet.finiso← fa _ )
|
|
|
138 ISO.iso→ iso-1 x = cong ( λ k → ( k , proj₂ x ) ) (FiniteSet.finiso→ fa _ )
|
|
|
139
|
|
|
140 iso-2 : {a : ℕ } → ISO (B ∨ (Fin a × B)) (Fin (suc a) × B)
|
|
|
141 ISO.A←B iso-2 (zero , b ) = case1 b
|
|
|
142 ISO.A←B iso-2 (suc fst , b ) = case2 ( fst , b )
|
|
|
143 ISO.B←A iso-2 (case1 b) = ( zero , b )
|
|
|
144 ISO.B←A iso-2 (case2 (a , b )) = ( suc a , b )
|
|
|
145 ISO.iso← iso-2 (case1 x) = refl
|
|
|
146 ISO.iso← iso-2 (case2 x) = refl
|
|
|
147 ISO.iso→ iso-2 (zero , b ) = refl
|
|
|
148 ISO.iso→ iso-2 (suc a , b ) = refl
|
|
|
149
|
|
|
150 fin-×-f : ( a : ℕ ) → FiniteSet ((Fin a) × B)
|
|
|
151 fin-×-f zero = record { Q←F = λ () ; F←Q = λ () ; finiso→ = λ () ; finiso← = λ () ; finite = 0 }
|
|
|
152 fin-×-f (suc a) = iso-fin ( fin-∨ fb ( fin-×-f a ) ) iso-2
|
|
|
153
|
|
|
154 open _∧_
|
|
|
155
|
|
|
156 fin-∧ : {A B : Set} → FiniteSet A → FiniteSet B → FiniteSet (A ∧ B)
|
|
|
157 fin-∧ {A} {B} fa fb with FiniteSet→Fin fa -- same thing for our tool
|
|
|
158 ... | a=f = iso-fin (fin-×-f a ) iso-1 where
|
|
|
159 a = FiniteSet.finite fa
|
|
|
160 b = FiniteSet.finite fb
|
|
|
161 iso-1 : ISO (Fin a ∧ B) ( A ∧ B )
|
|
|
162 ISO.A←B iso-1 x = record { proj1 = FiniteSet.F←Q fa (proj1 x) ; proj2 = proj2 x}
|
|
|
163 ISO.B←A iso-1 x = record { proj1 = FiniteSet.Q←F fa (proj1 x) ; proj2 = proj2 x}
|
|
|
164 ISO.iso← iso-1 x = lemma where
|
|
|
165 lemma : record { proj1 = FiniteSet.F←Q fa (FiniteSet.Q←F fa (proj1 x)) ; proj2 = proj2 x} ≡ record {proj1 = proj1 x ; proj2 = proj2 x }
|
|
|
166 lemma = cong ( λ k → record {proj1 = k ; proj2 = proj2 x } ) (FiniteSet.finiso← fa _ )
|
|
|
167 ISO.iso→ iso-1 x = cong ( λ k → record {proj1 = k ; proj2 = proj2 x } ) (FiniteSet.finiso→ fa _ )
|
|
|
168
|
|
|
169 iso-2 : {a : ℕ } → ISO (B ∨ (Fin a ∧ B)) (Fin (suc a) ∧ B)
|
|
|
170 ISO.A←B iso-2 (record { proj1 = zero ; proj2 = b }) = case1 b
|
|
|
171 ISO.A←B iso-2 (record { proj1 = suc fst ; proj2 = b }) = case2 ( record { proj1 = fst ; proj2 = b } )
|
|
|
172 ISO.B←A iso-2 (case1 b) = record {proj1 = zero ; proj2 = b }
|
|
|
173 ISO.B←A iso-2 (case2 (record { proj1 = a ; proj2 = b })) = record { proj1 = suc a ; proj2 = b }
|
|
|
174 ISO.iso← iso-2 (case1 x) = refl
|
|
|
175 ISO.iso← iso-2 (case2 x) = refl
|
|
|
176 ISO.iso→ iso-2 (record { proj1 = zero ; proj2 = b }) = refl
|
|
|
177 ISO.iso→ iso-2 (record { proj1 = suc a ; proj2 = b }) = refl
|
|
|
178
|
|
|
179 fin-×-f : ( a : ℕ ) → FiniteSet ((Fin a) ∧ B)
|
|
|
180 fin-×-f zero = record { Q←F = λ () ; F←Q = λ () ; finiso→ = λ () ; finiso← = λ () ; finite = 0 }
|
|
|
181 fin-×-f (suc a) = iso-fin ( fin-∨ fb ( fin-×-f a ) ) iso-2
|
|
|
182
|
|
|
183 -- import Data.Nat.DivMod
|
|
|
184
|
|
|
185 open import Data.Vec
|
|
|
186 import Data.Product
|
|
|
187
|
|
|
188 exp2 : (n : ℕ ) → exp 2 (suc n) ≡ exp 2 n Data.Nat.+ exp 2 n
|
|
|
189 exp2 n = begin
|
|
|
190 exp 2 (suc n)
|
|
|
191 ≡⟨⟩
|
|
|
192 2 * ( exp 2 n )
|
|
|
193 ≡⟨ *-comm 2 (exp 2 n) ⟩
|
|
|
194 ( exp 2 n ) * 2
|
|
|
195 ≡⟨ *-suc ( exp 2 n ) 1 ⟩
|
|
|
196 (exp 2 n ) Data.Nat.+ ( exp 2 n ) * 1
|
|
|
197 ≡⟨ cong ( λ k → (exp 2 n ) Data.Nat.+ k ) (proj₂ *-identity (exp 2 n) ) ⟩
|
|
|
198 exp 2 n Data.Nat.+ exp 2 n
|
|
|
199 ∎ where
|
|
|
200 open ≡-Reasoning
|
|
|
201 open Data.Product
|
|
|
202
|
|
|
203 cast-iso : {n m : ℕ } → (eq : n ≡ m ) → (f : Fin m ) → cast eq ( cast (sym eq ) f) ≡ f
|
|
|
204 cast-iso refl zero = refl
|
|
|
205 cast-iso refl (suc f) = cong ( λ k → suc k ) ( cast-iso refl f )
|
|
|
206
|
|
|
207
|
|
|
208 fin2List : {n : ℕ } → FiniteSet (Vec Bool n)
|
|
|
209 fin2List {zero} = record {
|
|
|
210 Q←F = λ _ → Vec.[]
|
|
|
211 ; F←Q = λ _ → # 0
|
|
|
212 ; finiso→ = finiso→
|
|
|
213 ; finiso← = finiso←
|
|
|
214 } where
|
|
|
215 Q = Vec Bool zero
|
|
|
216 finiso→ : (q : Q) → [] ≡ q
|
|
|
217 finiso→ [] = refl
|
|
|
218 finiso← : (f : Fin (exp 2 zero)) → # 0 ≡ f
|
|
|
219 finiso← zero = refl
|
|
|
220 fin2List {suc n} = subst (λ k → FiniteSet (Vec Bool (suc n)) ) (sym (exp2 n)) ( iso-fin (fin-∨ (fin2List ) (fin2List )) iso )
|
|
|
221 where
|
|
|
222 QtoR : Vec Bool (suc n) → Vec Bool n ∨ Vec Bool n
|
|
|
223 QtoR ( true ∷ x ) = case1 x
|
|
|
224 QtoR ( false ∷ x ) = case2 x
|
|
|
225 RtoQ : Vec Bool n ∨ Vec Bool n → Vec Bool (suc n)
|
|
|
226 RtoQ ( case1 x ) = true ∷ x
|
|
|
227 RtoQ ( case2 x ) = false ∷ x
|
|
|
228 isoRQ : (x : Vec Bool (suc n) ) → RtoQ ( QtoR x ) ≡ x
|
|
|
229 isoRQ (true ∷ _ ) = refl
|
|
|
230 isoRQ (false ∷ _ ) = refl
|
|
|
231 isoQR : (x : Vec Bool n ∨ Vec Bool n ) → QtoR ( RtoQ x ) ≡ x
|
|
|
232 isoQR (case1 x) = refl
|
|
|
233 isoQR (case2 x) = refl
|
|
|
234 iso : ISO (Vec Bool n ∨ Vec Bool n) (Vec Bool (suc n))
|
|
|
235 iso = record { A←B = QtoR ; B←A = RtoQ ; iso← = isoQR ; iso→ = isoRQ }
|
|
|
236
|
|
|
237 F2L : {Q : Set } {n : ℕ } → (fin : FiniteSet Q ) → n < suc (FiniteSet.finite fin) → ( (q : Q) → toℕ (FiniteSet.F←Q fin q ) < n → Bool ) → Vec Bool n
|
|
|
238 F2L {Q} {zero} fin _ Q→B = []
|
|
|
239 F2L {Q} {suc n} fin (s≤s n<m) Q→B = Q→B (FiniteSet.Q←F fin (fromℕ< n<m)) lemma6 ∷ F2L {Q} fin (NatP.<-trans n<m a<sa ) qb1 where
|
|
|
240 lemma6 : toℕ (FiniteSet.F←Q fin (FiniteSet.Q←F fin (fromℕ< n<m))) < suc n
|
|
|
241 lemma6 = subst (λ k → toℕ k < suc n ) (sym (FiniteSet.finiso← fin _ )) (subst (λ k → k < suc n) (sym (toℕ-fromℕ< n<m )) a<sa )
|
|
|
242 qb1 : (q : Q) → toℕ (FiniteSet.F←Q fin q) < n → Bool
|
|
|
243 qb1 q q<n = Q→B q (NatP.<-trans q<n a<sa)
|
|
|
244
|
|
|
245 List2Func : { Q : Set } → {n : ℕ } → (fin : FiniteSet Q ) → n < suc (FiniteSet.finite fin) → Vec Bool n → Q → Bool
|
|
|
246 List2Func {Q} {zero} fin (s≤s z≤n) [] q = false
|
|
|
247 List2Func {Q} {suc n} fin (s≤s n<m) (h ∷ t) q with FiniteSet.F←Q fin q ≟ fromℕ< n<m
|
|
|
248 ... | yes _ = h
|
|
|
249 ... | no _ = List2Func {Q} fin (NatP.<-trans n<m a<sa ) t q
|
|
|
250
|
|
|
251 open import Level renaming ( suc to Suc ; zero to Zero)
|
|
|
252 open import Axiom.Extensionality.Propositional
|
|
|
253 postulate f-extensionality : { n : Level} → Axiom.Extensionality.Propositional.Extensionality n n
|
|
|
254
|
|
|
255 F2L-iso : { Q : Set } → (fin : FiniteSet Q ) → (x : Vec Bool (FiniteSet.finite fin) ) → F2L fin a<sa (λ q _ → List2Func fin a<sa x q ) ≡ x
|
|
|
256 F2L-iso {Q} fin x = f2l m a<sa x where
|
|
|
257 m = FiniteSet.finite fin
|
|
|
258 f2l : (n : ℕ ) → (n<m : n < suc m )→ (x : Vec Bool n ) → F2L fin n<m (λ q q<n → List2Func fin n<m x q ) ≡ x
|
|
|
259 f2l zero (s≤s z≤n) [] = refl
|
|
|
260 f2l (suc n) (s≤s n<m) (h ∷ t ) = lemma1 lemma2 lemma3 where
|
|
|
261 lemma1 : {n : ℕ } → {h h1 : Bool } → {t t1 : Vec Bool n } → h ≡ h1 → t ≡ t1 → h ∷ t ≡ h1 ∷ t1
|
|
|
262 lemma1 refl refl = refl
|
|
|
263 lemma2 : List2Func fin (s≤s n<m) (h ∷ t) (FiniteSet.Q←F fin (fromℕ< n<m)) ≡ h
|
|
|
264 lemma2 with FiniteSet.F←Q fin (FiniteSet.Q←F fin (fromℕ< n<m)) ≟ fromℕ< n<m
|
|
|
265 lemma2 | yes p = refl
|
|
|
266 lemma2 | no ¬p = ⊥-elim ( ¬p (FiniteSet.finiso← fin _) )
|
|
|
267 lemma4 : (q : Q ) → toℕ (FiniteSet.F←Q fin q ) < n → List2Func fin (s≤s n<m) (h ∷ t) q ≡ List2Func fin (NatP.<-trans n<m a<sa) t q
|
|
|
268 lemma4 q _ with FiniteSet.F←Q fin q ≟ fromℕ< n<m
|
|
|
269 lemma4 q lt | yes p = ⊥-elim ( nat-≡< (toℕ-fromℕ< n<m) (lemma5 n lt (cong (λ k → toℕ k) p))) where
|
|
|
270 lemma5 : {j k : ℕ } → ( n : ℕ) → suc j ≤ n → j ≡ k → k < n
|
|
|
271 lemma5 {zero} (suc n) (s≤s z≤n) refl = s≤s z≤n
|
|
|
272 lemma5 {suc j} (suc n) (s≤s lt) refl = s≤s (lemma5 {j} n lt refl)
|
|
|
273 lemma4 q _ | no ¬p = refl
|
|
|
274 lemma3 : F2L fin (NatP.<-trans n<m a<sa) (λ q q<n → List2Func fin (s≤s n<m) (h ∷ t) q ) ≡ t
|
|
|
275 lemma3 = begin
|
|
|
276 F2L fin (NatP.<-trans n<m a<sa) (λ q q<n → List2Func fin (s≤s n<m) (h ∷ t) q )
|
|
|
277 ≡⟨ cong (λ k → F2L fin (NatP.<-trans n<m a<sa) ( λ q q<n → k q q<n ))
|
|
|
278 (f-extensionality ( λ q →
|
|
|
279 (f-extensionality ( λ q<n → lemma4 q q<n )))) ⟩
|
|
|
280 F2L fin (NatP.<-trans n<m a<sa) (λ q q<n → List2Func fin (NatP.<-trans n<m a<sa) t q )
|
|
|
281 ≡⟨ f2l n (NatP.<-trans n<m a<sa ) t ⟩
|
|
|
282 t
|
|
|
283 ∎ where
|
|
|
284 open ≡-Reasoning
|
|
|
285
|
|
|
286
|
|
|
287 L2F : {Q : Set } {n : ℕ } → (fin : FiniteSet Q ) → n < suc (FiniteSet.finite fin) → Vec Bool n → (q : Q ) → toℕ (FiniteSet.F←Q fin q ) < n → Bool
|
|
|
288 L2F fin n<m x q q<n = List2Func fin n<m x q
|
|
|
289
|
|
|
290 L2F-iso : { Q : Set } → (fin : FiniteSet Q ) → (f : Q → Bool ) → (q : Q ) → (L2F fin a<sa (F2L fin a<sa (λ q _ → f q) )) q (toℕ<n _) ≡ f q
|
|
|
291 L2F-iso {Q} fin f q = l2f m a<sa (toℕ<n _) where
|
|
|
292 m = FiniteSet.finite fin
|
|
|
293 lemma11 : {n : ℕ } → (n<m : n < m ) → ¬ ( FiniteSet.F←Q fin q ≡ fromℕ< n<m ) → toℕ (FiniteSet.F←Q fin q) ≤ n → toℕ (FiniteSet.F←Q fin q) < n
|
|
|
294 lemma11 n<m ¬q=n q≤n = lemma13 n<m (contra-position (lemma12 n<m _) ¬q=n ) q≤n where
|
|
|
295 lemma13 : {n nq : ℕ } → (n<m : n < m ) → ¬ ( nq ≡ n ) → nq ≤ n → nq < n
|
|
|
296 lemma13 {0} {0} (s≤s z≤n) nt z≤n = ⊥-elim ( nt refl )
|
|
|
297 lemma13 {suc _} {0} (s≤s (s≤s n<m)) nt z≤n = s≤s z≤n
|
|
|
298 lemma13 {suc n} {suc nq} n<m nt (s≤s nq≤n) = s≤s (lemma13 {n} {nq} (NatP.<-trans a<sa n<m ) (λ eq → nt ( cong ( λ k → suc k ) eq )) nq≤n)
|
|
|
299 lemma3 : {a b : ℕ } → (lt : a < b ) → fromℕ< (s≤s lt) ≡ suc (fromℕ< lt)
|
|
|
300 lemma3 (s≤s lt) = refl
|
|
|
301 lemma12 : {n m : ℕ } → (n<m : n < m ) → (f : Fin m ) → toℕ f ≡ n → f ≡ fromℕ< n<m
|
|
|
302 lemma12 {zero} {suc m} (s≤s z≤n) zero refl = refl
|
|
|
303 lemma12 {suc n} {suc m} (s≤s n<m) (suc f) refl = subst ( λ k → suc f ≡ k ) (sym (lemma3 n<m) ) ( cong ( λ k → suc k ) ( lemma12 {n} {m} n<m f refl ) )
|
|
|
304 l2f : (n : ℕ ) → (n<m : n < suc m ) → (q<n : toℕ (FiniteSet.F←Q fin q ) < n ) → (L2F fin n<m (F2L fin n<m (λ q _ → f q))) q q<n ≡ f q
|
|
|
305 l2f zero (s≤s z≤n) ()
|
|
|
306 l2f (suc n) (s≤s n<m) (s≤s n<q) with FiniteSet.F←Q fin q ≟ fromℕ< n<m
|
|
|
307 l2f (suc n) (s≤s n<m) (s≤s n<q) | yes p = begin
|
|
|
308 f (FiniteSet.Q←F fin (fromℕ< n<m))
|
|
|
309 ≡⟨ cong ( λ k → f (FiniteSet.Q←F fin k )) (sym p) ⟩
|
|
|
310 f (FiniteSet.Q←F fin ( FiniteSet.F←Q fin q ))
|
|
|
311 ≡⟨ cong ( λ k → f k ) (FiniteSet.finiso→ fin _ ) ⟩
|
|
|
312 f q
|
|
|
313 ∎ where
|
|
|
314 open ≡-Reasoning
|
|
|
315 l2f (suc n) (s≤s n<m) (s≤s n<q) | no ¬p = l2f n (NatP.<-trans n<m a<sa) (lemma11 n<m ¬p n<q)
|
|
|
316
|
|
|
317 fin→ : {A : Set} → FiniteSet A → FiniteSet (A → Bool )
|
|
|
318 fin→ {A} fin = iso-fin fin2List iso where
|
|
|
319 a = FiniteSet.finite fin
|
|
|
320 iso : ISO (Vec Bool a ) (A → Bool)
|
|
|
321 ISO.A←B iso x = F2L fin a<sa ( λ q _ → x q )
|
|
|
322 ISO.B←A iso x = List2Func fin a<sa x
|
|
|
323 ISO.iso← iso x = F2L-iso fin x
|
|
|
324 ISO.iso→ iso x = lemma where
|
|
|
325 lemma : List2Func fin a<sa (F2L fin a<sa (λ q _ → x q)) ≡ x
|
|
|
326 lemma = f-extensionality ( λ q → L2F-iso fin x q )
|
|
|
327
|
|
|
328
|
|
|
329 Fin2Finite : ( n : ℕ ) → FiniteSet (Fin n)
|
|
|
330 Fin2Finite n = record { F←Q = λ x → x ; Q←F = λ x → x ; finiso← = λ q → refl ; finiso→ = λ q → refl }
|
|
|
331
|
|
|
332 data fin-less { n : ℕ } { A : Set } (fa : FiniteSet A ) (n<m : n < FiniteSet.finite fa ) : Set where
|
|
|
333 elm1 : (elm : A ) → toℕ (FiniteSet.F←Q fa elm ) < n → fin-less fa n<m
|
|
|
334
|
|
|
335 get-elm : { n : ℕ } { A : Set } {fa : FiniteSet A } {n<m : n < FiniteSet.finite fa } → fin-less fa n<m → A
|
|
|
336 get-elm (elm1 a _ ) = a
|
|
|
337
|
|
|
338 get-< : { n : ℕ } { A : Set } {fa : FiniteSet A } {n<m : n < FiniteSet.finite fa }→ (f : fin-less fa n<m ) → toℕ (FiniteSet.F←Q fa (get-elm f )) < n
|
|
|
339 get-< (elm1 _ b ) = b
|
|
|
340
|
|
|
341 fin-less-cong : { n : ℕ } { A : Set } (fa : FiniteSet A ) (n<m : n < FiniteSet.finite fa )
|
|
|
342 → (x y : fin-less fa n<m ) → get-elm {n} {A} {fa} x ≡ get-elm {n} {A} {fa} y → get-< x ≅ get-< y → x ≡ y
|
|
|
343 fin-less-cong fa n<m (elm1 elm x) (elm1 elm x) refl HE.refl = refl
|
|
|
344
|
|
|
345 fin-< : {A : Set} → { n : ℕ } → (fa : FiniteSet A ) → (n<m : n < FiniteSet.finite fa ) → FiniteSet (fin-less fa n<m )
|
|
|
346 fin-< {A} {n} fa n<m = iso-fin (Fin2Finite n) iso where
|
|
|
347 m = FiniteSet.finite fa
|
|
|
348 iso : ISO (Fin n) (fin-less fa n<m )
|
|
|
349 lemma8 : {i j n : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n } → i<n ≅ j<n
|
|
|
350 lemma8 {zero} {zero} {suc n} refl {s≤s z≤n} {s≤s z≤n} = HE.refl
|
|
|
351 lemma8 {suc i} {suc i} {suc n} refl {s≤s i<n} {s≤s j<n} = HE.cong (λ k → s≤s k ) ( lemma8 {i} {i} refl )
|
|
|
352 lemma10 : {n i j : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n } → fromℕ< i<n ≡ fromℕ< j<n
|
|
|
353 lemma10 refl = HE.≅-to-≡ (HE.cong (λ k → fromℕ< k ) (lemma8 refl ))
|
|
|
354 lemma3 : {a b c : ℕ } → { a<b : a < b } { b<c : b < c } { a<c : a < c } → NatP.<-trans a<b b<c ≡ a<c
|
|
|
355 lemma3 {a} {b} {c} {a<b} {b<c} {a<c} = HE.≅-to-≡ (lemma8 refl)
|
|
|
356 lemma11 : {n : ℕ } {x : Fin n } → (n<m : n < m ) → toℕ (fromℕ< (NatP.<-trans (toℕ<n x) n<m)) ≡ toℕ x
|
|
|
357 lemma11 {n} {x} n<m = begin
|
|
|
358 toℕ (fromℕ< (NatP.<-trans (toℕ<n x) n<m))
|
|
|
359 ≡⟨ toℕ-fromℕ< _ ⟩
|
|
|
360 toℕ x
|
|
|
361 ∎ where
|
|
|
362 open ≡-Reasoning
|
|
|
363 ISO.A←B iso (elm1 elm x) = fromℕ< x
|
|
|
364 ISO.B←A iso x = elm1 (FiniteSet.Q←F fa (fromℕ< (NatP.<-trans x<n n<m ))) to<n where
|
|
|
365 x<n : toℕ x < n
|
|
|
366 x<n = toℕ<n x
|
|
|
367 to<n : toℕ (FiniteSet.F←Q fa (FiniteSet.Q←F fa (fromℕ< (NatP.<-trans x<n n<m)))) < n
|
|
|
368 to<n = subst (λ k → toℕ k < n ) (sym (FiniteSet.finiso← fa _ )) (subst (λ k → k < n ) (sym ( toℕ-fromℕ< (NatP.<-trans x<n n<m) )) x<n )
|
|
|
369 ISO.iso← iso x = lemma2 where
|
|
|
370 lemma2 : fromℕ< (subst (λ k → toℕ k < n) (sym
|
|
|
371 (FiniteSet.finiso← fa (fromℕ< (NatP.<-trans (toℕ<n x) n<m)))) (subst (λ k → k < n)
|
|
|
372 (sym (toℕ-fromℕ< (NatP.<-trans (toℕ<n x) n<m))) (toℕ<n x))) ≡ x
|
|
|
373 lemma2 = begin
|
|
|
374 fromℕ< (subst (λ k → toℕ k < n) (sym
|
|
|
375 (FiniteSet.finiso← fa (fromℕ< (NatP.<-trans (toℕ<n x) n<m)))) (subst (λ k → k < n)
|
|
|
376 (sym (toℕ-fromℕ< (NatP.<-trans (toℕ<n x) n<m))) (toℕ<n x)))
|
|
|
377 ≡⟨⟩
|
|
|
378 fromℕ< ( subst (λ k → toℕ ( k ) < n ) (sym (FiniteSet.finiso← fa _ )) lemma6 )
|
|
|
379 ≡⟨ lemma10 (cong (λ k → toℕ k) (FiniteSet.finiso← fa _ ) ) ⟩
|
|
|
380 fromℕ< lemma6
|
|
|
381 ≡⟨ lemma10 (lemma11 n<m ) ⟩
|
|
|
382 fromℕ< ( toℕ<n x )
|
|
|
383 ≡⟨ fromℕ<-toℕ _ _ ⟩
|
|
|
384 x
|
|
|
385 ∎ where
|
|
|
386 open ≡-Reasoning
|
|
|
387 lemma6 : toℕ (fromℕ< (NatP.<-trans (toℕ<n x) n<m)) < n
|
|
|
388 lemma6 = subst ( λ k → k < n ) (sym (toℕ-fromℕ< (NatP.<-trans (toℕ<n x) n<m))) (toℕ<n x )
|
|
|
389 ISO.iso→ iso (elm1 elm x) = fin-less-cong fa n<m _ _ lemma (lemma8 (cong (λ k → toℕ (FiniteSet.F←Q fa k) ) lemma ) ) where
|
|
|
390 lemma13 : toℕ (fromℕ< x) ≡ toℕ (FiniteSet.F←Q fa elm)
|
|
|
391 lemma13 = begin
|
|
|
392 toℕ (fromℕ< x)
|
|
|
393 ≡⟨ toℕ-fromℕ< _ ⟩
|
|
|
394 toℕ (FiniteSet.F←Q fa elm)
|
|
|
395 ∎ where open ≡-Reasoning
|
|
|
396 lemma : FiniteSet.Q←F fa (fromℕ< (NatP.<-trans (toℕ<n (ISO.A←B iso (elm1 elm x))) n<m)) ≡ elm
|
|
|
397 lemma = begin
|
|
|
398 FiniteSet.Q←F fa (fromℕ< (NatP.<-trans (toℕ<n (ISO.A←B iso (elm1 elm x))) n<m))
|
|
|
399 ≡⟨⟩
|
|
|
400 FiniteSet.Q←F fa (fromℕ< ( NatP.<-trans (toℕ<n ( fromℕ< x ) ) n<m))
|
|
|
401 ≡⟨ cong (λ k → FiniteSet.Q←F fa k) (lemma10 lemma13 ) ⟩
|
|
|
402 FiniteSet.Q←F fa (fromℕ< ( NatP.<-trans x n<m))
|
|
|
403 ≡⟨ cong (λ k → FiniteSet.Q←F fa (fromℕ< k )) lemma3 ⟩
|
|
|
404 FiniteSet.Q←F fa (fromℕ< ( toℕ<n (FiniteSet.F←Q fa elm)))
|
|
|
405 ≡⟨ cong (λ k → FiniteSet.Q←F fa k ) ( fromℕ<-toℕ _ _ ) ⟩
|
|
|
406 FiniteSet.Q←F fa (FiniteSet.F←Q fa elm )
|
|
|
407 ≡⟨ FiniteSet.finiso→ fa _ ⟩
|
|
|
408 elm
|
|
|
409 ∎ where open ≡-Reasoning
|
|
|
410
|
|
|
411
|
