Mercurial > hg > Members > kono > Proof > galois

comparison src/FLutil.agda @ 255:6d1619d9f880

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
library
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 09 Jan 2021 10:18:08 +0900
parents FLutil.agda@d782dd481a26
children f59a9f4cfd78
comparison
equal deleted inserted replaced
254:a5b3061f15ee 255:6d1619d9f880
1 {-# OPTIONS --allow-unsolved-metas #-}
2 module FLutil where
3
4 open import Level hiding ( suc ; zero )
5 open import Data.Fin hiding ( _<_ ; _≤_ ; _-_ ; _+_ ; _≟_)
6 open import Data.Fin.Properties hiding ( <-trans ; ≤-refl ; ≤-trans ; ≤-irrelevant ; _≟_ ) renaming ( <-cmp to <-fcmp )
7 open import Data.Fin.Permutation -- hiding ([_,_])
8 open import Data.Nat -- using (ℕ; suc; zero; s≤s ; z≤n )
9 open import Data.Nat.Properties as DNP
10 open import Relation.Binary.PropositionalEquality hiding ( [_] )
11 open import Data.List using (List; []; _∷_ ; length ; _++_ ; tail ) renaming (reverse to rev )
12 open import Data.Product
13 open import Relation.Nullary
14 open import Data.Empty
15 open import Relation.Binary.Core
16 open import Relation.Binary.Definitions
17 open import logic
18 open import nat
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 FLpos : {n : ℕ} → FL (suc n) → Fin (suc n)
34 FLpos (x :: _) = x
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 f<-trans : {n : ℕ } { x y z : FL n } → x f< y → y f< z → x f< z
57 f<-trans {suc n} (f<n x) (f<n x₁) = f<n ( Data.Fin.Properties.<-trans x x₁ )
58 f<-trans {suc n} (f<n x) (f<t y<z) = f<n x
59 f<-trans {suc n} (f<t x<y) (f<n x) = f<n x
60 f<-trans {suc n} (f<t x<y) (f<t y<z) = f<t (f<-trans x<y y<z)
61
62 infixr 250 _f<?_
63
64 _f<?_ : {n : ℕ} → (x y : FL n ) → Dec (x f< y )
65 x f<? y with FLcmp x y
66 ... | tri< a ¬b ¬c = yes a
67 ... | tri≈ ¬a refl ¬c = no ( ¬a )
68 ... | tri> ¬a ¬b c = no ( ¬a )
69
70 _f≤_ : {n : ℕ } (x : FL n ) (y : FL n) → Set
71 _f≤_ x y = (x ≡ y ) ∨ (x f< y )
72
73 FL0 : {n : ℕ } → FL n
74 FL0 {zero} = f0
75 FL0 {suc n} = zero :: FL0
76
77 fmax : { n : ℕ } → FL n
78 fmax {zero} = f0
79 fmax {suc n} = fromℕ< a<sa :: fmax {n}
80
81 fmax< : { n : ℕ } → {x : FL n } → ¬ (fmax f< x )
82 fmax< {suc n} {x :: y} (f<n lt) = nat-≤> (fmax1 x) lt where
83 fmax1 : {n : ℕ } → (x : Fin (suc n)) → toℕ x ≤ toℕ (fromℕ< {n} a<sa)
84 fmax1 {zero} zero = z≤n
85 fmax1 {suc n} zero = z≤n
86 fmax1 {suc n} (suc x) = s≤s (fmax1 x)
87 fmax< {suc n} {x :: y} (f<t lt) = fmax< {n} {y} lt
88
89 fmax¬ : { n : ℕ } → {x : FL n } → ¬ ( x ≡ fmax ) → x f< fmax
90 fmax¬ {zero} {f0} ne = ⊥-elim ( ne refl )
91 fmax¬ {suc n} {x} ne with FLcmp x fmax
92 ... | tri< a ¬b ¬c = a
93 ... | tri≈ ¬a b ¬c = ⊥-elim ( ne b)
94 ... | tri> ¬a ¬b c = ⊥-elim (fmax< c)
95
96 x≤fmax : {n : ℕ } → {x : FL n} → x f≤ fmax
97 x≤fmax {n} {x} with FLcmp x fmax
98 ... | tri< a ¬b ¬c = case2 a
99 ... | tri≈ ¬a b ¬c = case1 b
100 ... | tri> ¬a ¬b c = ⊥-elim ( fmax< c )
101
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 fsuc1 : suc (toℕ x) < n
106 fsuc1 = Data.Nat.Properties.≤-trans (s≤s lt) ( s≤s ( toℕ≤pred[n] (fromℕ< a<sa)) )
107 fsuc (x :: y) (f<t lt) = x :: fsuc y lt
108
109 open import fin
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 FL1 : List ℕ → List ℕ
122 FL1 [] = []
123 FL1 (x ∷ y) = suc x ∷ FL1 y
124
125 FL→plist : {n : ℕ} → FL n → List ℕ
126 FL→plist {0} f0 = []
127 FL→plist {suc n} (zero :: y) = zero ∷ FL1 (FL→plist y)
128 FL→plist {suc n} (suc x :: y) with FL→plist y
129 ... | [] = zero ∷ []
130 ... | x1 ∷ t = suc x1 ∷ FL2 x t where
131 FL2 : {n : ℕ} → Fin n → List ℕ → List ℕ
132 FL2 zero y = zero ∷ FL1 y
133 FL2 (suc i) [] = zero ∷ []
134 FL2 (suc i) (x ∷ y) = suc x ∷ FL2 i y
135
136 tt0 = (# 2) :: (# 1) :: (# 0) :: zero :: f0
137 tt1 = FL→plist tt0
138
139 open _∧_
140
141 find-zero : {n i : ℕ} → List ℕ → i < n → Fin n ∧ List ℕ
142 find-zero [] i<n = record { proj1 = fromℕ< i<n ; proj2 = [] }
143 find-zero x (s≤s z≤n) = record { proj1 = fromℕ< (s≤s z≤n) ; proj2 = x }
144 find-zero (zero ∷ y) (s≤s (s≤s i<n)) = record { proj1 = fromℕ< (s≤s (s≤s i<n)) ; proj2 = y }
145 find-zero (suc x ∷ y) (s≤s (s≤s i<n)) with find-zero y (s≤s i<n)
146 ... | record { proj1 = i ; proj2 = y1 } = record { proj1 = suc i ; proj2 = suc x ∷ y1 }
147
148 plist→FL : {n : ℕ} → List ℕ → FL n -- wrong implementation
149 plist→FL {zero} [] = f0
150 plist→FL {suc n} [] = zero :: plist→FL {n} []
151 plist→FL {zero} x = f0
152 plist→FL {suc n} x with find-zero x a<sa
153 ... | record { proj1 = i ; proj2 = y } = i :: plist→FL y
154
155 tt2 = 2 ∷ 1 ∷ 0 ∷ 3 ∷ []
156 tt3 : FL 4
157 tt3 = plist→FL tt2
158 tt4 = FL→plist tt3
159 tt5 = plist→FL {4} (FL→plist tt0)
160
161 -- maybe FL→iso can be easier using this ...
162 -- FL→plist-iso : {n : ℕ} → (f : FL n ) → plist→FL (FL→plist f ) ≡ f
163 -- FL→plist-iso = {!!}
164 -- FL→plist-inject : {n : ℕ} → (f g : FL n ) → FL→plist f ≡ FL→plist g → f ≡ g
165 -- FL→plist-inject = {!!}
166
167 open import Relation.Binary as B hiding (Decidable; _⇔_)
168 open import Data.Sum.Base as Sum -- inj₁
169 open import Relation.Nary using (⌊_⌋)
170 open import Data.List.Fresh hiding ([_])
171
172 FList : (n : ℕ ) → Set
173 FList n = List# (FL n) ⌊ _f<?_ ⌋
174
175 fr1 : FList 3
176 fr1 =
177 ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) ∷#
178 ((# 0) :: ((# 1) :: ((# 0 ) :: f0))) ∷#
179 ((# 1) :: ((# 0) :: ((# 0 ) :: f0))) ∷#
180 ((# 2) :: ((# 0) :: ((# 0 ) :: f0))) ∷#
181 ((# 2) :: ((# 1) :: ((# 0 ) :: f0))) ∷#
182 []
183
184 open import Data.Product
185 open import Relation.Nullary.Decidable hiding (⌊_⌋)
186 -- open import Data.Bool hiding (_<_ ; _≤_ )
187 open import Data.Unit.Base using (⊤ ; tt)
188
189 -- fresh a [] = ⊤
190 -- fresh a (x ∷# xs) = R a x × fresh a xs
191
192 -- toWitness
193 -- ttf< : {n : ℕ } → {x a : FL n } → x f< a → T (isYes (x f<? a))
194 -- ttf< {n} {x} {a} x<a with x f<? a
195 -- ... | yes y = subst (λ k → Data.Bool.T k ) refl tt
196 -- ... | no nn = ⊥-elim ( nn x<a )
197
198 ttf : {n : ℕ } {x a : FL (n)} → x f< a → (y : FList (n)) → fresh (FL (n)) ⌊ _f<?_ ⌋ a y → fresh (FL (n)) ⌊ _f<?_ ⌋ x y
199 ttf _ [] fr = Level.lift tt
200 ttf {_} {x} {a} lt (cons a₁ y x1) (lift lt1 , x2 ) = (Level.lift (fromWitness (ttf1 lt1 lt ))) , ttf (ttf1 lt1 lt) y x1 where
201 ttf1 : True (a f<? a₁) → x f< a → x f< a₁
202 ttf1 t x<a = f<-trans x<a (toWitness t)
203
204 -- by https://gist.github.com/aristidb/1684202
205
206 FLinsert : {n : ℕ } → FL n → FList n → FList n
207 FLfresh : {n : ℕ } → (a x : FL (suc n) ) → (y : FList (suc n) ) → a f< x
208 → fresh (FL (suc n)) ⌊ _f<?_ ⌋ a y → fresh (FL (suc n)) ⌊ _f<?_ ⌋ a (FLinsert x y)
209 FLinsert {zero} f0 y = f0 ∷# []
210 FLinsert {suc n} x [] = x ∷# []
211 FLinsert {suc n} x (cons a y x₁) with FLcmp x a
212 ... | tri≈ ¬a b ¬c = cons a y x₁
213 ... | tri< lt ¬b ¬c = cons x ( cons a y x₁) ( Level.lift (fromWitness lt ) , ttf lt y x₁)
214 FLinsert {suc n} x (cons a [] x₁) | tri> ¬a ¬b lt = cons a ( x ∷# [] ) ( Level.lift (fromWitness lt) , Level.lift tt )
215 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 )
216
217 FLfresh a x [] a<x (Level.lift tt) = Level.lift (fromWitness a<x) , Level.lift tt
218 FLfresh a x (cons b [] (Level.lift tt)) a<x (Level.lift a<b , a<y) with FLcmp x b
219 ... | tri< x<b ¬b ¬c = Level.lift (fromWitness a<x) , Level.lift a<b , Level.lift tt
220 ... | tri≈ ¬a refl ¬c = Level.lift (fromWitness a<x) , Level.lift tt
221 ... | tri> ¬a ¬b b<x = Level.lift a<b , Level.lift (fromWitness (f<-trans (toWitness a<b) b<x)) , Level.lift tt
222 FLfresh a x (cons b y br) a<x (Level.lift a<b , a<y) with FLcmp x b
223 ... | tri< x<b ¬b ¬c = Level.lift (fromWitness a<x) , Level.lift a<b , ttf (toWitness a<b) y br
224 ... | tri≈ ¬a refl ¬c = Level.lift (fromWitness a<x) , ttf a<x y br
225 FLfresh a x (cons b [] br) a<x (Level.lift a<b , a<y) | tri> ¬a ¬b b<x =
226 Level.lift a<b , Level.lift (fromWitness (f<-trans (toWitness a<b) b<x)) , Level.lift tt
227 FLfresh a x (cons b (cons a₁ y x₁) br) a<x (Level.lift a<b , a<y) | tri> ¬a ¬b b<x =
228 Level.lift a<b , FLfresh a x (cons a₁ y x₁) a<x a<y
229
230 fr6 = FLinsert ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) fr1
231
232 open import Data.List.Fresh.Relation.Unary.Any
233 open import Data.List.Fresh.Relation.Unary.All
234
235 x∈FLins : {n : ℕ} → (x : FL n ) → (xs : FList n) → Any (x ≡_) (FLinsert x xs)
236 x∈FLins {zero} f0 [] = here refl
237 x∈FLins {zero} f0 (cons f0 xs x) = here refl
238 x∈FLins {suc n} x [] = here refl
239 x∈FLins {suc n} x (cons a xs x₁) with FLcmp x a
240 ... | tri< x<a ¬b ¬c = here refl
241 ... | tri≈ ¬a b ¬c = here b
242 x∈FLins {suc n} x (cons a [] x₁) | tri> ¬a ¬b a<x = there ( here refl )
243 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₂) )
244
245 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 )
246 nextAny (here x₁) = there (here x₁)
247 nextAny (there any) = there (there any)
248
249 insAny : {n : ℕ} → {x h : FL n } → (xs : FList n) → Any (x ≡_) xs → Any (x ≡_) (FLinsert h xs)
250 insAny {zero} {f0} {f0} (cons a L xr) (here refl) = here refl
251 insAny {zero} {f0} {f0} (cons a L xr) (there any) = insAny {zero} {f0} {f0} L any
252 insAny {suc n} {x} {h} (cons a L xr) any with FLcmp h a
253 ... | tri< x<a ¬b ¬c = there any
254 ... | tri≈ ¬a b ¬c = any
255 insAny {suc n} {a} {h} (cons a [] (Level.lift tt)) (here refl) | tri> ¬a ¬b c = here refl
256 insAny {suc n} {x} {h} (cons a (cons a₁ L x₁) xr) (here refl) | tri> ¬a ¬b c = here refl
257 insAny {suc n} {x} {h} (cons a (cons a₁ L x₁) xr) (there any) | tri> ¬a ¬b c = there (insAny (cons a₁ L x₁) any)
258
259 -- FLinsert membership
260
261 module FLMB { n : ℕ } where
262
263 FL-Setoid : Setoid Level.zero Level.zero
264 FL-Setoid = record { Carrier = FL n ; _≈_ = _≡_ ; isEquivalence = record { sym = sym ; refl = refl ; trans = trans }}
265
266 open import Data.List.Fresh.Membership.Setoid FL-Setoid
267
268 FLinsert-mb : (x : FL n ) → (xs : FList n) → x ∈ FLinsert x xs
269 FLinsert-mb x xs = x∈FLins {n} x xs
270
271