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

changeset 1380:9ef69be89d06

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, 23 Jun 2023 11:49:24 +0900
parents f2755eab7b91
children 082d83168e25
files src/bijection.agda
diffstat 1 files changed, 27 insertions(+), 9 deletions(-) [+]
line wrap: on
line diff
--- a/src/bijection.agda	Fri Jun 23 10:09:53 2023 +0900
+++ b/src/bijection.agda	Fri Jun 23 11:49:24 2023 +0900
@@ -726,16 +726,21 @@
           cb : ℕ
           b=cn : fun← cn cb ≡ g b
           cb=n : count-B cb ≡ suc n
+          cb-inject : (b1 : B) → count-B (fun→ cn (g b)) ≡ count-B (fun→ cn (g b1)) → b ≡ b1
 
     lem01 : (n i : ℕ) → suc n ≤ count-B i → CountB n
     lem01 n i le = lem09 i (count-B i) le refl where
         -- starting from 0, if count B i ≡ suc n, this is it
         lem07 : (n i : ℕ) → count-B i ≡ suc n → CountB n
         lem07 n 0 eq with is-B (fun← cn 0) | inspect count-B 0
-        ... | yes isb | record { eq = eq1 } = record { b = Is.a isb ; cb = 0 ; b=cn = sym (Is.fa=c isb) ; cb=n = trans eq1 eq } 
+        ... | yes isb | record { eq = eq1 } = record { b = Is.a isb ; cb = 0 ; b=cn = sym (Is.fa=c isb) ; cb=n = trans eq1 eq ; cb-inject = lem12 } where
+            lem12 : (b2 : B) → count-B (fun→ cn (g (Is.a isb))) ≡ count-B (fun→ cn (g b2)) → Is.a isb ≡ b2
+            lem12 b2 eq = ?
         ... | no nisb | record { eq = eq1 } = ⊥-elim ( nat-≡< eq (s≤s z≤n ) )
         lem07 n (suc i) eq with is-B (fun← cn (suc i)) | inspect count-B (suc i)
-        ... | yes isb | record { eq = eq1 } = record { b = Is.a isb ; cb = suc i ; b=cn = sym (Is.fa=c isb) ; cb=n = trans eq1 eq} 
+        ... | yes isb | record { eq = eq1 } = record { b = Is.a isb ; cb = suc i ; b=cn = sym (Is.fa=c isb) ; cb=n = trans eq1 eq; cb-inject = lem12 } where
+            lem12 : (b2 : B) → count-B (fun→ cn (g (Is.a isb))) ≡ count-B (fun→ cn (g b2)) → Is.a isb ≡ b2
+            lem12 b2 eq = ?
         ... | no nisb | record { eq = eq1 } = lem07 n i  eq
 
         lem09 : (i j : ℕ) → suc n ≤ j → j ≡ count-B i →  CountB n
@@ -768,14 +773,27 @@
            CB  = lem01 n (maxAC.ac (lem02 n)) (≤-trans (maxAC.n<ca (lem02 n)) (ca≤cb0 (maxAC.ac (lem02 n))) )
 
     biso1 : (b : B) → ntob (bton b) ≡ b
-    biso1 b = InjectiveF.inject gi ( begin
-        g (ntob (bton b)) ≡⟨ refl ⟩
-        g (CountB.b CB) ≡⟨ sym (CountB.b=cn CB) ⟩
-        ? ≡⟨ ? ⟩
-        g b ∎ ) where
+    biso1 b with count-B (fun→ cn (g b)) | inspect count-B (fun→ cn (g b)) 
+    ... | zero  | record { eq = eq1 } = ⊥-elim ( nat-≡< (sym lem20) (lem21 _ refl) ) where
+        lem20 : count-B (fun→ cn (InjectiveF.f gi b)) ≡ zero
+        lem20 = eq1
+        lem21 : (i : ℕ) → i ≡ fun→ cn (InjectiveF.f gi b) → 0 < count-B  i
+        lem21 0 eq with is-B (fun← cn 0) | inspect count-B 0
+        ... | yes isb | record { eq = eq1 } = ≤-refl
+        ... | no nisb | record{ eq = eq1 } = ⊥-elim ( nisb record { a = b ; fa=c = trans (sym (fiso← cn _)) (cong (fun← cn) (sym eq)) } )
+        lem21 (suc i) eq with is-B (fun← cn (suc i)) | inspect count-B (suc i)
+        ... | yes isb | record{ eq = eq2 } = s≤s z≤n
+        ... | no nisb | record{ eq = eq2 } = ⊥-elim ( nisb record { a = b ; fa=c = trans (sym (fiso← cn _)) (cong (fun← cn) (sym eq)) } )
+    ... | suc n | record { eq = eq1 } = lem26 ( begin 
+              count-B (fun→ cn (g (CountB.b CB)))  ≡⟨ cong (λ k → count-B (fun→ cn k)) (sym (CountB.b=cn CB)) ⟩
+              count-B (fun→ cn (fun← cn (CountB.cb CB)))  ≡⟨ cong (λ k → count-B k) (fiso→ cn _) ⟩
+              count-B (CountB.cb CB)  ≡⟨ CountB.cb=n CB ⟩
+              suc n ≡⟨ sym eq1 ⟩
+              count-B (fun→ cn (g b)) ∎ ) where
            open ≡-Reasoning
-           n  = pred (count-B (fun→ cn (g b)))
-           CB = lem01 n (maxAC.ac (lem02 n)) (≤-trans (maxAC.n<ca (lem02 n)) (ca≤cb0 (maxAC.ac (lem02 n))) )
+           CB  = lem01 n (maxAC.ac (lem02 n)) (≤-trans (maxAC.n<ca (lem02 n)) (ca≤cb0 (maxAC.ac (lem02 n))) )
+           lem26 : count-B (fun→ cn (g (CountB.b CB))) ≡ count-B (fun→ cn (g b))  → CountB.b CB ≡ b
+           lem26 = CountB.cb-inject CB _
 
 bi-∧ : {A B C D : Set} → Bijection A B → Bijection C D → Bijection (A ∧ C) (B ∧ D)
 bi-∧ {A} {B} {C} {D} ab cd = record {