Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1377:ddb581d5599b
suc n
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 23 Jun 2023 08:52:08 +0900 |
| parents | aca9b1e67503 |
| children | 5349fe40b6d4 |
| files | src/bijection.agda |
| diffstat | 1 files changed, 26 insertions(+), 29 deletions(-) [+] |
line wrap: on
line diff
--- a/src/bijection.agda Fri Jun 23 08:13:22 2023 +0900 +++ b/src/bijection.agda Fri Jun 23 08:52:08 2023 +0900 @@ -674,8 +674,8 @@ any-cl : (i : ℕ) → (cl : List C) → Set any-cl i cl = (j : ℕ) → j ≤ i → Any (_≡_ (g (f (fun← an j)))) cl - n<ca-list : (n : ℕ) → n < ca-list (clist (c n)) - n<ca-list n = lem30 n (clist (c n)) ≤-refl (λ j le → clist-any n j le ) where + n≤ca-list : (n : ℕ) → n ≤ ca-list (clist (c n)) + n≤ca-list n = lem30 n (clist (c n)) ≤-refl (λ j le → clist-any n j le ) where -- -- we have ANY i on i ≤ n, so we can remove n element from clist (c n) -- induction on n is no good, because (ani (suc n)) may happen in clist (c n) @@ -700,14 +700,14 @@ → suc (ca-list (del i cl a)) ≡ ca-list cl del-ca i cl a = a-list-ca i cl (a i ≤-refl) - lem30 : (i : ℕ) → (cl : List C) → (i≤n : i ≤ n) → (a : any-cl i cl) → i < ca-list cl + lem30 : (i : ℕ) → (cl : List C) → (i≤n : i ≤ n) → (a : any-cl i cl) → i ≤ ca-list cl lem30 0 cl i≤n a = begin - 1 ≤⟨ s≤s z≤n ⟩ - suc (ca-list (del 0 cl a) ) ≡⟨ del-ca 0 cl a ⟩ - ca-list cl ∎ where + 0 ≤⟨ z≤n ⟩ + suc (ca-list (del 0 cl a) ) ≡⟨ del-ca 0 cl a ⟩ + ca-list cl ∎ where open ≤-Reasoning lem30 (suc i) cl i≤n a = begin - suc (suc i) ≤⟨ s≤s (lem30 i _ (≤-trans a≤sa i≤n) (del-any i cl a) ) ⟩ + suc i ≤⟨ s≤s (lem30 i _ (≤-trans a≤sa i≤n) (del-any i cl a) ) ⟩ suc (ca-list (del (suc i) cl a)) ≡⟨ del-ca (suc i) cl a ⟩ ca-list cl ∎ where open ≤-Reasoning @@ -715,22 +715,23 @@ record maxAC (n : ℕ) : Set where field ac : ℕ - n<ca : n < count-A ac + n<ca : n ≤ count-A ac lem02 : (n : ℕ) → maxAC n - lem02 n = record { ac = c n ; n<ca = subst (λ k → n < k) (ca-list=count-A (c n)) (n<ca-list n ) } + lem02 n = record { ac = c n ; n<ca = subst (λ k → n ≤ k) (ca-list=count-A (c n)) (n≤ca-list n ) } record CountB (n : ℕ) : Set where field b : B cb : ℕ b=cn : fun← cn cb ≡ g b - cb=n : count-B cb ≡ suc n + cb=n : count-B cb ≡ n - lem01 : (n i : ℕ) → suc n ≤ count-B i → CountB n - lem01 n i le = lem09 i (count-B i) le refl where + lem01 : (n i : ℕ) → n ≤ count-B i → CountB n + lem01 0 i le = ? + lem01 (suc n) i le = ? where -- lem09 (suc n) i (count-B i) ? ? where -- starting from 0, if count B i ≡ suc n, this is it - lem07 : (n i : ℕ) → count-B i ≡ suc n → CountB n + lem07 : (n i : ℕ) → count-B i ≡ suc n → CountB (suc 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 } ... | no nisb | record { eq = eq1 } = ⊥-elim ( nat-≡< eq (s≤s z≤n ) ) @@ -738,37 +739,33 @@ ... | 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} ... | no nisb | record { eq = eq1 } = lem07 n i eq - lem09 : (i j : ℕ) → suc n ≤ j → j ≡ count-B i → CountB n - lem09 0 (suc j) (s≤s le) eq with ≤-∨ (s≤s le) + lem09 : (n i j : ℕ) → suc n ≤ j → j ≡ count-B i → CountB (suc n) + lem09 n 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 ... | yes isb | record { eq = eq1 } = ⊥-elim ( nat-≤> (≤-trans (s≤s lt) (refl-≤≡ eq) ) (s≤s (s≤s z≤n)) ) ... | no nisb | record { eq = eq1 } = ⊥-elim (nat-≡< (sym eq) (s≤s z≤n)) - lem09 (suc i) (suc j) (s≤s le) eq with ≤-∨ (s≤s le) + lem09 n (suc i) (suc j) (s≤s le) eq with ≤-∨ (s≤s le) ... | case1 eq1 = lem07 n (suc i) (sym (trans eq1 eq )) ... | case2 (s≤s lt) with is-B (fun← cn (suc i)) | inspect count-B (suc i) - ... | yes isb | record { eq = eq1 } = lem09 i j lt (cong pred eq) - ... | no nisb | record { eq = eq1 } = lem09 i (suc j) (≤-trans lt a≤sa) eq + ... | yes isb | record { eq = eq1 } = lem09 n i j lt (cong pred eq) + ... | no nisb | record { eq = eq1 } = lem09 n i (suc j) (≤-trans lt a≤sa) eq bton : B → ℕ bton b = count-B (fun→ cn (g b)) ntob : (n : ℕ) → B - ntob n = CountB.b (lem01 n (maxAC.ac (lem02 n)) (≤-trans (maxAC.n<ca (lem02 n)) (ca≤cb0 (maxAC.ac (lem02 n))) )) + ntob n = CountB.b (lem01 n (maxAC.ac (lem02 n)) (≤-trans (maxAC.n<ca (lem02 n)) (ca≤cb0 (maxAC.ac (lem02 n))))) biso : (n : ℕ) → bton (ntob n) ≡ n - biso 0 = ? - biso (suc n) = begin -- lem03 _ (≤-trans (maxAC.n<ca (lem02 n )) ?) refl - bton (ntob (suc n)) ≡⟨ ? ⟩ - count-B (fun→ cn (g (CountB.b CB1))) ≡⟨ sym ( cong (λ k → count-B (fun→ cn k)) ( CountB.b=cn CB1)) ⟩ - count-B (fun→ cn (fun← cn (CountB.cb CB1))) ≡⟨ ? ⟩ - count-B (CountB.cb CB1) ≡⟨ CountB.cb=n CB1 ⟩ - ? ≡⟨ ? ⟩ - suc n ∎ where + biso n = begin + bton (ntob (suc n)) ≡⟨ refl ⟩ + count-B (fun→ cn (g (CountB.b CB))) ≡⟨ sym ( cong (λ k → count-B (fun→ cn k)) ( CountB.b=cn CB)) ⟩ + count-B (fun→ cn (fun← cn (CountB.cb CB))) ≡⟨ ? ⟩ + count-B (CountB.cb CB) ≡⟨ CountB.cb=n CB ⟩ + n ∎ where open ≡-Reasoning CB = lem01 n (maxAC.ac (lem02 n)) (≤-trans (maxAC.n<ca (lem02 n)) (ca≤cb0 (maxAC.ac (lem02 n))) ) - CB1 = lem01 (suc n) (maxAC.ac (lem02 (suc n))) (≤-trans (maxAC.n<ca (lem02 (suc n))) (ca≤cb0 (maxAC.ac (lem02 (suc n)))) ) - biso1 : (b : B) → ntob (bton b) ≡ b biso1 b = ?