|
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 ( _<_ ; _≤_ ; _-_ ; _+_ ; _≟_)
|
|
|
6 open import Data.Fin.Properties hiding ( <-trans ; ≤-trans ; ≤-irrelevant ; _≟_ ) renaming ( <-cmp to <-fcmp )
|
|
|
7 open import Data.Fin.Permutation
|
|
|
8 open import Data.Nat -- using (ℕ; suc; zero; s≤s ; z≤n )
|
|
|
9 open import Relation.Binary.PropositionalEquality
|
|
153
|
10 open import Data.List using (List; []; _∷_ ; length ; _++_ ; tail ) renaming (reverse to rev )
|
|
134
|
11 open import Data.Product
|
|
|
12 open import Relation.Nullary
|
|
|
13 open import Data.Empty
|
|
|
14 open import Relation.Binary.Core
|
|
|
15 open import Relation.Binary.Definitions
|
|
137
|
16 open import logic
|
|
|
17 open import nat
|
|
134
|
18
|
|
|
19 infixr 100 _::_
|
|
|
20
|
|
|
21 data FL : (n : ℕ )→ Set where
|
|
|
22 f0 : FL 0
|
|
|
23 _::_ : { n : ℕ } → Fin (suc n ) → FL n → FL (suc n)
|
|
|
24
|
|
|
25 data _f<_ : {n : ℕ } (x : FL n ) (y : FL n) → Set where
|
|
|
26 f<n : {m : ℕ } {xn yn : Fin (suc m) } {xt yt : FL m} → xn Data.Fin.< yn → (xn :: xt) f< ( yn :: yt )
|
|
|
27 f<t : {m : ℕ } {xn : Fin (suc m) } {xt yt : FL m} → xt f< yt → (xn :: xt) f< ( xn :: yt )
|
|
|
28
|
|
|
29 FLeq : {n : ℕ } {xn yn : Fin (suc n)} {x : FL n } {y : FL n} → xn :: x ≡ yn :: y → ( xn ≡ yn ) × (x ≡ y )
|
|
|
30 FLeq refl = refl , refl
|
|
|
31
|
|
|
32 f-<> : {n : ℕ } {x : FL n } {y : FL n} → x f< y → y f< x → ⊥
|
|
|
33 f-<> (f<n x) (f<n x₁) = nat-<> x x₁
|
|
|
34 f-<> (f<n x) (f<t lt2) = nat-≡< refl x
|
|
|
35 f-<> (f<t lt) (f<n x) = nat-≡< refl x
|
|
|
36 f-<> (f<t lt) (f<t lt2) = f-<> lt lt2
|
|
|
37
|
|
|
38 f-≡< : {n : ℕ } {x : FL n } {y : FL n} → x ≡ y → y f< x → ⊥
|
|
|
39 f-≡< refl (f<n x) = nat-≡< refl x
|
|
|
40 f-≡< refl (f<t lt) = f-≡< refl lt
|
|
|
41
|
|
|
42 FLcmp : {n : ℕ } → Trichotomous {Level.zero} {FL n} _≡_ _f<_
|
|
|
43 FLcmp f0 f0 = tri≈ (λ ()) refl (λ ())
|
|
|
44 FLcmp (xn :: xt) (yn :: yt) with <-fcmp xn yn
|
|
|
45 ... | tri< a ¬b ¬c = tri< (f<n a) (λ eq → nat-≡< (cong toℕ (proj₁ (FLeq eq)) ) a) (λ lt → f-<> lt (f<n a) )
|
|
|
46 ... | tri> ¬a ¬b c = tri> (λ lt → f-<> lt (f<n c) ) (λ eq → nat-≡< (cong toℕ (sym (proj₁ (FLeq eq)) )) c) (f<n c)
|
|
|
47 ... | tri≈ ¬a refl ¬c with FLcmp xt yt
|
|
|
48 ... | tri< a ¬b ¬c₁ = tri< (f<t a) (λ eq → ¬b (proj₂ (FLeq eq) )) (λ lt → f-<> lt (f<t a) )
|
|
|
49 ... | tri≈ ¬a₁ refl ¬c₁ = tri≈ (λ lt → f-≡< refl lt ) refl (λ lt → f-≡< refl lt )
|
|
|
50 ... | tri> ¬a₁ ¬b c = tri> (λ lt → f-<> lt (f<t c) ) (λ eq → ¬b (proj₂ (FLeq eq) )) (f<t c)
|
|
|
51
|
|
138
|
52 f<-trans : {n : ℕ } { x y z : FL n } → x f< y → y f< z → x f< z
|
|
|
53 f<-trans {suc n} (f<n x) (f<n x₁) = f<n ( Data.Fin.Properties.<-trans x x₁ )
|
|
|
54 f<-trans {suc n} (f<n x) (f<t y<z) = f<n x
|
|
|
55 f<-trans {suc n} (f<t x<y) (f<n x) = f<n x
|
|
|
56 f<-trans {suc n} (f<t x<y) (f<t y<z) = f<t (f<-trans x<y y<z)
|
|
|
57
|
|
134
|
58 infixr 250 _f<?_
|
|
|
59
|
|
|
60 _f<?_ : {n : ℕ} → (x y : FL n ) → Dec (x f< y )
|
|
|
61 x f<? y with FLcmp x y
|
|
|
62 ... | tri< a ¬b ¬c = yes a
|
|
|
63 ... | tri≈ ¬a refl ¬c = no ( ¬a )
|
|
|
64 ... | tri> ¬a ¬b c = no ( ¬a )
|
|
|
65
|
|
|
66 _f≤_ : {n : ℕ } (x : FL n ) (y : FL n) → Set
|
|
|
67 _f≤_ x y = (x ≡ y ) ∨ (x f< y )
|
|
|
68
|
|
|
69 FL0 : {n : ℕ } → FL n
|
|
|
70 FL0 {zero} = f0
|
|
|
71 FL0 {suc n} = zero :: FL0
|
|
|
72
|
|
|
73
|
|
|
74 fmax : { n : ℕ } → FL n
|
|
|
75 fmax {zero} = f0
|
|
|
76 fmax {suc n} = fromℕ< a<sa :: fmax {n}
|
|
|
77
|
|
|
78 fmax< : { n : ℕ } → {x : FL n } → ¬ (fmax f< x )
|
|
|
79 fmax< {suc n} {x :: y} (f<n lt) = nat-≤> (fmax1 x) lt where
|
|
|
80 fmax1 : {n : ℕ } → (x : Fin (suc n)) → toℕ x ≤ toℕ (fromℕ< {n} a<sa)
|
|
|
81 fmax1 {zero} zero = z≤n
|
|
|
82 fmax1 {suc n} zero = z≤n
|
|
|
83 fmax1 {suc n} (suc x) = s≤s (fmax1 x)
|
|
|
84 fmax< {suc n} {x :: y} (f<t lt) = fmax< {n} {y} lt
|
|
|
85
|
|
|
86 fmax¬ : { n : ℕ } → {x : FL n } → ¬ ( x ≡ fmax ) → x f< fmax
|
|
|
87 fmax¬ {zero} {f0} ne = ⊥-elim ( ne refl )
|
|
|
88 fmax¬ {suc n} {x} ne with FLcmp x fmax
|
|
|
89 ... | tri< a ¬b ¬c = a
|
|
|
90 ... | tri≈ ¬a b ¬c = ⊥-elim ( ne b)
|
|
|
91 ... | tri> ¬a ¬b c = ⊥-elim (fmax< c)
|
|
|
92
|
|
|
93 FL0≤ : {n : ℕ } → FL0 {n} f≤ fmax
|
|
|
94 FL0≤ {zero} = case1 refl
|
|
|
95 FL0≤ {suc zero} = case1 refl
|
|
|
96 FL0≤ {suc n} with <-fcmp zero (fromℕ< {n} a<sa)
|
|
|
97 ... | tri< a ¬b ¬c = case2 (f<n a)
|
|
|
98 ... | tri≈ ¬a b ¬c with FL0≤ {n}
|
|
|
99 ... | case1 x = case1 (subst₂ (λ j k → (zero :: FL0) ≡ (j :: k ) ) b x refl )
|
|
|
100 ... | case2 x = case2 (subst (λ k → (zero :: FL0) f< (k :: fmax)) b (f<t x) )
|
|
|
101
|
|
151
|
102 open import Data.Nat.Properties using ( ≤-trans ; <-trans )
|
|
|
103 fsuc : { n : ℕ } → (x : FL n ) → x f< fmax → FL n
|
|
|
104 fsuc {n} (x :: y) (f<n lt) = fromℕ< fsuc1 :: y where
|
|
|
105 fsuc2 : toℕ x < toℕ (fromℕ< a<sa)
|
|
|
106 fsuc2 = lt
|
|
|
107 fsuc1 : suc (toℕ x) < n
|
|
|
108 fsuc1 = Data.Nat.Properties.≤-trans (s≤s lt) ( s≤s ( toℕ≤pred[n] (fromℕ< a<sa)) )
|
|
|
109 fsuc (x :: y) (f<t lt) = x :: fsuc y lt
|
|
|
110
|
|
|
111 flist1 : {n : ℕ } (i : ℕ) → i < suc n → List (FL n) → List (FL n) → List (FL (suc n))
|
|
|
112 flist1 zero i<n [] _ = []
|
|
|
113 flist1 zero i<n (a ∷ x ) z = ( zero :: a ) ∷ flist1 zero i<n x z
|
|
|
114 flist1 (suc i) (s≤s i<n) [] z = flist1 i (Data.Nat.Properties.<-trans i<n a<sa) z z
|
|
|
115 flist1 (suc i) i<n (a ∷ x ) z = ((fromℕ< i<n ) :: a ) ∷ flist1 (suc i) i<n x z
|
|
|
116
|
|
|
117 flist : {n : ℕ } → FL n → List (FL n)
|
|
|
118 flist {zero} f0 = f0 ∷ []
|
|
|
119 flist {suc n} (x :: y) = flist1 n a<sa (flist y) (flist y)
|
|
|
120
|
|
|
121 fr22 : fsuc (zero :: zero :: f0) (fmax¬ (λ ())) ≡ (suc zero :: zero :: f0)
|
|
|
122 fr22 = refl
|
|
|
123
|
|
|
124 fr4 : List (FL 4)
|
|
|
125 fr4 = Data.List.reverse (flist (fmax {4}) )
|
|
|
126
|
|
|
127 -- fr5 : List (List ℕ)
|
|
|
128 -- fr5 = map plist (map FL→perm (Data.List.reverse (flist (fmax {4}) )))
|
|
|
129
|
|
|
130
|
|
134
|
131 open import Relation.Binary as B hiding (Decidable; _⇔_)
|
|
|
132 open import Data.Sum.Base as Sum -- inj₁
|
|
138
|
133 open import Relation.Nary using (⌊_⌋)
|
|
134
|
134 open import Data.List.Fresh
|
|
|
135
|
|
153
|
136 FList : (n : ℕ ) → Set
|
|
|
137 FList n = List# (FL n) ⌊ _f<?_ ⌋
|
|
134
|
138
|
|
153
|
139 fr1 : FList 3
|
|
134
|
140 fr1 =
|
|
|
141 ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) ∷#
|
|
|
142 ((# 0) :: ((# 1) :: ((# 0 ) :: f0))) ∷#
|
|
|
143 ((# 1) :: ((# 0) :: ((# 0 ) :: f0))) ∷#
|
|
|
144 ((# 2) :: ((# 0) :: ((# 0 ) :: f0))) ∷#
|
|
|
145 ((# 2) :: ((# 1) :: ((# 0 ) :: f0))) ∷#
|
|
|
146 []
|
|
|
147
|
|
|
148 open import Data.Product
|
|
135
|
149 open import Relation.Nullary.Decidable hiding (⌊_⌋)
|
|
152
|
150 open import Data.Bool hiding (_<_)
|
|
135
|
151 open import Data.Unit.Base using (⊤ ; tt)
|
|
|
152
|
|
138
|
153 -- fresh a [] = ⊤
|
|
|
154 -- fresh a (x ∷# xs) = R a x × fresh a xs
|
|
|
155
|
|
|
156 -- toWitness
|
|
|
157 -- ttf< : {n : ℕ } → {x a : FL n } → x f< a → T (isYes (x f<? a))
|
|
|
158 -- ttf< {n} {x} {a} x<a with x f<? a
|
|
|
159 -- ... | yes y = subst (λ k → Data.Bool.T k ) refl tt
|
|
|
160 -- ... | no nn = ⊥-elim ( nn x<a )
|
|
135
|
161
|
|
153
|
162 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
|
163 ttf _ [] fr = Level.lift tt
|
|
|
164 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
|
165 ttf1 : True (a f<? a₁) → x f< a → x f< a₁
|
|
|
166 ttf1 t x<a = f<-trans x<a (toWitness t)
|
|
|
167
|
|
151
|
168 -- by https://gist.github.com/aristidb/1684202
|
|
|
169
|
|
153
|
170 FLinsert : {n : ℕ } → FL n → FList n → FList n
|
|
|
171 FLfresh : {n : ℕ } → (a x : FL (suc n) ) → (y : FList (suc n) ) → a f< x
|
|
148
|
172 → fresh (FL (suc n)) ⌊ _f<?_ ⌋ a y → fresh (FL (suc n)) ⌊ _f<?_ ⌋ a (FLinsert x y)
|
|
138
|
173 FLinsert {zero} f0 y = f0 ∷# []
|
|
|
174 FLinsert {suc n} x [] = x ∷# []
|
|
148
|
175 FLinsert {suc n} x (cons a y x₁) with FLcmp x a
|
|
|
176 ... | tri≈ ¬a b ¬c = cons a y x₁
|
|
|
177 ... | tri< lt ¬b ¬c = cons x ( cons a y x₁) ( Level.lift (fromWitness lt ) , ttf lt y x₁)
|
|
153
|
178 FLinsert {suc n} x (cons a [] x₁) | tri> ¬a ¬b lt = cons a ( x ∷# [] ) ( Level.lift (fromWitness lt) , Level.lift tt )
|
|
|
179 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
|
180
|
|
150
|
181 FLfresh a x [] a<x (Level.lift tt) = Level.lift (fromWitness a<x) , Level.lift tt
|
|
|
182 FLfresh a x (cons b [] (Level.lift tt)) a<x (Level.lift a<b , a<y) with FLcmp x b
|
|
151
|
183 ... | tri< x<b ¬b ¬c = Level.lift (fromWitness a<x) , Level.lift a<b , Level.lift tt
|
|
149
|
184 ... | tri≈ ¬a refl ¬c = Level.lift (fromWitness a<x) , Level.lift tt
|
|
151
|
185 ... | tri> ¬a ¬b b<x = Level.lift a<b , Level.lift (fromWitness (f<-trans (toWitness a<b) b<x)) , Level.lift tt
|
|
150
|
186 FLfresh a x (cons b y br) a<x (Level.lift a<b , a<y) with FLcmp x b
|
|
151
|
187 ... | tri< x<b ¬b ¬c = Level.lift (fromWitness a<x) , Level.lift a<b , ttf (toWitness a<b) y br
|
|
|
188 ... | tri≈ ¬a refl ¬c = Level.lift (fromWitness a<x) , ttf a<x y br
|
|
150
|
189 FLfresh a x (cons b [] br) a<x (Level.lift a<b , a<y) | tri> ¬a ¬b b<x =
|
|
151
|
190 Level.lift a<b , Level.lift (fromWitness (f<-trans (toWitness a<b) b<x)) , Level.lift tt
|
|
150
|
191 FLfresh a x (cons b (cons a₁ y x₁) br) a<x (Level.lift a<b , a<y) | tri> ¬a ¬b b<x =
|
|
151
|
192 Level.lift a<b , FLfresh a x (cons a₁ y x₁) a<x a<y
|
|
134
|
193
|
|
138
|
194 fr6 = FLinsert ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) fr1
|
|
151
|
195
|
|
152
|
196 -- open import Data.List.Fresh.Relation.Unary.All
|
|
|
197 -- fr7 = append ( ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) ∷# [] ) fr1 ( ({!!} , {!!} ) ∷ [] )
|
|
|
198
|
|
153
|
199 Flist1 : {n : ℕ } (i : ℕ) → i < suc n → FList n → FList n → FList (suc n)
|
|
152
|
200 Flist1 zero i<n [] _ = []
|
|
|
201 Flist1 zero i<n (a ∷# x ) z = FLinsert ( zero :: a ) (Flist1 zero i<n x z )
|
|
|
202 Flist1 (suc i) (s≤s i<n) [] z = Flist1 i (Data.Nat.Properties.<-trans i<n a<sa) z z
|
|
|
203 Flist1 (suc i) i<n (a ∷# x ) z = FLinsert ((fromℕ< i<n ) :: a ) (Flist1 (suc i) i<n x z )
|
|
|
204
|
|
154
|
205 ∀Flist : {n : ℕ } → FL n → FList n
|
|
|
206 ∀Flist {zero} f0 = f0 ∷# []
|
|
|
207 ∀Flist {suc n} (x :: y) = Flist1 n a<sa (∀Flist y) (∀Flist y)
|
|
153
|
208
|
|
|
209 fr8 : FList 4
|
|
154
|
210 fr8 = ∀Flist fmax
|
|
|
211
|
|
|
212 open import Data.List.Fresh.Relation.Unary.Any
|
|
|
213
|
|
|
214 x∈FLins : {n : ℕ} → (x : FL n ) → (xs : FList n) → Any (x ≡_ ) (FLinsert x xs)
|
|
|
215 x∈FLins {zero} f0 [] = here refl
|
|
|
216 x∈FLins {zero} f0 (cons f0 xs x) = here refl
|
|
|
217 x∈FLins {suc n} x [] = here refl
|
|
|
218 x∈FLins {suc n} x (cons a xs x₁) with FLcmp x a
|
|
|
219 ... | tri< x<a ¬b ¬c = here refl
|
|
|
220 ... | tri≈ ¬a b ¬c = here b
|
|
|
221 x∈FLins {suc n} x (cons a [] x₁) | tri> ¬a ¬b a<x = there ( here refl )
|
|
|
222 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₂) )
|
|
|
223
|
|
155
|
224 open import fin
|
|
|
225
|
|
154
|
226 x∈∀Flist : {n : ℕ } → (x : FL n ) → Any (x ≡_ ) (∀Flist fmax)
|
|
|
227 x∈∀Flist {n} x = AFlist1 n x where
|
|
155
|
228 AFList0 : (n : ℕ ) → Any (_≡_ (fromℕ< a<sa :: fmax)) (Flist1 n a<sa (∀Flist fmax) (∀Flist fmax))
|
|
|
229 AFList0 = {!!}
|
|
|
230 AFList2 : (n : ℕ ) (x : FL (suc n)) → (x1 : Fin (suc n)) (y : FL n) → x f< ( x1 :: y) → Any (_≡_ x) (Flist1 n a<sa (∀Flist y) (∀Flist y))
|
|
|
231 AFList2 = {!!}
|
|
154
|
232 AFlist1 : (n : ℕ ) → (x : FL n) → Any (_≡_ x) (∀Flist fmax)
|
|
|
233 AFlist1 zero f0 = here refl
|
|
|
234 AFlist1 (suc n) x with FLcmp x fmax
|
|
155
|
235 ... | tri< a ¬b ¬c = AFList2 n x (fromℕ< a<sa) (fmax {n}) (fmax¬ ¬b)
|
|
|
236 ... | tri≈ ¬a refl ¬c = AFList0 n
|
|
154
|
237 ... | tri> ¬a ¬b c = ⊥-elim ( fmax< c )
|
|
|
238
|
|
152
|
239
|
|
|
240 -- FLinsert membership
|
|
|
241
|
|
|
242 module FLMB { n : ℕ } where
|
|
|
243
|
|
|
244 FL-Setoid : Setoid Level.zero Level.zero
|
|
|
245 FL-Setoid = record { Carrier = FL n ; _≈_ = _≡_ ; isEquivalence = record { sym = sym ; refl = refl ; trans = trans }}
|
|
|
246
|
|
|
247 open import Data.List.Fresh.Membership.Setoid FL-Setoid
|
|
|
248
|
|
153
|
249 FLinsert-mb : (x : FL n ) → (xs : FList n) → x ∈ FLinsert x xs
|
|
154
|
250 FLinsert-mb x xs = x∈FLins {n} x xs
|
|
153
|
251
|
|
154
|
252
|
