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

changeset 123:0c2cbf37e002

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 30 Jun 2019 20:31:10 +0900
parents 4d2434513228
children 55c6e1ddc739
files HOD.agda ordinal-definable.agda zf.agda
diffstat 3 files changed, 31 insertions(+), 23 deletions(-) [+]
line wrap: on
line diff
--- a/HOD.agda	Sun Jun 30 11:03:34 2019 +0900
+++ b/HOD.agda	Sun Jun 30 20:31:10 2019 +0900
@@ -78,6 +78,11 @@
   -- this should be ¬ (x == od∅ )→ ∃ ox → x ∋ Ord ox  ( minimum of x )
   x∋minimul : {n : Level } → (x : HOD {suc n} ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimul x ne ) )
   minimul-1 : {n : Level } → (x : HOD {suc n} ) → ( ne : ¬ (x == od∅ ) ) → (y : HOD {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 : HOD {suc n}} → x == y  → x ≡ y
+
+Ord-ord : {n : Level } {ox : Ordinal {suc n}} → Ord ox ≡ ord→od ox
+Ord-ord {n} {px} = trans (sym oiso) (cong ( λ k → ord→od k ) (sym ord-Ord)) 
 
 _∋_ : { n : Level } → ( a x : HOD {n} ) → Set n
 _∋_ {n} a x  = def a ( od→ord x )
@@ -108,6 +113,21 @@
     lemma : od→ord (ψ (ord→od (od→ord x))) o< sup-o (λ x → od→ord (ψ (ord→od x)))
     lemma = subst₂ (λ j k → j o< k ) refl diso (o<-subst sup-o< refl (sym diso)  )
 
+o<→o> : {n : Level} →  { x y : Ordinal {n} } →  (Ord x == Ord y) → x o< y → ⊥
+o<→o> {n} {x} {y} record { eq→ = xy ; eq← = yx } (case1 lt) with o<-subst (yx (case1 lt)) ord-Ord refl
+... | oyx with o<¬≡ refl (c<→o< {n} {Ord x} oyx )
+... | ()
+o<→o> {n} {x} {y} record { eq→ = xy ; eq← = yx } (case2 lt) with  o<-subst (yx (case2 lt)) ord-Ord refl
+... | oyx with o<¬≡ refl (c<→o< {n} {Ord x} oyx )
+... | ()
+
+Ord==→≡ : {n : Level} { x y : Ordinal {suc n}} → Ord x == Ord y → x ≡ y
+Ord==→≡ {n} {x} {y} eq with trio< x y
+Ord==→≡ {n} {x} {y} eq | tri< a ¬b ¬c = ⊥-elim ( o<→o> eq a )
+Ord==→≡ {n} {x} {y} eq | tri≈ ¬a b ¬c = b
+Ord==→≡ {n} {x} {y} eq | tri> ¬a ¬b c = ⊥-elim ( o<→o> (eq-sym eq) c )
+
+
 ∅3 : {n : Level} →  { x : Ordinal {n}}  → ( ∀(y : Ordinal {n}) → ¬ (y o< x ) ) → x ≡ o∅ {n}
 ∅3 {n} {x} = TransFinite {n} c2 c3 x where
    c0 : Nat →  Ordinal {n}  → Set n
@@ -234,29 +254,16 @@
 L {n}  record { lv = (Suc lx) ; ord = (Φ (Suc lx)) } = -- Union ( L α )
     cseq ( Ord (od→ord (L {n}  (record { lv = lx ; ord = Φ lx }))))
 
-LS :  {n : Level} → {la : Nat } → {oa : OrdinalD {suc n} la }
-        → L {n} (record { lv = la; ord = OSuc la oa })  ∋ L {n} (record { lv = la; ord = oa })
-LS {n} {la} {oa} = {!!} where
+L00 :   {n : Level} → (ox : Ordinal {suc n}) → ox o<  sup-o ( λ x → od→ord ( ZFSubset (Ord ox) (ord→od x )))
+L00 {n} ox =  o<-subst {suc n} {_} {_} {ox} {sup-o ( λ x → od→ord ( ZFSubset (Ord ox) (ord→od x )))}
+  (sup-o< {suc n} {λ x → od→ord ( ZFSubset (Ord ox) (ord→od x ))} {ox} ) (lemma0 ox) refl where
+      lemma1 : {n : Level } {ox z : Ordinal {suc n}} → ( def (Ord ox) z ∧ def (ord→od ox) z ) ⇔ def ( Ord ox ) z
+      lemma1 {n} {ox} {z} = record { proj1 = proj1 ; proj2 = λ t → record { proj1 = t ; proj2 = subst (λ k → def k z ) Ord-ord t }}
       lemma0 :  {n : Level} → (ox : Ordinal {suc n}) →  od→ord (ZFSubset (Ord ox) (ord→od ox)) ≡ ox
-      lemma0 = {!!}
-      lemma :   {n : Level} → (ox : Ordinal {suc n}) → ox o<  sup-o ( λ x → od→ord ( ZFSubset (Ord ox) (ord→od x )))
-      lemma {n} ox =  o<-subst {suc n} {_} {_} {ox} {sup-o ( λ x → od→ord ( ZFSubset (Ord ox) (ord→od x )))}
-          (sup-o< {suc n} {λ x → od→ord ( ZFSubset (Ord ox) (ord→od x ))} {ox} ) (lemma0 ox) refl
+      lemma0 {n} ox = trans (cong (λ k → od→ord k) (===-≡ (⇔→== lemma1) )) (sym ord-Ord)
 
-L0 :  {n : Level} → {la : Nat } → {oa : OrdinalD {suc n} (Suc la) }{ob : OrdinalD {suc n} la }
-   → L (record { lv = Suc la; ord = oa })  ∋ L (record { lv = la; ord = ob })
-L0 = {!!}
-
-L1 :  {n : Level} → (α β : Ordinal {suc n}) → α o< β → ∀ (x : HOD {suc n})  → L α ∋ x → L β ∋ x 
-L1 {n} record { lv = .0 ; ord = (Φ .0) } record { lv = .(Suc _) ; ord = ord₁ } (case1 (s≤s z≤n)) x (case1 ())
-L1 {n} record { lv = .0 ; ord = (Φ .0) } record { lv = .(Suc _) ; ord = ord₁ } (case1 (s≤s z≤n)) x (case2 ())
-L1 {n} record { lv = .0 ; ord = (OSuc .0 ord₂) } record { lv = (Suc lx) ; ord = ord₁ } (case1 (s≤s z≤n)) x α∋x = lemma α∋x where
-   lemma : (od→ord x) o< (sup-o (λ x₁ → od→ord (ZFSubset (L (record { lv = 0 ; ord = ord₂ })) (ord→od x₁))))
-       → L (record { lv = Suc lx ; ord = ord₁ }) ∋ x
-   lemma lt = {!!}
-L1 {n} record { lv = (Suc _) ; ord = ord₂ } record { lv = (Suc (Suc _)) ; ord = ord₁ } (case1 (s≤s (s≤s x₁))) x α∋x = {!!}
-L1 {n} record { lv = lx ; ord = (Φ lx) } record { lv = lx ; ord = (OSuc lx _) } (case2 Φ<) x α∋x = {!!}
-L1 {n} record { lv = lx ; ord = (OSuc lx _) } record { lv = lx ; ord = (OSuc lx _) } (case2 (s< x₁)) x α∋x = {!!}
+-- L0 :  {n : Level} → (α : Ordinal {suc n}) → α o< β → L (osuc α) ∋ L α
+-- L1 :  {n : Level} → (α β : Ordinal {suc n}) → α o< β → ∀ (x : HOD {suc n})  → L α ∋ x → L β ∋ x 
 
 omega : { n : Level } → Ordinal {n}
 omega = record { lv = Suc Zero ; ord = Φ 1 }
--- a/ordinal-definable.agda	Sun Jun 30 11:03:34 2019 +0900
+++ b/ordinal-definable.agda	Sun Jun 30 20:31:10 2019 +0900
@@ -276,7 +276,7 @@
 -- postulate f-extensionality : { n : Level}  → Relation.Binary.PropositionalEquality.Extensionality (suc n) (suc (suc n))
 
 csuc :  {n : Level} →  OD {suc n} → OD {suc n}
-csuc x = ord→od ( osuc ( od→ord x ))
+csuc x = Ord ( osuc ( od→ord x ))
 
 -- Power Set of X ( or constructible by λ y → def X (od→ord y )
 
@@ -284,7 +284,7 @@
 ZFSubset A x =  record { def = λ y → def A y ∧  def x y }  
 
 Def :  {n : Level} → (A :  OD {suc n}) → OD {suc n}
-Def {n} A = ord→od ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) )  
+Def {n} A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) )  
 
 -- Constructible Set on α
 L : {n : Level} → (α : Ordinal {suc n}) → OD {suc n}
--- a/zf.agda	Sun Jun 30 11:03:34 2019 +0900
+++ b/zf.agda	Sun Jun 30 20:31:10 2019 +0900
@@ -18,6 +18,7 @@
 _⇔_ : {n m : Level } → ( A : Set n ) ( B : Set m )  → Set (n ⊔ m)
 _⇔_ A B =  ( A → B ) ∧ ( B → A )
 
+
 open import Relation.Nullary
 open import Relation.Binary