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

changeset 1365:4e1150abfb86

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, 20 Jun 2023 19:24:48 +0900
parents ea44c917ca61
children 07fe8f8bb6d3
files src/bijection.agda
diffstat 1 files changed, 51 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/src/bijection.agda	Tue Jun 20 15:11:47 2023 +0900
+++ b/src/bijection.agda	Tue Jun 20 19:24:48 2023 +0900
@@ -651,7 +651,7 @@
 
     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 : (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))
@@ -681,8 +681,56 @@
         ... | 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 } 
+    -- cNL : (n : ℕ ) → NL n
+    -- cNL n = record { nlist = clist (c n) ; anyn = λ i le → clist-any n i le } 
+
+
+    ca-list : List C → ℕ
+    ca-list [] = 0
+    ca-list (h ∷ t) with is-A h
+    ... | yes _ = suc (ca-list t)
+    ... | no _ = ca-list t
+
+    ca-list=count-A : (n : ℕ) → ca-list (clist n) ≡ count-A n
+    ca-list=count-A n = lem02 n (clist n) refl  where
+        lem02 : (n : ℕ) → (cl : List C) → cl ≡ clist n → ca-list cl ≡ count-A n
+        lem02 zero [] ()
+        lem02 zero (h ∷ t) refl with is-A (fun← cn zero)
+        ... | yes _ = refl
+        ... | no _ = refl
+        lem02 (suc n) (h ∷ t) refl with is-A (fun← cn (suc n)) 
+        ... | yes _ = cong suc (lem02 n t refl)
+        ... | no _ = lem02 n t refl
+
+    a-list : (i : ℕ) → (cl : List C) → Any (_≡_ (g (f (fun← an i)))) cl → List C
+    a-list i (_ ∷ t) (here px) = t
+    a-list i (h ∷ t) (there a) = h ∷ ( a-list i t a )
+
+    a-list-ca : (i : ℕ) → (cl : List C) → (a : Any (_≡_ (g (f (fun← an i)))) cl ) 
+        → suc (ca-list (a-list i cl a)) ≡ ca-list cl
+    a-list-ca i cl a = lem03 i cl _ a refl where
+         lem03 : (i : ℕ) → (cl cal : List C) → (a : Any (_≡_ (g (f (fun← an i)))) cl )  → cal ≡  (a-list i cl a) → suc (ca-list cal)  ≡ ca-list cl
+         lem03 i (h ∷ t) (h1 ∷ t1) (here px) refl with is-A h
+         ... | yes _ = refl
+         ... | no nisa = ⊥-elim ( nisa record { a = _ ; fa=c = px } )
+         lem03 i (h ∷ t) (h ∷ t1) (there ah) refl with is-A h
+         ... | yes y = cong suc (lem03 i t t1 ah refl)
+         ... | no _ = lem03 i t t1 ah refl
+         lem03 i (x ∷ []) [] (here px) refl with is-A x
+         ... | yes y = refl
+         ... | no nisa = ⊥-elim ( nisa record { a = _ ; fa=c = px } )
+
+    n<ca-list : (n : ℕ) → n < ca-list (clist (c n))
+    n<ca-list zero = subst ( λ k → zero < k ) (a-list-ca zero (clist (c zero)) (clist-any zero zero ≤-refl)) ( <-transˡ a<sa (s≤s z≤n )) 
+    n<ca-list (suc n) = begin
+         suc (suc n) ≤⟨ (s≤s (n<ca-list n)) ⟩ 
+         suc (ca-list (clist (c n))) ≡⟨ ? ⟩ 
+         suc (ca-list (a-list (suc n) (clist (c (suc n))) (clist-any (suc n) (suc n) ≤-refl)))
+             ≡⟨ a-list-ca (suc n) (clist (c (suc n))) (clist-any (suc n) (suc n) ≤-refl) ⟩ 
+         ca-list (clist (c (suc n))) ∎ where open ≤-Reasoning
+
+    n<ca0 : {n : ℕ} → n < count-A (c n)
+    n<ca0 = ? 
 
     record maxAC (n : ℕ) : Set where
        field