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

changeset 1347:9a14ef021f8f

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 Sat, 17 Jun 2023 19:08:46 +0900
parents 79c1c3baba55
children c42647780620
files src/bijection.agda
diffstat 1 files changed, 81 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/src/bijection.agda	Sat Jun 17 17:01:23 2023 +0900
+++ b/src/bijection.agda	Sat Jun 17 19:08:46 2023 +0900
@@ -742,26 +742,103 @@
                c126 = begin
                   0 ≡⟨ sym ( inject-cgf c127) ⟩
                   fun→ an (Is.a isa) ∎ 
-    ... | tri≈ ¬a n=an ¬c = ?
+    ... | tri≈ ¬a n=an ¬c = c124 where
+         open ≡-Reasoning
+         c125 : fun→ cn (g (f (fun← an 0))) ≡ suc i
+         c125 = begin
+            fun→ cn (g (f (fun← an 0))) ≡⟨ 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 ∎ 
+         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) )))
+         ... | tri≈ ¬a b ¬c | _ = ⊥-elim ( nat-≡< (sym b) (subst (λ k → i < k) (sym c125) a<sa ))
+         ... | 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 ( ¬b₁ c125 )
     c1+1 (suc n) i isa with <-cmp (suc n) (fun→  an (Is.a isa))
-    ... | tri< n<an ¬b ¬c = ? where
+    ... | tri< n<an ¬b ¬c = c115 where
+         open ≡-Reasoning
          c110 : c1 n i ≡ c1 n (suc i)
          c110 with <-cmp n (fun→  an (Is.a isa)) | c1+1 n i isa
          ... | tri< a ¬b ¬c | s = s
          ... | tri≈ ¬a b ¬c | s = ⊥-elim ( nat-≡< b (<-trans a<sa n<an ))
          ... | tri> ¬a ¬b c₁ | s = ⊥-elim ( nat-≤> c₁ (<-trans (<-trans a<sa a<sa) (<-transʳ n<an a<sa ) ))
-    ... | tri≈ ¬a n=an ¬c = ? where
+         c115 : 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 | 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-≤> a≤sa (<-transˡ c₁ (≤-trans refl-≤s a ) ))
+         ... | 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≈ ¬a₁ b ¬c = ⊥-elim (nat-≡< c130 n<an) where
+              c118 : fun→ cn (g (f (fun← an (suc n)))) ≡ suc i
+              c118 = b
+              c128 : fun→ cn (g (f (fun← an (fun→ an (Is.a isa)))))  ≡ suc i
+              c128 = begin
+                  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) 
+              c130 = inject-cgf (trans c118 (sym c128 ))
+         ... | 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
          ... | tri< a ¬b ¬c | s = s
          ... | tri≈ ¬a b ¬c | s = ⊥-elim ( nat-≡< b (subst (λ k → n < k ) n=an a<sa ))
          ... | tri> ¬a ¬b c₁ | s = ⊥-elim ( nat-≡< (sym n=an) (<-trans c₁ a<sa ))
-    ... | tri> ¬a ¬b an<j = ? where
+         open ≡-Reasoning
+         c128 : fun→ cn (g (f (fun← an (fun→ an (Is.a isa)))))  ≡ suc i
+         c128 = begin
+              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 ∎ 
+         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 | tri< a₁ ¬b₁ ¬c₁ = ?
+         ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = ?
+         ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c₁ = ⊥-elim ( nat-≤> a≤sa (<-transˡ c₁ (≤-trans refl-≤s a ) ))
+         ... | 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-≤> (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≈ ¬a₁ b ¬c = cong suc c111 
+         ... | tri> ¬a ¬b c₁ | tri> ¬a₁ ¬b₁ c₂ = ?
+    ... | tri> ¬a ¬b an<j = c115 where
          c112 : suc (c1 n i) ≡ c1 n (suc i)
          c112 with <-cmp n (fun→  an (Is.a isa)) | c1+1 n i isa
          ... | tri< a ¬b ¬c | s = ⊥-elim (nat-≤> an<j (<-transʳ a a<sa) )
          ... | tri≈ ¬a b ¬c | s = s
          ... | tri> ¬a ¬b c₁ | s = s
+         open ≡-Reasoning
+         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 | 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-≤> a≤sa (<-transˡ c₁ (≤-trans refl-≤s a ) ))
+         ... | 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≈ ¬a₁ b ¬c = ? where
+              c118 : fun→ cn (g (f (fun← an (suc n)))) ≡ suc i
+              c118 = b
+              c128 : fun→ cn (g (f (fun← an (fun→ an (Is.a isa)))))  ≡ suc i
+              c128 = begin
+                  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) 
+              c130 = inject-cgf (trans c118 (sym c128 ))
+         ... | tri> ¬a ¬b c₁ | tri> ¬a₁ ¬b₁ c₂ = c112
 
     record maxAC (n : ℕ) : Set where
        field