Mercurial > hg > Members > kono > Proof > automaton

comparison automaton-in-agda/src/fin.agda @ 287:ce16779e72a5

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix decrement case
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 28 Dec 2021 03:17:29 +0900
parents f49c6d768e19
children e4b910112fdf
comparison
equal deleted inserted replaced
286:f49c6d768e19 287:ce16779e72a5
162 fin-dup-in-list>n : {n : ℕ } → (qs : List (Fin n)) → (len> : length qs > n ) → FDup-in-list n qs 162 fin-dup-in-list>n : {n : ℕ } → (qs : List (Fin n)) → (len> : length qs > n ) → FDup-in-list n qs
163 fin-dup-in-list>n {zero} [] () 163 fin-dup-in-list>n {zero} [] ()
164 fin-dup-in-list>n {zero} (() ∷ qs) lt 164 fin-dup-in-list>n {zero} (() ∷ qs) lt
165 fin-dup-in-list>n {suc n} qs lt = fdup-phase0 where 165 fin-dup-in-list>n {suc n} qs lt = fdup-phase0 where
166 open import Level using ( Level ) 166 open import Level using ( Level )
167 fdup+1 : (qs : List (Fin (suc n))) (i : Fin n) → fin-dup-in-list i (list-less qs) ≡ true → fin-dup-in-list (fin+1 i) qs ≡ true 167 fdup+1 : (qs : List (Fin (suc n))) (i : Fin n) → fin-dup-in-list i (list-less qs) ≡ true → FDup-in-list (suc n) qs
168 fdup+1 qs i p = f1-phase1 qs p where 168 fdup+1 qs i p with fin-dup-in-list (fromℕ< a<sa ) qs | inspect (fin-dup-in-list (fromℕ< a<sa )) qs
169 f1-phase2 : (qs : List (Fin (suc n)) ) → fin-phase2 i (list-less qs) ≡ true → fin-phase2 (fin+1 i) qs ≡ true 169 ... | true | record {eq = eq } = record { dup = fromℕ< a<sa ; is-dup = eq }
170 f1-phase2 (x ∷ qs) p with NatP.<-cmp (toℕ x) n 170 ... | false | record {eq = ne } = f1-phase1 qs p where
171 f1-phase2 (x ∷ qs) p | tri< a ¬b ¬c with <-fcmp (fin+1 i) x 171 f1-phase2 : (qs : List (Fin (suc n)) ) → fin-phase2 i (list-less qs) ≡ true → {!!}
172 f1-phase2 (x ∷ qs) p with <-fcmp (fin+1 i) x
173 f1-phase2 (x ∷ qs) p | tri< a ¬b ¬c with NatP.<-cmp (toℕ x) n
172 ... | tri< a₁ ¬b₁ ¬c₁ = f1-phase2 qs {!!} 174 ... | tri< a₁ ¬b₁ ¬c₁ = f1-phase2 qs {!!}
173 ... | tri≈ ¬a b ¬c₁ = refl 175 ... | tri≈ ¬a b ¬c₁ = f1-phase2 qs {!!}
174 ... | tri> ¬a ¬b₁ c = f1-phase2 qs {!!} 176 ... | tri> ¬a ¬b₁ c = {!!} -- ⊥-elim ( nat-<> fin<n c )
175 f1-phase2 (x ∷ qs) p | tri≈ ¬a b ¬c = {!!} 177 f1-phase2 (x ∷ qs) p | tri≈ ¬a b ¬c = refl
176 f1-phase2 (x ∷ qs) p | tri> ¬a ¬b c = ⊥-elim ( nat-≤> (fin≤n x) c ) 178 f1-phase2 (x ∷ qs) p | tri> ¬a ¬b c = f1-phase2 qs {!!}
177 f1-phase1 : (qs : List (Fin (suc n)) ) → fin-phase1 i (list-less qs) ≡ true → fin-phase1 (fin+1 i) qs ≡ true 179 f1-phase1 : (qs : List (Fin (suc n)) ) → fin-phase1 i (list-less qs) ≡ true → {!!}
178 f1-phase1 [] () 180 f1-phase1 [] ()
179 f1-phase1 (x ∷ qs) p with <-fcmp (fin+1 i) x 181 f1-phase1 (x ∷ qs) p with <-fcmp (fin+1 i) x
180 ... | tri< a ¬b ¬c = f1-phase1 qs {!!} 182 ... | tri< a ¬b ¬c = f1-phase1 qs {!!}
181 ... | tri≈ ¬a b ¬c = f1-phase2 qs {!!} 183 ... | tri≈ ¬a b ¬c = f1-phase2 qs {!!}
182 ... | tri> ¬a ¬b c = f1-phase1 qs {!!} 184 ... | tri> ¬a ¬b c = f1-phase1 qs {!!}
213 fdup5 : length (x<y→fin-1 c ∷ NList.ls nlist) ≡ length (x ∷ qs) 215 fdup5 : length (x<y→fin-1 c ∷ NList.ls nlist) ≡ length (x ∷ qs)
214 fdup5 = {!!} 216 fdup5 = {!!}
215 fdup-phase0 : FDup-in-list (suc n) qs 217 fdup-phase0 : FDup-in-list (suc n) qs
216 fdup-phase0 with fdup-phase1 qs 218 fdup-phase0 with fdup-phase1 qs
217 ... | case1 dup = record { dup = fromℕ< a<sa ; is-dup = dup } 219 ... | case1 dup = record { dup = fromℕ< a<sa ; is-dup = dup }
218 ... | case2 nlist = record { dup = fin+1 (FDup-in-list.dup fdup) 220 ... | case2 nlist = fdup+1 qs (FDup-in-list.dup fdup) (FDup-in-list.is-dup fdup) where
219 ; is-dup = fdup+1 qs (FDup-in-list.dup fdup) (FDup-in-list.is-dup fdup) } where
220 fdup04 : (length (NList.ls nlist) ≡ length qs) ∨ (suc (length (NList.ls nlist)) ≡ length qs) → length (list-less qs) > n 221 fdup04 : (length (NList.ls nlist) ≡ length qs) ∨ (suc (length (NList.ls nlist)) ≡ length qs) → length (list-less qs) > n
221 fdup04 (case1 eq) = px≤py ( begin 222 fdup04 (case1 eq) = px≤py ( begin
222 suc (suc n) ≤⟨ lt ⟩ 223 suc (suc n) ≤⟨ lt ⟩
223 length qs ≡⟨ sym eq ⟩ 224 length qs ≡⟨ sym eq ⟩
224 length (NList.ls nlist) ≡⟨ cong (λ k → length k) (sym (NList.lseq nlist )) ⟩ 225 length (NList.ls nlist) ≡⟨ cong (λ k → length k) (sym (NList.lseq nlist )) ⟩