Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 147:c848550c8b39
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 08 Jul 2019 19:35:23 +0900 |
| parents | 2eafa89733ed |
| children | 6e767ad3edc2 |
| files | HOD.agda ordinal.agda |
| diffstat | 2 files changed, 21 insertions(+), 49 deletions(-) [+] |
line wrap: on
line diff
--- a/HOD.agda Mon Jul 08 18:26:33 2019 +0900 +++ b/HOD.agda Mon Jul 08 19:35:23 2019 +0900 @@ -60,7 +60,6 @@ c<→o< : {n : Level} {x y : OD {n} } → def y ( od→ord x ) → od→ord x o< od→ord y oiso : {n : Level} {x : OD {n}} → ord→od ( od→ord x ) ≡ x diso : {n : Level} {x : Ordinal {n}} → od→ord ( ord→od x ) ≡ x - ord-Ord :{n : Level} {x : Ordinal {n}} → x ≡ od→ord (Ord x) ==→o≡ : {n : Level} → { x y : OD {suc n} } → (x == y) → x ≡ y -- next assumption causes ∀ x ∋ ∅ . It menas only an ordinal becomes a set -- o<→c< : {n : Level} {x y : Ordinal {n} } → x o< y → def (ord→od y) x @@ -78,12 +77,6 @@ -- we should prove this in agda, but simply put here ===-≡ : {n : Level} { x y : OD {suc n}} → x == y → x ≡ y -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 ) @@ -99,12 +92,6 @@ def-subst : {n : Level } {Z : OD {n}} {X : Ordinal {n} }{z : OD {n}} {x : Ordinal {n} }→ def Z X → Z ≡ z → X ≡ x → def z x def-subst df refl refl = df -o<→c< : {n : Level} {x y : Ordinal {n} } → x o< y → Ord y ∋ Ord x -o<→c< {n} {x} {y} lt = subst ( λ k → k o< y ) ord-Ord lt - -o<→c<' : {n : Level} {x y : OD {suc n} } → od→ord x o< od→ord y → y ∋ x -o<→c<' {n} {x} {y} lt = def-subst {suc n} {Ord (od→ord y)} {od→ord x} {y} {od→ord x} lt Ord-ord-≡ refl - sup-od : {n : Level } → ( OD {n} → OD {n}) → OD {n} sup-od ψ = Ord ( sup-o ( λ x → od→ord (ψ (ord→od x ))) ) @@ -114,20 +101,6 @@ lemma : od→ord (ψ (ord→od (od→ord x))) o< sup-o (λ x → od→ord (ψ (ord→od x))) lemma = subst₂ (λ j k → j o< k ) refl diso (o<-subst sup-o< refl (sym diso) ) -o<→o> : {n : Level} → { x y : Ordinal {n} } → (Ord x == Ord y) → x o< y → ⊥ -o<→o> {n} {x} {y} record { eq→ = xy ; eq← = yx } (case1 lt) with o<-subst (yx (case1 lt)) ord-Ord refl -... | oyx with o<¬≡ refl (c<→o< {n} {Ord x} oyx ) -... | () -o<→o> {n} {x} {y} record { eq→ = xy ; eq← = yx } (case2 lt) with o<-subst (yx (case2 lt)) ord-Ord refl -... | oyx with o<¬≡ refl (c<→o< {n} {Ord x} oyx ) -... | () - -Ord==→≡ : {n : Level} { x y : Ordinal {suc n}} → Ord x == Ord y → x ≡ y -Ord==→≡ {n} {x} {y} eq with trio< x y -Ord==→≡ {n} {x} {y} eq | tri< a ¬b ¬c = ⊥-elim ( o<→o> eq a ) -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 @@ -194,8 +167,7 @@ o∅≡od∅ {n} with trio< {n} (o∅ {suc n}) (od→ord (od∅ {suc n} )) o∅≡od∅ {n} | tri< a ¬b ¬c = ⊥-elim (lemma a) where lemma : o∅ {suc n } o< (od→ord (od∅ {suc n} )) → ⊥ - lemma lt with o<→c< lt - lemma lt | t = o<¬≡ refl t + lemma lt = {!!} o∅≡od∅ {n} | tri≈ ¬a b ¬c = trans (cong (λ k → ord→od k ) b ) oiso o∅≡od∅ {n} | tri> ¬a ¬b c = ⊥-elim (¬x<0 c) @@ -267,14 +239,6 @@ L {n} record { lv = (Suc lx) ; ord = (Φ (Suc lx)) } = -- Union ( L α ) cseq ( Ord (od→ord (L {n} (record { lv = lx ; ord = Φ lx })))) -L00 : {n : Level} → (ox : Ordinal {suc n}) → ox o< sup-o ( λ x → od→ord ( ZFSubset (Ord ox) (ord→od x ))) -L00 {n} ox = o<-subst {suc n} {_} {_} {ox} {sup-o ( λ x → od→ord ( ZFSubset (Ord ox) (ord→od x )))} - (sup-o< {suc n} {λ x → od→ord ( ZFSubset (Ord ox) (ord→od x ))} {ox} ) (lemma0 ox) refl where - lemma1 : {n : Level } {ox z : Ordinal {suc n}} → ( def (Ord ox) z ∧ def (ord→od ox) z ) ⇔ def ( Ord ox ) z - lemma1 {n} {ox} {z} = record { proj1 = proj1 ; proj2 = λ t → record { proj1 = t ; proj2 = subst (λ k → def k z ) Ord-ord t }} - lemma0 : {n : Level} → (ox : Ordinal {suc n}) → od→ord (ZFSubset (Ord ox) (ord→od ox)) ≡ ox - lemma0 {n} ox = trans (cong (λ k → od→ord k) (===-≡ (⇔→== lemma1) )) (sym ord-Ord) - -- L0 : {n : Level} → (α : Ordinal {suc n}) → α o< β → L (osuc α) ∋ L α -- L1 : {n : Level} → (α β : Ordinal {suc n}) → α o< β → ∀ (x : OD {suc n}) → L α ∋ x → L β ∋ x @@ -357,7 +321,7 @@ 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 = def-subst lemma1 (sym lemma0) diso where lemma0 : X ≡ Ord (od→ord X) - lemma0 = sym Ord-ord-≡ + lemma0 = sym {!!} lemma : osuc (od→ord z) o< od→ord X lemma = ordtrans c ( c<→o< ( proj1 xx ) ) lemma1 : Ord ( od→ord X) ∋ ord→od (osuc (od→ord z) ) @@ -365,7 +329,7 @@ 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 UX∋z = record { proj1 = lemma ; proj2 = <-osuc } where lemma : X ∋ union-u {X} {z} UX∋z - lemma = def-subst {suc n} {_} {_} {X} {od→ord (Ord (osuc ( od→ord z )))} UX∋z refl ord-Ord + lemma = def-subst {suc n} {_} {_} {X} {od→ord (Ord (osuc ( od→ord z )))} UX∋z refl {!!} ψiso : {ψ : OD {suc n} → Set (suc n)} {x y : OD {suc n}} → ψ x → x ≡ y → ψ y ψiso {ψ} t refl = t @@ -378,7 +342,7 @@ 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 (subst (λ k → Ord (od→ord x) ≡ k) oiso (Ord-ord) )) } )) + (sym (subst (λ k → Ord (od→ord x) ≡ k) oiso {!!} )) } )) replacement→ : {ψ : OD → OD} (X x : OD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : OD) → ¬ (x == ψ y)) replacement→ {ψ} X x lt = contra-position lemma (lemma2 (proj2 lt)) where lemma2 : ¬ ((y : Ordinal) → ¬ def X y ∧ ((od→ord x) ≡ od→ord (ψ (Ord y)))) @@ -402,7 +366,7 @@ -- In case of later, ZFSubset A ∋ t and t ∋ x implies A ∋ x by transitivity -- 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 + POrd {a} {t} 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 ; @@ -422,14 +386,14 @@ -- lemma1 hold because minsup is Ord (minα a sp) lemma1 : od→ord (Ord (od→ord t)) o< od→ord minsup → minsup ∋ Ord (od→ord t) lemma1 lt with OrdSubset a ( sup-x (λ x → od→ord ( ZFSubset (Ord a) (ord→od x)))) - ... | eq with subst ( λ k → ZFSubset (Ord a) k ≡ Ord (minα a sp)) Ord-ord eq - ... | eq1 = def-subst {suc n} {_} {_} {minsup} {od→ord (Ord (od→ord t))} (o<→c< lt) lemma2 (sym ord-Ord) where + ... | eq with subst ( λ k → ZFSubset (Ord a) k ≡ Ord (minα a sp)) {!!} eq + ... | eq1 = def-subst {suc n} {_} {_} {minsup} {od→ord (Ord (od→ord t))} {!!} lemma2 {!!} where lemma2 : Ord (od→ord (ZFSubset (Ord a) (ord→od sp))) ≡ minsup lemma2 = let open ≡-Reasoning in begin Ord (od→ord (ZFSubset (Ord a) (ord→od sp))) ≡⟨ cong (λ k → Ord (od→ord k)) eq1 ⟩ Ord (od→ord (Ord (minα a sp))) - ≡⟨ cong (λ k → Ord (od→ord k)) Ord-ord ⟩ + ≡⟨ cong (λ k → Ord (od→ord k)) {!!} ⟩ Ord (od→ord (ord→od (minα a sp))) ≡⟨ cong (λ k → Ord k) diso ⟩ Ord (minα a sp) @@ -480,12 +444,12 @@ lemma3 : Def (Ord a) ∋ t lemma3 = ord-power← a t lemma0 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 ) )) + lemma4 = cong ( λ k → od→ord k ) ( ===-≡ (subst (λ k → t == (A ∩ k)) {!!} {!!} )) 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)} {od→ord t} ... | lt = o<-subst {suc n} {_} {_} {_} {_} lt (sym (subst (λ k → od→ord t ≡ k) lemma5 lemma4 )) refl where lemma5 : od→ord (A ∩ Ord (od→ord t)) ≡ od→ord (A ∩ ord→od (od→ord t)) - lemma5 = cong (λ k → od→ord (A ∩ k )) Ord-ord + lemma5 = cong (λ k → od→ord (A ∩ k )) {!!} 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 @@ -517,7 +481,7 @@ def ( Ord ( omax (od→ord x) (od→ord (Ord (omax (od→ord x) (od→ord x) )) ))) ( osuc y ) ≡⟨⟩ osuc y o< omax (od→ord x) (od→ord (Ord (omax (od→ord x) (od→ord x) )) ) - ≡⟨ cong (λ k → osuc y o< omax (od→ord x) k ) (sym ord-Ord) ⟩ + ≡⟨ cong (λ k → osuc y o< omax (od→ord x) k ) {!!} ⟩ osuc y o< omax (od→ord x) (omax (od→ord x) (od→ord x) ) ≡⟨ cong (λ k → osuc y o< k ) (omxxx (od→ord x) ) ⟩ osuc y o< osuc (osuc (od→ord x)) @@ -525,13 +489,13 @@ infinite : OD {suc n} infinite = Ord omega infinity∅ : Ord omega ∋ od∅ {suc n} - infinity∅ = o<-subst (case1 (s≤s z≤n) ) ord-Ord refl + infinity∅ = o<-subst (case1 (s≤s z≤n) ) {!!} refl infinity : (x : OD) → infinite ∋ x → infinite ∋ Union (x , (x , x )) infinity x lt = o<-subst ( lemma (od→ord x) lt ) eq refl where eq : osuc (od→ord x) ≡ od→ord (Union (x , (x , x))) eq = let open ≡-Reasoning in begin osuc (od→ord x) - ≡⟨ ord-Ord ⟩ + ≡⟨ {!!} ⟩ od→ord (Ord (osuc (od→ord x))) ≡⟨ cong ( λ k → od→ord k ) ( sym (==→o≡ ( ⇔→== uxxx-ord ))) ⟩ od→ord (Union (x , (x , x)))
--- a/ordinal.agda Mon Jul 08 18:26:33 2019 +0900 +++ b/ordinal.agda Mon Jul 08 19:35:23 2019 +0900 @@ -118,6 +118,14 @@ =→¬< {Zero} () =→¬< {Suc x} (s≤s lt) = =→¬< lt +case12-⊥ : {n : Level} {x y : Ordinal {suc n}} → lv x < lv y → ord x d< ord y → ⊥ +case12-⊥ {x} {y} lt1 lt2 with d<→lv lt2 +... | refl = nat-≡< refl lt1 + +case21-⊥ : {n : Level} {x y : Ordinal {suc n}} → lv x < lv y → ord y d< ord x → ⊥ +case21-⊥ {x} {y} lt1 lt2 with d<→lv lt2 +... | refl = nat-≡< refl lt1 + o<¬≡ : {n : Level } { ox oy : Ordinal {n}} → ox ≡ oy → ox o< oy → ⊥ o<¬≡ {_} {ox} {ox} refl (case1 lt) = =→¬< lt o<¬≡ {_} {ox} {ox} refl (case2 (s< lt)) = trio<≡ refl lt