Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff HOD.agda @ 150:ebcbfd9d9c8e
fix some
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 08 Jul 2019 22:37:10 +0900 |
| parents | 6e767ad3edc2 |
| children | b5a337fb7a6d |
line wrap: on
line diff
--- a/HOD.agda Mon Jul 08 19:45:59 2019 +0900 +++ b/HOD.agda Mon Jul 08 22:37:10 2019 +0900 @@ -60,6 +60,7 @@ 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 + -- we should prove this in agda, but simply put here ==→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 @@ -74,8 +75,6 @@ -- this should be ¬ (x == od∅ )→ ∃ ox → x ∋ Ord ox ( minimum of x ) x∋minimul : {n : Level } → (x : OD {suc n} ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimul x ne ) ) minimul-1 : {n : Level } → (x : OD {suc n} ) → ( ne : ¬ (x == od∅ ) ) → (y : OD {suc n}) → ¬ ( def (minimul x ne) (od→ord y)) ∧ (def x (od→ord y) ) - -- we should prove this in agda, but simply put here - ===-≡ : {n : Level} { x y : OD {suc n}} → x == y → x ≡ y _∋_ : { n : Level } → ( a x : OD {n} ) → Set n _∋_ {n} a x = def a ( od→ord x ) @@ -163,7 +162,18 @@ t : (od→ord x) o< (od→ord a) t = c<→o< {suc n} {x} {a} lt --- o∅≡od∅ : {n : Level} → ord→od (o∅ {suc n}) ≡ od∅ {suc n} +o∅≡od∅ : {n : Level} → ord→od (o∅ {suc n}) ≡ od∅ {suc n} +o∅≡od∅ {n} = ==→o≡ lemma where + lemma0 : {x : Ordinal} → def (ord→od o∅) x → def od∅ x + lemma0 {x} lt = o<-subst (c<→o< {suc n} {ord→od x} {ord→od o∅} (def-subst {suc n} {ord→od o∅} {x} lt refl (sym diso)) ) diso diso + lemma1 : {x : Ordinal} → def od∅ x → def (ord→od o∅) x + lemma1 (case1 ()) + lemma1 (case2 ()) + lemma : ord→od o∅ == od∅ + lemma = record { eq→ = lemma0 ; eq← = lemma1 } + +ord-od∅ : {n : Level} → od→ord (od∅ {suc n}) ≡ o∅ {suc n} +ord-od∅ {n} = sym ( subst (λ k → k ≡ od→ord (od∅ {suc n}) ) diso (cong ( λ k → od→ord k ) o∅≡od∅ ) ) o<→¬c> : {n : Level} → { x y : OD {n} } → (od→ord x ) o< ( od→ord y) → ¬ (y c< x ) o<→¬c> {n} {x} {y} olt clt = o<> olt (c<→o< clt ) where @@ -207,7 +217,7 @@ Def {n} A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) ) OrdSubset : {n : Level} → (A x : Ordinal {suc n} ) → ZFSubset (Ord A) (Ord x) ≡ Ord ( minα A x ) -OrdSubset {n} A x = ===-≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where +OrdSubset {n} A x = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where lemma1 : {y : Ordinal} → def (ZFSubset (Ord A) (Ord x)) y → def (Ord (minα A x)) y lemma1 {y} s with trio< A x lemma1 {y} s | tri< a ¬b ¬c = proj1 s @@ -332,17 +342,16 @@ 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)) - {!!} } )) + 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 = contra-position lemma (lemma2 {!!}) where - lemma2 : ¬ ((y : Ordinal) → ¬ def X y ∧ ((od→ord x) ≡ od→ord (ψ (Ord y)))) - → ¬ ((y : Ordinal) → ¬ def X y ∧ (ord→od (od→ord x) == ψ (Ord y))) + replacement→ {ψ} X x lt = contra-position lemma (lemma2 (proj2 lt)) where + lemma2 : ¬ ((y : Ordinal) → ¬ def X y ∧ ((od→ord x) ≡ od→ord (ψ (ord→od y)))) + → ¬ ((y : Ordinal) → ¬ def X y ∧ (ord→od (od→ord x) == ψ (ord→od y))) lemma2 not not2 = not ( λ y d → not2 y (record { proj1 = proj1 d ; proj2 = lemma3 (proj2 d)})) where - lemma3 : {y : Ordinal } → (od→ord x ≡ od→ord (ψ (Ord y))) → (ord→od (od→ord x) == ψ (Ord y)) + lemma3 : {y : Ordinal } → (od→ord x ≡ od→ord (ψ (ord→od y))) → (ord→od (od→ord x) == ψ (ord→od y)) lemma3 {y} eq = subst (λ k → ord→od (od→ord x) == k ) oiso (o≡→== eq ) - 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 )) + lemma : ( (y : OD) → ¬ (x == ψ y)) → ( (y : Ordinal) → ¬ def X y ∧ (ord→od (od→ord x) == ψ (ord→od y)) ) + lemma not y not2 = not (ord→od y) (subst (λ k → k == ψ (ord→od y)) oiso ( proj2 not2 )) --- --- Power Set @@ -407,7 +416,7 @@ ( t→A (def-subst {suc n} {_} {_} {t} {od→ord (ord→od z)} w refl (sym diso) )) refl diso } lemma1 : {n : Level } {a : Ordinal {suc n}} { t : OD {suc n}} → (eq : ZFSubset (Ord a) t == t) → od→ord (ZFSubset (Ord a) (ord→od (od→ord t))) ≡ od→ord t - lemma1 {n} {a} {t} eq = subst (λ k → od→ord (ZFSubset (Ord a) k) ≡ od→ord t ) (sym oiso) (cong (λ k → od→ord k ) (===-≡ eq )) + lemma1 {n} {a} {t} eq = subst (λ k → od→ord (ZFSubset (Ord a) k) ≡ od→ord t ) (sym oiso) (cong (λ k → od→ord k ) (==→o≡ eq )) 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< @@ -435,7 +444,7 @@ 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)) {!!} {!!} )) + lemma4 = cong ( λ k → od→ord k ) ( ==→o≡ (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 @@ -480,7 +489,7 @@ infinite : OD {suc n} infinite = Ord omega infinity∅ : Ord omega ∋ od∅ {suc n} - infinity∅ = o<-subst (case1 (s≤s z≤n) ) {!!} refl + infinity∅ = o<-subst (case1 (s≤s z≤n) ) (sym ord-od∅) 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)))