Mercurial > hg > Members > kono > Proof > galois

changeset 233:ff1e5a6e42da

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 09 Dec 2020 07:03:11 +0900
parents 8f7c09ff96bd
children 3c3619b196dc
files FLComm.agda
diffstat 1 files changed, 22 insertions(+), 26 deletions(-) [+]
line wrap: on
line diff
--- a/FLComm.agda	Tue Dec 08 21:21:08 2020 +0900
+++ b/FLComm.agda	Wed Dec 09 07:03:11 2020 +0900
@@ -47,39 +47,35 @@
 -- Flist {suc n} (x :: y)  = Flist n a<sa (∀Flist y) (∀Flist y)   
 
 -------------
---    (suc n :: (fromℕ< a<sa  :: p))   (n ::  ) ....           (zero :: (fromℕ< a<sa :: p))
---    (suc n :: (n :: p)
---           :                     anyFL
---    (suc n :: (zero :: p)
+--    # 0 : # 0 : .... # 0 : # 0 :: f0
+--    # 0 : # 0 : .... # 1 : # 0 :: f0
+--   
+--    # sn: # 0 : .... # 0 : # 0 :: f0
+--   
+--    # sn: # n : .... # 1 : # 0 :: f0
+--  
 
 -- all FL
-record AnyFL {i : ℕ} (i<n : i < suc n) (y : FL n) : Set where
+record AnyFL (n : ℕ) {i : ℕ} (i<n : i < suc n) (y : FL n) : Set where
    field
-     anyList : FList (suc (suc n))
-     anyP : {x : FL (suc n)} → {j : ℕ}  → x f≤ (fromℕ< a<sa :: y) → (j≤i : j ≤ i)  → Any (fromℕ< (<-trans (s≤s j≤i) (s≤s i<n)) :: x ≡_ ) anyList 
+     anyList : FList (suc n)
+     anyP : (x : FL (suc n)) → Any (x ≡_ ) anyList 
 
 open import fin
 open AnyFL
 
-{-# TERMINATING #-}
-anyFL :  AnyFL a<sa fmax
-anyFL  = record { anyList = allListF a<sa ; anyP = {!!} } where 
-    allListFL : (x : FL (suc n)) → FList (suc (suc n))
-    allListFL (zero :: y) = {!!}
-    allListFL (suc x :: y) = FLinsert {!!} (allListFL (fin+1 x :: y))
-    allListF : {i : ℕ} → (i<n : i < suc n) → FList (suc (suc n))
-    allListF (s≤s z≤n) = allListFL fmax
-    allListF (s≤s (s≤s i<n)) = FLinsert {!!} (allListF  (<-trans (s≤s i<n) a<sa)) 
---  allListFL : (P1 : FL n) → FList (suc n)
---  allListFL f0 = []
---  allListFL (zero :: y) = cons (fromℕ< a<sa :: zero :: y) [] (Level.lift tt)
---  allListFL (suc x :: y) = FLinsert (fromℕ< a<sa :: suc x :: y) (allListFL (fin+1 x :: y)) 
---  allListF : {i : ℕ} → (Q1 : i < suc n) → FList (suc n)
---  allListF (s≤s z≤n) = allListFL fmax
---  allListF (s≤s (s≤s i<n)) = FLinsert (fin+1 (fromℕ< (s≤s i<n)) :: fmax) (allListF  (<-trans (s≤s i<n) a<sa)) 
---  anyFLP :  {i : ℕ } → (i<n : i < suc n) → (x : FL n) → Any (_≡_ (fromℕ< a<sa :: x)) (FLinsert (fromℕ< i<n :: fmax) (allListF i<n))
---  anyFLP (s≤s z≤n) x = {!!}
---  anyFLP (s≤s (s≤s i<n)) x = {!!}
+-- {-# TERMINATING #-}
+anyFL :  (n : ℕ) → AnyFL n a<sa fmax
+anyFL zero = record { anyList = (zero :: f0) ∷# [] ; anyP = anyFL0 } where 
+    anyFL0 : (x : FL 1) → Any (_≡_ x) (cons (zero :: f0) [] (Level.lift tt))
+    anyFL0 (zero :: f0) = here refl
+anyFL (suc n)  = record { anyList = allListF a<sa []; anyP = {!!} } where 
+    allListFL : (x : Fin (suc (suc n))) → FList (suc n) → FList (suc (suc n)) → FList (suc (suc n))
+    allListFL _ [] y = y
+    allListFL x (cons y L yr) z = cons (x :: y) (allListFL x L z) {!!}
+    allListF : {i : ℕ} → (i<n : i < suc (suc n)) → FList (suc (suc n)) → FList (suc (suc n))
+    allListF (s≤s z≤n) z = z
+    allListF (s≤s (s≤s i<n)) z = allListFL (fromℕ< {!!}) (anyList (anyFL n)) (allListF {!!} z)
 
 tl3 : (FL n) → ( z : FList n) → FList n → FList n
 tl3 h [] w = w