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

changeset 1357:29f686c654bf

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 Mon, 19 Jun 2023 11:22:29 +0900
parents e3302db6bbdc
children 4eac5585b6b1
files src/bijection.agda
diffstat 1 files changed, 27 insertions(+), 21 deletions(-) [+]
line wrap: on
line diff
--- a/src/bijection.agda	Mon Jun 19 08:11:48 2023 +0900
+++ b/src/bijection.agda	Mon Jun 19 11:22:29 2023 +0900
@@ -892,13 +892,13 @@
               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 zero zero with is-A (fun← cn zero) |  <-cmp (fun→ cn (g (f (fun← an zero)))) zero
+    c1<ca : (n i : ℕ) → c1 n i ≤ count-A i
+    c1<ca 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
+    c1<ca (suc n) zero with is-A (fun← cn zero) |  <-cmp (fun→ cn (g (f (fun← an (suc n))))) zero
     ... | no nisa | tri≈ ¬a b ¬c = ⊥-elim ( nisa record { a = fun← an (suc n) ; fa=c = trans (sym (fiso← cn _)) (cong (fun← cn) b ) } )
     ... | no nisa | tri> ¬a ¬b c₁ = lem01 n ≤-refl where
          lem01 : (i : ℕ) → i ≤ n → c1 i 0 ≤ 0
@@ -931,7 +931,7 @@
              ... | tri≈ ¬a bi2 ¬c = ⊥-elim (nat-≡< (sym (inject-cgf (trans bi (sym bi2)) )) (<-transʳ j≤i a<sa  ))
              lem02 (suc j) (s≤s j≤i) | tri> ¬a ¬b c₁ = lem02 j (≤-trans j≤i a≤sa)
          lem01 (suc i) (s≤s i≤n) | tri> ¬a ¬b c₁ = lem01 i (≤-trans i≤n a≤sa)
-    c1<count-A zero (suc i) with is-A (fun← cn (suc i)) |  <-cmp (fun→ cn (g (f (fun← an zero)))) (suc i)
+    c1<ca zero (suc i) with is-A (fun← cn (suc i)) |  <-cmp (fun→ cn (g (f (fun← an zero)))) (suc i)
     ... | no nisa | tri< a ¬b ¬c = lem12 where
          lem12 : 1 ≤ count-A i  -- ca contains ani 0
          lem12 = ?
@@ -940,7 +940,7 @@
     ... | yes isa | tri< a ¬b ¬c = s≤s z≤n
     ... | yes isa | tri≈ ¬a b ¬c = s≤s z≤n
     ... | yes isa | tri> ¬a ¬b c₁ = z≤n
-    c1<count-A (suc n) (suc i) with is-A (fun← cn (suc i)) 
+    c1<ca (suc n) (suc i) with is-A (fun← cn (suc i)) 
     ... | no nisa = ca00 where
        ca00 : c1 (suc n) (suc i) ≤ count-A i
        ca00 with <-cmp (fun→ cn (g (f (fun← an (suc n))))) (suc i)
@@ -948,39 +948,45 @@
              lem13 : c1 n i ≡ c1 n (suc i) 
              lem13 = c1+0 {n} {i} nisa
              lem10 : c1 n i ≤ count-A i
-             lem10 = c1<count-A n i
+             lem10 = c1<ca n i
              lem12 : suc (c1 n (suc i)) ≤ count-A i  -- becase count-A i contains (ani (suc n))
              lem12 = ?
        ... |  tri≈ ¬a b ¬c = ⊥-elim (nisa ? )
-       ... |  tri> ¬a ¬b c₁ = subst ( λ k → k ≤ count-A i) (c1+0 {n} {i} nisa) (c1<count-A n i)
+       ... |  tri> ¬a ¬b c₁ = subst ( λ k → k ≤ count-A i) (c1+0 {n} {i} nisa) (c1<ca n i)
     ... | yes isa = ca01 where
-       open ≤-Reasoning
        lem10 : c1 n i ≤ count-A i
-       lem10 = c1<count-A n i
+       lem10 = c1<ca n i
        lem12 : c1 n (suc i) ≤ suc (count-A i) 
        lem12 with <-cmp n (fun→  an (Is.a isa)) | c1+1 n i isa
-       ... | tri< a ¬b ¬c | eq = ≤-trans (subst (λ k → k ≤ count-A i) eq (c1<count-A n i)) a≤sa
+       ... | tri< a ¬b ¬c | eq = ≤-trans (subst (λ k → k ≤ count-A i) eq (c1<ca n i)) a≤sa
        ... | tri≈ ¬a b ¬c | eq = begin
             c1 n (suc i) ≡⟨ sym eq ⟩
-            suc ( c1 n i) ≤⟨ s≤s (c1<count-A n i) ⟩
-            suc (count-A i) ∎ 
+            suc ( c1 n i) ≤⟨ s≤s (c1<ca n i) ⟩
+            suc (count-A i) ∎ where open ≤-Reasoning
        ... | tri> ¬a ¬b c₁ | eq = begin
             c1 n (suc i) ≡⟨ sym eq ⟩
-            suc ( c1 n i) ≤⟨ s≤s (c1<count-A n i) ⟩
-            suc (count-A i) ∎ 
+            suc ( c1 n i) ≤⟨ s≤s (c1<ca n i) ⟩
+            suc (count-A i) ∎ where open ≤-Reasoning
        ca01 : c1 (suc n) (suc i) ≤ suc (count-A i)
        ca01 with <-cmp (fun→ cn (g (f (fun← an (suc n))))) (suc i)
        ... | tri< a ¬b ¬c = lem13 where  -- count-A contains (suc i), so keep ≤-relation
-             lem11 : c1 n (suc i) ≤ count-A (suc i)
-             lem11 = c1<count-A n (suc i)
              lem13 : suc (c1 n (suc i)) ≤ suc (count-A i) 
              lem13 = ?
-       ... | tri≈ ¬a b ¬c = ? where  -- count-A contains (suc i) here
+       ... | tri≈ ¬a b ¬c = lem13 where  -- count-A contains (suc i) here
+             lem15 : c1 n i ≡ c1 n (suc i) 
+             lem15 with <-cmp n (fun→ an (Is.a isa)) | c1+1 n i isa 
+             ... | tri< a ¬b ¬c | eq = eq
+             ... | tri≈ ¬a bi ¬c | eq = ⊥-elim ( nat-≡< (sym ( inject-cgf ( trans b lem16 ))) a<sa ) where
+                  lem16 : suc i ≡  fun→ cn (g (f (fun← an n )))
+                  lem16 = begin 
+                    suc i ≡⟨ sym ( fiso→ cn _) ⟩
+                    fun→ cn (fun← cn (suc i))  ≡⟨ cong (fun→ cn) (sym (Is.fa=c isa)) ⟩
+                    fun→ cn (g (f (Is.a isa)))  ≡⟨ cong (λ k → fun→ cn (g (f k)) ) (sym (fiso← an _)) ⟩
+                    fun→ cn (g (f (fun← an (fun→ an (Is.a isa)))))  ≡⟨  cong (λ k → fun→ cn (g (f (fun← an k))))  (sym bi) ⟩
+                    fun→ cn (g (f (fun← an n ))) ∎ where open ≡-Reasoning
+             ... | tri> ¬a ¬b c₁ | eq = ?
              lem13 : suc (c1 n (suc i)) ≤ suc (count-A i) 
-             lem13 with <-cmp n (fun→  an (Is.a isa)) | c1+1 n i isa
-             ... | tri< a ¬b ¬c | eq = s≤s (subst (λ k → k ≤ count-A i) eq (c1<count-A n i))
-             ... | tri≈ ¬a bi ¬c | eq = ?
-             ... | tri> ¬a ¬b c₁ | eq = ?
+             lem13 = s≤s ( subst (λ k → k ≤ count-A i) lem15 ( c1<ca n i) )
        ... | tri> ¬a ¬b c₁ = lem12 -- count-A is one degree larger now
 
     record maxAC (n : ℕ) : Set where