Mercurial > hg > Members > kono > Proof > galois

comparison FLutil.agda @ 182:eb94265d2a39 fresh-list

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Any based proof computation done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 26 Nov 2020 13:13:58 +0900
parents 7423f0fc124a
children b99927719b8e
comparison
equal deleted inserted replaced
181:7423f0fc124a 182:eb94265d2a39
229 229
230 -- open import Data.List.Fresh.Relation.Unary.All 230 -- open import Data.List.Fresh.Relation.Unary.All
231 -- fr7 = append ( ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) ∷# [] ) fr1 ( ({!!} , {!!} ) ∷ [] ) 231 -- fr7 = append ( ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) ∷# [] ) fr1 ( ({!!} , {!!} ) ∷ [] )
232 232
233 Flist : {n : ℕ } (i : ℕ) → i < suc n → FList n → FList n → FList (suc n) 233 Flist : {n : ℕ } (i : ℕ) → i < suc n → FList n → FList n → FList (suc n)
234 Ffresh0 : {n : ℕ } → (i<n : zero < suc n) → (a : FL n) → (x z : FList n )
235 → fresh (FL n) ⌊ _f<?_ ⌋ a x → fresh (FL (suc n)) ⌊ _f<?_ ⌋ (zero :: a) (Flist zero i<n x z)
236 Ffresh1 : {n : ℕ } → (i : ℕ) → (i<n : i < suc n) → 0 < i → (a : FL n) → (x z : FList n )
237 → (a₂ : FL (suc n)) (t : FList (suc n)) → fresh (FL (suc n)) ⌊ _f<?_ ⌋ a₂ t
238 → fresh (FL n) ⌊ _f<?_ ⌋ a x → fresh (FL (suc n)) ⌊ _f<?_ ⌋ (fromℕ< i<n :: a) t
239 Flist zero i<n [] _ = [] 234 Flist zero i<n [] _ = []
240 Flist zero i<n (cons a x xr) z = cons ( zero :: a ) (Flist zero i<n x z ) (Ffresh0 i<n a x z xr) 235 Flist zero i<n (a ∷# x ) z = FLinsert ( zero :: a ) (Flist zero i<n x z )
241 Flist (suc i) (s≤s i<n) [] z = Flist i (<-trans i<n a<sa) z z 236 Flist (suc i) (s≤s i<n) [] z = Flist i (<-trans i<n a<sa) z z
242 Flist (suc i) (s≤s i<n) (cons a [] xr) z = cons ((fromℕ< (s≤s i<n)) :: a) (Flist i (<-trans i<n a<sa) z z) {!!} 237 Flist (suc i) i<n (a ∷# x ) z = FLinsert ((fromℕ< i<n ) :: a ) (Flist (suc i) i<n x z )
243 Flist (suc i) (s≤s i<n) (cons a (cons a₁ x x₁) xr) z with Flist (suc i) (s≤s i<n) x z
244 ... | [] = cons ((fromℕ< (s≤s i<n)) :: a) [] (Level.lift tt)
245 ... | cons a₂ t x₂ = cons ((fromℕ< (s≤s i<n)) :: a) t (Ffresh1 (suc i) (s≤s i<n) 0<s a x z a₂ t x₂ ?)
246 Ffresh0 i<n a [] z xr = Level.lift tt
247 Ffresh0 i<n a (cons a₁ x x₁) z (lift a<a₁ , ar) = Fr0 , Ffresh0 i<n a x z ar where
248 Fr0 : ⌊ _f<?_ ⌋ (zero :: a) (zero :: a₁)
249 Fr0 = Level.lift (fromWitness (f<t (toWitness a<a₁)))
250 Ffresh1 = {!!}
251 238
252 ∀Flist : {n : ℕ } → FL n → FList n 239 ∀Flist : {n : ℕ } → FL n → FList n
253 ∀Flist {zero} f0 = f0 ∷# [] 240 ∀Flist {zero} f0 = f0 ∷# []
254 ∀Flist {suc n} (x :: y) = Flist n a<sa (∀Flist y) (∀Flist y) 241 ∀Flist {suc n} (x :: y) = Flist n a<sa (∀Flist y) (∀Flist y)
255 242
262 fr9 : FList 3 249 fr9 : FList 3
263 fr9 = ∀Flist fmax 250 fr9 = ∀Flist fmax
264 251
265 open import Data.List.Fresh.Relation.Unary.Any 252 open import Data.List.Fresh.Relation.Unary.Any
266 open import Data.List.Fresh.Relation.Unary.All 253 open import Data.List.Fresh.Relation.Unary.All
267
268 AnyFList : {n : ℕ } → (x : FL (suc n) ) → Any (x ≡_ ) (∀Flist fmax)
269 AnyFList {n} = {!!}
270 254
271 x∈FLins : {n : ℕ} → (x : FL n ) → (xs : FList n) → Any (x ≡_ ) (FLinsert x xs) 255 x∈FLins : {n : ℕ} → (x : FL n ) → (xs : FList n) → Any (x ≡_ ) (FLinsert x xs)
272 x∈FLins {zero} f0 [] = here refl 256 x∈FLins {zero} f0 [] = here refl
273 x∈FLins {zero} f0 (cons f0 xs x) = here refl 257 x∈FLins {zero} f0 (cons f0 xs x) = here refl
274 x∈FLins {suc n} x [] = here refl 258 x∈FLins {suc n} x [] = here refl
280 264
281 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 ) 265 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 )
282 nextAny (here x₁) = there (here x₁) 266 nextAny (here x₁) = there (here x₁)
283 nextAny (there any) = there (there any) 267 nextAny (there any) = there (there any)
284 268
285 record ∀FListP (n : ℕ ) : Set (Level.suc Level.zero) where 269 postulate
286 field 270 AnyFList : {n : ℕ } → (x : FL n ) → Any (x ≡_ ) (∀Flist fmax)
287 ∀list : FList n
288 x∈∀list : (x : FL n ) → Any (x ≡_ ) ∀list
289
290 open ∀FListP
291
292 -- tt1 : FList 3
293 -- tt1 = ∀FListP.∀list (∀FList 3)
294 271
295 -- FLinsert membership 272 -- FLinsert membership
296 273
297 module FLMB { n : ℕ } where 274 module FLMB { n : ℕ } where
298 275