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

changeset 1348:c42647780620

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 05:02:01 +0900
parents 9a14ef021f8f
children f5048a51d19f
files src/bijection.agda
diffstat 1 files changed, 50 insertions(+), 10 deletions(-) [+]
line wrap: on
line diff
--- a/src/bijection.agda	Sat Jun 17 19:08:46 2023 +0900
+++ b/src/bijection.agda	Sun Jun 18 05:02:01 2023 +0900
@@ -800,21 +800,24 @@
               fun→ cn (g (f (Is.a isa))) ≡⟨ cong (fun→ cn) (Is.fa=c isa) ⟩
               fun→ cn (fun← cn (suc i)) ≡⟨ fiso→ cn _ ⟩
               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 ∎ 
          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 | _ = ⊥-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> ¬a₁ ¬b₁ c₂ = ?
-    ... | tri> ¬a ¬b an<j = c115 where
+         ... | 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)
          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 = ⊥-elim (nat-≤> an<n (<-transʳ a a<sa) )
          ... | tri≈ ¬a b ¬c | s = s
          ... | tri> ¬a ¬b c₁ | s = s
          open ≡-Reasoning
@@ -827,7 +830,7 @@
          ... | 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
+         ... | 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
               c128 : fun→ cn (g (f (fun← an (fun→ an (Is.a isa)))))  ≡ suc i
@@ -840,6 +843,43 @@
               c130 = inject-cgf (trans c118 (sym c128 ))
          ... | tri> ¬a ¬b c₁ | tri> ¬a₁ ¬b₁ c₂ = c112
 
+    c1+0 : {n i : ℕ} → ¬ Is A C (λ x → g (f x)) (fun← cn (suc i)) →  c1 n i ≡ c1 n (suc i)
+    c1+0 {zero} {i} nisa with <-cmp (fun→ cn (g (f (fun← an zero)))) i  | <-cmp (fun→ cn (g (f (fun← an zero)))) (suc i)
+    ... | 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-≤> a≤sa (<-trans c₁ a) )
+    ... | 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₂ =  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 =  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
+    ... | 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-≤> a≤sa (<-transˡ c₁ (≤-trans refl-≤s a ) ))
+    ... | 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₂ | 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) = ?
+
     record maxAC (n : ℕ) : Set where
        field
            ac : ℕ