Mercurial > hg > Members > kono > Proof > galois

changeset 144:62364edeed3f

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 10:55:06 +0900
parents 029a7885fe57
children 0d59dcbbd0e1
files FL.agda
diffstat 1 files changed, 18 insertions(+), 9 deletions(-) [+]
line wrap: on
line diff
--- a/FL.agda	Fri Sep 11 09:38:23 2020 +0900
+++ b/FL.agda	Fri Sep 11 10:55:06 2020 +0900
@@ -166,6 +166,11 @@
        ttf1 : True (a f<? a₁) → x f< a  → x f< a₁
        ttf1 t x<a = f<-trans x<a (toWitness t)
 
+FLmin : {n : ℕ } → FList {n}  → FL n
+FLmin {zero} [] = {!!}
+FLmin {zero} (cons a x x₁) = {!!}
+FLmin {suc n} x = {!!}
+
 FLinsert : {n : ℕ } → FL n → FList {n}  → FList {n} 
 FLinsert {zero} f0 y = f0 ∷# []
 FLinsert {suc n} x [] = x ∷# []
@@ -176,14 +181,18 @@
 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 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 = {!!}
+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₂ t x₁ with total a₁ a₂
+... | inj₁ (case1 refl) = cons a (cons a₁ y x₂) (Level.lift a<a₁ , fr-ay)
+... | inj₁ (case2 lt2)  = cons a (cons a₂ t x₁) ( Level.lift (fromWitness a<a₂) , ttf a<a₂ t  x₁) where
+     a<a₂ : a f< a₂
+     a<a₂ = f<-trans (toWitness a<a₁) lt2
+... | inj₂ (case1 refl) = cons a (cons a₁ y x₂) (Level.lift a<a₁ , fr-ay)
+... | inj₂ (case2 lt2)  = cons a (cons x (cons a₁ y x₂) ttf2) ( Level.lift (fromWitness lt) , ttf3 ) where
+    ttf2 : fresh (FL (suc n)) ⌊ _f<?_ ⌋ x (cons a₁ y x₂) --  a f< x ,  a₂ f< a₁, a < a₁ → x < a₁ , x f< a₂
+    ttf2 = {!!} ,  ttf (f<-trans {!!} lt2 ) y  x₂
+    ttf3 : fresh (FL (suc n)) ⌊ _f<?_ ⌋ a (cons a₁ y x₂)
+    ttf3 = Level.lift a<a₁ , fr-ay
 
 fr6 = FLinsert ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) fr1