Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1304:f832e986427d
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Wed, 07 Jun 2023 11:26:03 +0900 |
parents | 66a6804d867b |
children | 81f66cec617e |
files | src/bijection.agda |
diffstat | 1 files changed, 36 insertions(+), 21 deletions(-) [+] |
line wrap: on
line diff
--- a/src/bijection.agda Wed Jun 07 09:42:58 2023 +0900 +++ b/src/bijection.agda Wed Jun 07 11:26:03 2023 +0900 @@ -506,9 +506,6 @@ f = InjectiveF.f fi g = InjectiveF.f gi - cbn : ℕ → ℕ - cbn n = fun→ cn (g (f (fun← an (suc n)))) - -- -- count number of valid A and B in C -- the count of B is the numner of B in Bijection B ℕ @@ -521,8 +518,6 @@ ca≤cb : ca ≤ cb na : {i : ℕ} → i < ca → A nb : {i : ℕ} → i < cb → B - ia : {i j : ℕ } → { i<c : i < ca } → {j<c : j < ca } → na i<c ≡ na j<c → i ≡ j - ib : {i j : ℕ } → { i<c : i < cb } → {j<c : j < cb } → nb i<c ≡ nb j<c → i ≡ j ¬isA∧isB : (y : C ) → Is A C (λ x → g ( f x)) y → ¬ Is B C g y → ⊥ ¬isA∧isB y isa nisb = ⊥-elim ( nisb record { a = f (Is.a isa) ; fa=c = lem } ) where @@ -534,25 +529,47 @@ lb : (n : ℕ ) → CB n lb zero with is-A (fun← cn zero) | is-B (fun← cn zero) - ... | yes isA | yes isB = record { ca = suc zero ; cb = suc zero ; cb≤n = ≤-refl ; ca≤cb = ≤-refl ; na = λ _ → Is.a isA ; nb = λ _ → Is.a isB ; ia = ? ; ib = ? } - ... | yes isA | no nisB = ⊥-elim ( ¬isA∧isB _ isA nisB ) - ... | no nisA | yes isB = record { ca = zero ; cb = suc zero ; cb≤n = ≤-refl ; ca≤cb = ? ; na = λ () ; nb = ? ; ia = ? ; ib = ? } - ... | no nisA | no nisB = record { ca = zero ; cb = zero ; cb≤n = ? ; ca≤cb = ? ; na = λ () ; nb = λ () ; ia = ? ; ib = ? } - lb (suc n) with is-A (fun← cn (suc n)) | is-B (fun← cn (suc n)) - ... | yes isA | yes isB = record { ca = suc (CB.ca (lb n)) ; cb = suc (CB.cb (lb n)) ; cb≤n = ? ; ca≤cb = ? ; na = ? ; nb = ? ; ia = ? ; ib = ? } + ... | yes isA | yes isB = record { ca = suc zero ; cb = suc zero ; cb≤n = ≤-refl ; ca≤cb = ≤-refl ; na = λ _ → Is.a isA ; nb = λ _ → Is.a isB } ... | yes isA | no nisB = ⊥-elim ( ¬isA∧isB _ isA nisB ) - ... | no nisA | yes isB = record { ca = CB.ca (lb n) ; cb = suc (CB.cb (lb n)) ; cb≤n = ? ; ca≤cb = ? ; na = ? ; nb = ? ; ia = ? ; ib = ? } - ... | no nisA | no nisB = record { ca = CB.ca (lb n) ; cb = CB.cb (lb n) ; cb≤n = ? ; ca≤cb = ? ; na = ? ; nb = ? ; ia = ? ; ib = ? } - -- record { ca = ? ; cb = ? ; na = ? ; nb = ? ; ia = ? ; ib = ? } where - -- cbn : CB n - -- cbn = lb n - -- + ... | no nisA | yes isB = record { ca = zero ; cb = suc zero ; cb≤n = ≤-refl ; ca≤cb = px≤x ; na = λ () ; nb = λ _ → Is.a isB } + ... | no nisA | no nisB = record { ca = zero ; cb = zero ; cb≤n = px≤x ; ca≤cb = ≤-refl ; na = λ () ; nb = λ () } + lb (suc n) with is-A (fun← cn (suc n)) | is-B (fun← cn (suc n)) + ... | yes isA | yes isB = record { ca = suc (CB.ca (lb n)) ; cb = suc (CB.cb (lb n)) ; cb≤n = s≤s (CB.cb≤n (lb n)) ; ca≤cb = s≤s (CB.ca≤cb (lb n)) + ; na = na ; nb = nb } where + na : {i : ℕ} → i < suc (CB.ca (lb n)) → A + na {i} i<a with <-∨ i<a + ... | case1 refl = Is.a isA + ... | case2 i<a = CB.na (lb n) i<a + nb : {i : ℕ} → i < suc (CB.cb (lb n)) → B + nb {i} i<a with <-∨ i<a + ... | case1 refl = Is.a isB + ... | case2 i<a = CB.nb (lb n) i<a + ... | yes isA | no nisB = ⊥-elim ( ¬isA∧isB _ isA nisB ) + ... | no nisA | yes isB = record { ca = CB.ca (lb n) ; cb = suc (CB.cb (lb n)) ; cb≤n = s≤s (CB.cb≤n (lb n)) ; ca≤cb = ≤-trans (CB.ca≤cb (lb n)) px≤x + ; na = CB.na (lb n) ; nb = nb } where + nb : {i : ℕ} → i < suc (CB.cb (lb n)) → B + nb {i} i<a with <-∨ i<a + ... | case1 refl = Is.a isB + ... | case2 i<a = CB.nb (lb n) i<a + ... | no nisA | no nisB = record { ca = CB.ca (lb n) ; cb = CB.cb (lb n) ; cb≤n = ≤-trans (CB.cb≤n (lb n)) px≤x ; ca≤cb = CB.ca≤cb (lb n) + ; na = CB.na (lb n) ; nb = CB.nb (lb n) } + + cbn : ℕ → ℕ + cbn n = fun→ cn (g (f (fun← an n))) cb< : (n : ℕ) → CB.cb (lb (cbn n)) < CB.cb (lb (cbn (suc n))) cb< = ? n<cbn : (n : ℕ) → n < CB.cb (lb (cbn n)) - n<cbn zero = ? + n<cbn zero with is-A (fun← cn zero) | is-B (fun← cn zero) | inspect lb zero + ... | yes isA | yes isB | record { eq = eq1 } = subst (λ k → 1 ≤ CB.cb (lb k)) lem02 lem01 where + lem01 : 1 ≤ CB.cb (lb 0) + lem01 = subst (λ k → 1 ≤ k ) (sym (cong CB.cb eq1)) ≤-refl + lem02 : 0 ≡ fun→ cn (g (f (fun← an 0))) + lem02 = ? + ... | yes isA | no nisB | record { eq = eq1 } = ⊥-elim ( ¬isA∧isB _ isA nisB ) + ... | no nisA | yes isB | record { eq = eq1 } = ? + ... | no nisA | no nisB | record { eq = eq1 } = ? n<cbn (suc n) = begin suc (suc n) ≤⟨ s≤s (n<cbn n) ⟩ suc (CB.cb (lb (cbn n))) ≤⟨ cb< n ⟩ @@ -562,9 +579,7 @@ bton : B → ℕ bton b = CB.cb (lb (fun→ cn (g b))) ntob : ℕ → B - ntob n = CB.nb (lb (fun→ cn (g (f (fun← an (suc n)))))) {n} (n<cbn n) - - + ntob n = CB.nb (lb (fun→ cn (g (f (fun← an n))))) (n<cbn n) bi-∧ : {A B C D : Set} → Bijection A B → Bijection C D → Bijection (A ∧ C) (B ∧ D) bi-∧ {A} {B} {C} {D} ab cd = record {