Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1358:4eac5585b6b1
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 19 Jun 2023 12:33:23 +0900 |
| parents | 29f686c654bf |
| children | 88356bb882d4 |
| files | src/bijection.agda |
| diffstat | 1 files changed, 35 insertions(+), 15 deletions(-) [+] |
line wrap: on
line diff
--- a/src/bijection.agda Mon Jun 19 11:22:29 2023 +0900 +++ b/src/bijection.agda Mon Jun 19 12:33:23 2023 +0900 @@ -960,18 +960,25 @@ lem12 with <-cmp n (fun→ an (Is.a isa)) | c1+1 n i isa ... | tri< a ¬b ¬c | eq = ≤-trans (subst (λ k → k ≤ count-A i) eq (c1<ca n i)) a≤sa ... | tri≈ ¬a b ¬c | eq = begin - c1 n (suc i) ≡⟨ sym eq ⟩ - suc ( c1 n i) ≤⟨ s≤s (c1<ca n i) ⟩ - suc (count-A i) ∎ where open ≤-Reasoning + c1 n (suc i) ≡⟨ sym eq ⟩ + suc ( c1 n i) ≤⟨ s≤s (c1<ca n i) ⟩ + suc (count-A i) ∎ where open ≤-Reasoning ... | tri> ¬a ¬b c₁ | eq = begin - c1 n (suc i) ≡⟨ sym eq ⟩ - suc ( c1 n i) ≤⟨ s≤s (c1<ca n i) ⟩ - suc (count-A i) ∎ where open ≤-Reasoning + c1 n (suc i) ≡⟨ sym eq ⟩ + suc ( c1 n i) ≤⟨ s≤s (c1<ca n i) ⟩ + suc (count-A i) ∎ where open ≤-Reasoning ca01 : c1 (suc n) (suc i) ≤ suc (count-A i) ca01 with <-cmp (fun→ cn (g (f (fun← an (suc n))))) (suc i) - ... | tri< a ¬b ¬c = lem13 where -- count-A contains (suc i), so keep ≤-relation - lem13 : suc (c1 n (suc i)) ≤ suc (count-A i) - lem13 = ? + ... | tri< a ¬b ¬c = lem13 n ≤-refl where -- count-A contains (suc i), so keep ≤-relation + lem13 : (j : ℕ) → j ≤ n → suc (c1 j (suc i)) ≤ suc (count-A i) + lem13 0 j≤n with <-cmp (fun→ cn (g (f (fun← an 0)))) (suc i) + ... | tri< a ¬b ¬c = ? + ... | tri≈ ¬a b ¬c = ? + ... | tri> ¬a ¬b c₁ = ? + lem13 (suc j) j≤n with <-cmp (fun→ cn (g (f (fun← an (suc j))))) (suc i) + ... | tri< a ¬b ¬c = ? + ... | tri≈ ¬a b ¬c = ? + ... | tri> ¬a ¬b c₁ = ? ... | tri≈ ¬a b ¬c = lem13 where -- count-A contains (suc i) here lem15 : c1 n i ≡ c1 n (suc i) lem15 with <-cmp n (fun→ an (Is.a isa)) | c1+1 n i isa @@ -979,12 +986,25 @@ ... | tri≈ ¬a bi ¬c | eq = ⊥-elim ( nat-≡< (sym ( inject-cgf ( trans b lem16 ))) a<sa ) where lem16 : suc i ≡ fun→ cn (g (f (fun← an n ))) lem16 = begin - suc i ≡⟨ sym ( fiso→ cn _) ⟩ - fun→ cn (fun← cn (suc i)) ≡⟨ cong (fun→ cn) (sym (Is.fa=c isa)) ⟩ - fun→ cn (g (f (Is.a isa))) ≡⟨ cong (λ k → fun→ cn (g (f k)) ) (sym (fiso← an _)) ⟩ - fun→ cn (g (f (fun← an (fun→ an (Is.a isa))))) ≡⟨ cong (λ k → fun→ cn (g (f (fun← an k)))) (sym bi) ⟩ - fun→ cn (g (f (fun← an n ))) ∎ where open ≡-Reasoning - ... | tri> ¬a ¬b c₁ | eq = ? + suc i ≡⟨ sym ( fiso→ cn _) ⟩ + fun→ cn (fun← cn (suc i)) ≡⟨ cong (fun→ cn) (sym (Is.fa=c isa)) ⟩ + fun→ cn (g (f (Is.a isa))) ≡⟨ cong (λ k → fun→ cn (g (f k)) ) (sym (fiso← an _)) ⟩ + fun→ cn (g (f (fun← an (fun→ an (Is.a isa))))) ≡⟨ cong (λ k → fun→ cn (g (f (fun← an k)))) (sym bi) ⟩ + fun→ cn (g (f (fun← an n ))) ∎ where open ≡-Reasoning + ... | tri> ¬a ¬b c₁ | eq = ⊥-elim ( nat-≡< refl lem17 ) where + lem18 : fun→ cn (g (f (fun← an (suc n)))) ≡ fun→ cn (g (f (fun← an (fun→ an (Is.a isa))))) + lem18 = begin + fun→ cn (g (f (fun← an (suc n)))) ≡⟨ b ⟩ + suc i ≡⟨ sym ( fiso→ cn _) ⟩ + fun→ cn (fun← cn (suc i)) ≡⟨ sym (cong (fun→ cn) (Is.fa=c isa)) ⟩ + fun→ cn (g (f (Is.a isa))) ≡⟨ cong (λ k → fun→ cn (g (f k))) (sym (fiso← an _)) ⟩ + fun→ cn (g (f (fun← an (fun→ an (Is.a isa))))) ∎ where open ≡-Reasoning + lem17 : suc n ≤ n + lem17 = begin + suc n <⟨ s≤s a<sa ⟩ + suc (suc n) ≡⟨ cong (λ k → suc k) (inject-cgf lem18 ) ⟩ + suc (fun→ an (Is.a isa)) ≤⟨ c₁ ⟩ + n ∎ where open ≤-Reasoning lem13 : suc (c1 n (suc i)) ≤ suc (count-A i) lem13 = s≤s ( subst (λ k → k ≤ count-A i) lem15 ( c1<ca n i) ) ... | tri> ¬a ¬b c₁ = lem12 -- count-A is one degree larger now