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

changeset 1349:f5048a51d19f

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 Sun, 18 Jun 2023 06:00:57 +0900
parents c42647780620
children 575777026a72
files src/bijection.agda
diffstat 1 files changed, 64 insertions(+), 34 deletions(-) [+]
line wrap: on
line diff
--- a/src/bijection.agda	Sun Jun 18 05:02:01 2023 +0900
+++ b/src/bijection.agda	Sun Jun 18 06:00:57 2023 +0900
@@ -682,13 +682,13 @@
         m<i = begin
            suc (fun→ cn (g (f (fun← an (suc n)))))  ≤⟨ s≤s (x≤max _ _) ⟩
            suc (max (fun→ cn (g (f (fun← an (suc n))))) (c n))  ≤⟨ cn<i ⟩
-           i ∎ where 
+           i ∎ where
              open ≤-Reasoning
         c102 : c n < i
         c102 = begin
            suc (c n)  ≤⟨ s≤s (y≤max _ _) ⟩
            suc (max (fun→ cn (g (f (fun← an (suc n))))) (c n))  ≤⟨ cn<i ⟩
-           i ∎ where 
+           i ∎ where
              open ≤-Reasoning
         c101 : c1 (suc n) i ≡ suc (suc n)
         c101 with <-cmp (fun→ cn (g (f (fun← an (suc n))))) i
@@ -696,14 +696,14 @@
         ... | tri≈ ¬a b ¬c = cong suc (c1-max n i c102 )
         ... | tri> ¬a ¬b c₁ = ⊥-elim ( nat-<> c₁ m<i )
 
-    gf-is-a :  (i : ℕ) → Is A C (λ i → g (f i)) (g (f (fun← an i))) 
+    gf-is-a :  (i : ℕ) → Is A C (λ i → g (f i)) (g (f (fun← an i)))
     gf-is-a i = record { a = fun← an i ; fa=c = refl }
 
     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 ))) 
-    
+    inject-cgf {i} {j} eq = bi-inject← an (InjectiveF.inject fi (InjectiveF.inject gi ( bi-inject→ cn eq )))
+
     ani : (i : ℕ) → ℕ
-    ani i = fun→ cn (g (f (fun← an i))) 
+    ani i = fun→ cn (g (f (fun← an i)))
 
     i-in-n : (i n : ℕ) → i ≤ n → Set
     i-in-n i n i≤n = c1 n (suc (c n)) ≤ i
@@ -715,8 +715,8 @@
     ... | tri≈ ¬a n=an ¬c = suc (c1 n i) ≡ c1 n (suc i)
     ... | tri> ¬a ¬b an<n = suc (c1 n i) ≡ c1 n (suc i)
 
-    c1+1 : (n i : ℕ) → (isa : Is A C (λ x → g (f x)) (fun← cn (suc i))) 
-        →  c1+1P n i isa 
+    c1+1 : (n i : ℕ) → (isa : Is A C (λ x → g (f x)) (fun← cn (suc i)))
+        →  c1+1P n i isa
     c1+1 0 i isa with <-cmp 0 (fun→  an (Is.a isa))
     ... | tri< n<an ¬b ¬c = c123 where
          c123 : c1 zero i ≡ c1 zero (suc i)
@@ -729,7 +729,7 @@
          ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c₁ = ⊥-elim ( nat-≤> (subst (λ k → k ≤ _) (sym b) a≤sa ) c₁  )
          ... | tri> ¬a ¬b c₁ | tri< a ¬b₁ ¬c = ⊥-elim ( nat-≤> a (s≤s c₁))
          ... | tri> ¬a ¬b c₁ | tri> ¬a₁ ¬b₁ c₂ = refl
-         ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c = ⊥-elim ( nat-≡< c126 n<an ) where 
+         ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c = ⊥-elim ( nat-≡< c126 n<an ) where
                open ≡-Reasoning
                c127 : fun→ cn (g (f (fun← an (fun→ an (Is.a isa))))) ≡ fun→ cn (g (f (fun← an 0)))
                c127 = begin
@@ -737,11 +737,11 @@
                   fun→ cn (g (f (Is.a isa))) ≡⟨ cong (fun→ cn) (Is.fa=c isa) ⟩
                   fun→ cn (fun← cn (suc i)) ≡⟨ fiso→ cn _ ⟩
                   suc i ≡⟨ sym b ⟩
-                  fun→ cn (g (f (fun← an 0))) ∎ 
+                  fun→ cn (g (f (fun← an 0))) ∎
                c126 : 0 ≡ fun→ an (Is.a isa)
                c126 = begin
                   0 ≡⟨ sym ( inject-cgf c127) ⟩
-                  fun→ an (Is.a isa) ∎ 
+                  fun→ an (Is.a isa) ∎
     ... | tri≈ ¬a n=an ¬c = c124 where
          open ≡-Reasoning
          c125 : fun→ cn (g (f (fun← an 0))) ≡ suc i
@@ -750,7 +750,7 @@
             fun→ cn (g (f (fun← an (fun→ an (Is.a isa))))) ≡⟨  cong (λ k → fun→ cn (g (f k))) (fiso← an _) ⟩
             fun→ cn (g (f (Is.a isa))) ≡⟨ cong (fun→ cn) (Is.fa=c isa) ⟩
             fun→ cn (fun← cn (suc i)) ≡⟨ fiso→ cn _ ⟩
-            suc i ∎ 
+            suc i ∎
          c124 : suc (c1 zero i) ≡ c1 zero (suc i)
          c124 with <-cmp (ani 0) i | <-cmp (ani 0) (suc i)
          ... | tri< a ¬b ¬c | _ = ⊥-elim ( nat-≤> a (<-trans a<sa (subst (λ k → suc i < suc k ) (sym c125) (s≤s a<sa) )))
@@ -774,7 +774,7 @@
          ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = cong suc c110
          ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ = cong suc c110
          ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c₁ = ⊥-elim ( nat-≤> (subst (λ k → k ≤ _) (sym b) a≤sa ) c₁  )
-         ... | tri> ¬a ¬b c₁ | tri< (s≤s a) ¬b₁ ¬c = ⊥-elim (nat-≡< refl (<-transˡ c₁ a)) 
+         ... | tri> ¬a ¬b c₁ | tri< (s≤s a) ¬b₁ ¬c = ⊥-elim (nat-≡< refl (<-transˡ c₁ a))
          ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c = ⊥-elim (nat-≡< c130 n<an) where
               c118 : fun→ cn (g (f (fun← an (suc n)))) ≡ suc i
               c118 = b
@@ -783,10 +783,10 @@
                   fun→ cn (g (f (fun← an (fun→ an (Is.a isa)))))  ≡⟨ cong (λ k → fun→ cn (g (f k))) (fiso← an _) ⟩
                   fun→ cn (g (f (Is.a isa))) ≡⟨ cong (fun→ cn) (Is.fa=c isa) ⟩
                   fun→ cn (fun← cn (suc i)) ≡⟨ fiso→ cn _ ⟩
-                  suc i ∎ 
-              c130 : suc n ≡ fun→ an (Is.a isa) 
+                  suc i ∎
+              c130 : suc n ≡ fun→ an (Is.a isa)
               c130 = inject-cgf (trans c118 (sym c128 ))
-         ... | tri> ¬a ¬b c₁ | tri> ¬a₁ ¬b₁ c₂ = c110 
+         ... | tri> ¬a ¬b c₁ | tri> ¬a₁ ¬b₁ c₂ = c110
     ... | tri≈ ¬a n=an ¬c = c115 where
          c111 : c1 n i ≡ c1 n (suc i)
          c111 with <-cmp n (fun→  an (Is.a isa)) | c1+1 n i isa
@@ -799,20 +799,20 @@
               fun→ cn (g (f (fun← an (fun→ an (Is.a isa)))))  ≡⟨ cong (λ k → fun→ cn (g (f k))) (fiso← an _) ⟩
               fun→ cn (g (f (Is.a isa))) ≡⟨ cong (fun→ cn) (Is.fa=c isa) ⟩
               fun→ cn (fun← cn (suc i)) ≡⟨ fiso→ cn _ ⟩
-              suc i ∎ 
+              suc i ∎
          c129 : fun→ cn (g (f (fun← an (suc n))))  ≡ suc i
          c129 = begin
               fun→ cn (g (f (fun← an (suc n))))  ≡⟨ cong (λ k → fun→ cn (g (f (fun← an k)))) n=an ⟩
               fun→ cn (g (f (fun← an (fun→ an (Is.a isa)))))  ≡⟨ cong (λ k → fun→ cn (g (f k))) (fiso← an _) ⟩
               fun→ cn (g (f (Is.a isa))) ≡⟨ cong (fun→ cn) (Is.fa=c isa) ⟩
               fun→ cn (fun← cn (suc i)) ≡⟨ fiso→ cn _ ⟩
-              suc i ∎ 
+              suc i ∎
          c115 : suc (c1 (suc n) i) ≡ c1 (suc n) (suc i)
          c115 with <-cmp (ani (suc n)) i | <-cmp (ani (suc n)) (suc i)
          ... | tri< a ¬b ¬c | _ = ⊥-elim ( nat-≡< c129 (<-trans a a<sa ))
          ... | tri≈ ¬a b ¬c | _ = ⊥-elim ( nat-≡< (trans (sym b) c129) a<sa )
-         ... | tri> ¬a ¬b c₁ | tri< (s≤s a) ¬b₁ ¬c = ⊥-elim (nat-≡< refl (<-transˡ c₁ a)) 
-         ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c = cong suc c111 
+         ... | tri> ¬a ¬b c₁ | tri< (s≤s a) ¬b₁ ¬c = ⊥-elim (nat-≡< refl (<-transˡ c₁ a))
+         ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c = cong suc c111
          ... | tri> ¬a ¬b c₁ | tri> ¬a₁ ¬b₁ c₂ = ⊥-elim ( nat-≡< (sym c129) c₂ )
     ... | tri> ¬a ¬b an<n = c115 where
          c112 : suc (c1 n i) ≡ c1 n (suc i)
@@ -829,7 +829,7 @@
          ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = cong suc c112
          ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ = cong suc c112
          ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c₁ = ⊥-elim ( nat-≤> (subst (λ k → k ≤ _) (sym b) a≤sa ) c₁  )
-         ... | tri> ¬a ¬b c₁ | tri< (s≤s a) ¬b₁ ¬c = ⊥-elim (nat-≡< refl (<-transˡ c₁ a)) 
+         ... | tri> ¬a ¬b c₁ | tri< (s≤s a) ¬b₁ ¬c = ⊥-elim (nat-≡< refl (<-transˡ c₁ a))
          ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c = ⊥-elim ( nat-≡< (sym c130) an<n )  where
               c118 : fun→ cn (g (f (fun← an (suc n)))) ≡ suc i
               c118 = b
@@ -838,8 +838,8 @@
                   fun→ cn (g (f (fun← an (fun→ an (Is.a isa)))))  ≡⟨ cong (λ k → fun→ cn (g (f k))) (fiso← an _) ⟩
                   fun→ cn (g (f (Is.a isa))) ≡⟨ cong (fun→ cn) (Is.fa=c isa) ⟩
                   fun→ cn (fun← cn (suc i)) ≡⟨ fiso→ cn _ ⟩
-                  suc i ∎ 
-              c130 : suc n ≡ fun→ an (Is.a isa) 
+                  suc i ∎
+              c130 : suc n ≡ fun→ an (Is.a isa)
               c130 = inject-cgf (trans c118 (sym c128 ))
          ... | tri> ¬a ¬b c₁ | tri> ¬a₁ ¬b₁ c₂ = c112
 
@@ -851,16 +851,28 @@
     ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ =  refl
     ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ =  refl
     ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c₁ = ⊥-elim ( nat-≤> (subst (λ k → k ≤ _) (sym b) a≤sa) c₁  )
-    ... | tri> ¬a ¬b c₁ | tri< a ¬b₁ ¬c = ?
-    ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c = ?
+    ... | tri> ¬a ¬b c₁ | tri< a ¬b₁ ¬c = ⊥-elim ( nat-≤> a (s≤s c₁))
+    ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c = ⊥-elim ( nisa record { a = fun← an 0 ; fa=c = c00 } ) where
+           open ≡-Reasoning
+           c00 : g (f (fun← an 0)) ≡ fun← cn (suc i)
+           c00 = begin
+              g (f (fun← an 0)) ≡⟨ sym (fiso← cn _) ⟩
+              fun← cn (fun→ cn (g (f (fun← an 0))))  ≡⟨ cong (fun← cn) b ⟩
+              fun← cn (suc i) ∎
     ... | tri> ¬a ¬b c₁ | tri> ¬a₁ ¬b₁ c₂ =  refl
     c1+0 {suc n} {zero}  nisa with <-cmp (fun→ cn (g (f (fun← an (suc n))))) zero  | <-cmp (fun→ cn (g (f (fun← an (suc n))))) (suc zero)
         | c1+0 {n} {zero} nisa
     ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ | eq =  (cong suc eq)
     ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ | eq =  (cong suc eq)
     ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c₁ | _ = ⊥-elim ( nat-≡< (sym b) (≤-trans (s≤s z≤n) c₁)  )
-    ... | tri> ¬a ¬b c₁ | tri< a ¬b₁ ¬c | eq = ?
-    ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c | eq = ?
+    ... | tri> ¬a ¬b c₁ | tri< a ¬b₁ ¬c | eq = ⊥-elim ( nat-≤> a (s≤s c₁))
+    ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c | eq = ⊥-elim ( nisa record { a = fun← an (suc n) ; fa=c = c00 } ) where
+           open ≡-Reasoning
+           c00 : g (f (fun← an (suc n))) ≡ fun← cn 1
+           c00 = begin
+              g (f (fun← an (suc n))) ≡⟨ sym (fiso← cn _) ⟩
+              fun← cn (fun→ cn (g (f (fun← an (suc n)))))  ≡⟨ cong (fun← cn) b ⟩
+              fun← cn 1 ∎
     ... | tri> ¬a ¬b c₁ | tri> ¬a₁ ¬b₁ c₂ | eq =  eq
     c1+0 {suc n} {suc i}  nisa with <-cmp (fun→ cn (g (f (fun← an (suc n))))) (suc i) | <-cmp (fun→ cn (g (f (fun← an (suc n))))) (suc (suc i))
          | c1+0 {n} {suc i}  nisa
@@ -870,15 +882,33 @@
     ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ | eq = cong suc eq
     ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ | eq =  cong suc eq
     ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c₁ | u = ⊥-elim ( nat-≤> (subst (λ k → k ≤ _) (sym b) a≤sa) c₁  )
-    ... | tri> ¬a ¬b c₁ | tri< a ¬b₁ ¬c | eq = ?
-    ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c | eq = ?
+    ... | tri> ¬a ¬b c₁ | tri< a ¬b₁ ¬c | eq = ⊥-elim ( nat-≤> a (s≤s c₁))
+    ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c | eq = ⊥-elim ( nisa record { a = fun← an (suc n) ; fa=c = c00 } ) where 
+           open ≡-Reasoning
+           c00 : g (f (fun← an (suc n))) ≡ fun← cn (suc (suc i))
+           c00 = begin
+              g (f (fun← an (suc n))) ≡⟨ sym (fiso← cn _) ⟩
+              fun← cn (fun→ cn (g (f (fun← an (suc n)))))  ≡⟨ cong (fun← cn) b ⟩
+              fun← cn (suc (suc i)) ∎
     ... | tri> ¬a ¬b c₁ | tri> ¬a₁ ¬b₁ c₂ | u = u
 
-    c1<count-A : (n i : ℕ) → c1 n i < count-A i
-    c1<count-A n zero with is-A (fun← cn zero) 
-    ... | no nisa = ?
-    ... | yes isa = ?
-    c1<count-A n (suc i) = ?
+    c1<count-A : (n i : ℕ) → c1 n i ≤ count-A i
+    c1<count-A zero zero with is-A (fun← cn zero) |  <-cmp (fun→ cn (g (f (fun← an zero)))) zero
+    ... | no nisa | tri≈ ¬a b ¬c = ⊥-elim ( nisa record { a = fun← an 0 ; fa=c = trans (sym (fiso← cn _)) (cong (fun← cn) b) })
+    ... | no nisa | tri> ¬a ¬b c₁ = ≤-refl
+    ... | yes isa | tri≈ ¬a b ¬c = ≤-refl
+    ... | yes isa | tri> ¬a ¬b c₁ = a≤sa
+    c1<count-A (suc n) zero with is-A (fun← cn zero) |  <-cmp (fun→ cn (g (f (fun← an (suc n))))) zero
+    ... | no nisa | s = ?
+    ... | yes isa | tri≈ ¬a b ¬c = ? where
+         -- only one a in c1 n loop
+         lem00 : c1 n zero ≤ count-A zero
+         lem00 = c1<count-A n zero
+    ... | yes isa | tri> ¬a ¬b c₁ = ?
+    c1<count-A zero (suc i) = ?
+    c1<count-A (suc n) (suc i) with is-A (fun← cn zero) |  <-cmp (fun→ cn (g (f (fun← an (suc n))))) zero
+    ... | no nisa | t = ?
+    ... | yes isa | t = ?
 
     record maxAC (n : ℕ) : Set where
        field