--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/FL.agda	Tue Sep 08 11:07:27 2020 +0900
@@ -0,0 +1,161 @@
+module FL where
+
+open import Level hiding ( suc ; zero )
+open import Data.Fin hiding ( _<_  ; _≤_ ; _-_ ; _+_ ; _≟_)
+open import Data.Fin.Properties hiding ( <-trans ; ≤-trans ; ≤-irrelevant ; _≟_ ) renaming ( <-cmp to <-fcmp )
+open import Data.Fin.Permutation
+open import Data.Nat -- using (ℕ; suc; zero; s≤s ; z≤n )
+open import Relation.Binary.PropositionalEquality 
+open import Data.List using (List; []; _∷_ ; length ; _++_ ; head ; tail ) renaming (reverse to rev )
+open import Data.Product
+open import Relation.Nullary
+open import Data.Empty
+open import  Relation.Binary.Core
+open import  Relation.Binary.Definitions
+
+infixr  100 _::_
+
+data  FL : (n : ℕ )→ Set where
+   f0 :  FL 0 
+   _::_ :  { n : ℕ } → Fin (suc n ) → FL n → FL (suc n)
+
+data _f<_  : {n : ℕ } (x : FL n ) (y : FL n)  → Set  where
+   f<n : {m : ℕ } {xn yn : Fin (suc m) } {xt yt : FL m} → xn Data.Fin.< yn →   (xn :: xt) f< ( yn :: yt )
+   f<t : {m : ℕ } {xn : Fin (suc m) } {xt yt : FL m} → xt f< yt →   (xn :: xt) f< ( xn :: yt )
+
+FLeq : {n : ℕ } {xn yn : Fin (suc n)} {x : FL n } {y : FL n}  → xn :: x ≡ yn :: y → ( xn ≡ yn )  × (x ≡ y )
+FLeq refl = refl , refl 
+
+nat-<> : { x y : ℕ } → x < y → y < x → ⊥
+nat-<>  (s≤s x<y) (s≤s y<x) = nat-<> x<y y<x
+nat-<≡ : { x : ℕ } → x < x → ⊥
+nat-<≡  (s≤s lt) = nat-<≡ lt
+nat-≡< : { x y : ℕ } → x ≡ y → x < y → ⊥
+nat-≡< refl lt = nat-<≡ lt
+
+f-<> :  {n : ℕ } {x : FL n } {y : FL n}  → x f< y → y f< x → ⊥
+f-<> (f<n x) (f<n x₁) = nat-<> x x₁
+f-<> (f<n x) (f<t lt2) = nat-≡< refl x
+f-<> (f<t lt) (f<n x) = nat-≡< refl x
+f-<> (f<t lt) (f<t lt2) = f-<> lt lt2
+
+f-≡< :  {n : ℕ } {x : FL n } {y : FL n}  → x ≡ y → y f< x → ⊥
+f-≡< refl (f<n x) = nat-≡< refl x
+f-≡< refl (f<t lt) = f-≡< refl lt 
+
+FLcmp : {n : ℕ } → Trichotomous {Level.zero} {FL n}  _≡_  _f<_
+FLcmp f0 f0 = tri≈ (λ ()) refl (λ ())
+FLcmp (xn :: xt) (yn :: yt) with <-fcmp xn yn
+... | tri< a ¬b ¬c = tri< (f<n a) (λ eq → nat-≡< (cong toℕ (proj₁ (FLeq eq)) ) a) (λ lt  → f-<> lt (f<n a) )
+... | tri> ¬a ¬b c = tri> (λ lt  → f-<> lt (f<n c) ) (λ eq → nat-≡< (cong toℕ (sym (proj₁ (FLeq eq)) )) c) (f<n c)
+... | tri≈ ¬a refl ¬c with FLcmp xt yt
+... | tri< a ¬b ¬c₁ = tri< (f<t a) (λ eq → ¬b (proj₂ (FLeq eq) )) (λ lt  → f-<> lt (f<t a) )
+... | tri≈ ¬a₁ refl ¬c₁ = tri≈ (λ lt → f-≡< refl lt )  refl (λ lt → f-≡< refl lt )
+... | tri> ¬a₁ ¬b c = tri> (λ lt  → f-<> lt (f<t c) ) (λ eq → ¬b (proj₂ (FLeq eq) )) (f<t c)
+
+infixr 250 _f<?_
+
+_f<?_ : {n  : ℕ} → (x y : FL n ) → Dec (x f< y )
+x f<? y with FLcmp x y
+... | tri< a ¬b ¬c = yes a
+... | tri≈ ¬a refl ¬c = no ( ¬a )
+... | tri> ¬a ¬b c = no ( ¬a )
+
+open import logic
+
+_f≤_ : {n : ℕ } (x : FL n ) (y : FL n)  → Set
+_f≤_ x y = (x ≡ y ) ∨  (x f< y )
+
+FL0 : {n : ℕ } → FL n
+FL0 {zero} = f0
+FL0 {suc n} = zero :: FL0
+
+open import logic
+open import nat
+
+fmax : { n : ℕ } →  FL n
+fmax {zero} = f0
+fmax {suc n} = fromℕ< a<sa :: fmax {n}
+
+fmax< : { n : ℕ } → {x : FL n } → ¬ (fmax f< x )
+fmax< {suc n} {x :: y} (f<n lt) = nat-≤> (fmax1 x) lt where
+    fmax1 : {n : ℕ } → (x : Fin (suc n)) → toℕ x ≤ toℕ (fromℕ< {n} a<sa)
+    fmax1 {zero} zero = z≤n
+    fmax1 {suc n} zero = z≤n
+    fmax1 {suc n} (suc x) = s≤s (fmax1 x) 
+fmax< {suc n} {x :: y} (f<t lt) = fmax< {n} {y} lt
+
+fmax¬ : { n : ℕ } → {x : FL n } → ¬ ( x ≡ fmax ) → x f< fmax
+fmax¬ {zero} {f0} ne = ⊥-elim ( ne refl ) 
+fmax¬ {suc n} {x} ne with FLcmp x fmax
+... | tri< a ¬b ¬c = a
+... | tri≈ ¬a b ¬c = ⊥-elim ( ne b)
+... | tri> ¬a ¬b c = ⊥-elim (fmax< c)
+
+FL0≤ : {n : ℕ } → FL0 {n} f≤ fmax
+FL0≤ {zero} = case1 refl
+FL0≤ {suc zero} = case1 refl
+FL0≤ {suc n} with <-fcmp zero (fromℕ< {n} a<sa)
+... | tri< a ¬b ¬c = case2 (f<n a)
+... | tri≈ ¬a b ¬c with FL0≤ {n}
+... | case1 x = case1 (subst₂ (λ j k → (zero :: FL0) ≡ (j :: k ) ) b x refl )
+... | case2 x = case2 (subst (λ k →  (zero :: FL0) f< (k :: fmax)) b (f<t x)  )
+
+open import Relation.Binary as B hiding (Decidable; _⇔_)
+
+-- f≤-isDecTotalOrder : ∀ {n} → IsDecTotalOrder _≡_ (_f≤_ {n})
+-- f≤-isDecTotalOrder = record { isTotalOrder = record { isPartialOrder = record { isPreorder = {!!}
+--         ; antisym = {!!}
+--         }
+--      ; total = {!!}
+--      }
+--   ; _≟_          = {!!}
+--   ; _≤?_         = {!!}
+--   }
+
+open import Data.Sum.Base as Sum --  inj₁
+
+total : {n : ℕ } → Total (_f≤_ {n})
+total f0 f0 = inj₁  (case1 refl) 
+total (x :: xt) (y :: yt) = {!!}
+
+open import Relation.Nary using (⌊_⌋; fromWitness)
+open import Data.List.Fresh
+open import Data.List.Fresh.Relation.Unary.All
+open import Data.List.Fresh.Relation.Unary.Any as Any using (Any; here; there)
+
+FList : {n : ℕ } → Set
+FList {n} = List# (FL n) ⌊ _f<?_ ⌋
+
+fr1 : FList
+fr1 =
+   ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) ∷# 
+   ((# 0) :: ((# 1) :: ((# 0 ) :: f0))) ∷# 
+   ((# 1) :: ((# 0) :: ((# 0 ) :: f0))) ∷# 
+   ((# 2) :: ((# 0) :: ((# 0 ) :: f0))) ∷# 
+   ((# 2) :: ((# 1) :: ((# 0 ) :: f0))) ∷# 
+   []
+
+open import Data.Product
+-- open import Data.Maybe
+-- open TotalOrder
+
+FLcons : {n : ℕ } → FL n → FList {n}  → FList {n} 
+FLcons {zero} f0 y = f0 ∷# []
+FLcons {suc n} x [] = x ∷# []
+FLcons {suc n} x (cons a y x₁) with FLcmp x a
+... | tri≈ ¬a b ¬c = (cons a y x₁)
+... | tri< a₁ ¬b ¬c = cons x ( cons a y x₁) (FLcons1  x₁) where
+   FLcons1 :  a # y →  x # (cons a y x₁)
+   FLcons1 ay with total a x
+   ... | inj₁ (case1 eq) = ⊥-elim ( ¬b (sym eq) )
+   ... | inj₁ (case2 lt) = fromWitness _ (yes lt) , ? 
+   ... | inj₂ (case1 eq) = ⊥-elim ( ¬b eq )
+   ... | inj₂ (case2 lt) = {!!}
+... | tri> ¬a ¬b c with FLcons x y
+... | [] = a ∷# []
+... | cons a₁ t x₂ = cons a ( cons a₁ t x₂ ) FLcons2 where
+   FLcons2 :  fresh (FL (suc n)) ⌊ _f<?_ ⌋ a  (cons a₁ t x₂)
+   FLcons2 =  {!!} , {!!}
+
+fr6 = FLcons ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) fr1