Mercurial > hg > Members > kono > Proof > automaton
annotate automaton-in-agda/src/finiteSetUtil.agda @ 346:4456eebbd1bc
copying countable bijection may not easy
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 17 Jul 2023 11:00:19 +0900 |
| parents | bcf3ca6ba87b |
| children |
| rev | line source |
|---|---|
| 163 | 1 {-# OPTIONS --allow-unsolved-metas #-} |
| 2 | |
| 3 module finiteSetUtil where | |
| 141 | 4 |
| 5 open import Data.Nat hiding ( _≟_ ) | |
|
346
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
6 open import Data.Fin renaming ( _<_ to _<<_ ; _>_ to _f>_ ; _≟_ to _f≟_ ) hiding (_≤_ ; pred ) |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
7 open import Data.Fin.Properties hiding ( <-trans ) renaming ( <-cmp to <-fcmp ) hiding (≤-refl ; ≤-trans ) |
| 141 | 8 open import Data.Empty |
| 9 open import Relation.Nullary | |
| 10 open import Relation.Binary.Definitions | |
| 11 open import Relation.Binary.PropositionalEquality | |
| 12 open import logic | |
| 13 open import nat | |
| 14 open import finiteSet | |
| 163 | 15 open import fin |
| 337 | 16 open import Data.Nat.Properties as NP hiding ( _≟_ ) |
| 141 | 17 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) |
| 18 | |
| 163 | 19 record Found ( Q : Set ) (p : Q → Bool ) : Set where |
| 20 field | |
| 21 found-q : Q | |
| 22 found-p : p found-q ≡ true | |
| 23 | |
| 264 | 24 open Bijection |
| 25 | |
| 268 | 26 open import Axiom.Extensionality.Propositional |
| 27 open import Level hiding (suc ; zero) | |
| 28 postulate f-extensionality : { n : Level} → Axiom.Extensionality.Propositional.Extensionality n n -- (Level.suc n) | |
| 29 | |
| 163 | 30 module _ {Q : Set } (F : FiniteSet Q) where |
| 31 open FiniteSet F | |
| 268 | 32 equal?-refl : { x : Q } → equal? x x ≡ true |
| 33 equal?-refl {x} with F←Q x ≟ F←Q x | |
| 34 ... | yes refl = refl | |
| 35 ... | no ne = ⊥-elim (ne refl) | |
| 163 | 36 equal→refl : { x y : Q } → equal? x y ≡ true → x ≡ y |
| 37 equal→refl {q0} {q1} eq with F←Q q0 ≟ F←Q q1 | |
| 38 equal→refl {q0} {q1} refl | yes eq = begin | |
| 39 q0 | |
| 40 ≡⟨ sym ( finiso→ q0) ⟩ | |
| 41 Q←F (F←Q q0) | |
| 42 ≡⟨ cong (λ k → Q←F k ) eq ⟩ | |
| 43 Q←F (F←Q q1) | |
| 264 | 44 ≡⟨ finiso→ q1 ⟩ |
| 163 | 45 q1 |
| 46 ∎ where open ≡-Reasoning | |
| 318 | 47 eqP : (x y : Q) → Dec ( x ≡ y ) |
| 48 eqP x y with F←Q x ≟ F←Q y | |
| 49 ... | yes eq = yes (subst₂ (λ j k → j ≡ k ) (finiso→ x) (finiso→ y) (cong Q←F eq) ) | |
| 50 ... | no n = no (λ eq → n (cong F←Q eq)) | |
| 163 | 51 End : (m : ℕ ) → (p : Q → Bool ) → Set |
| 52 End m p = (i : Fin finite) → m ≤ toℕ i → p (Q←F i ) ≡ false | |
| 53 first-end : ( p : Q → Bool ) → End finite p | |
| 54 first-end p i i>n = ⊥-elim (nat-≤> i>n (fin<n {finite} {i}) ) | |
| 55 next-end : {m : ℕ } → ( p : Q → Bool ) → End (suc m) p | |
| 56 → (m<n : m < finite ) → p (Q←F (fromℕ< m<n )) ≡ false | |
| 57 → End m p | |
| 337 | 58 next-end {m} p prev m<n np i m<i with NP.<-cmp m (toℕ i) |
| 163 | 59 next-end p prev m<n np i m<i | tri< a ¬b ¬c = prev i a |
| 60 next-end p prev m<n np i m<i | tri> ¬a ¬b c = ⊥-elim ( nat-≤> m<i c ) | |
| 61 next-end {m} p prev m<n np i m<i | tri≈ ¬a b ¬c = subst ( λ k → p (Q←F k) ≡ false) (m<n=i i b m<n ) np where | |
| 62 m<n=i : {n : ℕ } (i : Fin n) {m : ℕ } → m ≡ (toℕ i) → (m<n : m < n ) → fromℕ< m<n ≡ i | |
| 264 | 63 m<n=i i refl m<n = fromℕ<-toℕ i m<n |
| 163 | 64 found : { p : Q → Bool } → (q : Q ) → p q ≡ true → exists p ≡ true |
| 337 | 65 found {p} q pt = found1 finite (NP.≤-refl ) ( first-end p ) where |
| 163 | 66 found1 : (m : ℕ ) (m<n : m Data.Nat.≤ finite ) → ((i : Fin finite) → m ≤ toℕ i → p (Q←F i ) ≡ false ) → exists1 m m<n p ≡ true |
| 67 found1 0 m<n end = ⊥-elim ( ¬-bool (subst (λ k → k ≡ false ) (cong (λ k → p k) (finiso→ q) ) (end (F←Q q) z≤n )) pt ) | |
| 68 found1 (suc m) m<n end with bool-≡-? (p (Q←F (fromℕ< m<n))) true | |
| 264 | 69 found1 (suc m) m<n end | yes eq = subst (λ k → k \/ exists1 m (<to≤ m<n) p ≡ true ) (sym eq) (bool-or-4 {exists1 m (<to≤ m<n) p} ) |
| 163 | 70 found1 (suc m) m<n end | no np = begin |
| 264 | 71 p (Q←F (fromℕ< m<n)) \/ exists1 m (<to≤ m<n) p |
| 163 | 72 ≡⟨ bool-or-1 (¬-bool-t np ) ⟩ |
| 264 | 73 exists1 m (<to≤ m<n) p |
| 74 ≡⟨ found1 m (<to≤ m<n) (next-end p end m<n (¬-bool-t np )) ⟩ | |
| 163 | 75 true |
| 76 ∎ where open ≡-Reasoning | |
| 268 | 77 not-found : { p : Q → Bool } → ( (q : Q ) → p q ≡ false ) → exists p ≡ false |
| 337 | 78 not-found {p} pn = not-found2 finite NP.≤-refl where |
| 268 | 79 not-found2 : (m : ℕ ) → (m<n : m Data.Nat.≤ finite ) → exists1 m m<n p ≡ false |
| 80 not-found2 zero _ = refl | |
| 81 not-found2 ( suc m ) m<n with pn (Q←F (fromℕ< {m} {finite} m<n)) | |
| 82 not-found2 (suc m) m<n | eq = begin | |
| 83 p (Q←F (fromℕ< m<n)) \/ exists1 m (<to≤ m<n) p | |
| 84 ≡⟨ bool-or-1 eq ⟩ | |
| 85 exists1 m (<to≤ m<n) p | |
| 86 ≡⟨ not-found2 m (<to≤ m<n) ⟩ | |
| 87 false | |
| 88 ∎ where open ≡-Reasoning | |
| 89 found← : { p : Q → Bool } → exists p ≡ true → Found Q p | |
| 337 | 90 found← {p} exst = found2 finite NP.≤-refl (first-end p ) where |
| 268 | 91 found2 : (m : ℕ ) (m<n : m Data.Nat.≤ finite ) → End m p → Found Q p |
| 92 found2 0 m<n end = ⊥-elim ( ¬-bool (not-found (λ q → end (F←Q q) z≤n ) ) (subst (λ k → exists k ≡ true) (sym lemma) exst ) ) where | |
| 93 lemma : (λ z → p (Q←F (F←Q z))) ≡ p | |
| 94 lemma = f-extensionality ( λ q → subst (λ k → p k ≡ p q ) (sym (finiso→ q)) refl ) | |
| 95 found2 (suc m) m<n end with bool-≡-? (p (Q←F (fromℕ< m<n))) true | |
| 96 found2 (suc m) m<n end | yes eq = record { found-q = Q←F (fromℕ< m<n) ; found-p = eq } | |
| 97 found2 (suc m) m<n end | no np = | |
| 98 found2 m (<to≤ m<n) (next-end p end m<n (¬-bool-t np )) | |
| 99 not-found← : { p : Q → Bool } → exists p ≡ false → (q : Q ) → p q ≡ false | |
| 100 not-found← {p} np q = ¬-bool-t ( contra-position {_} {_} {_} {exists p ≡ true} (found q) (λ ep → ¬-bool np ep ) ) | |
| 101 | |
| 163 | 102 |
| 103 | |
| 264 | 104 iso-fin : {A B : Set} → FiniteSet A → Bijection A B → FiniteSet B |
| 141 | 105 iso-fin {A} {B} fin iso = record { |
| 330 | 106 Q←F = λ f → fun→ iso ( FiniteSet.Q←F fin f ) |
| 264 | 107 ; F←Q = λ b → FiniteSet.F←Q fin (fun← iso b ) |
| 108 ; finiso→ = finiso→ | |
| 109 ; finiso← = finiso← | |
| 141 | 110 } where |
| 264 | 111 finiso→ : (q : B) → fun→ iso (FiniteSet.Q←F fin (FiniteSet.F←Q fin (Bijection.fun← iso q))) ≡ q |
| 141 | 112 finiso→ q = begin |
| 264 | 113 fun→ iso (FiniteSet.Q←F fin (FiniteSet.F←Q fin (Bijection.fun← iso q))) |
| 114 ≡⟨ cong (λ k → fun→ iso k ) (FiniteSet.finiso→ fin _ ) ⟩ | |
| 115 fun→ iso (Bijection.fun← iso q) | |
| 116 ≡⟨ fiso→ iso _ ⟩ | |
| 141 | 117 q |
| 264 | 118 ∎ where open ≡-Reasoning |
| 119 finiso← : (f : Fin (FiniteSet.finite fin ))→ FiniteSet.F←Q fin (Bijection.fun← iso (Bijection.fun→ iso (FiniteSet.Q←F fin f))) ≡ f | |
| 141 | 120 finiso← f = begin |
| 264 | 121 FiniteSet.F←Q fin (Bijection.fun← iso (Bijection.fun→ iso (FiniteSet.Q←F fin f))) |
| 122 ≡⟨ cong (λ k → FiniteSet.F←Q fin k ) (Bijection.fiso← iso _) ⟩ | |
| 141 | 123 FiniteSet.F←Q fin (FiniteSet.Q←F fin f) |
| 124 ≡⟨ FiniteSet.finiso← fin _ ⟩ | |
| 125 f | |
| 126 ∎ where | |
| 127 open ≡-Reasoning | |
| 128 | |
| 129 data One : Set where | |
| 130 one : One | |
| 131 | |
| 132 fin-∨1 : {B : Set} → (fb : FiniteSet B ) → FiniteSet (One ∨ B) | |
| 133 fin-∨1 {B} fb = record { | |
| 330 | 134 Q←F = Q←F |
| 135 ; F←Q = F←Q | |
| 136 ; finiso→ = finiso→ | |
| 137 ; finiso← = finiso← | |
| 141 | 138 } where |
| 139 b = FiniteSet.finite fb | |
| 140 Q←F : Fin (suc b) → One ∨ B | |
| 141 Q←F zero = case1 one | |
| 142 Q←F (suc f) = case2 (FiniteSet.Q←F fb f) | |
| 143 F←Q : One ∨ B → Fin (suc b) | |
| 144 F←Q (case1 one) = zero | |
| 145 F←Q (case2 f ) = suc (FiniteSet.F←Q fb f) | |
| 146 finiso→ : (q : One ∨ B) → Q←F (F←Q q) ≡ q | |
| 147 finiso→ (case1 one) = refl | |
| 148 finiso→ (case2 b) = cong (λ k → case2 k ) (FiniteSet.finiso→ fb b) | |
| 149 finiso← : (q : Fin (suc b)) → F←Q (Q←F q) ≡ q | |
| 150 finiso← zero = refl | |
| 151 finiso← (suc f) = cong ( λ k → suc k ) (FiniteSet.finiso← fb f) | |
| 152 | |
| 153 | |
| 154 fin-∨2 : {B : Set} → ( a : ℕ ) → FiniteSet B → FiniteSet (Fin a ∨ B) | |
| 155 fin-∨2 {B} zero fb = iso-fin fb iso where | |
| 264 | 156 iso : Bijection B (Fin zero ∨ B) |
| 157 iso = record { | |
| 158 fun← = fun←1 | |
| 159 ; fun→ = λ b → case2 b | |
| 160 ; fiso→ = fiso→1 | |
| 161 ; fiso← = λ _ → refl | |
| 141 | 162 } where |
| 264 | 163 fun←1 : Fin zero ∨ B → B |
| 164 fun←1 (case2 x) = x | |
| 165 fiso→1 : (f : Fin zero ∨ B ) → case2 (fun←1 f) ≡ f | |
| 166 fiso→1 (case2 x) = refl | |
| 141 | 167 fin-∨2 {B} (suc a) fb = iso-fin (fin-∨1 (fin-∨2 a fb) ) iso |
| 168 where | |
| 264 | 169 iso : Bijection (One ∨ (Fin a ∨ B) ) (Fin (suc a) ∨ B) |
| 170 fun← iso (case1 zero) = case1 one | |
| 171 fun← iso (case1 (suc f)) = case2 (case1 f) | |
| 172 fun← iso (case2 b) = case2 (case2 b) | |
| 173 fun→ iso (case1 one) = case1 zero | |
| 174 fun→ iso (case2 (case1 f)) = case1 (suc f) | |
| 175 fun→ iso (case2 (case2 b)) = case2 b | |
| 176 fiso← iso (case1 one) = refl | |
| 177 fiso← iso (case2 (case1 x)) = refl | |
| 178 fiso← iso (case2 (case2 x)) = refl | |
| 179 fiso→ iso (case1 zero) = refl | |
| 180 fiso→ iso (case1 (suc x)) = refl | |
| 181 fiso→ iso (case2 x) = refl | |
| 141 | 182 |
| 183 | |
| 264 | 184 FiniteSet→Fin : {A : Set} → (fin : FiniteSet A ) → Bijection (Fin (FiniteSet.finite fin)) A |
| 185 fun← (FiniteSet→Fin fin) f = FiniteSet.F←Q fin f | |
| 186 fun→ (FiniteSet→Fin fin) f = FiniteSet.Q←F fin f | |
| 187 fiso← (FiniteSet→Fin fin) = FiniteSet.finiso← fin | |
| 188 fiso→ (FiniteSet→Fin fin) = FiniteSet.finiso→ fin | |
| 141 | 189 |
| 190 | |
| 191 fin-∨ : {A B : Set} → FiniteSet A → FiniteSet B → FiniteSet (A ∨ B) | |
| 192 fin-∨ {A} {B} fa fb = iso-fin (fin-∨2 a fb ) iso2 where | |
| 193 a = FiniteSet.finite fa | |
| 194 ia = FiniteSet→Fin fa | |
| 264 | 195 iso2 : Bijection (Fin a ∨ B ) (A ∨ B) |
| 196 fun← iso2 (case1 x) = case1 (fun← ia x ) | |
| 197 fun← iso2 (case2 x) = case2 x | |
| 198 fun→ iso2 (case1 x) = case1 (fun→ ia x ) | |
| 199 fun→ iso2 (case2 x) = case2 x | |
| 200 fiso← iso2 (case1 x) = cong ( λ k → case1 k ) (Bijection.fiso← ia x) | |
| 201 fiso← iso2 (case2 x) = refl | |
| 202 fiso→ iso2 (case1 x) = cong ( λ k → case1 k ) (Bijection.fiso→ ia x) | |
| 203 fiso→ iso2 (case2 x) = refl | |
| 141 | 204 |
|
278
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
205 open import Data.Product hiding ( map ) |
| 141 | 206 |
| 207 fin-× : {A B : Set} → FiniteSet A → FiniteSet B → FiniteSet (A × B) | |
| 208 fin-× {A} {B} fa fb with FiniteSet→Fin fa | |
| 209 ... | a=f = iso-fin (fin-×-f a ) iso-1 where | |
| 210 a = FiniteSet.finite fa | |
| 211 b = FiniteSet.finite fb | |
| 264 | 212 iso-1 : Bijection (Fin a × B) ( A × B ) |
| 213 fun← iso-1 x = ( FiniteSet.F←Q fa (proj₁ x) , proj₂ x) | |
| 214 fun→ iso-1 x = ( FiniteSet.Q←F fa (proj₁ x) , proj₂ x) | |
| 215 fiso← iso-1 x = lemma where | |
| 141 | 216 lemma : (FiniteSet.F←Q fa (FiniteSet.Q←F fa (proj₁ x)) , proj₂ x) ≡ ( proj₁ x , proj₂ x ) |
| 217 lemma = cong ( λ k → ( k , proj₂ x ) ) (FiniteSet.finiso← fa _ ) | |
| 264 | 218 fiso→ iso-1 x = cong ( λ k → ( k , proj₂ x ) ) (FiniteSet.finiso→ fa _ ) |
| 141 | 219 |
| 264 | 220 iso-2 : {a : ℕ } → Bijection (B ∨ (Fin a × B)) (Fin (suc a) × B) |
| 221 fun← iso-2 (zero , b ) = case1 b | |
| 222 fun← iso-2 (suc fst , b ) = case2 ( fst , b ) | |
| 223 fun→ iso-2 (case1 b) = ( zero , b ) | |
| 224 fun→ iso-2 (case2 (a , b )) = ( suc a , b ) | |
| 225 fiso← iso-2 (case1 x) = refl | |
| 226 fiso← iso-2 (case2 x) = refl | |
| 227 fiso→ iso-2 (zero , b ) = refl | |
| 228 fiso→ iso-2 (suc a , b ) = refl | |
| 141 | 229 |
| 230 fin-×-f : ( a : ℕ ) → FiniteSet ((Fin a) × B) | |
| 231 fin-×-f zero = record { Q←F = λ () ; F←Q = λ () ; finiso→ = λ () ; finiso← = λ () ; finite = 0 } | |
| 232 fin-×-f (suc a) = iso-fin ( fin-∨ fb ( fin-×-f a ) ) iso-2 | |
| 233 | |
| 234 open _∧_ | |
| 235 | |
| 236 fin-∧ : {A B : Set} → FiniteSet A → FiniteSet B → FiniteSet (A ∧ B) | |
| 237 fin-∧ {A} {B} fa fb with FiniteSet→Fin fa -- same thing for our tool | |
| 238 ... | a=f = iso-fin (fin-×-f a ) iso-1 where | |
| 239 a = FiniteSet.finite fa | |
| 240 b = FiniteSet.finite fb | |
| 264 | 241 iso-1 : Bijection (Fin a ∧ B) ( A ∧ B ) |
| 242 fun← iso-1 x = record { proj1 = FiniteSet.F←Q fa (proj1 x) ; proj2 = proj2 x} | |
| 243 fun→ iso-1 x = record { proj1 = FiniteSet.Q←F fa (proj1 x) ; proj2 = proj2 x} | |
| 244 fiso← iso-1 x = lemma where | |
| 141 | 245 lemma : record { proj1 = FiniteSet.F←Q fa (FiniteSet.Q←F fa (proj1 x)) ; proj2 = proj2 x} ≡ record {proj1 = proj1 x ; proj2 = proj2 x } |
| 246 lemma = cong ( λ k → record {proj1 = k ; proj2 = proj2 x } ) (FiniteSet.finiso← fa _ ) | |
| 264 | 247 fiso→ iso-1 x = cong ( λ k → record {proj1 = k ; proj2 = proj2 x } ) (FiniteSet.finiso→ fa _ ) |
| 141 | 248 |
| 264 | 249 iso-2 : {a : ℕ } → Bijection (B ∨ (Fin a ∧ B)) (Fin (suc a) ∧ B) |
| 250 fun← iso-2 (record { proj1 = zero ; proj2 = b }) = case1 b | |
| 251 fun← iso-2 (record { proj1 = suc fst ; proj2 = b }) = case2 ( record { proj1 = fst ; proj2 = b } ) | |
| 252 fun→ iso-2 (case1 b) = record {proj1 = zero ; proj2 = b } | |
| 253 fun→ iso-2 (case2 (record { proj1 = a ; proj2 = b })) = record { proj1 = suc a ; proj2 = b } | |
| 254 fiso← iso-2 (case1 x) = refl | |
| 255 fiso← iso-2 (case2 x) = refl | |
| 256 fiso→ iso-2 (record { proj1 = zero ; proj2 = b }) = refl | |
| 257 fiso→ iso-2 (record { proj1 = suc a ; proj2 = b }) = refl | |
| 141 | 258 |
| 259 fin-×-f : ( a : ℕ ) → FiniteSet ((Fin a) ∧ B) | |
| 260 fin-×-f zero = record { Q←F = λ () ; F←Q = λ () ; finiso→ = λ () ; finiso← = λ () ; finite = 0 } | |
| 261 fin-×-f (suc a) = iso-fin ( fin-∨ fb ( fin-×-f a ) ) iso-2 | |
| 262 | |
| 263 -- import Data.Nat.DivMod | |
| 264 | |
|
278
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
265 open import Data.Vec hiding ( map ; length ) |
| 141 | 266 import Data.Product |
| 267 | |
| 268 exp2 : (n : ℕ ) → exp 2 (suc n) ≡ exp 2 n Data.Nat.+ exp 2 n | |
| 269 exp2 n = begin | |
| 270 exp 2 (suc n) | |
| 271 ≡⟨⟩ | |
| 272 2 * ( exp 2 n ) | |
| 273 ≡⟨ *-comm 2 (exp 2 n) ⟩ | |
| 274 ( exp 2 n ) * 2 | |
| 275 ≡⟨ *-suc ( exp 2 n ) 1 ⟩ | |
| 276 (exp 2 n ) Data.Nat.+ ( exp 2 n ) * 1 | |
| 277 ≡⟨ cong ( λ k → (exp 2 n ) Data.Nat.+ k ) (proj₂ *-identity (exp 2 n) ) ⟩ | |
| 278 exp 2 n Data.Nat.+ exp 2 n | |
| 279 ∎ where | |
| 280 open ≡-Reasoning | |
| 281 open Data.Product | |
| 282 | |
| 283 cast-iso : {n m : ℕ } → (eq : n ≡ m ) → (f : Fin m ) → cast eq ( cast (sym eq ) f) ≡ f | |
| 284 cast-iso refl zero = refl | |
| 285 cast-iso refl (suc f) = cong ( λ k → suc k ) ( cast-iso refl f ) | |
| 286 | |
| 287 | |
| 288 fin2List : {n : ℕ } → FiniteSet (Vec Bool n) | |
| 289 fin2List {zero} = record { | |
| 290 Q←F = λ _ → Vec.[] | |
| 291 ; F←Q = λ _ → # 0 | |
| 292 ; finiso→ = finiso→ | |
| 293 ; finiso← = finiso← | |
| 294 } where | |
| 295 Q = Vec Bool zero | |
| 296 finiso→ : (q : Q) → [] ≡ q | |
| 297 finiso→ [] = refl | |
| 298 finiso← : (f : Fin (exp 2 zero)) → # 0 ≡ f | |
| 299 finiso← zero = refl | |
| 300 fin2List {suc n} = subst (λ k → FiniteSet (Vec Bool (suc n)) ) (sym (exp2 n)) ( iso-fin (fin-∨ (fin2List ) (fin2List )) iso ) | |
| 301 where | |
| 302 QtoR : Vec Bool (suc n) → Vec Bool n ∨ Vec Bool n | |
| 303 QtoR ( true ∷ x ) = case1 x | |
| 304 QtoR ( false ∷ x ) = case2 x | |
| 305 RtoQ : Vec Bool n ∨ Vec Bool n → Vec Bool (suc n) | |
| 306 RtoQ ( case1 x ) = true ∷ x | |
| 307 RtoQ ( case2 x ) = false ∷ x | |
| 308 isoRQ : (x : Vec Bool (suc n) ) → RtoQ ( QtoR x ) ≡ x | |
| 309 isoRQ (true ∷ _ ) = refl | |
| 310 isoRQ (false ∷ _ ) = refl | |
| 311 isoQR : (x : Vec Bool n ∨ Vec Bool n ) → QtoR ( RtoQ x ) ≡ x | |
| 312 isoQR (case1 x) = refl | |
| 313 isoQR (case2 x) = refl | |
| 264 | 314 iso : Bijection (Vec Bool n ∨ Vec Bool n) (Vec Bool (suc n)) |
| 315 iso = record { fun← = QtoR ; fun→ = RtoQ ; fiso← = isoQR ; fiso→ = isoRQ } | |
| 141 | 316 |
| 317 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 | |
| 318 F2L {Q} {zero} fin _ Q→B = [] | |
| 337 | 319 F2L {Q} {suc n} fin (s≤s n<m) Q→B = Q→B (FiniteSet.Q←F fin (fromℕ< n<m)) lemma6 ∷ F2L {Q} fin (NP.<-trans n<m a<sa ) qb1 where |
| 141 | 320 lemma6 : toℕ (FiniteSet.F←Q fin (FiniteSet.Q←F fin (fromℕ< n<m))) < suc n |
| 321 lemma6 = subst (λ k → toℕ k < suc n ) (sym (FiniteSet.finiso← fin _ )) (subst (λ k → k < suc n) (sym (toℕ-fromℕ< n<m )) a<sa ) | |
| 322 qb1 : (q : Q) → toℕ (FiniteSet.F←Q fin q) < n → Bool | |
| 337 | 323 qb1 q q<n = Q→B q (NP.<-trans q<n a<sa) |
| 141 | 324 |
| 325 List2Func : { Q : Set } → {n : ℕ } → (fin : FiniteSet Q ) → n < suc (FiniteSet.finite fin) → Vec Bool n → Q → Bool | |
| 326 List2Func {Q} {zero} fin (s≤s z≤n) [] q = false | |
| 327 List2Func {Q} {suc n} fin (s≤s n<m) (h ∷ t) q with FiniteSet.F←Q fin q ≟ fromℕ< n<m | |
| 328 ... | yes _ = h | |
| 337 | 329 ... | no _ = List2Func {Q} fin (NP.<-trans n<m a<sa ) t q |
| 141 | 330 |
| 331 open import Level renaming ( suc to Suc ; zero to Zero) | |
| 332 open import Axiom.Extensionality.Propositional | |
| 268 | 333 -- postulate f-extensionality : { n : Level} → Axiom.Extensionality.Propositional.Extensionality n n |
| 141 | 334 |
| 335 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 | |
| 336 F2L-iso {Q} fin x = f2l m a<sa x where | |
| 337 m = FiniteSet.finite fin | |
| 338 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 | |
| 339 f2l zero (s≤s z≤n) [] = refl | |
| 163 | 340 f2l (suc n) (s≤s n<m) (h ∷ t ) = lemma1 lemma2 lemma3f where |
| 141 | 341 lemma1 : {n : ℕ } → {h h1 : Bool } → {t t1 : Vec Bool n } → h ≡ h1 → t ≡ t1 → h ∷ t ≡ h1 ∷ t1 |
| 342 lemma1 refl refl = refl | |
| 343 lemma2 : List2Func fin (s≤s n<m) (h ∷ t) (FiniteSet.Q←F fin (fromℕ< n<m)) ≡ h | |
| 344 lemma2 with FiniteSet.F←Q fin (FiniteSet.Q←F fin (fromℕ< n<m)) ≟ fromℕ< n<m | |
| 345 lemma2 | yes p = refl | |
| 346 lemma2 | no ¬p = ⊥-elim ( ¬p (FiniteSet.finiso← fin _) ) | |
| 337 | 347 lemma4 : (q : Q ) → toℕ (FiniteSet.F←Q fin q ) < n → List2Func fin (s≤s n<m) (h ∷ t) q ≡ List2Func fin (NP.<-trans n<m a<sa) t q |
| 141 | 348 lemma4 q _ with FiniteSet.F←Q fin q ≟ fromℕ< n<m |
| 349 lemma4 q lt | yes p = ⊥-elim ( nat-≡< (toℕ-fromℕ< n<m) (lemma5 n lt (cong (λ k → toℕ k) p))) where | |
| 350 lemma5 : {j k : ℕ } → ( n : ℕ) → suc j ≤ n → j ≡ k → k < n | |
| 351 lemma5 {zero} (suc n) (s≤s z≤n) refl = s≤s z≤n | |
| 352 lemma5 {suc j} (suc n) (s≤s lt) refl = s≤s (lemma5 {j} n lt refl) | |
| 353 lemma4 q _ | no ¬p = refl | |
| 337 | 354 lemma3f : F2L fin (NP.<-trans n<m a<sa) (λ q q<n → List2Func fin (s≤s n<m) (h ∷ t) q ) ≡ t |
| 163 | 355 lemma3f = begin |
| 337 | 356 F2L fin (NP.<-trans n<m a<sa) (λ q q<n → List2Func fin (s≤s n<m) (h ∷ t) q ) |
| 357 ≡⟨ cong (λ k → F2L fin (NP.<-trans n<m a<sa) ( λ q q<n → k q q<n )) | |
| 141 | 358 (f-extensionality ( λ q → |
| 359 (f-extensionality ( λ q<n → lemma4 q q<n )))) ⟩ | |
| 337 | 360 F2L fin (NP.<-trans n<m a<sa) (λ q q<n → List2Func fin (NP.<-trans n<m a<sa) t q ) |
| 361 ≡⟨ f2l n (NP.<-trans n<m a<sa ) t ⟩ | |
| 141 | 362 t |
| 363 ∎ where | |
| 364 open ≡-Reasoning | |
| 365 | |
| 366 | |
| 367 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 | |
| 368 L2F fin n<m x q q<n = List2Func fin n<m x q | |
| 369 | |
| 370 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 | |
| 371 L2F-iso {Q} fin f q = l2f m a<sa (toℕ<n _) where | |
| 372 m = FiniteSet.finite fin | |
| 163 | 373 lemma11f : {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 |
| 374 lemma11f n<m ¬q=n q≤n = lemma13 n<m (contra-position (lemma12 n<m _) ¬q=n ) q≤n where | |
| 141 | 375 lemma13 : {n nq : ℕ } → (n<m : n < m ) → ¬ ( nq ≡ n ) → nq ≤ n → nq < n |
| 376 lemma13 {0} {0} (s≤s z≤n) nt z≤n = ⊥-elim ( nt refl ) | |
| 377 lemma13 {suc _} {0} (s≤s (s≤s n<m)) nt z≤n = s≤s z≤n | |
| 337 | 378 lemma13 {suc n} {suc nq} n<m nt (s≤s nq≤n) = s≤s (lemma13 {n} {nq} (NP.<-trans a<sa n<m ) (λ eq → nt ( cong ( λ k → suc k ) eq )) nq≤n) |
| 163 | 379 lemma3f : {a b : ℕ } → (lt : a < b ) → fromℕ< (s≤s lt) ≡ suc (fromℕ< lt) |
| 380 lemma3f (s≤s lt) = refl | |
| 381 lemma12f : {n m : ℕ } → (n<m : n < m ) → (f : Fin m ) → toℕ f ≡ n → f ≡ fromℕ< n<m | |
| 382 lemma12f {zero} {suc m} (s≤s z≤n) zero refl = refl | |
| 383 lemma12f {suc n} {suc m} (s≤s n<m) (suc f) refl = subst ( λ k → suc f ≡ k ) (sym (lemma3f n<m) ) ( cong ( λ k → suc k ) ( lemma12f {n} {m} n<m f refl ) ) | |
| 141 | 384 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 |
| 385 l2f zero (s≤s z≤n) () | |
| 386 l2f (suc n) (s≤s n<m) (s≤s n<q) with FiniteSet.F←Q fin q ≟ fromℕ< n<m | |
| 387 l2f (suc n) (s≤s n<m) (s≤s n<q) | yes p = begin | |
| 388 f (FiniteSet.Q←F fin (fromℕ< n<m)) | |
| 389 ≡⟨ cong ( λ k → f (FiniteSet.Q←F fin k )) (sym p) ⟩ | |
| 390 f (FiniteSet.Q←F fin ( FiniteSet.F←Q fin q )) | |
| 391 ≡⟨ cong ( λ k → f k ) (FiniteSet.finiso→ fin _ ) ⟩ | |
| 392 f q | |
| 393 ∎ where | |
| 394 open ≡-Reasoning | |
| 337 | 395 l2f (suc n) (s≤s n<m) (s≤s n<q) | no ¬p = l2f n (NP.<-trans n<m a<sa) (lemma11f n<m ¬p n<q) |
| 141 | 396 |
| 397 fin→ : {A : Set} → FiniteSet A → FiniteSet (A → Bool ) | |
| 398 fin→ {A} fin = iso-fin fin2List iso where | |
| 399 a = FiniteSet.finite fin | |
| 264 | 400 iso : Bijection (Vec Bool a ) (A → Bool) |
| 401 fun← iso x = F2L fin a<sa ( λ q _ → x q ) | |
| 402 fun→ iso x = List2Func fin a<sa x | |
| 403 fiso← iso x = F2L-iso fin x | |
| 404 fiso→ iso x = lemma where | |
| 141 | 405 lemma : List2Func fin a<sa (F2L fin a<sa (λ q _ → x q)) ≡ x |
| 406 lemma = f-extensionality ( λ q → L2F-iso fin x q ) | |
| 407 | |
| 408 | |
| 409 Fin2Finite : ( n : ℕ ) → FiniteSet (Fin n) | |
| 410 Fin2Finite n = record { F←Q = λ x → x ; Q←F = λ x → x ; finiso← = λ q → refl ; finiso→ = λ q → refl } | |
| 411 | |
| 412 data fin-less { n : ℕ } { A : Set } (fa : FiniteSet A ) (n<m : n < FiniteSet.finite fa ) : Set where | |
| 413 elm1 : (elm : A ) → toℕ (FiniteSet.F←Q fa elm ) < n → fin-less fa n<m | |
| 414 | |
| 415 get-elm : { n : ℕ } { A : Set } {fa : FiniteSet A } {n<m : n < FiniteSet.finite fa } → fin-less fa n<m → A | |
| 416 get-elm (elm1 a _ ) = a | |
| 417 | |
| 418 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 | |
| 419 get-< (elm1 _ b ) = b | |
| 420 | |
| 421 fin-less-cong : { n : ℕ } { A : Set } (fa : FiniteSet A ) (n<m : n < FiniteSet.finite fa ) | |
| 422 → (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 | |
| 423 fin-less-cong fa n<m (elm1 elm x) (elm1 elm x) refl HE.refl = refl | |
| 424 | |
| 425 fin-< : {A : Set} → { n : ℕ } → (fa : FiniteSet A ) → (n<m : n < FiniteSet.finite fa ) → FiniteSet (fin-less fa n<m ) | |
| 426 fin-< {A} {n} fa n<m = iso-fin (Fin2Finite n) iso where | |
| 427 m = FiniteSet.finite fa | |
| 264 | 428 iso : Bijection (Fin n) (fin-less fa n<m ) |
| 163 | 429 lemma8f : {i j n : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n } → i<n ≅ j<n |
| 430 lemma8f {zero} {zero} {suc n} refl {s≤s z≤n} {s≤s z≤n} = HE.refl | |
| 431 lemma8f {suc i} {suc i} {suc n} refl {s≤s i<n} {s≤s j<n} = HE.cong (λ k → s≤s k ) ( lemma8f {i} {i} refl ) | |
| 432 lemma10f : {n i j : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n } → fromℕ< i<n ≡ fromℕ< j<n | |
| 433 lemma10f refl = HE.≅-to-≡ (HE.cong (λ k → fromℕ< k ) (lemma8f refl )) | |
| 337 | 434 lemma3f : {a b c : ℕ } → { a<b : a < b } { b<c : b < c } { a<c : a < c } → NP.<-trans a<b b<c ≡ a<c |
| 163 | 435 lemma3f {a} {b} {c} {a<b} {b<c} {a<c} = HE.≅-to-≡ (lemma8f refl) |
| 337 | 436 lemma11f : {n : ℕ } {x : Fin n } → (n<m : n < m ) → toℕ (fromℕ< (NP.<-trans (toℕ<n x) n<m)) ≡ toℕ x |
| 163 | 437 lemma11f {n} {x} n<m = begin |
| 337 | 438 toℕ (fromℕ< (NP.<-trans (toℕ<n x) n<m)) |
| 141 | 439 ≡⟨ toℕ-fromℕ< _ ⟩ |
| 440 toℕ x | |
| 441 ∎ where | |
| 442 open ≡-Reasoning | |
| 264 | 443 fun← iso (elm1 elm x) = fromℕ< x |
| 337 | 444 fun→ iso x = elm1 (FiniteSet.Q←F fa (fromℕ< (NP.<-trans x<n n<m ))) to<n where |
| 141 | 445 x<n : toℕ x < n |
| 446 x<n = toℕ<n x | |
| 337 | 447 to<n : toℕ (FiniteSet.F←Q fa (FiniteSet.Q←F fa (fromℕ< (NP.<-trans x<n n<m)))) < n |
| 448 to<n = subst (λ k → toℕ k < n ) (sym (FiniteSet.finiso← fa _ )) (subst (λ k → k < n ) (sym ( toℕ-fromℕ< (NP.<-trans x<n n<m) )) x<n ) | |
| 264 | 449 fiso← iso x = lemma2 where |
| 141 | 450 lemma2 : fromℕ< (subst (λ k → toℕ k < n) (sym |
| 337 | 451 (FiniteSet.finiso← fa (fromℕ< (NP.<-trans (toℕ<n x) n<m)))) (subst (λ k → k < n) |
| 452 (sym (toℕ-fromℕ< (NP.<-trans (toℕ<n x) n<m))) (toℕ<n x))) ≡ x | |
| 141 | 453 lemma2 = begin |
| 454 fromℕ< (subst (λ k → toℕ k < n) (sym | |
| 337 | 455 (FiniteSet.finiso← fa (fromℕ< (NP.<-trans (toℕ<n x) n<m)))) (subst (λ k → k < n) |
| 456 (sym (toℕ-fromℕ< (NP.<-trans (toℕ<n x) n<m))) (toℕ<n x))) | |
| 141 | 457 ≡⟨⟩ |
| 458 fromℕ< ( subst (λ k → toℕ ( k ) < n ) (sym (FiniteSet.finiso← fa _ )) lemma6 ) | |
| 459 ≡⟨ lemma10 (cong (λ k → toℕ k) (FiniteSet.finiso← fa _ ) ) ⟩ | |
| 460 fromℕ< lemma6 | |
| 461 ≡⟨ lemma10 (lemma11 n<m ) ⟩ | |
| 462 fromℕ< ( toℕ<n x ) | |
| 463 ≡⟨ fromℕ<-toℕ _ _ ⟩ | |
| 464 x | |
| 465 ∎ where | |
| 466 open ≡-Reasoning | |
| 337 | 467 lemma6 : toℕ (fromℕ< (NP.<-trans (toℕ<n x) n<m)) < n |
| 468 lemma6 = subst ( λ k → k < n ) (sym (toℕ-fromℕ< (NP.<-trans (toℕ<n x) n<m))) (toℕ<n x ) | |
| 264 | 469 fiso→ iso (elm1 elm x) = fin-less-cong fa n<m _ _ lemma (lemma8 (cong (λ k → toℕ (FiniteSet.F←Q fa k) ) lemma ) ) where |
| 141 | 470 lemma13 : toℕ (fromℕ< x) ≡ toℕ (FiniteSet.F←Q fa elm) |
| 471 lemma13 = begin | |
| 472 toℕ (fromℕ< x) | |
| 473 ≡⟨ toℕ-fromℕ< _ ⟩ | |
| 474 toℕ (FiniteSet.F←Q fa elm) | |
| 475 ∎ where open ≡-Reasoning | |
| 337 | 476 lemma : FiniteSet.Q←F fa (fromℕ< (NP.<-trans (toℕ<n (Bijection.fun← iso (elm1 elm x))) n<m)) ≡ elm |
| 141 | 477 lemma = begin |
| 337 | 478 FiniteSet.Q←F fa (fromℕ< (NP.<-trans (toℕ<n (Bijection.fun← iso (elm1 elm x))) n<m)) |
| 141 | 479 ≡⟨⟩ |
| 337 | 480 FiniteSet.Q←F fa (fromℕ< ( NP.<-trans (toℕ<n ( fromℕ< x ) ) n<m)) |
| 264 | 481 ≡⟨ cong (λ k → FiniteSet.Q←F fa k) (lemma10 lemma13 ) ⟩ |
| 337 | 482 FiniteSet.Q←F fa (fromℕ< ( NP.<-trans x n<m)) |
| 264 | 483 ≡⟨ cong (λ k → FiniteSet.Q←F fa (fromℕ< k )) (HE.≅-to-≡ (lemma8 refl)) ⟩ |
| 141 | 484 FiniteSet.Q←F fa (fromℕ< ( toℕ<n (FiniteSet.F←Q fa elm))) |
| 485 ≡⟨ cong (λ k → FiniteSet.Q←F fa k ) ( fromℕ<-toℕ _ _ ) ⟩ | |
| 486 FiniteSet.Q←F fa (FiniteSet.F←Q fa elm ) | |
| 487 ≡⟨ FiniteSet.finiso→ fa _ ⟩ | |
| 488 elm | |
| 489 ∎ where open ≡-Reasoning | |
| 490 | |
|
278
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
491 open import Data.List |
| 141 | 492 |
|
278
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
493 open FiniteSet |
|
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
494 |
|
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
495 memberQ : { Q : Set } (finq : FiniteSet Q) (q : Q) (qs : List Q ) → Bool |
|
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
496 memberQ {Q} finq q [] = false |
|
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
497 memberQ {Q} finq q (q0 ∷ qs) with equal? finq q q0 |
|
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
498 ... | true = true |
|
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
499 ... | false = memberQ finq q qs |
|
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
500 |
| 316 | 501 -- |
| 502 -- there is a duplicate element in finite list | |
| 503 -- | |
| 504 | |
| 330 | 505 -- |
| 506 -- How about this? | |
| 507 -- get list of Q | |
| 508 -- remove one element for each Q from list | |
| 509 -- there must be remaining list > 1 | |
| 510 -- theses are duplicates | |
| 511 -- actualy it is duplicate | |
| 512 | |
|
278
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
513 phase2 : { Q : Set } (finq : FiniteSet Q) (q : Q) (qs : List Q ) → Bool |
|
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
514 phase2 finq q [] = false |
|
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
515 phase2 finq q (x ∷ qs) with equal? finq q x |
|
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
516 ... | true = true |
|
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
517 ... | false = phase2 finq q qs |
|
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
518 phase1 : { Q : Set } (finq : FiniteSet Q) (q : Q) (qs : List Q ) → Bool |
|
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
519 phase1 finq q [] = false |
|
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
520 phase1 finq q (x ∷ qs) with equal? finq q x |
|
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
521 ... | true = phase2 finq q qs |
|
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
522 ... | false = phase1 finq q qs |
|
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
523 |
|
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
524 dup-in-list : { Q : Set } (finq : FiniteSet Q) (q : Q) (qs : List Q ) → Bool |
|
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
525 dup-in-list {Q} finq q qs = phase1 finq q qs |
|
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
526 |
| 316 | 527 -- |
| 528 -- if length of the list is longer than kinds of a finite set, there is a duplicate | |
| 529 -- prove this based on the theorem on Data.Fin | |
| 530 -- | |
| 531 | |
| 283 | 532 dup-in-list+fin : { Q : Set } (finq : FiniteSet Q) |
|
278
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
533 → (q : Q) (qs : List Q ) |
| 283 | 534 → fin-dup-in-list (F←Q finq q) (map (F←Q finq) qs) ≡ true |
|
278
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
535 → dup-in-list finq q qs ≡ true |
| 283 | 536 dup-in-list+fin {Q} finq q qs p = i-phase1 qs p where |
| 537 i-phase2 : (qs : List Q) → fin-phase2 (F←Q finq q) (map (F←Q finq) qs) ≡ true | |
|
278
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
538 → phase2 finq q qs ≡ true |
| 294 | 539 i-phase2 (x ∷ qs) p with equal? finq q x | inspect (equal? finq q ) x | <-fcmp (F←Q finq q) (F←Q finq x) |
| 540 ... | true | _ | t = refl | |
| 541 ... | false | _ | tri< a ¬b ¬c = i-phase2 qs p | |
| 542 ... | false | record { eq = eq } | tri≈ ¬a b ¬c = ⊥-elim (¬-bool eq | |
| 543 (subst₂ (λ j k → equal? finq j k ≡ true) (finiso→ finq q) (subst (λ k → Q←F finq k ≡ x) (sym b) (finiso→ finq x)) ( equal?-refl finq ))) | |
| 544 ... | false | _ | tri> ¬a ¬b c = i-phase2 qs p | |
| 283 | 545 i-phase1 : (qs : List Q) → fin-phase1 (F←Q finq q) (map (F←Q finq) qs) ≡ true |
|
278
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
546 → phase1 finq q qs ≡ true |
| 294 | 547 i-phase1 (x ∷ qs) p with equal? finq q x | inspect (equal? finq q ) x | <-fcmp (F←Q finq q) (F←Q finq x) |
| 548 ... | true | record { eq = eq } | tri< a ¬b ¬c = ⊥-elim ( nat-≡< (cong (λ x → toℕ (F←Q finq x)) ( equal→refl finq eq )) a ) | |
| 549 ... | true | _ | tri≈ ¬a b ¬c = i-phase2 qs p | |
| 550 ... | true | record { eq = eq} | tri> ¬a ¬b c = ⊥-elim ( nat-≡< (cong (λ x → toℕ (F←Q finq x)) (sym ( equal→refl finq eq ))) c ) | |
| 551 ... | false | _ | tri< a ¬b ¬c = i-phase1 qs p | |
| 552 ... | false | record {eq = eq} | tri≈ ¬a b ¬c = ⊥-elim (¬-bool eq | |
| 553 (subst₂ (λ j k → equal? finq j k ≡ true) (finiso→ finq q) (subst (λ k → Q←F finq k ≡ x) (sym b) (finiso→ finq x)) ( equal?-refl finq ))) | |
| 554 ... | false | _ | tri> ¬a ¬b c = i-phase1 qs p | |
|
278
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
555 |
|
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
556 record Dup-in-list {Q : Set } (finq : FiniteSet Q) (qs : List Q) : Set where |
|
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
557 field |
|
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
558 dup : Q |
|
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
559 is-dup : dup-in-list finq dup qs ≡ true |
|
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
560 |
|
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
561 dup-in-list>n : {Q : Set } → (finq : FiniteSet Q) → (qs : List Q) → (len> : length qs > finite finq ) → Dup-in-list finq qs |
| 283 | 562 dup-in-list>n {Q} finq qs lt = record { dup = Q←F finq (FDup-in-list.dup dl) |
| 563 ; is-dup = dup-in-list+fin finq (Q←F finq (FDup-in-list.dup dl)) qs dl01 } where | |
| 294 | 564 maplen : (qs : List Q) → length (map (F←Q finq) qs) ≡ length qs |
| 565 maplen [] = refl | |
| 566 maplen (x ∷ qs) = cong suc (maplen qs) | |
| 283 | 567 dl : FDup-in-list (finite finq ) (map (F←Q finq) qs) |
| 294 | 568 dl = fin-dup-in-list>n (map (F←Q finq) qs) (subst (λ k → k > finite finq ) (sym (maplen qs)) lt) |
| 283 | 569 dl01 : fin-dup-in-list (F←Q finq (Q←F finq (FDup-in-list.dup dl))) (map (F←Q finq) qs) ≡ true |
| 570 dl01 = subst (λ k → fin-dup-in-list k (map (F←Q finq) qs) ≡ true ) | |
| 294 | 571 (sym (finiso← finq _)) ( FDup-in-list.is-dup dl ) |
| 337 | 572 |
| 573 open import bijection using ( InjectiveF ; Is ) | |
| 574 | |
| 575 inject-fin : {A B : Set} (fa : FiniteSet A ) | |
|
346
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
576 → (gi : InjectiveF B A) |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
577 → (is-B : (a : A ) → Dec (Is B A (InjectiveF.f gi) a) ) |
| 337 | 578 → FiniteSet B |
|
346
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
579 inject-fin {A} {B} fa gi is-B with finite fa | inspect finite fa |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
580 inject-fin {A} {B} fa gi is-B | zero | record { eq = eq1 } = ? |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
581 inject-fin {A} {B} fa gi is-B | suc pfa | record { eq = eq1 } = record { |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
582 finite = maxb |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
583 ; Q←F = λ fb → ntob (toℕ fb) fin<n |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
584 ; F←Q = λ b → fromℕ< (bton<maxb b) |
| 337 | 585 ; finiso→ = ? |
| 586 ; finiso← = ? | |
| 587 } where | |
|
346
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
588 g = InjectiveF.f gi |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
589 pfa<fa : pfa < finite fa |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
590 pfa<fa = subst (λ k → pfa < k ) (sym eq1) a<sa |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
591 h : ℕ → A |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
592 h i with <-cmp i (finite fa) |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
593 ... | tri< a ¬b ¬c = Q←F fa (fromℕ< a ) |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
594 ... | tri≈ ¬a b ¬c = Q←F fa (fromℕ< pfa<fa ) |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
595 ... | tri> ¬a ¬b c = Q←F fa (fromℕ< pfa<fa ) |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
596 C = A |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
597 h⁻¹ : A → ℕ |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
598 h⁻¹ a = toℕ (F←Q fa a) |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
599 |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
600 h-iso : (i : ℕ) → i < finite fa → h⁻¹ (h i) ≡ i |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
601 h-iso = ? |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
602 |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
603 count-B : ℕ → ℕ |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
604 count-B zero with is-B (h zero) |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
605 ... | yes isb = 1 |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
606 ... | no nisb = 0 |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
607 count-B (suc n) with is-B (h (suc n)) |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
608 ... | yes isb = suc (count-B n) |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
609 ... | no nisb = count-B n |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
610 |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
611 maxb : ℕ |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
612 maxb = count-B (finite fa) |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
613 |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
614 -- |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
615 -- countB record create ℕ → B and its injection |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
616 -- |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
617 record CountB (n : ℕ) : Set where |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
618 field |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
619 b : B |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
620 cb : ℕ |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
621 b=cn : h cb ≡ g b |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
622 cb=n : count-B cb ≡ suc n |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
623 cb-inject : (cb1 : ℕ) → Is B C g (h cb1) → count-B cb ≡ count-B cb1 → cb ≡ cb1 |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
624 |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
625 count-B-mono : {i j : ℕ} → i ≤ j → count-B i ≤ count-B j |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
626 count-B-mono {i} {j} i≤j with ≤-∨ i≤j |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
627 ... | case1 refl = ≤-refl |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
628 ... | case2 i<j = lem00 _ _ i<j where |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
629 lem00 : (i j : ℕ) → i < j → count-B i ≤ count-B j |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
630 lem00 i (suc j) (s≤s i<j) = ≤-trans (count-B-mono i<j) (lem01 j) where |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
631 lem01 : (j : ℕ) → count-B j ≤ count-B (suc j) |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
632 lem01 zero with is-B (h (suc zero)) |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
633 ... | yes isb = refl-≤s |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
634 ... | no nisb = ≤-refl |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
635 lem01 (suc n) with is-B (h (suc (suc n))) |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
636 ... | yes isb = refl-≤s |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
637 ... | no nisb = ≤-refl |
| 341 | 638 |
|
346
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
639 lem01 : (n i : ℕ) → suc n ≤ count-B i → CountB n |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
640 lem01 n i le = lem09 i (count-B i) le refl where |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
641 -- injection of count-B |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
642 --- |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
643 lem06 : (i j : ℕ ) → Is B C g (h i) → Is B C g (h j) → count-B i ≡ count-B j → i ≡ j |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
644 lem06 i j bi bj eq = lem08 where |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
645 lem20 : (i j : ℕ) → i < j → Is B C g (h i) → Is B C g (h j) → count-B j ≡ count-B i → ⊥ |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
646 lem20 zero (suc j) i<j bi bj le with is-B (h 0) | inspect count-B 0 | is-B (h (suc j)) | inspect count-B (suc j) |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
647 ... | no nisc | _ | _ | _ = ⊥-elim (nisc bi) |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
648 ... | yes _ | _ | no nisc | _ = ⊥-elim (nisc bj) |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
649 ... | yes _ | record { eq = eq1 } | yes _ | record { eq = eq2 } = ⊥-elim ( nat-≤> lem25 a<sa) where |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
650 lem22 : 1 ≡ count-B 0 |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
651 lem22 with is-B (h 0) | inspect count-B 0 |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
652 ... | yes _ | record { eq = eq1 } = refl |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
653 ... | no nisa | _ = ⊥-elim ( nisa bi ) |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
654 lem24 : count-B j ≡ 0 |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
655 lem24 = cong pred le |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
656 lem25 : 1 ≤ 0 |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
657 lem25 = begin |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
658 1 ≡⟨ lem22 ⟩ |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
659 count-B 0 ≤⟨ count-B-mono {0} {j} z≤n ⟩ |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
660 count-B j ≡⟨ lem24 ⟩ |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
661 0 ∎ where open ≤-Reasoning |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
662 lem20 (suc i) zero () bi bj le |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
663 lem20 (suc i) (suc j) (s≤s i<j) bi bj le = ⊥-elim ( nat-≡< lem24 lem21 ) where |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
664 -- |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
665 -- i < suc i ≤ j |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
666 -- cb i < suc (cb i) < cb (suc i) ≤ cb j |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
667 -- suc (cb i) ≡ suc (cb j) → cb i ≡ cb j |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
668 lem22 : suc (count-B i) ≡ count-B (suc i) |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
669 lem22 with is-B (h (suc i)) | inspect count-B (suc i) |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
670 ... | yes _ | record { eq = eq1 } = refl |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
671 ... | no nisa | _ = ⊥-elim ( nisa bi ) |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
672 lem23 : suc (count-B j) ≡ count-B (suc j) |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
673 lem23 with is-B (h (suc j)) | inspect count-B (suc j) |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
674 ... | yes _ | record { eq = eq1 } = refl |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
675 ... | no nisa | _ = ⊥-elim ( nisa bj ) |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
676 lem24 : count-B i ≡ count-B j |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
677 lem24 with is-B (h (suc i)) | inspect count-B (suc i) | is-B (h (suc j)) | inspect count-B (suc j) |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
678 ... | no nisc | _ | _ | _ = ⊥-elim (nisc bi) |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
679 ... | yes _ | _ | no nisc | _ = ⊥-elim (nisc bj) |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
680 ... | yes _ | record { eq = eq1 } | yes _ | record { eq = eq2 } = sym (cong pred le) |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
681 lem21 : suc (count-B i) ≤ count-B j |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
682 lem21 = begin |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
683 suc (count-B i) ≡⟨ lem22 ⟩ |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
684 count-B (suc i) ≤⟨ count-B-mono i<j ⟩ |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
685 count-B j ∎ where |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
686 open ≤-Reasoning |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
687 lem08 : i ≡ j |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
688 lem08 with <-cmp i j |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
689 ... | tri< a ¬b ¬c = ⊥-elim ( lem20 i j a bi bj (sym eq) ) |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
690 ... | tri≈ ¬a b ¬c = b |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
691 ... | tri> ¬a ¬b c₁ = ⊥-elim ( lem20 j i c₁ bj bi eq ) |
| 341 | 692 |
|
346
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
693 lem07 : (n i : ℕ) → count-B i ≡ suc n → CountB n |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
694 lem07 n 0 eq with is-B (h 0) | inspect count-B 0 |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
695 ... | yes isb | record { eq = eq1 } = record { b = Is.a isb ; cb = 0 ; b=cn = sym (Is.fa=c isb) ; cb=n = trans eq1 eq |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
696 ; cb-inject = λ cb1 iscb1 cb1eq → lem12 cb1 iscb1 (subst (λ k → k ≡ count-B cb1) eq1 cb1eq) } where |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
697 lem12 : (cb1 : ℕ) → Is B C g (h cb1) → 1 ≡ count-B cb1 → 0 ≡ cb1 |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
698 lem12 cb1 iscb1 cbeq = lem06 0 cb1 isb iscb1 (trans eq1 cbeq) |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
699 ... | no nisb | record { eq = eq1 } = ⊥-elim ( nat-≡< eq (s≤s z≤n ) ) |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
700 lem07 n (suc i) eq with is-B (h (suc i)) | inspect count-B (suc i) |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
701 ... | yes isb | record { eq = eq1 } = record { b = Is.a isb ; cb = suc i ; b=cn = sym (Is.fa=c isb) ; cb=n = trans eq1 eq |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
702 ; cb-inject = λ cb1 iscb1 cb1eq → lem12 cb1 iscb1 (subst (λ k → k ≡ count-B cb1) eq1 cb1eq) } where |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
703 lem12 : (cb1 : ℕ) → Is B C g (h cb1) → suc (count-B i) ≡ count-B cb1 → suc i ≡ cb1 |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
704 lem12 cb1 iscb1 cbeq = lem06 (suc i) cb1 isb iscb1 (trans eq1 cbeq) |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
705 ... | no nisb | record { eq = eq1 } = lem07 n i eq |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
706 |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
707 -- starting from 0, if count B i ≡ suc n, this is it |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
708 |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
709 lem09 : (i j : ℕ) → suc n ≤ j → j ≡ count-B i → CountB n |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
710 lem09 0 (suc j) (s≤s le) eq with ≤-∨ (s≤s le) |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
711 ... | case1 eq1 = lem07 n 0 (sym (trans eq1 eq )) |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
712 ... | case2 (s≤s lt) with is-B (h 0) | inspect count-B 0 |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
713 ... | yes isb | record { eq = eq1 } = ⊥-elim ( nat-≤> (≤-trans (s≤s lt) (refl-≤≡ eq) ) (s≤s (s≤s z≤n)) ) |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
714 ... | no nisb | record { eq = eq1 } = ⊥-elim (nat-≡< (sym eq) (s≤s z≤n)) |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
715 lem09 (suc i) (suc j) (s≤s le) eq with ≤-∨ (s≤s le) |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
716 ... | case1 eq1 = lem07 n (suc i) (sym (trans eq1 eq )) |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
717 ... | case2 (s≤s lt) with is-B (h (suc i)) | inspect count-B (suc i) |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
718 ... | yes isb | record { eq = eq1 } = lem09 i j lt (cong pred eq) |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
719 ... | no nisb | record { eq = eq1 } = lem09 i (suc j) (≤-trans lt a≤sa) eq |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
720 |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
721 bton : B → ℕ |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
722 bton b = pred (count-B (h⁻¹ (g b))) |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
723 |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
724 lem22 : {n : ℕ } → n < maxb → suc n ≤ count-B n |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
725 lem22 {n} n<mb = ? |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
726 |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
727 lem23 : (b : B) → 0 < count-B (h⁻¹ (g b)) |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
728 lem23 = ? |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
729 |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
730 bton<maxb : (b : B) → bton b < maxb |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
731 bton<maxb b = begin |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
732 suc (bton b) ≡⟨ sucprd (lem23 b) ⟩ |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
733 count-B (h⁻¹ (g b)) ≤⟨ count-B-mono {h⁻¹ (g b)} {finite fa} (<to≤ fin<n) ⟩ |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
734 count-B (finite fa) ≡⟨ refl ⟩ |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
735 maxb ∎ where |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
736 open ≤-Reasoning |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
737 |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
738 ntob : (n : ℕ) → n < maxb → B |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
739 ntob n n<mb = CountB.b (lem01 n n (lem22 n<mb)) |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
740 |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
741 biso : (n : ℕ) → (n<mb : n < maxb) → bton (ntob n n<mb ) ≡ n |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
742 biso n n<mb = begin |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
743 bton (ntob n n<mb ) ≡⟨ refl ⟩ |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
744 pred (count-B (h⁻¹ (g (CountB.b CB)))) ≡⟨ sym ( cong (λ k → pred (count-B (h⁻¹ k))) ( CountB.b=cn CB)) ⟩ |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
745 pred (count-B (h⁻¹ (h (CountB.cb CB)))) ≡⟨ cong (λ k → pred (count-B k)) (h-iso _ cb<fa) ⟩ |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
746 pred (count-B (CountB.cb CB)) ≡⟨ cong pred (CountB.cb=n CB) ⟩ |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
747 pred (suc n) ≡⟨ refl ⟩ |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
748 n ∎ where |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
749 open ≡-Reasoning |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
750 CB : CountB n |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
751 CB = lem01 n n (lem22 n<mb) |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
752 cb<fa : CountB.cb CB < finite fa |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
753 cb<fa = ? |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
754 |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
755 |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
756 -- |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
757 -- uniqueness of ntob is proved by injection |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
758 -- |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
759 biso1 : (b : B) → ntob (bton b) (bton<maxb b) ≡ b |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
760 biso1 b = ? |
|
4456eebbd1bc
copying countable bijection may not easy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
345
diff
changeset
|
761 |