Mercurial > hg > Members > kono > Proof > automaton

comparison automaton-in-agda/src/fin.agda @ 284:c9f20dec63ad

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 Mon, 27 Dec 2021 21:45:00 +0900
parents e5a0499e7b40
children 6e85b8b0d8db
comparison
equal deleted inserted replaced
283:e5a0499e7b40 284:c9f20dec63ad
1 {-# OPTIONS --allow-unsolved-metas #-} 1 {-# OPTIONS --allow-unsolved-metas #-}
2 2
3 module fin where 3 module fin where
4 4
5 open import Data.Fin hiding (_<_ ; _≤_ ; _>_ ; _+_ ) 5 open import Data.Fin hiding (_<_ ; _≤_ ; _>_ ; _+_ )
6 open import Data.Fin.Properties hiding ( <-trans ; ≤-refl ) renaming ( <-cmp to <-fcmp ) 6 open import Data.Fin.Properties hiding (≤-trans ; <-trans ; ≤-refl ) renaming ( <-cmp to <-fcmp )
7 open import Data.Nat 7 open import Data.Nat
8 open import Data.Nat.Properties
8 open import logic 9 open import logic
9 open import nat 10 open import nat
10 open import Relation.Binary.PropositionalEquality 11 open import Relation.Binary.PropositionalEquality
11 12
12 13
110 toℕ (fromℕ< (NatP.<-trans (toℕ<n x) n<m)) 111 toℕ (fromℕ< (NatP.<-trans (toℕ<n x) n<m))
111 ≡⟨ toℕ-fromℕ< _ ⟩ 112 ≡⟨ toℕ-fromℕ< _ ⟩
112 toℕ x 113 toℕ x
113 ∎ where 114 ∎ where
114 open ≡-Reasoning 115 open ≡-Reasoning
116
117 x<y→fin-1 : {n : ℕ } → { x y : Fin (suc n)} → toℕ x < toℕ y → Fin n
118 x<y→fin-1 {n} {x} {y} lt = fromℕ< (≤-trans lt (fin≤n _ ))
119
120 x<y→fin-1-eq : {n : ℕ } → { x y : Fin (suc n)} → (lt : toℕ x < toℕ y ) → toℕ x ≡ toℕ (x<y→fin-1 lt )
121 x<y→fin-1-eq {n} {x} {y} lt = sym ( begin
122 toℕ (fromℕ< (≤-trans lt (fin≤n y)) ) ≡⟨ toℕ-fromℕ< _ ⟩
123 toℕ x ∎ ) where open ≡-Reasoning
115 124
116 open import Data.List 125 open import Data.List
117 open import Relation.Binary.Definitions 126 open import Relation.Binary.Definitions
118 127
119 fin-phase2 : { n : ℕ } (q : Fin n) (qs : List (Fin n) ) → Bool 128 fin-phase2 : { n : ℕ } (q : Fin n) (qs : List (Fin n) ) → Bool
148 field 157 field
149 ls : List (Fin n) 158 ls : List (Fin n)
150 lseq : list-less qs ≡ ls 159 lseq : list-less qs ≡ ls
151 ls>n : m + length ls > n 160 ls>n : m + length ls > n
152 161
162
153 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 : {n : ℕ } → (qs : List (Fin n)) → (len> : length qs > n ) → FDup-in-list n qs
154 fin-dup-in-list>n {zero} [] () 164 fin-dup-in-list>n {zero} [] ()
155 fin-dup-in-list>n {zero} (() ∷ qs) lt 165 fin-dup-in-list>n {zero} (() ∷ qs) lt
156 fin-dup-in-list>n {suc n} qs lt = fdup-phase0 where 166 fin-dup-in-list>n {suc n} qs lt = fdup-phase0 where
167 open import Level using ( Level )
168 mapleneq : {n : Level} {a b : Set n} { x : List a } {f : a → b} → length (map f x) ≡ length x
169 mapleneq {_} {_} {_} {[]} {f} = refl
170 mapleneq {_} {_} {_} {x ∷ x₁} {f} = cong suc (mapleneq {_} {_} {_} {x₁})
171 lt-conv : {l : Level} {a : Set l} {m n : ℕ } ( qs : List a ) → m + suc ( length qs ) > n → suc m + length qs > n
172 lt-conv {_} {_} {m} {n} qs lt = begin
173 suc n ≤⟨ lt ⟩
174 m + suc (length qs) ≡⟨ sym (+-assoc m 1 _) ⟩
175 (m + 1) + length qs ≡⟨ cong (λ k → k + length qs) (+-comm m _ ) ⟩
176 suc m + length qs ∎ where open ≤-Reasoning
157 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 177 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
158 fdup+1 qs i p = f1-phase1 qs p where 178 fdup+1 qs i p = f1-phase1 qs p where
159 f1-phase2 : (qs : List (Fin (suc n)) ) → fin-phase2 i (list-less qs) ≡ true → fin-phase2 (fin+1 i) qs ≡ true 179 f1-phase2 : (qs : List (Fin (suc n)) ) → fin-phase2 i (list-less qs) ≡ true → fin-phase2 (fin+1 i) qs ≡ true
160 f1-phase2 (x ∷ qs) p with <-fcmp (fin+1 i) x 180 f1-phase2 (x ∷ qs) p with <-fcmp (fin+1 i) x
161 ... | tri< a ¬b ¬c = f1-phase2 qs {!!} -- fin-phase2 i (list-less (x ∷ qs)) ≡ true 181 ... | tri< a ¬b ¬c = f1-phase2 qs {!!} -- fin-phase2 i (list-less (x ∷ qs)) ≡ true → fin-phase2 i (list-less qs) ≡ true
162 ... | tri≈ ¬a b ¬c = refl 182 ... | tri≈ ¬a b ¬c = refl
163 ... | tri> ¬a ¬b c = f1-phase2 qs {!!} 183 ... | tri> ¬a ¬b c = f1-phase2 qs {!!}
164 f1-phase1 : (qs : List (Fin (suc n)) ) → fin-phase1 i (list-less qs) ≡ true → fin-phase1 (fin+1 i) qs ≡ true 184 f1-phase1 : (qs : List (Fin (suc n)) ) → fin-phase1 i (list-less qs) ≡ true → fin-phase1 (fin+1 i) qs ≡ true
165 f1-phase1 [] () 185 f1-phase1 [] ()
166 f1-phase1 (x ∷ qs) p with <-fcmp (fin+1 i) x 186 f1-phase1 (x ∷ qs) p with <-fcmp (fin+1 i) x
169 ... | tri> ¬a ¬b c = f1-phase1 qs {!!} 189 ... | tri> ¬a ¬b c = f1-phase1 qs {!!}
170 fdup-phase2 : (qs : List (Fin (suc n)) ) → {m : ℕ} → m + length qs > n 190 fdup-phase2 : (qs : List (Fin (suc n)) ) → {m : ℕ} → m + length qs > n
171 → ( fin-phase2 (fromℕ< a<sa ) qs ≡ true ) ∨ NList n m qs 191 → ( fin-phase2 (fromℕ< a<sa ) qs ≡ true ) ∨ NList n m qs
172 fdup-phase2 [] {m} lt = case2 record { ls = [] ; lseq = refl ; ls>n = lt } 192 fdup-phase2 [] {m} lt = case2 record { ls = [] ; lseq = refl ; ls>n = lt }
173 fdup-phase2 (x ∷ qs) {m} lt with <-fcmp (fromℕ< a<sa) x 193 fdup-phase2 (x ∷ qs) {m} lt with <-fcmp (fromℕ< a<sa) x
174 ... | tri< a ¬b ¬c = {!!} 194 ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a (subst (λ k → toℕ x < suc k) (sym fin<asa) fin<n ))
175 fdup-phase2 (x ∷ qs) {m} lt | tri≈ ¬a b ¬c = case1 refl 195 fdup-phase2 (x ∷ qs) {m} lt | tri≈ ¬a b ¬c = case1 refl
176 fdup-phase2 (x ∷ qs) {m} lt | tri> ¬a ¬b c with fdup-phase2 qs {suc m} {!!} 196 fdup-phase2 (x ∷ qs) {m} lt | tri> ¬a ¬b c with fdup-phase2 qs {suc m} (lt-conv qs lt)
177 ... | case1 p = case1 p 197 ... | case1 p = case1 p
178 ... | case2 nlist = case2 record { ls = {!!} ∷ NList.ls nlist ; lseq = {!!} ; ls>n = {!!} } 198 ... | case2 nlist = case2 record { ls = x<y→fin-1 c ∷ NList.ls nlist ; lseq = {!!} ; ls>n = {!!} }
179 fdup-phase1 : (qs : List (Fin (suc n)) ) → {m : ℕ} → m + length qs > n → (fin-phase1 (fromℕ< a<sa) qs ≡ true) ∨ NList n m qs 199 fdup-phase1 : (qs : List (Fin (suc n)) ) → {m : ℕ} → m + length qs > n → (fin-phase1 (fromℕ< a<sa) qs ≡ true) ∨ NList n m qs
180 fdup-phase1 [] {m} lt = case2 record { ls = [] ; lseq = refl ; ls>n = lt } 200 fdup-phase1 [] {m} lt = case2 record { ls = [] ; lseq = refl ; ls>n = lt }
181 fdup-phase1 (x ∷ qs) {m} lt with <-fcmp (fromℕ< a<sa) x 201 fdup-phase1 (x ∷ qs) {m} lt with <-fcmp (fromℕ< a<sa) x
182 fdup-phase1 (x ∷ qs) {m} lt | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a {!!} ) 202 fdup-phase1 (x ∷ qs) {m} lt | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a (subst (λ k → toℕ x < suc k) (sym fin<asa) fin<n ))
183 fdup-phase1 (x ∷ qs) {m} lt | tri≈ ¬a b ¬c with fdup-phase2 qs {m} {!!} 203 fdup-phase1 (x ∷ qs) {m} lt | tri≈ ¬a b ¬c with fdup-phase2 qs {m} ?
184 ... | case1 p = case1 p 204 ... | case1 p = case1 p
185 ... | case2 nlist = case2 record { ls = {!!} ∷ NList.ls nlist ; lseq = {!!} ; ls>n = {!!} } 205 ... | case2 nlist = case2 record { ls = NList.ls nlist ; lseq = {!!} ; ls>n = NList.ls>n nlist }
186 fdup-phase1 (x ∷ qs) {m} lt | tri> ¬a ¬b c with fdup-phase1 qs {m} {!!} 206 fdup-phase1 (x ∷ qs) {m} lt | tri> ¬a ¬b c with fdup-phase1 qs {m} {!!}
187 ... | case1 p = case1 p 207 ... | case1 p = case1 p
188 ... | case2 nlist = case2 record { ls = {!!} ∷ NList.ls nlist ; lseq = {!!} ; ls>n = {!!} } 208 ... | case2 nlist = case2 record { ls = x<y→fin-1 c ∷ NList.ls nlist ; lseq = {!!} ; ls>n = {!!} }
189 fdup-phase0 : FDup-in-list (suc n) qs 209 fdup-phase0 : FDup-in-list (suc n) qs
190 fdup-phase0 with fdup-phase1 qs {0} ( <-trans a<sa lt ) 210 fdup-phase0 with fdup-phase1 qs {0} ( <-trans a<sa lt )
191 ... | case1 dup = record { dup = fromℕ< a<sa ; is-dup = dup } 211 ... | case1 dup = record { dup = fromℕ< a<sa ; is-dup = dup }
192 ... | case2 nlist = record { dup = fin+1 (FDup-in-list.dup fdup) 212 ... | case2 nlist = record { dup = fin+1 (FDup-in-list.dup fdup)
193 ; is-dup = fdup+1 qs (FDup-in-list.dup fdup) (FDup-in-list.is-dup fdup) } where 213 ; is-dup = fdup+1 qs (FDup-in-list.dup fdup) (FDup-in-list.is-dup fdup) } where