Mercurial > hg > Members > kono > Proof > galois
annotate src/fin.agda @ 320:8fb16f9a882a
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 19 Sep 2023 11:11:38 +0900 |
parents | fff18d4a063b |
children | e9de2bfef88d |
rev | line source |
---|---|
318
fff18d4a063b
use stdlib-2.0 and safe-mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
1 {-# OPTIONS --cubical-compatible --safe #-} |
72 | 2 |
3 module fin where | |
4 | |
293 | 5 open import Data.Fin hiding (_<_ ; _≤_ ; _>_ ; _+_ ) |
6 open import Data.Fin.Properties hiding (≤-trans ; <-trans ; ≤-refl ) renaming ( <-cmp to <-fcmp ) | |
72 | 7 open import Data.Nat |
293 | 8 open import Data.Nat.Properties |
72 | 9 open import logic |
10 open import nat | |
11 open import Relation.Binary.PropositionalEquality | |
12 | |
13 | |
91 | 14 -- toℕ<n |
72 | 15 fin<n : {n : ℕ} {f : Fin n} → toℕ f < n |
16 fin<n {_} {zero} = s≤s z≤n | |
17 fin<n {suc n} {suc f} = s≤s (fin<n {n} {f}) | |
18 | |
91 | 19 -- toℕ≤n |
83 | 20 fin≤n : {n : ℕ} (f : Fin (suc n)) → toℕ f ≤ n |
21 fin≤n {_} zero = z≤n | |
22 fin≤n {suc n} (suc f) = s≤s (fin≤n {n} f) | |
23 | |
72 | 24 pred<n : {n : ℕ} {f : Fin (suc n)} → n > 0 → Data.Nat.pred (toℕ f) < n |
25 pred<n {suc n} {zero} (s≤s z≤n) = s≤s z≤n | |
26 pred<n {suc n} {suc f} (s≤s z≤n) = fin<n | |
27 | |
131 | 28 fin<asa : {n : ℕ} → toℕ (fromℕ< {n} a<sa) ≡ n |
29 fin<asa = toℕ-fromℕ< nat.a<sa | |
30 | |
91 | 31 -- fromℕ<-toℕ |
72 | 32 toℕ→from : {n : ℕ} {x : Fin (suc n)} → toℕ x ≡ n → fromℕ n ≡ x |
33 toℕ→from {0} {zero} refl = refl | |
34 toℕ→from {suc n} {suc x} eq = cong (λ k → suc k ) ( toℕ→from {n} {x} (cong (λ k → Data.Nat.pred k ) eq )) | |
35 | |
318
fff18d4a063b
use stdlib-2.0 and safe-mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
36 -- 0≤fmax : {n : ℕ } → (# 0) Data.Fin.≤ fromℕ< {n} a<sa |
fff18d4a063b
use stdlib-2.0 and safe-mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
37 -- 0≤fmax {n} = ? |
210 | 38 |
318
fff18d4a063b
use stdlib-2.0 and safe-mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
39 -- 0<fmax : {n : ℕ } → (# 0) Data.Fin.< fromℕ< {suc n} a<sa |
fff18d4a063b
use stdlib-2.0 and safe-mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
40 -- 0<fmax {n} = subst (λ k → 0 < k ) (sym (toℕ-fromℕ< {suc n} {suc (suc n)} a<sa)) (s≤s z≤n) |
210 | 41 |
91 | 42 -- toℕ-injective |
72 | 43 i=j : {n : ℕ} (i j : Fin n) → toℕ i ≡ toℕ j → i ≡ j |
44 i=j {suc n} zero zero refl = refl | |
45 i=j {suc n} (suc i) (suc j) eq = cong ( λ k → suc k ) ( i=j i j (cong ( λ k → Data.Nat.pred k ) eq) ) | |
46 | |
91 | 47 -- raise 1 |
72 | 48 fin+1 : { n : ℕ } → Fin n → Fin (suc n) |
49 fin+1 zero = zero | |
50 fin+1 (suc x) = suc (fin+1 x) | |
51 | |
52 open import Data.Nat.Properties as NatP hiding ( _≟_ ) | |
53 | |
74 | 54 fin+1≤ : { i n : ℕ } → (a : i < n) → fin+1 (fromℕ< a) ≡ fromℕ< (<-trans a a<sa) |
72 | 55 fin+1≤ {0} {suc i} (s≤s z≤n) = refl |
56 fin+1≤ {suc n} {suc (suc i)} (s≤s (s≤s a)) = cong (λ k → suc k ) ( fin+1≤ {n} {suc i} (s≤s a) ) | |
57 | |
58 fin+1-toℕ : { n : ℕ } → { x : Fin n} → toℕ (fin+1 x) ≡ toℕ x | |
59 fin+1-toℕ {suc n} {zero} = refl | |
60 fin+1-toℕ {suc n} {suc x} = cong (λ k → suc k ) (fin+1-toℕ {n} {x}) | |
61 | |
62 open import Relation.Nullary | |
63 open import Data.Empty | |
64 | |
65 fin-1 : { n : ℕ } → (x : Fin (suc n)) → ¬ (x ≡ zero ) → Fin n | |
66 fin-1 zero ne = ⊥-elim (ne refl ) | |
67 fin-1 {n} (suc x) ne = x | |
68 | |
69 fin-1-sx : { n : ℕ } → (x : Fin n) → fin-1 (suc x) (λ ()) ≡ x | |
70 fin-1-sx zero = refl | |
71 fin-1-sx (suc x) = refl | |
72 | |
73 fin-1-xs : { n : ℕ } → (x : Fin (suc n)) → (ne : ¬ (x ≡ zero )) → suc (fin-1 x ne ) ≡ x | |
74 fin-1-xs zero ne = ⊥-elim ( ne refl ) | |
75 fin-1-xs (suc x) ne = refl | |
76 | |
91 | 77 -- suc-injective |
72 | 78 -- suc-eq : {n : ℕ } {x y : Fin n} → Fin.suc x ≡ Fin.suc y → x ≡ y |
79 -- suc-eq {n} {x} {y} eq = subst₂ (λ j k → j ≡ k ) {!!} {!!} (cong (λ k → Data.Fin.pred k ) eq ) | |
80 | |
91 | 81 -- this is refl |
74 | 82 lemma3 : {a b : ℕ } → (lt : a < b ) → fromℕ< (s≤s lt) ≡ suc (fromℕ< lt) |
72 | 83 lemma3 (s≤s lt) = refl |
91 | 84 |
85 -- fromℕ<-toℕ | |
74 | 86 lemma12 : {n m : ℕ } → (n<m : n < m ) → (f : Fin m ) → toℕ f ≡ n → f ≡ fromℕ< n<m |
72 | 87 lemma12 {zero} {suc m} (s≤s z≤n) zero refl = refl |
91 | 88 lemma12 {suc n} {suc m} (s≤s n<m) (suc f) refl = cong suc ( lemma12 {n} {m} n<m f refl ) |
72 | 89 |
318
fff18d4a063b
use stdlib-2.0 and safe-mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
90 -- this requires K |
fff18d4a063b
use stdlib-2.0 and safe-mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
91 -- |
fff18d4a063b
use stdlib-2.0 and safe-mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
92 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) |
72 | 93 |
91 | 94 -- <-irrelevant |
318
fff18d4a063b
use stdlib-2.0 and safe-mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
95 -- <-nat=irr : {i j n : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n } → i<n ≅ j<n |
fff18d4a063b
use stdlib-2.0 and safe-mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
96 -- <-nat=irr {zero} {zero} {suc n} refl {s≤s z≤n} {s≤s z≤n} = HE.refl |
fff18d4a063b
use stdlib-2.0 and safe-mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
97 -- <-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 ) |
91 | 98 |
318
fff18d4a063b
use stdlib-2.0 and safe-mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
99 -- lemma8 : {i j n : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n } → i<n ≅ j<n |
fff18d4a063b
use stdlib-2.0 and safe-mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
100 -- lemma8 {zero} {zero} {suc n} refl {s≤s z≤n} {s≤s z≤n} = HE.refl |
fff18d4a063b
use stdlib-2.0 and safe-mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
101 -- lemma8 {suc i} {suc i} {suc n} refl {s≤s i<n} {s≤s j<n} = HE.cong (λ k → s≤s k ) ( lemma8 {i} {i} {n} refl ) |
91 | 102 |
103 -- fromℕ<-irrelevant | |
318
fff18d4a063b
use stdlib-2.0 and safe-mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
104 -- lemma10 : {n i j : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n } → fromℕ< i<n ≡ fromℕ< j<n |
fff18d4a063b
use stdlib-2.0 and safe-mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
105 -- lemma10 {n} refl = HE.≅-to-≡ (HE.cong (λ k → fromℕ< k ) (lemma8 refl )) |
91 | 106 |
320 | 107 lemma10 : {n i j : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n } → fromℕ< i<n ≡ fromℕ< j<n |
108 lemma10 {.(suc _)} {zero} {zero} refl {s≤s z≤n} {s≤s z≤n} = refl | |
109 lemma10 {suc n} {suc i} {suc i} refl {s≤s i<n} {s≤s j<n} = cong suc (lemma10 {n} {i} {i} refl {i<n} {j<n}) | |
110 | |
318
fff18d4a063b
use stdlib-2.0 and safe-mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
111 -- lemma31 : {a b c : ℕ } → { a<b : a < b } { b<c : b < c } { a<c : a < c } → NatP.<-trans a<b b<c ≡ a<c |
fff18d4a063b
use stdlib-2.0 and safe-mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
112 -- lemma31 {a} {b} {c} {a<b} {b<c} {a<c} = HE.≅-to-≡ (lemma8 refl) |
91 | 113 |
114 -- toℕ-fromℕ< | |
74 | 115 lemma11 : {n m : ℕ } {x : Fin n } → (n<m : n < m ) → toℕ (fromℕ< (NatP.<-trans (toℕ<n x) n<m)) ≡ toℕ x |
72 | 116 lemma11 {n} {m} {x} n<m = begin |
74 | 117 toℕ (fromℕ< (NatP.<-trans (toℕ<n x) n<m)) |
118 ≡⟨ toℕ-fromℕ< _ ⟩ | |
72 | 119 toℕ x |
120 ∎ where | |
121 open ≡-Reasoning | |
122 | |
293 | 123 x<y→fin-1 : {n : ℕ } → { x y : Fin (suc n)} → toℕ x < toℕ y → Fin n |
124 x<y→fin-1 {n} {x} {y} lt = fromℕ< (≤-trans lt (fin≤n _ )) | |
72 | 125 |
293 | 126 x<y→fin-1-eq : {n : ℕ } → { x y : Fin (suc n)} → (lt : toℕ x < toℕ y ) → toℕ x ≡ toℕ (x<y→fin-1 lt ) |
127 x<y→fin-1-eq {n} {x} {y} lt = sym ( begin | |
128 toℕ (fromℕ< (≤-trans lt (fin≤n y)) ) ≡⟨ toℕ-fromℕ< _ ⟩ | |
129 toℕ x ∎ ) where open ≡-Reasoning | |
130 | |
131 f<→< : {n : ℕ } → { x y : Fin n} → x Data.Fin.< y → toℕ x < toℕ y | |
132 f<→< {_} {zero} {suc y} (s≤s lt) = s≤s z≤n | |
133 f<→< {_} {suc x} {suc y} (s≤s lt) = s≤s (f<→< {_} {x} {y} lt) | |
134 | |
135 f≡→≡ : {n : ℕ } → { x y : Fin n} → x ≡ y → toℕ x ≡ toℕ y | |
136 f≡→≡ refl = refl | |
137 | |
138 open import Data.List | |
139 open import Relation.Binary.Definitions | |
140 | |
141 ----- | |
142 -- | |
143 -- find duplicate element in a List (Fin n) | |
144 -- | |
145 -- if the length is longer than n, we can find duplicate element as FDup-in-list | |
146 -- | |
147 -- How about do it in ℕ ? | |
148 | |
149 -- fin-count : { n : ℕ } (q : Fin n) (qs : List (Fin n) ) → ℕ | |
150 -- fin-count q p[ = 0 | |
151 -- fin-count q (q0 ∷ qs ) with <-fcmp q q0 | |
152 -- ... | tri-e = suc (fin-count q qs) | |
153 -- ... | false = fin-count q qs | |
154 | |
155 -- fin-not-dup-in-list : { n : ℕ} (qs : List (Fin n) ) → Set | |
156 -- fin-not-dup-in-list {n} qs = (q : Fin n) → fin-count q ≤ 1 | |
157 | |
158 -- this is far easier | |
159 -- 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 | |
160 -- fin-not-dup-in-list→len<n = ? | |
161 | |
162 fin-phase2 : { n : ℕ } (q : Fin n) (qs : List (Fin n) ) → Bool -- find the dup | |
163 fin-phase2 q [] = false | |
164 fin-phase2 q (x ∷ qs) with <-fcmp q x | |
165 ... | tri< a ¬b ¬c = fin-phase2 q qs | |
166 ... | tri≈ ¬a b ¬c = true | |
167 ... | tri> ¬a ¬b c = fin-phase2 q qs | |
168 fin-phase1 : { n : ℕ } (q : Fin n) (qs : List (Fin n) ) → Bool -- find the first element | |
169 fin-phase1 q [] = false | |
170 fin-phase1 q (x ∷ qs) with <-fcmp q x | |
171 ... | tri< a ¬b ¬c = fin-phase1 q qs | |
172 ... | tri≈ ¬a b ¬c = fin-phase2 q qs | |
173 ... | tri> ¬a ¬b c = fin-phase1 q qs | |
174 | |
175 fin-dup-in-list : { n : ℕ} (q : Fin n) (qs : List (Fin n) ) → Bool | |
176 fin-dup-in-list {n} q qs = fin-phase1 q qs | |
177 | |
178 record FDup-in-list (n : ℕ ) (qs : List (Fin n)) : Set where | |
179 field | |
180 dup : Fin n | |
181 is-dup : fin-dup-in-list dup qs ≡ true | |
182 | |
183 list-less : {n : ℕ } → List (Fin (suc n)) → List (Fin n) | |
184 list-less [] = [] | |
185 list-less {n} (i ∷ ls) with <-fcmp (fromℕ< a<sa) i | |
186 ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a (subst (λ k → toℕ i < suc k ) (sym fin<asa) (fin≤n _ ))) | |
187 ... | tri≈ ¬a b ¬c = list-less ls | |
188 ... | tri> ¬a ¬b c = x<y→fin-1 c ∷ list-less ls | |
189 | |
190 fin010 : {n m : ℕ } {x : Fin n} (c : suc (toℕ x) ≤ toℕ (fromℕ< {m} a<sa) ) → toℕ (fromℕ< (≤-trans c (fin≤n (fromℕ< a<sa)))) ≡ toℕ x | |
191 fin010 {_} {_} {x} c = begin | |
192 toℕ (fromℕ< (≤-trans c (fin≤n (fromℕ< a<sa)))) ≡⟨ toℕ-fromℕ< _ ⟩ | |
193 toℕ x ∎ where open ≡-Reasoning | |
194 | |
195 --- | |
196 --- if List (Fin n) is longer than n, there is at most one duplication | |
197 --- | |
198 fin-dup-in-list>n : {n : ℕ } → (qs : List (Fin n)) → (len> : length qs > n ) → FDup-in-list n qs | |
199 fin-dup-in-list>n {zero} [] () | |
200 fin-dup-in-list>n {zero} (() ∷ qs) lt | |
201 fin-dup-in-list>n {suc n} qs lt = fdup-phase0 where | |
202 open import Level using ( Level ) | |
203 -- make a dup from one level below | |
204 fdup+1 : (qs : List (Fin (suc n))) (i : Fin n) → fin-dup-in-list (fromℕ< a<sa ) qs ≡ false | |
205 → fin-dup-in-list i (list-less qs) ≡ true → FDup-in-list (suc n) qs | |
206 fdup+1 qs i ne p = record { dup = fin+1 i ; is-dup = f1-phase1 qs p (case1 ne) } where | |
207 -- we have two loops on the max element and the current level. The disjuction means the phases may differ. | |
208 f1-phase2 : (qs : List (Fin (suc n)) ) → fin-phase2 i (list-less qs) ≡ true | |
209 → (fin-phase1 (fromℕ< a<sa) qs ≡ false ) ∨ (fin-phase2 (fromℕ< a<sa) qs ≡ false) | |
210 → fin-phase2 (fin+1 i) qs ≡ true | |
211 f1-phase2 (x ∷ qs) p (case1 q1) with <-fcmp (fromℕ< a<sa) x | |
212 ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a (subst (λ k → toℕ x < suc k ) (sym fin<asa) (fin≤n _ ))) | |
213 f1-phase2 (x ∷ qs) p (case1 q1) | tri≈ ¬a b ¬c with <-fcmp (fin+1 i) x | |
214 ... | tri< a ¬b ¬c₁ = f1-phase2 qs p (case2 q1) | |
215 ... | tri≈ ¬a₁ b₁ ¬c₁ = refl | |
216 ... | tri> ¬a₁ ¬b c = f1-phase2 qs p (case2 q1) | |
217 -- two fcmp is only different in the size of Fin, but to develop both f1-phase and list-less both fcmps are required | |
218 f1-phase2 (x ∷ qs) p (case1 q1) | tri> ¬a ¬b c with <-fcmp i (fromℕ< (≤-trans c (fin≤n (fromℕ< a<sa)))) | <-fcmp (fin+1 i) x | |
219 ... | tri< a ¬b₁ ¬c | tri< a₁ ¬b₂ ¬c₁ = f1-phase2 qs p (case1 q1) | |
220 ... | tri< a ¬b₁ ¬c | tri≈ ¬a₁ b ¬c₁ = ⊥-elim ( ¬a₁ (subst₂ (λ j k → j < k) (sym fin+1-toℕ) (toℕ-fromℕ< _) a )) | |
221 ... | tri< a ¬b₁ ¬c | tri> ¬a₁ ¬b₂ c₁ = ⊥-elim ( ¬a₁ (subst₂ (λ j k → j < k) (sym fin+1-toℕ) (toℕ-fromℕ< _) a )) | |
222 ... | tri≈ ¬a₁ b ¬c | tri< a ¬b₁ ¬c₁ = ⊥-elim ( ¬a₁ (subst₂ (λ j k → j < k) fin+1-toℕ (sym (toℕ-fromℕ< _)) a )) | |
223 ... | tri≈ ¬a₁ b ¬c | tri≈ ¬a₂ b₁ ¬c₁ = refl | |
224 ... | tri≈ ¬a₁ b ¬c | tri> ¬a₂ ¬b₁ c₁ = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) fin+1-toℕ (sym (toℕ-fromℕ< _)) c₁ )) | |
225 ... | tri> ¬a₁ ¬b₁ c₁ | tri< a ¬b₂ ¬c = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) (sym fin+1-toℕ) (toℕ-fromℕ< _) c₁ )) | |
226 ... | tri> ¬a₁ ¬b₁ c₁ | tri≈ ¬a₂ b ¬c = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) (sym fin+1-toℕ) (toℕ-fromℕ< _) c₁ )) | |
227 ... | tri> ¬a₁ ¬b₁ c₁ | tri> ¬a₂ ¬b₂ c₂ = f1-phase2 qs p (case1 q1) | |
228 f1-phase2 (x ∷ qs) p (case2 q1) with <-fcmp (fromℕ< a<sa) x | |
229 ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a (subst (λ k → toℕ x < suc k ) (sym fin<asa) (fin≤n _ ))) | |
230 f1-phase2 (x ∷ qs) p (case2 q1) | tri≈ ¬a b ¬c with <-fcmp (fin+1 i) x | |
231 ... | tri< a ¬b ¬c₁ = ⊥-elim ( ¬-bool q1 refl ) | |
232 ... | tri≈ ¬a₁ b₁ ¬c₁ = refl | |
233 ... | tri> ¬a₁ ¬b c = ⊥-elim ( ¬-bool q1 refl ) | |
234 f1-phase2 (x ∷ qs) p (case2 q1) | tri> ¬a ¬b c with <-fcmp i (fromℕ< (≤-trans c (fin≤n (fromℕ< a<sa)))) | <-fcmp (fin+1 i) x | |
235 ... | tri< a ¬b₁ ¬c | tri< a₁ ¬b₂ ¬c₁ = f1-phase2 qs p (case2 q1) | |
236 ... | tri< a ¬b₁ ¬c | tri≈ ¬a₁ b ¬c₁ = ⊥-elim ( ¬a₁ (subst₂ (λ j k → j < k) (sym fin+1-toℕ) (toℕ-fromℕ< _) a )) | |
237 ... | tri< a ¬b₁ ¬c | tri> ¬a₁ ¬b₂ c₁ = ⊥-elim ( ¬a₁ (subst₂ (λ j k → j < k) (sym fin+1-toℕ) (toℕ-fromℕ< _) a )) | |
238 ... | tri≈ ¬a₁ b ¬c | tri< a ¬b₁ ¬c₁ = ⊥-elim ( ¬a₁ (subst₂ (λ j k → j < k) fin+1-toℕ (sym (toℕ-fromℕ< _)) a )) | |
239 ... | tri≈ ¬a₁ b ¬c | tri≈ ¬a₂ b₁ ¬c₁ = refl | |
240 ... | tri≈ ¬a₁ b ¬c | tri> ¬a₂ ¬b₁ c₁ = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) fin+1-toℕ (sym (toℕ-fromℕ< _)) c₁ )) | |
241 ... | tri> ¬a₁ ¬b₁ c₁ | tri< a ¬b₂ ¬c = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) (sym fin+1-toℕ) (toℕ-fromℕ< _) c₁ )) | |
242 ... | tri> ¬a₁ ¬b₁ c₁ | tri≈ ¬a₂ b ¬c = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) (sym fin+1-toℕ) (toℕ-fromℕ< _) c₁ )) | |
243 ... | tri> ¬a₁ ¬b₁ c₁ | tri> ¬a₂ ¬b₂ c₂ = f1-phase2 qs p (case2 q1 ) | |
244 f1-phase1 : (qs : List (Fin (suc n)) ) → fin-phase1 i (list-less qs) ≡ true | |
245 → (fin-phase1 (fromℕ< a<sa) qs ≡ false ) ∨ (fin-phase2 (fromℕ< a<sa) qs ≡ false) | |
246 → fin-phase1 (fin+1 i) qs ≡ true | |
247 f1-phase1 (x ∷ qs) p (case1 q1) with <-fcmp (fromℕ< a<sa) x | |
248 ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a (subst (λ k → toℕ x < suc k ) (sym fin<asa) (fin≤n _ ))) | |
249 f1-phase1 (x ∷ qs) p (case1 q1) | tri≈ ¬a b ¬c with <-fcmp (fin+1 i) x | |
250 ... | tri< a ¬b ¬c₁ = f1-phase1 qs p (case2 q1) | |
251 ... | tri≈ ¬a₁ b₁ ¬c₁ = ⊥-elim (fdup-10 b b₁) where | |
252 fdup-10 : fromℕ< a<sa ≡ x → fin+1 i ≡ x → ⊥ | |
253 fdup-10 eq eq1 = nat-≡< (cong toℕ (trans eq1 (sym eq))) (subst₂ (λ j k → j < k ) (sym fin+1-toℕ) (sym fin<asa) fin<n ) | |
254 ... | tri> ¬a₁ ¬b c = f1-phase1 qs p (case2 q1) | |
255 f1-phase1 (x ∷ qs) p (case1 q1) | tri> ¬a ¬b c with <-fcmp i (fromℕ< (≤-trans c (fin≤n (fromℕ< a<sa)))) | <-fcmp (fin+1 i) x | |
256 ... | tri< a ¬b₁ ¬c | tri< a₁ ¬b₂ ¬c₁ = f1-phase1 qs p (case1 q1) | |
257 ... | tri< a ¬b₁ ¬c | tri≈ ¬a₁ b ¬c₁ = ⊥-elim ( ¬a₁ (subst₂ (λ j k → j < k) (sym fin+1-toℕ) (toℕ-fromℕ< _) a )) | |
258 ... | tri< a ¬b₁ ¬c | tri> ¬a₁ ¬b₂ c₁ = ⊥-elim ( ¬a₁ (subst₂ (λ j k → j < k) (sym fin+1-toℕ) (toℕ-fromℕ< _) a )) | |
259 ... | tri≈ ¬a₁ b ¬c | tri< a ¬b₁ ¬c₁ = ⊥-elim ( ¬a₁ (subst₂ (λ j k → j < k) fin+1-toℕ (sym (toℕ-fromℕ< _)) a )) | |
260 ... | tri≈ ¬a₁ b ¬c | tri≈ ¬a₂ b₁ ¬c₁ = f1-phase2 qs p (case1 q1) | |
261 ... | tri≈ ¬a₁ b ¬c | tri> ¬a₂ ¬b₁ c₁ = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) fin+1-toℕ (sym (toℕ-fromℕ< _)) c₁ )) | |
262 ... | tri> ¬a₁ ¬b₁ c₁ | tri< a ¬b₂ ¬c = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) (sym fin+1-toℕ) (toℕ-fromℕ< _) c₁ )) | |
263 ... | tri> ¬a₁ ¬b₁ c₁ | tri≈ ¬a₂ b ¬c = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) (sym fin+1-toℕ) (toℕ-fromℕ< _) c₁ )) | |
264 ... | tri> ¬a₁ ¬b₁ c₁ | tri> ¬a₂ ¬b₂ c₂ = f1-phase1 qs p (case1 q1) | |
265 f1-phase1 (x ∷ qs) p (case2 q1) with <-fcmp (fromℕ< a<sa) x | |
266 ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a (subst (λ k → toℕ x < suc k ) (sym fin<asa) (fin≤n _ ))) | |
267 f1-phase1 (x ∷ qs) p (case2 q1) | tri≈ ¬a b ¬c = ⊥-elim ( ¬-bool q1 refl ) | |
268 f1-phase1 (x ∷ qs) p (case2 q1) | tri> ¬a ¬b c with <-fcmp i (fromℕ< (≤-trans c (fin≤n (fromℕ< a<sa)))) | <-fcmp (fin+1 i) x | |
269 ... | tri< a ¬b₁ ¬c | tri< a₁ ¬b₂ ¬c₁ = f1-phase1 qs p (case2 q1) | |
270 ... | tri< a ¬b₁ ¬c | tri≈ ¬a₁ b ¬c₁ = ⊥-elim ( ¬a₁ (subst₂ (λ j k → j < k) (sym fin+1-toℕ) (toℕ-fromℕ< _) a )) | |
271 ... | tri< a ¬b₁ ¬c | tri> ¬a₁ ¬b₂ c₁ = ⊥-elim ( ¬a₁ (subst₂ (λ j k → j < k) (sym fin+1-toℕ) (toℕ-fromℕ< _) a )) | |
272 ... | tri≈ ¬a₁ b ¬c | tri< a ¬b₁ ¬c₁ = ⊥-elim ( ¬a₁ (subst₂ (λ j k → j < k) fin+1-toℕ (sym (toℕ-fromℕ< _)) a )) | |
273 ... | tri≈ ¬a₁ b ¬c | tri≈ ¬a₂ b₁ ¬c₁ = f1-phase2 qs p (case2 q1) | |
274 ... | tri≈ ¬a₁ b ¬c | tri> ¬a₂ ¬b₁ c₁ = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) fin+1-toℕ (sym (toℕ-fromℕ< _)) c₁ )) | |
275 ... | tri> ¬a₁ ¬b₁ c₁ | tri< a ¬b₂ ¬c = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) (sym fin+1-toℕ) (toℕ-fromℕ< _) c₁ )) | |
276 ... | tri> ¬a₁ ¬b₁ c₁ | tri≈ ¬a₂ b ¬c = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) (sym fin+1-toℕ) (toℕ-fromℕ< _) c₁ )) | |
277 ... | tri> ¬a₁ ¬b₁ c₁ | tri> ¬a₂ ¬b₂ c₂ = f1-phase1 qs p (case2 q1) | |
278 fdup-phase0 : FDup-in-list (suc n) qs | |
318
fff18d4a063b
use stdlib-2.0 and safe-mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
279 fdup-phase0 with fin-dup-in-list (fromℕ< a<sa) qs in eq |
fff18d4a063b
use stdlib-2.0 and safe-mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
280 ... | true = record { dup = fromℕ< a<sa ; is-dup = eq } |
fff18d4a063b
use stdlib-2.0 and safe-mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
281 ... | false = fdup+1 qs (FDup-in-list.dup fdup) eq (FDup-in-list.is-dup fdup) where |
293 | 282 -- if no dup in the max element, the list without the element is only one length shorter |
283 fless : (qs : List (Fin (suc n))) → length qs > suc n → fin-dup-in-list (fromℕ< a<sa) qs ≡ false → n < length (list-less qs) | |
284 fless qs lt p = fl-phase1 n qs lt p where | |
285 fl-phase2 : (n1 : ℕ) (qs : List (Fin (suc n))) → length qs > n1 → fin-phase2 (fromℕ< a<sa) qs ≡ false → n1 < length (list-less qs) | |
286 fl-phase2 zero (x ∷ qs) (s≤s lt) p with <-fcmp (fromℕ< a<sa) x | |
287 ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a (subst (λ k → toℕ x < suc k ) (sym fin<asa) (fin≤n _ ))) | |
288 ... | tri> ¬a ¬b c = s≤s z≤n | |
289 fl-phase2 (suc n1) (x ∷ qs) (s≤s lt) p with <-fcmp (fromℕ< a<sa) x | |
290 ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a (subst (λ k → toℕ x < suc k ) (sym fin<asa) (fin≤n _ ))) | |
291 ... | tri> ¬a ¬b c = s≤s ( fl-phase2 n1 qs lt p ) | |
292 fl-phase1 : (n1 : ℕ) (qs : List (Fin (suc n))) → length qs > suc n1 → fin-phase1 (fromℕ< a<sa) qs ≡ false → n1 < length (list-less qs) | |
293 fl-phase1 zero (x ∷ qs) (s≤s lt) p with <-fcmp (fromℕ< a<sa) x | |
294 ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a (subst (λ k → toℕ x < suc k ) (sym fin<asa) (fin≤n _ ))) | |
295 ... | tri≈ ¬a b ¬c = fl-phase2 0 qs lt p | |
296 ... | tri> ¬a ¬b c = s≤s z≤n | |
297 fl-phase1 (suc n1) (x ∷ qs) (s≤s lt) p with <-fcmp (fromℕ< a<sa) x | |
298 ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a (subst (λ k → toℕ x < suc k ) (sym fin<asa) (fin≤n _ ))) | |
299 ... | tri≈ ¬a b ¬c = fl-phase2 (suc n1) qs lt p | |
300 ... | tri> ¬a ¬b c = s≤s ( fl-phase1 n1 qs lt p ) | |
301 -- if the list without the max element is only one length shorter, we can recurse | |
302 fdup : FDup-in-list n (list-less qs) | |
318
fff18d4a063b
use stdlib-2.0 and safe-mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
303 fdup = fin-dup-in-list>n (list-less qs) (fless qs lt eq) |
293 | 304 |
305 -- |