# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1689559219 -32400
# Node ID 4456eebbd1bcd49c5ce786a0c91d0d703ac27aa4
# Parent  bcf3ca6ba87b96a3f5fe3149d2d3c375eaa5e2a4
copying countable bijection may not easy

diff -r bcf3ca6ba87b -r 4456eebbd1bc automaton-in-agda/src/finiteSetUtil.agda
--- a/automaton-in-agda/src/finiteSetUtil.agda	Mon Jul 17 08:14:57 2023 +0900
+++ b/automaton-in-agda/src/finiteSetUtil.agda	Mon Jul 17 11:00:19 2023 +0900
@@ -3,8 +3,8 @@
 module finiteSetUtil  where
 
 open import Data.Nat hiding ( _≟_ )
-open import Data.Fin renaming ( _<_ to _<<_ ; _>_ to _f>_ ; _≟_ to _f≟_ ) hiding (_≤_ )
-open import Data.Fin.Properties hiding ( <-trans ) renaming ( <-cmp to <-fcmp )
+open import Data.Fin renaming ( _<_ to _<<_ ; _>_ to _f>_ ; _≟_ to _f≟_ ) hiding (_≤_ ; pred )
+open import Data.Fin.Properties hiding ( <-trans ) renaming ( <-cmp to <-fcmp ) hiding (≤-refl ; ≤-trans )
 open import Data.Empty
 open import Relation.Nullary
 open import Relation.Binary.Definitions
@@ -572,44 +572,190 @@
 
 open import bijection using ( InjectiveF ; Is )
 
-record countB (B : Set) : Set where
-   field
-      cb : ℕ
-      ib : {i : ℕ} → i < cb → B
-      ib-inject : {i j : ℕ} → (i<cb : i < cb) → (j<cb : j < cb) → ib i<cb ≡ ib j<cb  → i ≡ j
-
 inject-fin : {A B : Set}  (fa : FiniteSet A ) 
-   → (fi : InjectiveF B A) 
-   → (is-B : (a : A ) → Dec (Is B A (InjectiveF.f fi) a)  )
+   → (gi : InjectiveF B A) 
+   → (is-B : (a : A ) → Dec (Is B A (InjectiveF.f gi) a)  )
    → FiniteSet B
-inject-fin {A} {B} fa fi is-B = record {
-       finite = countB.cb (cb00 (finite fa) NP.≤-refl )
-       ; Q←F = λ fb → countB.ib (cb00 (finite fa) NP.≤-refl ) (fin<n {_} {fb})
-       ; F←Q =  λ b → fromℕ< (cb<cb (fin<n {_} {F←Q fa (InjectiveF.f fi b)} ))
+inject-fin {A} {B} fa gi is-B with finite fa | inspect finite fa
+inject-fin {A} {B} fa gi is-B | zero | record { eq = eq1 } = ?
+inject-fin {A} {B} fa gi is-B | suc pfa | record { eq = eq1 } = record {
+       finite = maxb
+       ; Q←F = λ fb → ntob (toℕ fb) fin<n
+       ; F←Q =  λ b → fromℕ< (bton<maxb b)
        ; finiso→ = ?
        ; finiso← = ?
        } where
-   f = InjectiveF.f fi
-   cb00 : (i : ℕ) → i ≤ finite fa → countB B
-   cb00 0 i<fa = record { cb = 0 ; ib = λ () ; ib-inject = λ () }
-   cb00 (suc i) i<fa with is-B (Q←F fa (fromℕ< i<fa))
-   ... | yes y = record { cb = suc (countB.cb (cb00 i (NP.≤-trans a≤sa i<fa))) ; ib = cb01 ; ib-inject = cb02 } where
-        pcb : countB B
-        pcb = cb00 i (NP.≤-trans a≤sa i<fa)
-        cb01 :  {j : ℕ} → j < suc (countB.cb (cb00 i (NP.≤-trans a≤sa i<fa))) → B
-        cb01 {j} j<c with <-∨ j<c
-        ... | case1 eq = Is.a y
-        ... | case2 lt = countB.ib (cb00 i (NP.≤-trans a≤sa i<fa)) lt
-        cb02 : {i1 : ℕ} {j : ℕ}
-            (i<cb : i1 < suc (countB.cb (cb00 i (NP.≤-trans a≤sa i<fa))))
-            (j<cb : j < suc (countB.cb (cb00 i (NP.≤-trans a≤sa i<fa)))) →
-            cb01 i<cb ≡ cb01 j<cb → i1 ≡ j
-        cb02 = ?
-   ... | no n  = record { cb = countB.cb (cb00 i (NP.≤-trans a≤sa i<fa))       ; ib = cb01 
-     ; ib-inject = countB.ib-inject (cb00 i (NP.≤-trans a≤sa i<fa))} where
-        cb01 :  {j : ℕ} → j < countB.cb (cb00 i (NP.≤-trans a≤sa i<fa)) → B
-        cb01 {j} j<c = countB.ib (cb00 i (NP.≤-trans a≤sa i<fa)) j<c
+    g = InjectiveF.f gi
+    pfa<fa : pfa < finite fa
+    pfa<fa = subst (λ k → pfa < k ) (sym eq1) a<sa
+    h : ℕ → A
+    h i with <-cmp i (finite fa)
+    ... | tri< a ¬b ¬c = Q←F fa (fromℕ< a )
+    ... | tri≈ ¬a b ¬c = Q←F fa (fromℕ< pfa<fa )
+    ... | tri> ¬a ¬b c = Q←F fa (fromℕ< pfa<fa )
+    C = A
+    h⁻¹ : A → ℕ
+    h⁻¹ a = toℕ (F←Q fa a)
+
+    h-iso : (i : ℕ) → i < finite fa → h⁻¹ (h i) ≡ i
+    h-iso = ?
+
+    count-B : ℕ → ℕ
+    count-B zero with is-B (h zero)
+    ... | yes isb = 1
+    ... | no nisb = 0
+    count-B (suc n) with is-B (h (suc n))
+    ... | yes isb = suc (count-B n)
+    ... | no nisb = count-B n
+
+    maxb : ℕ
+    maxb = count-B (finite fa)
+
+    --
+    -- countB record create ℕ → B and its injection
+    --
+    record CountB (n : ℕ) : Set where
+       field
+          b : B
+          cb : ℕ
+          b=cn : h cb ≡ g b
+          cb=n : count-B cb ≡ suc n
+          cb-inject : (cb1 : ℕ) → Is B C g (h cb1) → count-B cb ≡ count-B cb1 → cb ≡ cb1
+
+    count-B-mono : {i j : ℕ} → i ≤ j → count-B i ≤ count-B j
+    count-B-mono {i} {j} i≤j with ≤-∨ i≤j
+    ... | case1 refl = ≤-refl
+    ... | case2 i<j = lem00 _ _ i<j where
+         lem00 : (i j : ℕ) → i < j → count-B i ≤ count-B j
+         lem00 i (suc j) (s≤s i<j) = ≤-trans (count-B-mono i<j) (lem01 j) where
+             lem01 : (j : ℕ) → count-B j ≤ count-B (suc j)
+             lem01 zero with is-B (h (suc zero))
+             ... | yes isb = refl-≤s
+             ... | no nisb = ≤-refl
+             lem01 (suc n) with is-B (h (suc (suc n)))
+             ... | yes isb = refl-≤s
+             ... | no nisb = ≤-refl
 
-   cb<cb : {i : ℕ} → (i<fa : i ≤ finite fa) → countB.cb (cb00 _ i<fa) < countB.cb (cb00 _ NP.≤-refl)  
-   cb<cb = ?
+    lem01 : (n i : ℕ) → suc n ≤ count-B i → CountB n
+    lem01 n i le = lem09 i (count-B i) le refl where
+        -- injection of count-B
+        ---
+        lem06 : (i j : ℕ ) → Is B C g (h i) → Is B C g (h j) → count-B i ≡ count-B j → i ≡ j
+        lem06 i j bi bj eq = lem08  where
+            lem20 : (i j : ℕ) → i < j →  Is B C g (h i) → Is B C g (h j) → count-B j ≡ count-B i → ⊥
+            lem20 zero (suc j) i<j bi bj le with  is-B (h 0) | inspect count-B 0 | is-B (h (suc j)) | inspect count-B (suc j)
+            ... | no nisc  | _ | _ | _ = ⊥-elim (nisc bi)
+            ... |  yes _ | _ | no nisc | _  = ⊥-elim (nisc bj)
+            ... | yes _ | record { eq = eq1 } | yes _ | record { eq = eq2 } = ⊥-elim ( nat-≤> lem25 a<sa) where
+                 lem22 : 1 ≡ count-B 0
+                 lem22 with is-B (h 0) | inspect count-B 0
+                 ... | yes _ | record { eq = eq1 } = refl
+                 ... | no nisa | _ = ⊥-elim ( nisa bi )
+                 lem24 : count-B j ≡ 0
+                 lem24 = cong pred le
+                 lem25 : 1 ≤ 0
+                 lem25 = begin
+                    1 ≡⟨ lem22 ⟩
+                    count-B 0 ≤⟨ count-B-mono {0} {j} z≤n ⟩
+                    count-B j ≡⟨ lem24 ⟩
+                    0 ∎ where open ≤-Reasoning
+            lem20 (suc i) zero () bi bj le
+            lem20 (suc i) (suc j) (s≤s i<j) bi bj le = ⊥-elim ( nat-≡< lem24 lem21 ) where
+                 --
+                 --                    i  <     suc i  ≤    j
+                 --    cb i <  suc (cb i) < cb (suc i) ≤ cb j
+                 --    suc (cb i) ≡ suc (cb j) → cb i ≡ cb j
+                 lem22 : suc (count-B i) ≡ count-B (suc i)
+                 lem22 with is-B (h (suc i)) | inspect count-B (suc i)
+                 ... | yes _ | record { eq = eq1 } = refl
+                 ... | no nisa | _ = ⊥-elim ( nisa bi )
+                 lem23 : suc (count-B j) ≡ count-B (suc j)
+                 lem23 with is-B (h (suc j)) | inspect count-B (suc j)
+                 ... | yes _ | record { eq = eq1 } = refl
+                 ... | no nisa | _ = ⊥-elim ( nisa bj )
+                 lem24 : count-B i ≡ count-B j
+                 lem24 with  is-B (h (suc i)) | inspect count-B (suc i) | is-B (h (suc j)) | inspect count-B (suc j)
+                 ... | no nisc  | _ | _ | _ = ⊥-elim (nisc bi)
+                 ... |  yes _ | _ | no nisc | _  = ⊥-elim (nisc bj)
+                 ... | yes _ | record { eq = eq1 } | yes _ | record { eq = eq2 } = sym (cong pred le)
+                 lem21 : suc (count-B i) ≤ count-B j
+                 lem21 = begin
+                     suc (count-B i) ≡⟨ lem22 ⟩
+                     count-B (suc i) ≤⟨ count-B-mono i<j ⟩
+                     count-B j ∎ where
+                        open ≤-Reasoning
+            lem08 : i ≡ j
+            lem08 with <-cmp i j
+            ... | tri< a ¬b ¬c = ⊥-elim ( lem20 i j a bi bj (sym eq) )
+            ... | tri≈ ¬a b ¬c = b
+            ... | tri> ¬a ¬b c₁ = ⊥-elim ( lem20 j i c₁ bj bi eq )
 
+        lem07 : (n i : ℕ) → count-B i ≡ suc n → CountB n
+        lem07 n 0 eq with is-B (h 0) | inspect count-B 0
+        ... | yes isb | record { eq = eq1 } = record { b = Is.a isb ; cb = 0 ; b=cn = sym (Is.fa=c isb) ; cb=n = trans eq1 eq 
+                ; cb-inject = λ cb1 iscb1 cb1eq → lem12 cb1 iscb1 (subst (λ k → k ≡ count-B cb1) eq1 cb1eq)   } where
+            lem12 : (cb1 : ℕ) →  Is B C g (h cb1)  → 1 ≡ count-B cb1 → 0 ≡ cb1
+            lem12 cb1 iscb1 cbeq = lem06 0 cb1 isb iscb1 (trans eq1 cbeq) 
+        ... | no nisb | record { eq = eq1 } = ⊥-elim ( nat-≡< eq (s≤s z≤n ) )
+        lem07 n (suc i) eq with is-B (h (suc i)) | inspect count-B (suc i)
+        ... | yes isb | record { eq = eq1 } = record { b = Is.a isb ; cb = suc i ; b=cn = sym (Is.fa=c isb) ; cb=n = trans eq1 eq
+                 ; cb-inject = λ cb1 iscb1 cb1eq → lem12 cb1 iscb1 (subst (λ k → k ≡ count-B cb1) eq1 cb1eq)   } where
+            lem12 : (cb1 : ℕ) → Is B C g (h cb1) → suc (count-B i)  ≡ count-B cb1 → suc i ≡ cb1
+            lem12 cb1 iscb1 cbeq = lem06 (suc i) cb1 isb iscb1 (trans eq1 cbeq)
+        ... | no nisb | record { eq = eq1 } = lem07 n i  eq
+
+        -- starting from 0, if count B i ≡ suc n, this is it
+
+        lem09 : (i j : ℕ) → suc n ≤ j → j ≡ count-B i →  CountB n
+        lem09 0 (suc j) (s≤s le) eq with ≤-∨ (s≤s le)
+        ... | case1 eq1 = lem07 n 0 (sym (trans eq1 eq ))
+        ... | case2 (s≤s lt) with is-B (h 0) | inspect count-B 0
+        ... | yes isb | record { eq = eq1 } = ⊥-elim ( nat-≤> (≤-trans (s≤s lt) (refl-≤≡ eq) ) (s≤s (s≤s z≤n)) )
+        ... | no nisb | record { eq = eq1 } = ⊥-elim (nat-≡< (sym eq) (s≤s z≤n))
+        lem09 (suc i) (suc j) (s≤s le) eq with ≤-∨ (s≤s le)
+        ... | case1 eq1 = lem07 n (suc i) (sym (trans eq1 eq ))
+        ... | case2 (s≤s lt) with is-B (h (suc i)) | inspect count-B (suc i)
+        ... | yes isb | record { eq = eq1 } = lem09 i j lt (cong pred eq)
+        ... | no nisb | record { eq = eq1 } = lem09 i (suc j) (≤-trans lt a≤sa) eq
+
+    bton : B → ℕ
+    bton b = pred (count-B (h⁻¹ (g b)))
+
+    lem22 : {n : ℕ } →  n < maxb → suc n ≤ count-B n
+    lem22 {n} n<mb = ?
+
+    lem23 : (b : B) →  0 < count-B (h⁻¹ (g b))
+    lem23 = ?
+
+    bton<maxb : (b : B) →  bton b < maxb
+    bton<maxb b = begin
+       suc (bton b) ≡⟨ sucprd (lem23 b)  ⟩
+       count-B (h⁻¹ (g b)) ≤⟨ count-B-mono {h⁻¹ (g b)} {finite fa} (<to≤ fin<n) ⟩
+       count-B (finite fa) ≡⟨ refl ⟩
+       maxb ∎ where
+          open ≤-Reasoning
+
+    ntob : (n : ℕ) → n < maxb  → B
+    ntob n n<mb = CountB.b (lem01 n n (lem22 n<mb))
+
+    biso : (n : ℕ) → (n<mb : n < maxb) → bton (ntob n n<mb ) ≡ n
+    biso n n<mb = begin  
+        bton (ntob n n<mb ) ≡⟨ refl ⟩
+        pred (count-B (h⁻¹ (g (CountB.b CB)))) ≡⟨ sym ( cong (λ k → pred (count-B (h⁻¹ k))) ( CountB.b=cn CB)) ⟩
+        pred (count-B (h⁻¹ (h (CountB.cb CB)))) ≡⟨ cong (λ k → pred (count-B k)) (h-iso _ cb<fa) ⟩
+        pred (count-B (CountB.cb CB)) ≡⟨ cong pred (CountB.cb=n CB) ⟩
+        pred (suc n) ≡⟨ refl ⟩
+        n ∎ where
+           open ≡-Reasoning
+           CB  : CountB n
+           CB  = lem01 n n (lem22 n<mb)
+           cb<fa : CountB.cb CB < finite fa
+           cb<fa = ?
+
+
+    --
+    -- uniqueness of ntob is proved by injection
+    --
+    biso1 : (b : B) → ntob (bton b) (bton<maxb b) ≡ b
+    biso1 b = ?
+