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

changeset 84:4b2aff372b7c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
omax ..
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 04 Jun 2019 23:58:58 +0900
parents e013ccf00567
children 7494ae6b83c6
files ordinal-definable.agda ordinal.agda
diffstat 2 files changed, 45 insertions(+), 28 deletions(-) [+]
line wrap: on
line diff
--- a/ordinal-definable.agda	Tue Jun 04 12:28:43 2019 +0900
+++ b/ordinal-definable.agda	Tue Jun 04 23:58:58 2019 +0900
@@ -254,7 +254,7 @@
     Select : OD {suc n} → (OD {suc n} → Set (suc n) ) → OD {suc n}
     Select X ψ = record { def = λ x →  ( def X  x ∧  ψ ( ord→od x )) } 
     _,_ : OD {suc n} → OD {suc n} → OD {suc n}
-    x , y = record { def = λ z → ( (z ≡ od→ord x ) ∨ ( z ≡ od→ord y )) }
+    x , y = record { def = λ z → z o< (omax (od→ord x) (od→ord y)) }
     Union : OD {suc n} → OD {suc n}
     Union U = record { def = λ y → osuc y o< (od→ord U) }
     -- power : ∀ X ∃ A ∀ t ( t ∈ A ↔ ( ∀ {x} → t ∋ x →  X ∋ x )
@@ -293,8 +293,8 @@
          open _∧_ 
          open Minimumo
          pair : (A B : OD {suc n} ) → ((A , B) ∋ A) ∧  ((A , B) ∋ B)
-         proj1 (pair A B ) =  case1 refl 
-         proj2 (pair A B ) =  case2 refl 
+         proj1 (pair A B ) = omax-x {n} {od→ord A} {od→ord B}
+         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 = λ y → ∀ (x : Ordinal {suc n} ) → ( def X x ∧ def (ord→od y) x )  }
@@ -343,29 +343,20 @@
          extensionality : {A B : OD {suc n}} → ((z : OD) → (A ∋ z) ⇔ (B ∋ z)) → A == B
          eq→ (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {A} {B} (sym diso) (proj1 (eq (ord→od x))) d  
          eq← (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {B} {A} (sym diso) (proj2 (eq (ord→od x))) d  
-         pair-or : {x y : OD {suc n} } → (x , x) ∋ y → (y == x ) ∨ (x ∋ y )
-         pair-or {x} {y} lt with tri-c< x y
-         pair-or {x} {y} lt | tri< a ¬b ¬c = {!!}   --     x < y < ( x ,  x )
-         pair-or {x} {y} lt | tri≈ ¬a b ¬c = case1 (eq-sym b)
-         pair-or {x} {y} lt | tri> ¬a ¬b c = case2 c
-         pair-osuc : (x : OD) →  od→ord (x , x) ≡ osuc (od→ord x)
-         pair-osuc x with trio< (od→ord (x , x)) (osuc (od→ord x))
-         pair-osuc x | tri< a ¬b ¬c = ⊥-elim ( osuc-<  a (c<→o< (proj1 (pair x x )) ))
-         pair-osuc x | tri≈ ¬a b ¬c = b
-         pair-osuc x | tri> ¬a ¬b c with pair-or (def-subst (o<→c<  c ) oiso refl ) --  (x , x)  ∋ ord→od (osuc (od→ord x) )
-         pair-osuc x | tri> ¬a ¬b c | case1 eq = ⊥-elim ( o<→¬== (def-subst {suc n} (o<→c<  c ) refl diso ) eq )
-         pair-osuc x | tri> ¬a ¬b c | case2 lt = ⊥-elim (c<> c lt ) where
-             lemma2 : (z : Ordinal {suc n} ) → lv (od→ord (ord→od z , ord→od z) ) ≡ lv z
-             lemma2 z = {!!}
+         pair-osuc : {x y : OD {suc n}} →  (x , x)  ∋ y →  (od→ord y ) o< osuc (od→ord x) 
+         pair-osuc {x} {y} z with union← (x , x) y z
+         ... | t = {!!}
          next : (x : OD) → Union (x , (x , x)) == ord→od (osuc (od→ord x))
-         eq→ (next x ) {y} z = {!!}
+         eq→ (next x ) {y} z = {!!}       --   z : y o< osuc (osuc ox ) → y < osuc ox
          eq← (next x ) {y} z = def-subst {suc n} {_} {_} {Union (x , (x , x))} {_}
                   (union→ (x , (x , x)) (ord→od y) (ord→od (osuc y)) (record { proj1 = lemma1 ; proj2 = lemma2 } )) refl diso where
+             lemma0 :  (x , x) ∋ ord→od y 
+             lemma0 = o<-subst {suc n} {od→ord (ord→od y)} {od→ord {!!}} (c<→o< z) {!!} {!!}
              lemma1 : (x , (x , x)) ∋ ord→od (osuc y)    -- z : def (ord→od (osuc (od→ord x))) y
-             lemma1 with tri-c< (x , x) (ord→od (osuc (od→ord x)))
-             lemma1 | tri< a ¬b ¬c = {!!}
-             lemma1 | tri≈ ¬a b ¬c = {!!}
-             lemma1 | tri> ¬a ¬b c = {!!}
+             lemma1 with osuc-≡< {suc n} (def-subst {suc n} (o<→c< z) oiso refl)
+             lemma1 | case1 x = {!!}
+             lemma1 | case2 t = {!!}
+             -- = o<-subst (c<→o< {suc n} {_} {ord→od y} {!!} ) {!!} {!!}
              lemma2 : ord→od (osuc y) ∋ ord→od y
              lemma2 = o<→c< <-osuc
          next' : (x : OD) →  ord→od ( od→ord ( Union (x , (x , x)))) == ord→od (osuc (od→ord x))
--- a/ordinal.agda	Tue Jun 04 12:28:43 2019 +0900
+++ b/ordinal.agda	Tue Jun 04 23:58:58 2019 +0900
@@ -153,12 +153,6 @@
 maxαd x y | tri≈ ¬a b ¬c = x
 maxαd x y | tri> ¬a ¬b c = x
 
-maxα : {n : Level} →  Ordinal {n} →  Ordinal  → Ordinal
-maxα x y with <-cmp (lv x) (lv y)
-maxα x y | tri< a ¬b ¬c = x
-maxα x y | tri> ¬a ¬b c = y
-maxα x y | tri≈ ¬a refl ¬c = record { lv = lv x ; ord = maxαd (ord x) (ord y) }
-
 _o≤_ : {n : Level} → Ordinal → Ordinal → Set (suc n)
 a o≤ b  = (a ≡ b)  ∨ ( a o< b )
 
@@ -199,6 +193,38 @@
    lemma1 (case1 x) = ¬a x
    lemma1 (case2 x) = ≡→¬d< x
 
+maxα : {n : Level} →  Ordinal {n} →  Ordinal  → Ordinal
+maxα x y with <-cmp (lv x) (lv y)
+maxα x y | tri< a ¬b ¬c = x
+maxα x y | tri> ¬a ¬b c = y
+maxα x y | tri≈ ¬a refl ¬c = record { lv = lv x ; ord = maxαd (ord x) (ord y) }
+
+omax : {n : Level} ( x y : Ordinal {suc n} ) → Ordinal {suc n}
+omax {n} x y with <-cmp (lv x) (lv y)
+omax {n} x y | tri< a ¬b ¬c = osuc y
+omax {n} x y | tri> ¬a ¬b c = osuc x
+omax {n} x y | tri≈ ¬a refl ¬c with triOrdd (ord x) (ord y)
+omax {n} x y | tri≈ ¬a refl ¬c | tri< a ¬b ¬c₁ = osuc y
+omax {n} x y | tri≈ ¬a refl ¬c | tri≈ ¬a₁ b ¬c₁ = osuc x
+omax {n} x y | tri≈ ¬a refl ¬c | tri> ¬a₁ ¬b c = osuc x
+
+omax< : {n : Level} ( x y : Ordinal {suc n} ) → x o< y → osuc y ≡ omax x y
+omax< {n} x y lt with <-cmp (lv x) (lv y)
+omax< {n} x y lt | tri< a ¬b ¬c = refl
+omax< {n} x y (case1 lt) | tri> ¬a ¬b c = ⊥-elim (¬a lt)
+omax< {n} x y (case2 lt) | tri> ¬a ¬b c = ⊥-elim (¬b (d<→lv lt ))
+omax< {n} x y (case1 lt) | tri≈ ¬a b ¬c = ⊥-elim (¬a lt)
+omax< {n} x y (case2 lt) | tri≈ ¬a refl ¬c with triOrdd (ord x) (ord y)
+omax< {n} x y (case2 lt) | tri≈ ¬a refl ¬c | tri< a ¬b ¬c₁ = refl
+omax< {n} x y (case2 lt) | tri≈ ¬a refl ¬c | tri≈ ¬a₁ b ¬c₁ = ⊥-elim ( trio<≡ b lt )
+omax< {n} x y (case2 lt) | tri≈ ¬a refl ¬c | tri> ¬a₁ ¬b c = ⊥-elim ( o<> (case2 lt) (case2 c) )
+
+omaxx : {n : Level} ( x y : Ordinal {suc n} ) → x o< omax x y
+omaxx {n} x y with trio< x y 
+omaxx {n} x y | tri< a ¬b ¬c = {!!}
+omaxx {n} x y | tri> ¬a ¬b c = {!!}
+omaxx {n} x y | tri≈ ¬a b ¬c = {!!}
+
 OrdTrans : {n : Level} → Transitive {suc n} _o≤_
 OrdTrans (case1 refl) (case1 refl) = case1 refl
 OrdTrans (case1 refl) (case2 lt2) = case2 lt2