# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1606175028 -32400
# Node ID 32e2097f570288b68c071ab627a51379ee860b23
# Parent  825b3237169c8d799952a21399ce5b5d4468b283
AnyFList

diff -r 825b3237169c -r 32e2097f5702 FLutil.agda
--- a/FLutil.agda	Mon Nov 23 19:24:12 2020 +0900
+++ b/FLutil.agda	Tue Nov 24 08:43:48 2020 +0900
@@ -4,16 +4,16 @@
 open import Level hiding ( suc ; zero )
 open import Data.Fin hiding ( _<_  ; _≤_ ; _-_ ; _+_ ; _≟_)
 open import Data.Fin.Properties hiding ( <-trans ; ≤-refl ; ≤-trans ; ≤-irrelevant ; _≟_ ) renaming ( <-cmp to <-fcmp )
-open import Data.Fin.Permutation
+open import Data.Fin.Permutation  -- hiding ([_,_])
 open import Data.Nat -- using (ℕ; suc; zero; s≤s ; z≤n )
 open import Data.Nat.Properties
-open import Relation.Binary.PropositionalEquality 
+open import Relation.Binary.PropositionalEquality hiding ( [_] )
 open import Data.List using (List; []; _∷_ ; length ; _++_ ; tail ) renaming (reverse to rev )
 open import Data.Product
 open import Relation.Nullary
 open import Data.Empty
 open import  Relation.Binary.Core
-open import  Relation.Binary.Definitions
+open import  Relation.Binary.Definitions 
 open import logic
 open import nat
 
@@ -132,7 +132,7 @@
 open import Relation.Binary as B hiding (Decidable; _⇔_)
 open import Data.Sum.Base as Sum --  inj₁
 open import Relation.Nary using (⌊_⌋)
-open import Data.List.Fresh
+open import Data.List.Fresh hiding ([_])
 
 FList : (n : ℕ ) → Set
 FList n = List# (FL n) ⌊ _f<?_ ⌋
@@ -148,7 +148,7 @@
 
 open import Data.Product
 open import Relation.Nullary.Decidable hiding (⌊_⌋)
-open import Data.Bool hiding (_<_ ; _≤_ )
+-- open import Data.Bool hiding (_<_ ; _≤_ )
 open import Data.Unit.Base using (⊤ ; tt)
 
 --  fresh a []        = ⊤
@@ -210,6 +210,9 @@
 fr8 : FList 4
 fr8 = ∀Flist fmax
 
+fr9 : FList 3
+fr9 = ∀Flist fmax
+
 open import Data.List.Fresh.Relation.Unary.Any 
 open import Data.List.Fresh.Relation.Unary.All 
 
@@ -230,43 +233,22 @@
     ∀list :   FList n 
     x∈∀list : (x : FL n ) → Any (x ≡_ ) ∀list 
 
-∀FList : (n : ℕ )  → ∀FListP n
-∀FList zero = record { ∀list = f0 ∷# [] ; x∈∀list = af1 } where
-    af1 : (x : FL zero) → Any  (_≡_ x) (cons f0 [] (Level.lift tt))
-    af1 f0 = here refl
-∀FList (suc n) with ∀FListP.∀list (∀FList n) | ∀FListP.x∈∀list (∀FList n) fmax
-∀FList (suc n) | [] | ()
-∀FList (suc n) | cons A X FR | _ = record { ∀list = af4 n ≤-refl A X FR
-       ; x∈∀list = λ x → {!!} } where
-    af0 : ∀FListP n
-    af0 = ∀FList n
-    af3 : (w : Fin (suc n)) (x y : FL n) → Level.Lift Level.zero (True (x f<? y )) → (w :: x ) f< (w :: y )
-    af3 w x y (Level.lift z) with x f<? y
-    ... | yes x<y = f<t x<y
-    af4  : (i : ℕ) → (i<n : i < suc n) 
-        → (a : FL n) → (y : FList n) → fresh (FL n) ⌊ _f<?_ ⌋ a y  
-        →  FList (suc n)
-    af4r  : (i : ℕ) → (i<n : i < suc n) 
-        → (a a₁ : FL n) → a f< a₁ → (y : FList n) → (fr : fresh (FL n) ⌊ _f<?_ ⌋ a₁ y )
-        →  fresh (FL (suc n)) ⌊ _f<?_ ⌋ (fromℕ< i<n :: a) (af4 i i<n a₁ y fr)
-    af4 zero i<n a [] fr = cons (fromℕ< i<n :: a) [] (Level.lift tt)
-    af4 zero i<n a (cons a₁ y x) (lift p , fr) =
-        cons (fromℕ< i<n :: a) (af4 zero i<n a₁ y x ) (af4r zero i<n a a₁ (toWitness p) y x)
-    af4 (suc i) (s≤s i<n) a' [] fr' = af4 i (<-trans i<n a<sa) A X FR
-    af4 (suc i) (s≤s i<n) a (cons a₁ y x) (lift p , fr) = 
-        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)
-    af4r zero i<n a a₁ a<a₁ [] fr = Level.lift (fromWitness (f<t a<a₁)) , Level.lift tt
-    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
-       af41 : a f< a₂
-       af41 = f<-trans a<a₁ (toWitness p)
-    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
-       af43 : (fromℕ< (s≤s i<n) :: a') f< (fromℕ< (<-trans i<n a<sa) :: a')
-       af43 = {!!}
-       af44 : a' f< A
-       af44 = {!!}
-    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
-       af42 : a f< a₂
-       af42 = f<-trans a<a₁ (toWitness p)
+open ∀FListP
+
+AnyFList : (n : ℕ )  → (x : FL n ) →  Any (x ≡_ ) (∀Flist fmax)
+AnyFList n x = AnyFlist0 fmax x where
+   AnyFlist1 :  {n : ℕ } (i : ℕ) → (i<n : i < suc n ) → (x : Fin (suc n)) → toℕ x < suc i → (y : FL n) → (L L1 : FList n )
+       → Any (y ≡_ ) L  →  Any ((x :: y ) ≡_ ) (Flist1 i i<n L L1 )
+   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 )
+   AnyFlist1 zero i<n (suc x) (s≤s ()) y (cons y L ar) L1 (here refl)
+   AnyFlist1 (suc i) i<n x x<i y (cons y L ar) L1 (here refl) = ?
+   AnyFlist1 i i<n x x<i y (cons a L ar) L1 (there any) = {!!}
+   AnyFlist0 : {n : ℕ } → (y x : FL n ) →  Any (x ≡_ ) (∀Flist y)
+   AnyFlist0 {zero} f0 f0 = here refl
+   AnyFlist0 {suc n} (_ :: z) (x :: y) = AnyFlist1 n a<sa x fin<n y (∀Flist z) (∀Flist z) (AnyFlist0 z y) where
+
+-- tt1 : FList 3
+-- tt1 = ∀FListP.∀list (∀FList 3)
 
 -- FLinsert membership