|
163
|
1 {-# OPTIONS --allow-unsolved-metas #-}
|
|
|
2
|
|
|
3 module fin where
|
|
|
4
|
|
283
|
5 open import Data.Fin hiding (_<_ ; _≤_ ; _>_ ; _+_ )
|
|
284
|
6 open import Data.Fin.Properties hiding (≤-trans ; <-trans ; ≤-refl ) renaming ( <-cmp to <-fcmp )
|
|
163
|
7 open import Data.Nat
|
|
284
|
8 open import Data.Nat.Properties
|
|
163
|
9 open import logic
|
|
|
10 open import nat
|
|
|
11 open import Relation.Binary.PropositionalEquality
|
|
|
12
|
|
|
13
|
|
|
14 -- toℕ<n
|
|
|
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
|
|
|
19 -- toℕ≤n
|
|
|
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
|
|
|
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
|
|
|
28 fin<asa : {n : ℕ} → toℕ (fromℕ< {n} a<sa) ≡ n
|
|
|
29 fin<asa = toℕ-fromℕ< nat.a<sa
|
|
|
30
|
|
|
31 -- fromℕ<-toℕ
|
|
|
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
|
|
|
36 0≤fmax : {n : ℕ } → (# 0) Data.Fin.≤ fromℕ< {n} a<sa
|
|
|
37 0≤fmax = subst (λ k → 0 ≤ k ) (sym (toℕ-fromℕ< a<sa)) z≤n
|
|
|
38
|
|
|
39 0<fmax : {n : ℕ } → (# 0) Data.Fin.< fromℕ< {suc n} a<sa
|
|
|
40 0<fmax = subst (λ k → 0 < k ) (sym (toℕ-fromℕ< a<sa)) (s≤s z≤n)
|
|
|
41
|
|
|
42 -- toℕ-injective
|
|
|
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
|
|
|
47 -- raise 1
|
|
|
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
|
|
|
54 fin+1≤ : { i n : ℕ } → (a : i < n) → fin+1 (fromℕ< a) ≡ fromℕ< (<-trans a a<sa)
|
|
|
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
|
|
|
77 -- suc-injective
|
|
|
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
|
|
|
81 -- this is refl
|
|
|
82 lemma3 : {a b : ℕ } → (lt : a < b ) → fromℕ< (s≤s lt) ≡ suc (fromℕ< lt)
|
|
|
83 lemma3 (s≤s lt) = refl
|
|
|
84
|
|
|
85 -- fromℕ<-toℕ
|
|
|
86 lemma12 : {n m : ℕ } → (n<m : n < m ) → (f : Fin m ) → toℕ f ≡ n → f ≡ fromℕ< n<m
|
|
|
87 lemma12 {zero} {suc m} (s≤s z≤n) zero refl = refl
|
|
|
88 lemma12 {suc n} {suc m} (s≤s n<m) (suc f) refl = cong suc ( lemma12 {n} {m} n<m f refl )
|
|
|
89
|
|
|
90 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
|
|
|
91
|
|
|
92 -- <-irrelevant
|
|
|
93 <-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
|
|
|
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 )
|
|
|
96
|
|
|
97 lemma8 : {i j n : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n } → i<n ≅ j<n
|
|
|
98 lemma8 {zero} {zero} {suc n} refl {s≤s z≤n} {s≤s z≤n} = HE.refl
|
|
|
99 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 )
|
|
|
100
|
|
|
101 -- fromℕ<-irrelevant
|
|
|
102 lemma10 : {n i j : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n } → fromℕ< i<n ≡ fromℕ< j<n
|
|
|
103 lemma10 {n} refl = HE.≅-to-≡ (HE.cong (λ k → fromℕ< k ) (lemma8 refl ))
|
|
|
104
|
|
|
105 lemma31 : {a b c : ℕ } → { a<b : a < b } { b<c : b < c } { a<c : a < c } → NatP.<-trans a<b b<c ≡ a<c
|
|
|
106 lemma31 {a} {b} {c} {a<b} {b<c} {a<c} = HE.≅-to-≡ (lemma8 refl)
|
|
|
107
|
|
|
108 -- toℕ-fromℕ<
|
|
|
109 lemma11 : {n m : ℕ } {x : Fin n } → (n<m : n < m ) → toℕ (fromℕ< (NatP.<-trans (toℕ<n x) n<m)) ≡ toℕ x
|
|
|
110 lemma11 {n} {m} {x} n<m = begin
|
|
|
111 toℕ (fromℕ< (NatP.<-trans (toℕ<n x) n<m))
|
|
|
112 ≡⟨ toℕ-fromℕ< _ ⟩
|
|
|
113 toℕ x
|
|
|
114 ∎ where
|
|
|
115 open ≡-Reasoning
|
|
|
116
|
|
284
|
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
|
|
|
124
|
|
289
|
125 f<→< : {n : ℕ } → { x y : Fin n} → x Data.Fin.< y → toℕ x < toℕ y
|
|
|
126 f<→< {_} {zero} {suc y} (s≤s lt) = s≤s z≤n
|
|
|
127 f<→< {_} {suc x} {suc y} (s≤s lt) = s≤s (f<→< {_} {x} {y} lt)
|
|
|
128
|
|
|
129 f≡→≡ : {n : ℕ } → { x y : Fin n} → x ≡ y → toℕ x ≡ toℕ y
|
|
|
130 f≡→≡ refl = refl
|
|
|
131
|
|
283
|
132 open import Data.List
|
|
|
133 open import Relation.Binary.Definitions
|
|
|
134
|
|
|
135 fin-phase2 : { n : ℕ } (q : Fin n) (qs : List (Fin n) ) → Bool
|
|
|
136 fin-phase2 q [] = false
|
|
|
137 fin-phase2 q (x ∷ qs) with <-fcmp q x
|
|
|
138 ... | tri< a ¬b ¬c = fin-phase2 q qs
|
|
|
139 ... | tri≈ ¬a b ¬c = true
|
|
|
140 ... | tri> ¬a ¬b c = fin-phase2 q qs
|
|
|
141 fin-phase1 : { n : ℕ } (q : Fin n) (qs : List (Fin n) ) → Bool
|
|
|
142 fin-phase1 q [] = false
|
|
|
143 fin-phase1 q (x ∷ qs) with <-fcmp q x
|
|
|
144 ... | tri< a ¬b ¬c = fin-phase1 q qs
|
|
|
145 ... | tri≈ ¬a b ¬c = fin-phase2 q qs
|
|
|
146 ... | tri> ¬a ¬b c = fin-phase1 q qs
|
|
|
147
|
|
|
148 fin-dup-in-list : { n : ℕ} (q : Fin n) (qs : List (Fin n) ) → Bool
|
|
|
149 fin-dup-in-list {n} q qs = fin-phase1 q qs
|
|
|
150
|
|
|
151 record FDup-in-list (n : ℕ ) (qs : List (Fin n)) : Set where
|
|
|
152 field
|
|
|
153 dup : Fin n
|
|
|
154 is-dup : fin-dup-in-list dup qs ≡ true
|
|
|
155
|
|
|
156 list-less : {n : ℕ } → List (Fin (suc n)) → List (Fin n)
|
|
|
157 list-less [] = []
|
|
288
|
158 list-less {n} (i ∷ ls) with <-fcmp (fromℕ< a<sa) i
|
|
|
159 ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a (subst (λ k → toℕ i < suc k ) (sym fin<asa) (fin≤n _ )))
|
|
283
|
160 ... | tri≈ ¬a b ¬c = list-less ls
|
|
288
|
161 ... | tri> ¬a ¬b c = x<y→fin-1 c ∷ list-less ls
|
|
283
|
162
|
|
285
|
163 record NList (n : ℕ) (qs : List (Fin (suc n))) : Set where
|
|
283
|
164 field
|
|
|
165 ls : List (Fin n)
|
|
|
166 lseq : list-less qs ≡ ls
|
|
286
|
167 ls< : (length ls ≡ length qs) ∨ (suc (length ls) ≡ length qs)
|
|
284
|
168
|
|
289
|
169 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
|
|
|
170 fin010 {_} {_} {x} c = begin
|
|
|
171 toℕ (fromℕ< (≤-trans c (fin≤n (fromℕ< a<sa)))) ≡⟨ toℕ-fromℕ< _ ⟩
|
|
|
172 toℕ x ∎ where open ≡-Reasoning
|
|
|
173
|
|
283
|
174 fin-dup-in-list>n : {n : ℕ } → (qs : List (Fin n)) → (len> : length qs > n ) → FDup-in-list n qs
|
|
|
175 fin-dup-in-list>n {zero} [] ()
|
|
|
176 fin-dup-in-list>n {zero} (() ∷ qs) lt
|
|
|
177 fin-dup-in-list>n {suc n} qs lt = fdup-phase0 where
|
|
284
|
178 open import Level using ( Level )
|
|
287
|
179 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
|
|
|
180 fdup+1 qs i p with fin-dup-in-list (fromℕ< a<sa ) qs | inspect (fin-dup-in-list (fromℕ< a<sa )) qs
|
|
|
181 ... | true | record {eq = eq } = record { dup = fromℕ< a<sa ; is-dup = eq }
|
|
288
|
182 ... | false | record {eq = ne } = record { dup = fin+1 i ; is-dup = f1-phase1 qs p (case1 ne) } where
|
|
|
183 f1-phase2 : (qs : List (Fin (suc n)) ) → fin-phase2 i (list-less qs) ≡ true
|
|
|
184 → (fin-phase1 (fromℕ< a<sa) qs ≡ false ) ∨ (fin-phase2 (fromℕ< a<sa) qs ≡ false)
|
|
|
185 → fin-phase2 (fin+1 i) qs ≡ true
|
|
|
186 f1-phase2 (x ∷ qs) p (case1 q1) with <-fcmp (fromℕ< a<sa) x
|
|
|
187 ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a (subst (λ k → toℕ x < suc k ) (sym fin<asa) (fin≤n _ )))
|
|
289
|
188 f1-phase2 (x ∷ qs) p (case1 q1) | tri≈ ¬a b ¬c with <-fcmp (fin+1 i) x
|
|
|
189 ... | tri< a ¬b ¬c₁ = f1-phase2 qs p (case2 q1)
|
|
|
190 ... | tri≈ ¬a₁ b₁ ¬c₁ = refl
|
|
|
191 ... | tri> ¬a₁ ¬b c = f1-phase2 qs p (case2 q1)
|
|
288
|
192 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
|
|
|
193 ... | tri< a ¬b₁ ¬c | tri< a₁ ¬b₂ ¬c₁ = f1-phase2 qs p (case1 q1)
|
|
289
|
194 ... | tri< a ¬b₁ ¬c | tri≈ ¬a₁ b ¬c₁ = ⊥-elim ( ¬a₁ (subst₂ (λ j k → j < k) (sym fin+1-toℕ) (toℕ-fromℕ< _) a ))
|
|
|
195 ... | tri< a ¬b₁ ¬c | tri> ¬a₁ ¬b₂ c₁ = ⊥-elim ( ¬a₁ (subst₂ (λ j k → j < k) (sym fin+1-toℕ) (toℕ-fromℕ< _) a ))
|
|
|
196 ... | tri≈ ¬a₁ b ¬c | tri< a ¬b₁ ¬c₁ = ⊥-elim ( ¬a₁ (subst₂ (λ j k → j < k) fin+1-toℕ (sym (toℕ-fromℕ< _)) a ))
|
|
288
|
197 ... | tri≈ ¬a₁ b ¬c | tri≈ ¬a₂ b₁ ¬c₁ = refl
|
|
289
|
198 ... | tri≈ ¬a₁ b ¬c | tri> ¬a₂ ¬b₁ c₁ = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) fin+1-toℕ (sym (toℕ-fromℕ< _)) c₁ ))
|
|
|
199 ... | tri> ¬a₁ ¬b₁ c₁ | tri< a ¬b₂ ¬c = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) (sym fin+1-toℕ) (toℕ-fromℕ< _) c₁ ))
|
|
|
200 ... | tri> ¬a₁ ¬b₁ c₁ | tri≈ ¬a₂ b ¬c = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) (sym fin+1-toℕ) (toℕ-fromℕ< _) c₁ ))
|
|
288
|
201 ... | tri> ¬a₁ ¬b₁ c₁ | tri> ¬a₂ ¬b₂ c₂ = f1-phase2 qs p (case1 q1)
|
|
289
|
202 f1-phase2 (x ∷ qs) p (case2 q1) with <-fcmp (fromℕ< a<sa) x
|
|
|
203 ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a (subst (λ k → toℕ x < suc k ) (sym fin<asa) (fin≤n _ )))
|
|
|
204 f1-phase2 (x ∷ qs) p (case2 q1) | tri≈ ¬a b ¬c with <-fcmp (fin+1 i) x
|
|
|
205 ... | tri< a ¬b ¬c₁ = ⊥-elim ( ¬-bool q1 refl )
|
|
|
206 ... | tri≈ ¬a₁ b₁ ¬c₁ = refl
|
|
|
207 ... | tri> ¬a₁ ¬b c = ⊥-elim ( ¬-bool q1 refl )
|
|
|
208 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
|
|
|
209 ... | tri< a ¬b₁ ¬c | tri< a₁ ¬b₂ ¬c₁ = f1-phase2 qs p (case2 q1)
|
|
|
210 ... | tri< a ¬b₁ ¬c | tri≈ ¬a₁ b ¬c₁ = ⊥-elim ( ¬a₁ (subst₂ (λ j k → j < k) (sym fin+1-toℕ) (toℕ-fromℕ< _) a ))
|
|
|
211 ... | tri< a ¬b₁ ¬c | tri> ¬a₁ ¬b₂ c₁ = ⊥-elim ( ¬a₁ (subst₂ (λ j k → j < k) (sym fin+1-toℕ) (toℕ-fromℕ< _) a ))
|
|
|
212 ... | tri≈ ¬a₁ b ¬c | tri< a ¬b₁ ¬c₁ = ⊥-elim ( ¬a₁ (subst₂ (λ j k → j < k) fin+1-toℕ (sym (toℕ-fromℕ< _)) a ))
|
|
|
213 ... | tri≈ ¬a₁ b ¬c | tri≈ ¬a₂ b₁ ¬c₁ = refl
|
|
|
214 ... | tri≈ ¬a₁ b ¬c | tri> ¬a₂ ¬b₁ c₁ = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) fin+1-toℕ (sym (toℕ-fromℕ< _)) c₁ ))
|
|
|
215 ... | tri> ¬a₁ ¬b₁ c₁ | tri< a ¬b₂ ¬c = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) (sym fin+1-toℕ) (toℕ-fromℕ< _) c₁ ))
|
|
|
216 ... | tri> ¬a₁ ¬b₁ c₁ | tri≈ ¬a₂ b ¬c = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) (sym fin+1-toℕ) (toℕ-fromℕ< _) c₁ ))
|
|
|
217 ... | tri> ¬a₁ ¬b₁ c₁ | tri> ¬a₂ ¬b₂ c₂ = f1-phase2 qs p (case2 q1 )
|
|
288
|
218 f1-phase1 : (qs : List (Fin (suc n)) ) → fin-phase1 i (list-less qs) ≡ true
|
|
|
219 → (fin-phase1 (fromℕ< a<sa) qs ≡ false ) ∨ (fin-phase2 (fromℕ< a<sa) qs ≡ false)
|
|
|
220 → fin-phase1 (fin+1 i) qs ≡ true
|
|
290
|
221 f1-phase1 (x ∷ qs) p (case1 q1) with <-fcmp (fromℕ< a<sa) x
|
|
|
222 ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a (subst (λ k → toℕ x < suc k ) (sym fin<asa) (fin≤n _ )))
|
|
|
223 f1-phase1 (x ∷ qs) p (case1 q1) | tri≈ ¬a b ¬c with <-fcmp (fin+1 i) x
|
|
|
224 ... | tri< a ¬b ¬c₁ = f1-phase1 qs p (case2 q1)
|
|
|
225 ... | tri≈ ¬a₁ b₁ ¬c₁ = f1-phase2 qs {!!} (case2 q1) -- fin-phase1 i (list-less qs) ≡ true
|
|
|
226 ... | tri> ¬a₁ ¬b c = f1-phase1 qs p (case2 q1)
|
|
|
227 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
|
|
|
228 ... | tri< a ¬b₁ ¬c | tri< a₁ ¬b₂ ¬c₁ = f1-phase1 qs p (case1 q1)
|
|
|
229 ... | tri< a ¬b₁ ¬c | tri≈ ¬a₁ b ¬c₁ = ⊥-elim ( ¬a₁ (subst₂ (λ j k → j < k) (sym fin+1-toℕ) (toℕ-fromℕ< _) a ))
|
|
|
230 ... | tri< a ¬b₁ ¬c | tri> ¬a₁ ¬b₂ c₁ = ⊥-elim ( ¬a₁ (subst₂ (λ j k → j < k) (sym fin+1-toℕ) (toℕ-fromℕ< _) a ))
|
|
|
231 ... | tri≈ ¬a₁ b ¬c | tri< a ¬b₁ ¬c₁ = ⊥-elim ( ¬a₁ (subst₂ (λ j k → j < k) fin+1-toℕ (sym (toℕ-fromℕ< _)) a ))
|
|
|
232 ... | tri≈ ¬a₁ b ¬c | tri≈ ¬a₂ b₁ ¬c₁ = f1-phase2 qs p (case1 q1)
|
|
|
233 ... | tri≈ ¬a₁ b ¬c | tri> ¬a₂ ¬b₁ c₁ = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) fin+1-toℕ (sym (toℕ-fromℕ< _)) c₁ ))
|
|
|
234 ... | tri> ¬a₁ ¬b₁ c₁ | tri< a ¬b₂ ¬c = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) (sym fin+1-toℕ) (toℕ-fromℕ< _) c₁ ))
|
|
|
235 ... | tri> ¬a₁ ¬b₁ c₁ | tri≈ ¬a₂ b ¬c = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) (sym fin+1-toℕ) (toℕ-fromℕ< _) c₁ ))
|
|
|
236 ... | tri> ¬a₁ ¬b₁ c₁ | tri> ¬a₂ ¬b₂ c₂ = f1-phase1 qs p (case1 q1)
|
|
|
237 f1-phase1 (x ∷ qs) p (case2 q1) with <-fcmp (fromℕ< a<sa) x
|
|
|
238 ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a (subst (λ k → toℕ x < suc k ) (sym fin<asa) (fin≤n _ )))
|
|
|
239 f1-phase1 (x ∷ qs) p (case2 q1) | tri≈ ¬a b ¬c = ⊥-elim ( ¬-bool q1 refl )
|
|
|
240 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
|
|
|
241 ... | tri< a ¬b₁ ¬c | tri< a₁ ¬b₂ ¬c₁ = f1-phase1 qs p (case2 q1)
|
|
|
242 ... | tri< a ¬b₁ ¬c | tri≈ ¬a₁ b ¬c₁ = ⊥-elim ( ¬a₁ (subst₂ (λ j k → j < k) (sym fin+1-toℕ) (toℕ-fromℕ< _) a ))
|
|
|
243 ... | tri< a ¬b₁ ¬c | tri> ¬a₁ ¬b₂ c₁ = ⊥-elim ( ¬a₁ (subst₂ (λ j k → j < k) (sym fin+1-toℕ) (toℕ-fromℕ< _) a ))
|
|
|
244 ... | tri≈ ¬a₁ b ¬c | tri< a ¬b₁ ¬c₁ = ⊥-elim ( ¬a₁ (subst₂ (λ j k → j < k) fin+1-toℕ (sym (toℕ-fromℕ< _)) a ))
|
|
|
245 ... | tri≈ ¬a₁ b ¬c | tri≈ ¬a₂ b₁ ¬c₁ = f1-phase2 qs p (case2 q1)
|
|
|
246 ... | tri≈ ¬a₁ b ¬c | tri> ¬a₂ ¬b₁ c₁ = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) fin+1-toℕ (sym (toℕ-fromℕ< _)) c₁ ))
|
|
|
247 ... | tri> ¬a₁ ¬b₁ c₁ | tri< a ¬b₂ ¬c = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) (sym fin+1-toℕ) (toℕ-fromℕ< _) c₁ ))
|
|
|
248 ... | tri> ¬a₁ ¬b₁ c₁ | tri≈ ¬a₂ b ¬c = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) (sym fin+1-toℕ) (toℕ-fromℕ< _) c₁ ))
|
|
|
249 ... | tri> ¬a₁ ¬b₁ c₁ | tri> ¬a₂ ¬b₂ c₂ = f1-phase1 qs p (case2 q1)
|
|
285
|
250 fdup-phase2 : (qs : List (Fin (suc n)) )
|
|
|
251 → ( fin-phase2 (fromℕ< a<sa ) qs ≡ true ) ∨ NList n qs
|
|
286
|
252 fdup-phase2 [] = case2 record { ls = [] ; lseq = refl ; ls< = case1 refl }
|
|
285
|
253 fdup-phase2 (x ∷ qs) with <-fcmp (fromℕ< a<sa) x
|
|
284
|
254 ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a (subst (λ k → toℕ x < suc k) (sym fin<asa) fin<n ))
|
|
285
|
255 fdup-phase2 (x ∷ qs) | tri≈ ¬a b ¬c = case1 refl
|
|
|
256 fdup-phase2 (x ∷ qs) | tri> ¬a ¬b c with fdup-phase2 qs
|
|
283
|
257 ... | case1 p = case1 p
|
|
286
|
258 ... | case2 nlist = case2 record { ls = x<y→fin-1 c ∷ NList.ls nlist ; lseq = fdup01 ; ls< = case1 {!!} } where
|
|
285
|
259 fdup01 : list-less (x ∷ qs) ≡ x<y→fin-1 c ∷ NList.ls nlist
|
|
288
|
260 fdup01 with <-fcmp (fromℕ< a<sa) x
|
|
|
261 ... | tri< a ¬b ¬c = {!!} -- begin
|
|
|
262 -- fromℕ< a ∷ list-less qs ≡⟨ cong₂ (λ j k → j ∷ k ) (lemma10 refl) (NList.lseq nlist) ⟩
|
|
|
263 -- fromℕ< (≤-trans c (fin≤n (fromℕ< a<sa))) ∷ NList.ls nlist ∎ where open ≡-Reasoning
|
|
|
264 ... | tri≈ ¬a b ¬c = {!!} -- ⊥-elim ( nat-≡< b (subst (λ k → toℕ x < k ) fin<asa c ))
|
|
|
265 ... | tri> ¬a ¬b c = {!!} -- ⊥-elim ( nat-≤> (fin≤n x) c )
|
|
285
|
266 fdup-phase1 : (qs : List (Fin (suc n)) ) → (fin-phase1 (fromℕ< a<sa) qs ≡ true) ∨ NList n qs
|
|
286
|
267 fdup-phase1 [] = case2 record { ls = [] ; lseq = refl ; ls< = case1 refl }
|
|
285
|
268 fdup-phase1 (x ∷ qs) with <-fcmp (fromℕ< a<sa) x
|
|
|
269 fdup-phase1 (x ∷ qs) | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a (subst (λ k → toℕ x < suc k) (sym fin<asa) fin<n ))
|
|
|
270 fdup-phase1 (x ∷ qs) | tri≈ ¬a b ¬c with fdup-phase2 qs
|
|
283
|
271 ... | case1 p = case1 p
|
|
286
|
272 ... | case2 nlist = case2 record { ls = NList.ls nlist ; lseq = {!!} ; ls< = case2 {!!} } where
|
|
285
|
273 fdup03 : list-less (x ∷ qs) ≡ NList.ls nlist
|
|
|
274 fdup03 = {!!}
|
|
286
|
275 fdup06 : suc (length (NList.ls nlist)) ≡ length (x ∷ qs)
|
|
|
276 fdup06 = {!!}
|
|
285
|
277 fdup-phase1 (x ∷ qs) | tri> ¬a ¬b c with fdup-phase1 qs
|
|
283
|
278 ... | case1 p = case1 p
|
|
286
|
279 ... | case2 nlist = case2 record { ls = x<y→fin-1 c ∷ NList.ls nlist ; lseq = {!!} ; ls< = case1 fdup5 } where
|
|
|
280 fdup5 : length (x<y→fin-1 c ∷ NList.ls nlist) ≡ length (x ∷ qs)
|
|
|
281 fdup5 = {!!}
|
|
283
|
282 fdup-phase0 : FDup-in-list (suc n) qs
|
|
285
|
283 fdup-phase0 with fdup-phase1 qs
|
|
283
|
284 ... | case1 dup = record { dup = fromℕ< a<sa ; is-dup = dup }
|
|
287
|
285 ... | case2 nlist = fdup+1 qs (FDup-in-list.dup fdup) (FDup-in-list.is-dup fdup) where
|
|
286
|
286 fdup04 : (length (NList.ls nlist) ≡ length qs) ∨ (suc (length (NList.ls nlist)) ≡ length qs) → length (list-less qs) > n
|
|
|
287 fdup04 (case1 eq) = px≤py ( begin
|
|
|
288 suc (suc n) ≤⟨ lt ⟩
|
|
|
289 length qs ≡⟨ sym eq ⟩
|
|
|
290 length (NList.ls nlist) ≡⟨ cong (λ k → length k) (sym (NList.lseq nlist )) ⟩
|
|
|
291 length (list-less qs) ≤⟨ refl-≤s ⟩
|
|
|
292 suc (length (list-less qs)) ∎ ) where open ≤-Reasoning
|
|
|
293 fdup04 (case2 eq) = px≤py ( begin
|
|
|
294 suc (suc n) ≤⟨ lt ⟩
|
|
|
295 length qs ≡⟨ sym eq ⟩
|
|
|
296 suc (length (NList.ls nlist)) ≡⟨ cong (λ k → suc (length k)) (sym (NList.lseq nlist )) ⟩
|
|
|
297 suc (length (list-less qs)) ∎ ) where open ≤-Reasoning
|
|
283
|
298 fdup : FDup-in-list n (list-less qs)
|
|
286
|
299 fdup = fin-dup-in-list>n (list-less qs) ( fdup04 (NList.ls< nlist) )
|
