Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 142:c30bc9f5bd0d
Power Set
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 08 Jul 2019 12:13:19 +0900 |
| parents | 21b2654985c4 |
| children | 21b9e78e9359 |
| files | HOD.agda ordinal.agda |
| diffstat | 2 files changed, 55 insertions(+), 13 deletions(-) [+] |
line wrap: on
line diff
--- a/HOD.agda Mon Jul 08 00:20:30 2019 +0900 +++ b/HOD.agda Mon Jul 08 12:13:19 2019 +0900 @@ -81,6 +81,9 @@ Ord-ord : {n : Level } {ox : Ordinal {suc n}} → Ord ox ≡ ord→od ox Ord-ord {n} {px} = trans (sym oiso) (cong ( λ k → ord→od k ) (sym ord-Ord)) +Ord-ord-≡ : {n : Level } {t : OD {suc n}} → Ord (od→ord t) ≡ t +Ord-ord-≡ {n} {t} = subst₂ (λ k j → k ≡ j ) oiso oiso (cong (λ k → ord→od k) (sym ord-Ord)) + _∋_ : { n : Level } → ( a x : OD {n} ) → Set n _∋_ {n} a x = def a ( od→ord x ) @@ -122,6 +125,8 @@ Ord==→≡ {n} {x} {y} eq | tri≈ ¬a b ¬c = b Ord==→≡ {n} {x} {y} eq | tri> ¬a ¬b c = ⊥-elim ( o<→o> (eq-sym eq) c ) +otrans : {n : Level} {a x : Ordinal {n} } → def (Ord a) x → { y : Ordinal {n} } → y o< x → def (Ord a) y +otrans {n} {a} {x} x<a {y} y<x = ordtrans y<x x<a ∅3 : {n : Level} → { x : Ordinal {n}} → ( ∀(y : Ordinal {n}) → ¬ (y o< x ) ) → x ≡ o∅ {n} ∅3 {n} {x} = TransFinite {n} c2 c3 x where @@ -302,7 +307,7 @@ _⊆_ : ( A B : ZFSet ) → ∀{ x : ZFSet } → Set (suc n) _⊆_ A B {x} = A ∋ x → B ∋ x _∩_ : ( A B : ZFSet ) → ZFSet - A ∩ B = Select (A , B) ( λ x → ( A ∋ x ) ∧ (B ∋ x) ) + A ∩ B = record { def = λ x → def A x ∧ def B x } -- Select (A , B) ( λ x → ( A ∋ x ) ∧ (B ∋ x) ) Power : OD {suc n} → OD {suc n} Power A = Replace (Def (Ord (od→ord A))) ( λ x → A ∩ x ) -- _∪_ : ( A B : ZFSet ) → ZFSet @@ -351,12 +356,17 @@ -- POrd : {a : Ordinal } {t : OD} → Def (Ord a) ∋ t → Def (Ord a) ∋ Ord (od→ord t) POrd {a} {t} P∋t = o<→c< P∋t + ∩-≡ : { a b : OD {suc n} } → ({x : OD {suc n} } → (a ∋ x → b ∋ x)) → a == ( b ∩ a ) + ∩-≡ {a} {b} inc = record { + eq→ = λ {x} x<a → record { proj2 = x<a ; + proj1 = def-subst {suc n} {_} {_} {b} {x} (inc (def-subst {suc n} {_} {_} {a} {_} x<a refl (sym diso) )) refl diso } ; + eq← = λ {x} x<a∩b → proj2 x<a∩b } ord-power→ : (a : Ordinal ) ( t : OD) → Def (Ord a) ∋ t → {x : OD} → t ∋ x → Ord a ∋ x ord-power→ a t P∋t {x} t∋x with osuc-≡< (sup-lb (POrd P∋t)) ... | case1 eq = proj1 (def-subst (Ltx t∋x) (sym (subst₂ (λ j k → j ≡ k ) oiso oiso ( cong (λ k → ord→od k) (sym eq) ))) refl ) where Ltx : {n : Level} → {x t : OD {suc n}} → t ∋ x → Ord (od→ord t) ∋ x Ltx {n} {x} {t} lt = c<→o< lt - ... | case2 lt = {!!} where + ... | case2 lt = lemma3 where sp = sup-x (λ x → od→ord ( ZFSubset (Ord a) (ord→od x))) minsup : OD minsup = ZFSubset (Ord a) ( ord→od ( sup-x (λ x → od→ord ( ZFSubset (Ord a) (ord→od x))))) @@ -379,6 +389,8 @@ ≡⟨ sym eq1 ⟩ minsup ∎ + lemma3 : od→ord x o< a + lemma3 = otrans (proj1 (lemma1 lt) ) (c<→o< {suc n} {x} {Ord (od→ord t)} (Ltx t∋x) ) -- -- we have t ∋ x → A ∋ x means t is a subset of A, that is ZFSubset A t == t -- Power A is a sup of ZFSubset A t, so Power A ∋ t @@ -397,15 +409,6 @@ lemma : od→ord (ZFSubset (Ord a) (ord→od (od→ord t)) ) o< sup-o (λ x → od→ord (ZFSubset (Ord a) (ord→od x))) lemma = sup-o< - -- Power A = Replace (Def (Ord (od→ord A))) ( λ x → A ∩ x ) - power→ : ( A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → A ∋ x - power→ = {!!} - power← : (A t : OD) → ({x : OD} → (t ∋ x → A ∋ x)) → Power A ∋ t - power← A t t→A = {!!} where - a = od→ord A - ψ : OD → OD - ψ y = Def (Ord a) ∩ y - union-u : {X z : OD {suc n}} → (U>z : Union X ∋ z ) → OD {suc n} union-u {X} {z} U>z = Ord ( osuc ( od→ord z ) ) union→ : (X z u : OD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z @@ -413,7 +416,8 @@ union→ X z u xx | tri< a ¬b ¬c with osuc-< a (c<→o< (proj2 xx)) union→ X z u xx | tri< a ¬b ¬c | () union→ X z u xx | tri≈ ¬a b ¬c = def-subst {suc n} {_} {_} {X} {osuc (od→ord z)} (proj1 xx) refl b - union→ X z u xx | tri> ¬a ¬b c = {!!} + union→ X z u xx | tri> ¬a ¬b c = {!!} --- osuc ( od→ord z )) o< od→ord u o< od→ord X + union← : (X z : OD) (X∋z : Union X ∋ z) → (X ∋ union-u {X} {z} X∋z ) ∧ (union-u {X} {z} X∋z ∋ z ) union← X z X∋z = record { proj1 = lemma ; proj2 = <-osuc } where lemma : X ∋ union-u {X} {z} X∋z @@ -441,6 +445,34 @@ lemma : ( (y : OD) → ¬ (x == ψ y)) → ( (y : Ordinal) → ¬ def X y ∧ (ord→od (od→ord x) == ψ (Ord y)) ) lemma not y not2 = not (Ord y) (subst (λ k → k == ψ (Ord y)) oiso ( proj2 not2 )) + -- Power A = Replace (Def (Ord (od→ord A))) ( λ y → A ∩ y ) + power→ : ( A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → A ∋ x + power→ A t P∋t {x} t∋x = TransFiniteExists {suc n} {λ y → (t == (A ∩ ord→od y))} + lemma4 lemma5 where + a = od→ord A + lemma2 : ¬ ( (y : OD) → ¬ (t == (A ∩ y))) + lemma2 = replacement→ (Def (Ord (od→ord A))) t P∋t + lemma3 : (y : OD) → t == ( A ∩ y ) → A ∋ x + lemma3 y eq = proj1 (eq→ eq t∋x) + lemma4 : ¬ ((y : Ordinal) → ¬ (t == (A ∩ ord→od y))) + lemma4 not = lemma2 ( λ y not1 → not (od→ord y) (subst (λ k → t == ( A ∩ k )) (sym oiso) not1 )) + lemma5 : {y : Ordinal} → t == (A ∩ ord→od y) → def A (od→ord x) + lemma5 {y} eq = lemma3 (ord→od y) eq + power← : (A t : OD) → ({x : OD} → (t ∋ x → A ∋ x)) → Power A ∋ t + power← A t t→A = record { proj1 = lemma1 ; proj2 = lemma2 } where + a = od→ord A + lemma0 : {x : OD} → t ∋ x → Ord a ∋ x + lemma0 {x} t∋x = c<→o< (t→A t∋x) + lemma3 : Def (Ord a) ∋ t + lemma3 = ord-power← a t lemma0 + lemma1 : od→ord t o< sup-o (λ x → od→ord (A ∩ ord→od x)) + lemma1 with sup-o< {suc n} {λ x → od→ord (A ∩ ord→od x)} {{!!}} + ... | lt = {!!} + lemma2 : def (in-codomain (Def (Ord (od→ord A))) (_∩_ A)) (od→ord t) + lemma2 not = ⊥-elim ( not (od→ord t) (record { proj1 = lemma3 ; proj2 = lemma4 }) ) where + lemma4 : od→ord t ≡ od→ord (A ∩ Ord (od→ord t)) + lemma4 = cong ( λ k → od→ord k ) ( ===-≡ (subst (λ k → t == (A ∩ k)) (sym Ord-ord-≡) (∩-≡ t→A ) )) + ∅-iso : {x : OD} → ¬ (x == od∅) → ¬ ((ord→od (od→ord x)) == od∅) ∅-iso {x} neq = subst (λ k → ¬ k) (=-iso {n} ) neq regularity : (x : OD) (not : ¬ (x == od∅)) → @@ -450,7 +482,8 @@ lemma1 : {x₁ : Ordinal} → def (Select (minimul x not) (λ x₂ → (minimul x not ∋ x₂) ∧ (x ∋ x₂))) x₁ → def od∅ x₁ lemma1 {x₁} s = ⊥-elim ( minimul-1 x not (ord→od x₁) lemma3 ) where lemma3 : def (minimul x not) (od→ord (ord→od x₁)) ∧ def x (od→ord (ord→od x₁)) - lemma3 = {!!} + lemma3 = record { proj1 = def-subst {suc n} {_} {_} {minimul x not} {_} (proj1 s) refl (sym diso) + ; proj2 = proj2 (proj2 s) } lemma2 : {x₁ : Ordinal} → def od∅ x₁ → def (Select (minimul x not) (λ x₂ → (minimul x not ∋ x₂) ∧ (x ∋ x₂))) x₁ lemma2 {y} d = ⊥-elim (empty (ord→od y) (def-subst {suc n} {_} {_} {od∅} {od→ord (ord→od y)} d refl (sym diso) ))
--- a/ordinal.agda Mon Jul 08 00:20:30 2019 +0900 +++ b/ordinal.agda Mon Jul 08 12:13:19 2019 +0900 @@ -313,3 +313,12 @@ TransFinite caseΦ caseOSuc record { lv = lx ; ord = (OSuc lx ox) } = caseOSuc lx ox (TransFinite caseΦ caseOSuc record { lv = lx ; ord = ox }) +-- (¬ (∀ y → ¬ ( ψ y ))) → (ψ y → p ) → p +TransFiniteExists : {n : Level} → { ψ : Ordinal {n} → Set n } + → (exists : ¬ (∀ y → ¬ ( ψ y ) )) + → {p : Set n} ( P : { y : Ordinal {n} } → ψ y → p ) + → p +TransFiniteExists {n} {ψ} exists {p} P = ⊥-elim ( exists lemma ) where + lemma : (y : Ordinal {n} ) → ¬ ψ y + lemma y ψy = ( TransFinite {n} {{!!}} {!!} {!!} y ) ψy +