|
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
|
|
|
15
|
|
|
16 infixr 100 _::_
|
|
|
17
|
|
|
18 data FL : (n : ℕ )→ Set where
|
|
|
19 f0 : FL 0
|
|
|
20 _::_ : { n : ℕ } → Fin (suc n ) → FL n → FL (suc n)
|
|
|
21
|
|
|
22 data _f<_ : {n : ℕ } (x : FL n ) (y : FL n) → Set where
|
|
|
23 f<n : {m : ℕ } {xn yn : Fin (suc m) } {xt yt : FL m} → xn Data.Fin.< yn → (xn :: xt) f< ( yn :: yt )
|
|
|
24 f<t : {m : ℕ } {xn : Fin (suc m) } {xt yt : FL m} → xt f< yt → (xn :: xt) f< ( xn :: yt )
|
|
|
25
|
|
|
26 FLeq : {n : ℕ } {xn yn : Fin (suc n)} {x : FL n } {y : FL n} → xn :: x ≡ yn :: y → ( xn ≡ yn ) × (x ≡ y )
|
|
|
27 FLeq refl = refl , refl
|
|
|
28
|
|
|
29 nat-<> : { x y : ℕ } → x < y → y < x → ⊥
|
|
|
30 nat-<> (s≤s x<y) (s≤s y<x) = nat-<> x<y y<x
|
|
|
31 nat-<≡ : { x : ℕ } → x < x → ⊥
|
|
|
32 nat-<≡ (s≤s lt) = nat-<≡ lt
|
|
|
33 nat-≡< : { x y : ℕ } → x ≡ y → x < y → ⊥
|
|
|
34 nat-≡< refl lt = nat-<≡ lt
|
|
|
35
|
|
|
36 f-<> : {n : ℕ } {x : FL n } {y : FL n} → x f< y → y f< x → ⊥
|
|
|
37 f-<> (f<n x) (f<n x₁) = nat-<> x x₁
|
|
|
38 f-<> (f<n x) (f<t lt2) = nat-≡< refl x
|
|
|
39 f-<> (f<t lt) (f<n x) = nat-≡< refl x
|
|
|
40 f-<> (f<t lt) (f<t lt2) = f-<> lt lt2
|
|
|
41
|
|
|
42 f-≡< : {n : ℕ } {x : FL n } {y : FL n} → x ≡ y → y f< x → ⊥
|
|
|
43 f-≡< refl (f<n x) = nat-≡< refl x
|
|
|
44 f-≡< refl (f<t lt) = f-≡< refl lt
|
|
|
45
|
|
|
46 FLcmp : {n : ℕ } → Trichotomous {Level.zero} {FL n} _≡_ _f<_
|
|
|
47 FLcmp f0 f0 = tri≈ (λ ()) refl (λ ())
|
|
|
48 FLcmp (xn :: xt) (yn :: yt) with <-fcmp xn yn
|
|
|
49 ... | tri< a ¬b ¬c = tri< (f<n a) (λ eq → nat-≡< (cong toℕ (proj₁ (FLeq eq)) ) a) (λ lt → f-<> lt (f<n a) )
|
|
|
50 ... | tri> ¬a ¬b c = tri> (λ lt → f-<> lt (f<n c) ) (λ eq → nat-≡< (cong toℕ (sym (proj₁ (FLeq eq)) )) c) (f<n c)
|
|
|
51 ... | tri≈ ¬a refl ¬c with FLcmp xt yt
|
|
|
52 ... | tri< a ¬b ¬c₁ = tri< (f<t a) (λ eq → ¬b (proj₂ (FLeq eq) )) (λ lt → f-<> lt (f<t a) )
|
|
|
53 ... | tri≈ ¬a₁ refl ¬c₁ = tri≈ (λ lt → f-≡< refl lt ) refl (λ lt → f-≡< refl lt )
|
|
|
54 ... | tri> ¬a₁ ¬b c = tri> (λ lt → f-<> lt (f<t c) ) (λ eq → ¬b (proj₂ (FLeq eq) )) (f<t c)
|
|
|
55
|
|
|
56 infixr 250 _f<?_
|
|
|
57
|
|
|
58 _f<?_ : {n : ℕ} → (x y : FL n ) → Dec (x f< y )
|
|
|
59 x f<? y with FLcmp x y
|
|
|
60 ... | tri< a ¬b ¬c = yes a
|
|
|
61 ... | tri≈ ¬a refl ¬c = no ( ¬a )
|
|
|
62 ... | tri> ¬a ¬b c = no ( ¬a )
|
|
|
63
|
|
|
64 open import logic
|
|
|
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 open import logic
|
|
|
74 open import nat
|
|
|
75
|
|
|
76 fmax : { n : ℕ } → FL n
|
|
|
77 fmax {zero} = f0
|
|
|
78 fmax {suc n} = fromℕ< a<sa :: fmax {n}
|
|
|
79
|
|
|
80 fmax< : { n : ℕ } → {x : FL n } → ¬ (fmax f< x )
|
|
|
81 fmax< {suc n} {x :: y} (f<n lt) = nat-≤> (fmax1 x) lt where
|
|
|
82 fmax1 : {n : ℕ } → (x : Fin (suc n)) → toℕ x ≤ toℕ (fromℕ< {n} a<sa)
|
|
|
83 fmax1 {zero} zero = z≤n
|
|
|
84 fmax1 {suc n} zero = z≤n
|
|
|
85 fmax1 {suc n} (suc x) = s≤s (fmax1 x)
|
|
|
86 fmax< {suc n} {x :: y} (f<t lt) = fmax< {n} {y} lt
|
|
|
87
|
|
|
88 fmax¬ : { n : ℕ } → {x : FL n } → ¬ ( x ≡ fmax ) → x f< fmax
|
|
|
89 fmax¬ {zero} {f0} ne = ⊥-elim ( ne refl )
|
|
|
90 fmax¬ {suc n} {x} ne with FLcmp x fmax
|
|
|
91 ... | tri< a ¬b ¬c = a
|
|
|
92 ... | tri≈ ¬a b ¬c = ⊥-elim ( ne b)
|
|
|
93 ... | tri> ¬a ¬b c = ⊥-elim (fmax< c)
|
|
|
94
|
|
|
95 FL0≤ : {n : ℕ } → FL0 {n} f≤ fmax
|
|
|
96 FL0≤ {zero} = case1 refl
|
|
|
97 FL0≤ {suc zero} = case1 refl
|
|
|
98 FL0≤ {suc n} with <-fcmp zero (fromℕ< {n} a<sa)
|
|
|
99 ... | tri< a ¬b ¬c = case2 (f<n a)
|
|
|
100 ... | tri≈ ¬a b ¬c with FL0≤ {n}
|
|
|
101 ... | case1 x = case1 (subst₂ (λ j k → (zero :: FL0) ≡ (j :: k ) ) b x refl )
|
|
|
102 ... | case2 x = case2 (subst (λ k → (zero :: FL0) f< (k :: fmax)) b (f<t x) )
|
|
|
103
|
|
|
104 open import Relation.Binary as B hiding (Decidable; _⇔_)
|
|
|
105
|
|
|
106 -- f≤-isDecTotalOrder : ∀ {n} → IsDecTotalOrder _≡_ (_f≤_ {n})
|
|
|
107 -- f≤-isDecTotalOrder = record { isTotalOrder = record { isPartialOrder = record { isPreorder = {!!}
|
|
|
108 -- ; antisym = {!!}
|
|
|
109 -- }
|
|
|
110 -- ; total = {!!}
|
|
|
111 -- }
|
|
|
112 -- ; _≟_ = {!!}
|
|
|
113 -- ; _≤?_ = {!!}
|
|
|
114 -- }
|
|
|
115
|
|
|
116 open import Data.Sum.Base as Sum -- inj₁
|
|
|
117
|
|
|
118 total : {n : ℕ } → Total (_f≤_ {n})
|
|
|
119 total f0 f0 = inj₁ (case1 refl)
|
|
135
|
120 total (x :: xt) (y :: yt) with <-fcmp x y
|
|
|
121 ... | tri< a ¬b ¬c = inj₁ (case2 (f<n a))
|
|
|
122 ... | tri> ¬a ¬b c = inj₂ (case2 (f<n c))
|
|
|
123 ... | tri≈ ¬a b ¬c with FLcmp xt yt
|
|
|
124 ... | tri< a ¬b ¬c₁ = inj₁ (case2 (subst (λ k → (x :: xt ) f< (k :: yt) ) b (f<t a)))
|
|
|
125 ... | tri≈ ¬a₁ b₁ ¬c₁ = inj₁ (case1 (subst₂ (λ j k → j :: k ≡ y :: yt ) (sym b) (sym b₁ ) refl ))
|
|
|
126 ... | tri> ¬a₁ ¬b c = inj₂ (case2 (subst (λ k → (y :: yt ) f< (k :: xt) ) (sym b) (f<t c)))
|
|
134
|
127
|
|
|
128 open import Relation.Nary using (⌊_⌋; fromWitness)
|
|
|
129 open import Data.List.Fresh
|
|
|
130 open import Data.List.Fresh.Relation.Unary.All
|
|
|
131 open import Data.List.Fresh.Relation.Unary.Any as Any using (Any; here; there)
|
|
|
132
|
|
|
133 FList : {n : ℕ } → Set
|
|
|
134 FList {n} = List# (FL n) ⌊ _f<?_ ⌋
|
|
|
135
|
|
|
136 fr1 : FList
|
|
|
137 fr1 =
|
|
|
138 ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) ∷#
|
|
|
139 ((# 0) :: ((# 1) :: ((# 0 ) :: f0))) ∷#
|
|
|
140 ((# 1) :: ((# 0) :: ((# 0 ) :: f0))) ∷#
|
|
|
141 ((# 2) :: ((# 0) :: ((# 0 ) :: f0))) ∷#
|
|
|
142 ((# 2) :: ((# 1) :: ((# 0 ) :: f0))) ∷#
|
|
|
143 []
|
|
|
144
|
|
|
145 open import Data.Product
|
|
|
146 -- open import Data.Maybe
|
|
|
147 -- open TotalOrder
|
|
|
148
|
|
135
|
149 open import Relation.Nullary.Decidable hiding (⌊_⌋)
|
|
|
150 open import Data.Bool -- hiding (T)
|
|
|
151 open import Data.Unit.Base using (⊤ ; tt)
|
|
|
152
|
|
|
153 -- T : Data.Bool.Bool → Set
|
|
|
154 -- T true = ⊤
|
|
|
155 -- T false = ⊥
|
|
|
156
|
|
|
157
|
|
134
|
158 FLcons : {n : ℕ } → FL n → FList {n} → FList {n}
|
|
|
159 FLcons {zero} f0 y = f0 ∷# []
|
|
|
160 FLcons {suc n} x [] = x ∷# []
|
|
135
|
161 FLcons {suc n} x (cons a y x₁) with total x a
|
|
|
162 ... | inj₁ (case1 eq) = cons a y x₁
|
|
136
|
163 FLcons {suc n} x (cons a y x₁) | inj₁ (case2 lt) = cons x ( cons a y x₁) ( {!!} , ttf a y x₁) where
|
|
|
164 ttf : (a : FL (suc n)) → (y : FList {suc n}) → fresh (FL (suc n)) ⌊ _f<?_ ⌋ a y → fresh (FL (suc n)) ⌊ _f<?_ ⌋ x y
|
|
|
165 ttf a [] fr = Level.lift tt
|
|
|
166 ttf a (cons a₁ y x) fr = {!!} , ttf a₁ y x
|
|
135
|
167 ... | inj₂ (case1 eq) = cons a y x₁
|
|
|
168 ... | inj₂ (case2 lt) = cons a (cons x y {!!}) {!!}
|
|
134
|
169
|
|
|
170 fr6 = FLcons ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) fr1
|
