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

changeset 1339:23bba94a980f

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 18:33:50 +0900
parents b969f1710434
children 4c32cd3b84c2
files src/bijection.agda
diffstat 1 files changed, 29 insertions(+), 21 deletions(-) [+]
line wrap: on
line diff
--- a/src/bijection.agda	Fri Jun 16 11:38:05 2023 +0900
+++ b/src/bijection.agda	Fri Jun 16 18:33:50 2023 +0900
@@ -669,31 +669,39 @@
     ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c | case2 le = case2 (≤-trans le refl-≤s ) 
     ... | tri> ¬a ¬b c₁ | tri> ¬a₁ ¬b₁ c₂ | u = u
 
-    --
+    record An (n i : ℕ) : Set where
+        field
+          ai : ℕ
+          ai≤n : ai ≤ n
+          cn=ai : 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₁ )
+
     c1-at-i : (n i : ℕ) → 
-           (suc (c1 n i) ≡ c1 n (suc i) →  fun→ cn (g (f (fun← an n))) ≡ suc i)
-         ∧ ( (fun→ cn (g (f (fun← an n))) ≡ suc i)  → suc (c1 n i) ≡ c1 n (suc 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-≡< eq (<-trans a a<sa)))  ⟫ 
-    ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = ⟪ ( λ () ) , (λ eq → ⊥-elim (nat-≡< eq (<-trans a a<sa)))  ⟫ 
-    ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c₁ = ⟪ ( λ () ) , (λ eq → ⊥-elim (nat-≡< eq (<-trans a a<sa)))  ⟫ 
-    ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = ⟪ ( λ () ) , (λ eq → ⊥-elim ( ¬b eq ))  ⟫ 
+    ... | 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 eq ))  ⟫ 
+    ... | 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 = ⟪ ( λ _ → b ) , ( λ _ → refl ) ⟫
-    ... | tri> ¬a ¬b c₁ | tri> ¬a₁ ¬b₁ c₂ = ⟪ ( λ () ) , ( λ eq → ⊥-elim (¬b₁ eq )) ⟫
-    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₁ eq)) ⟫ where   
-        -- a (suc n) is less than (suc i) → c1 (suc n) (suc (suc i)) ≡ c1 (suc n) (suc i)
-        lemc00 : ¬ ( suc (suc (c1 n (suc i))) ≡ suc (c1 n (suc (suc i))) )
-        lemc00 = ?
-    ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = ?
-    ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c₁ = ?
-    ... | tri≈ ¬a b ¬c | t = ?
-    ... | tri> ¬a ¬b c₁ | t = ?
+    ... | 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 = ?
+
 
     -- 
     -- c n < i means j < suc n → fun← an j < c n, we cannot have more else