{-# OPTIONS --allow-unsolved-metas #-} 
module FLutil where

open import Level hiding ( suc ; zero )
open import Algebra
open import Algebra.Structures
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 Function hiding (id ; flip)
open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_)
open import Function.LeftInverse  using ( _LeftInverseOf_ )
open import Function.Equality using (Π)
open import Data.Nat -- using (ℕ; suc; zero; s≤s ; z≤n )
open import Data.Nat.Properties -- using (<-trans)
open import Relation.Binary.PropositionalEquality 
-- open import Data.List using (List; []; _∷_ ; length ; _++_ ; head ; tail ) renaming (reverse to rev )
open import nat

open import Symmetric

open import Relation.Nullary
open import Data.Empty
open import  Relation.Binary.Core
open import  Relation.Binary.Definitions
open import fin
open import Putil
open import Gutil
open import Solvable

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 : ℕ } → FL n
FL0 {zero} = f0
FL0 {suc n} = zero :: FL0

open import logic

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)  )

fsuc : { n : ℕ } → (x : FL n ) → x f< fmax → FL n 
fsuc {n} (x :: y) (f<n lt) = fromℕ< fsuc1 :: y where
    fsuc2 : toℕ x < toℕ (fromℕ< a<sa) 
    fsuc2 = lt
    fsuc1 : suc (toℕ x) < n
    fsuc1 =  ≤-trans (s≤s lt) ( s≤s ( toℕ≤pred[n] (fromℕ< a<sa)) )
fsuc (x :: y) (f<t lt) = x :: fsuc y lt

open import Data.List

flist1 :  {n : ℕ } (i : ℕ) → i < suc n → List (FL n) → List (FL n) → List (FL (suc n)) 
flist1 zero i<n [] _ = []
flist1 zero i<n (a ∷ x ) z  = ( zero :: a ) ∷ flist1 zero i<n x z 
flist1 (suc i) (s≤s i<n) [] z  = flist1 i (<-trans i<n a<sa) z z 
flist1 (suc i) i<n (a ∷ x ) z  = ((fromℕ< i<n ) :: a ) ∷ flist1 (suc i) i<n x z 

flist : {n : ℕ } → FL n → List (FL n) 
flist {zero} f0 = f0 ∷ [] 
flist {suc n} (x :: y)  = flist1 n a<sa (flist y) (flist y)   

fr22 : fsuc (zero :: zero :: f0) (fmax¬ (λ ())) ≡ (suc zero :: zero :: f0)
fr22 = refl

fr4 : List (FL 4)
fr4 = Data.List.reverse (flist (fmax {4}) )

fr5 : List (List ℕ)
fr5 = map plist (map FL→perm  (Data.List.reverse (flist (fmax {4}) )))

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

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 = ? , ?
... | 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