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

changeset 91:b4742cf4ef97

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
infinity axiom done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 05 Jun 2019 18:24:32 +0900
parents 38d139b5edac
children ef0dfc4b97fd
files ordinal-definable.agda ordinal.agda
diffstat 2 files changed, 49 insertions(+), 13 deletions(-) [+]
line wrap: on
line diff
--- a/ordinal-definable.agda	Wed Jun 05 14:35:32 2019 +0900
+++ b/ordinal-definable.agda	Wed Jun 05 18:24:32 2019 +0900
@@ -178,6 +178,16 @@
 od≡-def : {n : Level} →  { x : Ordinal {suc n} } → ord→od x ≡ record { def = λ z → z o< x } 
 od≡-def {n} {x} = subst (λ k  → ord→od x ≡ k ) oiso (cong ( λ k → ord→od k ) (≡-def {n} {x} ))
 
+∋→o< : {n : Level} →  { a x : OD {suc n} } → a ∋ x → od→ord x o< od→ord a
+∋→o< {n} {a} {x} lt = t where
+         t : (od→ord x) o< (od→ord a)
+         t = c<→o< {suc n} {x} {a} lt 
+
+o<∋→ : {n : Level} →  { a x : OD {suc n} } → od→ord x o< od→ord a → a ∋ x 
+o<∋→ {n} {a} {x} lt = subst₂ (λ k j → def k j ) oiso diso t  where
+         t : def (ord→od (od→ord a)) (od→ord (ord→od (od→ord x)))
+         t = o<→c< {suc n} {od→ord x} {od→ord a} lt 
+
 ¬x<0 : {n : Level} →  { x  : Ordinal {suc n} } → ¬ ( x o< o∅ {suc n} )
 ¬x<0 {n} {x} (case1 ())
 ¬x<0 {n} {x} (case2 ())
@@ -362,27 +372,44 @@
          xx-union {x} = cong ( λ k → record { def = λ z → z o< k } ) (omxx (od→ord x))
          xxx-union : {x  : OD {suc n}} → (x , (x , x)) ≡ record { def = λ z → z o< osuc (osuc (od→ord x))}
          xxx-union {x} = cong ( λ k → record { def = λ z → z o< k } ) lemma where
+             lemma1 : {x  : OD {suc n}} → od→ord x o< od→ord (x , x)
+             lemma1 {x} = c<→o< ( proj1 (pair x x ) )
+             lemma2 : {x  : OD {suc n}} → od→ord (x , x) ≡ osuc (od→ord x)
+             lemma2 = trans ( cong ( λ k →  od→ord k ) xx-union ) (sym ≡-def)
              lemma : {x  : OD {suc n}} → omax (od→ord x) (od→ord (x , x)) ≡ osuc (osuc (od→ord x))
-             lemma {x} = trans ( sym ( omax< (od→ord x) (od→ord (x , x)) {!!} ) ) ( cong ( λ k → osuc k ) {!!} )
+             lemma {x} = trans ( sym ( omax< (od→ord x) (od→ord (x , x)) lemma1 ) ) ( cong ( λ k → osuc k ) lemma2 )
          uxxx-union : {x  : OD {suc n}} → Union (x , (x , x)) ≡ record { def = λ z → osuc z o< osuc (osuc (od→ord x)) }
          uxxx-union {x} = cong ( λ k → record { def = λ z → osuc z o< k } ) lemma where
              lemma : od→ord (x , (x , x)) ≡ osuc (osuc (od→ord x))
-             lemma = {!!}
+             lemma = trans ( cong ( λ k → od→ord k ) xxx-union ) (sym ≡-def )
+         uxxx-2 : {x  : OD {suc n}} → record { def = λ z → osuc z o< osuc (osuc (od→ord x)) } == record { def = λ z → z o< osuc (od→ord x) }
+         eq→ ( uxxx-2 {x} ) {m} lt = proj1 (osuc2 m (od→ord x)) lt
+         eq← ( uxxx-2 {x} ) {m} lt = proj2 (osuc2 m (od→ord x)) lt
+         uxxx-ord : {x  : OD {suc n}} → od→ord (Union (x , (x , x))) ≡ osuc (od→ord x)
+         uxxx-ord {x} = trans (cong (λ k →  od→ord k ) uxxx-union) (==→o≡ (subst₂ (λ j k → j == k ) (sym oiso) (sym od≡-def ) uxxx-2 )) 
+         omega = record { lv = Suc Zero ; ord = Φ 1 }
          infinite : OD {suc n}
-         infinite = ord→od ( record { lv = Suc Zero ; ord = Φ 1 } )
-         infinity∅ : ord→od ( record { lv = Suc Zero ; ord = Φ 1  } ) ∋ od∅ {suc n}
+         infinite = ord→od ( omega )
+         infinity∅ : ord→od ( omega ) ∋ od∅ {suc n}
          infinity∅ = def-subst {suc n} {_} {od→ord (ord→od o∅)} {infinite} {od→ord od∅}
               (o<→c< ( case1 (s≤s z≤n )))  refl (cong (λ k →  od→ord k) o∅≡od∅ )
+         infinite∋x : (x : OD) → infinite ∋ x → od→ord x o< omega
+         infinite∋x x lt = subst (λ k → od→ord x o< k ) diso t where
+              t  : od→ord x o< od→ord (ord→od (omega))
+              t  = ∋→o< {n} {infinite} {x} lt
+         infinite∋uxxx : (x : OD) → osuc (od→ord x) o< omega → infinite ∋ Union (x , (x , x ))
+         infinite∋uxxx x lt = o<∋→ t where
+              t  :  od→ord (Union (x , (x , x))) o< od→ord (ord→od (omega))
+              t  = subst (λ k →  od→ord (Union (x , (x , x))) o< k ) (sym diso ) ( subst ( λ k → k o< omega ) ( sym  (uxxx-ord {x} ) ) lt ) 
          infinity : (x : OD) → infinite ∋ x → infinite ∋ Union (x , (x , x ))
-         infinity x ∞∋x = {!!}
-           where
-             lemma : (ox : Ordinal {suc n} ) → ox o< record { lv = Suc Zero ; ord = Φ 1 } → osuc ox o< record { lv = Suc Zero ; ord = Φ 1 } 
-             lemma record { lv = Zero ; ord = (Φ .0) } (case1 (s≤s x)) = case1 (s≤s z≤n)
-             lemma record { lv = Zero ; ord = (OSuc .0 ord₁) } (case1 (s≤s x)) = case1 (s≤s z≤n)
-             lemma record { lv = (Suc lv₁) ; ord = (Φ .(Suc lv₁)) } (case1 (s≤s ()))
-             lemma record { lv = (Suc lv₁) ; ord = (OSuc .(Suc lv₁) ord₁) } (case1 (s≤s ()))
-             lemma record { lv = 1 ; ord = (Φ 1) } (case2 c2) with d<→lv c2
-             lemma record { lv = (Suc Zero) ; ord = (Φ .1) } (case2 ()) | refl
+         infinity x lt = infinite∋uxxx x ( lemma (od→ord x) (infinite∋x x lt ))   where
+              lemma : (ox : Ordinal {suc n} ) → ox o< omega → osuc ox o< omega 
+              lemma record { lv = Zero ; ord = (Φ .0) } (case1 (s≤s x)) = case1 (s≤s z≤n)
+              lemma record { lv = Zero ; ord = (OSuc .0 ord₁) } (case1 (s≤s x)) = case1 (s≤s z≤n)
+              lemma record { lv = (Suc lv₁) ; ord = (Φ .(Suc lv₁)) } (case1 (s≤s ()))
+              lemma record { lv = (Suc lv₁) ; ord = (OSuc .(Suc lv₁) ord₁) } (case1 (s≤s ()))
+              lemma record { lv = 1 ; ord = (Φ 1) } (case2 c2) with d<→lv c2
+              lemma record { lv = (Suc Zero) ; ord = (Φ .1) } (case2 ()) | refl
          replacement : {ψ : OD → OD} (X x : OD) → Replace X ψ ∋ ψ x
          replacement {ψ} X x = {!!}
 
--- a/ordinal.agda	Wed Jun 05 14:35:32 2019 +0900
+++ b/ordinal.agda	Wed Jun 05 18:24:32 2019 +0900
@@ -242,6 +242,15 @@
 omxxx : {n : Level} ( x : Ordinal {suc n} ) → omax x (omax x x ) ≡ osuc (osuc x)
 omxxx {n} x = trans ( cong ( λ k → omax x k ) (omxx x )) (sym ( omax< x (osuc x) <-osuc ))
 
+open _∧_
+
+osuc2 : {n : Level} ( x y : Ordinal {suc n} ) → ( osuc x o< osuc (osuc y )) ⇔ (x o< osuc y)
+proj1 (osuc2 {n} x y) (case1 lt) = case1 lt
+proj1 (osuc2 {n} x y) (case2 (s< lt)) = case2 lt
+proj2 (osuc2 {n} x y) (case1 lt) = case1 lt
+proj2 (osuc2 {n} x y) (case2 lt) with d<→lv lt
+... | refl = case2 (s< lt)
+
 -- omax≡ (omax x x ) (osuc x) (omxx x)
 
 OrdTrans : {n : Level} → Transitive {suc n} _o≤_