Mercurial > hg > Members > kono > Proof > ZF-in-agda

comparison HOD.agda @ 119:6e264c78e420

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
infinite equlaity of set
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 26 Jun 2019 22:53:30 +0900
parents 78fe704c3543
children ac214eab1c3c
comparison
equal deleted inserted replaced
118:78fe704c3543 119:6e264c78e420
204 is-o∅ {n} record { lv = Zero ; ord = (Φ .0) } = yes refl 204 is-o∅ {n} record { lv = Zero ; ord = (Φ .0) } = yes refl
205 is-o∅ {n} record { lv = Zero ; ord = (OSuc .0 ord₁) } = no ( λ () ) 205 is-o∅ {n} record { lv = Zero ; ord = (OSuc .0 ord₁) } = no ( λ () )
206 is-o∅ {n} record { lv = (Suc lv₁) ; ord = ord } = no (λ()) 206 is-o∅ {n} record { lv = (Suc lv₁) ; ord = ord } = no (λ())
207 207
208 open _∧_ 208 open _∧_
209
210 ord⇔ : {n : Level} → ( x y : HOD {suc n} ) → ( {z : Ordinal {suc n} } → def x z ⇔ def y z ) → od→ord x ≡ od→ord y
211 ord⇔ = {!!}
209 212
210 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 213 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
211 -- postulate f-extensionality : { n : Level} → Relation.Binary.PropositionalEquality.Extensionality (suc n) (suc (suc n)) 214 -- postulate f-extensionality : { n : Level} → Relation.Binary.PropositionalEquality.Extensionality (suc n) (suc (suc n))
212 215
213 csuc : {n : Level} → HOD {suc n} → HOD {suc n} 216 csuc : {n : Level} → HOD {suc n} → HOD {suc n}
369 lemma2 : {x₁ : Ordinal} → def od∅ x₁ → def (Select (minimul x not) (λ x₂ → (minimul x not ∋ x₂) ∧ (x ∋ x₂))) x₁ 372 lemma2 : {x₁ : Ordinal} → def od∅ x₁ → def (Select (minimul x not) (λ x₂ → (minimul x not ∋ x₂) ∧ (x ∋ x₂))) x₁
370 lemma2 {y} d = ⊥-elim (empty (ord→od y) (def-subst {suc n} {_} {_} {od∅} {od→ord (ord→od y)} d refl (sym diso) )) 373 lemma2 {y} d = ⊥-elim (empty (ord→od y) (def-subst {suc n} {_} {_} {od∅} {od→ord (ord→od y)} d refl (sym diso) ))
371 extensionality : {A B : HOD {suc n}} → ((z : HOD) → (A ∋ z) ⇔ (B ∋ z)) → A == B 374 extensionality : {A B : HOD {suc n}} → ((z : HOD) → (A ∋ z) ⇔ (B ∋ z)) → A == B
372 eq→ (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {A} {B} (sym diso) (proj1 (eq (ord→od x))) d 375 eq→ (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {A} {B} (sym diso) (proj1 (eq (ord→od x))) d
373 eq← (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {B} {A} (sym diso) (proj2 (eq (ord→od x))) d 376 eq← (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {B} {A} (sym diso) (proj2 (eq (ord→od x))) d
374 xx-union : {x : HOD {suc n}} → (x , x) ≡ record { def = λ z → z o< osuc (od→ord x) } 377 open import Relation.Binary.PropositionalEquality
375 xx-union {x} = cong ( λ k → Ord k ) (omxx (od→ord x)) 378 uxxx-ord : {x : HOD {suc n}} → {y : Ordinal {suc n}} → def (Union (x , (x , x))) y ⇔ ( y o< osuc (od→ord x) )
376 xxx-union : {x : HOD {suc n}} → (x , (x , x)) ≡ record { def = λ z → z o< osuc (osuc (od→ord x))} 379 uxxx-ord {x} {y} = subst (λ k → k ⇔ ( y o< osuc (od→ord x) )) (sym lemma) ( osuc2 y (od→ord x)) where
377 xxx-union {x} = cong ( λ k → Ord k ) lemma where 380 lemma : {y : Ordinal {suc n}} → def (Union (x , (x , x))) y ≡ osuc y o< osuc (osuc (od→ord x))
378 lemma1 : {x : HOD {suc n}} → od→ord x o< od→ord (x , x) 381 lemma {y} = let open ≡-Reasoning in begin
379 lemma1 {x} = c<→o< ( proj1 (pair x x ) ) 382 def (Union (x , (x , x))) y
380 lemma2 : {x : HOD {suc n}} → od→ord (x , x) ≡ osuc (od→ord x) 383 ≡⟨⟩
381 lemma2 = trans ( cong ( λ k → od→ord k ) xx-union ) {!!} 384 def ( Ord ( omax (od→ord x) (od→ord (Ord (omax (od→ord x) (od→ord x) )) ))) ( osuc y )
382 lemma : {x : HOD {suc n}} → omax (od→ord x) (od→ord (x , x)) ≡ osuc (osuc (od→ord x)) 385 ≡⟨⟩
383 lemma {x} = trans ( sym ( omax< (od→ord x) (od→ord (x , x)) lemma1 ) ) ( cong ( λ k → osuc k ) lemma2 ) 386 osuc y o< omax (od→ord x) (od→ord (Ord (omax (od→ord x) (od→ord x) )) )
384 uxxx-union : {x : HOD {suc n}} → Union (x , (x , x)) ≡ record { def = λ z → osuc z o< osuc (osuc (od→ord x)) } 387 ≡⟨ cong (λ k → osuc y o< omax (od→ord x) k ) (sym ord-Ord) ⟩
385 uxxx-union {x} = cong ( λ k → record { def = λ z → osuc z o< k ; otrans = {!!} } ) {!!} where 388 osuc y o< omax (od→ord x) (omax (od→ord x) (od→ord x) )
386 lemma : od→ord (x , (x , x)) ≡ osuc (osuc (od→ord x)) 389 ≡⟨ cong (λ k → osuc y o< k ) (omxxx (od→ord x) ) ⟩
387 lemma = trans ( cong ( λ k → od→ord k ) xxx-union ) {!!} 390 osuc y o< osuc (osuc (od→ord x))
388 uxxx-2 : {x : HOD {suc n}} → record { def = λ z → osuc z o< osuc (osuc (od→ord x)) } == record { def = λ z → z o< osuc (od→ord x) } 391 ∎
389 eq→ ( uxxx-2 {x} ) {m} lt = proj1 (osuc2 m (od→ord x)) lt
390 eq← ( uxxx-2 {x} ) {m} lt = proj2 (osuc2 m (od→ord x)) lt
391 uxxx-ord : {x : HOD {suc n}} → od→ord (Union (x , (x , x))) ≡ osuc (od→ord x)
392 uxxx-ord {x} = trans (cong (λ k → od→ord k ) uxxx-union) {!!}
393 infinite : HOD {suc n} 392 infinite : HOD {suc n}
394 infinite = Ord omega 393 infinite = Ord omega
395 infinity∅ : Ord omega ∋ od∅ {suc n} 394 infinity∅ : Ord omega ∋ od∅ {suc n}
396 infinity∅ = {!!} 395 infinity∅ = o<-subst (case1 (s≤s z≤n) ) ord-Ord refl
397 infinity : (x : HOD) → infinite ∋ x → infinite ∋ Union (x , (x , x )) 396 infinity : (x : HOD) → infinite ∋ x → infinite ∋ Union (x , (x , x ))
398 infinity x lt = {!!} where 397 infinity x lt = {!!} where
399 lemma : (ox : Ordinal {suc n} ) → ox o< omega → osuc ox o< omega 398 lemma : (ox : Ordinal {suc n} ) → ox o< omega → osuc ox o< omega
400 lemma record { lv = Zero ; ord = (Φ .0) } (case1 (s≤s x)) = case1 (s≤s z≤n) 399 lemma record { lv = Zero ; ord = (Φ .0) } (case1 (s≤s x)) = case1 (s≤s z≤n)
401 lemma record { lv = Zero ; ord = (OSuc .0 ord₁) } (case1 (s≤s x)) = case1 (s≤s z≤n) 400 lemma record { lv = Zero ; ord = (OSuc .0 ord₁) } (case1 (s≤s x)) = case1 (s≤s z≤n)