# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1687558963 -32400
# Node ID 0cf6d7702dabb83ddd388ea11951145306493c62
# Parent  0d29328c0441d1946f2bc0ce9a66aa906982dc3a
Countable-Bernstein done

diff -r 0d29328c0441 -r 0cf6d7702dab src/bijection.agda
--- a/src/bijection.agda	Sat Jun 24 01:44:24 2023 +0900
+++ b/src/bijection.agda	Sat Jun 24 07:22:43 2023 +0900
@@ -506,13 +506,14 @@
 
 Countable-Bernstein : (A B C : Set) → Bijection A ℕ → Bijection C ℕ
      → (fi : InjectiveF A  B ) → (gi : InjectiveF  B C )
-     → (is-A : (c : C ) → Dec (Is A C (λ x → (InjectiveF.f gi (InjectiveF.f fi x))) c )) → (is-B : (c : C ) → Dec (Is B C (InjectiveF.f gi) c)  )
+     → (is-A : (c : C ) → Dec (Is A C (λ x → (InjectiveF.f gi (InjectiveF.f fi x))) c )) 
+     → (is-B : (c : C ) → Dec (Is B C (InjectiveF.f gi) c)  )
      → Bijection B ℕ
 Countable-Bernstein A B C an cn fi gi is-A is-B = record {
        fun→  = λ x → bton x
      ; fun←  = λ n → ntob n
-     ; fiso→ = λ n → ?
-     ; fiso← = λ x → ?
+     ; fiso→ = biso
+     ; fiso← = biso1 
    } where
     --
     --     an     f     g     cn
@@ -740,18 +741,33 @@
 
     lem01 : (n i : ℕ) → suc n ≤ count-B i → CountB n
     lem01 n i le = lem09 i (count-B i) le refl where
-        -- starting from 0, if count B i ≡ suc n, this is it
-
+        -- injection of count-B
+        ---
         lem06 : (i j : ℕ ) → Is B C g (fun← cn i) → Is B C g (fun← cn 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 (fun← cn i) → Is B C g (fun← cn j) → count-B j ≡ count-B i → ⊥
-            lem20 zero j i<j bi bj le = ?
+            lem20 zero (suc j) i<j bi bj le with  is-B (fun← cn 0) | inspect count-B 0 | is-B (fun← cn (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 (fun← cn 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 = ? where
+            lem20 (suc i) (suc j) (s≤s i<j) bi bj le = ⊥-elim ( nat-≡< lem24 lem21 ) where
                  --
                  --                    i  <     suc i  ≤    j
-                 --            suc (cb i) < cb (suc i) ≤ cb 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 (fun← cn (suc i)) | inspect count-B (suc i)
                  ... | yes _ | record { eq = eq1 } = refl
@@ -762,9 +778,8 @@
                  ... | no nisa | _ = ⊥-elim ( nisa bj )
                  lem24 : count-B i ≡ count-B j
                  lem24 with  is-B (fun← cn (suc i)) | inspect count-B (suc i) | is-B (fun← cn (suc j)) | inspect count-B (suc j)
-                 ... | no nisc  | _ | _ | _ = ?
-                 ... |  yes _ | _ | no nisc | _  = ?
-                 ... |  no _ | _ | no nisc | _  = ?
+                 ... | 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
@@ -778,8 +793,6 @@
             ... | tri≈ ¬a b ¬c = b
             ... | tri> ¬a ¬b c₁ = ⊥-elim ( lem20 j i c₁ bj bi eq )
 
-        lem09 : (i j : ℕ) → suc n ≤ j → j ≡ count-B i →  CountB n
-
         lem07 : (n i : ℕ) → count-B i ≡ suc n → CountB n
         lem07 n 0 eq with is-B (fun← cn 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 
@@ -794,6 +807,9 @@
             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 (fun← cn 0) | inspect count-B 0
@@ -867,7 +883,7 @@
 ---   ℕ ⊆ List A ⊆ List (Maybe A) ⊆ List A ∧ List Bool ⊆ ℕ
 
 LMℕ : (A : Set ) → Bijection (List A) ℕ → Bijection (List (Maybe A)) ℕ
-LMℕ A Ln = Countable-Bernstein (List A) (List (Maybe A)) (List A ∧ List Bool) Ln (LM1 A Ln)  fi gi ? ? where
+LMℕ A Ln = Countable-Bernstein (List A) (List (Maybe A)) (List A ∧ List Bool) Ln (LM1 A Ln)  fi gi dec0 dec1 where
    f : List A → List (Maybe A)
    f [] = []
    f (x ∷ t) = just x ∷ f t
@@ -901,6 +917,25 @@
    fi = record { f = f ; inject = f-inject  }
    gi : InjectiveF (List (Maybe A)) (List A ∧ List Bool )
    gi = record { f = g ; inject = g-inject }
+   dec0 : (c : List A ∧ List Bool) → Dec (Is (List A) (List A ∧ List Bool) (λ x → g (f x)) c)
+   dec0 ⟪ [] , [] ⟫ = yes record { a = [] ; fa=c = refl }
+   dec0 ⟪ h ∷ t , [] ⟫ = ?
+   dec0 ⟪ [] , true ∷ bt ⟫ = ?
+   dec0 ⟪ [] , false ∷ bt ⟫ = ?
+   dec0 ⟪ h ∷ t , (true ∷ bt) ⟫ with dec0 ⟪ t , bt ⟫
+   ... | yes y = yes record { a = h ∷ Is.a y ; fa=c = cong₂ (λ j k → ⟪ h ∷ j , true ∷ k ⟫ ) (cong proj1 (Is.fa=c y)) (cong proj2 (Is.fa=c y))  }
+   ... | no n = no ( λ np →  ⊥-elim ( n record { a = ? ; fa=c = ? }  ) )
+   dec0 ⟪ (h ∷ t) , (false ∷ bt) ⟫ = no ( λ np → ? )
+   dec1 : (c : List A ∧ List Bool) → Dec (Is (List (Maybe A)) (List A ∧ List Bool) g c)
+   dec1 ⟪ [] , [] ⟫ = yes record { a = [] ; fa=c = refl }
+   dec1 ⟪ h ∷ t , [] ⟫ = ?
+   dec1 ⟪ [] , _ ∷ bt ⟫ = ?
+   dec1 ⟪ h ∷ t , true ∷ bt ⟫ with dec1 ⟪ t , bt ⟫
+   ... | yes y = yes record { a = just h ∷ Is.a y ; fa=c = cong₂ (λ j k → ⟪ h ∷ j , true ∷ k ⟫ ) (cong proj1 (Is.fa=c y)) (cong proj2 (Is.fa=c y))   }
+   ... | no n = ?
+   dec1 ⟪ h ∷ t , false ∷ bt ⟫  with dec1 ⟪ t , bt ⟫
+   ... | yes y = yes record { a = nothing ∷ Is.a y ; fa=c = cong₂ (λ j k → ⟪ h ∷ j , false ∷ k ⟫ ) (cong proj1 (Is.fa=c y)) (cong proj2 (Is.fa=c y))   }
+   ... | no n = ?
 
 -- open import Data.Fin
 --