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

changeset 1368:e5e592584382

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 Wed, 21 Jun 2023 13:24:54 +0900
parents f93ef96caeb7
children 43471e03d6fe
files src/bijection.agda
diffstat 1 files changed, 8 insertions(+), 96 deletions(-) [+]
line wrap: on
line diff
--- a/src/bijection.agda	Wed Jun 21 12:23:58 2023 +0900
+++ b/src/bijection.agda	Wed Jun 21 13:24:54 2023 +0900
@@ -592,73 +592,9 @@
     ani : (i : ℕ) → ℕ
     ani i = fun→ cn (g (f (fun← an i)))
 
-    -- if a list contains n different A, length of list is greater than n
-
-    record NL (n : ℕ) : Set where
-       field
-          nlist : List C
-          anyn : (i : ℕ) → i ≤ n →  Any (λ y → g ( f (fun← an i)) ≡ y) nlist
-
     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 (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 (_≡_ (cfi i)) (remove-n n (NL.nlist nl))
-        nl03 i i≤n = nl04 _ (NL.anyn nl i ? )  where
-           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 (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)
-
-    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 = ? 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 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 (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)
-        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 ) ⟩
-            length (NL.nlist (NL-1 _ nl )) <⟨ nl00 _ nl ⟩
-            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
@@ -741,27 +677,17 @@
     any-cl : (i : ℕ) → (cl : List C) → Set
     any-cl i cl = (j : ℕ) → j ≤ i → Any (_≡_ (g (f (fun← an j)))) cl
 
-    n<ca-list0 : (n : ℕ) → n < ca-list (clist (c n))
-    n<ca-list0 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-list0 (suc n) = lem06 where
+    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) = lem06 where
          --
          --  we have ANY i on i ≤ n, so we can remove n element from clist (c n)
          --  induction on n is no good, because (ani (suc n)) may happen in clist (c n)
          --  so we cannot recurse on n<ca-list itself.
          --
-         lem04 : (i : ℕ) → suc i ≤ n → (cl : List C) → suc i < ca-list cl → (ai : Any (_≡_ (g (f (fun← an i)))) cl)  → i < ca-list (a-list i cl ai)
-         lem04 0 0≤n cl i<c ai = sx≤py→x≤y ( begin
-             2 ≤⟨ i<c ⟩
-             ca-list cl  ≡⟨ sym (a-list-ca 0 cl ai) ⟩
-             suc (ca-list (a-list 0 cl ai)) ∎ ) where
-                 open ≤-Reasoning
-         lem04 (suc i) i≤n cl i<c ai = sx≤py→x≤y ( begin
-             suc (suc (suc i)) ≤⟨ ? ⟩ 
-             suc (ca-list (a-list (suc i) cl ai)) ∎ ) where 
-                 open ≤-Reasoning
          del : (i : ℕ) → (cl : List C) → any-cl (suc i) cl → List C   -- del 0 contains ani 0
          del = ?
-         del-any : (i : ℕ) → (cl : List C) → any-cl (suc i) cl  → any-cl i cl  
+         del-any : (i : ℕ) → (cl : List C) → (a : any-cl (suc i) cl)  → any-cl i (del i cl a )
          del-any = ?
          del-ca : (i : ℕ) → (cl : List C) → (a : any-cl (suc i) cl  )
               → suc (ca-list cl) ≡ ca-list (del i cl a)
@@ -769,28 +695,14 @@
          lem06 : suc n < ca-list (clist (c (suc n)))
          lem06 = lem31 where
             lem30 : (i : ℕ) → (cl : List C) → (i≤n : i ≤ suc n) → (a : any-cl (suc i) cl) → suc i < ca-list cl
-            lem30 i cl i≤n a = begin
-               suc (suc i)  ≤⟨ ? ⟩ 
+            lem30 0 cl i≤n a = ?
+            lem30 (suc i) cl i≤n a = begin
+               suc (suc (suc i))   ≤⟨ s≤s (lem30 i (del (suc i) cl  a  ) (≤-trans a≤sa i≤n) (del-any (suc i) cl a)) ⟩ 
+               suc (ca-list (del (suc i) cl a))  ≡⟨ del-ca (suc i) cl a ⟩ 
                ca-list cl ∎ where
                    open ≤-Reasoning
             lem31 : suc n < ca-list (clist (c (suc n)))
             lem31 = lem30 n (clist (c (suc n))) a≤sa (λ j le  → clist-any (suc n) j le )
-            lem07 : (i : ℕ) → (cl : List C) → (i≤n : i ≤ suc n) → (a : any-cl (suc i) cl) → i < ca-list (del i cl a)
-            lem07 0 cl le a = ?
-            lem07 (suc i) cl le a = sx≤py→x≤y ( begin
-                suc (suc (suc i)) ≤⟨ ? ⟩
-                suc (suc (ca-list cl)) ≡⟨ ? ⟩
-                ca-list (del (suc (suc i)) (del (suc i) cl a) ?)  ≡⟨ ? ⟩
-                suc (ca-list (del (suc i) cl a )) ∎ ) where
-                    open ≤-Reasoning
-                    lem08 : i < ca-list (del (suc i) cl a)                                           
-                    lem08 = lem07 i (del (suc i) cl a) (≤-trans a≤sa le) (del-any (suc i) cl a)      
-            lem10 : (n i : ℕ) → i ≤ n → Any (_≡_ (g (f (fun← an i)))) (clist (c n))
-            lem10 n i le = clist-any n i le
-            lem09 : any-cl (suc (suc n)) (clist (c (suc (suc n))))
-            lem09 i le = clist-any (suc (suc n)) i le
-    n<ca-list : (n : ℕ) → n < ca-list (clist (c n))
-    n<ca-list n = ? 
 
     n<ca0 : {n : ℕ} → n < count-A (c n)
     n<ca0 = ?