Mercurial > hg > Members > kono > Proof > ZF-in-agda

comparison src/bijection.agda @ 1383:51abc18e6f17

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
using clist is no good
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 23 Jun 2023 15:36:09 +0900
parents 4ecb12396ebd
children 0d29328c0441
comparison
equal deleted inserted replaced
1382:4ecb12396ebd 1383:51abc18e6f17
612 ... | case2 le = ⊥-elim (nat-≤> z≤n le ) 612 ... | case2 le = ⊥-elim (nat-≤> z≤n le )
613 lem00 (suc j) f≤j with ≤-∨ f≤j 613 lem00 (suc j) f≤j with ≤-∨ f≤j
614 ... | case1 eq = here ( trans (sym (fiso← cn _)) ( cong (fun← cn) eq )) 614 ... | case1 eq = here ( trans (sym (fiso← cn _)) ( cong (fun← cn) eq ))
615 ... | case2 (s≤s le) = there (lem00 j le) 615 ... | case2 (s≤s le) = there (lem00 j le)
616 616
617 -- cNL : (n : ℕ ) → NL n
618 -- cNL n = record { nlist = clist (c n) ; anyn = λ i le → clist-any n i le }
619
620
621 ca-list : List C → ℕ 617 ca-list : List C → ℕ
622 ca-list [] = 0 618 ca-list [] = 0
623 ca-list (h ∷ t) with is-A h 619 ca-list (h ∷ t) with is-A h
624 ... | yes _ = suc (ca-list t) 620 ... | yes _ = suc (ca-list t)
625 ... | no _ = ca-list t 621 ... | no _ = ca-list t
710 suc (suc i) ≤⟨ s≤s (lem30 i _ (≤-trans a≤sa i≤n) (del-any i cl a) ) ⟩ 706 suc (suc i) ≤⟨ s≤s (lem30 i _ (≤-trans a≤sa i≤n) (del-any i cl a) ) ⟩
711 suc (ca-list (del (suc i) cl a)) ≡⟨ del-ca (suc i) cl a ⟩ 707 suc (ca-list (del (suc i) cl a)) ≡⟨ del-ca (suc i) cl a ⟩
712 ca-list cl ∎ where 708 ca-list cl ∎ where
713 open ≤-Reasoning 709 open ≤-Reasoning
714 710
711 anygb : (b : B) → Any (_≡_ (g b)) (clist (c (fun→ cn (g b))))
712 anygb = ?
713
714 bton1 : B → ℕ
715 bton1 b = bton10 b (clist (c (fun→ cn (g b)))) ? where
716 bton10 : (b : B) → (x : List C) → Any (_≡_ (g b)) x → ℕ
717 bton10 b (h ∷ t) (here px) = count-B ( fun→ cn h )
718 bton10 b (h ∷ t) (there ax) = bton10 b t ax
719
720 anycb : (n : ℕ) → Any (λ c₁ → Is B C g c₁ ∧ (count-B (fun→ cn c₁) ≡ n)) (clist (c n))
721 anycb = ?
722
723 ntob1 : (n : ℕ) → B
724 ntob1 n = bton10 n (clist (c n)) ? where
725 bton10 : (n : ℕ) → (x : List C) → Any (λ c → Is B C g c ∧ (count-B (fun→ cn c) ≡ n)) x → B
726 bton10 n (h ∷ t) (here px) = Is.a (proj1 px)
727 bton10 n (h ∷ t) (there ax) = bton10 n t ax
728
715 record maxAC (n : ℕ) : Set where 729 record maxAC (n : ℕ) : Set where
716 field 730 field
717 ac : ℕ 731 ac : ℕ
718 n<ca : n < count-A ac 732 n<ca : n < count-A ac
719 733
736 lem07 : (n i : ℕ) → count-B i ≡ suc n → CountB n 750 lem07 : (n i : ℕ) → count-B i ≡ suc n → CountB n
737 lem07 n 0 eq with is-B (fun← cn 0) | inspect count-B 0 751 lem07 n 0 eq with is-B (fun← cn 0) | inspect count-B 0
738 ... | yes isb | record { eq = eq1 } = record { b = Is.a isb ; cb = 0 ; b=cn = sym (Is.fa=c isb) ; cb=n = trans eq1 eq 752 ... | yes isb | record { eq = eq1 } = record { b = Is.a isb ; cb = 0 ; b=cn = sym (Is.fa=c isb) ; cb=n = trans eq1 eq
739 ; cb-inject = λ cb1 cb1eq → lem12 cb1 (subst (λ k → k ≡ count-B cb1) eq1 cb1eq) } where 753 ; cb-inject = λ cb1 cb1eq → lem12 cb1 (subst (λ k → k ≡ count-B cb1) eq1 cb1eq) } where
740 lem12 : (cb1 : ℕ) → 1 ≡ count-B cb1 → 0 ≡ cb1 754 lem12 : (cb1 : ℕ) → 1 ≡ count-B cb1 → 0 ≡ cb1
741 lem12 = ? 755 lem12 cb1 cbeq with <-cmp 0 cb1
756 ... | tri≈ ¬a b ¬c = b
757 ... | tri< a ¬b ¬c = ?
742 ... | no nisb | record { eq = eq1 } = ⊥-elim ( nat-≡< eq (s≤s z≤n ) ) 758 ... | no nisb | record { eq = eq1 } = ⊥-elim ( nat-≡< eq (s≤s z≤n ) )
743 lem07 n (suc i) eq with is-B (fun← cn (suc i)) | inspect count-B (suc i) 759 lem07 n (suc i) eq with is-B (fun← cn (suc i)) | inspect count-B (suc i)
744 ... | 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 760 ... | 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
745 ; cb-inject = λ cb1 cb1eq → lem12 cb1 (subst (λ k → k ≡ count-B cb1) eq1 cb1eq) } where 761 ; cb-inject = λ cb1 cb1eq → lem12 cb1 (subst (λ k → k ≡ count-B cb1) eq1 cb1eq) } where
746 lem12 : (cb1 : ℕ) → suc (count-B i) ≡ count-B cb1 → suc i ≡ cb1 762 lem12 : (cb1 : ℕ) → suc (count-B i) ≡ count-B cb1 → suc i ≡ cb1
747 lem12 cb cbeq with CountB.cb-inject ( lem09 n (count-B n) ? refl ) 763 lem12 cb1 cbeq with <-cmp (suc i) cb1
748 ... | t = ? 764 ... | tri< a ¬b ¬c = ?
765 ... | tri≈ ¬a b ¬c = b
766 ... | tri> ¬a ¬b c₁ = ?
767 -- with CountB.cb-inject ( lem09 n (count-B n) ? refl )
768 -- ... | t = ?
749 ... | no nisb | record { eq = eq1 } = lem07 n i eq 769 ... | no nisb | record { eq = eq1 } = lem07 n i eq
750 770
751 lem09 0 (suc j) (s≤s le) eq with ≤-∨ (s≤s le) 771 lem09 0 (suc j) (s≤s le) eq with ≤-∨ (s≤s le)
752 ... | case1 eq1 = lem07 n 0 (sym (trans eq1 eq )) 772 ... | case1 eq1 = lem07 n 0 (sym (trans eq1 eq ))
753 ... | case2 (s≤s lt) with is-B (fun← cn 0) | inspect count-B 0 773 ... | case2 (s≤s lt) with is-B (fun← cn 0) | inspect count-B 0