Mercurial > hg > Members > kono > Proof > ZF-in-agda

changeset 1328:17a8e67ec124

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 13 Jun 2023 08:42:46 +0900
parents b8f02f27d8eb
children 75894c1665f7
files src/bijection.agda
diffstat 1 files changed, 60 insertions(+), 12 deletions(-) [+]
line wrap: on
line diff
--- a/src/bijection.agda	Mon Jun 12 08:51:26 2023 +0900
+++ b/src/bijection.agda	Tue Jun 13 08:42:46 2023 +0900
@@ -514,7 +514,7 @@
    } where
     --
     --     an     f     g     cn
-    --   ℕ →   A  →  B  →  C  →   ℕ
+    --   ℕ ↔   A  →  B  →  C  ↔   ℕ
     --
     open Bijection
     f = InjectiveF.f fi
@@ -545,12 +545,12 @@
     ... | yes isb = suc (count-A n)
     ... | no nisb = count-A n
 
-    count-A-homo : {i j : ℕ} → i ≤ j → count-A i ≤ count-A j
-    count-A-homo {i} {j} i≤j with ≤-∨ i≤j
+    count-A-mono : {i j : ℕ} → i ≤ j → count-A i ≤ count-A j
+    count-A-mono {i} {j} i≤j with ≤-∨ i≤j
     ... | case1 refl = ≤-refl
     ... | case2 i<j = lem00 _ _ i<j where
          lem00 : (i j : ℕ) → i < j → count-A i ≤ count-A j
-         lem00 i (suc j) (s≤s i<j) = ≤-trans (count-A-homo i<j) (lem01 j) where
+         lem00 i (suc j) (s≤s i<j) = ≤-trans (count-A-mono i<j) (lem01 j) where
              lem01 : (j : ℕ) → count-A j ≤ count-A (suc j) 
              lem01 zero with is-A (fun← cn (suc zero))
              ... | yes isb = refl-≤s
@@ -775,16 +775,62 @@
          fa = flany n
          fm = fla-max n
          cm = count-A fm
-         c : FL fm → ℕ 
-         c fl = ?
-         cn<fm : (fl : FL fm) → c fl < fla-max n
+         flen =  Data.List.Fresh.length 
+         len=n : flen (FLany.flist fa) ≡ suc n
+         len=n = ?
+         flist-top : (fl : FList fm) → 0 < flen fl  → ℕ
+         flist-top [] ()
+         flist-top (cons (ca<n i x₁) fl x) _ = fun→ cn (g (f (fun← an i)))
+         n<ca1 : ( fl : FList fm) → (0<fl : 0 < flen fl ) → flen fl + count-A (flist-top fl 0<fl ) ≤ count-A fm
+         n<ca1 [] _ = ≤-trans ? ( count-A-mono {0} {fm} z≤n )
+         n<ca1 (cons (ca<n i ci≤fm) [] fr) 0<fl = ?
+         n<ca1 (cons (ca<n i ci≤fm) (cons a fl fr0) fr) 0<fl = ? where
+            lem10 : flen fl + count-A (flist-top fl ? ) ≤ count-A fm
+            lem10 = n<ca1 fl ?
+            lem11 : suc (suc ? + count-A (fun→ cn (g (f (fun← an i))))) ≤ count-A fm
+            lem11 = begin
+               ? ≡⟨ ? ⟩ 
+               suc (flen fl + count-A (fun→ cn (g (f (fun← an i))))) ≡⟨ refl ⟩ 
+               (1 + flen fl ) + count-A (fun→ cn (g (f (fun← an i)))) ≡⟨ cong (λ k → k + count-A (fun→ cn (g (f (fun← an i))))) (+-comm 1 _) ⟩ 
+               (flen fl + 1) + count-A (fun→ cn (g (f (fun← an i)))) ≡⟨ ( +-assoc ( flen fl) 1  _ ) ⟩ 
+               flen fl + (suc (count-A (fun→ cn (g (f (fun← an i)))))) ≡⟨ ? ⟩ 
+               flen fl + count-A (suc (fun→ cn (g (f (fun← an i))))) ≤⟨ ≤-plus-0 ( count-A-mono (lem12 fl ? )) ⟩ 
+               flen fl + count-A (flist-top fl ? ) ≤⟨ n<ca1 fl ? ⟩
+               count-A fm ∎ where
+                  open ≤-Reasoning
+                  lem12 : (fl : FList fm) → fresh (FL fm) ⌊ _f<?_ ⌋  _ fl  → suc (fun→ cn (g (f (fun← an i)))) ≤ flist-top fl ?
+                  lem12 (cons (ca<n j x₂) fl1 x1) (lift lt1 , fr2) = begin
+                     suc (fun→ cn (g (f (fun← an i)))) ≤⟨ ttf1 lt1  ⟩
+                     fun→ cn (g (f (fun← an j))) ∎ where 
+                        open ≤-Reasoning 
+                        ttf1 : True (ca<n i ci≤fm f<? ca<n j x₂) 
+                          →  suc (fun→ cn (g (f (fun← an i)))) ≤ fun→ cn (g (f (fun← an j)))
+                        ttf1 t = toWitness t
+                  lem12 [] (lift tt) = ?
+
+                  
+
+         c : {i : ℕ} → i < suc n → ℕ 
+         c {i} i<n = ?
+         cn<fm : { i : ℕ} → (i<n : i < suc n ) → c i<n < fla-max n
          cn<fm = ?
-         c-inc : (fl : FL fm) → suc (count-A (c fl)) ≡  count-A (suc (c fl)) 
+         c-inc :  { i : ℕ} → (i<n : i < suc n ) → suc (count-A (c i<n)) ≡  count-A (suc (c i<n)) 
          c-inc = ?
-         len=n : (x : FList fm) → Data.List.Fresh.length x ≡ suc n
-         len=n = ?
-         n<ca : (i j : ℕ) → j + i ≡ n → count-A j + i < count-A (fla-max n) 
-         n<ca i j j+i=n = ?
+         n<ca : (i : ℕ) →  (i<n : i < suc n ) → i + count-A (suc (c i<n)) ≤ n + count-A (fla-max n)
+         n<ca zero i<n = lem00 where
+            lem00 : 0 + count-A (c i<n) ≤ n + count-A (fla-max n)
+            lem00 = ?
+         n<ca (suc i) i<n  = lem03 where
+            lem01 : i + count-A (c i<n) ≤ n + count-A (fla-max n)
+            lem01 = n<ca i (<-trans a<sa i<n)
+            lem04 : i + count-A (suc (c i<n)) ≤ n + count-A (fla-max n) 
+            lem04 = ?
+            lem03 : suc (i + count-A (c i<n)) ≤ n + count-A (fla-max n) 
+            lem03 = begin
+                suc (i + count-A (c i<n)) ≤⟨ ? ⟩
+                suc (n + count-A (fla-max n)) ≤⟨ ? ⟩
+                n + count-A (fla-max n) ∎ where
+                   open ≤-Reasoning
 
     record CountB (n : ℕ) : Set where
        field
@@ -835,6 +881,8 @@
 open import Data.List.Properties
 open import Data.Maybe.Properties
 
+---   ℕ ⊆ 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
    f : List A → List (Maybe A)