Mercurial > hg > Members > kono > Proof > automaton
annotate agda/finiteSet.agda @ 134:14cf0e1c8d91
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 24 Nov 2019 14:52:20 +0900 |
| parents | 65bea0aad363 |
| children | 2d70f90565c6 |
| rev | line source |
|---|---|
| 111 | 1 {-# OPTIONS --allow-unsolved-metas #-} |
| 44 | 2 module finiteSet where |
| 3 | |
| 69 | 4 open import Data.Nat hiding ( _≟_ ) |
| 83 | 5 open import Data.Fin renaming ( _<_ to _<<_ ) hiding (_≤_) |
| 69 | 6 open import Data.Fin.Properties |
| 76 | 7 open import Data.Empty |
| 69 | 8 open import Relation.Nullary |
| 44 | 9 open import Relation.Binary.Core |
| 46 | 10 open import Relation.Binary.PropositionalEquality |
| 69 | 11 open import logic |
| 78 | 12 open import nat |
| 13 open import Data.Nat.Properties hiding ( _≟_ ) | |
| 44 | 14 |
| 79 | 15 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) |
| 16 | |
| 85 | 17 record Found ( Q : Set ) (p : Q → Bool ) : Set where |
| 18 field | |
| 92 | 19 found-q : Q |
| 20 found-p : p found-q ≡ true | |
| 79 | 21 |
| 115 | 22 lt0 : (n : ℕ) → n Data.Nat.≤ n |
| 23 lt0 zero = z≤n | |
| 24 lt0 (suc n) = s≤s (lt0 n) | |
| 25 lt2 : {m n : ℕ} → m < n → m Data.Nat.≤ n | |
| 26 lt2 {zero} lt = z≤n | |
| 27 lt2 {suc m} {zero} () | |
| 28 lt2 {suc m} {suc n} (s≤s lt) = s≤s (lt2 lt) | |
| 29 | |
| 85 | 30 record FiniteSet ( Q : Set ) { n : ℕ } : Set where |
| 44 | 31 field |
| 32 Q←F : Fin n → Q | |
| 33 F←Q : Q → Fin n | |
| 34 finiso→ : (q : Q) → Q←F ( F←Q q ) ≡ q | |
| 35 finiso← : (f : Fin n ) → F←Q ( Q←F f ) ≡ f | |
| 70 | 36 finℕ : ℕ |
| 37 finℕ = n | |
| 76 | 38 exists1 : (m : ℕ ) → m Data.Nat.≤ n → (Q → Bool) → Bool |
| 39 exists1 zero _ _ = false | |
| 40 exists1 ( suc m ) m<n p = p (Q←F (fromℕ≤ {m} {n} m<n)) \/ exists1 m (lt2 m<n) p | |
| 44 | 41 exists : ( Q → Bool ) → Bool |
| 76 | 42 exists p = exists1 n (lt0 n) p |
|
104
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
95
diff
changeset
|
43 |
| 114 | 44 open import Data.List |
| 45 list1 : (m : ℕ ) → m Data.Nat.≤ n → (Q → Bool) → List Q | |
|
104
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
95
diff
changeset
|
46 list1 zero _ _ = [] |
|
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
95
diff
changeset
|
47 list1 ( suc m ) m<n p with bool-≡-? (p (Q←F (fromℕ≤ {m} {n} m<n))) true |
|
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
95
diff
changeset
|
48 ... | yes _ = Q←F (fromℕ≤ {m} {n} m<n) ∷ list1 m (lt2 m<n) p |
| 114 | 49 ... | no _ = list1 m (lt2 m<n) p |
| 50 to-list : ( Q → Bool ) → List Q | |
|
104
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
95
diff
changeset
|
51 to-list p = list1 n (lt0 n) p |
|
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
95
diff
changeset
|
52 |
| 69 | 53 equal? : Q → Q → Bool |
| 54 equal? q0 q1 with F←Q q0 ≟ F←Q q1 | |
| 55 ... | yes p = true | |
| 56 ... | no ¬p = false | |
| 95 | 57 equal→refl : { x y : Q } → equal? x y ≡ true → x ≡ y |
| 58 equal→refl {q0} {q1} eq with F←Q q0 ≟ F←Q q1 | |
| 59 equal→refl {q0} {q1} refl | yes eq = begin | |
| 60 q0 | |
| 61 ≡⟨ sym ( finiso→ q0) ⟩ | |
| 62 Q←F (F←Q q0) | |
| 63 ≡⟨ cong (λ k → Q←F k ) eq ⟩ | |
| 64 Q←F (F←Q q1) | |
| 65 ≡⟨ finiso→ q1 ⟩ | |
| 66 q1 | |
| 67 ∎ where open ≡-Reasoning | |
| 68 equal→refl {q0} {q1} () | no ne | |
| 87 | 69 equal?-refl : {q : Q} → equal? q q ≡ true |
| 70 equal?-refl {q} with F←Q q ≟ F←Q q | |
| 71 ... | yes p = refl | |
| 72 ... | no ne = ⊥-elim (ne refl) | |
| 77 | 73 fin<n : {n : ℕ} {f : Fin n} → toℕ f < n |
| 74 fin<n {_} {zero} = s≤s z≤n | |
| 75 fin<n {suc n} {suc f} = s≤s (fin<n {n} {f}) | |
| 84 | 76 i=j : {n : ℕ} (i j : Fin n) → toℕ i ≡ toℕ j → i ≡ j |
| 77 i=j {suc n} zero zero refl = refl | |
| 78 i=j {suc n} (suc i) (suc j) eq = cong ( λ k → suc k ) ( i=j i j (cong ( λ k → Data.Nat.pred k ) eq) ) | |
| 85 | 79 -- ¬∀⟶∃¬ : ∀ n {p} (P : Pred (Fin n) p) → Decidable P → ¬ (∀ i → P i) → (∃ λ i → ¬ P i) |
| 80 End : (m : ℕ ) → (p : Q → Bool ) → Set | |
| 81 End m p = (i : Fin n) → m ≤ toℕ i → p (Q←F i ) ≡ false | |
| 82 next-end : {m : ℕ } → ( p : Q → Bool ) → End (suc m) p | |
| 83 | 83 → (m<n : m < n ) → p (Q←F (fromℕ≤ m<n )) ≡ false |
| 85 | 84 → End m p |
| 85 next-end {m} p prev m<n np i m<i with Data.Nat.Properties.<-cmp m (toℕ i) | |
| 86 next-end p prev m<n np i m<i | tri< a ¬b ¬c = prev i a | |
| 87 next-end p prev m<n np i m<i | tri> ¬a ¬b c = ⊥-elim ( nat-≤> m<i c ) | |
| 88 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 | |
| 83 | 89 m<n=i : {n : ℕ } (i : Fin n) {m : ℕ } → m ≡ (toℕ i) → (m<n : m < n ) → fromℕ≤ m<n ≡ i |
| 84 | 90 m<n=i i eq m<n = i=j (fromℕ≤ m<n) i (subst (λ k → k ≡ toℕ i) (sym (toℕ-fromℕ≤ m<n)) eq ) |
| 85 | 91 first-end : ( p : Q → Bool ) → End n p |
| 92 first-end p i i>n = ⊥-elim (nat-≤> i>n (fin<n {n} {i}) ) | |
| 88 | 93 found : { p : Q → Bool } → (q : Q ) → p q ≡ true → exists p ≡ true |
| 94 found {p} q pt = found1 n (lt0 n) ( first-end p ) where | |
| 83 | 95 found1 : (m : ℕ ) (m<n : m Data.Nat.≤ n ) → ((i : Fin n) → m ≤ toℕ i → p (Q←F i ) ≡ false ) → exists1 m m<n p ≡ true |
| 96 found1 0 m<n end = ⊥-elim ( ¬-bool (subst (λ k → k ≡ false ) (cong (λ k → p k) (finiso→ q) ) (end (F←Q q) z≤n )) pt ) | |
| 84 | 97 found1 (suc m) m<n end with bool-≡-? (p (Q←F (fromℕ≤ m<n))) true |
| 98 found1 (suc m) m<n end | yes eq = subst (λ k → k \/ exists1 m (lt2 m<n) p ≡ true ) (sym eq) (bool-or-4 {exists1 m (lt2 m<n) p} ) | |
| 99 found1 (suc m) m<n end | no np = begin | |
| 82 | 100 p (Q←F (fromℕ≤ m<n)) \/ exists1 m (lt2 m<n) p |
| 85 | 101 ≡⟨ bool-or-1 (¬-bool-t np ) ⟩ |
| 82 | 102 exists1 m (lt2 m<n) p |
| 85 | 103 ≡⟨ found1 m (lt2 m<n) (next-end p end m<n (¬-bool-t np )) ⟩ |
| 82 | 104 true |
| 105 ∎ where open ≡-Reasoning | |
| 83 | 106 not-found : { p : Q → Bool } → ( (q : Q ) → p q ≡ false ) → exists p ≡ false |
| 107 not-found {p} pn = not-found2 n (lt0 n) where | |
| 108 not-found2 : (m : ℕ ) → (m<n : m Data.Nat.≤ n ) → exists1 m m<n p ≡ false | |
| 109 not-found2 zero _ = refl | |
| 110 not-found2 ( suc m ) m<n with pn (Q←F (fromℕ≤ {m} {n} m<n)) | |
| 111 not-found2 (suc m) m<n | eq = begin | |
| 112 p (Q←F (fromℕ≤ m<n)) \/ exists1 m (lt2 m<n) p | |
| 85 | 113 ≡⟨ bool-or-1 eq ⟩ |
| 83 | 114 exists1 m (lt2 m<n) p |
| 115 ≡⟨ not-found2 m (lt2 m<n) ⟩ | |
| 116 false | |
| 117 ∎ where open ≡-Reasoning | |
| 85 | 118 open import Level |
| 119 postulate f-extensionality : { n : Level} → Relation.Binary.PropositionalEquality.Extensionality n n -- (Level.suc n) | |
| 120 found← : { p : Q → Bool } → exists p ≡ true → Found Q p | |
| 121 found← {p} exst = found2 n (lt0 n) (first-end p ) where | |
| 122 found2 : (m : ℕ ) (m<n : m Data.Nat.≤ n ) → End m p → Found Q p | |
| 123 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 | |
| 124 lemma : (λ z → p (Q←F (F←Q z))) ≡ p | |
| 125 lemma = f-extensionality ( λ q → subst (λ k → p k ≡ p q ) (sym (finiso→ q)) refl ) | |
| 126 found2 (suc m) m<n end with bool-≡-? (p (Q←F (fromℕ≤ m<n))) true | |
| 92 | 127 found2 (suc m) m<n end | yes eq = record { found-q = Q←F (fromℕ≤ m<n) ; found-p = eq } |
| 85 | 128 found2 (suc m) m<n end | no np = |
| 129 found2 m (lt2 m<n) (next-end p end m<n (¬-bool-t np )) | |
| 130 not-found← : { p : Q → Bool } → exists p ≡ false → (q : Q ) → p q ≡ false | |
| 88 | 131 not-found← {p} np q = ¬-bool-t ( contra-position {_} {_} {_} {exists p ≡ true} (found q) (λ ep → ¬-bool np ep ) ) |
| 44 | 132 |
| 119 | 133 record ISO (A B : Set) : Set where |
| 134 field | |
| 135 A←B : B → A | |
| 136 B←A : A → B | |
| 137 iso← : (q : A) → A←B ( B←A q ) ≡ q | |
| 138 iso→ : (f : B) → B←A ( A←B f ) ≡ f | |
| 139 | |
| 140 iso-fin : {A B : Set} → {n : ℕ } → FiniteSet A {n} → ISO A B → FiniteSet B {n} | |
| 141 iso-fin {A} {B} {n} fin iso = record { | |
| 142 Q←F = λ f → ISO.B←A iso ( FiniteSet.Q←F fin f ) | |
| 143 ; F←Q = λ b → FiniteSet.F←Q fin ( ISO.A←B iso b ) | |
| 144 ; finiso→ = finiso→ | |
| 145 ; finiso← = finiso← | |
| 146 } where | |
| 147 finiso→ : (q : B) → ISO.B←A iso (FiniteSet.Q←F fin (FiniteSet.F←Q fin (ISO.A←B iso q))) ≡ q | |
| 148 finiso→ q = begin | |
| 149 ISO.B←A iso (FiniteSet.Q←F fin (FiniteSet.F←Q fin (ISO.A←B iso q))) | |
| 150 ≡⟨ cong (λ k → ISO.B←A iso k ) (FiniteSet.finiso→ fin _ ) ⟩ | |
| 151 ISO.B←A iso (ISO.A←B iso q) | |
| 152 ≡⟨ ISO.iso→ iso _ ⟩ | |
| 153 q | |
| 154 ∎ where | |
| 155 open ≡-Reasoning | |
| 156 finiso← : (f : Fin n) → FiniteSet.F←Q fin (ISO.A←B iso (ISO.B←A iso (FiniteSet.Q←F fin f))) ≡ f | |
| 157 finiso← f = begin | |
| 158 FiniteSet.F←Q fin (ISO.A←B iso (ISO.B←A iso (FiniteSet.Q←F fin f))) | |
| 159 ≡⟨ cong (λ k → FiniteSet.F←Q fin k ) (ISO.iso← iso _) ⟩ | |
| 160 FiniteSet.F←Q fin (FiniteSet.Q←F fin f) | |
| 161 ≡⟨ FiniteSet.finiso← fin _ ⟩ | |
| 162 f | |
| 163 ∎ where | |
| 164 open ≡-Reasoning | |
| 165 | |
| 120 | 166 data One : Set where |
| 167 one : One | |
| 119 | 168 |
| 120 | 169 fin-∨1 : {B : Set} → { b : ℕ } → FiniteSet B {b} → FiniteSet (One ∨ B) {suc b} |
| 170 fin-∨1 {B} {b} fb = record { | |
| 171 Q←F = Q←F | |
| 172 ; F←Q = F←Q | |
| 173 ; finiso→ = finiso→ | |
| 174 ; finiso← = finiso← | |
| 175 } where | |
| 176 Q←F : Fin (suc b) → One ∨ B | |
| 177 Q←F zero = case1 one | |
| 178 Q←F (suc f) = case2 (FiniteSet.Q←F fb f) | |
| 179 F←Q : One ∨ B → Fin (suc b) | |
| 180 F←Q (case1 one) = zero | |
| 181 F←Q (case2 f ) = suc (FiniteSet.F←Q fb f) | |
| 182 finiso→ : (q : One ∨ B) → Q←F (F←Q q) ≡ q | |
| 183 finiso→ (case1 one) = refl | |
| 184 finiso→ (case2 b) = cong (λ k → case2 k ) (FiniteSet.finiso→ fb b) | |
| 185 finiso← : (q : Fin (suc b)) → F←Q (Q←F q) ≡ q | |
| 186 finiso← zero = refl | |
| 187 finiso← (suc f) = cong ( λ k → suc k ) (FiniteSet.finiso← fb f) | |
| 188 | |
| 189 | |
| 190 fin-∨2 : {B : Set} → ( a : ℕ ) → { b : ℕ } → FiniteSet B {b} → FiniteSet (Fin a ∨ B) {a Data.Nat.+ b} | |
| 191 fin-∨2 {B} zero {b} fb = iso-fin fb iso where | |
| 119 | 192 iso : ISO B (Fin zero ∨ B) |
| 193 iso = record { | |
| 194 A←B = A←B | |
| 195 ; B←A = λ b → case2 b | |
| 196 ; iso→ = iso→ | |
| 197 ; iso← = λ _ → refl | |
| 198 } where | |
| 199 A←B : Fin zero ∨ B → B | |
| 200 A←B (case2 x) = x | |
| 201 iso→ : (f : Fin zero ∨ B ) → case2 (A←B f) ≡ f | |
| 202 iso→ (case2 x) = refl | |
| 120 | 203 fin-∨2 {B} (suc a) {b} fb = iso-fin (fin-∨1 (fin-∨2 a fb) ) iso |
| 204 where | |
| 205 iso : ISO (One ∨ (Fin a ∨ B) ) (Fin (suc a) ∨ B) | |
| 206 ISO.A←B iso (case1 zero) = case1 one | |
| 207 ISO.A←B iso (case1 (suc f)) = case2 (case1 f) | |
| 208 ISO.A←B iso (case2 b) = case2 (case2 b) | |
| 209 ISO.B←A iso (case1 one) = case1 zero | |
| 210 ISO.B←A iso (case2 (case1 f)) = case1 (suc f) | |
| 211 ISO.B←A iso (case2 (case2 b)) = case2 b | |
| 212 ISO.iso← iso (case1 one) = refl | |
| 213 ISO.iso← iso (case2 (case1 x)) = refl | |
| 214 ISO.iso← iso (case2 (case2 x)) = refl | |
| 215 ISO.iso→ iso (case1 zero) = refl | |
| 216 ISO.iso→ iso (case1 (suc x)) = refl | |
| 217 ISO.iso→ iso (case2 x) = refl | |
| 119 | 218 |
| 219 | |
| 120 | 220 FiniteSet→Fin : {A : Set} → { a : ℕ } → (fin : FiniteSet A {a} ) → ISO (Fin a) A |
| 221 ISO.A←B (FiniteSet→Fin fin) f = FiniteSet.F←Q fin f | |
| 222 ISO.B←A (FiniteSet→Fin fin) f = FiniteSet.Q←F fin f | |
| 223 ISO.iso← (FiniteSet→Fin fin) = FiniteSet.finiso← fin | |
| 224 ISO.iso→ (FiniteSet→Fin fin) = FiniteSet.finiso→ fin | |
| 225 | |
| 226 | |
| 121 | 227 fin-∨ : {A B : Set} → { a b : ℕ } → FiniteSet A {a} → FiniteSet B {b} → FiniteSet (A ∨ B) {a Data.Nat.+ b} |
| 228 fin-∨ {A} {B} {a} {b} fa fb = iso-fin (fin-∨2 a fb ) iso2 where | |
| 120 | 229 ia = FiniteSet→Fin fa |
| 230 iso2 : ISO (Fin a ∨ B ) (A ∨ B) | |
| 231 ISO.A←B iso2 (case1 x) = case1 ( ISO.A←B ia x ) | |
| 232 ISO.A←B iso2 (case2 x) = case2 x | |
| 233 ISO.B←A iso2 (case1 x) = case1 ( ISO.B←A ia x ) | |
| 234 ISO.B←A iso2 (case2 x) = case2 x | |
| 235 ISO.iso← iso2 (case1 x) = cong ( λ k → case1 k ) (ISO.iso← ia x) | |
| 236 ISO.iso← iso2 (case2 x) = refl | |
| 237 ISO.iso→ iso2 (case1 x) = cong ( λ k → case1 k ) (ISO.iso→ ia x) | |
| 238 ISO.iso→ iso2 (case2 x) = refl | |
| 111 | 239 |
| 240 import Data.Nat.DivMod | |
| 241 import Data.Nat.Properties | |
| 242 | |
| 112 | 243 open _∧_ |
| 244 | |
| 114 | 245 open import Data.Vec |
| 246 import Data.Product | |
| 247 | |
| 248 exp2 : (n : ℕ ) → exp 2 (suc n) ≡ exp 2 n Data.Nat.+ exp 2 n | |
| 249 exp2 n = begin | |
| 250 exp 2 (suc n) | |
| 251 ≡⟨⟩ | |
| 252 2 * ( exp 2 n ) | |
| 253 ≡⟨ *-comm 2 (exp 2 n) ⟩ | |
| 254 ( exp 2 n ) * 2 | |
| 255 ≡⟨ +-*-suc ( exp 2 n ) 1 ⟩ | |
| 256 (exp 2 n ) Data.Nat.+ ( exp 2 n ) * 1 | |
| 257 ≡⟨ cong ( λ k → (exp 2 n ) Data.Nat.+ k ) (proj₂ *-identity (exp 2 n) ) ⟩ | |
| 258 exp 2 n Data.Nat.+ exp 2 n | |
| 259 ∎ where | |
| 260 open ≡-Reasoning | |
| 261 open Data.Product | |
| 262 | |
| 263 cast-iso : {n m : ℕ } → (eq : n ≡ m ) → (f : Fin m ) → cast eq ( cast (sym eq ) f) ≡ f | |
| 264 cast-iso refl zero = refl | |
| 265 cast-iso refl (suc f) = cong ( λ k → suc k ) ( cast-iso refl f ) | |
| 266 | |
| 267 | |
| 268 fin2List : {n : ℕ } → FiniteSet (Vec Bool n) {exp 2 n } | |
| 269 fin2List {zero} = record { | |
| 270 Q←F = λ _ → Vec.[] | |
| 271 ; F←Q = λ _ → # 0 | |
| 111 | 272 ; finiso→ = finiso→ |
| 273 ; finiso← = finiso← | |
| 274 } where | |
| 114 | 275 Q = Vec Bool zero |
| 276 finiso→ : (q : Q) → [] ≡ q | |
| 277 finiso→ [] = refl | |
| 278 finiso← : (f : Fin (exp 2 zero)) → # 0 ≡ f | |
| 279 finiso← zero = refl | |
| 121 | 280 fin2List {suc n} = subst (λ k → FiniteSet (Vec Bool (suc n)) {k} ) (sym (exp2 n)) ( iso-fin (fin-∨ (fin2List {n}) (fin2List {n})) iso ) |
| 120 | 281 where |
| 114 | 282 QtoR : Vec Bool (suc n) → Vec Bool n ∨ Vec Bool n |
| 283 QtoR ( true ∷ x ) = case1 x | |
| 284 QtoR ( false ∷ x ) = case2 x | |
| 285 RtoQ : Vec Bool n ∨ Vec Bool n → Vec Bool (suc n) | |
| 286 RtoQ ( case1 x ) = true ∷ x | |
| 287 RtoQ ( case2 x ) = false ∷ x | |
| 288 isoRQ : (x : Vec Bool (suc n) ) → RtoQ ( QtoR x ) ≡ x | |
| 289 isoRQ (true ∷ _ ) = refl | |
| 290 isoRQ (false ∷ _ ) = refl | |
| 291 isoQR : (x : Vec Bool n ∨ Vec Bool n ) → QtoR ( RtoQ x ) ≡ x | |
| 292 isoQR (case1 x) = refl | |
| 293 isoQR (case2 x) = refl | |
| 120 | 294 iso : ISO (Vec Bool n ∨ Vec Bool n) (Vec Bool (suc n)) |
| 295 iso = record { A←B = QtoR ; B←A = RtoQ ; iso← = isoQR ; iso→ = isoRQ } | |
| 111 | 296 |
| 124 | 297 F2L : {Q : Set } {n m : ℕ } → n < suc m → (fin : FiniteSet Q {m} ) → ( (q : Q) → toℕ (FiniteSet.F←Q fin q ) < n → Bool ) → Vec Bool n |
| 298 F2L {Q} {zero} fin _ Q→B = [] | |
| 299 F2L {Q} {suc n} (s≤s n<m) fin Q→B = Q→B (FiniteSet.Q←F fin (fromℕ≤ n<m)) lemma6 ∷ F2L {Q} {n} (Data.Nat.Properties.<-trans n<m a<sa ) fin qb1 where | |
| 300 lemma6 : toℕ (FiniteSet.F←Q fin (FiniteSet.Q←F fin (fromℕ≤ n<m))) < suc n | |
| 301 lemma6 = subst (λ k → toℕ k < suc n ) (sym (FiniteSet.finiso← fin _ )) (subst (λ k → k < suc n) (sym (toℕ-fromℕ≤ n<m )) a<sa ) | |
| 302 qb1 : (q : Q) → toℕ (FiniteSet.F←Q fin q) < n → Bool | |
| 303 qb1 q q<n = Q→B q (Data.Nat.Properties.<-trans q<n a<sa) | |
| 116 | 304 |
| 117 | 305 List2Func : { Q : Set } → {n m : ℕ } → n < suc m → FiniteSet Q {m} → Vec Bool n → Q → Bool |
| 121 | 306 List2Func {Q} {zero} (s≤s z≤n) fin [] q = false |
| 117 | 307 List2Func {Q} {suc n} {m} (s≤s n<m) fin (h ∷ t) q with FiniteSet.F←Q fin q ≟ fromℕ≤ n<m |
| 116 | 308 ... | yes _ = h |
| 117 | 309 ... | no _ = List2Func {Q} {n} {m} (Data.Nat.Properties.<-trans n<m a<sa ) fin t q |
| 116 | 310 |
| 124 | 311 F2L-iso : { Q : Set } → {n : ℕ } → (fin : FiniteSet Q {n}) → (x : Vec Bool n ) → F2L a<sa fin (λ q _ → List2Func a<sa fin x q ) ≡ x |
| 312 F2L-iso {Q} {m} fin x = f2l m a<sa x where | |
| 313 f2l : (n : ℕ ) → (n<m : n < suc m )→ (x : Vec Bool n ) → F2L n<m fin (λ q q<n → List2Func n<m fin x q ) ≡ x | |
| 120 | 314 f2l zero (s≤s z≤n) [] = refl |
| 123 | 315 f2l (suc n) (s≤s n<m) (h ∷ t ) = lemma1 lemma2 lemma3 where |
| 121 | 316 lemma1 : {n : ℕ } → {h h1 : Bool } → {t t1 : Vec Bool n } → h ≡ h1 → t ≡ t1 → h ∷ t ≡ h1 ∷ t1 |
| 317 lemma1 refl refl = refl | |
| 318 lemma2 : List2Func (s≤s n<m) fin (h ∷ t) (FiniteSet.Q←F fin (fromℕ≤ n<m)) ≡ h | |
| 319 lemma2 with FiniteSet.F←Q fin (FiniteSet.Q←F fin (fromℕ≤ n<m)) ≟ fromℕ≤ n<m | |
| 320 lemma2 | yes p = refl | |
| 124 | 321 lemma2 | no ¬p = ⊥-elim ( ¬p (FiniteSet.finiso← fin _) ) |
| 123 | 322 lemma4 : (q : Q ) → toℕ (FiniteSet.F←Q fin q ) < n → List2Func (s≤s n<m) fin (h ∷ t) q ≡ List2Func (Data.Nat.Properties.<-trans n<m a<sa) fin t q |
| 323 lemma4 q _ with FiniteSet.F←Q fin q ≟ fromℕ≤ n<m | |
| 324 lemma4 q lt | yes p = ⊥-elim ( nat-≡< (toℕ-fromℕ≤ n<m) (lemma5 n lt (cong (λ k → toℕ k) p))) where | |
| 325 lemma5 : {j k : ℕ } → ( n : ℕ) → suc j ≤ n → j ≡ k → k < n | |
| 326 lemma5 {zero} (suc n) (s≤s z≤n) refl = s≤s z≤n | |
| 327 lemma5 {suc j} (suc n) (s≤s lt) refl = s≤s (lemma5 {j} n lt refl) | |
| 328 lemma4 q _ | no ¬p = refl | |
| 124 | 329 lemma3 : F2L (Data.Nat.Properties.<-trans n<m a<sa) fin (λ q q<n → List2Func (s≤s n<m) fin (h ∷ t) q ) ≡ t |
| 123 | 330 lemma3 = begin |
| 124 | 331 F2L (Data.Nat.Properties.<-trans n<m a<sa) fin (λ q q<n → List2Func (s≤s n<m) fin (h ∷ t) q ) |
| 332 ≡⟨ cong (λ k → F2L (Data.Nat.Properties.<-trans n<m a<sa) fin ( λ q q<n → k q q<n )) | |
| 123 | 333 (FiniteSet.f-extensionality fin ( λ q → |
| 334 (FiniteSet.f-extensionality fin ( λ q<n → lemma4 q q<n )))) ⟩ | |
| 124 | 335 F2L (Data.Nat.Properties.<-trans n<m a<sa) fin (λ q q<n → List2Func (Data.Nat.Properties.<-trans n<m a<sa) fin t q ) |
| 123 | 336 ≡⟨ f2l n (Data.Nat.Properties.<-trans n<m a<sa ) t ⟩ |
| 337 t | |
| 338 ∎ where | |
| 339 open ≡-Reasoning | |
| 111 | 340 |
| 125 | 341 |
| 342 L2F : {Q : Set } {n m : ℕ } → n < suc m → (fin : FiniteSet Q {m} ) → Vec Bool n → (q : Q ) → toℕ (FiniteSet.F←Q fin q ) < n → Bool | |
| 343 L2F n<m fin x q q<n = List2Func n<m fin x q | |
| 344 | |
| 345 L2F-iso : { Q : Set } → {n : ℕ } → (fin : FiniteSet Q {n}) → (f : Q → Bool ) → (q : Q ) → (L2F a<sa fin (F2L a<sa fin (λ q _ → f q) )) q (toℕ<n _) ≡ f q | |
| 346 L2F-iso {Q} {m} fin f q = l2f m a<sa (toℕ<n _) where | |
| 347 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 | |
| 348 lemma11 {n} n<m ¬q=n q≤n = lemma13 n<m (contra-position (lemma12 n<m _) ¬q=n ) q≤n where | |
| 349 lemma13 : {n nq : ℕ } → (n<m : n < m ) → ¬ ( nq ≡ n ) → nq ≤ n → nq < n | |
| 350 lemma13 {0} {0} (s≤s z≤n) nt z≤n = ⊥-elim ( nt refl ) | |
| 351 lemma13 {suc _} {0} (s≤s (s≤s n<m)) nt z≤n = s≤s z≤n | |
| 352 lemma13 {suc n} {suc nq} n<m nt (s≤s nq≤n) = s≤s (lemma13 {n} {nq} (Data.Nat.Properties.<-trans a<sa n<m ) (λ eq → nt ( cong ( λ k → suc k ) eq )) nq≤n) | |
| 353 lemma3 : {a b : ℕ } → (lt : a < b ) → fromℕ≤ (s≤s lt) ≡ suc (fromℕ≤ lt) | |
| 354 lemma3 (s≤s lt) = refl | |
| 355 lemma12 : {n m : ℕ } → (n<m : n < m ) → (f : Fin m ) → toℕ f ≡ n → f ≡ fromℕ≤ n<m | |
| 356 lemma12 {zero} {suc m} (s≤s z≤n) zero refl = refl | |
| 357 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 ) ) | |
| 358 l2f : (n : ℕ ) → (n<m : n < suc m ) → (q<n : toℕ (FiniteSet.F←Q fin q ) < n ) → (L2F n<m fin (F2L n<m fin (λ q _ → f q))) q q<n ≡ f q | |
| 359 l2f zero (s≤s z≤n) () | |
| 126 | 360 l2f (suc n) (s≤s n<m) (s≤s n<q) with FiniteSet.F←Q fin q ≟ fromℕ≤ n<m |
| 361 l2f (suc n) (s≤s n<m) (s≤s n<q) | yes p with inspect f q | |
| 362 l2f (suc n) (s≤s n<m) (s≤s n<q) | yes p | record { eq = refl } = begin | |
| 363 f (FiniteSet.Q←F fin (fromℕ≤ n<m)) | |
| 364 ≡⟨ cong ( λ k → f (FiniteSet.Q←F fin k )) (sym p) ⟩ | |
| 365 f (FiniteSet.Q←F fin ( FiniteSet.F←Q fin q )) | |
| 366 ≡⟨ cong ( λ k → f k ) (FiniteSet.finiso→ fin _ ) ⟩ | |
| 367 f q | |
| 368 ∎ where | |
| 369 open ≡-Reasoning | |
| 125 | 370 l2f (suc n) (s≤s n<m) (s≤s n<q) | no ¬p = l2f n (Data.Nat.Properties.<-trans n<m a<sa) (lemma11 n<m ¬p n<q) |
| 126 | 371 |
| 372 fin→ : {A : Set} → { a : ℕ } → FiniteSet A {a} → FiniteSet (A → Bool ) {exp 2 a} | |
| 373 fin→ {A} {a} fin = iso-fin fin2List iso where | |
| 374 iso : ISO (Vec Bool a ) (A → Bool) | |
| 375 ISO.A←B iso x = F2L a<sa fin ( λ q _ → x q ) | |
| 376 ISO.B←A iso x = List2Func a<sa fin x | |
| 377 ISO.iso← iso x = F2L-iso fin x | |
| 378 ISO.iso→ iso x = lemma where | |
| 379 lemma : List2Func a<sa fin (F2L a<sa fin (λ q _ → x q)) ≡ x | |
| 380 lemma = FiniteSet.f-extensionality fin ( λ q → L2F-iso fin x q ) | |
| 381 | |
| 382 | |
| 383 open import Data.Product | |
| 384 | |
| 128 | 385 record Fin-< { n m : ℕ } (n<m : n < m ) { A : Set } (fa : FiniteSet A {m}) : Set where |
| 386 field | |
| 387 elm : A | |
| 388 elm<n : toℕ (FiniteSet.F←Q fa elm ) < n | |
| 389 | |
| 130 | 390 open Fin-< |
| 133 | 391 |
| 392 Fin-<-cong : { n m : ℕ } (n<m : n < m ) { A : Set } (fa : FiniteSet A {m}) | |
| 393 → ( s t : Fin-< n<m fa ) | |
| 394 → ( elm s ≡ elm t) → ( elm<n s ≅ elm<n t ) → s ≡ t | |
| 395 Fin-<-cong n<m fa _ _ refl HE.refl = refl | |
| 396 | |
| 397 lemma1 : {m n : ℕ } → ( i j : m < n ) → i ≡ j | |
| 398 lemma1 {zero} {suc n} (s≤s z≤n) (s≤s z≤n) = refl | |
| 399 lemma1 {suc m} {suc n} (s≤s i) (s≤s j) = cong ( λ k → s≤s k ) ( lemma1 {m} {n} i j ) | |
| 400 | |
| 128 | 401 fin-< : {A : Set} → { n m : ℕ } → (n<m : n < m ) → (fa : FiniteSet A {m}) → FiniteSet (Fin-< n<m fa) {n} |
|
129
fb6237e9a98b
bad direction on fin-<
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
128
diff
changeset
|
402 fin-< {A} {zero} {m} (s≤s z≤n) fa = record { Q←F = λ () ; F←Q = λ () ; finiso← = λ () ; finiso→ = λ () } |
|
fb6237e9a98b
bad direction on fin-<
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
128
diff
changeset
|
403 fin-< {A} {suc n} {m} (s≤s n<m) fa = iso-fin (fin-∨1 (fin-< {A} {n} {m} (Data.Nat.Properties.<-trans n<m a<sa) fa)) iso where |
|
fb6237e9a98b
bad direction on fin-<
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
128
diff
changeset
|
404 fin- : FiniteSet (Fin-< (Data.Nat.Properties.<-trans n<m a<sa) fa) |
|
fb6237e9a98b
bad direction on fin-<
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
128
diff
changeset
|
405 fin- = fin-< {A} {n} {m} (Data.Nat.Properties.<-trans n<m a<sa) fa |
| 130 | 406 iso : ISO (One ∨ Fin-< (Data.Nat.Properties.<-trans n<m a<sa) fa) (Fin-< (s≤s n<m) fa) |
| 132 | 407 lastf = FiniteSet.F←Q fa (FiniteSet.Q←F fa (fromℕ≤ (Data.Nat.Properties.<-trans n<m a<sa) )) |
| 408 c1 : toℕ lastf ≡ n | |
| 130 | 409 c1 = subst (λ k → toℕ k ≡ n ) (sym (FiniteSet.finiso← fa _ )) (subst (λ k → k ≡ n) (sym (toℕ-fromℕ≤ _ )) refl ) |
| 132 | 410 f<n : toℕ lastf < suc n |
| 130 | 411 f<n = subst ( λ k → k < suc n ) (sym c1) a<sa |
| 133 | 412 last1 = FiniteSet.Q←F fa (fromℕ≤ (Data.Nat.Properties.<-trans n<m a<sa)) |
| 130 | 413 ISO.A←B iso x with Data.Nat.Properties.<-cmp (toℕ (FiniteSet.F←Q fa (elm x )) ) n |
| 414 ISO.A←B iso x | tri< a ¬b ¬c = case2 record { elm = elm x ; elm<n = a } | |
| 415 ISO.A←B iso x | tri≈ ¬a b ¬c = case1 one | |
| 416 ISO.A←B iso x | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c (elm<n x) ) | |
| 132 | 417 ISO.B←A iso (case1 one) = record { elm = last1 ; elm<n = f<n } |
| 130 | 418 ISO.B←A iso (case2 x) = record { elm = elm x ; elm<n = Data.Nat.Properties.<-trans (elm<n x) a<sa } |
| 419 ISO.iso← iso (case1 one) with Data.Nat.Properties.<-cmp (toℕ (FiniteSet.F←Q fa (elm (ISO.B←A iso (case1 one))))) n | |
| 420 ISO.iso← iso (case1 one) | tri< a ¬b ¬c = ⊥-elim ( ¬b c1 ) | |
| 421 ISO.iso← iso (case1 one) | tri≈ ¬a b ¬c = refl | |
| 422 ISO.iso← iso (case1 one) | tri> ¬a ¬b c = ⊥-elim ( ¬b c1 ) | |
| 423 ISO.iso← iso (case2 x) with Data.Nat.Properties.<-cmp (toℕ (FiniteSet.F←Q fa (elm x))) n | |
| 424 ISO.iso← iso (case2 x) | tri< a ¬b ¬c = cong ( λ k → case2 record { elm = elm x ; elm<n = k } ) (lemma1 _ _) where | |
| 425 ISO.iso← iso (case2 x) | tri≈ ¬a b ¬c = ⊥-elim ( nat-≡< b (elm<n x) ) | |
| 426 ISO.iso← iso (case2 x) | tri> ¬a ¬b c = ⊥-elim ( nat-<> c (elm<n x) ) | |
| 132 | 427 ISO.iso→ iso x with ISO.A←B iso x |
| 134 | 428 ISO.iso→ iso x | case1 one with Data.Nat.Properties.<-cmp (toℕ (FiniteSet.F←Q fa (elm x )) ) n |
| 429 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c (elm<n x) ) | |
| 430 ... | tri< a ¬b ¬c = {!!} | |
| 431 ... | tri≈ ¬a b ¬c = begin | |
| 133 | 432 record { elm = FiniteSet.Q←F fa (fromℕ≤ (Data.Nat.Properties.<-trans n<m a<sa)) ; elm<n = lemma5 } |
| 433 ≡⟨ Fin-<-cong (s≤s n<m) fa _ _ (sym (lemma2 b)) lemma7 ⟩ | |
| 434 record { elm = elm x ; elm<n = elm<n x } | |
| 435 ≡⟨⟩ | |
| 436 x | |
| 437 ∎ | |
| 438 where | |
| 439 open ≡-Reasoning | |
| 440 lemma3 : {n m : ℕ } (x : Fin m) → toℕ x ≡ n → (n<m : n < m ) → x ≡ fromℕ≤ n<m | |
| 441 lemma3 _ refl n<m = sym ( fromℕ≤-toℕ _ n<m ) | |
| 442 lemma4 : {x : A } → (x=n : toℕ (FiniteSet.F←Q fa x) ≡ n ) → fromℕ≤ (Data.Nat.Properties.<-trans n<m a<sa) ≡ FiniteSet.F←Q fa x | |
| 443 lemma4 {x} refl = sym ( lemma3 _ refl (Data.Nat.Properties.<-trans n<m a<sa)) | |
| 444 lemma2 : {x : A} → toℕ (FiniteSet.F←Q fa x) ≡ n → x ≡ FiniteSet.Q←F fa (fromℕ≤ (Data.Nat.Properties.<-trans n<m a<sa)) | |
| 445 lemma2 {x} refl = sym ( begin | |
| 446 FiniteSet.Q←F fa (fromℕ≤ (Data.Nat.Properties.<-trans n<m a<sa)) | |
| 447 ≡⟨ cong (λ k → FiniteSet.Q←F fa k) (lemma4 refl) ⟩ | |
| 448 FiniteSet.Q←F fa ( FiniteSet.F←Q fa x ) | |
| 449 ≡⟨ FiniteSet.finiso→ fa _ ⟩ | |
| 450 x | |
| 451 ∎ ) where open ≡-Reasoning | |
| 452 lemma5 : toℕ (FiniteSet.F←Q fa (FiniteSet.Q←F fa (fromℕ≤ (Data.Nat.Properties.<-trans n<m a<sa)))) < suc n | |
| 453 lemma5 = subst (λ k → suc k ≤ suc n) | |
| 454 (sym | |
| 455 (subst (λ k → toℕ k ≡ n) | |
| 456 (sym | |
| 457 (FiniteSet.finiso← fa | |
| 458 (fromℕ≤ (Data.Nat.Properties.<-trans n<m a<sa)))) | |
| 459 (subst (λ k → k ≡ n) | |
| 460 (sym (toℕ-fromℕ≤ (Data.Nat.Properties.<-trans n<m a<sa))) refl))) | |
| 461 a<sa | |
| 462 lemma7 : lemma5 ≅ elm<n x | |
| 463 lemma7 with lemma2 b | |
| 464 ... | refl with lemma1 lemma5 (elm<n x) | |
| 465 ... | refl = HE.refl | |
| 466 | |
| 132 | 467 ISO.iso→ iso x | case2 x1 = {!!} |
| 131 | 468 -- ISO.iso→ iso x | case2 x1 | tri< a ¬b ¬c = ? |
| 469 -- ISO.iso→ iso x | case2 x1 | tri≈ ¬a b ¬c = {!!} | |
| 470 -- ISO.iso→ iso x | case2 x1 | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c (elm<n x) ) | |
| 128 | 471 |
| 126 | 472 fin-× : {A B : Set} → { a b : ℕ } → FiniteSet A {a} → FiniteSet B {b} → FiniteSet (A × B) {a * b} |
| 473 fin-× {A} {B} {a} {b} fa fb with FiniteSet→Fin fa | |
| 474 ... | a=f = iso-fin (fin-×-f a ) iso-1 where | |
| 475 iso-1 : ISO (Fin a × B) ( A × B ) | |
| 476 ISO.A←B iso-1 x = ( FiniteSet.F←Q fa (proj₁ x) , proj₂ x) | |
| 477 ISO.B←A iso-1 x = ( FiniteSet.Q←F fa (proj₁ x) , proj₂ x) | |
| 478 ISO.iso← iso-1 x = lemma where | |
| 479 lemma : (FiniteSet.F←Q fa (FiniteSet.Q←F fa (proj₁ x)) , proj₂ x) ≡ ( proj₁ x , proj₂ x ) | |
| 480 lemma = cong ( λ k → ( k , proj₂ x ) ) (FiniteSet.finiso← fa _ ) | |
| 481 ISO.iso→ iso-1 x = cong ( λ k → ( k , proj₂ x ) ) (FiniteSet.finiso→ fa _ ) | |
| 482 iso-2 : {a : ℕ } → ISO (B ∨ (Fin a × B)) (Fin (suc a) × B) | |
| 483 ISO.A←B iso-2 (zero , b ) = case1 b | |
| 484 ISO.A←B iso-2 (suc fst , b ) = case2 ( fst , b ) | |
| 485 ISO.B←A iso-2 (case1 b) = ( zero , b ) | |
| 486 ISO.B←A iso-2 (case2 (a , b )) = ( suc a , b ) | |
| 487 ISO.iso← iso-2 (case1 x) = refl | |
| 488 ISO.iso← iso-2 (case2 x) = refl | |
| 489 ISO.iso→ iso-2 (zero , b ) = refl | |
| 490 ISO.iso→ iso-2 (suc a , b ) = refl | |
| 491 fin-×-f : ( a : ℕ ) → FiniteSet ((Fin a) × B) {a * b} | |
| 492 fin-×-f zero = record { Q←F = λ () ; F←Q = λ () ; finiso→ = λ () ; finiso← = λ () } | |
| 493 fin-×-f (suc a) = iso-fin ( fin-∨ fb ( fin-×-f a ) ) iso-2 |