|
153
|
1 {-# OPTIONS --allow-unsolved-metas #-}
|
|
151
|
2 module FLutil where
|
|
134
|
3
|
|
|
4 open import Level hiding ( suc ; zero )
|
|
|
5 open import Data.Fin hiding ( _<_ ; _≤_ ; _-_ ; _+_ ; _≟_)
|
|
156
|
6 open import Data.Fin.Properties hiding ( <-trans ; ≤-refl ; ≤-trans ; ≤-irrelevant ; _≟_ ) renaming ( <-cmp to <-fcmp )
|
|
172
|
7 open import Data.Fin.Permutation -- hiding ([_,_])
|
|
134
|
8 open import Data.Nat -- using (ℕ; suc; zero; s≤s ; z≤n )
|
|
173
|
9 open import Data.Nat.Properties as DNP
|
|
172
|
10 open import Relation.Binary.PropositionalEquality hiding ( [_] )
|
|
153
|
11 open import Data.List using (List; []; _∷_ ; length ; _++_ ; tail ) renaming (reverse to rev )
|
|
134
|
12 open import Data.Product
|
|
|
13 open import Relation.Nullary
|
|
|
14 open import Data.Empty
|
|
|
15 open import Relation.Binary.Core
|
|
172
|
16 open import Relation.Binary.Definitions
|
|
137
|
17 open import logic
|
|
|
18 open import nat
|
|
134
|
19
|
|
|
20 infixr 100 _::_
|
|
|
21
|
|
|
22 data FL : (n : ℕ )→ Set where
|
|
|
23 f0 : FL 0
|
|
|
24 _::_ : { n : ℕ } → Fin (suc n ) → FL n → FL (suc n)
|
|
|
25
|
|
|
26 data _f<_ : {n : ℕ } (x : FL n ) (y : FL n) → Set where
|
|
|
27 f<n : {m : ℕ } {xn yn : Fin (suc m) } {xt yt : FL m} → xn Data.Fin.< yn → (xn :: xt) f< ( yn :: yt )
|
|
|
28 f<t : {m : ℕ } {xn : Fin (suc m) } {xt yt : FL m} → xt f< yt → (xn :: xt) f< ( xn :: yt )
|
|
|
29
|
|
|
30 FLeq : {n : ℕ } {xn yn : Fin (suc n)} {x : FL n } {y : FL n} → xn :: x ≡ yn :: y → ( xn ≡ yn ) × (x ≡ y )
|
|
|
31 FLeq refl = refl , refl
|
|
|
32
|
|
|
33 f-<> : {n : ℕ } {x : FL n } {y : FL n} → x f< y → y f< x → ⊥
|
|
|
34 f-<> (f<n x) (f<n x₁) = nat-<> x x₁
|
|
|
35 f-<> (f<n x) (f<t lt2) = nat-≡< refl x
|
|
|
36 f-<> (f<t lt) (f<n x) = nat-≡< refl x
|
|
|
37 f-<> (f<t lt) (f<t lt2) = f-<> lt lt2
|
|
|
38
|
|
|
39 f-≡< : {n : ℕ } {x : FL n } {y : FL n} → x ≡ y → y f< x → ⊥
|
|
|
40 f-≡< refl (f<n x) = nat-≡< refl x
|
|
|
41 f-≡< refl (f<t lt) = f-≡< refl lt
|
|
|
42
|
|
|
43 FLcmp : {n : ℕ } → Trichotomous {Level.zero} {FL n} _≡_ _f<_
|
|
|
44 FLcmp f0 f0 = tri≈ (λ ()) refl (λ ())
|
|
|
45 FLcmp (xn :: xt) (yn :: yt) with <-fcmp xn yn
|
|
|
46 ... | tri< a ¬b ¬c = tri< (f<n a) (λ eq → nat-≡< (cong toℕ (proj₁ (FLeq eq)) ) a) (λ lt → f-<> lt (f<n a) )
|
|
|
47 ... | tri> ¬a ¬b c = tri> (λ lt → f-<> lt (f<n c) ) (λ eq → nat-≡< (cong toℕ (sym (proj₁ (FLeq eq)) )) c) (f<n c)
|
|
|
48 ... | tri≈ ¬a refl ¬c with FLcmp xt yt
|
|
|
49 ... | tri< a ¬b ¬c₁ = tri< (f<t a) (λ eq → ¬b (proj₂ (FLeq eq) )) (λ lt → f-<> lt (f<t a) )
|
|
|
50 ... | tri≈ ¬a₁ refl ¬c₁ = tri≈ (λ lt → f-≡< refl lt ) refl (λ lt → f-≡< refl lt )
|
|
|
51 ... | tri> ¬a₁ ¬b c = tri> (λ lt → f-<> lt (f<t c) ) (λ eq → ¬b (proj₂ (FLeq eq) )) (f<t c)
|
|
|
52
|
|
138
|
53 f<-trans : {n : ℕ } { x y z : FL n } → x f< y → y f< z → x f< z
|
|
|
54 f<-trans {suc n} (f<n x) (f<n x₁) = f<n ( Data.Fin.Properties.<-trans x x₁ )
|
|
|
55 f<-trans {suc n} (f<n x) (f<t y<z) = f<n x
|
|
|
56 f<-trans {suc n} (f<t x<y) (f<n x) = f<n x
|
|
|
57 f<-trans {suc n} (f<t x<y) (f<t y<z) = f<t (f<-trans x<y y<z)
|
|
|
58
|
|
134
|
59 infixr 250 _f<?_
|
|
|
60
|
|
|
61 _f<?_ : {n : ℕ} → (x y : FL n ) → Dec (x f< y )
|
|
|
62 x f<? y with FLcmp x y
|
|
|
63 ... | tri< a ¬b ¬c = yes a
|
|
|
64 ... | tri≈ ¬a refl ¬c = no ( ¬a )
|
|
|
65 ... | tri> ¬a ¬b c = no ( ¬a )
|
|
|
66
|
|
|
67 _f≤_ : {n : ℕ } (x : FL n ) (y : FL n) → Set
|
|
|
68 _f≤_ x y = (x ≡ y ) ∨ (x f< y )
|
|
|
69
|
|
|
70 FL0 : {n : ℕ } → FL n
|
|
|
71 FL0 {zero} = f0
|
|
|
72 FL0 {suc n} = zero :: FL0
|
|
|
73
|
|
|
74
|
|
|
75 fmax : { n : ℕ } → FL n
|
|
|
76 fmax {zero} = f0
|
|
|
77 fmax {suc n} = fromℕ< a<sa :: fmax {n}
|
|
|
78
|
|
|
79 fmax< : { n : ℕ } → {x : FL n } → ¬ (fmax f< x )
|
|
|
80 fmax< {suc n} {x :: y} (f<n lt) = nat-≤> (fmax1 x) lt where
|
|
|
81 fmax1 : {n : ℕ } → (x : Fin (suc n)) → toℕ x ≤ toℕ (fromℕ< {n} a<sa)
|
|
|
82 fmax1 {zero} zero = z≤n
|
|
|
83 fmax1 {suc n} zero = z≤n
|
|
|
84 fmax1 {suc n} (suc x) = s≤s (fmax1 x)
|
|
|
85 fmax< {suc n} {x :: y} (f<t lt) = fmax< {n} {y} lt
|
|
|
86
|
|
|
87 fmax¬ : { n : ℕ } → {x : FL n } → ¬ ( x ≡ fmax ) → x f< fmax
|
|
|
88 fmax¬ {zero} {f0} ne = ⊥-elim ( ne refl )
|
|
|
89 fmax¬ {suc n} {x} ne with FLcmp x fmax
|
|
|
90 ... | tri< a ¬b ¬c = a
|
|
|
91 ... | tri≈ ¬a b ¬c = ⊥-elim ( ne b)
|
|
|
92 ... | tri> ¬a ¬b c = ⊥-elim (fmax< c)
|
|
|
93
|
|
|
94 FL0≤ : {n : ℕ } → FL0 {n} f≤ fmax
|
|
|
95 FL0≤ {zero} = case1 refl
|
|
|
96 FL0≤ {suc zero} = case1 refl
|
|
|
97 FL0≤ {suc n} with <-fcmp zero (fromℕ< {n} a<sa)
|
|
|
98 ... | tri< a ¬b ¬c = case2 (f<n a)
|
|
|
99 ... | tri≈ ¬a b ¬c with FL0≤ {n}
|
|
|
100 ... | case1 x = case1 (subst₂ (λ j k → (zero :: FL0) ≡ (j :: k ) ) b x refl )
|
|
|
101 ... | case2 x = case2 (subst (λ k → (zero :: FL0) f< (k :: fmax)) b (f<t x) )
|
|
|
102
|
|
151
|
103 open import Data.Nat.Properties using ( ≤-trans ; <-trans )
|
|
|
104 fsuc : { n : ℕ } → (x : FL n ) → x f< fmax → FL n
|
|
|
105 fsuc {n} (x :: y) (f<n lt) = fromℕ< fsuc1 :: y where
|
|
|
106 fsuc1 : suc (toℕ x) < n
|
|
|
107 fsuc1 = Data.Nat.Properties.≤-trans (s≤s lt) ( s≤s ( toℕ≤pred[n] (fromℕ< a<sa)) )
|
|
|
108 fsuc (x :: y) (f<t lt) = x :: fsuc y lt
|
|
|
109
|
|
174
|
110 -- fsuc0 : { n : ℕ } → (x : FL n ) → FL n
|
|
|
111 -- fsuc0 {n} (x :: y) (f<n lt) = fromℕ< fsuc2 :: y where
|
|
|
112 -- fsuc2 : suc (toℕ x) < n
|
|
|
113 -- fsuc2 = Data.Nat.Properties.≤-trans (s≤s lt) ( s≤s ( toℕ≤pred[n] (fromℕ< a<sa)) )
|
|
|
114 -- fsuc0 (x :: y) (f<t lt) = x :: fsuc y lt
|
|
|
115
|
|
|
116 open import Data.Maybe
|
|
|
117 open import fin
|
|
|
118
|
|
|
119 fpredm : { n : ℕ } → (x : FL n ) → Maybe (FL n)
|
|
|
120 fpredm f0 = nothing
|
|
|
121 fpredm (x :: y) with fpredm y
|
|
|
122 ... | just y1 = just (x :: y1)
|
|
|
123 fpredm (zero :: y) | nothing = nothing
|
|
|
124 fpredm (suc x :: y) | nothing = just (fin+1 x :: fmax)
|
|
|
125
|
|
|
126 ¬<FL0 : {n : ℕ} {y : FL n} → ¬ y f< FL0
|
|
|
127 ¬<FL0 {suc n} {zero :: y} (f<t lt) = ¬<FL0 {n} {y} lt
|
|
|
128
|
|
|
129 fpred : { n : ℕ } → (x : FL n ) → FL0 f< x → FL n
|
|
|
130 fpred (zero :: y) (f<t lt) = zero :: fpred y lt
|
|
|
131 fpred (x :: y) (f<n lt) with FLcmp FL0 y
|
|
|
132 ... | tri< a ¬b ¬c = x :: fpred y a
|
|
|
133 ... | tri> ¬a ¬b c = ⊥-elim (¬<FL0 c)
|
|
|
134 fpred {suc _} (suc x :: y) (f<n lt) | tri≈ ¬a b ¬c = fin+1 x :: fmax
|
|
|
135
|
|
|
136 fpred< : { n : ℕ } → (x : FL n ) → (lt : FL0 f< x ) → fpred x lt f< x
|
|
|
137 fpred< (zero :: y) (f<t lt) = f<t (fpred< y lt)
|
|
|
138 fpred< (suc x :: y) (f<n lt) with FLcmp FL0 y
|
|
|
139 ... | tri< a ¬b ¬c = f<t ( fpred< y a)
|
|
|
140 ... | tri> ¬a ¬b c = ⊥-elim (¬<FL0 c)
|
|
|
141 ... | tri≈ ¬a refl ¬c = f<n fpr1 where
|
|
|
142 fpr1 : {n : ℕ } {x : Fin n} → fin+1 x Data.Fin.< suc x
|
|
|
143 fpr1 {suc _} {zero} = s≤s z≤n
|
|
|
144 fpr1 {suc _} {suc x} = s≤s fpr1
|
|
|
145
|
|
151
|
146 flist1 : {n : ℕ } (i : ℕ) → i < suc n → List (FL n) → List (FL n) → List (FL (suc n))
|
|
|
147 flist1 zero i<n [] _ = []
|
|
|
148 flist1 zero i<n (a ∷ x ) z = ( zero :: a ) ∷ flist1 zero i<n x z
|
|
|
149 flist1 (suc i) (s≤s i<n) [] z = flist1 i (Data.Nat.Properties.<-trans i<n a<sa) z z
|
|
|
150 flist1 (suc i) i<n (a ∷ x ) z = ((fromℕ< i<n ) :: a ) ∷ flist1 (suc i) i<n x z
|
|
|
151
|
|
|
152 flist : {n : ℕ } → FL n → List (FL n)
|
|
|
153 flist {zero} f0 = f0 ∷ []
|
|
|
154 flist {suc n} (x :: y) = flist1 n a<sa (flist y) (flist y)
|
|
|
155
|
|
|
156 fr22 : fsuc (zero :: zero :: f0) (fmax¬ (λ ())) ≡ (suc zero :: zero :: f0)
|
|
|
157 fr22 = refl
|
|
|
158
|
|
|
159 fr4 : List (FL 4)
|
|
174
|
160 fr4 = Data.List.reverse (flist (fmax {4}) )
|
|
151
|
161 -- fr5 : List (List ℕ)
|
|
|
162 -- fr5 = map plist (map FL→perm (Data.List.reverse (flist (fmax {4}) )))
|
|
|
163
|
|
|
164
|
|
134
|
165 open import Relation.Binary as B hiding (Decidable; _⇔_)
|
|
|
166 open import Data.Sum.Base as Sum -- inj₁
|
|
138
|
167 open import Relation.Nary using (⌊_⌋)
|
|
172
|
168 open import Data.List.Fresh hiding ([_])
|
|
134
|
169
|
|
153
|
170 FList : (n : ℕ ) → Set
|
|
|
171 FList n = List# (FL n) ⌊ _f<?_ ⌋
|
|
134
|
172
|
|
153
|
173 fr1 : FList 3
|
|
134
|
174 fr1 =
|
|
|
175 ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) ∷#
|
|
|
176 ((# 0) :: ((# 1) :: ((# 0 ) :: f0))) ∷#
|
|
|
177 ((# 1) :: ((# 0) :: ((# 0 ) :: f0))) ∷#
|
|
|
178 ((# 2) :: ((# 0) :: ((# 0 ) :: f0))) ∷#
|
|
|
179 ((# 2) :: ((# 1) :: ((# 0 ) :: f0))) ∷#
|
|
|
180 []
|
|
|
181
|
|
|
182 open import Data.Product
|
|
135
|
183 open import Relation.Nullary.Decidable hiding (⌊_⌋)
|
|
172
|
184 -- open import Data.Bool hiding (_<_ ; _≤_ )
|
|
135
|
185 open import Data.Unit.Base using (⊤ ; tt)
|
|
|
186
|
|
138
|
187 -- fresh a [] = ⊤
|
|
|
188 -- fresh a (x ∷# xs) = R a x × fresh a xs
|
|
|
189
|
|
|
190 -- toWitness
|
|
|
191 -- ttf< : {n : ℕ } → {x a : FL n } → x f< a → T (isYes (x f<? a))
|
|
|
192 -- ttf< {n} {x} {a} x<a with x f<? a
|
|
|
193 -- ... | yes y = subst (λ k → Data.Bool.T k ) refl tt
|
|
|
194 -- ... | no nn = ⊥-elim ( nn x<a )
|
|
135
|
195
|
|
153
|
196 ttf : {n : ℕ } {x a : FL (suc n)} → x f< a → (y : FList (suc n)) → fresh (FL (suc n)) ⌊ _f<?_ ⌋ a y → fresh (FL (suc n)) ⌊ _f<?_ ⌋ x y
|
|
143
|
197 ttf _ [] fr = Level.lift tt
|
|
|
198 ttf {_} {x} {a} lt (cons a₁ y x1) (lift lt1 , x2 ) = (Level.lift (fromWitness (ttf1 lt1 lt ))) , ttf (ttf1 lt1 lt) y x1 where
|
|
141
|
199 ttf1 : True (a f<? a₁) → x f< a → x f< a₁
|
|
|
200 ttf1 t x<a = f<-trans x<a (toWitness t)
|
|
|
201
|
|
151
|
202 -- by https://gist.github.com/aristidb/1684202
|
|
|
203
|
|
153
|
204 FLinsert : {n : ℕ } → FL n → FList n → FList n
|
|
|
205 FLfresh : {n : ℕ } → (a x : FL (suc n) ) → (y : FList (suc n) ) → a f< x
|
|
148
|
206 → fresh (FL (suc n)) ⌊ _f<?_ ⌋ a y → fresh (FL (suc n)) ⌊ _f<?_ ⌋ a (FLinsert x y)
|
|
138
|
207 FLinsert {zero} f0 y = f0 ∷# []
|
|
|
208 FLinsert {suc n} x [] = x ∷# []
|
|
148
|
209 FLinsert {suc n} x (cons a y x₁) with FLcmp x a
|
|
|
210 ... | tri≈ ¬a b ¬c = cons a y x₁
|
|
|
211 ... | tri< lt ¬b ¬c = cons x ( cons a y x₁) ( Level.lift (fromWitness lt ) , ttf lt y x₁)
|
|
153
|
212 FLinsert {suc n} x (cons a [] x₁) | tri> ¬a ¬b lt = cons a ( x ∷# [] ) ( Level.lift (fromWitness lt) , Level.lift tt )
|
|
|
213 FLinsert {suc n} x (cons a y yr) | tri> ¬a ¬b a<x = cons a (FLinsert x y) (FLfresh a x y a<x yr )
|
|
147
|
214
|
|
150
|
215 FLfresh a x [] a<x (Level.lift tt) = Level.lift (fromWitness a<x) , Level.lift tt
|
|
|
216 FLfresh a x (cons b [] (Level.lift tt)) a<x (Level.lift a<b , a<y) with FLcmp x b
|
|
151
|
217 ... | tri< x<b ¬b ¬c = Level.lift (fromWitness a<x) , Level.lift a<b , Level.lift tt
|
|
149
|
218 ... | tri≈ ¬a refl ¬c = Level.lift (fromWitness a<x) , Level.lift tt
|
|
151
|
219 ... | tri> ¬a ¬b b<x = Level.lift a<b , Level.lift (fromWitness (f<-trans (toWitness a<b) b<x)) , Level.lift tt
|
|
150
|
220 FLfresh a x (cons b y br) a<x (Level.lift a<b , a<y) with FLcmp x b
|
|
151
|
221 ... | tri< x<b ¬b ¬c = Level.lift (fromWitness a<x) , Level.lift a<b , ttf (toWitness a<b) y br
|
|
|
222 ... | tri≈ ¬a refl ¬c = Level.lift (fromWitness a<x) , ttf a<x y br
|
|
150
|
223 FLfresh a x (cons b [] br) a<x (Level.lift a<b , a<y) | tri> ¬a ¬b b<x =
|
|
151
|
224 Level.lift a<b , Level.lift (fromWitness (f<-trans (toWitness a<b) b<x)) , Level.lift tt
|
|
150
|
225 FLfresh a x (cons b (cons a₁ y x₁) br) a<x (Level.lift a<b , a<y) | tri> ¬a ¬b b<x =
|
|
151
|
226 Level.lift a<b , FLfresh a x (cons a₁ y x₁) a<x a<y
|
|
134
|
227
|
|
138
|
228 fr6 = FLinsert ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) fr1
|
|
151
|
229
|
|
152
|
230 -- open import Data.List.Fresh.Relation.Unary.All
|
|
|
231 -- fr7 = append ( ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) ∷# [] ) fr1 ( ({!!} , {!!} ) ∷ [] )
|
|
|
232
|
|
153
|
233 Flist1 : {n : ℕ } (i : ℕ) → i < suc n → FList n → FList n → FList (suc n)
|
|
152
|
234 Flist1 zero i<n [] _ = []
|
|
|
235 Flist1 zero i<n (a ∷# x ) z = FLinsert ( zero :: a ) (Flist1 zero i<n x z )
|
|
|
236 Flist1 (suc i) (s≤s i<n) [] z = Flist1 i (Data.Nat.Properties.<-trans i<n a<sa) z z
|
|
|
237 Flist1 (suc i) i<n (a ∷# x ) z = FLinsert ((fromℕ< i<n ) :: a ) (Flist1 (suc i) i<n x z )
|
|
|
238
|
|
154
|
239 ∀Flist : {n : ℕ } → FL n → FList n
|
|
|
240 ∀Flist {zero} f0 = f0 ∷# []
|
|
|
241 ∀Flist {suc n} (x :: y) = Flist1 n a<sa (∀Flist y) (∀Flist y)
|
|
153
|
242
|
|
|
243 fr8 : FList 4
|
|
154
|
244 fr8 = ∀Flist fmax
|
|
|
245
|
|
172
|
246 fr9 : FList 3
|
|
|
247 fr9 = ∀Flist fmax
|
|
|
248
|
|
174
|
249 ∀Flist' : (n : ℕ ) → FList n
|
|
|
250 ∀Flist' n = ∀Flist0' n n FL0 {!!} where
|
|
|
251 ∀Flist0' : (i j : ℕ) → (x : FL n) → x f< fmax → FList n
|
|
|
252 ∀Flist0' zero zero x _ = []
|
|
|
253 ∀Flist0' zero (suc j) x lt = ∀Flist0' j j fmax {!!}
|
|
|
254 ∀Flist0' (suc i) j x lt = cons (fsuc x lt) (∀Flist0' i j (fsuc x lt) {!!} ) {!!}
|
|
|
255
|
|
|
256 -- open import Size
|
|
|
257 --
|
|
|
258 -- record CFresh {n : ℕ } (i : Size) : Set where
|
|
|
259 -- coinductive
|
|
|
260 -- field
|
|
|
261 -- δ : ∀{j : Size< i} → (y : FL n) → CFresh {n} j
|
|
|
262 -- -- δ : ∀{j : Size< i} → (y : FL n) → (xr : fresh (FL n) ⌊ _f<?_ ⌋ y x) → CFresh {n} j (cons y x xr)
|
|
|
263 --
|
|
|
264 -- open CFresh
|
|
|
265 --
|
|
|
266 -- ∀CF : ∀{i} {n : ℕ } → FL n → CFresh {n} i ?
|
|
|
267 -- δ (∀CF x) y fr = {!!}
|
|
|
268
|
|
154
|
269 open import Data.List.Fresh.Relation.Unary.Any
|
|
156
|
270 open import Data.List.Fresh.Relation.Unary.All
|
|
154
|
271
|
|
174
|
272 AnyFList' : (n : ℕ ) → (x : FL n ) → Any (x ≡_ ) (∀Flist' n)
|
|
|
273 AnyFList' 0 f0 = ?
|
|
|
274 AnyFList' (suc n) (x :: y) = {!!}
|
|
|
275
|
|
154
|
276 x∈FLins : {n : ℕ} → (x : FL n ) → (xs : FList n) → Any (x ≡_ ) (FLinsert x xs)
|
|
|
277 x∈FLins {zero} f0 [] = here refl
|
|
|
278 x∈FLins {zero} f0 (cons f0 xs x) = here refl
|
|
|
279 x∈FLins {suc n} x [] = here refl
|
|
|
280 x∈FLins {suc n} x (cons a xs x₁) with FLcmp x a
|
|
|
281 ... | tri< x<a ¬b ¬c = here refl
|
|
|
282 ... | tri≈ ¬a b ¬c = here b
|
|
|
283 x∈FLins {suc n} x (cons a [] x₁) | tri> ¬a ¬b a<x = there ( here refl )
|
|
|
284 x∈FLins {suc n} x (cons a (cons a₁ xs x₂) x₁) | tri> ¬a ¬b a<x = there ( x∈FLins x (cons a₁ xs x₂) )
|
|
|
285
|
|
173
|
286 nextAny : {n : ℕ} → {x h : FL n } → {L : FList n} → {hr : fresh (FL n) ⌊ _f<?_ ⌋ h L } → Any (x ≡_ ) L → Any (x ≡_ ) (cons h L hr )
|
|
|
287 nextAny (here x₁) = there (here x₁)
|
|
|
288 nextAny (there any) = there (there any)
|
|
|
289
|
|
156
|
290 record ∀FListP (n : ℕ ) : Set (Level.suc Level.zero) where
|
|
|
291 field
|
|
|
292 ∀list : FList n
|
|
|
293 x∈∀list : (x : FL n ) → Any (x ≡_ ) ∀list
|
|
|
294
|
|
172
|
295 open ∀FListP
|
|
|
296
|
|
173
|
297 -- open import Data.Fin.Properties as FinP
|
|
|
298
|
|
172
|
299 AnyFList : (n : ℕ ) → (x : FL n ) → Any (x ≡_ ) (∀Flist fmax)
|
|
|
300 AnyFList n x = AnyFlist0 fmax x where
|
|
173
|
301 AnyFlist1 : {n : ℕ } (i : ℕ) → (i<n : i < suc n ) → (x : Fin (suc n)) → (y : FL n) → toℕ x < suc i → (L L1 : FList n )
|
|
|
302 → Any (y ≡_ ) L1 → Any (y ≡_ ) L → Any ((x :: y ) ≡_ ) (Flist1 i i<n L L1 )
|
|
|
303 AnyFlist1 zero i<n zero y (s≤s x<i) (cons _ L _) L1 any (here refl) = x∈FLins (zero :: y) (Flist1 zero i<n L L1 )
|
|
|
304 AnyFlist1 zero i<n zero y (s≤s x<i) (cons a L ar) L1 any (there any0) = anf0 (AnyFlist1 zero i<n zero y (s≤s x<i) L L1 any any0) where
|
|
|
305 anf0 : Any ((zero :: y ) ≡_ ) (Flist1 zero i<n L L1) → Any (_≡_ (zero :: y)) (Flist1 zero i<n (cons a L ar) L1)
|
|
|
306 anf0 = {!!}
|
|
|
307 AnyFlist1 (suc i) i<n x y x<i (cons y L ar) L1 any (here refl) with <-fcmp x (fromℕ< i<n)
|
|
|
308 ... | tri≈ ¬a refl ¬c = subst {!!} {!!} (x∈FLins (x :: y) (Flist1 (suc i) i<n L L1 ))
|
|
|
309 ... | tri> ¬a ¬b c = {!!}
|
|
|
310 ... | tri< a ¬b ¬c with AnyFlist1 i {!!} x y {!!} L1 L1 any any
|
|
|
311 ... | t = {!!}
|
|
|
312 AnyFlist1 (suc i) i<n x y x<i (cons a L ar) L1 any (there any0) with AnyFlist1 (suc i) i<n x y x<i L L1 any any0
|
|
|
313 ... | t = {!!}
|
|
172
|
314 AnyFlist0 : {n : ℕ } → (y x : FL n ) → Any (x ≡_ ) (∀Flist y)
|
|
|
315 AnyFlist0 {zero} f0 f0 = here refl
|
|
173
|
316 AnyFlist0 {suc n} (_ :: z) (x :: y) = AnyFlist1 n a<sa x y fin<n (∀Flist z) (∀Flist z) (AnyFlist0 z y) (AnyFlist0 z y)
|
|
172
|
317
|
|
|
318 -- tt1 : FList 3
|
|
|
319 -- tt1 = ∀FListP.∀list (∀FList 3)
|
|
152
|
320
|
|
|
321 -- FLinsert membership
|
|
|
322
|
|
|
323 module FLMB { n : ℕ } where
|
|
|
324
|
|
|
325 FL-Setoid : Setoid Level.zero Level.zero
|
|
|
326 FL-Setoid = record { Carrier = FL n ; _≈_ = _≡_ ; isEquivalence = record { sym = sym ; refl = refl ; trans = trans }}
|
|
|
327
|
|
|
328 open import Data.List.Fresh.Membership.Setoid FL-Setoid
|
|
|
329
|
|
153
|
330 FLinsert-mb : (x : FL n ) → (xs : FList n) → x ∈ FLinsert x xs
|
|
154
|
331 FLinsert-mb x xs = x∈FLins {n} x xs
|
|
153
|
332
|
|
154
|
333
|
