Mercurial > hg > Members > kono > Proof > galois

changeset 143:029a7885fe57

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 Fri, 11 Sep 2020 09:38:23 +0900
parents 435159e2897a
children 62364edeed3f
files FL.agda
diffstat 1 files changed, 13 insertions(+), 9 deletions(-) [+]
line wrap: on
line diff
--- a/FL.agda	Thu Sep 10 20:55:19 2020 +0900
+++ b/FL.agda	Fri Sep 11 09:38:23 2020 +0900
@@ -160,9 +160,9 @@
 -- ... | 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 
+ttf : {n : ℕ } {x 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 _ [] fr = Level.lift tt
+ttf {_} {x} {a} lt (cons a₁ y x1) (lift lt1 , x2 ) = (Level.lift (fromWitness (ttf1 lt1 lt ))) , ttf (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)
 
@@ -171,15 +171,19 @@
 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 x lt y  x₁) 
+FLinsert {suc n} x (cons a y x₁) | inj₁ (case2 lt) = cons x ( cons a y x₁) ( Level.lift (fromWitness lt ) , ttf 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₂) (lift a<a₁ , fr-ay)) | inj₂ (case2 lt) with FLinsert x (cons a₁ y x₂)
-... | [] = cons a (cons x ( cons a₁ [] (Level.lift tt) ) {!!} ) {!!} 
-... | cons a₂ t x₁ = cons a ( cons a₂ t x₁) ( Level.lift (fromWitness (ttf2 {!!} {!!})) , ( ttf a₂ a (ttf2 {!!} {!!} ) t x₁ )) where
-    ttf2 :  fresh (FL (suc n)) ⌊ _f<?_ ⌋ a y →  fresh (FL (suc n)) ⌊ _f<?_ ⌋ a₂ t → a f< a₂
-    ttf2 = {!!}
+FLinsert {suc n} x (cons a (cons a₁ y x₂) (lift a<a₁ , fr-ay)) | inj₂ (case2 lt) with FLcmp x a₁ | FLinsert x  (cons a₁ y x₂)
+... | _ | [] = []
+... | tri< x<a₁ ¬b ¬c | cons a₂ t x₁ = cons a (cons a₂ t x₁) ( Level.lift (fromWitness ttf2 )  , (ttf ttf2 t x₁)) where -- a₂ ≡ x
+   ttf2 : a f< a₂
+   ttf2 = {!!}
+... | tri≈ ¬a b ¬c    | cons a₂ t x₁ = cons a (cons a₁ y x₂) (Level.lift a<a₁ , fr-ay)
+... | tri> ¬a ¬b a₁<x | cons a₂ t x₁ = cons a (cons a₂ t x₁) ( Level.lift (fromWitness ttf3 )  , (ttf ttf3 t x₁)) where -- a₂ < x
+   ttf3 : a f< a₂
+   ttf3 = {!!}
 
 fr6 = FLinsert ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) fr1