Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1384:0d29328c0441
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 24 Jun 2023 01:44:24 +0900 |
| parents | 51abc18e6f17 |
| children | 0cf6d7702dab |
| files | src/bijection.agda |
| diffstat | 1 files changed, 59 insertions(+), 33 deletions(-) [+] |
line wrap: on
line diff
--- a/src/bijection.agda Fri Jun 23 15:36:09 2023 +0900 +++ b/src/bijection.agda Sat Jun 24 01:44:24 2023 +0900 @@ -708,24 +708,6 @@ ca-list cl ∎ where open ≤-Reasoning - anygb : (b : B) → Any (_≡_ (g b)) (clist (c (fun→ cn (g b)))) - anygb = ? - - bton1 : B → ℕ - bton1 b = bton10 b (clist (c (fun→ cn (g b)))) ? where - bton10 : (b : B) → (x : List C) → Any (_≡_ (g b)) x → ℕ - bton10 b (h ∷ t) (here px) = count-B ( fun→ cn h ) - bton10 b (h ∷ t) (there ax) = bton10 b t ax - - anycb : (n : ℕ) → Any (λ c₁ → Is B C g c₁ ∧ (count-B (fun→ cn c₁) ≡ n)) (clist (c n)) - anycb = ? - - ntob1 : (n : ℕ) → B - ntob1 n = bton10 n (clist (c n)) ? where - bton10 : (n : ℕ) → (x : List C) → Any (λ c → Is B C g c ∧ (count-B (fun→ cn c) ≡ n)) x → B - bton10 n (h ∷ t) (here px) = Is.a (proj1 px) - bton10 n (h ∷ t) (there ax) = bton10 n t ax - record maxAC (n : ℕ) : Set where field ac : ℕ @@ -740,32 +722,76 @@ cb : ℕ b=cn : fun← cn cb ≡ g b cb=n : count-B cb ≡ suc n - cb-inject : (cb1 : ℕ) → count-B cb ≡ count-B cb1 → cb ≡ cb1 + cb-inject : (cb1 : ℕ) → Is B C g (fun← cn cb1) → count-B cb ≡ count-B cb1 → cb ≡ cb1 + + count-B-mono : {i j : ℕ} → i ≤ j → count-B i ≤ count-B j + count-B-mono {i} {j} i≤j with ≤-∨ i≤j + ... | case1 refl = ≤-refl + ... | case2 i<j = lem00 _ _ i<j where + lem00 : (i j : ℕ) → i < j → count-B i ≤ count-B j + lem00 i (suc j) (s≤s i<j) = ≤-trans (count-B-mono i<j) (lem01 j) where + lem01 : (j : ℕ) → count-B j ≤ count-B (suc j) + lem01 zero with is-B (fun← cn (suc zero)) + ... | yes isb = refl-≤s + ... | no nisb = ≤-refl + lem01 (suc n) with is-B (fun← cn (suc (suc n))) + ... | yes isb = refl-≤s + ... | no nisb = ≤-refl 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 + + lem06 : (i j : ℕ ) → Is B C g (fun← cn i) → Is B C g (fun← cn j) → count-B i ≡ count-B j → i ≡ j + lem06 i j bi bj eq = lem08 where + lem20 : (i j : ℕ) → i < j → Is B C g (fun← cn i) → Is B C g (fun← cn j) → count-B j ≡ count-B i → ⊥ + lem20 zero j i<j bi bj le = ? + lem20 (suc i) zero () bi bj le + lem20 (suc i) (suc j) (s≤s i<j) bi bj le = ? where + -- + -- i < suc i ≤ j + -- suc (cb i) < cb (suc i) ≤ cb j + -- + lem22 : suc (count-B i) ≡ count-B (suc i) + lem22 with is-B (fun← cn (suc i)) | inspect count-B (suc i) + ... | yes _ | record { eq = eq1 } = refl + ... | no nisa | _ = ⊥-elim ( nisa bi ) + lem23 : suc (count-B j) ≡ count-B (suc j) + lem23 with is-B (fun← cn (suc j)) | inspect count-B (suc j) + ... | yes _ | record { eq = eq1 } = refl + ... | no nisa | _ = ⊥-elim ( nisa bj ) + lem24 : count-B i ≡ count-B j + lem24 with is-B (fun← cn (suc i)) | inspect count-B (suc i) | is-B (fun← cn (suc j)) | inspect count-B (suc j) + ... | no nisc | _ | _ | _ = ? + ... | yes _ | _ | no nisc | _ = ? + ... | no _ | _ | no nisc | _ = ? + ... | yes _ | record { eq = eq1 } | yes _ | record { eq = eq2 } = sym (cong pred le) + lem21 : suc (count-B i) ≤ count-B j + lem21 = begin + suc (count-B i) ≡⟨ lem22 ⟩ + count-B (suc i) ≤⟨ count-B-mono i<j ⟩ + count-B j ∎ where + open ≤-Reasoning + lem08 : i ≡ j + lem08 with <-cmp i j + ... | tri< a ¬b ¬c = ⊥-elim ( lem20 i j a bi bj (sym eq) ) + ... | tri≈ ¬a b ¬c = b + ... | tri> ¬a ¬b c₁ = ⊥-elim ( lem20 j i c₁ bj bi eq ) + lem09 : (i j : ℕ) → suc n ≤ j → j ≡ count-B i → CountB n 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 = λ cb1 cb1eq → lem12 cb1 (subst (λ k → k ≡ count-B cb1) eq1 cb1eq) } where - lem12 : (cb1 : ℕ) → 1 ≡ count-B cb1 → 0 ≡ cb1 - lem12 cb1 cbeq with <-cmp 0 cb1 - ... | tri≈ ¬a b ¬c = b - ... | tri< a ¬b ¬c = ? + ; cb-inject = λ cb1 iscb1 cb1eq → lem12 cb1 iscb1 (subst (λ k → k ≡ count-B cb1) eq1 cb1eq) } where + lem12 : (cb1 : ℕ) → Is B C g (fun← cn cb1) → 1 ≡ count-B cb1 → 0 ≡ cb1 + lem12 cb1 iscb1 cbeq = lem06 0 cb1 isb iscb1 (trans eq1 cbeq) ... | 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 = λ 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 cb1 cbeq with <-cmp (suc i) cb1 - ... | tri< a ¬b ¬c = ? - ... | tri≈ ¬a b ¬c = b - ... | tri> ¬a ¬b c₁ = ? - -- with CountB.cb-inject ( lem09 n (count-B n) ? refl ) - -- ... | t = ? + ; cb-inject = λ cb1 iscb1 cb1eq → lem12 cb1 iscb1 (subst (λ k → k ≡ count-B cb1) eq1 cb1eq) } where + lem12 : (cb1 : ℕ) → Is B C g (fun← cn cb1) → suc (count-B i) ≡ count-B cb1 → suc i ≡ cb1 + lem12 cb1 iscb1 cbeq = lem06 (suc i) cb1 isb iscb1 (trans eq1 cbeq) ... | no nisb | record { eq = eq1 } = lem07 n i eq lem09 0 (suc j) (s≤s le) eq with ≤-∨ (s≤s le) @@ -812,7 +838,7 @@ 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)) ⟩ + CountB.cb CB ≡⟨ CountB.cb-inject CB _ record { a = b ; fa=c = sym (fiso← cn _) } (trans (CountB.cb=n CB) (sym eq1)) ⟩ fun→ cn (InjectiveF.f gi b) ∎ )) ⟩ b ∎ where open ≡-Reasoning