|
134
|
1 module FL where
|
|
|
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
|
|
|
101 open import Relation.Binary as B hiding (Decidable; _⇔_)
|
|
|
102
|
|
|
103 -- f≤-isDecTotalOrder : ∀ {n} → IsDecTotalOrder _≡_ (_f≤_ {n})
|
|
|
104 -- f≤-isDecTotalOrder = record { isTotalOrder = record { isPartialOrder = record { isPreorder = {!!}
|
|
|
105 -- ; antisym = {!!}
|
|
|
106 -- }
|
|
|
107 -- ; total = {!!}
|
|
|
108 -- }
|
|
|
109 -- ; _≟_ = {!!}
|
|
|
110 -- ; _≤?_ = {!!}
|
|
|
111 -- }
|
|
|
112
|
|
|
113 open import Data.Sum.Base as Sum -- inj₁
|
|
|
114
|
|
|
115 total : {n : ℕ } → Total (_f≤_ {n})
|
|
|
116 total f0 f0 = inj₁ (case1 refl)
|
|
135
|
117 total (x :: xt) (y :: yt) with <-fcmp x y
|
|
|
118 ... | tri< a ¬b ¬c = inj₁ (case2 (f<n a))
|
|
|
119 ... | tri> ¬a ¬b c = inj₂ (case2 (f<n c))
|
|
|
120 ... | tri≈ ¬a b ¬c with FLcmp xt yt
|
|
|
121 ... | tri< a ¬b ¬c₁ = inj₁ (case2 (subst (λ k → (x :: xt ) f< (k :: yt) ) b (f<t a)))
|
|
|
122 ... | tri≈ ¬a₁ b₁ ¬c₁ = inj₁ (case1 (subst₂ (λ j k → j :: k ≡ y :: yt ) (sym b) (sym b₁ ) refl ))
|
|
|
123 ... | tri> ¬a₁ ¬b c = inj₂ (case2 (subst (λ k → (y :: yt ) f< (k :: xt) ) (sym b) (f<t c)))
|
|
134
|
124
|
|
138
|
125 open import Relation.Nary using (⌊_⌋)
|
|
134
|
126 open import Data.List.Fresh
|
|
|
127 open import Data.List.Fresh.Relation.Unary.All
|
|
|
128 open import Data.List.Fresh.Relation.Unary.Any as Any using (Any; here; there)
|
|
|
129
|
|
|
130 FList : {n : ℕ } → Set
|
|
|
131 FList {n} = List# (FL n) ⌊ _f<?_ ⌋
|
|
|
132
|
|
|
133 fr1 : FList
|
|
|
134 fr1 =
|
|
|
135 ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) ∷#
|
|
|
136 ((# 0) :: ((# 1) :: ((# 0 ) :: f0))) ∷#
|
|
|
137 ((# 1) :: ((# 0) :: ((# 0 ) :: f0))) ∷#
|
|
|
138 ((# 2) :: ((# 0) :: ((# 0 ) :: f0))) ∷#
|
|
|
139 ((# 2) :: ((# 1) :: ((# 0 ) :: f0))) ∷#
|
|
|
140 []
|
|
|
141
|
|
|
142 open import Data.Product
|
|
|
143 -- open import Data.Maybe
|
|
|
144 -- open TotalOrder
|
|
|
145
|
|
135
|
146 open import Relation.Nullary.Decidable hiding (⌊_⌋)
|
|
|
147 open import Data.Bool -- hiding (T)
|
|
|
148 open import Data.Unit.Base using (⊤ ; tt)
|
|
|
149
|
|
|
150 -- T : Data.Bool.Bool → Set
|
|
|
151 -- T true = ⊤
|
|
|
152 -- T false = ⊥
|
|
|
153
|
|
138
|
154 -- fresh a [] = ⊤
|
|
|
155 -- fresh a (x ∷# xs) = R a x × fresh a xs
|
|
|
156
|
|
|
157 -- toWitness
|
|
|
158 -- ttf< : {n : ℕ } → {x a : FL n } → x f< a → T (isYes (x f<? a))
|
|
|
159 -- ttf< {n} {x} {a} x<a with x f<? a
|
|
|
160 -- ... | yes y = subst (λ k → Data.Bool.T k ) refl tt
|
|
|
161 -- ... | no nn = ⊥-elim ( nn x<a )
|
|
135
|
162
|
|
138
|
163 FLinsert : {n : ℕ } → FL n → FList {n} → FList {n}
|
|
|
164 FLinsert {zero} f0 y = f0 ∷# []
|
|
|
165 FLinsert {suc n} x [] = x ∷# []
|
|
|
166 FLinsert {suc n} x (cons a y x₁) with total x a
|
|
135
|
167 ... | inj₁ (case1 eq) = cons a y x₁
|
|
138
|
168 FLinsert {suc n} x (cons a y x₁) | inj₁ (case2 lt) = cons x ( cons a y x₁) ( Level.lift (fromWitness lt ) , ttf a lt y x₁) where
|
|
|
169 ttf : (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
|
|
|
170 ttf a _ [] fr = Level.lift tt
|
|
|
171 ttf a lt (cons a₁ y x1) (lift lt1 , x2 ) = (Level.lift (fromWitness (ttf1 lt1 lt ))) , ttf a₁ (ttf1 lt1 lt) y x1 where
|
|
|
172 ttf1 : True (a f<? a₁) → x f< a → x f< a₁
|
|
|
173 ttf1 t x<a = f<-trans x<a (toWitness t)
|
|
135
|
174 ... | inj₂ (case1 eq) = cons a y x₁
|
|
139
|
175 ... | inj₂ (case2 lt) = cons a ( FLinsert x y ) (ttf2 y) where
|
|
|
176 ttf2 : (y : FList {suc n}) → fresh (FL (suc n)) ⌊ _f<?_ ⌋ a (FLinsert x y)
|
|
|
177 ttf2 [] with FLinsert x []
|
|
|
178 ... | [] = Level.lift tt
|
|
|
179 ... | cons a t x = {!!} , {!!}
|
|
|
180 ttf2 (cons a [] x) = {!!}
|
|
|
181 ttf2 (cons a (cons a₁ y x₁) x) = {!!}
|
|
134
|
182
|
|
138
|
183 fr6 = FLinsert ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) fr1
|
