Mercurial > hg > Members > kono > Proof > galois

changeset 141:35c0b6878863

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, 10 Sep 2020 20:25:31 +0900
parents 6006d2beaf24
children 435159e2897a
files FL.agda
diffstat 1 files changed, 11 insertions(+), 9 deletions(-) [+]
line wrap: on
line diff
--- a/FL.agda	Wed Sep 09 18:45:51 2020 +0900
+++ b/FL.agda	Thu Sep 10 20:25:31 2020 +0900
@@ -160,23 +160,25 @@
 -- ... | yes y = subst (λ k → Data.Bool.T k ) refl tt
 -- ... | no nn = ⊥-elim ( nn x<a )
 
+ttf : {n : ℕ } (a x : FL (suc n)) → x f< a → (y : FList {suc n}) →  fresh (FL (suc n)) ⌊ _f<?_ ⌋  a y  → fresh (FL (suc n)) ⌊ _f<?_ ⌋  x y
+ttf a x _ [] fr = Level.lift tt
+ttf a x lt (cons a₁ y x1) (lift lt1 , x2 ) = (Level.lift (fromWitness (ttf1 lt1 lt ))) , ttf a₁ x (ttf1 lt1 lt) y x1 where 
+       ttf1 : True (a f<? a₁) → x f< a  → x f< a₁
+       ttf1 t x<a = f<-trans x<a (toWitness t)
+
 FLinsert : {n : ℕ } → FL n → FList {n}  → FList {n} 
 FLinsert {zero} f0 y = f0 ∷# []
 FLinsert {suc n} x [] = x ∷# []
 FLinsert {suc n} x (cons a y x₁) with total x a
 ... | inj₁ (case1 eq) = cons a y x₁
-FLinsert {suc n} x (cons a y x₁) | inj₁ (case2 lt) = cons x ( cons a y x₁) ( Level.lift (fromWitness lt ) , ttf a lt y  x₁) where
-   ttf : (a : FL (suc n)) → x f< a → (y : FList {suc n}) →  fresh (FL (suc n)) ⌊ _f<?_ ⌋  a y  → fresh (FL (suc n)) ⌊ _f<?_ ⌋  x y
-   ttf a _ [] fr = Level.lift tt
-   ttf a lt (cons a₁ y x1) (lift lt1 , x2 ) = (Level.lift (fromWitness (ttf1 lt1 lt ))) , ttf a₁ (ttf1 lt1 lt) y x1 where 
-       ttf1 : True (a f<? a₁) → x f< a  → x f< a₁
-       ttf1 t x<a = f<-trans x<a (toWitness t)
+FLinsert {suc n} x (cons a y x₁) | inj₁ (case2 lt) = cons x ( cons a y x₁) ( Level.lift (fromWitness lt ) , ttf a x lt y  x₁) 
 ... | inj₂ (case1 eq) = cons a y x₁
 FLinsert {suc n} x (cons a [] x₁) | inj₂ (case2 lt) with FLinsert x [] | inspect ( FLinsert x ) []
 ... | [] | ()
 ... | cons a₁ t x₂ | e = cons a ( x  ∷# []  ) ( Level.lift (fromWitness lt) , Level.lift tt )
-FLinsert {suc n} x (cons a (cons a₁ y x₂) x₁) | inj₂ (case2 lt) with FLinsert x [] | inspect ( FLinsert x ) []
-... | [] | ()
-... | cons a₂ t x₃ | record { eq = eq1 }  = cons a ( cons a₂ t x₃) ( Level.lift (fromWitness {!!}), {!!} )
+FLinsert {suc n} x (cons a (cons a₁ y x₂) (lift a<a₁ , fr-ay)) | inj₂ (case2 lt) = ttf2 a a₁ x (FLinsert x (cons a₁ y x₂)) where
+    ttf2 : {n : ℕ } → (a a₁ x : FL (suc n))  → ( y : FList {suc n} ) → FList {suc n}
+    ttf2 a a₁ x [] = cons a (cons x ( cons a₁ [] (Level.lift tt) ) {!!} ) {!!} 
+    ttf2 a a₁ x (cons a₂ t x₁) = cons a ( cons a₂ t x₁) ( {!!} , ( ttf x a ? t {!!}) )
 
 fr6 = FLinsert ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) fr1