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

changeset 1340:4c32cd3b84c2

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 Fri, 16 Jun 2023 20:45:28 +0900
parents 23bba94a980f
children 49e5a4d8c958
files src/bijection.agda
diffstat 1 files changed, 17 insertions(+), 22 deletions(-) [+]
line wrap: on
line diff
--- a/src/bijection.agda	Fri Jun 16 18:33:50 2023 +0900
+++ b/src/bijection.agda	Fri Jun 16 20:45:28 2023 +0900
@@ -672,36 +672,31 @@
     record An (n i : ℕ) : Set where
         field
           ai : ℕ
-          ai≤n : ai ≤ n
-          cn=ai : fun→ cn (g (f (fun← an ai))) ≡ suc i
+          ai<n : ai ≤ n
+          cn=n : fun→ cn (g (f (fun← an ai))) ≡ suc i
         cn=a0 : n ≡ 0 → fun→ cn (g (f (fun← an 0))) ≡ suc i
-        cn=a0 refl with <-cmp ai 0
-        ... | tri≈ ¬a b ¬c = subst (λ k → fun→ cn (g (f (fun← an k))) ≡ suc i) b cn=ai
-        ... | tri> ¬a ¬b c₁ = ⊥-elim ( nat-≤> ai≤n c₁ )
+        cn=a0 n=0 with <-cmp ai n
+        ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a (subst (λ k → k < suc ai) (sym n=0) (s≤s z≤n)  ))
+        ... | tri≈ ¬a b ¬c = subst (λ k → fun→ cn (g (f (fun← an k))) ≡ suc i) (trans b n=0) cn=n
+        ... | tri> ¬a ¬b c₁ = ⊥-elim ( nat-≤> c₁ (<-transʳ ai<n a<sa) )
 
     c1-at-i : (n i : ℕ) → 
            (suc (c1 n i) ≡ c1 n (suc i) →  An n i)                             
          ∧ ( An n i → suc (c1 n i) ≡ c1 n (suc i) )
     c1-at-i 0 i 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₁ = ⟪ ( λ () ) , (λ eq → ⊥-elim (nat-≡< (An.cn=a0 eq refl ) (<-trans a a<sa)))  ⟫ 
-    ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = ⟪ ( λ () ) , (λ eq → ⊥-elim (nat-≡< (An.cn=a0 eq refl ) (<-trans a a<sa)))  ⟫ 
-    ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c₁ = ⟪ ( λ () ) , (λ eq → ⊥-elim (nat-≡< (An.cn=a0 eq refl ) (<-trans a a<sa)))  ⟫ 
-    ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = ⟪ ( λ () ) , (λ eq → ⊥-elim ( ¬b (An.cn=a0 eq refl ) ))  ⟫ 
+    ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = ⟪ ( λ () ) , (λ eq → ⊥-elim (nat-≡< (An.cn=a0 eq refl) (<-trans a a<sa)))  ⟫ 
+    ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = ⟪ ( λ () ) , (λ eq → ⊥-elim (nat-≡< (An.cn=a0 eq refl) (<-trans a a<sa)))  ⟫ 
+    ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c₁ = ⟪ ( λ () ) , (λ eq → ⊥-elim (nat-≡< (An.cn=a0 eq refl) (<-trans a a<sa)))  ⟫ 
+    ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = ⟪ ( λ () ) , (λ eq → ⊥-elim ( ¬b (An.cn=a0 eq refl) ))  ⟫ 
     ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ = ⟪ ( λ () ) , (λ eq → ⊥-elim (nat-≡< (sym b) (subst (λ k → i < k) (sym b₁) a<sa) ))  ⟫ 
-    ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c₁ = ⟪ ( λ () ) , (λ eq → ⊥-elim ( ¬b (An.cn=a0 eq refl ) ))  ⟫ 
+    ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c₁ = ⟪ ( λ () ) , (λ eq → ⊥-elim ( ¬b (An.cn=a0 eq refl) ))  ⟫ 
     ... | tri> ¬a ¬b c₁ | tri< (s≤s a) ¬b₁ ¬c = ⊥-elim (nat-≡< refl (≤-trans c₁ a))
-    ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c = ⟪ ( λ eq → record { ai = 0 ; ai≤n = ≤-refl ; cn=ai = b } ) , ( λ _ → refl ) ⟫
-    ... | tri> ¬a ¬b c₁ | tri> ¬a₁ ¬b₁ c₂ = ⟪ ( λ () ) , ( λ eq → ⊥-elim (¬b₁ (An.cn=a0 eq refl ) )) ⟫
-    c1-at-i (suc n) i = ⟪ ( λ eq → ca00 n _ ≤-refl eq) , ( λ an0 → ca01 an0) ⟫  where
-         --  if (suc (c1 (suc n) i)) ≡ c1 (suc n) (suc i)  then fun← cn (suc i) have to be g (f (fun← an ai)) where ai <= suc n
-         ca00 : (n ai : ℕ ) → ai ≤ suc n → suc (c1 (suc n) i) ≡ c1 (suc n) (suc i)  → An (suc n) i
-         ca00 0 ai a<n eq = ?
-         ca00 (suc n) ai a<n eq with <-cmp (fun→ cn (g (f (fun← an (suc (suc n)))))) i | <-cmp (fun→ cn (g (f (fun← an (suc (suc n)))))) (suc i)
-         ... | t | s = ?
-         ca01 : An (suc n) i → suc (c1 (suc n) i) ≡ c1 (suc n) (suc i) 
-         ca01 an0 with <-cmp (fun→ cn (g (f (fun← an (suc n))))) i | <-cmp (fun→ cn (g (f (fun← an (suc n))))) (suc i)
-         ... | s | t = ?
-
+    ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c = ⟪ ( λ eq → record { ai = 0 ; ai<n = z≤n ; cn=n = b } ) , ( λ _ → refl ) ⟫
+    ... | tri> ¬a ¬b c₁ | tri> ¬a₁ ¬b₁ c₂ = ⟪ ( λ () ) , ( λ eq → ⊥-elim (¬b₁ (An.cn=a0 eq refl) )) ⟫
+    c1-at-i (suc n) zero with <-cmp (fun→ cn (g (f (fun← an (suc n))))) zero | <-cmp (fun→ cn (g (f (fun← an (suc n))))) (suc zero)
+    ... | s | t = ?
+    c1-at-i (suc n) (suc i) with  <-cmp (fun→ cn (g (f (fun← an (suc n))))) (suc i) | <-cmp (fun→ cn (g (f (fun← an (suc n))))) (suc (suc i)) 
+    ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = ⟪ ? , (λ eq → ⊥-elim ( ¬b₁ ? )) ⟫ 
 
     -- 
     -- c n < i means j < suc n → fun← an j < c n, we cannot have more else