Mercurial > hg > Members > kono > Proof > automaton

comparison automaton-in-agda/src/fin.agda @ 344:43bce021e3d2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 15 Jul 2023 18:44:51 +0900
parents e45dab4b0a7f
children 6ba2836177b4
comparison
equal deleted inserted replaced
343:e45dab4b0a7f 344:43bce021e3d2
135 ----- 135 -----
136 -- 136 --
137 -- find duplicate element in a List (Fin n) 137 -- find duplicate element in a List (Fin n)
138 -- 138 --
139 -- if the length is longer than n, we can find duplicate element as FDup-in-list 139 -- if the length is longer than n, we can find duplicate element as FDup-in-list
140 --
141
142 -- record fDUP {n m : ℕ} (n<m : n < m) ( f : Fin m → Fin n ) : Set where
143 -- field
144 -- i j : Fin m
145 -- i<j : toℕ i < toℕ j
146 -- dup : f i ≡ f j
147 --
148 -- n<m→fDUP : (n m : ℕ) → (n<m : n < m ) → ( f : Fin m → Fin n ) → fDUP n<m f
149 -- n<m→fDUP n (suc m) n<sm f = ? where
150 -- f-1 : Fin m → Fin n
151 -- f-1 zero = f zero
152 -- f-1 (suc x) = f (fromℕ< (<-trans (fin<n {_} {suc x}) a<sa))
153 -- nf00 : fDUP n<sm f ∨ ( (n<m : n < m ) → fDUP n<m f-1 )
154 -- nf00 = ?
155
156 n<m→fDUP : (n m : ℕ) → (n<m : n < m ) → ( f : Fin m → Fin n ) → ¬ ((i j : Fin m) → f i ≡ f j → i ≡ j )
157 n<m→fDUP n m n<m f fi = ? where
158 record IsImage (x : ℕ) : Set where
159 field
160 x<n : x < n
161 y : Fin m
162 x=fy : fromℕ< x<n ≡ f y
163 data gfImage : (x : ℕ) → Set where
164 a-g : (x : Fin n) → (¬ib : ¬ IsImage (toℕ x) ) → gfImage (toℕ x)
165 next-gf : {x : Fin n} → (ix : IsImage (toℕ x)) → (gfiy : gfImage (toℕ (IsImage.y ix)) ) → gfImage (toℕ x)
166 nf00 : (x : Fin n) → Dec ( gfImage (toℕ x))
167 nf00 x = ? where
168 nf04 : (i : ℕ) → i < m → Dec ( gfImage (toℕ x))
169 nf04 zero i<m with <-cmp (toℕ (f (fromℕ< i<m))) (toℕ x)
170 ... | tri< a ¬b ¬c = yes (a-g ? ?)
171 ... | tri≈ ¬a b ¬c = no (λ lt → ? )
172 ... | tri> ¬a ¬b c = ?
173 nf04 (suc i) i<m = ?
174 nf01 : (x : Fin m) → Dec ( IsImage (toℕ x))
175 nf01 x = ? where
176 nf04 : (i : ℕ) → i < m → Dec ( IsImage (toℕ x))
177 nf04 zero i<m with <-cmp (toℕ (f (fromℕ< i<m))) (toℕ x)
178 ... | tri< a ¬b ¬c = yes (?)
179 ... | tri≈ ¬a b ¬c = yes record { x<n = ? ; y = ? ; x=fy = ? }
180 ... | tri> ¬a ¬b c = ?
181 nf04 (suc i) i<m = ?
182 nf02 : (x : Fin n) → ¬ ( gfImage (toℕ x)) → IsImage (toℕ x)
183 nf02 = ?
184 f⁻¹ : Fin n → Fin m
185 f⁻¹ = ?
186 fiso : (x : Fin n) → f (f⁻¹ x) ≡ x
187 fiso = ?
188 nf03 : n < toℕ ( f ( fromℕ< ? ) )
189 nf03 = ?
190 140
191 list2func : (n : ℕ) → (x : List (Fin n)) → n < length x → Fin (length x) → Fin n 141 list2func : (n : ℕ) → (x : List (Fin n)) → n < length x → Fin (length x) → Fin n
192 list2func n x n<l y = lf00 (toℕ y) x fin<n where 142 list2func n x n<l y = lf00 (toℕ y) x fin<n where
193 lf00 : (i : ℕ) → (x : List (Fin n)) → i < length x → Fin n 143 lf00 : (i : ℕ) → (x : List (Fin n)) → i < length x → Fin n
194 lf00 zero (x ∷ t) lt = x 144 lf00 zero (x ∷ t) lt = x