# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1686446769 -32400
# Node ID 70d46c446b0d379a95f82256027da889840f166d
# Parent  1f43bbfff797fa8b55558bdaecf17ba6092c14a7
using Fresh List

diff -r 1f43bbfff797 -r 70d46c446b0d src/bijection.agda
--- a/src/bijection.agda	Sun Jun 11 01:20:46 2023 +0900
+++ b/src/bijection.agda	Sun Jun 11 10:26:09 2023 +0900
@@ -10,7 +10,7 @@
 open import Data.Nat.Properties
 open import Relation.Nullary
 open import Data.Empty
-open import Data.Unit hiding ( _≤_ )
+open import Data.Unit using ( tt ; ⊤ )
 open import  Relation.Binary.Core hiding (_⇔_)
 open import  Relation.Binary.Definitions
 open import Relation.Binary.PropositionalEquality
@@ -41,6 +41,12 @@
 bi-sym : {n m : Level} (R : Set n) (S : Set m) → Bijection R S →  Bijection S R
 bi-sym R S eq = record {  fun← =  fun→ eq ; fun→  = fun← eq  ; fiso← =  fiso→ eq ;  fiso→ =  fiso← eq }
 
+bi-inject← : {n m : Level} {R : Set n} {S : Set m} → (rs : Bijection R S) → {x y : S} → fun← rs x ≡ fun← rs y → x ≡ y 
+bi-inject← rs {x} {y} eq = subst₂ (λ j k → j ≡ k ) (fiso→  rs _) (fiso→ rs _) (cong (fun→ rs) eq)
+
+bi-inject→ : {n m : Level} {R : Set n} {S : Set m} → (rs : Bijection R S) → {x y : R} → fun→ rs x ≡ fun→ rs y → x ≡ y 
+bi-inject→ rs {x} {y} eq = subst₂ (λ j k → j ≡ k ) (fiso←  rs _) (fiso← rs _) (cong (fun← rs) eq)
+
 open import Relation.Binary.Structures
 
 bijIsEquivalence : {n : Level } → IsEquivalence  (Bijection {n} {n})
@@ -478,6 +484,13 @@
 -- Bernstein is non constructive, so we cannot use this without some assumption
 --   but in case of ℕ, we can construct it directly.
 
+open import Data.Product
+open import Relation.Nary using (⌊_⌋)
+open import Relation.Nullary.Decidable hiding (⌊_⌋)
+open import Data.Unit.Base using (⊤ ; tt)
+open import Data.List.Fresh hiding ([_])
+
+
 record InjectiveF (A B : Set) : Set where
    field
       f : A → B
@@ -585,6 +598,79 @@
     ... | no nisA | yes isB = ≤-trans (ca≤cb0 n) px≤x
     ... | no nisA | no nisB = ca≤cb0 n
 
+    data  FL : (n : ℕ ) → Set where
+       ca<n : {n : ℕ} → (i : ℕ) →  fun→ cn (g (f (fun← an i))) < n →  FL n
+
+    _f<_  : {n : ℕ } (x : FL n ) (y : FL n)  → Set  
+    _f<_  {n} (ca<n i i<n) (ca<n j j<n) = fun→ cn (g (f (fun← an i))) < fun→ cn (g (f (fun← an j))) 
+
+    infixr 250 _f<?_
+
+    f<-trans : {n : ℕ } { x y z : FL n } → x f< y → y f< z → x f< z
+    f<-trans {n} {ca<n i x} {ca<n i₁ x₁} {ca<n i₂ x₂} x<y y<z = <-trans x<y y<z
+
+    FL-eq0 : {n i j : ℕ} → {x : fun→ cn (g (f (fun← an i))) < n } {y : fun→ cn (g (f (fun← an j))) < n}  
+         → ca<n i x ≡ ca<n j y 
+         → fun→ cn (g (f (fun← an i))) ≡ fun→ cn (g (f (fun← an j)))
+    FL-eq0 {n} {i} {.i} {x} {.x} refl = refl
+
+    -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_;refl)
+
+    FL-eq1 : {n i j : ℕ} → {x : fun→ cn (g (f (fun← an i))) < n } {y : fun→ cn (g (f (fun← an j))) < n}  
+         → fun→ cn (g (f (fun← an i))) ≡ fun→ cn (g (f (fun← an j)))
+         → ca<n i x ≡ ca<n j y 
+    FL-eq1 {n} {i} {j} {x} {y} eq = lem00 i=j where
+        i=j : i ≡ j
+        i=j = bi-inject← an (InjectiveF.inject fi ( InjectiveF.inject gi (bi-inject→ cn eq) ))
+        lem00 : {x : fun→ cn (g (f (fun← an i))) < n } {y : fun→ cn (g (f (fun← an j))) < n} → i ≡ j → ca<n i x ≡ ca<n j y
+        lem00 {x} {y} refl with <-irrelevant x y
+        ... | refl = refl
+
+    FLcmp : {n : ℕ } → Trichotomous {Level.zero} {FL n}  _≡_  _f<_
+    FLcmp {n} (ca<n i x) (ca<n j y) with <-cmp (fun→ cn (g (f (fun← an i)))) (fun→ cn (g (f (fun← an j))) )
+    ... | tri< a ¬b ¬c = tri< a (λ eq → ¬b (FL-eq0 eq) ) ¬c 
+    ... | tri≈ ¬a eq ¬c = tri≈ ¬a (FL-eq1 eq) ¬c 
+    ... | tri> ¬a ¬b c = tri> ¬a (λ eq → ¬b (FL-eq0 eq) )  c 
+
+    _f<?_ : {n  : ℕ} → (x y : FL n ) → Dec (x f< y )
+    _f<?_ {n} x y with FLcmp x y
+    ... | tri< a ¬b ¬c = yes a
+    ... | tri≈ ¬a b ¬c = no ¬a
+    ... | tri> ¬a ¬b c = no ¬a
+
+    FList : (n : ℕ ) → Set
+    FList n = List# (FL n) ⌊ _f<?_ ⌋
+
+    ttf : {n : ℕ } {x a : FL (n)} → x f< a → (y : FList (n)) →  fresh (FL (n)) ⌊ _f<?_ ⌋  a y  → fresh (FL (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)
+
+    FLinsert : {n : ℕ } → FL n → FList n  → FList n 
+    FLfresh : {n : ℕ } → (a x : FL (suc n) ) → (y : FList (suc n) ) → a f< x
+         → fresh (FL (suc n)) ⌊ _f<?_ ⌋ a y → fresh (FL (suc n)) ⌊ _f<?_ ⌋ a (FLinsert x y)
+    FLinsert {zero} f0 y = f0 ∷# []
+    FLinsert {suc n} x [] = x ∷# []
+    FLinsert {suc n} x (cons a y x₁) with FLcmp x a
+    ... | tri≈ ¬a b ¬c  = cons a y x₁
+    ... | tri< lt ¬b ¬c  = cons x ( cons a y x₁) ( Level.lift (fromWitness lt ) , ttf lt y  x₁) 
+    FLinsert {suc n} x (cons a [] x₁) | tri> ¬a ¬b lt  = cons a ( x  ∷# []  ) ( Level.lift (fromWitness lt) , Level.lift tt )
+    FLinsert {suc n} x (cons a y yr)  | tri> ¬a ¬b a<x = cons a (FLinsert x y) (FLfresh a x y a<x yr )
+
+    FLfresh a x [] a<x (Level.lift tt) = Level.lift (fromWitness a<x) , Level.lift tt
+    FLfresh a x (cons b [] (Level.lift tt)) a<x (Level.lift a<b , a<y) with FLcmp x b
+    ... | tri< x<b ¬b ¬c  = Level.lift (fromWitness a<x) , Level.lift a<b , Level.lift tt
+    ... | tri≈ ¬a refl ¬c = Level.lift (fromWitness a<x) , Level.lift tt
+    ... | tri> ¬a ¬b b<x =  Level.lift a<b  ,  Level.lift (fromWitness  (f<-trans (toWitness a<b) b<x))  , Level.lift tt
+    FLfresh a x (cons b y br) a<x (Level.lift a<b , a<y) with FLcmp x b
+    ... | tri< x<b ¬b ¬c =  Level.lift (fromWitness a<x) , Level.lift a<b , ttf (toWitness a<b) y br
+    ... | tri≈ ¬a refl ¬c = Level.lift (fromWitness a<x) , ttf a<x y br
+    FLfresh a x (cons b [] br) a<x (Level.lift a<b , a<y) | tri> ¬a ¬b b<x =
+        Level.lift a<b , Level.lift (fromWitness (f<-trans (toWitness a<b) b<x)) , Level.lift tt
+    FLfresh a x (cons b (cons a₁ y x₁) br) a<x (Level.lift a<b , a<y) | tri> ¬a ¬b b<x =
+        Level.lift a<b , FLfresh a x (cons a₁ y x₁) a<x a<y
+
     record maxAC (n : ℕ) : Set where
        field
            ac : ℕ
@@ -604,14 +690,7 @@
                 lem12 (suc i) i=z with is-A (fun← cn  (suc i)) | inspect ( count-A ) (suc i)
                 ... | yes isa | record { eq = eq1 } = record { ac = suc i ; n<ca = subst (λ k → 0 < k) (sym eq1) 0<s ; all-a = ? }
                 ... | no nisa | record { eq = eq1 } = ⊥-elim ( nisa record { a = fun← an zero ; fa=c = trans (sym (fiso←  cn _)) (sym (cong (fun← cn) i=z))  } ) 
-            lem10 (suc j) with <-cmp (suc j) (count-A (maxAC.ac (lem10 j)))
-            ... | tri< a ¬b ¬c = record { ac = max (fun→ cn (g (f (fun← an (suc j))))) (maxAC.ac (lem10 j)) ; n<ca = ? ; all-a = ? } 
-            ... | tri> ¬a ¬b ca<sj = ? --   maxAC (suc j) contains at least (suc j) elements of A
-            ... | tri≈ ¬a sj=ca ¬c = record { ac = nac ; n<ca = ? ; all-a = ? } where
-                -- 
-                -- maxAC contains all 0 to j th element of A and nothing else
-                --    using full-a, we can take fun← cn which is smaller than suc j
-                --    so it cannot be fan.
+            lem10 (suc j) = record { ac = max (fun→ cn (g (f (fun← an (suc j))))) (maxAC.ac (lem10 j)) ; n<ca = ? ; all-a = ? }  where
                 
                 fan = fun→ cn (g (f (fun← an (suc j)))) 
                 ac = maxAC.ac (lem10 j)
@@ -624,6 +703,8 @@
                     n<ca0 = maxAC.n<ca (lem10 j)
                     n<ca2 : j < count-A nac
                     n<ca2 = ≤-trans n<ca0 (count-A-homo (y≤max fan ac))
+                    fun< : (i : ℕ) → count-A (fun→ cn (g (f (fun← an i)))) < count-A (suc (fun→ cn (g (f (fun← an i)))))
+                    fun< = ?
 
                     n<ca1 : (i n : ℕ ) → i ≤ suc j → n ≤ nac  →  i < count-A n
                     n<ca1 zero n with is-A (fun← cn zero)