Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1337:31c9f7fc6466
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 16 Jun 2023 08:49:25 +0900 |
| parents | d1aae9bbf30c |
| children | b969f1710434 |
| files | src/bijection.agda src/nat.agda |
| diffstat | 2 files changed, 145 insertions(+), 22 deletions(-) [+] |
line wrap: on
line diff
--- a/src/bijection.agda Wed Jun 14 12:34:45 2023 +0900 +++ b/src/bijection.agda Fri Jun 16 08:49:25 2023 +0900 @@ -599,26 +599,13 @@ ... | no nisA | yes isB = ≤-trans (ca≤cb0 n) px≤x ... | no nisA | no nisB = ca≤cb0 n - -- (c m) is the number of a of C , where there is (a m) - -- c = (g (f (fun← an (a m)))) : C contains all a which number is less than m + -- (c n) is + -- fun→ c, where c contains all "a" less than n + -- (i n : ℕ) → i < suc n → fun→ cn (g (f (fun← an i))) < suc (c n) c : (n : ℕ) → ℕ c zero = fun→ cn (g (f (fun← an zero))) c (suc n) = max (fun→ cn (g (f (fun← an (suc n))))) (c n) - a : (n : ℕ) → ℕ - a zero = zero - a (suc n) with <-cmp (fun→ cn (g (f (fun← an (suc n))))) (c n) - ... | tri< lt ¬b ¬c = c n - ... | tri≈ ¬a eq ¬c = suc n - ... | tri> ¬a ¬b lt = suc n - - a=cn : (n : ℕ) → c n ≡ fun→ cn (g (f (fun← an (a n)))) - a=cn zero = refl - a=cn (suc n) with <-cmp (fun→ cn (g (f (fun← an (suc n))))) (c n) - ... | tri< lt ¬b ¬c = ? - ... | tri≈ ¬a eq ¬c = ? - ... | tri> ¬a ¬b lt = ? - c< : (i n : ℕ) → i < suc n → fun→ cn (g (f (fun← an i))) < suc (c n) c< zero zero (s≤s z≤n) = a<sa c< (suc i) zero (s≤s ()) @@ -627,11 +614,124 @@ ... | case1 refl = s≤s (x≤max (fun→ cn (g (f (fun← an (suc n))))) (c n)) ... | case2 (s≤s (s≤s i<n)) = ≤-trans (c< i n (<-transʳ i<n a<sa)) (s≤s (y≤max (fun→ cn (InjectiveF.f gi (InjectiveF.f fi (fun← an (suc n))))) (c n))) + -- (c1 n i) is number of a which fun← an a ≤ n ∧ fun→ cn (g (f a)) < i ∧ g (f a) is A + + c1 : (n i : ℕ) → ℕ + c1 zero i with <-cmp (fun→ cn (g (f (fun← an zero)))) i + ... | tri< a ¬b ¬c = 1 + ... | tri≈ ¬a b ¬c = 1 + ... | tri> ¬a ¬b c₁ = 0 + c1 (suc n) i with <-cmp (fun→ cn (g (f (fun← an (suc n))))) i + ... | tri< a ¬b ¬c = suc (c1 n i) + ... | tri≈ ¬a b ¬c = suc (c1 n i) + ... | tri> ¬a ¬b c₁ = c1 n i + + c1-mono : {n i j : ℕ} → i ≤ j → (c1 n i ≡ c1 n j) ∨ (c1 n i < c1 n j) + c1-mono {zero} {i} {j} le with <-cmp (fun→ cn (g (f (fun← an zero)))) i | <-cmp (fun→ cn (g (f (fun← an zero)))) j + ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = case1 refl + ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = case1 refl + ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c₁ = ⊥-elim ( nat-≤> le (<-trans c₁ a) ) + ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = case1 refl + ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ = case1 refl + ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c₁ = ⊥-elim ( nat-≤> (subst (λ k → k ≤ _) (sym b) le) c₁ ) + ... | tri> ¬a ¬b c₁ | tri< a ¬b₁ ¬c = case2 ≤-refl + ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c = case2 ≤-refl + ... | tri> ¬a ¬b c₁ | tri> ¬a₁ ¬b₁ c₂ = case1 refl + c1-mono {suc n} {zero} {zero} z≤n = case1 refl + c1-mono {suc n} {zero} {suc j} z≤n with <-cmp (fun→ cn (g (f (fun← an (suc n))))) zero | <-cmp (fun→ cn (g (f (fun← an (suc n))))) (suc j) + | c1-mono {n} {zero} {suc j} z≤n + ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ | case1 eq = case1 (cong suc eq) + ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ | case2 le = case2 ( s≤s le ) + ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ | case1 eq = case1 (cong suc eq) + ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ | case2 le = case2 ( s≤s le ) + ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c₁ | _ = ⊥-elim ( nat-≡< (sym b) (≤-trans (s≤s z≤n) c₁) ) + ... | tri> ¬a ¬b c₁ | tri< a ¬b₁ ¬c | case1 eq = case2 ( subst (λ k → suc (c1 n zero) ≤ k ) (cong suc eq) ≤-refl ) + ... | tri> ¬a ¬b c₁ | tri< a ¬b₁ ¬c | case2 le = case2 (≤-trans le refl-≤s ) + ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c | case1 eq = case2 ( subst (λ k → suc (c1 n zero) ≤ k ) (cong suc eq) ≤-refl ) + ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c | case2 le = case2 (≤-trans le refl-≤s ) + ... | tri> ¬a ¬b c₁ | tri> ¬a₁ ¬b₁ c₂ | case1 eq = case1 eq + ... | tri> ¬a ¬b c₁ | tri> ¬a₁ ¬b₁ c₂ | case2 le = case2 le + c1-mono {suc n} {suc i} {suc j} (s≤s le) with <-cmp (fun→ cn (g (f (fun← an (suc n))))) (suc i) | <-cmp (fun→ cn (g (f (fun← an (suc n))))) (suc j) + | c1-mono {n} {suc i} {suc j} (s≤s le) + ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ | case1 eq = case1 (cong suc eq) + ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ | case2 le = case2 (s≤s le) + ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ | case1 eq = case1 (cong suc eq) + ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ | case2 le = case2 (s≤s le) + ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c₁ | u = ⊥-elim ( nat-≤> (s≤s le) (<-transˡ c₁ (≤-trans refl-≤s a ) )) + ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ | case1 eq = case1 (cong suc eq) + ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ | case2 le = case2 (s≤s le) + ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ | case1 eq = case1 (cong suc eq) + ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ | case2 le = case2 (s≤s le) + ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c₁ | u = ⊥-elim ( nat-≤> (subst (λ k → k ≤ _) (sym b) (s≤s le)) c₁ ) + ... | tri> ¬a ¬b c₁ | tri< a ¬b₁ ¬c | case1 eq = case2 ( subst (λ k → suc (c1 n (suc i)) ≤ k ) (cong suc eq) ≤-refl ) + ... | tri> ¬a ¬b c₁ | tri< a ¬b₁ ¬c | case2 le = case2 (≤-trans le refl-≤s ) + ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c | case1 eq = case2 ( subst (λ k → suc (c1 n (suc i)) ≤ k ) (cong suc eq) ≤-refl ) + ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c | case2 le = case2 (≤-trans le refl-≤s ) + ... | tri> ¬a ¬b c₁ | tri> ¬a₁ ¬b₁ c₂ | u = u + + -- + c1-at-i : (n i : ℕ) → + (suc (c1 n i) ≡ c1 n (suc i) → Is A C (λ i → g (f i)) (g (f (fun← an i))) ) + ∧ (Is A C (λ i → g (f i)) (g (f (fun← an i))) → suc (c1 n i) ≡ c1 n (suc i) ) + c1-at-i = ? + -- + -- c n < i means j < suc n → fun← an j < c n, we cannot have more else + -- ∃ j → j < suc n → c n < fun← an j + -- + c1-max : (n i : ℕ) → c n < i → c1 n i ≡ c1 n (suc i) + c1-max zero zero () + c1-max zero (suc i) (s≤s c0<i) with <-cmp (fun→ cn (g (f (fun← an zero)))) (suc i) + --- we only have one (fun← an zero), it is in c1 zero (suc i) ≡ c1 zero i ≡ 1 + ... | tri≈ ¬a b ¬c = ? where + lem00 : c1 zero i ≡ c1 zero (suc i) + lem00 = c1-max zero i ? + ... | tri> ¬a ¬b c = ? + ... | tri< a ¬b ¬c with is-A (g (f (fun← an zero))) + ... | yes _ = ? + ... | no _ = ? + c1-max (suc n) zero () + c1-max (suc n) (suc i) cn<i with <-cmp (fun→ cn (g (f (fun← an (suc n))))) (suc i) + --- we already have all j < suc n → (fun← an j), it is in c1 (suc n) (suc i) ≡ c1 (suc n) i ≡ suc n + ... | tri≈ ¬a b ¬c = ? -- c1-max n i ? + ... | tri> ¬a ¬b c = ? -- c1-max n i ? + ... | tri< a ¬b ¬c with is-A (g (f (fun← an (suc n)))) + ... | yes _ = ? -- cong suc (c1-max n i ?) + ... | no _ = ? -- c1-max n i ? + + --- c1 n i + c1+1 : (n i : ℕ) → i < c n → Is A C (λ i → g (f i)) (g (f (fun← an i))) → suc (c1 n i) ≡ c1 n (suc i) + c1+1 zero i i<c0 isa = c1+10 where + c1+10 : suc (c1 zero i) ≡ c1 zero (suc i) + c1+10 with <-cmp (fun→ cn (g (f (fun← an zero)))) i + ... | tri≈ ¬a b ¬c = ⊥-elim (¬a ? ) + ... | tri> ¬a ¬b c = ? + ... | tri< a ¬b ¬c with is-A (g (f (fun← an zero))) + ... | yes _ = ? + ... | no _ = ? + c1+1 (suc n) i i<cn isa with <-cmp (fun→ cn (g (f (fun← an (suc n))))) i + ... | tri≈ ¬a b ¬c = ? -- c1+1 n i ? + ... | tri> ¬a ¬b c = ? -- c1+1 n i ? + ... | tri< a ¬b ¬c with is-A (g (f (fun← an (suc n)))) + ... | yes _ = ? -- cong suc (c1+1 n i ?) + ... | no _ = ? -- c1+1 n i ? + + c1=c1 : (n i : ℕ) → i < c n → ¬ (Is A C (λ i → g (f i)) (g (f (fun← an i)))) → c1 n i ≡ c1 n (suc i) + c1=c1 = ? + + c1=sn : (n i : ℕ) → c n < i → c1 n i ≡ suc n + c1=sn = ? + + c1=count-A : (n i : ℕ) → c n < i → c1 n i ≤ count-A n + c1=count-A = ? + record maxAC (n : ℕ) : Set where field ac : ℕ n<ca : n < count-A ac + lem03 : (n : ℕ) → maxAC n + lem03 n = record { ac = c1 n (suc (c n)) ; n<ca = ? } + -- -- we have n C sequcence having n A which is less than c n as FList (c n) , so we have n -- c i = i th FL (c n) where @@ -642,8 +742,10 @@ -- it means -- n < count-A (c n) -- + cl07 : { i j : ℕ } → suc i < suc j → i < j cl07 {i} {j} (s≤s lt) = lt + lem02 : (n : ℕ) → maxAC n lem02 n = record { ac = c n ; n<ca = n<ca n } where ca+1 : (i : ℕ) → i < fun→ cn (g (f (fun← an i))) → count-A i < count-A (fun→ cn (g (f (fun← an i)))) @@ -666,10 +768,28 @@ ... | suc ca | record { eq = eq1 } = cl24 where cl24 : 1 ≤ count-A (suc ca) cl24 = ? - n<ca (suc n) with fun→ cn (g (f (fun← an n))) | inspect (fun→ cn) (g (f (fun← an n))) - ... | zero | record { eq = eq1 } = cl25 where + n<ca (suc n) with <-cmp (c n) (fun→ cn (g (f (fun← an (suc n))))) + ... | tri< ca<an ¬b ¬c = ? where + cl26 : n < count-A (c n) + cl26 = n<ca n + cl25 : suc (suc n) ≤ count-A (fun→ cn (g (f (fun← an (suc n))))) + cl25 = begin + suc (suc n) ≤⟨ s≤s (n<ca n) ⟩ + suc (count-A (c n)) ≤⟨ s≤s (count-A-mono ( sx≤py→x≤y ( begin + suc (c n) ≤⟨ ca<an ⟩ + fun→ cn (InjectiveF.f gi (InjectiveF.f fi (fun← an (suc n)))) ≤⟨ ? ⟩ + suc (pred (fun→ cn (InjectiveF.f gi (InjectiveF.f fi (fun← an (suc n)))))) ∎ ) )) ⟩ + suc (count-A (pred (fun→ cn (g (f (fun← an (suc n))))))) ≡⟨ ? ⟩ + count-A (fun→ cn (g (f (fun← an (suc n))))) ∎ where + open ≤-Reasoning + ... | tri≈ ¬a ca=an ¬c = ? + ... | tri> ¬a ¬b an<ca = ? where cl25 : suc (suc n) ≤ count-A (max (fun→ cn (g (f (fun← an (suc n))))) (c n)) cl25 = ? + cl27 : fun→ cn (g (f (fun← an (suc n) )) ) < c (suc n) + cl27 = ? + cl26 : fun→ cn (g (f (fun← an ? )) ) < fun→ cn (g (f (fun← an (suc n)))) + cl26 = ? -- -- count-A (c m) < count (c (suc m)) ≤ count (c n) -- fun→ cn (g (f (fun← an i))) < suc (fun→ cn (g (f (fun← an (suc n))))) ≤ fun→ cn (g (f (fun← an j))) ≤ fun→ cn (g (f (fun← an j))) ≡ c n @@ -677,10 +797,6 @@ -- fun→ cn (g (f (fun← an i))) < fun→ cn (g (f (fun← an (suc n)))) < fun→ cn (g (f (fun← an j))) ≤ fun→ cn (g (f (fun← an j))) ≡ c n -- c i c (suc i) c (suc (suc i)) c (suc n) -- count-A (c m) = count-A (c (suc m)) count-A (c (suc m)) < count (c (suc (suc m)) ≤ count (c (suc n)) - ... | suc ca | record { eq = eq1 } = ? where - cl26 : suc (suc n) ≤ count-A (max (fun→ cn (g (f (fun← an (suc n))))) (c n)) - cl26 = ? - -- = <-transʳ (count-A-mono ?) (ca+1 zero ?) where record CountB (n : ℕ) : Set where field
--- a/src/nat.agda Wed Jun 14 12:34:45 2023 +0900 +++ b/src/nat.agda Fri Jun 16 08:49:25 2023 +0900 @@ -252,6 +252,12 @@ px≤py {zero} {suc y} lt = z≤n px≤py {suc x} {suc y} (s≤s lt) = lt +sx≤py→x≤y : {x y : ℕ } → suc x ≤ suc y → x ≤ y +sx≤py→x≤y (s≤s lt) = lt + +sx<py→x<y : {x y : ℕ } → suc x < suc y → x < y +sx<py→x<y (s≤s lt) = lt + sx≤y→x≤y : {x y : ℕ } → suc x ≤ y → x ≤ y sx≤y→x≤y {zero} {suc y} (s≤s le) = z≤n sx≤y→x≤y {suc x} {suc y} (s≤s le) = s≤s (sx≤y→x≤y {x} {y} le) @@ -724,3 +730,4 @@ ; ind = λ {p} prev → ind p prev } +