Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 140:312e27aa3cb5
remove otrans again. start over
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 07 Jul 2019 23:02:47 +0900 |
| parents | 53077af367e9 |
| children | 21b2654985c4 |
| files | HOD.agda ordinal-definable.agda zf.agda |
| diffstat | 3 files changed, 21 insertions(+), 63 deletions(-) [+] |
line wrap: on
line diff
--- a/HOD.agda Sun Jul 07 22:23:02 2019 +0900 +++ b/HOD.agda Sun Jul 07 23:02:47 2019 +0900 @@ -16,7 +16,6 @@ record HOD {n : Level} : Set (suc n) where field def : (x : Ordinal {n} ) → Set n - otrans : {x : Ordinal {n} } → def x → { y : Ordinal {n} } → y o< x → def y open HOD open import Data.Unit @@ -49,9 +48,7 @@ -- Ordinal in HOD ( and ZFSet ) Ord : { n : Level } → ( a : Ordinal {n} ) → HOD {n} -Ord {n} a = record { def = λ y → y o< a ; otrans = lemma } where - lemma : {x : Ordinal} → x o< a → {y : Ordinal} → y o< x → y o< a - lemma {x} x<a {y} y<x = ordtrans {n} {y} {x} {a} y<x x<a +Ord {n} a = record { def = λ y → y o< a } od∅ : {n : Level} → HOD {n} od∅ {n} = Ord o∅ @@ -94,9 +91,7 @@ a c≤ b = (a ≡ b) ∨ ( b ∋ a ) cseq : {n : Level} → HOD {n} → HOD {n} -cseq x = record { def = λ y → def x (osuc y) ; otrans = lemma } where - lemma : {ox : Ordinal} → def x (osuc ox) → { oy : Ordinal}→ oy o< ox → def x (osuc oy) - lemma {ox} oox<Ox {oy} oy<ox = otrans x oox<Ox (osucc oy<ox ) +cseq x = record { def = λ y → def x (osuc y) } where def-subst : {n : Level } {Z : HOD {n}} {X : Ordinal {n} }{z : HOD {n}} {x : Ordinal {n} }→ def Z X → Z ≡ z → X ≡ x → def z x def-subst df refl refl = df @@ -145,10 +140,6 @@ ... | t with t (case2 (s< s<refl ) ) c3 lx (OSuc .lx x₁) d not | t | () -transitive : {n : Level } { z y x : HOD {suc n} } → z ∋ y → y ∋ x → z ∋ x -transitive {n} {z} {y} {x} z∋y x∋y with ordtrans ( c<→o< {suc n} {x} {y} x∋y ) ( c<→o< {suc n} {y} {z} z∋y ) -... | t = otrans z z∋y (c<→o< {suc n} {x} {y} x∋y ) - ∅5 : {n : Level} → { x : Ordinal {n} } → ¬ ( x ≡ o∅ {n} ) → o∅ {n} o< x ∅5 {n} {record { lv = Zero ; ord = (Φ .0) }} not = ⊥-elim (not refl) ∅5 {n} {record { lv = Zero ; ord = (OSuc .0 ord) }} not = case2 Φ< @@ -206,7 +197,7 @@ o≡→¬c< : {n : Level} → { x y : HOD {n} } → (od→ord x ) ≡ ( od→ord y) → ¬ x c< y o≡→¬c< {n} {x} {y} oeq lt = o<¬≡ (orefl oeq ) (c<→o< lt) -∅0 : {n : Level} → record { def = λ x → Lift n ⊥ ; otrans = λ () } == od∅ {n} +∅0 : {n : Level} → record { def = λ x → Lift n ⊥ } == od∅ {n} eq→ ∅0 {w} (lift ()) eq← ∅0 {w} (case1 ()) eq← ∅0 {w} (case2 ()) @@ -236,9 +227,7 @@ -- Power Set of X ( or constructible by λ y → def X (od→ord y ) ZFSubset : {n : Level} → (A x : HOD {suc n} ) → HOD {suc n} -ZFSubset A x = record { def = λ y → def A y ∧ def x y ; otrans = lemma } where - lemma : {z : Ordinal} → def A z ∧ def x z → {y : Ordinal} → y o< z → def A y ∧ def x y - lemma {z} d {y} y<z = record { proj1 = otrans A (proj1 d) y<z ; proj2 = otrans x (proj2 d) y<z } +ZFSubset A x = record { def = λ y → def A y ∧ def x y } where Def : {n : Level} → (A : HOD {suc n}) → HOD {suc n} Def {n} A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) ) @@ -296,12 +285,7 @@ ; isZF = isZF } where Select : (X : HOD {suc n} ) → ((x : HOD {suc n} ) → Set (suc n) ) → HOD {suc n} - Select X ψ = record { def = λ x → ((y : Ordinal {suc n} ) → X ∋ ord→od y → ψ (ord→od y)) ∧ (X ∋ ord→od x ) ; otrans = lemma } where - lemma : {x : Ordinal} → ((y : Ordinal) → X ∋ ord→od y → ψ (ord→od y)) ∧ (X ∋ ord→od x) → - {y : Ordinal} → y o< x → ((y₁ : Ordinal) → X ∋ ord→od y₁ → ψ (ord→od y₁)) ∧ (X ∋ ord→od y) - lemma {x} select {y} y<x = record { proj1 = proj1 select ; proj2 = y<X } where - y<X : X ∋ ord→od y - y<X = otrans X (proj2 select) (o<-subst y<x (sym diso) (sym diso) ) + Select X ψ = record { def = λ x → ( def X x ∧ ψ ( ord→od x )) } Replace : HOD {suc n} → (HOD {suc n} → HOD {suc n} ) → HOD {suc n} Replace X ψ = Select ( Ord (sup-o ( λ x → od→ord (ψ (ord→od x ))))) ( λ x → ¬ (∀ (y : Ordinal ) → ¬ ( def X y ∧ ( x == ψ (Ord y) )))) _,_ : HOD {suc n} → HOD {suc n} → HOD {suc n} @@ -369,8 +353,7 @@ ... | 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 : HOD {suc n}} → t ∋ x → Ord (od→ord t) ∋ x Ltx {n} {x} {t} lt = c<→o< lt - ... | case2 lt = otrans (Ord a) (proj1 (lemma1 lt) ) - (c<→o< {suc n} {x} {Ord (od→ord t)} (Ltx t∋x) ) where + ... | case2 lt = {!!} where sp = sup-x (λ x → od→ord ( ZFSubset (Ord a) (ord→od x))) minsup : HOD minsup = ZFSubset (Ord a) ( ord→od ( sup-x (λ x → od→ord ( ZFSubset (Ord a) (ord→od x))))) @@ -427,7 +410,7 @@ 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 = otrans X (proj1 xx) c + union→ X z u xx | tri> ¬a ¬b c = {!!} union← : (X z : HOD) (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 @@ -435,35 +418,12 @@ -- ψiso : {ψ : HOD {suc n} → Set (suc n)} {x y : HOD {suc n}} → ψ x → x ≡ y → ψ y -- ψiso {ψ} t refl = t - selection : {X : HOD } {ψ : (x : HOD ) → Set (suc n)} {y : HOD} → (((y₁ : HOD) → X ∋ y₁ → ψ y₁) ∧ (X ∋ y)) ⇔ (Select X ψ ∋ y) - selection {X} {ψ} {y} = record { proj1 = λ s → record { - proj1 = λ y1 y1<X → proj1 s (ord→od y1) y1<X ; proj2 = subst (λ k → def X k ) (sym diso) (proj2 s) } - ; proj2 = λ s → record { proj1 = λ y1 dy1 → - subst (λ k → ψ k ) oiso ((proj1 s) (od→ord y1) (def-subst {suc n} {_} {_} {X} {_} dy1 refl (sym diso ))) - ; proj2 = def-subst {suc n} {_} {_} {X} {od→ord y} (proj2 s ) refl diso } } where - -- ψ< : {ψ : HOD {suc n} → HOD {suc n}} {x y y' : HOD {suc n}} → ψ y ∋ x → ψ y' == x - -- ψ< = {!!} + selection : {ψ : HOD → Set (suc n)} {X y : HOD} → ((X ∋ y) ∧ ψ y) ⇔ (Select X ψ ∋ y) + selection {X} {ψ} {y} = {!!} replacement← : {ψ : HOD → HOD} (X x : HOD) → X ∋ x → Replace X ψ ∋ ψ x - replacement← {ψ} X x lt = record { proj1 = lemma - ; proj2 = sup-o∋ψx - } - where - sup-o∋ψx : Ord (sup-o (λ x₁ → od→ord (ψ (ord→od x₁)))) ∋ ord→od (od→ord (ψ x)) - sup-o∋ψx = def-subst {suc n} {_} {_} {Ord (sup-o (λ x₁ → od→ord (ψ (ord→od x₁))))} { od→ord (ord→od (od→ord (ψ x)))} - (sup-c< ψ {x}) refl (sym diso) - lemma : (y : Ordinal) → Ord (sup-o (λ x₁ → od→ord (ψ (ord→od x₁)))) ∋ ord→od y → - ¬ ((y₁ : Ordinal) → ¬ def X y₁ ∧ (ord→od y == ψ (Ord y₁))) - lemma y lt1 not = not (minα (od→ord x) (sup-x ( λ w → od→ord (ψ (ord→od w ))))) (record { - proj1 = ? - ; proj2 = subst₂ (λ k j → k == j ) refl oiso (o≡→== {!!}) } ) where - lemma1 : y o< osuc ( od→ord (ψ (ord→od ( sup-x ( λ w → od→ord (ψ (ord→od w ))) )))) - lemma1 = o<-subst (sup-lb lt1) diso refl - lemma2 : ord→od y ≡ ψ (ord→od ( sup-x ( λ w → od→ord (ψ (ord→od w ))))) - lemma2 with osuc-≡< lemma1 - lemma2 | case1 refl = subst (λ k → ord→od y ≡ k ) oiso refl - lemma2 | case2 t = {!!} + replacement← {ψ} X x lt = {!!} replacement→ : {ψ : HOD → HOD} (X x : HOD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : HOD) → ¬ (x == ψ y)) - replacement→ {ψ} X x lt = contra-position lemma (proj1 lt (od→ord x) (proj2 lt)) where + replacement→ {ψ} X x lt = contra-position lemma {!!} where lemma : ( (y : HOD) → ¬ (x == ψ y)) → ( (y : Ordinal) → ¬ def X y ∧ (ord→od (od→ord x) == ψ (Ord y)) ) lemma not y not2 = not (ord→od y) (subst₂ ( λ k j → k == j ) oiso (cong (λ k → ψ k ) Ord-ord ) (proj2 not2 )) @@ -476,7 +436,7 @@ 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 = proj1 s x₁ (proj2 s) + lemma3 = {!!} 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-definable.agda Sun Jul 07 22:23:02 2019 +0900 +++ b/ordinal-definable.agda Sun Jul 07 23:02:47 2019 +0900 @@ -311,7 +311,7 @@ ; isZF = isZF } where Select : OD {suc n} → (OD {suc n} → Set (suc n) ) → OD {suc n} - Select X ψ = record { def = λ x → ((y : Ordinal {suc n}) → def X y → ψ ( ord→od y )) ∧ def X x } + Select X ψ = record { def = λ x → ( def X x ∧ ψ ( ord→od x )) } _,_ : OD {suc n} → OD {suc n} → OD {suc n} x , y = record { def = λ z → z o< (omax (od→ord x) (od→ord y)) } _∩_ : ( A B : OD {suc n} ) → OD @@ -348,7 +348,7 @@ ; regularity = regularity ; infinity∅ = infinity∅ ; infinity = λ _ → infinity - ; selection = λ {X} {ψ} {y} → selection {ψ} {X} {y} + ; selection = λ {ψ} {X} {y} → selection {ψ} {X} {y} ; replacement← = replacement← ; replacement→ = replacement→ } where @@ -408,19 +408,17 @@ union← X z X∋z = record { proj1 = def-subst {suc n} {_} {_} {X} {od→ord (csuc z )} (o<→c< X∋z) oiso (sym diso) ; proj2 = union-lemma-u X∋z } ψiso : {ψ : OD {suc n} → Set (suc n)} {x y : OD {suc n}} → ψ x → x ≡ y → ψ y ψiso {ψ} t refl = t - selection : {ψ : OD → Set (suc n)} {X y : OD} → (((y : OD) → X ∋ y → ψ y) ∧ (X ∋ y)) ⇔ (Select X ψ ∋ y) + selection : {ψ : OD → Set (suc n)} {X y : OD} → ((X ∋ y) ∧ ψ y) ⇔ (Select X ψ ∋ y) selection {ψ} {X} {y} = record { - proj1 = λ cond → record { proj1 = λ y X>y → proj1 cond (ord→od y) (subst (λ k → def X k ) (sym diso) X>y) ; proj2 = proj2 cond } - ; proj2 = λ select → record { proj1 = λ y X>y → subst (λ k → ψ k ) oiso (proj1 select (od→ord y) X>y ) ; proj2 = proj2 select } - } where - lemma : (cond : ((y : OD) → X ∋ y → ψ y ) ∧ (X ∋ y) ) → ψ y - lemma cond = (proj1 cond) y (proj2 cond) + proj1 = λ cond → record { proj1 = proj1 cond ; proj2 = ψiso {ψ} (proj2 cond) (sym oiso) } + ; proj2 = λ select → record { proj1 = proj1 select ; proj2 = ψiso {ψ} (proj2 select) oiso } + } replacement← : {ψ : OD → OD} (X x : OD) → X ∋ x → Replace X ψ ∋ ψ x replacement← {ψ} X x lt = record { proj1 = sup-c< ψ {x} ; proj2 = lemma } where lemma : def (in-codomain X ψ) (od→ord (ψ x)) lemma not = ⊥-elim ( not ( od→ord x ) (record { proj1 = lt ; proj2 = cong (λ k → od→ord (ψ k)) (sym oiso)} ) ) replacement→ : {ψ : OD → OD} (X x : OD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : OD) → ¬ (x == ψ y)) - replacement→ {ψ} X x lt not = ⊥-elim ( not {!!} (ord→== {!!} ) ) + replacement→ {ψ} X x lt not = ⊥-elim ( not {!!} (ord→== {!!}) ) ∅-iso : {x : OD} → ¬ (x == od∅) → ¬ ((ord→od (od→ord x)) == od∅) ∅-iso {x} neq = subst (λ k → ¬ k) (=-iso {n} ) neq minimul : (x : OD {suc n} ) → ¬ (x == od∅ )→ OD {suc n} @@ -433,7 +431,7 @@ lemma (case1 ()) lemma (case2 ()) reg : {y : Ordinal} → def (Select (minimul x not) (λ x₂ → (minimul x not ∋ x₂) ∧ (x ∋ x₂))) y → def od∅ y - reg {y} t with proj1 t y (proj2 t) + reg {y} t with {!!} ... | x∈∅ = o<-subst (proj1 x∈∅) diso refl extensionality : {A B : OD {suc n}} → ((z : OD) → (A ∋ z) ⇔ (B ∋ z)) → A == B eq→ (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {A} {B} (sym diso) (proj1 (eq (ord→od x))) d
--- a/zf.agda Sun Jul 07 22:23:02 2019 +0900 +++ b/zf.agda Sun Jul 07 23:02:47 2019 +0900 @@ -75,7 +75,7 @@ -- infinity : ∃ A ( ∅ ∈ A ∧ ∀ x ∈ A ( x ∪ { x } ∈ A ) ) infinity∅ : ∅ ∈ infinite infinity : ∀( X x : ZFSet ) → x ∈ infinite → ( x ∪ ｛ x ｝) ∈ infinite - selection : ∀ { X : ZFSet } → { ψ : (x : ZFSet ) → Set m } → ∀ { y : ZFSet } → (((y : ZFSet) → y ∈ X → ψ y ) ∧ ( y ∈ X ) ) ⇔ (y ∈ Select X ψ ) + selection : { ψ : ZFSet → Set m } → ∀ { X y : ZFSet } → ( ( y ∈ X ) ∧ ψ y ) ⇔ (y ∈ Select X ψ ) -- replacement : ∀ x ∀ y ∀ z ( ( ψ ( x , y ) ∧ ψ ( x , z ) ) → y = z ) → ∀ X ∃ A ∀ y ( y ∈ A ↔ ∃ x ∈ X ψ ( x , y ) ) replacement← : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet ) → x ∈ X → ψ x ∈ Replace X ψ replacement→ : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet ) → ( lt : x ∈ Replace X ψ ) → ¬ ( ∀ (y : ZFSet) → ¬ ( x ≈ ψ y ) )