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

changeset 32:9988ee04cf8c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
oridnal dead end
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 21 May 2019 18:13:48 +0900
parents 97ff3f7933fe
children
files ordinal.agda
diffstat 1 files changed, 34 insertions(+), 52 deletions(-) [+]
line wrap: on
line diff
--- a/ordinal.agda	Tue May 21 10:32:34 2019 +0900
+++ b/ordinal.agda	Tue May 21 18:13:48 2019 +0900
@@ -1,3 +1,4 @@
+{-# OPTIONS --allow-unsolved-metas #-} 
 open import Level
 module ordinal where
 
@@ -29,7 +30,7 @@
    field
      lv : Nat
      ord : OrdinalD {n} lv
-     order : ¬ ( ord  ≡ Φ lv ) → { prev : OrdinalD {n} lv } → prev d< ord
+     order : ¬ ( ord  ≡ Φ lv ) → Φ lv  d< ord
 
 open Ordinal
 
@@ -42,10 +43,10 @@
 ¬ℵ (OSuc lv₁ x) = ¬ℵ x
 ¬ℵ (ℵ lv₁) = ⊥
 
-s<refl : {n : Level } {lx : Nat } { x : OrdinalD {n} lx } → ¬ℵ x  → x d< OSuc lx x
-s<refl {n} {.lv₁} {Φ lv₁} t = Φ<
-s<refl {n} {.lv₁} {OSuc lv₁ x} t = s< (s<refl t)
-s<refl {n} {.(Suc lv₁)} {ℵ lv₁} ()
+s<refl : {n : Level } {lx : Nat } { x : OrdinalD {n} lx } → x d< OSuc lx x
+s<refl {n} {.lv₁} {Φ lv₁}  = Φ<
+s<refl {n} {.lv₁} {OSuc lv₁ x}  = s< s<refl 
+s<refl {n} {.(Suc lv₁)} {ℵ lv₁} = {!!}
 
 o∅ : {n : Level} → Ordinal {n}
 o∅  = record { lv = Zero ; ord = Φ Zero ; order = λ n → ⊥-elim (n refl)  }
@@ -81,11 +82,11 @@
 triOrdd  {_} {lv} (OSuc lv x) (OSuc lv x) | tri≈ ¬a refl ¬c = tri≈ ≡→¬d< refl ≡→¬d<
 triOrdd  {_} {lv} (OSuc lv x) (OSuc lv y) | tri> ¬a ¬b c = tri> (  λ lt → trio<> lt (s< c) ) (λ tx=ty → trio>≡ tx=ty (s< c) ) (s< c)
 
-d<→lv : {n : Level} {x y  : Ordinal {n}}   → ord x d< ord y → lv x ≡ lv y
-d<→lv Φ< = refl
-d<→lv (s< lt) = refl
-d<→lv ℵΦ< = refl
-d<→lv ℵ< = refl
+d<→lv : {n : Level} (x y  : Ordinal {n})   → ord x d< ord y → lv x ≡ lv y
+d<→lv x y Φ< = refl
+d<→lv x y (s< lt) = refl
+d<→lv x y ℵΦ< = refl
+d<→lv x y ℵ< = refl
 
 orddtrans : {n : Level} {lx : Nat} {x y z : OrdinalD {n}  lx }   → x d< y → y d< z → x d< z
 orddtrans {_} {lx} {.(Φ lx)} {.(OSuc lx _)} {.(OSuc lx _)} Φ< (s< y<z) = Φ< 
@@ -104,51 +105,30 @@
 maxαd : {n : Level} → { lx : Nat } → (x y : OrdinalD {n} lx ) →  OrdinalD  lx
 maxαd x y with triOrdd x y
 maxαd x y | tri< a ¬b ¬c = y
-maxαd x y | tri≈ ¬a b ¬c = x
+maxαd x y | tri≈ ¬a refl ¬c = x
 maxαd x y | tri> ¬a ¬b c = x
 
-maxΦ :  {n : Level} → { lx : Nat } → {x y : OrdinalD {n} lx } → maxαd x y ≡ Φ lx → ( x  ≡ Φ lx ) ∧ ( y  ≡ Φ lx  )
-maxΦ {_} {lv} {x} {y} m with triOrdd x y
-maxΦ {_} {lv} {.(Φ lv)} {.(Φ lv)} refl | tri≈ ¬a refl ¬c = record { proj1 = refl ; proj2 = refl }
-maxΦ {_} {lv} {.(Φ lv)} {.(OSuc lv _)} () | tri< Φ< ¬b ¬c
-maxΦ {_} {lv} {.(OSuc lv _)} {.(OSuc lv _)} () | tri< (s< a) ¬b ¬c
-maxΦ {_} {.(Suc _)} {.(Φ (Suc _))} {.(ℵ _)} () | tri< ℵΦ< ¬b ¬c
-maxΦ {_} {.(Suc _)} {.(OSuc (Suc _) _)} {.(ℵ _)} () | tri< ℵ< ¬b ¬c
-maxΦ {_} {lv} {.(OSuc lv _)} {.(Φ lv)} () | tri> ¬a ¬b Φ<
-maxΦ {_} {lv} {.(OSuc lv _)} {.(OSuc lv _)} () | tri> ¬a ¬b (s< c)
-maxΦ {_} {.(Suc _)} {.(ℵ _)} {.(Φ (Suc _))} () | tri> ¬a ¬b ℵΦ<
-maxΦ {_} {.(Suc _)} {.(ℵ _)} {.(OSuc (Suc _) _)} () | tri> ¬a ¬b ℵ<
-
-maxΦ' : {n : Level} → { lx : Nat } → {x y : OrdinalD {n} lx } → ¬ (maxαd x y ≡ Φ lx ) → ( ¬ x  ≡ Φ lx ) ∨ (¬  y  ≡ Φ lx  )
-maxΦ' {n} {lx} {x} {y} m with triOrdd x y
-maxΦ' {n} {lx} {x} {y} m | tri< a ¬b ¬c = case2 {!!}
-maxΦ' {n} {lx} {x} {y} m | tri≈ ¬a refl ¬c = {!!}
-maxΦ' {n} {lx} {x} {y} m | tri> ¬a ¬b c = {!!}
-
 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) ; order = lemma } where
-   lemma : ¬ maxαd (ord x) (ord y) ≡ Φ (lv y) → {prev : OrdinalD (lv y)} → prev d< maxαd (ord x) (ord y)
-   lemma n with maxΦ' n | triOrdd (ord x) (ord y)
-   lemma n | case1 m | tri< a ¬b ¬c = {!!}
-   lemma n | case2 m | tri< a ¬b ¬c = order y m
-   lemma n | case1 m | tri≈ ¬a refl ¬c = order y m
-   lemma n | case2 m | tri≈ ¬a refl ¬c = order y m
-   lemma n | case1 m | tri> ¬a ¬b c = order x m
-   lemma n | case2 m | tri> ¬a ¬b c = {!!}
+   lemma : ¬ maxαd (ord x) (ord y) ≡ Φ (lv y) → Φ (lv y) d< maxαd (ord x) (ord y)
+   lemma n with triOrdd (ord x) (ord y)
+   lemma n | tri< a ¬b ¬c = {!!}
+   lemma n | tri≈ ¬a refl ¬c = {!!}
+   lemma n | tri> ¬a ¬b c = {!!}
 
 _o≤_ : {n : Level} → Ordinal → Ordinal → Set (suc n)
 a o≤ b  = (a ≡ b)  ∨ ( a o< b )
 
 ordtrans : {n : Level} {x y z : Ordinal {n} }   → x o< y → y o< z → x o< z
 ordtrans {n} {x} {y} {z} (case1 x₁) (case1 x₂) = case1 ( <-trans x₁ x₂ )
-ordtrans {n} {x} {y} {z} (case1 x₁) (case2 x₂) with d<→lv x₂
+ordtrans {n} {x} {y} {z} (case1 x₁) (case2 x₂) with d<→lv y z x₂
 ... | refl = case1 x₁
-ordtrans {n} {x} {y} {z} (case2 x₁) (case1 x₂) with d<→lv x₁
+ordtrans {n} {x} {y} {z} (case2 x₁) (case1 x₂) with d<→lv x y x₁
 ... | refl = case1 x₂
-ordtrans {n} {x} {y} {z} (case2 x₁) (case2 x₂) with d<→lv x₁ | d<→lv x₂
+ordtrans {n} {x} {y} {z} (case2 x₁) (case2 x₂) with d<→lv x y x₁ | d<→lv y z x₂
 ... | refl | refl = case2 ( orddtrans x₁ x₂ )
 
 
@@ -157,12 +137,12 @@
 trio< a b | tri< a₁ ¬b ¬c = tri< (case1  a₁) (λ refl → ¬b (cong ( λ x → lv x ) refl ) ) lemma1 where
    lemma1 : ¬ (Suc (lv b) ≤ lv a) ∨ (ord b d< ord a)
    lemma1 (case1 x) = ¬c x
-   lemma1 (case2 x) with d<→lv x
+   lemma1 (case2 x) with d<→lv b a x
    lemma1 (case2 x) | refl = ¬b refl
 trio< a b | tri> ¬a ¬b c = tri> lemma1 (λ refl → ¬b (cong ( λ x → lv x ) refl ) ) (case1 c) where
    lemma1 : ¬ (Suc (lv a) ≤ lv b) ∨ (ord a d< ord b)
    lemma1 (case1 x) = ¬a x
-   lemma1 (case2 x) with d<→lv x
+   lemma1 (case2 x) with d<→lv a b x
    lemma1 (case2 x) | refl = ¬b refl
 trio< a b | tri≈ ¬a refl ¬c with triOrdd ( ord a ) ( ord b )
 trio< record { lv = .(lv b) ; ord = x } b | tri≈ ¬a refl ¬c | tri< a ¬b ¬c₁ = tri< (case2 a) (λ refl → ¬b (lemma1 refl )) lemma2 where
@@ -177,21 +157,23 @@
    lemma2 : ¬ (Suc (lv b) ≤ lv b) ∨ (x d< ord b)
    lemma2 (case1 x) = ¬a x
    lemma2 (case2 x) = trio<> x c
-trio< record { lv = .(lv b) ; ord = x } b | tri≈ ¬a refl ¬c | tri≈ ¬a₁ refl ¬c₁ = tri≈ lemma1 {!!} lemma1 where
+trio< record { lv = .(lv b) ; ord = x ; order  = z } b | tri≈ ¬a refl ¬c | tri≈ ¬a₁ refl ¬c₁ = tri≈ lemma1 lemma2 lemma1 where
    lemma1 : ¬ (Suc (lv b) ≤ lv b) ∨ (ord b d< ord b)
    lemma1 (case1 x) = ¬a x
    lemma1 (case2 x) = ≡→¬d< x
+   lemma2 : record { lv = lv b ; ord = ord b ; order = z } ≡ b
+   lemma2 = {!!}
 
 OrdTrans : {n : Level} → Transitive {suc n} _o≤_
 OrdTrans (case1 refl) (case1 refl) = case1 refl
 OrdTrans (case1 refl) (case2 lt2) = case2 lt2
 OrdTrans (case2 lt1) (case1 refl) = case2 lt1
 OrdTrans (case2 (case1 x)) (case2 (case1 y)) = case2 (case1 ( <-trans x y ) )
-OrdTrans (case2 (case1 x)) (case2 (case2 y)) with d<→lv y
+OrdTrans {_} {a} {b} {c} (case2 (case1 x)) (case2 (case2 y)) with d<→lv b c y
 OrdTrans (case2 (case1 x)) (case2 (case2 y)) | refl = case2 (case1 x )
-OrdTrans (case2 (case2 x)) (case2 (case1 y)) with d<→lv x
+OrdTrans {_} {a} {b} {c}  (case2 (case2 x)) (case2 (case1 y)) with d<→lv a b x
 OrdTrans (case2 (case2 x)) (case2 (case1 y)) | refl = case2 (case1 y)
-OrdTrans (case2 (case2 x)) (case2 (case2 y)) with d<→lv x | d<→lv y
+OrdTrans {_} {a} {b} {c} (case2 (case2 x)) (case2 (case2 y)) with d<→lv a b x | d<→lv b c y
 OrdTrans (case2 (case2 x)) (case2 (case2 y)) | refl | refl = case2 (case2 (orddtrans x y ))
 
 OrdPreorder : {n : Level} → Preorder (suc n) (suc n) (suc n)
@@ -206,12 +188,12 @@
  }
 
 TransFinite : {n : Level} → { ψ : Ordinal {n} → Set n }
-  → ( ∀ (lx : Nat ) → ψ ( record { lv = Suc lx ; ord = ℵ lx } )) 
-  → ( ∀ (lx : Nat ) → ψ ( record { lv = lx ; ord = Φ lx } ) )
-  → ( ∀ (lx : Nat ) → (x : OrdinalD lx )  → ψ ( record { lv = lx ; ord = x } ) → ψ ( record { lv = lx ; ord = OSuc lx x } ) )
+  → ( ∀ (lx : Nat ) → ψ ( record { lv = Suc lx ; ord = ℵ lx ; order = {!!}} )) 
+  → ( ∀ (lx : Nat ) → ψ ( record { lv = lx ; ord = Φ lx ; order = {!!} } ) )
+  → ( ∀ (lx : Nat ) → (x : OrdinalD lx )  → ψ ( record { lv = lx ; ord = x ; order = {!!}} ) → ψ ( record { lv = lx ; ord = OSuc lx x ; order = {!!}} ) )
   →  ∀ (x : Ordinal)  → ψ x
-TransFinite caseℵ caseΦ caseOSuc record { lv = lv ; ord = Φ lv } = {!!}
-TransFinite caseℵ caseΦ caseOSuc record { lv = lv ; ord = OSuc lv ord₁ } = {!!}
+TransFinite caseℵ caseΦ caseOSuc record { lv = lv ; ord = Φ lv ; order = z } = {!!}
+TransFinite caseℵ caseΦ caseOSuc record { lv = lv ; ord = OSuc lv ord₁ ; order = z } = {!!}
    -- caseOSuc lv ord₁ ( TransFinite caseℵ caseΦ caseOSuc (record { lv = lv ; ord = ord₁ } ))
-TransFinite caseℵ caseΦ caseOSuc record { lv = Suc lv₁ ; ord = ℵ lv₁ } = {!!} -- caseℵ lv₁
+TransFinite caseℵ caseΦ caseOSuc record { lv = Suc lv₁ ; ord = ℵ lv₁ ; order = z } = {!!} -- caseℵ lv₁