Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1385:0cf6d7702dab
Countable-Bernstein done
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 24 Jun 2023 07:22:43 +0900 |
| parents | 0d29328c0441 |
| children | 0afcd5b99548 |
| files | src/bijection.agda |
| diffstat | 1 files changed, 50 insertions(+), 15 deletions(-) [+] |
line wrap: on
line diff
--- a/src/bijection.agda Sat Jun 24 01:44:24 2023 +0900 +++ b/src/bijection.agda Sat Jun 24 07:22:43 2023 +0900 @@ -506,13 +506,14 @@ Countable-Bernstein : (A B C : Set) → Bijection A ℕ → Bijection C ℕ → (fi : InjectiveF A B ) → (gi : InjectiveF B C ) - → (is-A : (c : C ) → Dec (Is A C (λ x → (InjectiveF.f gi (InjectiveF.f fi x))) c )) → (is-B : (c : C ) → Dec (Is B C (InjectiveF.f gi) c) ) + → (is-A : (c : C ) → Dec (Is A C (λ x → (InjectiveF.f gi (InjectiveF.f fi x))) c )) + → (is-B : (c : C ) → Dec (Is B C (InjectiveF.f gi) c) ) → Bijection B ℕ Countable-Bernstein A B C an cn fi gi is-A is-B = record { fun→ = λ x → bton x ; fun← = λ n → ntob n - ; fiso→ = λ n → ? - ; fiso← = λ x → ? + ; fiso→ = biso + ; fiso← = biso1 } where -- -- an f g cn @@ -740,18 +741,33 @@ 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 - + -- injection of count-B + --- 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 zero (suc j) i<j bi bj le with is-B (fun← cn 0) | inspect count-B 0 | is-B (fun← cn (suc j)) | inspect count-B (suc j) + ... | no nisc | _ | _ | _ = ⊥-elim (nisc bi) + ... | yes _ | _ | no nisc | _ = ⊥-elim (nisc bj) + ... | yes _ | record { eq = eq1 } | yes _ | record { eq = eq2 } = ⊥-elim ( nat-≤> lem25 a<sa) where + lem22 : 1 ≡ count-B 0 + lem22 with is-B (fun← cn 0) | inspect count-B 0 + ... | yes _ | record { eq = eq1 } = refl + ... | no nisa | _ = ⊥-elim ( nisa bi ) + lem24 : count-B j ≡ 0 + lem24 = cong pred le + lem25 : 1 ≤ 0 + lem25 = begin + 1 ≡⟨ lem22 ⟩ + count-B 0 ≤⟨ count-B-mono {0} {j} z≤n ⟩ + count-B j ≡⟨ lem24 ⟩ + 0 ∎ where open ≤-Reasoning lem20 (suc i) zero () bi bj le - lem20 (suc i) (suc j) (s≤s i<j) bi bj le = ? where + lem20 (suc i) (suc j) (s≤s i<j) bi bj le = ⊥-elim ( nat-≡< lem24 lem21 ) where -- -- i < suc i ≤ j - -- suc (cb i) < cb (suc i) ≤ cb j - -- + -- cb i < suc (cb i) < cb (suc i) ≤ cb j + -- suc (cb i) ≡ suc (cb j) → cb 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 @@ -762,9 +778,8 @@ ... | 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 | _ = ? + ... | no nisc | _ | _ | _ = ⊥-elim (nisc bi) + ... | yes _ | _ | no nisc | _ = ⊥-elim (nisc bj) ... | yes _ | record { eq = eq1 } | yes _ | record { eq = eq2 } = sym (cong pred le) lem21 : suc (count-B i) ≤ count-B j lem21 = begin @@ -778,8 +793,6 @@ ... | 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 @@ -794,6 +807,9 @@ lem12 cb1 iscb1 cbeq = lem06 (suc i) cb1 isb iscb1 (trans eq1 cbeq) ... | no nisb | record { eq = eq1 } = lem07 n i eq + -- starting from 0, if count B i ≡ suc n, this is it + + lem09 : (i j : ℕ) → suc n ≤ j → j ≡ count-B i → CountB n lem09 0 (suc j) (s≤s le) eq with ≤-∨ (s≤s le) ... | case1 eq1 = lem07 n 0 (sym (trans eq1 eq )) ... | case2 (s≤s lt) with is-B (fun← cn 0) | inspect count-B 0 @@ -867,7 +883,7 @@ --- ℕ ⊆ List A ⊆ List (Maybe A) ⊆ List A ∧ List Bool ⊆ ℕ LMℕ : (A : Set ) → Bijection (List A) ℕ → Bijection (List (Maybe A)) ℕ -LMℕ A Ln = Countable-Bernstein (List A) (List (Maybe A)) (List A ∧ List Bool) Ln (LM1 A Ln) fi gi ? ? where +LMℕ A Ln = Countable-Bernstein (List A) (List (Maybe A)) (List A ∧ List Bool) Ln (LM1 A Ln) fi gi dec0 dec1 where f : List A → List (Maybe A) f [] = [] f (x ∷ t) = just x ∷ f t @@ -901,6 +917,25 @@ fi = record { f = f ; inject = f-inject } gi : InjectiveF (List (Maybe A)) (List A ∧ List Bool ) gi = record { f = g ; inject = g-inject } + dec0 : (c : List A ∧ List Bool) → Dec (Is (List A) (List A ∧ List Bool) (λ x → g (f x)) c) + dec0 ⟪ [] , [] ⟫ = yes record { a = [] ; fa=c = refl } + dec0 ⟪ h ∷ t , [] ⟫ = ? + dec0 ⟪ [] , true ∷ bt ⟫ = ? + dec0 ⟪ [] , false ∷ bt ⟫ = ? + dec0 ⟪ h ∷ t , (true ∷ bt) ⟫ with dec0 ⟪ t , bt ⟫ + ... | yes y = yes record { a = h ∷ Is.a y ; fa=c = cong₂ (λ j k → ⟪ h ∷ j , true ∷ k ⟫ ) (cong proj1 (Is.fa=c y)) (cong proj2 (Is.fa=c y)) } + ... | no n = no ( λ np → ⊥-elim ( n record { a = ? ; fa=c = ? } ) ) + dec0 ⟪ (h ∷ t) , (false ∷ bt) ⟫ = no ( λ np → ? ) + dec1 : (c : List A ∧ List Bool) → Dec (Is (List (Maybe A)) (List A ∧ List Bool) g c) + dec1 ⟪ [] , [] ⟫ = yes record { a = [] ; fa=c = refl } + dec1 ⟪ h ∷ t , [] ⟫ = ? + dec1 ⟪ [] , _ ∷ bt ⟫ = ? + dec1 ⟪ h ∷ t , true ∷ bt ⟫ with dec1 ⟪ t , bt ⟫ + ... | yes y = yes record { a = just h ∷ Is.a y ; fa=c = cong₂ (λ j k → ⟪ h ∷ j , true ∷ k ⟫ ) (cong proj1 (Is.fa=c y)) (cong proj2 (Is.fa=c y)) } + ... | no n = ? + dec1 ⟪ h ∷ t , false ∷ bt ⟫ with dec1 ⟪ t , bt ⟫ + ... | yes y = yes record { a = nothing ∷ Is.a y ; fa=c = cong₂ (λ j k → ⟪ h ∷ j , false ∷ k ⟫ ) (cong proj1 (Is.fa=c y)) (cong proj2 (Is.fa=c y)) } + ... | no n = ? -- open import Data.Fin --