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