Mercurial > hg > Members > kono > Proof > galois

comparison FLutil.agda @ 172:32e2097f5702

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
AnyFList
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 24 Nov 2020 08:43:48 +0900
parents 825b3237169c
children 715093a948be
comparison
equal deleted inserted replaced
171:825b3237169c 172:32e2097f5702
2 module FLutil where 2 module FLutil where
3 3
4 open import Level hiding ( suc ; zero ) 4 open import Level hiding ( suc ; zero )
5 open import Data.Fin hiding ( _<_ ; _≤_ ; _-_ ; _+_ ; _≟_) 5 open import Data.Fin hiding ( _<_ ; _≤_ ; _-_ ; _+_ ; _≟_)
6 open import Data.Fin.Properties hiding ( <-trans ; ≤-refl ; ≤-trans ; ≤-irrelevant ; _≟_ ) renaming ( <-cmp to <-fcmp ) 6 open import Data.Fin.Properties hiding ( <-trans ; ≤-refl ; ≤-trans ; ≤-irrelevant ; _≟_ ) renaming ( <-cmp to <-fcmp )
7 open import Data.Fin.Permutation 7 open import Data.Fin.Permutation -- hiding ([_,_])
8 open import Data.Nat -- using (ℕ; suc; zero; s≤s ; z≤n ) 8 open import Data.Nat -- using (ℕ; suc; zero; s≤s ; z≤n )
9 open import Data.Nat.Properties 9 open import Data.Nat.Properties
10 open import Relation.Binary.PropositionalEquality 10 open import Relation.Binary.PropositionalEquality hiding ( [_] )
11 open import Data.List using (List; []; _∷_ ; length ; _++_ ; tail ) renaming (reverse to rev ) 11 open import Data.List using (List; []; _∷_ ; length ; _++_ ; tail ) renaming (reverse to rev )
12 open import Data.Product 12 open import Data.Product
13 open import Relation.Nullary 13 open import Relation.Nullary
14 open import Data.Empty 14 open import Data.Empty
15 open import Relation.Binary.Core 15 open import Relation.Binary.Core
16 open import Relation.Binary.Definitions 16 open import Relation.Binary.Definitions
17 open import logic 17 open import logic
18 open import nat 18 open import nat
19 19
20 infixr 100 _::_ 20 infixr 100 _::_
21 21
130 130
131 131
132 open import Relation.Binary as B hiding (Decidable; _⇔_) 132 open import Relation.Binary as B hiding (Decidable; _⇔_)
133 open import Data.Sum.Base as Sum -- inj₁ 133 open import Data.Sum.Base as Sum -- inj₁
134 open import Relation.Nary using (⌊_⌋) 134 open import Relation.Nary using (⌊_⌋)
135 open import Data.List.Fresh 135 open import Data.List.Fresh hiding ([_])
136 136
137 FList : (n : ℕ ) → Set 137 FList : (n : ℕ ) → Set
138 FList n = List# (FL n) ⌊ _f<?_ ⌋ 138 FList n = List# (FL n) ⌊ _f<?_ ⌋
139 139
140 fr1 : FList 3 140 fr1 : FList 3
146 ((# 2) :: ((# 1) :: ((# 0 ) :: f0))) ∷# 146 ((# 2) :: ((# 1) :: ((# 0 ) :: f0))) ∷#
147 [] 147 []
148 148
149 open import Data.Product 149 open import Data.Product
150 open import Relation.Nullary.Decidable hiding (⌊_⌋) 150 open import Relation.Nullary.Decidable hiding (⌊_⌋)
151 open import Data.Bool hiding (_<_ ; _≤_ ) 151 -- open import Data.Bool hiding (_<_ ; _≤_ )
152 open import Data.Unit.Base using (⊤ ; tt) 152 open import Data.Unit.Base using (⊤ ; tt)
153 153
154 -- fresh a [] = ⊤ 154 -- fresh a [] = ⊤
155 -- fresh a (x ∷# xs) = R a x × fresh a xs 155 -- fresh a (x ∷# xs) = R a x × fresh a xs
156 156
208 ∀Flist {suc n} (x :: y) = Flist1 n a<sa (∀Flist y) (∀Flist y) 208 ∀Flist {suc n} (x :: y) = Flist1 n a<sa (∀Flist y) (∀Flist y)
209 209
210 fr8 : FList 4 210 fr8 : FList 4
211 fr8 = ∀Flist fmax 211 fr8 = ∀Flist fmax
212 212
213 fr9 : FList 3
214 fr9 = ∀Flist fmax
215
213 open import Data.List.Fresh.Relation.Unary.Any 216 open import Data.List.Fresh.Relation.Unary.Any
214 open import Data.List.Fresh.Relation.Unary.All 217 open import Data.List.Fresh.Relation.Unary.All
215 218
216 x∈FLins : {n : ℕ} → (x : FL n ) → (xs : FList n) → Any (x ≡_ ) (FLinsert x xs) 219 x∈FLins : {n : ℕ} → (x : FL n ) → (xs : FList n) → Any (x ≡_ ) (FLinsert x xs)
217 x∈FLins {zero} f0 [] = here refl 220 x∈FLins {zero} f0 [] = here refl
228 record ∀FListP (n : ℕ ) : Set (Level.suc Level.zero) where 231 record ∀FListP (n : ℕ ) : Set (Level.suc Level.zero) where
229 field 232 field
230 ∀list : FList n 233 ∀list : FList n
231 x∈∀list : (x : FL n ) → Any (x ≡_ ) ∀list 234 x∈∀list : (x : FL n ) → Any (x ≡_ ) ∀list
232 235
233 ∀FList : (n : ℕ ) → ∀FListP n 236 open ∀FListP
234 ∀FList zero = record { ∀list = f0 ∷# [] ; x∈∀list = af1 } where 237
235 af1 : (x : FL zero) → Any (_≡_ x) (cons f0 [] (Level.lift tt)) 238 AnyFList : (n : ℕ ) → (x : FL n ) → Any (x ≡_ ) (∀Flist fmax)
236 af1 f0 = here refl 239 AnyFList n x = AnyFlist0 fmax x where
237 ∀FList (suc n) with ∀FListP.∀list (∀FList n) | ∀FListP.x∈∀list (∀FList n) fmax 240 AnyFlist1 : {n : ℕ } (i : ℕ) → (i<n : i < suc n ) → (x : Fin (suc n)) → toℕ x < suc i → (y : FL n) → (L L1 : FList n )
238 ∀FList (suc n) | [] | () 241 → Any (y ≡_ ) L → Any ((x :: y ) ≡_ ) (Flist1 i i<n L L1 )
239 ∀FList (suc n) | cons A X FR | _ = record { ∀list = af4 n ≤-refl A X FR 242 AnyFlist1 zero i<n zero x<i y (cons y L ar) L1 (here refl) = x∈FLins (zero :: y) (Flist1 zero i<n L L1 )
240 ; x∈∀list = λ x → {!!} } where 243 AnyFlist1 zero i<n (suc x) (s≤s ()) y (cons y L ar) L1 (here refl)
241 af0 : ∀FListP n 244 AnyFlist1 (suc i) i<n x x<i y (cons y L ar) L1 (here refl) = ?
242 af0 = ∀FList n 245 AnyFlist1 i i<n x x<i y (cons a L ar) L1 (there any) = {!!}
243 af3 : (w : Fin (suc n)) (x y : FL n) → Level.Lift Level.zero (True (x f<? y )) → (w :: x ) f< (w :: y ) 246 AnyFlist0 : {n : ℕ } → (y x : FL n ) → Any (x ≡_ ) (∀Flist y)
244 af3 w x y (Level.lift z) with x f<? y 247 AnyFlist0 {zero} f0 f0 = here refl
245 ... | yes x<y = f<t x<y 248 AnyFlist0 {suc n} (_ :: z) (x :: y) = AnyFlist1 n a<sa x fin<n y (∀Flist z) (∀Flist z) (AnyFlist0 z y) where
246 af4 : (i : ℕ) → (i<n : i < suc n) 249
247 → (a : FL n) → (y : FList n) → fresh (FL n) ⌊ _f<?_ ⌋ a y 250 -- tt1 : FList 3
248 → FList (suc n) 251 -- tt1 = ∀FListP.∀list (∀FList 3)
249 af4r : (i : ℕ) → (i<n : i < suc n)
250 → (a a₁ : FL n) → a f< a₁ → (y : FList n) → (fr : fresh (FL n) ⌊ _f<?_ ⌋ a₁ y )
251 → fresh (FL (suc n)) ⌊ _f<?_ ⌋ (fromℕ< i<n :: a) (af4 i i<n a₁ y fr)
252 af4 zero i<n a [] fr = cons (fromℕ< i<n :: a) [] (Level.lift tt)
253 af4 zero i<n a (cons a₁ y x) (lift p , fr) =
254 cons (fromℕ< i<n :: a) (af4 zero i<n a₁ y x ) (af4r zero i<n a a₁ (toWitness p) y x)
255 af4 (suc i) (s≤s i<n) a' [] fr' = af4 i (<-trans i<n a<sa) A X FR
256 af4 (suc i) (s≤s i<n) a (cons a₁ y x) (lift p , fr) =
257 cons (fromℕ< (s≤s i<n) :: a) ( af4 (suc i) (s≤s i<n) a₁ y x ) (af4r (suc i) (s≤s i<n) a a₁ (toWitness p) y x)
258 af4r zero i<n a a₁ a<a₁ [] fr = Level.lift (fromWitness (f<t a<a₁)) , Level.lift tt
259 af4r zero i<n a a₁ a<a₁ (cons a₂ y x) (lift p , _) = Level.lift (fromWitness (f<t a<a₁)) , af4r zero i<n a a₂ af41 y x where
260 af41 : a f< a₂
261 af41 = f<-trans a<a₁ (toWitness p)
262 af4r (suc i) (s≤s i<n) a' a₁ a<a₁ [] (lift tt) = ttf af43 (af4 i (<-trans i<n a<sa) A X FR) (af4r i (<-trans i<n a<sa) a' A af44 X FR) where
263 af43 : (fromℕ< (s≤s i<n) :: a') f< (fromℕ< (<-trans i<n a<sa) :: a')
264 af43 = {!!}
265 af44 : a' f< A
266 af44 = {!!}
267 af4r (suc i) (s≤s i<n) a a₁ a<a₁ (cons a₂ y x) (lift p , _) = Level.lift (fromWitness (f<t a<a₁)) , af4r (suc i) (s≤s i<n) a a₂ af42 y x where
268 af42 : a f< a₂
269 af42 = f<-trans a<a₁ (toWitness p)
270 252
271 -- FLinsert membership 253 -- FLinsert membership
272 254
273 module FLMB { n : ℕ } where 255 module FLMB { n : ℕ } where
274 256