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

changeset 1310:29637e5921f5

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, 09 Jun 2023 18:04:08 +0900
parents a93764db7c67
children 0d2f3a042fa9
files src/bijection.agda
diffstat 1 files changed, 37 insertions(+), 16 deletions(-) [+]
line wrap: on
line diff
--- a/src/bijection.agda	Fri Jun 09 16:54:51 2023 +0900
+++ b/src/bijection.agda	Fri Jun 09 18:04:08 2023 +0900
@@ -551,25 +551,46 @@
     ... | no nisA | yes isB = ≤-trans (ca≤cb0 n) px≤x
     ... | no nisA | no nisB = ca≤cb0 n
 
+    lem02 : (n i : ℕ) → i ≡ fun→ cn (g (f (fun← an n))) → n < count-A i
+    lem02 zero zero eq with is-A (fun← cn zero)
+    ... | yes isA = ≤-refl
+    ... | no nisA = ⊥-elim (nisA record { a = (fun← an zero) ; fa=c = trans (sym (fiso← cn _)) (cong (fun← cn) (sym eq))  })
+    lem02 zero (suc i) eq with is-A (fun← cn (suc i))
+    ... | yes isA = s≤s z≤n
+    ... | no nisA = ⊥-elim (nisA record { a = (fun← an zero) ; fa=c = trans (sym (fiso← cn _)) (cong (fun← cn) (sym eq))  })
+    lem02 (suc n) zero eq with is-A (fun← cn zero)
+    ... | yes isA = ?
+    ... | no nisA = ⊥-elim (nisA record { a = (fun← an (suc n)) ; fa=c = trans (sym (fiso← cn _)) (cong (fun← cn) (sym eq))  })
+    lem02 (suc n) (suc i) eq with is-A (fun← cn (suc i))
+    ... | yes isA = ? where
+          --  nth a can be larger than (n+1)th
+          lem04 : n < count-A (fun→ cn (g (f (fun← an n))))
+          lem04 = lem02 n _ refl
+    ... | no nisA = ⊥-elim (nisA record { a = (fun← an (suc n)) ; fa=c = trans (sym (fiso← cn _)) (cong (fun← cn) (sym eq))  })
+    
+    lem01 : (n i : ℕ) → n < count-B i → B
+    lem01 zero zero lt with is-B (fun← cn zero)
+    ... | yes isB = Is.a isB
+    ... | no nisB = ⊥-elim (¬a≤a lt)
+    lem01 zero (suc i) lt with is-B (fun← cn (suc i))
+    ... | yes isB = Is.a isB
+    ... | no nisB = lem01 zero i lt 
+    lem01 (suc n) zero lt with is-B (fun← cn zero)
+    ... | yes isB = Is.a isB
+    ... | no nisB = ? -- ⊥-elim (¬a≤a lt)
+    lem01 (suc n) (suc i) lt with is-B (fun← cn (suc i))
+    ... | yes isB = Is.a isB
+    ... | no nisB = lem01 (suc n) i lt 
+
     ntob : (n : ℕ) → B
-    ntob n = lem01 (fun→ cn (g (f (fun← an n)))) (≤-trans (lem02 _ refl ) (ca≤cb0 (fun→ cn (g (f (fun← an n)))))) where
-        lem02 : (i : ℕ) → i ≡ fun→ cn (g (f (fun← an n))) → 1 ≤ count-A i
-        lem02 zero eq with is-A (fun← cn zero)
-        ... | yes isA = ≤-refl
-        ... | no nisA = ⊥-elim (nisA record { a = (fun← an n) ; fa=c = trans (sym (fiso← cn _)) (cong (fun← cn) (sym eq))  })
-        lem02 (suc i) eq with is-A (fun← cn (suc i))
-        ... | yes isA = s≤s z≤n
-        ... | no nisA = ⊥-elim (nisA record { a = (fun← an n) ; fa=c = trans (sym (fiso← cn _)) (cong (fun← cn) (sym eq))  })
-        lem01 : (i : ℕ) → zero < count-B i → B
-        lem01 zero lt with is-B (fun← cn zero)
-        ... | yes isB = Is.a isB
-        ... | no nisB = ⊥-elim (¬a≤a lt)
-        lem01 (suc i) lt with is-B (fun← cn (suc i))
-        ... | yes isB = Is.a isB
-        ... | no nisB = lem01 i lt 
+    ntob n = lem01 n (fun→ cn (g (f (fun← an n)))) (≤-trans (lem02 n _ refl ) (ca≤cb0 (fun→ cn (g (f (fun← an n)))))) 
 
     biso : (n : ℕ) → bton (ntob n) ≡ n
-    biso n = ?
+    biso n = lem03 _ (≤-trans (lem02 n _ refl ) (ca≤cb0 (fun→ cn (g (f (fun← an n)))))) refl where
+        lem03 :  (i : ℕ) → (lt : n < count-B i )
+           → i ≡ (fun→ cn (g (f (fun← an n))))
+           → count-B (fun→ cn (g (lem01 n i lt ))) ≡ n
+        lem03 = ?
 
     biso1 : (b : B) → ntob (bton b) ≡ b
     biso1 b = ?