Mercurial > hg > Members > kono > Proof > galois

changeset 180:d631469259f2

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 Thu, 26 Nov 2020 08:10:06 +0900
parents abc6acbd4452
children 7423f0fc124a
files FLutil.agda
diffstat 1 files changed, 18 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/FLutil.agda	Thu Nov 26 00:30:05 2020 +0900
+++ b/FLutil.agda	Thu Nov 26 08:10:06 2020 +0900
@@ -231,10 +231,25 @@
 -- fr7 = append ( ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) ∷# [] ) fr1 ( ({!!} , {!!} ) ∷ [] )
 
 Flist :  {n : ℕ } (i : ℕ) → i < suc n → FList n → FList n → FList (suc n)
+Ffresh0 : {n : ℕ } → (i<n : zero < suc n) → (a : FL n) → (x z : FList n )
+    →  fresh (FL n) ⌊ _f<?_ ⌋ a x →  fresh (FL (suc n)) ⌊ _f<?_ ⌋ (zero :: a) (Flist zero i<n x z)
+Ffresh1 : {n : ℕ } → (i : ℕ) → (i<n : i < suc n) → 0 < i → (a : FL n) → (x z : FList n )
+    →  fresh (FL n) ⌊ _f<?_ ⌋ a x →  fresh (FL (suc n)) ⌊ _f<?_ ⌋ (fromℕ< i<n :: a) (Flist i i<n x z)
 Flist zero i<n [] _ = []
-Flist zero i<n (a ∷# x ) z  = FLinsert ( zero :: a ) (Flist zero i<n x z )
-Flist (suc i) (s≤s i<n) [] z  = Flist i (Data.Nat.Properties.<-trans i<n a<sa) z z 
-Flist (suc i) i<n (a ∷# x ) z  = FLinsert ((fromℕ< i<n ) :: a ) (Flist (suc i) i<n x z )
+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)
+Flist (suc i) (s≤s i<n) [] z  = Flist i (<-trans i<n a<sa) z z 
+Flist (suc i) i<n (cons a x xr) z  = cons ((fromℕ< i<n ) :: a ) (Flist (suc i) i<n x z ) (Ffresh1 (suc i) i<n 0<s a x z xr)
+Ffresh0 i<n a [] z xr = Level.lift tt
+Ffresh0 i<n a (cons a₁ x x₁) z (lift a<a₁ , ar) = Fr0 , Ffresh0 i<n a x z ar where
+   Fr0 : ⌊ _f<?_ ⌋ (zero :: a) (zero :: a₁)
+   Fr0 = Level.lift (fromWitness (f<t (toWitness a<a₁)))
+Ffresh1 zero i<n () a [] z xr 
+Ffresh1 (suc i) (s≤s i<n) a _ [] z (Level.lift tt) with Flist i (<-trans i<n a<sa) z z 
+... | [] = Level.lift tt
+... | cons a₁ t x = {!!} , ttf {!!} t x
+Ffresh1 zero i<n () a (cons a₁ x xr) z (a<a₁ , ar) 
+Ffresh1 {n} (suc i) i<n _ a (cons a₁ x xr) z (a<a₁ , ar) with Ffresh1 {n} (suc i) i<n 0<s a x z ar  --  (suc (fromℕ< (≤-pred i<n)) :: a) (Flist (suc i) i<n x z)
+... | t = {!!} -- (suc (fromℕ< (≤-pred i<n)) :: a) (Flist (suc i) i<n (cons a₁ x xr) z)
 
 ∀Flist : {n : ℕ } → FL n → FList n
 ∀Flist {zero} f0 = f0 ∷# []