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

comparison HOD.agda @ 150:ebcbfd9d9c8e

fix some

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Mon, 08 Jul 2019 22:37:10 +0900
parents	6e767ad3edc2
children	b5a337fb7a6d

comparison

equal deleted inserted replaced

-:6e767ad3edc2
+:ebcbfd9d9c8e
 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
 oiso   : {n : Level} {x : OD {n}}     → ord→od ( od→ord x ) ≡ x
 diso   : {n : Level} {x : Ordinal {n}} → od→ord ( ord→od x ) ≡ x
+-- we should prove this in agda, but simply put here
 ==→o≡ : {n : Level} →  { x y : OD {suc n} } → (x == y) → x ≡ y
 -- next assumption causes ∀ x ∋ ∅ . It menas only an ordinal becomes a set
 -- o<→c<  : {n : Level} {x y : Ordinal {n} } → x o< y             → def (ord→od y) x
 -- supermum as Replacement Axiom
 sup-o  : {n : Level } → ( Ordinal {n} → Ordinal {n}) →  Ordinal {n}
 -- sup-lb : {n : Level } → ( ψ : Ordinal {n} →  Ordinal {n}) → ( ∀ {x : Ordinal {n}} →  ψx  o<  z ) →  z o< osuc ( sup-o ψ )
 minimul : {n : Level } → (x : OD {suc n} ) → ¬ (x == od∅ )→ OD {suc n}
 -- this should be ¬ (x == od∅ )→ ∃ ox → x ∋ Ord ox  ( minimum of x )
 x∋minimul : {n : Level } → (x : OD {suc n} ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimul x ne ) )
 minimul-1 : {n : Level } → (x : OD {suc n} ) → ( ne : ¬ (x == od∅ ) ) → (y : OD {suc n}) → ¬ ( def (minimul x ne) (od→ord y)) ∧ (def x (od→ord  y) )
--- we should prove this in agda, but simply put here
-===-≡ : {n : Level} { x y : OD {suc n}} → x == y  → x ≡ y
 _∋_ : { 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
 ∋→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∅≡od∅ : {n : Level} → ord→od (o∅ {suc n}) ≡ od∅ {suc n}
+o∅≡od∅ : {n : Level} → ord→od (o∅ {suc n}) ≡ od∅ {suc n}
+o∅≡od∅ {n} = ==→o≡ lemma where
+lemma0 :  {x : Ordinal} → def (ord→od o∅) x → def od∅ x
+lemma0 {x} lt = o<-subst (c<→o< {suc n} {ord→od x} {ord→od o∅} (def-subst {suc n} {ord→od o∅} {x} lt refl (sym diso)) ) diso diso
+lemma1 :  {x : Ordinal} → def od∅ x → def (ord→od o∅) x
+lemma1 (case1 ())
+lemma1 (case2 ())
+lemma : ord→od o∅ == od∅
+lemma = record { eq→ = lemma0 ; eq← = lemma1 }
+ord-od∅ : {n : Level} → od→ord (od∅ {suc n}) ≡ o∅ {suc n}
+ord-od∅ {n} = sym ( subst (λ k → k ≡  od→ord (od∅ {suc n}) ) diso (cong ( λ k → od→ord k ) o∅≡od∅ ) )
 o<→¬c> : {n : Level} →  { x y : OD {n} } → (od→ord x ) o< ( od→ord y) →  ¬ (y c< x )
 o<→¬c> {n} {x} {y} olt clt = o<> olt (c<→o< clt ) where
 o≡→¬c< : {n : Level} →  { x y : OD {n} } →  (od→ord x ) ≡ ( od→ord y) →   ¬ x c< y
 Def :  {n : Level} → (A :  OD {suc n}) → OD {suc n}
 Def {n} A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) )
 OrdSubset : {n : Level} → (A x : Ordinal {suc n} ) → ZFSubset (Ord A) (Ord x) ≡ Ord ( minα A x )
-OrdSubset {n} A x = ===-≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where
+OrdSubset {n} A x = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where
 lemma1 :  {y : Ordinal} → def (ZFSubset (Ord A) (Ord x)) y → def (Ord (minα A x)) y
 lemma1 {y} s with trio< A x
 lemma1 {y} s | tri< a ¬b ¬c = proj1 s
 lemma1 {y} s | tri≈ ¬a refl ¬c = proj1 s
 lemma1 {y} s | tri> ¬a ¬b c = proj2 s
 ; proj2 = λ select → record { proj1 = proj1 select  ; proj2 =  ψiso {ψ} (proj2 select) oiso  }
 }
 replacement← : {ψ : OD → OD} (X x : OD) →  X ∋ x → Replace X ψ ∋ ψ x
 replacement← {ψ} X x lt = record { proj1 =  sup-c< ψ {x} ; proj2 = lemma } where
 lemma : def (in-codomain X ψ) (od→ord (ψ x))
-lemma not = ⊥-elim ( not ( od→ord x ) (record { proj1 = lt ; proj2 = cong (λ k → od→ord (ψ k))
+lemma not = ⊥-elim ( not ( od→ord x ) (record { proj1 = lt ; proj2 = cong (λ k → od→ord (ψ k)) (sym oiso)} ))
-{!!} } ))
 replacement→ : {ψ : OD → OD} (X x : OD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : OD) → ¬ (x == ψ y))
-replacement→ {ψ} X x lt = contra-position lemma (lemma2 {!!}) where
+replacement→ {ψ} X x lt = contra-position lemma (lemma2 (proj2 lt)) where
-lemma2 :  ¬ ((y : Ordinal) → ¬ def X y ∧ ((od→ord x) ≡ od→ord (ψ (Ord y))))
+lemma2 :  ¬ ((y : Ordinal) → ¬ def X y ∧ ((od→ord x) ≡ od→ord (ψ (ord→od y))))
-→ ¬ ((y : Ordinal) → ¬ def X y ∧ (ord→od (od→ord x) == ψ (Ord y)))
+→ ¬ ((y : Ordinal) → ¬ def X y ∧ (ord→od (od→ord x) == ψ (ord→od y)))
 lemma2 not not2  = not ( λ y d →  not2 y (record { proj1 = proj1 d ; proj2 = lemma3 (proj2 d)})) where
-lemma3 : {y : Ordinal } → (od→ord x ≡ od→ord (ψ (Ord y))) → (ord→od (od→ord x) == ψ (Ord y))
+lemma3 : {y : Ordinal } → (od→ord x ≡ od→ord (ψ (ord→od  y))) → (ord→od (od→ord x) == ψ (ord→od y))
 lemma3 {y} eq = subst (λ k  → ord→od (od→ord x) == k ) oiso (o≡→== eq )
-lemma :  ( (y : OD) → ¬ (x == ψ y)) → ( (y : Ordinal) → ¬ def X y ∧ (ord→od (od→ord x) == ψ (Ord y)) )
+lemma :  ( (y : OD) → ¬ (x == ψ y)) → ( (y : Ordinal) → ¬ def X y ∧ (ord→od (od→ord x) == ψ (ord→od y)) )
-lemma not y not2 = not (Ord y) (subst (λ k → k == ψ (Ord y)) oiso  ( proj2 not2 ))
+lemma not y not2 = not (ord→od y) (subst (λ k → k == ψ (ord→od y)) oiso  ( proj2 not2 ))
 ---
 --- Power Set
 ---
 ---    First consider ordinals in OD
 eq← lemma-eq {z} w = record { proj2 = w  ;
 proj1 = def-subst {suc n} {_} {_} {(Ord a)} {z}
 ( t→A (def-subst {suc n} {_} {_} {t} {od→ord (ord→od z)} w refl (sym diso) )) refl diso  }
 lemma1 : {n : Level } {a : Ordinal {suc n}} { t : OD {suc n}}
 → (eq : ZFSubset (Ord a) t == t)  → od→ord (ZFSubset (Ord a) (ord→od (od→ord t))) ≡ od→ord t
-lemma1 {n} {a} {t} eq = subst (λ k → od→ord (ZFSubset (Ord a) k) ≡ od→ord t ) (sym oiso) (cong (λ k → od→ord k ) (===-≡ eq ))
+lemma1 {n} {a} {t} eq = subst (λ k → od→ord (ZFSubset (Ord a) k) ≡ od→ord t ) (sym oiso) (cong (λ k → od→ord k ) (==→o≡ eq ))
 lemma :  od→ord (ZFSubset (Ord a) (ord→od (od→ord t)) ) o< sup-o (λ x → od→ord (ZFSubset (Ord a) (ord→od x)))
 lemma = sup-o<
 --
 -- Every set in OD is a subset of Ordinals
 lemma0 : {x : OD} → t ∋ x → Ord a ∋ x
 lemma0 {x} t∋x = c<→o< (t→A t∋x)
 lemma3 : Def (Ord a) ∋ t
 lemma3 = ord-power← a t lemma0
 lemma4 : od→ord t ≡ od→ord (A ∩ Ord (od→ord t))
-lemma4 = cong ( λ k → od→ord k ) ( ===-≡ (subst (λ k → t == (A ∩ k)) {!!} {!!} ))
+lemma4 = cong ( λ k → od→ord k ) ( ==→o≡ (subst (λ k → t == (A ∩ k)) {!!} {!!} ))
 lemma1 : od→ord t o< sup-o (λ x → od→ord (A ∩ ord→od x))
 lemma1 with sup-o< {suc n} {λ x → od→ord (A ∩ ord→od x)} {od→ord t}
 ... | lt = o<-subst {suc n} {_} {_} {_} {_} lt (sym (subst (λ k → od→ord t ≡ k) lemma5 lemma4 )) refl where
 lemma5 : od→ord (A ∩ Ord (od→ord t)) ≡ od→ord (A ∩ ord→od (od→ord t))
 lemma5 = cong (λ k → od→ord (A ∩ k )) {!!}
 osuc y o< osuc (osuc (od→ord x))
 ∎
 infinite : OD {suc n}
 infinite = Ord omega
 infinity∅ : Ord omega  ∋ od∅ {suc n}
-infinity∅ = o<-subst (case1 (s≤s z≤n) ) {!!} refl
+infinity∅ = o<-subst (case1 (s≤s z≤n) ) (sym ord-od∅) refl
 infinity : (x : OD) → infinite ∋ x → infinite ∋ Union (x , (x , x ))
 infinity x lt = o<-subst ( lemma (od→ord x) lt ) eq refl where
 eq :  osuc (od→ord x) ≡ od→ord (Union (x , (x , x)))
 eq = let open ≡-Reasoning in begin
 osuc (od→ord x)

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

comparison HOD.agda @ 150:ebcbfd9d9c8e