Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1382:4ecb12396ebd
..
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 23 Jun 2023 13:20:00 +0900 |
| parents | 082d83168e25 |
| children | 51abc18e6f17 |
| files | src/bijection.agda |
| diffstat | 1 files changed, 16 insertions(+), 26 deletions(-) [+] |
line wrap: on
line diff
--- a/src/bijection.agda Fri Jun 23 12:47:17 2023 +0900 +++ b/src/bijection.agda Fri Jun 23 13:20:00 2023 +0900 @@ -735,14 +735,17 @@ 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 ; cb-inject = ? } 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 = ? + ... | 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 = λ cb1 cb1eq → lem12 cb1 (subst (λ k → k ≡ count-B cb1) eq1 cb1eq) } where + lem12 : (cb1 : ℕ) → 1 ≡ count-B cb1 → 0 ≡ cb1 + lem12 = ? ... | 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; cb-inject = ? } 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 = ? + ... | 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 = λ cb1 cb1eq → lem12 cb1 (subst (λ k → k ≡ count-B cb1) eq1 cb1eq) } where + lem12 : (cb1 : ℕ) → suc (count-B i) ≡ count-B cb1 → suc i ≡ cb1 + lem12 cb cbeq with CountB.cb-inject ( lem09 n (count-B n) ? refl ) + ... | t = ? ... | no nisb | record { eq = eq1 } = lem07 n i eq lem09 0 (suc j) (s≤s le) eq with ≤-∨ (s≤s le) @@ -785,28 +788,15 @@ 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 + ... | suc n | record { eq = eq1 } = begin + CountB.b CB ≡⟨ InjectiveF.inject gi (bi-inject→ cn (begin + fun→ cn (g (CountB.b CB)) ≡⟨ cong (fun→ cn) (sym (CountB.b=cn CB)) ⟩ + fun→ cn (fun← cn (CountB.cb CB)) ≡⟨ fiso→ cn _ ⟩ + CountB.cb CB ≡⟨ CountB.cb-inject CB _ (trans (CountB.cb=n CB) (sym eq1)) ⟩ + fun→ cn (InjectiveF.f gi b) ∎ )) ⟩ + b ∎ where open ≡-Reasoning 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 eq = begin - CountB.b CB ≡⟨ InjectiveF.inject gi ( begin - g (CountB.b CB) ≡⟨ bi-inject→ cn ( begin - fun→ cn (g (CountB.b CB)) ≡⟨ cong (fun→ cn) (sym (CountB.b=cn CB)) ⟩ - fun→ cn (fun← cn (CountB.cb CB)) ≡⟨ fiso→ cn _ ⟩ - CountB.cb CB ≡⟨ CountB.cb-inject CB _ ( begin - count-B (CountB.cb CB) ≡⟨ cong count-B ? ⟩ - count-B (fun→ cn (g (CountB.b CB))) ≡⟨ eq ⟩ - count-B (fun→ cn (g b)) ∎ ) ⟩ - fun→ cn (g b) ∎ ) ⟩ - g b ∎ ) ⟩ - b ∎ - -- ? ≡⟨ cong (fun← cn) (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 {