# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1687230852 -32400
# Node ID 9130c44031a56f46be305fbf22fbf69143957b07
# Parent  0472bfb4964eacea37df2f3b7290e0c6b8755978
...

diff -r 0472bfb4964e -r 9130c44031a5 src/bijection.agda
--- a/src/bijection.agda	Mon Jun 19 17:57:43 2023 +0900
+++ b/src/bijection.agda	Tue Jun 20 12:14:12 2023 +0900
@@ -116,6 +116,13 @@
 i≤0→i≡0 : {i : ℕ } → i ≤ 0 → i ≡ 0
 i≤0→i≡0 {0} z≤n = refl
 
+----
+--    (0, 0) (0, 1)  (0, 2) ....
+--    (1, 0) (1, 1)  (1, 2) ....
+--    (2, 0) (2, 1)  (2, 2) ....
+--      :      :      :
+--      :      :      :
+--
 
 nxn : Bijection ℕ (ℕ ∧ ℕ)
 nxn = record {
@@ -567,14 +574,18 @@
     c zero = fun→ cn (g (f (fun← an zero)))
     c (suc n) = max (fun→ cn (g (f (fun← an (suc n))))) (c n)
 
-    c< : (i n : ℕ) → i < suc n → fun→ cn (g (f (fun← an i))) < suc (c n)
-    c< zero zero (s≤s z≤n) = a<sa
-    c< (suc i) zero  (s≤s ())
-    c< zero (suc n) (s≤s z≤n) = ≤-trans (c< zero n (<-transʳ  z≤n a<sa) ) (s≤s (y≤max (fun→ cn (g (f (fun← an (suc n))))) (c n)))
-    c< (i @ (suc _)) (suc n) i≤n with ≤-∨ i≤n
-    ... | case1 refl = s≤s (x≤max  (fun→ cn (g (f (fun← an (suc n))))) (c n))
-    ... | case2 (s≤s (s≤s i<n)) = ≤-trans (c< i n (<-transʳ i<n a<sa)) 
-        (s≤s (y≤max (fun→ cn (InjectiveF.f gi (InjectiveF.f fi (fun← an (suc n))))) (c n)))
+    c< : (i : ℕ) → fun→ cn (g (f (fun← an i))) ≤ c i
+    c< zero = ≤-refl
+    c< (suc i) = x≤max _ _
+
+    c-mono : {i n : ℕ} → i ≤ n → c i ≤ c n
+    c-mono {zero} {zero} z≤n = ≤-refl
+    c-mono {zero} {suc n} z≤n = ≤-trans (c-mono {zero} {n} z≤n) (y≤max _ _ )
+    c-mono {suc i} {suc n} (s≤s i≤n) with <-cmp (fun→ cn (g (f (fun← an (suc i))))) (c i)
+    ... | tri< a ¬b ¬c = subst (λ k → k ≤ _ ) (sym (x≤y→max=y _ _ (≤-trans a≤sa a ))) (≤-trans ( c-mono {i} {n} i≤n ) ( y≤max _ _ ))
+    ... | tri≈ ¬a b ¬c = subst (λ k → k ≤ _ ) (sym (x≤y→max=y _ _ (subst (λ k → k ≤ c i) (sym b) ≤-refl ))) 
+         (≤-trans ( c-mono {i} {n} i≤n ) ( y≤max _ _ ))
+    ... | tri> ¬a ¬b c₁ = ≤-trans (≤-trans ? ( c< (suc i) )) ?
 
     inject-cgf : {i j : ℕ} → fun→ cn (g (f (fun← an i))) ≡ fun→ cn (g (f (fun← an j))) → i ≡ j
     inject-cgf {i} {j} eq = bi-inject← an (InjectiveF.inject fi (InjectiveF.inject gi ( bi-inject→ cn eq )))
@@ -585,27 +596,30 @@
     -- if a list contains n different A, length of list is greater than n
 
     record NL (n : ℕ) : Set where
-       field 
-          nlist : List A
-          anyn : (i : ℕ) → i ≤ n →  Any (λ y → fun← an i ≡ y) nlist
+       field
+          nlist : List C
+          anyn : (i : ℕ) → i ≤ n →  Any (λ y → g ( f (fun← an i)) ≡ y) nlist
 
-    remove-n : (n : ℕ) → List A → List A
+    ncfi = λ n → (fun→ cn (g (f (fun← an n) )))
+    cfi = λ n → (g (f (fun← an n) ))
+
+    remove-n : (n : ℕ) → List C → List C
     remove-n n [] = []
-    remove-n n (h ∷ t ) with <-cmp n (fun→ an h)
+    remove-n n (h ∷ t ) with <-cmp (fun→ cn (g (f (fun← an n) ))) (fun→ cn h)
     ... | tri< a ¬b ¬c = t
     ... | tri≈ ¬a b ¬c = h ∷ remove-n n t
     ... | tri> ¬a ¬b c₁ = h ∷ remove-n n t
 
     NL-1 : (n : ℕ) → NL (suc n) → NL n
     NL-1 n nl = record { nlist = remove-n n (NL.nlist nl) ; anyn = ? } where
-        nl03 : (i : ℕ) → i ≤ n → Any (_≡_ (fun← an i)) (remove-n n (NL.nlist nl))
+        nl03 : (i : ℕ) → i ≤ n → Any (_≡_ (cfi i)) (remove-n n (NL.nlist nl))
         nl03 i i≤n = nl04 _ (NL.anyn nl i ? )  where
-           nl04 : (x : List A) → Any (_≡_ (fun← an i)) x → Any (_≡_ (fun← an i)) (remove-n n x)
-           nl04 (h ∷ t) (here px) with <-cmp n (fun→ an h)
+           nl04 : (x : List C) → Any (_≡_ (cfi i)) x → Any (_≡_ (cfi i)) (remove-n n x)
+           nl04 (h ∷ t) (here px) with <-cmp (ncfi n) (fun→ cn h)
            ... | tri< a ¬b ¬c = ?
            ... | tri≈ ¬a b ¬c = here px
            ... | tri> ¬a ¬b c₁ = here px
-           nl04 (h ∷ t) (there a) with <-cmp n (fun→ an h)
+           nl04 (h ∷ t) (there a) with <-cmp (ncfi n) (fun→ cn h)
            ... | tri< a ¬b ¬c = ?
            ... | tri≈ ¬a b ¬c = there (nl04 t a)
            ... | tri> ¬a ¬b c₁ = there (nl04 t a)
@@ -613,34 +627,71 @@
     n<list : (n : ℕ) → (nl : NL n) → n < length (NL.nlist nl)
     n<list 0 nl = ?
     n<list (suc zero) nl = ?
-    n<list (suc (suc n)) nl = nl03 (suc n) ? ? where
+    n<list (suc (suc n)) nl = ? where -- nl03 (suc n) ? ? where
         nl00 : (n : ℕ ) → (nl : NL (suc n))  → length (NL.nlist (NL-1 _ nl )) < length (NL.nlist nl )
         nl00 n nl = nl02 n (NL.nlist nl) (NL.anyn nl n ? )  where
-           nl02 : (n : ℕ) (x : List A) → Any (λ y → fun← an n ≡ y) x → length (remove-n n x) < length x
-           nl02 n (h ∷ ta) (here px) with <-cmp n (fun→ an h)
+           nl02 : (n : ℕ) (x : List C) → Any (λ y → g ( f (fun← an n)) ≡ y) x → length (remove-n n x) < length x
+           nl02 n (h ∷ ta) (here px) with <-cmp (ncfi n) (fun→ cn h)
            ... | tri< a ¬b ¬c = ≤-refl
            ... | tri≈ ¬a b ¬c = ?
            ... | tri> ¬a ¬b c₁ = ?
-           nl02 n (h ∷ ta) (there a) with <-cmp n (fun→ an h)
+           nl02 n (h ∷ ta) (there a) with <-cmp (ncfi n) (fun→ cn h)
            ... | tri< a ¬b ¬c = ≤-refl
            ... | tri≈ ¬a b ¬c = s≤s (nl02 n ta a)
            ... | tri> ¬a ¬b c₁ = s≤s (nl02 n ta a)
-        nl03 : (i : ℕ) → i ≤ suc n → (nl : NL i) → suc i < length (NL.nlist nl)
-        nl03 0 i≤sn nl = ?
+        nl04 : (nl : NL 0) → 1 ≤ length (NL.nlist nl)
+        nl04 nl = ?
+        nl03 : (i : ℕ) → i ≤ suc n → (nl : NL i) → suc i ≤ length (NL.nlist nl)
+        nl03 0 i≤sn nl = nl04 nl
         nl03 (suc i) i≤sn nl = begin
             ? ≤⟨ ? ⟩
-            suc i <⟨ nl03 i ? (NL-1 _ nl ) ⟩
+            suc i ≤⟨ nl03 i ? (NL-1 _ nl ) ⟩
             length (NL.nlist (NL-1 _ nl )) <⟨ nl00 _ nl ⟩
-            length (NL.nlist nl) ∎  where 
+            length (NL.nlist nl) ∎  where
                open ≤-Reasoning
 
+    acNL : (n : ℕ ) → NL n
+    acNL zero = record { nlist = g (f (fun← an zero)) ∷ [] ; anyn = lem00 } where
+        lem00 : (i : ℕ) → i ≤ zero → Any (_≡_ (g (f (fun← an i)))) (g ( f (fun← an zero)) ∷ [])
+        lem00 zero z≤n = here refl
+    acNL (suc n) = record { nlist = g (f (fun← an (suc n))) ∷ NL.nlist (acNL n) ; anyn = lem00 } where
+        lem00 : (i : ℕ) → i ≤ suc n → Any (_≡_ (g (f ((fun← an i))))) ((g ( f (fun← an (suc n)))) ∷ NL.nlist (acNL n))
+        lem00 i le with ≤-∨ le
+        ... | case1 eq = here (cong (λ k → g (f (fun← an k))) eq )
+        ... | case2 (s≤s le) = there (NL.anyn (acNL n) _ le)
+
+    clist : (n : ℕ) → List C
+    clist 0 = fun← cn 0 ∷ []
+    clist (suc n) = fun← cn (suc n) ∷ clist n
+
+    clist-more : {i j : ℕ} → i ≤ j → {c : C} →  Any (_≡_ c) (clist i) →  Any (_≡_ c) (clist j)
+    clist-more {zero} {zero} z≤n a = a
+    clist-more {zero} {suc n} i≤n a = there (clist-more {zero} {n} z≤n a)
+    clist-more {suc i} {suc n} (s≤s le) {c} (there a) = there (clist-more {i} {n} le a)
+    clist-more {suc i} {suc n} (s≤s le) {c} (here px) with ≤-∨ le
+    ... | case1 refl = here px
+    ... | case2 lt = there (clist-more {suc i} {n} lt {c} (here px) )
+
+    clist-any : (n i : ℕ) → i ≤ n → Any (_≡_ (g (f (fun← an i)))) (clist (c n))
+    clist-any n i i≤n = clist-more ? (lem00 (c i) (c< i))   where
+        lem00 : (j : ℕ ) → fun→ cn (g (f (fun← an i))) ≤ j → Any (_≡_ (g (f (fun← an i)))) (clist j)
+        lem00 0 f≤j with  ≤-∨ f≤j
+        ... | case1 eq = here ( trans (sym (fiso← cn _)) ( cong (fun← cn) eq ))
+        ... | case2 le = ⊥-elim (nat-≤> z≤n le )
+        lem00 (suc j) f≤j with  ≤-∨ f≤j
+        ... | case1 eq = here ( trans (sym (fiso← cn _)) ( cong (fun← cn) eq ))
+        ... | case2 (s≤s le) = there (lem00 j le)
+
+    cNL : (n : ℕ ) → NL n
+    cNL n = record { nlist = clist (c n) ; anyn = λ i le → clist-any n i le } 
+
     record maxAC (n : ℕ) : Set where
        field
            ac : ℕ
            n<ca : n < count-A ac
 
     lem02 : (n : ℕ) → maxAC n
-    lem02 n = record { ac = ? ; n<ca = ? }
+    lem02 n = record { ac = c n ; n<ca = ? }
 
     record CountB (n : ℕ) : Set where
        field
diff -r 0472bfb4964e -r 9130c44031a5 src/nat.agda
--- a/src/nat.agda	Mon Jun 19 17:57:43 2023 +0900
+++ b/src/nat.agda	Tue Jun 20 12:14:12 2023 +0900
@@ -71,6 +71,17 @@
 y≤max (suc x) zero = z≤n
 y≤max (suc x) (suc y) = s≤s( y≤max x y )
 
+x≤y→max=y : (x y : ℕ) → x ≤ y → max x y ≡ y
+x≤y→max=y zero zero x≤y = refl
+x≤y→max=y zero (suc y) x≤y = refl
+x≤y→max=y (suc x) (suc y) (s≤s x≤y) = cong suc (x≤y→max=y x y x≤y )
+
+y≤x→max=x : (x y : ℕ) → y ≤ x → max x y ≡ x
+y≤x→max=x zero zero y≤x = refl
+y≤x→max=x zero (suc y) ()
+y≤x→max=x (suc x) zero lt = refl
+y≤x→max=x (suc x) (suc y) (s≤s y≤x) = cong suc (y≤x→max=x x y y≤x )
+
 -- _*_ : ℕ → ℕ → ℕ
 -- _*_ zero _ = zero
 -- _*_ (suc n) m = m + ( n * m )