Members/kono/Proof/ZF-in-agda: OD.agda comparison

comparison OD.agda @ 396:8c092c042093

...

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Mon, 27 Jul 2020 15:11:54 +0900
parents	77c6123f49ee
children	382a4a411aff

comparison

equal deleted inserted replaced

-:77c6123f49ee
+:8c092c042093
 od∅  = Ord o∅
 odef : HOD → Ordinal → Set n
 odef A x = def ( od A ) x
+_∋_ : ( a x : HOD  ) → Set n
+_∋_  a x  = odef a ( od→ord x )
+_c<_ : ( x a : HOD  ) → Set n
+x c< a = a ∋ x
+d→∋ : ( a : HOD  ) { x : Ordinal} → odef a x → a ∋ (ord→od x)
+d→∋ a lt = subst (λ k → odef a k ) (sym diso) lt
+cseq :  HOD  →  HOD
+cseq x = record { od = record { def = λ y → odef x (osuc y) } ; odmax = osuc (odmax x) ; <odmax = lemma } where
+lemma : {y : Ordinal} → def (od x) (osuc y) → y o< osuc (odmax x)
+lemma {y} lt = ordtrans <-osuc (ordtrans (<odmax x lt) <-osuc )
+odef-subst :  {Z : HOD } {X : Ordinal  }{z : HOD } {x : Ordinal  }→ odef Z X → Z ≡ z  →  X ≡ x  →  odef z x
+odef-subst df refl refl = df
+otrans : {a x y : Ordinal  } → odef (Ord a) x → odef (Ord x) y → odef (Ord a) y
+otrans x<a y<x = ordtrans y<x x<a
+odef→o< :  {X : HOD } → {x : Ordinal } → odef X x → x o< od→ord X
+odef→o<  {X} {x} lt = o<-subst  {_} {_} {x} {od→ord X} ( c<→o< ( odef-subst  {X} {x}  lt (sym oiso) (sym diso) )) diso diso
+odefo→o< :  {X y : Ordinal } → odef (ord→od X) y → y o< X
+odefo→o< {X} {y} lt = subst₂ (λ j k → j o< k ) diso diso ( c<→o< (subst (λ k → odef (ord→od X) k ) (sym diso ) lt ))
 -- If we have reverse of c<→o<, everything becomes Ordinal
 o<→c<→HOD=Ord : ( o<→c< : {x y : Ordinal  } → x o< y → odef (ord→od y) x ) → {x : HOD } →  x ≡ Ord (od→ord x)
 o<→c<→HOD=Ord o<→c< {x} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where
 lemma1 : {y : Ordinal} → odef x y → odef (Ord (od→ord x)) y
-lemma1 {y} lt = subst ( λ k → k o< od→ord x ) diso (c<→o< {ord→od y} {x} (subst (λ k → odef x k ) (sym diso) lt))
+lemma1 {y} lt = subst ( λ k → k o< od→ord x ) diso (c<→o< {ord→od y} {x} (d→∋ x lt))
 lemma2 : {y : Ordinal} → odef (Ord (od→ord x)) y → odef x y
 lemma2 {y} lt = subst (λ k → odef k y ) oiso (o<→c< {y} {od→ord x} lt )
-_∋_ : ( a x : HOD  ) → Set n
-_∋_  a x  = odef a ( od→ord x )
-_c<_ : ( x a : HOD  ) → Set n
-x c< a = a ∋ x
-cseq :  HOD  →  HOD
-cseq x = record { od = record { def = λ y → odef x (osuc y) } ; odmax = osuc (odmax x) ; <odmax = lemma } where
-lemma : {y : Ordinal} → def (od x) (osuc y) → y o< osuc (odmax x)
-lemma {y} lt = ordtrans <-osuc (ordtrans (<odmax x lt) <-osuc )
-odef-subst :  {Z : HOD } {X : Ordinal  }{z : HOD } {x : Ordinal  }→ odef Z X → Z ≡ z  →  X ≡ x  →  odef z x
-odef-subst df refl refl = df
-otrans : {a x y : Ordinal  } → odef (Ord a) x → odef (Ord x) y → odef (Ord a) y
-otrans x<a y<x = ordtrans y<x x<a
-odef→o< :  {X : HOD } → {x : Ordinal } → odef X x → x o< od→ord X
-odef→o<  {X} {x} lt = o<-subst  {_} {_} {x} {od→ord X} ( c<→o< ( odef-subst  {X} {x}  lt (sym oiso) (sym diso) )) diso diso
-odefo→o< :  {X y : Ordinal } → odef (ord→od X) y → y o< X
-odefo→o< {X} {y} lt = subst₂ (λ j k → j o< k ) diso diso ( c<→o< (subst (λ k → odef (ord→od X) k ) (sym diso ) lt ))
 -- avoiding lv != Zero error
 orefl : { x : HOD  } → { y : Ordinal  } → od→ord x ≡ y → od→ord x ≡ y
 orefl refl = refl
 -- another possible restriction. We reqest no minimality on odmax, so it may arbitrary larger.
 odmax<od→ord  : { x y : HOD } → x ∋ y →  Set n
 odmax<od→ord {x} {y} x∋y = odmax x o< od→ord x
--- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
 -- postulate f-extensionality : { n : Level}  → Relation.Binary.PropositionalEquality.Extensionality n (suc n)
 in-codomain : (X : HOD  ) → ( ψ : HOD  → HOD  ) → OD
 in-codomain  X ψ = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( odef X y ∧  ( x ≡ od→ord (ψ (ord→od y )))))  }
 refl-⊆ : {A : HOD} → A ⊆ A
 refl-⊆ {A} = record { incl = λ x → x }
 od⊆→o≤  : {x y : HOD } → x ⊆ y → od→ord x o< osuc (od→ord y)
-od⊆→o≤ {x} {y} lt  =  ⊆→o≤ {x} {y} (λ {z} x>z  → subst (λ k → def (od y) k ) diso (incl lt (subst (λ k → def (od x) k ) (sym diso) x>z )))
+od⊆→o≤ {x} {y} lt  =  ⊆→o≤ {x} {y} (λ {z} x>z  → subst (λ k → def (od y) k ) diso (incl lt (d→∋ x x>z)))
 -- if we have od→ord (x , x) ≡ osuc (od→ord x),  ⊆→o≤ → c<→o<
 ⊆→o≤→c<→o< : ({x : HOD} → od→ord (x , x) ≡ osuc (od→ord x) )
 →  ({y z : HOD  }   → ({x : Ordinal} → def (od y) x → def (od z) x ) → od→ord y o< osuc (od→ord z) )
 →   {x y : HOD  }   → def (od y) ( od→ord x ) → od→ord x o< od→ord y
 }
 power< : {A x : HOD  } → x ⊆ A → Ord (osuc (od→ord A)) ∋ x
 power< {A} {x} x⊆A = ⊆→o≤  (λ {y} x∋y → subst (λ k →  def (od A) k) diso (lemma y x∋y ) ) where
 lemma : (y : Ordinal) → def (od x) y → def (od A) (od→ord (ord→od y))
-lemma y x∋y = incl x⊆A (subst (λ k → def (od x) k ) (sym diso) x∋y )
+lemma y x∋y = incl x⊆A (d→∋ x x∋y)
 open import Data.Unit
 ε-induction : { ψ : HOD  → Set n}
 → ( {x : HOD } → ({ y : HOD } →  x ∋ y → ψ y ) → ψ x )
 rmax : Ordinal
 rmax = sup-o X (λ y X∋y → od→ord (ψ (ord→od y)))
 rmax< :  {y : Ordinal} → (y o< rmax) ∧ def (in-codomain X ψ) y → y o< rmax
 rmax< lt = proj1 lt
-d→∋ : ( a : HOD  ) { x : Ordinal} → odef a x → a ∋ (ord→od x)
-d→∋ a lt = subst (λ k → odef a k ) (sym diso) lt
 --
 -- If we have LEM, Replace' is equivalent to Replace
 --
 in-codomain' : (X : HOD  ) → ((x : HOD) → X ∋ x → HOD) → OD
 in-codomain'  X ψ = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( odef X y ∧  ((lt : odef X y) →  x ≡ od→ord (ψ (ord→od y ) (d→∋ X lt) ))))  }
 Union U = record { od = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((odef U u) ∧ (odef (ord→od u) x)))  }
 ; odmax = osuc (od→ord U) ; <odmax = umax< } where
 umax< :  {y : Ordinal} → ¬ ((u : Ordinal) → ¬ def (od U) u ∧ def (od (ord→od u)) y) → y o< osuc (od→ord U)
 umax< {y} not = lemma (FExists _ lemma1 not ) where
 lemma0 : {x : Ordinal} → def (od (ord→od x)) y → y o< x
-lemma0 {x} x<y = subst₂ (λ j k → j o< k ) diso  diso (c<→o< (subst (λ k → def (od (ord→od x)) k) (sym diso) x<y))
+lemma0 {x} x<y = subst₂ (λ j k → j o< k ) diso  diso (c<→o< (d→∋ (ord→od x) x<y ))
 lemma2 : {x : Ordinal} → def (od U) x → x o< od→ord U
-lemma2 {x} x<U = subst (λ k → k o< od→ord U ) diso (c<→o< (subst (λ k → def (od U) k) (sym diso) x<U))
+lemma2 {x} x<U = subst (λ k → k o< od→ord U ) diso (c<→o< (d→∋ U x<U))
 lemma1 : {x : Ordinal} → def (od U) x ∧ def (od (ord→od x)) y → ¬ (od→ord U o< y)
 lemma1 {x} lt u<y = o<> u<y (ordtrans (lemma0 (proj2 lt)) (lemma2 (proj1 lt)) )
 lemma : ¬ ((od→ord U) o< y ) → y o< osuc (od→ord U)
 lemma not with trio< y (od→ord U)
 lemma not | tri< a ¬b ¬c = ordtrans a <-osuc
 lemma = subst (λ k → od→ord (Union (k , ( k , k ))) ≡ od→ord (nat→ω (Suc n))) (sym oiso) refl
 _=h=_ : (x y : HOD) → Set n
 x =h= y  = od x == od y
+open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
+ord∋eq : {n : Level } {A i : HOD } → { f : (x : HOD ) → A ∋ x → Set n}
+→ ( ( x : Ordinal ) → ( lx : odef A x ) → f (ord→od x) (d→∋ A lx) )
+→ ( lt : A ∋ i ) → f i lt
+ord∋eq {n} {A} {i} {f} of lt = subst (λ k → odef A k ) ?  (of (od→ord i) ?)
+nat→ω-iso : {i : HOD} → (lt : infinite ∋ i ) → nat→ω ( ω→nat i lt ) ≡ i
+nat→ω-iso  {i} lt = ord∋eq {_} {infinite} {i} (λ x lx → lemma lx ) lt where
+lemma : {x : Ordinal} → (lx : infinite-d x ) → nat→ω ( ω→nat (ord→od x) (d→∋ infinite lx) ) ≡ ord→od x
+lemma = {!!}
 infixr  200 _∈_
 -- infixr  230 _∩_ _∪_
 pair→ : ( x y t : HOD  ) →  (x , y)  ∋ t  → ( t =h= x ) ∨ ( t =h= y )
 pair→ x y t (case1 t≡x ) = case1 (subst₂ (λ j k → j =h= k ) oiso oiso (o≡→== t≡x ))
 union→ X z u xx not = ⊥-elim ( not (od→ord u) ( record { proj1 = proj1 xx
 ; proj2 = subst ( λ k → odef k (od→ord z)) (sym oiso) (proj2 xx) } ))
 union← :  (X z : HOD) (X∋z : Union X ∋ z) →  ¬  ( (u : HOD ) → ¬ ((X ∋  u) ∧ (u ∋ z )))
 union← X z UX∋z =  FExists _ lemma UX∋z where
 lemma : {y : Ordinal} → odef X y ∧ odef (ord→od y) (od→ord z) → ¬ ((u : HOD) → ¬ (X ∋ u) ∧ (u ∋ z))
-lemma {y} xx not = not (ord→od y) record { proj1 = subst ( λ k → odef X k ) (sym diso) (proj1 xx ) ; proj2 = proj2 xx }
+lemma {y} xx not = not (ord→od y) record { proj1 = d→∋ X (proj1 xx) ; proj2 = proj2 xx }
 ψiso :  {ψ : HOD  → Set n} {x y : HOD } → ψ x → x ≡ y   → ψ y
 ψiso {ψ} t refl = t
 selection : {ψ : HOD → Set n} {X y : HOD} → ((X ∋ y) ∧ ψ y) ⇔ (Select X ψ ∋ y)
 selection {ψ} {X} {y} = record {
 --
 --
 ∩-≡ :  { a b : HOD  } → ({x : HOD  } → (a ∋ x → b ∋ x)) → a =h= ( b ∩ a )
 ∩-≡ {a} {b} inc = record {
 eq→ = λ {x} x<a → record { proj2 = x<a ;
-proj1 = odef-subst  {_} {_} {b} {x} (inc (odef-subst  {_} {_} {a} {_} x<a refl (sym diso) )) refl diso  } ;
+proj1 = odef-subst  {_} {_} {b} {x} (inc (d→∋ a x<a)) refl diso  } ;
 eq← = λ {x} x<a∩b → proj2 x<a∩b }
 --
 -- Transitive Set case
 -- we have t ∋ x → Ord a ∋ x means t is a subset of Ord a, that is (Ord a) ∩ t =h= t
 -- OPwr (Ord a) is a sup of (Ord a) ∩ t, so OPwr (Ord a) ∋ t
 lemma refl (lemma1 lemma-eq )where
 lemma-eq :  ((Ord a) ∩ t) =h= t
 eq→ lemma-eq {z} w = proj2 w
 eq← lemma-eq {z} w = record { proj2 = w  ;
 proj1 = odef-subst  {_} {_} {(Ord a)} {z}
-( t→A (odef-subst  {_} {_} {t} {od→ord (ord→od z)} w refl (sym diso) )) refl diso  }
+( t→A (d→∋ t w)) refl diso  }
 lemma1 :  {a : Ordinal } { t : HOD }
 → (eq : ((Ord a) ∩ t) =h= t)  → od→ord ((Ord a) ∩ (ord→od (od→ord t))) ≡ od→ord t
 lemma1  {a} {t} eq = subst (λ k → od→ord ((Ord a) ∩ k) ≡ od→ord t ) (sym oiso) (cong (λ k → od→ord k ) (==→o≡ eq ))
 lemma2 : (od→ord t) o< (osuc (od→ord (Ord a)))
-lemma2 = ⊆→o≤  {t} {Ord a} (λ {x} x<t → subst (λ k → def (od (Ord a)) k) diso (t→A (subst (λ k → def (od t) k) (sym diso) x<t)))
+lemma2 = ⊆→o≤  {t} {Ord a} (λ {x} x<t → subst (λ k → def (od (Ord a)) k) diso (t→A (d→∋ t x<t)))
 lemma :  od→ord ((Ord a) ∩ (ord→od (od→ord t)) ) o< sup-o (Ord (osuc (od→ord (Ord a)))) (λ x lt → od→ord ((Ord a) ∩ (ord→od x)))
 lemma = sup-o< _ lemma2
 --
 -- Every set in HOD is a subset of Ordinals, so make OPwr (Ord (od→ord A)) first
 lemma9 : def (od (Ord (Ordinals.osuc O (od→ord (Ord (od→ord A)))))) (od→ord (Ord (od→ord A)))
 lemma9 = <-osuc
 lemmab : od→ord ((Ord (od→ord A)) ∩ (ord→od (od→ord (Ord (od→ord A) )))) o< sup1
 lemmab = sup-o< (Ord (osuc (od→ord (Ord (od→ord A))))) lemma9
 lemmad : Ord (osuc (od→ord A)) ∋ t
-lemmad = ⊆→o≤ (λ {x} lt → subst (λ k → def (od A) k ) diso (t→A (subst (λ k → def (od t) k ) (sym diso) lt)))
+lemmad = ⊆→o≤ (λ {x} lt → subst (λ k → def (od A) k ) diso (t→A (d→∋ t lt)))
 lemmac : ((Ord (od→ord A)) ∩  (ord→od (od→ord (Ord (od→ord A) )))) =h= Ord (od→ord A)
 lemmac = record { eq→ = lemmaf ; eq← = lemmag } where
 lemmaf : {x : Ordinal} → def (od ((Ord (od→ord A)) ∩  (ord→od (od→ord (Ord (od→ord A)))))) x → def (od (Ord (od→ord A))) x
 lemmaf {x} lt = proj1 lt
 lemmag :  {x : Ordinal} → def (od (Ord (od→ord A))) x → def (od ((Ord (od→ord A)) ∩ (ord→od (od→ord (Ord (od→ord A)))))) x

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

comparison OD.agda @ 396:8c092c042093