Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1316:a6e3fa2ded00
bad appraoch
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 10 Jun 2023 20:22:28 +0900 |
| parents | 08cd04cc33fe |
| children | 97a637690bdf |
| files | src/bijection.agda |
| diffstat | 1 files changed, 13 insertions(+), 53 deletions(-) [+] |
line wrap: on
line diff
--- a/src/bijection.agda Sat Jun 10 16:22:47 2023 +0900 +++ b/src/bijection.agda Sat Jun 10 20:22:28 2023 +0900 @@ -589,7 +589,6 @@ field ac : ℕ n<ca : n < count-A ac - full : ac < count-A n → n ≡ ac record maxACN (n : ℕ) : Set where field @@ -612,61 +611,22 @@ 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) ; full = λ _ → refl } + ... | yes isa | record { eq = eq1 } = record { ac = zero ; n<ca = subst (λ k → 0 < k) (sym eq1) (s≤s z≤n) } ... | no nisa | record { eq = eq1 } = ⊥-elim ( nisa record { a = fun← an 0 ; fa=c = trans (sym (fiso← cn _)) (sym (cong (fun← cn) i=z)) } ) 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 ; full = ? } + ... | 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) with <-cmp (suc j) (count-A (maxAC.ac (lem10 j))) - ... | tri< a ¬b ¬c = record { ac = maxAC.ac (lem10 j) ; n<ca = a ; full = ? } -- 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 ; full = ? } where - -- - -- then suc j ≡ count-A (maxAC.ac (lem10 j)) - -- it means count-A is full - -- the new one must be above - -- - lem40 : (j : ℕ) → maxAC.ac (lem10 j) < count-A j → j ≡ maxAC.ac (lem10 j) - lem40 j j<ca = maxAC.full (lem10 j) j<ca - lem31 : suc j < count-A (fun→ cn (g (f (fun← an (suc j))))) - lem31 with <∨≤ j (fun→ cn (g (f (fun← an (suc j))))) - ... | case1 lt = lem12 _ lt ≤-refl where - lem13 : j < fun→ cn (g (f (fun← an (suc j)))) - lem13 = lt - -- suc j is current count of A - -- it increase at fun→ cn (g (f (fun← an (suc j)))) - -- otherwise ≤ - lem12 : (i : ℕ) → j < i → i ≤ fun→ cn (g (f (fun← an (suc j)))) → suc j < count-A i - lem12 (suc i) (s≤s sj<i) i≤fj with ≤-∨ sj<i - ... | case1 refl = lem16 where -- subst (λ k → k < count-A (suc i)) (sym eq) lem16 where - lem17 : i < count-A i - lem17 = subst (λ k → i < k ) ? a<sa - lem16 : suc i < count-A (suc i) - lem16 = ? - ... | case2 lt = ≤-trans lem14 lem15 where - lem14 : suc j < count-A i - lem14 = lem12 i lt (≤-trans refl-≤s i≤fj) - lem15 : count-A i ≤ count-A (suc i) - lem15 = count-A-≤cong refl-≤s - ... | 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 + lem10 (suc j) = nac where + ac = maxAC.ac (lem10 j) + nac : maxAC (suc j) + nac with <-cmp ac (fun→ cn (g (f (fun← an (suc j))))) + ... | tri< a ¬b ¬c = record { ac = fun→ cn (g (f (fun← an (suc j)))) ; n<ca = ? } + ... | tri≈ ¬a b ¬c = record { ac = ac ; n<ca = ? } + ... | tri> ¬a ¬b c = record { ac = ac ; n<ca = ? } + lem14 : j < count-A ac + lem14 = ? + lem13 : (i : ℕ) → i ≤ nac → suc j < count-A i + lem13 i i≤n = ? lem01 : (n i : ℕ) → n < count-B i → B lem01 zero zero lt with is-B (fun← cn zero)