Members/kono/Proof/ZF-in-agda: ordinal-definable.agda comparison

comparison ordinal-definable.agda @ 95:f3da2c87cee0

clean up

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Sat, 08 Jun 2019 17:33:09 +0900
parents	4659a815b70d
children	f239ffc27fd0

comparison

equal deleted inserted replaced

-:4659a815b70d
+:f3da2c87cee0
 open import zf
 open import ordinal
 open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ )
 open import  Relation.Binary.PropositionalEquality
 open import Data.Nat.Properties
 open import Data.Empty
 open import Relation.Nullary
 open import Relation.Binary
 open import Relation.Binary.Core
 -- Ordinal Definable Set
 open OD
 open import Data.Unit
 open Ordinal
-postulate
-od→ord : {n : Level} → OD {n} → Ordinal {n}
-ord→od : {n : Level} → Ordinal {n} → OD {n}
-_∋_ : { n : Level } → ( a x : OD {n} ) → Set n
-_∋_ {n} a x  = def a ( od→ord x )
-_c<_ : { n : Level } → ( x a : OD {n} ) → Set n
-x c< a = a ∋ x
 record _==_ {n : Level} ( a b :  OD {n} ) : Set n where
 field
 eq→ : ∀ { x : Ordinal {n} } → def a x → def b x
 eq← : ∀ { x : Ordinal {n} } → def b x → def a x
 eq-sym eq = record { eq→ = eq← eq ; eq← = eq→ eq }
 eq-trans : {n : Level} {  x y z :  OD {n} } → x == y → y == z → x == z
 eq-trans x=y y=z = record { eq→ = λ t → eq→ y=z ( eq→ x=y  t) ; eq← = λ t → eq← x=y ( eq← y=z t) }
+od∅ : {n : Level} → OD {n}
+od∅ {n} = record { def = λ _ → Lift n ⊥ }
+postulate
+od→ord : {n : Level} → OD {n} → Ordinal {n}
+ord→od : {n : Level} → Ordinal {n} → OD {n}
+c<→o<  : {n : Level} {x y : OD {n} }      → def y ( od→ord x ) → od→ord x o< od→ord y
+o<→c<  : {n : Level} {x y : Ordinal {n} } → x o< y             → def (ord→od y) x
+oiso   : {n : Level} {x : OD {n}}      → ord→od ( od→ord x ) ≡ x
+diso   : {n : Level} {x : Ordinal {n}} → od→ord ( ord→od x ) ≡ x
+sup-o  : {n : Level } → ( Ordinal {n} → Ordinal {n}) →  Ordinal {n}
+sup-o< : {n : Level } → ( ψ : Ordinal {n} →  Ordinal {n}) → ∀ {x : Ordinal {n}} →  ψ x  o<  sup-o ψ
+_∋_ : { n : Level } → ( a x : OD {n} ) → Set n
+_∋_ {n} a x  = def a ( od→ord x )
+_c<_ : { n : Level } → ( x a : OD {n} ) → Set n
+x c< a = a ∋ x
 _c≤_ : {n : Level} →  OD {n} →  OD {n} → Set (suc n)
 a c≤ b  = (a ≡ b)  ∨ ( b ∋ a )
-od∅ : {n : Level} → OD {n}
+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
-od∅ {n} = record { def = λ _ → Lift n ⊥ }
+def-subst df refl refl = df
-postulate
+sup-od : {n : Level } → ( OD {n} → OD {n}) →  OD {n}
-c<→o< : {n : Level} {x y : OD {n} } → x c< y → od→ord x o< od→ord y
+sup-od ψ = ord→od ( sup-o ( λ x → od→ord (ψ (ord→od x ))) )
-o<→c< : {n : Level} {x y : Ordinal {n} } → x o< y → ord→od x c< ord→od y
-oiso : {n : Level} {x : OD {n}} → ord→od ( od→ord x ) ≡ x
+sup-c< : {n : Level } → ( ψ : OD {n} →  OD {n}) → ∀ {x : OD {n}} → def ( sup-od ψ ) (od→ord ( ψ x ))
-diso : {n : Level} {x : Ordinal {n}} → od→ord ( ord→od x ) ≡ x
+sup-c< {n} ψ {x} = def-subst {n} {_} {_} {sup-od ψ} {od→ord ( ψ x )}
-sup-od : {n : Level } → ( OD {n} → OD {n}) →  OD {n}
+( o<→c< ( sup-o< ( λ y → od→ord (ψ (ord→od y ))) {od→ord x } )) refl (cong ( λ k → od→ord (ψ k) ) oiso)
-sup-c< : {n : Level } → ( ψ : OD {n} →  OD {n}) → ∀ {x : OD {n}} → ψ x  c< sup-od ψ
 ∅1 : {n : Level} →  ( x : OD {n} )  → ¬ ( x c< od∅ {n} )
 ∅1 {n} x (lift ())
 ∅3 : {n : Level} →  { x : Ordinal {n}}  → ( ∀(y : Ordinal {n}) → ¬ (y o< x ) ) → x ≡ o∅ {n}
 c3 lx (Φ .lx) d not | t | ()
 c3 lx (OSuc .lx x₁) d not with not (  record { lv = lx ; ord = OSuc lx x₁ } )
 ... | t with t (case2 (s< s<refl ) )
 c3 lx (OSuc .lx x₁) d not | t | ()
-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
 transitive : {n : Level } { z y x : OD {suc n} } → z ∋ y → y ∋ x → z  ∋ x
 transitive  {n} {z} {y} {x} z∋y x∋y  with  ordtrans ( c<→o< {suc n} {x} {y} x∋y ) (  c<→o< {suc n} {y} {z} z∋y )
 ... | t = lemma0 (lemma t) where
-lemma : ( od→ord x ) o< ( od→ord z ) → def ( ord→od ( od→ord z )) ( od→ord ( ord→od ( od→ord x )))
+lemma : ( od→ord x ) o< ( od→ord z ) → def ( ord→od ( od→ord z )) ( od→ord x)
 lemma xo<z = o<→c< xo<z
-lemma0 :  def ( ord→od ( od→ord z )) ( od→ord ( ord→od ( od→ord x ))) →  def z (od→ord x)
+lemma0 :  def ( ord→od ( od→ord z )) ( od→ord x) →  def z (od→ord x)
-lemma0 dz  = def-subst {suc n} { ord→od ( od→ord z )} { od→ord ( ord→od ( od→ord x))} dz (oiso) (diso)
+lemma0 dz  = def-subst {suc n} { ord→od ( od→ord z )} { od→ord x} dz (oiso)  refl
 record Minimumo {n : Level } (x : Ordinal {n}) : Set (suc n) where
 field
 mino : Ordinal {n}
 min<x :  mino o< x
 c≤-refl : {n : Level} →  ( x : OD {n} ) → x c≤ x
 c≤-refl x = case1 refl
 o<→o> : {n : Level} →  { x y : OD {n} } →  (x == y) → (od→ord x ) o< ( od→ord y) → ⊥
 o<→o> {n} {x} {y} record { eq→ = xy ; eq← = yx } (case1 lt) with
-yx (def-subst {n} {ord→od (od→ord y)} {od→ord (ord→od (od→ord x))} (o<→c< (case1 lt )) oiso diso )
+yx (def-subst {n} {ord→od (od→ord y)} {od→ord x} (o<→c< (case1 lt )) oiso refl )
 ... | oyx with o<¬≡ (od→ord x) (od→ord x) refl (c<→o< oyx )
 ... | ()
 o<→o> {n} {x} {y} record { eq→ = xy ; eq← = yx } (case2 lt) with
-yx (def-subst {n} {ord→od (od→ord y)} {od→ord (ord→od (od→ord x))} (o<→c< (case2 lt )) oiso diso )
+yx (def-subst {n} {ord→od (od→ord y)} {od→ord x} (o<→c< (case2 lt )) oiso refl )
 ... | oyx with o<¬≡ (od→ord x) (od→ord x) refl (c<→o< oyx )
 ... | ()
 ==→o≡ : {n : Level} →  { x y : Ordinal {suc n} } → ord→od x == ord→od y →  x ≡ y
 ==→o≡ {n} {x} {y} eq with trio< {n} x y
 ==→o≡ {n} {x} {y} eq | tri> ¬a ¬b c = ⊥-elim ( o<→o> (eq-sym eq) (o<-subst c (sym ord-iso) (sym ord-iso )))
 ≡-def : {n : Level} →  { x : Ordinal {suc n} } → x ≡ od→ord (record { def = λ z → z o< x } )
 ≡-def {n} {x} = ==→o≡ {n} (subst (λ k → ord→od x == k ) (sym oiso) lemma ) where
 lemma :  ord→od x == record { def = λ z → z o< x }
-eq→ lemma {w} z = subst₂ (λ k j → k o< j ) diso diso t where
+eq→ lemma {w} z = subst₂ (λ k j → k o< j ) diso refl (subst (λ k → (od→ord ( ord→od w)) o< k ) diso t ) where
 t : (od→ord ( ord→od w)) o< (od→ord (ord→od x))
 t = c<→o< {suc n} {ord→od w} {ord→od x} (def-subst {suc n} {_} {_} {ord→od x} {_} z refl (sym diso))
-eq← lemma {w} z = def-subst {suc n} {_} {_} {ord→od x} {w} ( o<→c< {suc n} {_} {_} z ) refl diso
+eq← lemma {w} z = def-subst {suc n} {_} {_} {ord→od x} {w} ( o<→c< {suc n} {_} {_} z ) refl refl
 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
+o<∋→ {n} {a} {x} lt = subst₂ (λ k j → def k j ) oiso refl t  where
-t : def (ord→od (od→ord a)) (od→ord (ord→od (od→ord x)))
+t : def (ord→od (od→ord a)) (od→ord x)
 t = o<→c< {suc n} {od→ord x} {od→ord a} lt
 o∅≡od∅ : {n : Level} → ord→od (o∅ {suc n}) ≡ od∅ {suc n}
 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
 o≡→¬c< : {n : Level} →  { x y : OD {n} } →  (od→ord x ) ≡ ( od→ord y) →   ¬ x c< y
 o≡→¬c< {n} {x} {y} oeq lt  = o<¬≡ (od→ord x) (od→ord y) (orefl oeq ) (c<→o< lt)
 tri-c< : {n : Level} →  Trichotomous _==_ (_c<_ {suc n})
 tri-c< {n} x y with trio< {n} (od→ord x) (od→ord y)
-tri-c< {n} x y | tri< a ¬b ¬c = tri< (def-subst (o<→c< a) oiso diso) (o<→¬== a) ( o<→¬c> a )
+tri-c< {n} x y | tri< a ¬b ¬c = tri< (def-subst (o<→c< a) oiso refl) (o<→¬== a) ( o<→¬c> a )
 tri-c< {n} x y | tri≈ ¬a b ¬c = tri≈ (o≡→¬c< b) (ord→== b) (o≡→¬c< (sym b))
-tri-c< {n} x y | tri> ¬a ¬b c = tri>  ( o<→¬c> c) (λ eq → o<→¬== c (eq-sym eq ) ) (def-subst (o<→c< c) oiso diso)
+tri-c< {n} x y | tri> ¬a ¬b c = tri>  ( o<→¬c> c) (λ eq → o<→¬== c (eq-sym eq ) ) (def-subst (o<→c< c) oiso refl)
 c<> : {n : Level } { x y : OD {suc n}} → x c<  y  → y c< x  →  ⊥
 c<> {n} {x} {y} x<y y<x with tri-c< x y
 c<> {n} {x} {y} x<y y<x | tri< a ¬b ¬c = ¬c y<x
 c<> {n} {x} {y} x<y y<x | tri≈ ¬a b ¬c = o<→o> b ( c<→o< x<y )
 lemma ox ne with is-o∅ ox
 lemma ox ne | yes refl with ne ( ord→== lemma1 ) where
 lemma1 : od→ord (ord→od o∅) ≡ od→ord od∅
 lemma1 = cong ( λ k → od→ord k ) o∅≡od∅
 lemma o∅ ne | yes refl | ()
-lemma ox ne | no ¬p = subst ( λ k → def (ord→od ox) (od→ord k) ) o∅≡od∅ (o<→c< (∅5 ¬p))
+lemma ox ne | no ¬p = subst ( λ k → def (ord→od ox) (od→ord k) ) o∅≡od∅ (o<→c< (subst (λ k → k o< ox ) (sym diso) (∅5 ¬p)) )
 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
 -- postulate f-extensionality : { n : Level}  → Relation.Binary.PropositionalEquality.Extensionality (suc n) (suc (suc n))
-Def : OD {suc n} → OD {suc n}
+Def :  {n : Level} →  OD {suc n} → OD {suc n}
-Def X = record { def = λ y → ∀ (x : Ordinal {suc n} ) → def X x → def (ord→od y) x  }
+Def {n} X = record { def = λ y → ∀ (x : Ordinal {suc n} ) → def X x → def (ord→od y) x  }
 OD→ZF : {n : Level} → ZF {suc (suc n)} {suc n}
 OD→ZF {n}  = record {
 ZFSet = OD {suc n}
 proj2 (pair A B ) = omax-y {n} (od→ord A) (od→ord B)
 empty : (x : OD {suc n} ) → ¬  (od∅ ∋ x)
 empty x ()
 --- Power X = record { def = λ t → ∀ (x : Ordinal {suc n} ) → def (ord→od t) x  →  def X x }
 power→ : (A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → A ∋ x
-power→ A t P∋t {x} t∋x = ?
+power→ A t P∋t {x} t∋x = {!!}
 power← : (A t : OD) → ({x : OD} → (t ∋ x → A ∋ x)) → Power A ∋ t
-power← A t t→A z _ = ?
+power← A t t→A z _ = {!!}
 union-u : (X z : OD {suc n}) → Union X ∋ z → OD {suc n}
 union-u X z U>z = ord→od ( osuc ( od→ord z ) )
 union-lemma-u : {X z : OD {suc n}} → (U>z : Union X ∋ z ) → union-u X z U>z  ∋ z
 union-lemma-u {X} {z} U>z = lemma <-osuc where
 lemma : {oz ooz : Ordinal {suc n}} → oz o< ooz → def (ord→od ooz) oz
-lemma {oz} {ooz} lt = def-subst {suc n} {ord→od  ooz} (o<→c< lt) refl diso
+lemma {oz} {ooz} lt = def-subst {suc n} {ord→od  ooz} (o<→c< lt) refl refl
 union→ :  (X z u : OD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z
 union→ X y u xx with trio< ( od→ord u ) ( osuc ( od→ord y ))
 union→ X y u xx | tri< a ¬b ¬c with  osuc-< a (c<→o< (proj2 xx))
 union→ X y u xx | tri< a ¬b ¬c | ()
 union→ X y u xx | tri≈ ¬a b ¬c = lemma b (c<→o< (proj1 xx )) where
 lemma : {oX ou ooy : Ordinal {suc n}} →  ou ≡ ooy  → ou o< oX   → ooy  o< oX
 lemma refl lt = lt
 union→ X y u xx | tri> ¬a ¬b c = ordtrans {suc n} {osuc ( od→ord y )} {od→ord u} {od→ord X} c ( c<→o< (proj1 xx ))
 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 X∋z = record { proj1 = def-subst {suc n} (o<→c< X∋z) oiso refl ; proj2 = union-lemma-u X∋z }
+union← X z X∋z = record { proj1 = def-subst {suc n} {_} {_} {X} {od→ord (union-u X z X∋z)} (o<→c< X∋z) oiso (sym diso) ; proj2 = union-lemma-u X∋z }
 ψiso :  {ψ : OD {suc n} → Set (suc n)} {x y : OD {suc n}} → ψ x → x ≡ y   → ψ y
 ψiso {ψ} t refl = t
 selection : {ψ : OD → Set (suc n)} {X y : OD} → ((X ∋ y) ∧ ψ y) ⇔ (Select X ψ ∋ y)
 selection {ψ} {X} {y} = record {
 proj1 = λ cond → record { proj1 = proj1 cond ; proj2 = ψiso {ψ} (proj2 cond) (sym oiso)  }
 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 ( omega )
 infinity∅ : ord→od ( omega ) ∋ od∅ {suc n}
-infinity∅ = def-subst {suc n} {_} {od→ord (ord→od o∅)} {infinite} {od→ord od∅}
+infinity∅ = def-subst {suc n} {_} {o∅} {infinite} {od→ord od∅}
-(o<→c< ( case1 (s≤s z≤n )))  refl (cong (λ k →  od→ord k) o∅≡od∅ )
+(o<→c< ( case1 (s≤s z≤n )))  refl (subst ( λ k → ( k ≡ od→ord od∅ )) diso (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 ))

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

comparison ordinal-definable.agda @ 95:f3da2c87cee0