Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1313:b8489dcae236
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 10 Jun 2023 11:47:43 +0900 |
| parents | 1ea21618aa61 |
| children | 8cd195679686 |
| files | src/bijection.agda |
| diffstat | 1 files changed, 75 insertions(+), 12 deletions(-) [+] |
line wrap: on
line diff
--- a/src/bijection.agda Sat Jun 10 08:05:56 2023 +0900 +++ b/src/bijection.agda Sat Jun 10 11:47:43 2023 +0900 @@ -531,6 +531,40 @@ ... | yes isb = suc (count-A n) ... | no nisb = count-A n + count-A-≤cong : {i j : ℕ} → i ≤ j → count-A i ≤ count-A j + count-A-≤cong {i} {j} i≤j with ≤-∨ i≤j + ... | case1 refl = ≤-refl + ... | case2 i<j = lem00 _ _ i<j where + lem00 : (i j : ℕ) → i < j → count-A i ≤ count-A j + lem00 i (suc j) (s≤s i<j) = ≤-trans (count-A-≤cong i<j) (lem01 j) where + lem01 : (j : ℕ) → count-A j ≤ count-A (suc j) + lem01 zero with is-A (fun← cn (suc zero)) + ... | yes isb = refl-≤s + ... | no nisb = ≤-refl + lem01 (suc n) with is-A (fun← cn (suc (suc n))) + ... | yes isb = refl-≤s + ... | no nisb = ≤-refl + + count-A<i : (i : ℕ) → count-A i ≤ suc i + count-A<i zero with is-A (fun← cn zero) | inspect ( count-A ) zero + ... | yes isa | record { eq = eq1 } = ≤-refl + ... | no nisa | record { eq = eq1 } = refl-≤s + count-A<i (suc i) with is-A (fun← cn (suc i)) | inspect ( count-A ) (suc i) + ... | yes isa | record { eq = eq1 } = s≤s ( count-A<i i ) + ... | no nisa | record { eq = eq1 } = ≤-trans (count-A<i i ) refl-≤s + + full-a : (i : ℕ) → i < count-A i → Is A C (λ x → g (f x)) (fun← cn i) + full-a zero i<ci with is-A (fun← cn zero) | inspect ( count-A ) zero + ... | yes isa | record { eq = eq1 } = isa + ... | no nisa | record { eq = eq1 } = ⊥-elim ( nat-≡< refl i<ci ) + full-a (suc i) i<ci with is-A (fun← cn (suc i)) | inspect ( count-A ) (suc i) + ... | yes isa | record { eq = eq1 } = isa + ... | no nisa | record { eq = eq1 } = ⊥-elim ( nat-≤> (≤-trans lem36 lem39) a<sa ) where + lem36 : suc (suc i) ≤ count-A i + lem36 = i<ci + lem39 : count-A i ≤ suc i + lem39 = count-A<i i + ¬isA∧isB : (y : C ) → Is A C (λ x → g ( f x)) y → ¬ Is B C g y → ⊥ ¬isA∧isB y isa nisb = ⊥-elim ( nisb record { a = f (Is.a isa) ; fa=c = lem } ) where lem : g (f (Is.a isa)) ≡ y @@ -570,11 +604,11 @@ ... | tri≈ ¬a b ¬c = record { acn = maxACN.acn (maxac i) ; cn<acn = ? } ... | tri> ¬a ¬b c = record { acn = fun→ cn (g (f (fun← an (suc i)))) ; cn<acn = ? } lem03 : (i : ℕ) → maxAC i - lem03 i = lem10 i ? where + lem03 i = lem10 i where lem11 : (i : ℕ) → i ≤ n → fun→ cn (g (f (fun← an i))) ≤ maxACN.acn (maxac n) lem11 i i≤n = maxACN.cn<acn (maxac n) i i≤n - lem10 : (j : ℕ) → j ≤ maxACN.acn (maxac n) → maxAC j - lem10 zero j≤m = lem12 _ refl where + lem10 : (j : ℕ) → maxAC j + lem10 zero = lem12 _ refl where lem12 : (i : ℕ) → i ≡ fun→ cn (g (f (fun← an zero))) → maxAC zero lem12 zero i=z with is-A (fun← cn zero) | inspect ( count-A ) zero ... | yes isa | record { eq = eq1 } = record { ac = zero ; n<ca = subst (λ k → 0 < k) (sym eq1) (s≤s z≤n) } @@ -582,15 +616,44 @@ lem12 (suc i) i=z with is-A (fun← cn (suc i)) | inspect ( count-A ) (suc i) ... | yes isa | record { eq = eq1 } = record { ac = suc i ; n<ca = subst (λ k → 0 < k) (sym eq1) 0<s } ... | no nisa | record { eq = eq1 } = ⊥-elim ( nisa record { a = fun← an zero ; fa=c = trans (sym (fiso← cn _)) (sym (cong (fun← cn) i=z)) } ) - lem10 (suc j) j≤m = ? where - lem13 : (i : ℕ) → i ≡ fun→ cn (g (f (fun← an (suc j)))) → maxAC (suc j) - lem13 zero i=z with is-A (fun← cn zero) | inspect ( count-A ) zero - ... | yes isa | record { eq = eq1 } = record { ac = zero ; n<ca = ? } - ... | no nisa | record { eq = eq1 } = ⊥-elim ( nisa record { a = fun← an 0 ; fa=c = trans (sym (fiso← cn _)) (sym (cong (fun← cn) ? )) } ) - lem13 (suc i) i=z with is-A (fun← cn (suc i)) | inspect ( count-A ) (suc i) - ... | yes isa | record { eq = eq1 } = record { ac = suc i ; n<ca = ? } -- subst (λ k → 0 < k) (sym eq1) 0<s } - ... | no nisa | record { eq = eq1 } = ⊥-elim ( nisa record { a = fun← an zero ; fa=c = trans (sym (fiso← cn _)) (sym (cong (fun← cn) ? )) } ) - + lem10 (suc j) with <-cmp (suc j) (count-A (maxAC.ac (lem10 j))) + ... | tri< a ¬b ¬c = record { ac = maxAC.ac (lem10 j) ; n<ca = a } -- if suc j < count-A (maxAC.ac lem14) , we can reuse lem10 j + ... | tri> ¬a ¬b (s≤s c) = ⊥-elim ( nat-≤> c (maxAC.n<ca (lem10 j))) + ... | tri≈ ¬a sj=ca ¬c = record { ac = fun→ cn (g (f (fun← an (suc j)))) ; n<ca = lem31 } where + -- + -- then suc j ≡ count-A (maxAC.ac (lem10 j)) + -- it means count-A is full + -- the new one must be above + -- + lem31 : suc j < count-A (fun→ cn (g (f (fun← an (suc j))))) + lem31 with <∨≤ (suc j) (fun→ cn (g (f (fun← an (suc j))))) + ... | case1 lt = lem12 _ refl where + lem12 : (i : ℕ) → i ≡ fun→ cn (g (f (fun← an (suc j)))) → suc j < count-A (fun→ cn (g (f (fun← an (suc j))))) + lem12 zero i=z with is-A (fun← cn zero) | inspect ( count-A ) zero + ... | yes isa | record { eq = eq1 } = ? + ... | no nisa | record { eq = eq1 } = ⊥-elim ( nisa record { a = fun← an 0 ; fa=c = trans (sym (fiso← cn _)) (sym (cong (fun← cn) ? )) } ) + lem12 (suc i) i=z with is-A (fun← cn (suc i)) | inspect ( count-A ) (suc i) + ... | yes isa | record { eq = eq1 } = ? + ... | no nisa | record { eq = eq1 } = ⊥-elim ( nisa record { a = fun← an zero ; fa=c = trans (sym (fiso← cn _)) (sym (cong (fun← cn) ?)) } ) + ... | case2 le = ? where + -- count-A<i : (i : ℕ) → count-A i ≤ suc i + lem33 : (i : ℕ) → i ≡ fun→ cn (g (f (fun← an (suc j)))) → ¬ (i ≤ maxAC.ac (lem10 j)) + lem33 zero i=f i≤m = ? + lem33 (suc i) si=f= i≤m = ? + lem34 : maxAC.ac (lem10 j) ≤ fun→ cn (g (f (fun← an (suc j)))) + lem34 = ? + lem32 : suc j ≤ count-A (fun→ cn (g (f (fun← an (suc j))))) + lem32 with <∨≤ (count-A (fun→ cn (g (f (fun← an (suc j))))) ) (suc j) + ... | case2 le = le + ... | case1 lt = ? + lem30 : maxAC.ac (lem10 j) < fun→ cn (g (f (fun← an (suc j)))) + lem30 = ? + lem20 : suc j ≡ count-A (maxAC.ac (lem10 j)) + lem20 = sj=ca + lem14 : maxAC j + lem14 = lem10 j + lem17 : j < count-A (maxAC.ac lem14) + lem17 = maxAC.n<ca lem14 lem01 : (n i : ℕ) → n < count-B i → B lem01 zero zero lt with is-B (fun← cn zero)