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

changeset 1346:79c1c3baba55

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
... 0 case on c1+1P
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 17 Jun 2023 17:01:23 +0900
parents 0ad61d75e488
children 9a14ef021f8f
files src/bijection.agda
diffstat 1 files changed, 18 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/src/bijection.agda	Sat Jun 17 11:05:09 2023 +0900
+++ b/src/bijection.agda	Sat Jun 17 17:01:23 2023 +0900
@@ -699,6 +699,9 @@
     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 ))) 
+    
     ani : (i : ℕ) → ℕ
     ani i = fun→ cn (g (f (fun← an i))) 
 
@@ -706,13 +709,13 @@
     i-in-n i n i≤n = c1 n (suc (c n)) ≤ i
 
     --- c1 n i
-    c1+1P : (n i : ℕ) → (isa : Is A C (λ x → g (f x)) (fun← cn i)) →  Set
+    c1+1P : (n i : ℕ) → (isa : Is A C (λ x → g (f x)) (fun← cn (suc i))) →  Set
     c1+1P n i isa with <-cmp n (fun→  an (Is.a isa))
     ... | tri< n<an ¬b ¬c = c1 n i ≡ c1 n (suc i)
     ... | 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 i)) 
+    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
@@ -725,8 +728,20 @@
          ... | 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 = ⊥-elim ( nat-≤> a (s≤s c₁))
-         ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c = ?     -- ani 0 ≡ suc i, ani ? ≡ i
          ... | tri> ¬a ¬b c₁ | tri> ¬a₁ ¬b₁ c₂ = refl
+         ... | 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
+                  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 ≡⟨ sym b ⟩
+                  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) ∎ 
     ... | tri≈ ¬a n=an ¬c = ?
     c1+1 (suc n) i isa with <-cmp (suc n) (fun→  an (Is.a isa))
     ... | tri< n<an ¬b ¬c = ? where