Mercurial > hg > Members > kono > Proof > automaton

comparison automaton-in-agda/src/fin.agda @ 283:e5a0499e7b40

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 19:48:00 +0900
parents 8006cbd87b20
children c9f20dec63ad
comparison
equal deleted inserted replaced
282:80276659bb18 283:e5a0499e7b40
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 ) 6 open import Data.Fin.Properties hiding ( <-trans ; ≤-refl ) renaming ( <-cmp to <-fcmp )
7 open import Data.Nat 7 open import Data.Nat
8 open import logic 8 open import logic
9 open import nat 9 open import nat
10 open import Relation.Binary.PropositionalEquality 10 open import Relation.Binary.PropositionalEquality
11 11
85 lemma12 : {n m : ℕ } → (n<m : n < m ) → (f : Fin m ) → toℕ f ≡ n → f ≡ fromℕ< n<m 85 lemma12 : {n m : ℕ } → (n<m : n < m ) → (f : Fin m ) → toℕ f ≡ n → f ≡ fromℕ< n<m
86 lemma12 {zero} {suc m} (s≤s z≤n) zero refl = refl 86 lemma12 {zero} {suc m} (s≤s z≤n) zero refl = refl
87 lemma12 {suc n} {suc m} (s≤s n<m) (suc f) refl = cong suc ( lemma12 {n} {m} n<m f refl ) 87 lemma12 {suc n} {suc m} (s≤s n<m) (suc f) refl = cong suc ( lemma12 {n} {m} n<m f refl )
88 88
89 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 89 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
90 open import Data.Fin.Properties
91 90
92 -- <-irrelevant 91 -- <-irrelevant
93 <-nat=irr : {i j n : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n } → i<n ≅ j<n 92 <-nat=irr : {i j n : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n } → i<n ≅ j<n
94 <-nat=irr {zero} {zero} {suc n} refl {s≤s z≤n} {s≤s z≤n} = HE.refl 93 <-nat=irr {zero} {zero} {suc n} refl {s≤s z≤n} {s≤s z≤n} = HE.refl
95 <-nat=irr {suc i} {suc i} {suc n} refl {s≤s i<n} {s≤s j<n} = HE.cong (λ k → s≤s k ) ( <-nat=irr {i} {i} {n} refl ) 94 <-nat=irr {suc i} {suc i} {suc n} refl {s≤s i<n} {s≤s j<n} = HE.cong (λ k → s≤s k ) ( <-nat=irr {i} {i} {n} refl )
112 ≡⟨ toℕ-fromℕ< _ ⟩ 111 ≡⟨ toℕ-fromℕ< _ ⟩
113 toℕ x 112 toℕ x
114 ∎ where 113 ∎ where
115 open ≡-Reasoning 114 open ≡-Reasoning
116 115
116 open import Data.List
117 open import Relation.Binary.Definitions
118
119 fin-phase2 : { n : ℕ } (q : Fin n) (qs : List (Fin n) ) → Bool
120 fin-phase2 q [] = false
121 fin-phase2 q (x ∷ qs) with <-fcmp q x
122 ... | tri< a ¬b ¬c = fin-phase2 q qs
123 ... | tri≈ ¬a b ¬c = true
124 ... | tri> ¬a ¬b c = fin-phase2 q qs
125 fin-phase1 : { n : ℕ } (q : Fin n) (qs : List (Fin n) ) → Bool
126 fin-phase1 q [] = false
127 fin-phase1 q (x ∷ qs) with <-fcmp q x
128 ... | tri< a ¬b ¬c = fin-phase1 q qs
129 ... | tri≈ ¬a b ¬c = fin-phase2 q qs
130 ... | tri> ¬a ¬b c = fin-phase1 q qs
131
132 fin-dup-in-list : { n : ℕ} (q : Fin n) (qs : List (Fin n) ) → Bool
133 fin-dup-in-list {n} q qs = fin-phase1 q qs
134
135 record FDup-in-list (n : ℕ ) (qs : List (Fin n)) : Set where
136 field
137 dup : Fin n
138 is-dup : fin-dup-in-list dup qs ≡ true
139
140 list-less : {n : ℕ } → List (Fin (suc n)) → List (Fin n)
141 list-less [] = []
142 list-less {n} (i ∷ ls) with NatP.<-cmp (toℕ i) n
143 ... | tri< a ¬b ¬c = fromℕ< a ∷ list-less ls
144 ... | tri≈ ¬a b ¬c = list-less ls
145 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> (fin≤n i) c )
146
147 record NList (n m : ℕ) (qs : List (Fin (suc n))) : Set where
148 field
149 ls : List (Fin n)
150 lseq : list-less qs ≡ ls
151 ls>n : m + length ls > n
152
153 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} [] ()
155 fin-dup-in-list>n {zero} (() ∷ qs) lt
156 fin-dup-in-list>n {suc n} qs lt = fdup-phase0 where
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
158 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
160 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
162 ... | tri≈ ¬a b ¬c = refl
163 ... | 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
165 f1-phase1 [] ()
166 f1-phase1 (x ∷ qs) p with <-fcmp (fin+1 i) x
167 ... | tri< a ¬b ¬c = f1-phase1 qs {!!}
168 ... | tri≈ ¬a b ¬c = f1-phase2 qs {!!}
169 ... | tri> ¬a ¬b c = f1-phase1 qs {!!}
170 fdup-phase2 : (qs : List (Fin (suc n)) ) → {m : ℕ} → m + length qs > n
171 → ( fin-phase2 (fromℕ< a<sa ) qs ≡ true ) ∨ NList n m qs
172 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
174 ... | tri< a ¬b ¬c = {!!}
175 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} {!!}
177 ... | case1 p = case1 p
178 ... | case2 nlist = case2 record { ls = {!!} ∷ 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
180 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
182 fdup-phase1 (x ∷ qs) {m} lt | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a {!!} )
183 fdup-phase1 (x ∷ qs) {m} lt | tri≈ ¬a b ¬c with fdup-phase2 qs {m} {!!}
184 ... | case1 p = case1 p
185 ... | case2 nlist = case2 record { ls = {!!} ∷ NList.ls nlist ; lseq = {!!} ; ls>n = {!!} }
186 fdup-phase1 (x ∷ qs) {m} lt | tri> ¬a ¬b c with fdup-phase1 qs {m} {!!}
187 ... | case1 p = case1 p
188 ... | case2 nlist = case2 record { ls = {!!} ∷ NList.ls nlist ; lseq = {!!} ; ls>n = {!!} }
189 fdup-phase0 : FDup-in-list (suc n) qs
190 fdup-phase0 with fdup-phase1 qs {0} ( <-trans a<sa lt )
191 ... | case1 dup = record { dup = fromℕ< a<sa ; is-dup = dup }
192 ... | 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
194 flt : length (list-less qs) > n
195 flt = subst ( λ k → length k > n ) (sym (NList.lseq nlist)) ( NList.ls>n nlist )
196 fdup : FDup-in-list n (list-less qs)
197 fdup = fin-dup-in-list>n (list-less qs) flt