Mercurial > hg > Members > kono > Proof > automaton

comparison automaton-in-agda/src/fin.agda @ 320:4a00e5f2b793

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 Fri, 14 Jan 2022 14:39:36 +0900
parents 16e47a3c4eda
children ce4e44cee2d3
comparison
equal deleted inserted replaced
319:cd91a9f313dd 320:4a00e5f2b793
130 f≡→≡ refl = refl 130 f≡→≡ refl = refl
131 131
132 open import Data.List 132 open import Data.List
133 open import Relation.Binary.Definitions 133 open import Relation.Binary.Definitions
134 134
135
136 -----
137 --
138 -- find duplicate element in a List (Fin n)
139 --
140 -- if the length is longer than n, we can find duplicate element as FDup-in-list
141 --
142
135 -- fin-count : { n : ℕ } (q : Fin n) (qs : List (Fin n) ) → ℕ 143 -- fin-count : { n : ℕ } (q : Fin n) (qs : List (Fin n) ) → ℕ
136 -- fin-count q p[ = 0 144 -- fin-count q p[ = 0
137 -- fin-count q (q0 ∷ qs ) with <-fcmp q q0 145 -- fin-count q (q0 ∷ qs ) with <-fcmp q q0
138 -- ... | tri-e = suc (fin-count q qs) 146 -- ... | tri-e = suc (fin-count q qs)
139 -- ... | false = fin-count q qs 147 -- ... | false = fin-count q qs
143 151
144 -- this is far easier 152 -- this is far easier
145 -- fin-not-dup-in-list→len<n : { n : ℕ} (qs : List (Fin n) ) → ( (q : Fin n) → fin-not-dup-in-list qs q) → length qs ≤ n 153 -- fin-not-dup-in-list→len<n : { n : ℕ} (qs : List (Fin n) ) → ( (q : Fin n) → fin-not-dup-in-list qs q) → length qs ≤ n
146 -- fin-not-dup-in-list→len<n = ? 154 -- fin-not-dup-in-list→len<n = ?
147 155
148 fin-phase2 : { n : ℕ } (q : Fin n) (qs : List (Fin n) ) → Bool 156 fin-phase2 : { n : ℕ } (q : Fin n) (qs : List (Fin n) ) → Bool -- find the dup
149 fin-phase2 q [] = false 157 fin-phase2 q [] = false
150 fin-phase2 q (x ∷ qs) with <-fcmp q x 158 fin-phase2 q (x ∷ qs) with <-fcmp q x
151 ... | tri< a ¬b ¬c = fin-phase2 q qs 159 ... | tri< a ¬b ¬c = fin-phase2 q qs
152 ... | tri≈ ¬a b ¬c = true 160 ... | tri≈ ¬a b ¬c = true
153 ... | tri> ¬a ¬b c = fin-phase2 q qs 161 ... | tri> ¬a ¬b c = fin-phase2 q qs
154 fin-phase1 : { n : ℕ } (q : Fin n) (qs : List (Fin n) ) → Bool 162 fin-phase1 : { n : ℕ } (q : Fin n) (qs : List (Fin n) ) → Bool -- find the first element
155 fin-phase1 q [] = false 163 fin-phase1 q [] = false
156 fin-phase1 q (x ∷ qs) with <-fcmp q x 164 fin-phase1 q (x ∷ qs) with <-fcmp q x
157 ... | tri< a ¬b ¬c = fin-phase1 q qs 165 ... | tri< a ¬b ¬c = fin-phase1 q qs
158 ... | tri≈ ¬a b ¬c = fin-phase2 q qs 166 ... | tri≈ ¬a b ¬c = fin-phase2 q qs
159 ... | tri> ¬a ¬b c = fin-phase1 q qs 167 ... | tri> ¬a ¬b c = fin-phase1 q qs