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

changeset 12:b531d2b417ad

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
dead end
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 14 May 2019 00:23:30 +0900
parents 2df90eb0896c
children 8f3ff7bd2ff0
files zf.agda
diffstat 1 files changed, 70 insertions(+), 36 deletions(-) [+]
line wrap: on
line diff
--- a/zf.agda	Mon May 13 20:51:45 2019 +0900
+++ b/zf.agda	Tue May 14 00:23:30 2019 +0900
@@ -128,65 +128,99 @@
   open import  Relation.Binary.PropositionalEquality
   
   data Ordinal {n : Level }  :  Set n where
-     Φ : {lv : Nat} → Ordinal {n} lv
-     T-suc : {lv : Nat} → Ordinal {n} lv → Ordinal lv
-     ℵ_ :  (lv : Nat) → Ordinal (Suc lv)
+     Φ : {lv : Nat} → Ordinal {n} 
+     T-suc : {lv : Nat} → Ordinal {n} → Ordinal 
+     ℵ_ :  (lv : Nat) → Ordinal 
+
+  olevel : {n : Level } → Ordinal {n} → Nat
+  olevel (Φ {lv}) = lv
+  olevel (T-suc {lv} x) = lv
+  olevel (ℵ lv) = lv
 
   data _o<_ {n : Level } :  Ordinal {n}  →  Ordinal {n}  → Set n where
-     l< : {lx ly : Nat }  → {x : Ordinal {n} lx } →  {y : Ordinal {n} ly } → lx < ly → x o< y
-     Φ<  : {lx : Nat} → {x : Ordinal {n} lx}  →  Φ {n} {lx} o< T-suc {n} {lx} x
-     s<  : {lx : Nat} → {x : Ordinal {n} lx}  →  x o< T-suc {n} {lx} x
-     ℵΦ< : {lx : Nat} → {x : Ordinal {n} lx } →  Φ {n} {lx} o< (ℵ lx) 
-     ℵ<  : {lx : Nat} → {x : Ordinal {n} lx } →  T-suc {n} {lx} x o< (ℵ lx) 
+     l<  : {x y : Ordinal {n} }  →  olevel x < olevel y → x o< y
+     Φ<  : {x : Ordinal {n} }  →  Φ {n} {olevel x}  o< T-suc {n} {olevel x} x
+     s<  : {x : Ordinal {n} }  →  x o< T-suc {n} {olevel x} x
+     ℵΦ< : {x : Ordinal {n} } →  Φ {n} {olevel x} o< (ℵ (olevel x) ) 
+     ℵ<  : {x : Ordinal {n} } →  T-suc {n} {olevel x} x o< (ℵ (olevel x)) 
+
+  open import Data.Nat.Properties 
+
+  triO> : {n : Level } → {x y : Ordinal {n} }  →  olevel y < olevel x → x o< y → ⊥
+  triO> {n} {x} {y} y<x xo<y with <-cmp  (olevel x ) (olevel y )
+  triO> {n} {x} {y} y<x xo<y | tri< a ¬b ¬c =  ¬c y<x 
+  triO> {n} {x} {y} y<x xo<y | tri≈ ¬a b ¬c =  ¬c y<x 
+  triO> {n} {x} {y} y<x (l< x₁) | tri> ¬a ¬b c =  ¬a x₁ 
+  triO> {n} {Φ} {T-suc _} y<x Φ< | tri> ¬a ¬b c =  ¬b refl 
+  triO> {n} {x} {T-suc x} y<x s< | tri> ¬a ¬b c =  ¬b refl 
+  triO> {n} {Φ {u}} {ℵ u} y<x ℵΦ< | tri> ¬a ¬b c = ¬b refl
+  triO> {n} {(T-suc _)} {ℵ u} y<x ℵ< | tri> ¬a ¬b c =  ¬b refl 
 
-  _o≈_ : {n : Level } {lv : Nat } → Rel ( Ordinal {n} lv ) n
-  _o≈_  = {!!}
+  nat< : { x y : Nat } → x ≡ y → x < y → ⊥
+  nat< {Zero} {Zero} refl ()
+  nat< {Suc x} {.(Suc x)} refl (s≤s t) = nat< {x} {x} refl t
+  
+  trio! : {n : Level } → {x  : Ordinal {n} }  → x o< x → ⊥
+  trio! {n} {x} (l< y) = nat< refl y
 
-  triO : {n : Level } → {lx ly : Nat}   → Trichotomous  _o≈_ ( _o<_ {n} {lx} {ly} )
-  triO {n} {lv} Φ y = {!!}
-  triO {n} {lv} (T-suc x) y = {!!}
-  triO {n} {.(Suc lv)} (ℵ lv) y = {!!}
+  triO : {n : Level } → Trichotomous  _≡_ ( _o<_ {n} )
+  triO x y with <-cmp (olevel x ) (olevel y )
+  triO x y | tri< a ¬b ¬c = tri< (l< a) (λ x=y → ¬b (cong (λ z → olevel z) x=y ) ) ( triO> a )
+  triO x y | tri> ¬a ¬b c = tri> (triO> c) (λ x=y → ¬b (cong (λ z → olevel z) x=y ) ) (l< c)
+  triO Φ Φ | tri≈ ¬a refl ¬c = tri≈ trio!  refl trio!
+  triO (ℵ lv) (ℵ lv) | tri≈ ¬a refl ¬c = tri≈ trio! refl trio!
+
+  triO Φ (T-suc y) | tri≈ ¬a refl ¬c = tri≈ {!!} {!!} {!!}
+  triO Φ (ℵ lv) | tri≈ ¬a refl ¬c = tri≈ {!!} {!!} {!!} 
+  triO (T-suc x) Φ | tri≈ ¬a refl ¬c = tri≈ {!!} {!!} {!!}
+  triO (T-suc x) (ℵ lv) | tri≈ ¬a refl ¬c = tri≈ {!!} {!!} {!!} 
+  triO (ℵ lv) Φ | tri≈ ¬a refl ¬c = tri≈ {!!} {!!} {!!}
+  triO (ℵ lv) (T-suc y) | tri≈ ¬a refl ¬c = tri≈ {!!} {!!} {!!}
+
+  triO (T-suc x) (T-suc y) | tri≈ ¬a refl ¬c with triO x y
+  triO (T-suc x) (T-suc y) | tri≈ ¬a refl ¬c | tri< a ¬b ¬c₁ = tri< {!!} {!!} {!!}
+  triO (T-suc x) (T-suc x) | tri≈ ¬a refl ¬c | tri≈ ¬a₁ refl ¬c₁ = tri≈ trio! refl trio!
+  triO (T-suc x) (T-suc y) | tri≈ ¬a refl ¬c | tri> ¬a₁ ¬b c = {!!}
 
 
   max = Data.Nat._⊔_
   
-  maxα : {n : Level } → { lx ly : Nat } → Ordinal {n} lx  →  Ordinal {n} ly  → Ordinal {n} (max lx ly)
+  maxα : {n : Level } → Ordinal {n} →  Ordinal {n} → Ordinal {n} 
   maxα x y with x o< y
   ... | t = {!!}
 
   -- X' = { x ∈ X |  ψ  x } ∪ X , Mα = ( ∪ (β < α) Mβ ) '
 
-  data Constructible {n : Level } {lv : Nat} ( α : Ordinal {n} lv )  :  Set (suc n) where
-     fsub : ( ψ : Ordinal {n} lv → Set n ) → Constructible  α
-     xself : Ordinal {n} lv → Constructible  α
+  data Constructible {n : Level }  ( α : Ordinal {n} )  :  Set (suc n) where
+     fsub : ( ψ : Ordinal {n} → Set n ) → Constructible  α
+     xself : Ordinal {n} → Constructible  α
   
   record ConstructibleSet {n : Level } : Set (suc n) where
    field
-      level : Nat
-      α : Ordinal {n} level 
+      α : Ordinal {n} 
       constructible : Constructible α
   
   open ConstructibleSet
   
-  data _c∋_ {n : Level } : {lv lv' : Nat} {α : Ordinal {n} lv } {α' : Ordinal {n} lv' } →
-        Constructible {n} {lv} α → Constructible {n} {lv'} α' → Set n where
-     c> : {lv lv' : Nat} {α : Ordinal {n} lv } {α' : Ordinal {n} lv' }
-        (ta : Constructible {n} {lv} α ) ( tx : Constructible {n} {lv'} α' ) → α' o< α →  ta c∋ tx
-     xself-fsub  : {lv : Nat} {α : Ordinal {n} lv } 
-         (ta : Ordinal {n} lv ) ( ψ : Ordinal {n} lv → Set n ) → _c∋_ {n} {_} {_} {α} {α} (xself ta ) ( fsub ψ)  
-     fsub-fsub : {lv lv' : Nat} {α : Ordinal {n} lv } 
-          ( ψ : Ordinal {n} lv → Set n ) ( ψ₁ : Ordinal {n} lv → Set n ) →
-         ( ∀ ( x :  Ordinal {n} lv ) → ψ x →  ψ₁ x ) →  _c∋_ {n} {_} {_} {α} {α} ( fsub ψ ) ( fsub ψ₁) 
+  data _c∋_ {n : Level } :  {α : Ordinal {n} } {α' : Ordinal {n} } →
+        Constructible {n} α → Constructible {n}  α' → Set n where
+     c> :  {α : Ordinal {n} } {α' : Ordinal {n}  }
+        (ta : Constructible {n}  α ) ( tx : Constructible {n}  α' ) → α' o< α →  ta c∋ tx
+     xself-fsub  :  {α : Ordinal {n} } 
+         (ta : Ordinal {n} ) ( ψ : Ordinal {n} → Set n ) → _c∋_ {n} {α} {α} (xself ta ) ( fsub ψ)  
+     fsub-fsub :  {α : Ordinal {n} } 
+          ( ψ : Ordinal {n} → Set n ) ( ψ₁ : Ordinal {n} → Set n ) →
+         ( ∀ ( x :  Ordinal {n} ) → ψ x →  ψ₁ x ) →  _c∋_ {n}   {α} {α} ( fsub ψ ) ( fsub ψ₁) 
 
   _∋_  : {n : Level} → (ConstructibleSet {n}) → (ConstructibleSet {n} ) → Set n 
   a ∋ x  = constructible a c∋ constructible x
 
-  data _c≈_ {n : Level } : {lv lv' : Nat} {α : Ordinal {n} lv } {α' : Ordinal {n} lv' } →
-        Constructible {n} {lv} α → Constructible {n} {lv'} α' → Set n where
-      crefl :  {lv : Nat} {α : Ordinal {n} lv } → _c≈_ {n} {_} {_} {α} {α} (xself α ) (xself α )
-      feq :  {lv : Nat} {α : Ordinal {n} lv }
-          → ( ψ : Ordinal {n} lv → Set n ) ( ψ₁ : Ordinal {n} lv → Set n ) 
-          → (∀ ( x :  Ordinal {n} lv ) → ψ x  ⇔ ψ₁ x ) → _c≈_ {n} {_} {_} {α} {α} ( fsub ψ ) ( fsub ψ₁)
+  data _c≈_ {n : Level } :  {α : Ordinal {n} } {α' : Ordinal {n}  } →
+        Constructible {n}  α → Constructible {n}  α' → Set n where
+      crefl :   {α : Ordinal {n} } → _c≈_ {n} {α} {α} (xself α ) (xself α )
+      feq :   {α : Ordinal {n} }
+          → ( ψ : Ordinal {n} → Set n ) ( ψ₁ : Ordinal {n} → Set n ) 
+          → (∀ ( x :  Ordinal {n} ) → ψ x  ⇔ ψ₁ x ) → _c≈_ {n}   {α} {α} ( fsub ψ ) ( fsub ψ₁)
 
   _≈_  : {n : Level} → (ConstructibleSet {n}) → (ConstructibleSet {n} ) → Set n 
   a ≈ x  = constructible a c≈ constructible x
@@ -197,7 +231,7 @@
        ZFSet = ConstructibleSet 
      ; _∋_ = _∋_
      ; _≈_ = _≈_ 
-     ; ∅  = record { level = Zero ; α = Φ ; constructible = xself Φ }
+     ; ∅  = record { α = Φ ; constructible = xself Φ }
      ; _×_ = {!!}
      ; Union = {!!}
      ; Power = {!!}