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

comparison OD.agda @ 400:48ea49494fd1

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
use induction
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 28 Jul 2020 08:35:58 +0900
parents 03a4e1b8f3fb
children 59152f16125a
comparison
equal deleted inserted replaced
399:03a4e1b8f3fb 400:48ea49494fd1
404 -- ωmax : Ordinal 404 -- ωmax : Ordinal
405 -- <ωmax : {y : Ordinal} → infinite-d y → y o< ωmax 405 -- <ωmax : {y : Ordinal} → infinite-d y → y o< ωmax
406 -- 406 --
407 -- infinite : HOD 407 -- infinite : HOD
408 -- infinite = record { od = record { def = λ x → infinite-d x } ; odmax = ωmax ; <odmax = <ωmax } 408 -- infinite = record { od = record { def = λ x → infinite-d x } ; odmax = ωmax ; <odmax = <ωmax }
409
410 odsuc : (y : HOD) → HOD
411 odsuc y = Union (y , (y , y))
409 412
410 infinite : HOD 413 infinite : HOD
411 infinite = record { od = record { def = λ x → infinite-d x } ; odmax = next o∅ ; <odmax = lemma } where 414 infinite = record { od = record { def = λ x → infinite-d x } ; odmax = next o∅ ; <odmax = lemma } where
412 u : (y : Ordinal ) → HOD 415 u : (y : Ordinal ) → HOD
413 u y = Union (ord→od y , (ord→od y , ord→od y)) 416 u y = Union (ord→od y , (ord→od y , ord→od y))
435 438
436 nat→ω : Nat → HOD 439 nat→ω : Nat → HOD
437 nat→ω Zero = od∅ 440 nat→ω Zero = od∅
438 nat→ω (Suc y) = Union (nat→ω y , (nat→ω y , nat→ω y)) 441 nat→ω (Suc y) = Union (nat→ω y , (nat→ω y , nat→ω y))
439 442
443 ω→nato : {y : Ordinal} → infinite-d y → Nat
444 ω→nato iφ = Zero
445 ω→nato (isuc lt) = Suc (ω→nato lt)
446
440 ω→nat : (n : HOD) → infinite ∋ n → Nat 447 ω→nat : (n : HOD) → infinite ∋ n → Nat
441 ω→nat n = lemma where 448 ω→nat n = ω→nato
442 lemma : {y : Ordinal} → infinite-d y → Nat
443 lemma iφ = Zero
444 lemma (isuc lt) = Suc (lemma lt)
445 449
446 ω∋nat→ω : {n : Nat} → def (od infinite) (od→ord (nat→ω n)) 450 ω∋nat→ω : {n : Nat} → def (od infinite) (od→ord (nat→ω n))
447 ω∋nat→ω {Zero} = subst (λ k → def (od infinite) k) (sym ord-od∅) iφ 451 ω∋nat→ω {Zero} = subst (λ k → def (od infinite) k) (sym ord-od∅) iφ
448 ω∋nat→ω {Suc n} = subst (λ k → def (od infinite) k) lemma (isuc ( ω∋nat→ω {n})) where 452 ω∋nat→ω {Suc n} = subst (λ k → def (od infinite) k) lemma (isuc ( ω∋nat→ω {n})) where
449 lemma : od→ord (Union (ord→od (od→ord (nat→ω n)) , (ord→od (od→ord (nat→ω n)) , ord→od (od→ord (nat→ω n))))) ≡ od→ord (nat→ω (Suc n)) 453 lemma : od→ord (Union (ord→od (od→ord (nat→ω n)) , (ord→od (od→ord (nat→ω n)) , ord→od (od→ord (nat→ω n))))) ≡ od→ord (nat→ω (Suc n))
450 lemma = subst (λ k → od→ord (Union (k , ( k , k ))) ≡ od→ord (nat→ω (Suc n))) (sym oiso) refl 454 lemma = subst (λ k → od→ord (Union (k , ( k , k ))) ≡ od→ord (nat→ω (Suc n))) (sym oiso) refl
451 455
452 _=h=_ : (x y : HOD) → Set n 456 _=h=_ : (x y : HOD) → Set n
453 x =h= y = od x == od y 457 x =h= y = od x == od y
454 458
455 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 459 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
456 postulate f-extensionality : { n m : Level} → HE.Extensionality n m 460 -- postulate f-extensionality : { n m : Level} → HE.Extensionality n m
457
458
459 ord∋eq : {A i : HOD } → { f : (x : HOD ) → A ∋ x → Set (suc n)}
460 → ( ( x : Ordinal ) → ( lx : odef A x ) → f (ord→od x) (d→∋ A lx) )
461 → ( lt : A ∋ i ) → f i lt
462 ord∋eq {A} {i} {f} of lt = lemma oiso lt where
463 lemma2 : (j : Ordinal) → (ltj : odef A j )
464 → (i : HOD) → (lti : odef A (od→ord i) )
465 → (ord→od j ≡ i ) → d→∋ A ltj ≅ lti
466 lemma2 j _ i _ refl = HE.refl
467 lemma1 : (j : Ordinal) → (ltj : odef A j )
468 → (i : HOD) → (lti : odef A (od→ord i) )
469 → (ord→od j ≡ i ) → d→∋ A ltj ≅ lti
470 → f (ord→od j) (d→∋ A ltj) ≡ f i lti
471 lemma1 j _ i _ refl HE.refl = refl
472 lemma0 : (j : Ordinal) → (lt : odef A j ) → f (ord→od j) (d→∋ A lt)
473 lemma0 j lt = of j lt
474 lemma : {i : HOD } → {j : Ordinal} → ord→od j ≡ i → (lti : odef A (od→ord i)) → f i lti
475 lemma {i} {j} refl lt = subst (λ k → f (ord→od j) k ) {!!} ( of j (subst (λ k → odef A k ) diso lt ))
476 461
477 nat→ω-iso : {i : HOD} → (lt : infinite ∋ i ) → nat→ω ( ω→nat i lt ) ≡ i 462 nat→ω-iso : {i : HOD} → (lt : infinite ∋ i ) → nat→ω ( ω→nat i lt ) ≡ i
478 nat→ω-iso {i} lt = ord∋eq {infinite} {i} (λ x lx → lemma lx ) lt where 463 nat→ω-iso {i} lt = lemma lt i (sym oiso) od∅ iφ (sym o∅≡od∅) init where
479 lemma : {x : Ordinal} → (lx : infinite-d x ) → nat→ω ( ω→nat (ord→od x) (d→∋ infinite lx) ) ≡ ord→od x 464 init : nat→ω ( ω→nato iφ ) ≡ od∅
480 lemma {o∅} iφ = begin 465 init = refl
481 nat→ω (ω→nat (ord→od o∅) (d→∋ infinite iφ)) 466 lemma : {x y : Ordinal } → (ltd : infinite-d x ) → (xi : HOD) → xi ≡ ord→od x
482 ≡⟨ {!!} ⟩ 467 → (pi : HOD) → (prev : infinite-d y ) → pi ≡ ord→od y → nat→ω (ω→nato prev) ≡ pi
483 nat→ω Zero 468 → nat→ω (ω→nato ltd) ≡ xi
484 ≡⟨ sym o∅≡od∅ ⟩ 469 lemma {x} {y} ltd xi xi=x p pi prev pi=p = {!!}
485 ord→od o∅ 470
486 ∎ where open ≡-Reasoning 471 nat→ω-iso' : {i : HOD} → (lt : infinite ∋ i ) → nat→ω ( ω→nat i lt ) ≡ i
487 lemma {x1} (isuc lx) = {!!} 472 nat→ω-iso' {i} = ε-induction1 {λ i → (lt : infinite ∋ i ) → nat→ω ( ω→nat i lt ) ≡ i } ind i where
488 473 ind : {x : HOD} → ({y : HOD} → x ∋ y → (lt : infinite ∋ y) → nat→ω (ω→nat y lt) ≡ y) →
474 (lt : infinite ∋ x) → nat→ω (ω→nat x lt) ≡ x
475 ind {x} prev lt = ind1 lt oiso where
476 ind1 : {ox : Ordinal } → (ltd : infinite-d ox ) → ord→od ox ≡ x → nat→ω (ω→nato ltd) ≡ x
477 ind1 {o∅} iφ refl = sym o∅≡od∅
478 ind1 (isuc ltd) ox=x = trans (cong (λ k → odsuc k ) (prev {!!} {!!}) ) ?
479
489 480
490 infixr 200 _∈_ 481 infixr 200 _∈_
491 -- infixr 230 _∩_ _∪_ 482 -- infixr 230 _∩_ _∪_
492 483
493 pair→ : ( x y t : HOD ) → (x , y) ∋ t → ( t =h= x ) ∨ ( t =h= y ) 484 pair→ : ( x y t : HOD ) → (x , y) ∋ t → ( t =h= x ) ∨ ( t =h= y )