Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1440:a7d46b1c2a70
fix HODBijection (sorry)
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 04 Jul 2023 10:14:27 +0900 |
| parents | 900c98ffde05 |
| children | 1a9859a0b14d |
| files | src/ZProduct.agda src/cardinal.agda |
| diffstat | 2 files changed, 44 insertions(+), 94 deletions(-) [+] |
line wrap: on
line diff
--- a/src/ZProduct.agda Tue Jul 04 09:28:09 2023 +0900 +++ b/src/ZProduct.agda Tue Jul 04 10:14:27 2023 +0900 @@ -366,12 +366,12 @@ record HODBijection (A B : HOD ) : Set n where field - fun← : (x : Ordinal ) → odef A x → Ordinal - fun→ : (x : Ordinal ) → odef B x → Ordinal - funB : (x : Ordinal ) → ( lt : odef A x ) → odef B ( fun← x lt ) - funA : (x : Ordinal ) → ( lt : odef B x ) → odef A ( fun→ x lt ) - fiso← : (x : Ordinal ) → ( lt : odef B x ) → fun← ( fun→ x lt ) ( funA x lt ) ≡ x - fiso→ : (x : Ordinal ) → ( lt : odef A x ) → fun→ ( fun← x lt ) ( funB x lt ) ≡ x + fun← : (x : Ordinal ) → odef B x → Ordinal + fun→ : (x : Ordinal ) → odef A x → Ordinal + funB : (x : Ordinal ) → ( lt : odef A x ) → odef B ( fun→ x lt ) + funA : (x : Ordinal ) → ( lt : odef B x ) → odef A ( fun← x lt ) + fiso← : (x : Ordinal ) → ( lt : odef A x ) → fun← ( fun→ x lt ) ( funB x lt ) ≡ x + fiso→ : (x : Ordinal ) → ( lt : odef B x ) → fun→ ( fun← x lt ) ( funA x lt ) ≡ x hodbij-refl : { a b : HOD } → a ≡ b → HODBijection a b hodbij-refl {a} refl = record { @@ -416,12 +416,12 @@ ZFPsym1 : (A B : HOD) → HODBijection (ZFP A B) (ZFP (ZPI2 A B) (ZPI1 A B)) ZFPsym1 A B = record { - fun← = λ xy ab → & < * ( zπ2 ab) , * ( zπ1 ab) > - ; fun→ = λ xy ab → & < * ( zπ2 ab) , * ( zπ1 ab) > + fun→ = λ xy ab → & < * ( zπ2 ab) , * ( zπ1 ab) > + ; fun← = λ xy ab → & < * ( zπ2 ab) , * ( zπ1 ab) > ; funB = pj2 A B ; funA = pj1 A B - ; fiso← = λ xy ab → pj00 A B ab - ; fiso→ = λ xy ab → zp-iso ab + ; fiso→ = λ xy ab → pj00 A B ab + ; fiso← = λ xy ab → zp-iso ab } where pj10 : (A B : HOD) → {xy : Ordinal} → (ab : odef (ZFP (ZPI2 A B) (ZPI1 A B)) xy ) → & < * (zπ1 ab) , * (zπ2 ab) > ≡ & < * (zπ2 (pj1 A B xy ab)) , * (zπ1 (pj1 A B xy ab)) >
--- a/src/cardinal.agda Tue Jul 04 09:28:09 2023 +0900 +++ b/src/cardinal.agda Tue Jul 04 10:14:27 2023 +0900 @@ -44,23 +44,13 @@ -- record HODBijection (A B : HOD ) : Set n where -- field +-- fun→ : (x : Ordinal ) → odef B x → Ordinal -- fun← : (x : Ordinal ) → odef A x → Ordinal --- fun→ : (x : Ordinal ) → odef B x → Ordinal -- funB : (x : Ordinal ) → ( lt : odef A x ) → odef B ( fun← x lt ) -- funA : (x : Ordinal ) → ( lt : odef B x ) → odef A ( fun→ x lt ) +-- fiso→ : (x : Ordinal ) → ( lt : odef A x ) → fun→ ( fun← x lt ) ( funB x lt ) ≡ x -- fiso← : (x : Ordinal ) → ( lt : odef B x ) → fun← ( fun→ x lt ) ( funA x lt ) ≡ x --- fiso→ : (x : Ordinal ) → ( lt : odef A x ) → fun→ ( fun← x lt ) ( funB x lt ) ≡ x --- --- rrdbij-refl : { a b : HOD } → a ≡ b → HODBijection a b --- rrdbij-refl {a} refl = record { --- fun← = λ x _ → x --- ; fun→ = λ x _ → x --- ; funB = λ x lt → lt --- ; funA = λ x lt → lt --- ; fiso← = λ x lt → refl --- ; fiso→ = λ x lt → refl --- } - + open Injection open HODBijection @@ -115,19 +105,19 @@ bi-∪ : {A B C D : HOD } → (ab : HODBijection A B) → (cd : HODBijection C D ) → HODBijection (A ∪ C) (B ∪ D) bi-∪ {A} {B} {C} {D} ab cd = record { - fun← = fa - ; fun→ = fb + fun→ = fa + ; fun← = fb ; funB = fa-isb ; funA = fb-isa - ; fiso← = faiso - ; fiso→ = fbiso + ; fiso→ = faiso + ; fiso← = fbiso } where fa : (x : Ordinal) → odef (A ∪ C) x → Ordinal - fa x (case1 a) = fun← ab x a - fa x (case2 c) = fun← cd x c + fa x (case1 a) = fun→ ab x a + fa x (case2 c) = fun→ cd x c fb : (x : Ordinal) → odef (B ∪ D) x → Ordinal - fb x (case1 b) = fun→ ab x b - fb x (case2 d) = fun→ cd x d + fb x (case1 b) = fun← ab x b + fb x (case2 d) = fun← cd x d fa-isb : (x : Ordinal) (lt : odef (A ∪ C) x) → odef (B ∪ D) (fa x lt) fa-isb x (case1 a) = case1 (funB ab x a) fa-isb x (case2 c) = case2 (funB cd x c) @@ -135,11 +125,11 @@ fb-isa x (case1 b) = case1 (funA ab x b) fb-isa x (case2 d) = case2 (funA cd x d) faiso : (x : Ordinal) (lt : odef (B ∪ D) x) → fa (fb x lt) (fb-isa x lt) ≡ x - faiso x (case1 b) = fiso← ab x b - faiso x (case2 d) = fiso← cd x d + faiso x (case1 b) = fiso→ ab x b + faiso x (case2 d) = fiso→ cd x d fbiso : (x : Ordinal) (lt : odef (A ∪ C) x) → fb (fa x lt) (fa-isb x lt) ≡ x - fbiso x (case1 b) = fiso→ ab x b - fbiso x (case2 d) = fiso→ cd x d + fbiso x (case1 b) = fiso← ab x b + fbiso x (case2 d) = fiso← cd x d -- -- f : A → B OrdBijection A (Image A f) @@ -280,12 +270,12 @@ bi-UC : HODBijection UC fUC bi-UC = record { - fun← = λ x lt → fU1 x lt - ; fun→ = λ x lt → Uf1 x lt + fun→ = λ x lt → fU1 x lt + ; fun← = λ x lt → Uf1 x lt ; funB = λ x lt → record { y = _ ; ay = lt ; x=fy = refl } ; funA = λ x lt → UC∋Uf1 lt - ; fiso← = λ x lt → fU-iso1 lt - ; fiso→ = λ x lt → fU-iso0 lt + ; fiso→ = λ x lt → fU-iso1 lt + ; fiso← = λ x lt → fU-iso0 lt } b-FUC∋g⁻¹ : {x : Ordinal } → (lt : odef a-UC x )→ odef b-fUC (g⁻¹ (proj1 lt) (nimg (proj1 lt) (proj2 lt))) @@ -304,12 +294,12 @@ bi-fUC : HODBijection a-UC b-fUC bi-fUC = record { - fun← = λ x lt → g⁻¹ (proj1 lt) (nimg (proj1 lt) (proj2 lt)) - ; fun→ = λ x lt → fba x (proj1 lt) + fun→ = λ x lt → g⁻¹ (proj1 lt) (nimg (proj1 lt) (proj2 lt)) + ; fun← = λ x lt → fba x (proj1 lt) ; funB = λ x lt → b-FUC∋g⁻¹ lt ; funA = λ x lt → a-UC∋g lt - ; fiso← = λ x lt → fUC-iso1 lt - ; fiso→ = λ x lt → fUC-iso0 lt + ; fiso→ = λ x lt → fUC-iso1 lt + ; fiso← = λ x lt → fUC-iso0 lt } @@ -358,65 +348,25 @@ b : HODBijection (Power S) S b = subst₂ (λ j k → HODBijection j k) *iso *iso ( Bernstein f2 f1) - decS : (S : HOD) (x : Ordinal) → odef S x ∨ ( ¬ odef S x ) - decS S x = ODC.p∨¬p O (odef S x ) - - record T : Set n where - field - x : Ordinal - Sx : odef S x - - -- HODBijection (Power S) S → Bijection ( T → Bool ) T - -- - -- bt : Bijection (T → Bool) T - -- fun← : T → (T → Bool) - -- fun→ : (T → Bool) → T - - record TT ( isT : T → Bool ) (x : Ordinal) : Set n where - field - sx : odef S x - T=true : isT record { x = x ; Sx = sx } ≡ true - - sx→T : {x : Ordinal } → odef S x → T - sx→T {x} sx = record { x = x ; Sx = sx } - - tb : (T → Bool ) → Ordinal - tb fx = & record { od = record { def = λ x → TT fx x} ; odmax = & S ; <odmax = ? } - - TB→PS : (fx : T → Bool ) → odef (Power S) (tb fx) - TB→PS fx y txy with subst (λ k → odef k y ) *iso txy - ... | tt = TT.sx tt - - PS→TB : {x : Ordinal } → odef (Power S) x → T → Bool - PS→TB {x} psx t with decS (* x) (T.x t) - ... | case1 iss = true - ... | case2 niss = false - - s← : T → (T → Bool ) - s← t = PS→TB ( funA b (T.x t) (T.Sx t) ) - - s→ : (T → Bool) → T - s→ fx = record { x = fun← b (tb fx) (TB→PS fx) ; Sx = funB b (tb fx) (TB→PS fx) } - - -- we can prove bt here - -- but prove contradiction directly + is-S : (S : HOD) → (x : Ordinal ) → Bool + is-S S x with ODC.p∨¬p O (odef S x ) + ... | case1 _ = true + ... | case2 _ = false --- if t ∋ x then false else true --- diag : T → Bool diag : {x : Ordinal } → odef S x → Bool - diag {x} sx = not (s← (sx→T sx) (sx→T sx) ) + diag {x} sx = not (is-S (* (fun← b x ? )) x ) where + ca00 : odef (Power S) x + ca01 : odef (Power S) (fun← b x ? ) + ca01 = ? -- funA b x ? + ca00 z xz = ? - diagn1 : {x : Ordinal } (sx : odef S x ) → ¬ (fun→ b x sx ≡ x ) + diagn1 : {x : Ordinal } (sx : odef S x ) → ¬ (fun→ b x ? ≡ x ) diagn1 {x} sx dn = ¬t=f (diag sx ) ( begin not (diag sx ) - ≡⟨⟩ - not (not (s← (sx→T sx) (sx→T sx) ) ) - ≡⟨ cong (λ k → not k ) (sym ? ) ⟩ - not (s← (s→ (λ t → diag (T.Sx t)) ) (sx→T sx) ) - ≡⟨ cong (λ k → not ? ) dn ⟩ - not (s← (sx→T sx) (sx→T sx) ) - ≡⟨⟩ + ≡⟨ ? ⟩ diag sx ∎ ) where open ≡-Reasoning