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

changeset 552:fb210e812eba

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 Thu, 28 Apr 2022 18:33:10 +0900
parents 9f24214f4270
children 567a1a9f3e0a
files src/zorn.agda
diffstat 1 files changed, 31 insertions(+), 134 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Thu Apr 28 17:56:53 2022 +0900
+++ b/src/zorn.agda	Thu Apr 28 18:33:10 2022 +0900
@@ -1,19 +1,18 @@
 {-# OPTIONS --allow-unsolved-metas #-}
 open import Level hiding ( suc ; zero )
 open import Ordinals
+open import Relation.Binary 
+open import Relation.Binary.Core
+open import Relation.Binary.PropositionalEquality
 import OD 
-module zorn {n : Level } (O : Ordinals {n}) (_<_ : (x y : OD.HOD O ) → Set n ) where
+module zorn {n : Level } (O : Ordinals {n}) (_<_ : (x y : OD.HOD O ) → Set n ) (PO : IsStrictPartialOrder _≡_ _<_ ) where
 
 open import zf
 open import logic
 -- open import partfunc {n} O
 
 open import Relation.Nullary 
-open import Relation.Binary 
 open import Data.Empty 
-open import Relation.Binary
-open import Relation.Binary.Core
-open import Relation.Binary.PropositionalEquality
 import BAlgbra 
 
 
@@ -43,117 +42,14 @@
 _≤_ : (x y : HOD) → Set (Level.suc n)
 x ≤ y = ( x ≡ y ) ∨ ( x < y )
 
-record Element (A : HOD) : Set (Level.suc n) where
-    field
-       elm : HOD
-       is-elm : A ∋ elm
-
-open Element
-
-_<A_ : {A : HOD} → (x y : Element A ) → Set n
-x <A y = elm x < elm y
-_≡A_ : {A : HOD} → (x y : Element A ) → Set (Level.suc n)
-x ≡A y = elm x ≡ elm y
-
-IsPartialOrderSet : ( A : HOD ) → Set (Level.suc n)
-IsPartialOrderSet A = IsStrictPartialOrder (_≡A_ {A}) _<A_  
 
 open _==_
 open _⊆_
 
-isA : { A B  : HOD } → B ⊆ A → (x : Element B) → Element A
-isA B⊆A x = record { elm = elm x ; is-elm = incl B⊆A (is-elm x) }
-
-⊆-IsPartialOrderSet : { A B  : HOD } → B ⊆ A → IsPartialOrderSet A → IsPartialOrderSet B 
-⊆-IsPartialOrderSet {A} {B} B⊆A  PA = record {
-       isEquivalence = record { refl = refl ; sym = sym ; trans = trans } ;  trans = λ {x} {y} {z} → trans1 {x} {y} {z} 
-     ; irrefl = λ {x} {y} → irrefl1 {x} {y} ; <-resp-≈ = resp0 
-   } where
-   _<B_ : (x y : Element B ) → Set n
-   x <B y = elm x < elm y
-   trans1 : {x y z : Element B} → x <B y → y <B z → x <B z 
-   trans1 {x} {y} {z} x<y y<z  = IsStrictPartialOrder.trans PA {isA B⊆A x} {isA B⊆A y} {isA B⊆A z} x<y y<z 
-   irrefl1 : {x y : Element B} → elm x ≡ elm y → ¬ ( x <B y  )
-   irrefl1 {x} {y} x=y x<y = IsStrictPartialOrder.irrefl PA {isA B⊆A x} {isA B⊆A y} x=y x<y 
-   open import Data.Product
-   resp0 : ({x y z : Element B} → elm y ≡ elm z → x <B y → x <B z) × ({x y z : Element B} → elm y ≡ elm z → y <B x → z <B x) 
-   resp0 = Data.Product._,_  (λ {x} {y} {z} → proj₁ (IsStrictPartialOrder.<-resp-≈ PA) {isA B⊆A x } {isA B⊆A y }{isA B⊆A z }) 
-                             (λ {x} {y} {z} → proj₂ (IsStrictPartialOrder.<-resp-≈ PA) {isA B⊆A x } {isA B⊆A y }{isA B⊆A z })
-
 -- open import Relation.Binary.Properties.Poset as Poset
 
-IsTotalOrderSet : ( A : HOD ) →  Set (Level.suc n)
-IsTotalOrderSet A = IsStrictTotalOrder  (_≡A_ {A}) _<A_ 
-
-me : { A a : HOD } → A ∋ a → Element A
-me {A} {a} lt = record { elm = a ; is-elm = lt }
-
-A∋x-irr : (A : HOD) {x y : HOD} → x ≡ y → (A ∋ x) ≡ (A ∋ y )
-A∋x-irr A {x} {y} refl = refl
-
-me-elm-refl : (A : HOD) → (x : Element A) → elm (me {A} (d→∋ A (is-elm x))) ≡ elm x
-me-elm-refl A record { elm = ex ; is-elm = ax } = *iso 
-
--- <-induction : (A : HOD) { ψ : (x : HOD) → A ∋ x → Set (Level.suc n)}
---    →  IsPartialOrderSet A
---    → ( {x : HOD } → A ∋ x → ({ y : HOD } → A ∋ y →  y < x → ψ y ) → ψ x )
---    → {x0 x : HOD } → A ∋ x0 → A ∋ x → x0 < x → ψ x
--- <-induction A {ψ} PO ind ax0 ax x0<a = subst (λ k → ψ k ) *iso (<-induction-ord (osuc (& x)) <-osuc )  where
---      -- y < * ox → & y o< ox
---      induction : (ox : Ordinal) → ((oy : Ordinal) → oy o< ox → ψ (* oy)) → ψ (* ox)
---      induction ox prev = ind  ( λ {y} lt → subst (λ k → ψ k ) *iso (prev (& y) {!!})) 
---      <-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (* oy)
---      <-induction-ord ox {oy} lt = TransFinite {λ oy → ψ (* oy)} induction oy
-
-
-open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
-
--- Don't use Element other than Order, you'll be in a trouble
--- postulate   -- may be proved by transfinite induction and functional extentionality
---   ∋x-irr : (A : HOD) {x y : HOD} → x ≡ y → (ax : A ∋ x) (ay : A ∋ y ) → ax ≅ ay 
---   odef-irr : (A : OD) {x y : Ordinal} → x ≡ y → (ax : def A x) (ay : def A y ) → ax ≅ ay 
-
--- is-elm-irr : (A : HOD) → {x y : Element A } → elm x ≡ elm y → is-elm x ≅ is-elm y 
--- is-elm-irr A {x} {y} eq = ∋x-irr A eq (is-elm x) (is-elm y )
-
-El-irr2 : (A : HOD) → {x y : Element A } → elm x ≡ elm y → is-elm x ≅ is-elm y → x ≡ y
-El-irr2  A {x} {y} refl HE.refl = refl
-
--- El-irr : {A : HOD} → {x y : Element A } → elm x ≡ elm y → x ≡ y
--- El-irr {A} {x} {y} eq = El-irr2 A eq ( is-elm-irr A eq ) 
-
-record _Set≈_ (A B : Ordinal ) : Set n where
-   field
-       fun←  : {x : Ordinal } → odef (* A)  x → Ordinal
-       fun→  : {x : Ordinal } → odef (* B)  x → Ordinal
-       funB  : {x : Ordinal } → ( lt : odef (* A)  x ) → odef (* B) ( fun← lt )
-       funA  : {x : Ordinal } → ( lt : odef (* B)  x ) → odef (* A) ( fun→ lt )
-       fiso← : {x : Ordinal } → ( lt : odef (* B)  x ) → fun←  ( funA lt ) ≡ x
-       fiso→ : {x : Ordinal } → ( lt : odef (* A)  x ) → fun→  ( funB lt ) ≡ x
-
-open _Set≈_
-record _OS≈_ {A B : HOD} (TA : IsTotalOrderSet A ) (TB : IsTotalOrderSet B ) : Set (Level.suc n) where
-   field
-      iso : (& A ) Set≈  (& B)
-      fmap : {x y : Ordinal} → (ax : odef A x) → (ay : odef A y) → * x < * y
-          → * (fun← iso (subst (λ k → odef k x) (sym *iso) ax)) < * (fun← iso (subst (λ k → odef k y) (sym *iso) ay))
-
-Cut< : ( A x : HOD )  → HOD
-Cut<  A x = record { od = record { def = λ y → ( odef A y ) ∧ ( x < * y ) } ; odmax = & A
-    ; <odmax = λ lt → subst (λ k → k o< & A) &iso (c<→o< (subst (λ k → odef A k ) (sym &iso) (proj1 lt))) }
-
-Cut<T : {A : HOD}   → (TA : IsTotalOrderSet A ) ( x : HOD )→  IsTotalOrderSet ( Cut< A x )
-Cut<T {A} TA x =  record { isEquivalence = record { refl = refl ; trans = trans ; sym = sym }
-   ; trans = λ {x} {y} {z} → IsStrictTotalOrder.trans TA {me (proj1 (is-elm x))} {me (proj1 (is-elm y))} {me (proj1 (is-elm z))} ;
-         compare = λ x y → IsStrictTotalOrder.compare TA (me (proj1 (is-elm x))) (me (proj1 (is-elm y)))  }
-
-record _OS<_ {A B : HOD} (TA : IsTotalOrderSet A ) (TB : IsTotalOrderSet B ) : Set (Level.suc n) where
-   field
-      x : HOD
-      iso : TA OS≈ (Cut<T TA x) 
-
--- OS<-cmp : {x : HOD} → Trichotomous {_} {IsTotalOrderSet x} _OS≈_ _OS<_ 
--- OS<-cmp A B = {!!}
+IsTotalOrderSet : ( A : HOD ) → Set (Level.suc n)
+IsTotalOrderSet A = {a b : HOD} → odef A (& a) → odef A (& b)  → Tri (a < b) (a ≡ b) (b < a )
 
       
 record Maximal ( A : HOD )  : Set (Level.suc n) where
@@ -205,16 +101,15 @@
 
 Zorn-lemma : { A : HOD } 
     → o∅ o< & A 
-    → IsPartialOrderSet A 
     → ( ( B : HOD) → (B⊆A : B ⊆ A) → IsTotalOrderSet B → SUP A B   ) -- SUP condition
     → Maximal A 
-Zorn-lemma {A}  0<A PO supP = zorn00 where
+Zorn-lemma {A}  0<A supP = zorn00 where
      supO : (C : Ordinal ) → (* C) ⊆ A → IsTotalOrderSet (* C) → Ordinal
      supO C C⊆A TC = & ( SUP.sup ( supP (* C)  C⊆A TC ))
      z01 : {a b : HOD} → A ∋ a → A ∋ b  → (a ≡ b ) ∨ (a < b ) → b < a → ⊥
-     z01 {a} {b} A∋a A∋b (case1 a=b) b<a = IsStrictPartialOrder.irrefl PO {me A∋b} {me A∋a} (sym a=b) b<a
-     z01 {a} {b} A∋a A∋b (case2 a<b) b<a = IsStrictPartialOrder.irrefl PO {me A∋b} {me A∋b} refl
-          (IsStrictPartialOrder.trans PO {me A∋b} {me A∋a} {me A∋b}  b<a a<b)
+     z01 {a} {b} A∋a A∋b (case1 a=b) b<a = IsStrictPartialOrder.irrefl PO   (sym a=b) b<a
+     z01 {a} {b} A∋a A∋b (case2 a<b) b<a = IsStrictPartialOrder.irrefl PO   refl
+          (IsStrictPartialOrder.trans PO     b<a a<b)
      z07 :   {y : Ordinal} → {P : Set n} → odef A y ∧ P → y o< & A
      z07 {y} p = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) (proj1 p )))
      s : HOD
@@ -291,7 +186,7 @@
                ... | case1 eq = ⊥-elim ( ne (cong (&) eq) )
                ... | case2 lt = subst₂ (λ j k → j < k ) (sym *iso) (sym *iso) lt
            z14 :  f (& (SUP.sup (sp0 f mf zc))) ≡ & (SUP.sup (sp0 f mf zc))
-           z14 with IsStrictTotalOrder.compare (ZChain.f-total zc ) (me (subst (λ k → odef chain k) (sym &iso)  (ZChain.f-next zc z12 ))) (me z12 )
+           z14 with ZChain.f-total zc  (subst (λ k → odef chain k) (sym &iso)  (ZChain.f-next zc z12 )) z12 
            ... | tri< a ¬b ¬c = ⊥-elim z16 where
                z16 : ⊥
                z16 with proj1 (mf (& ( SUP.sup sp1)) ( SUP.A∋maximal sp1 ))
@@ -361,15 +256,22 @@
                 zc9 = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next =  ZChain.f-next zc0
                      ; f-immediate =  ZChain.f-immediate zc0 ; chain∋x  = ZChain.chain∋x zc0 ; is-max = zc17 }  -- no extention
           ... | case2 ¬fy<x with ODC.p∨¬p O ( x ≡ & ( SUP.sup ( supP ( ZChain.chain zc0 ) (ZChain.chain⊆A zc0 ) (ZChain.f-total zc0) ) ))
-          ... | case1 x=sup = record { chain = {!!} ; chain⊆A = {!!} ; f-total = {!!} ; f-next =  {!!}
-                     ; f-immediate =  {!!} ; chain∋x  = {!!} ; is-max = {!!} } where -- x is sup
+          ... | case1 x=sup = record { chain = schain ; chain⊆A = {!!} ; f-total = {!!} ; f-next =  {!!}
+                     ; f-immediate =  {!!} ; chain∋x  = case1 (ZChain.chain∋x zc0) ; is-max = {!!} } where -- x is sup
                 sp = SUP.sup ( supP ( ZChain.chain zc0 ) (ZChain.chain⊆A zc0 ) (ZChain.f-total zc0) ) 
                 chain = ZChain.chain zc0
-                z20 : HOD
-                z20 = record { od = record { def = λ x → odef chain x ∨ (FClosure A f (& sp) x) } ; odmax = & A ; <odmax = {!!} }
-
-          ... | case2 ¬x=sup = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next = {!!}
-                     ; f-immediate = {!!} ; chain∋x  = {!!} ; is-max = {!!} }  -- no extention
+                schain : HOD
+                schain = record { od = record { def = λ x → odef chain x ∨ (FClosure A f (& sp) x) } ; odmax = & A ; <odmax = {!!} }
+          ... | case2 ¬x=sup = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next = ZChain.f-next zc0
+                     ; f-immediate = ZChain.f-immediate zc0 ; chain∋x  =  ZChain.chain∋x zc0 ; is-max = {!!} }  where -- no extention
+                z18 :  {a b : Ordinal} → odef (ZChain.chain zc0) a → b o< x → (ba : odef A b) →
+                            Prev< A (ZChain.chain zc0) ba f ∨ (& (SUP.sup (supP (* (& (ZChain.chain zc0)))
+                               (subst (λ k → k ⊆ A) (sym *iso) (ZChain.chain⊆A zc0))
+                               (subst IsTotalOrderSet (sym *iso) (ZChain.f-total zc0))))
+                             ≡ b) →
+                            * a < * b → odef (ZChain.chain zc0) b
+                z18 {a} {b} za b<x ba (case1 p) a<b = {!!}
+                z18 {a} {b} za b<x ba (case2 p) a<b = {!!}
      ... | no ¬ox with trio< (& A) x   --- limit ordinal case
      ... | tri< a ¬b ¬c = {!!} where
           zc0 = prev (& A) a
@@ -419,7 +321,6 @@
                         zc15 : {z : Ordinal } → ( odef (ZChain.chain zc0) z ∨ (z ≡ f x) ) → odef A z
                         zc15 {z} (case1 zz) = subst (λ k → odef A k ) &iso ( incl (ZChain.chain⊆A zc0) (subst (λ k → odef chain  k ) (sym &iso) zz ) )
                         zc15 (case2 refl) = proj2 ( mf x (subst (λ k → odef A k ) &iso {!!} ) )
-                    IPO = ⊆-IsPartialOrderSet  ⊆-zc5 PO
                     zc8 : { A B x : HOD } → (ax : A ∋ x ) → (P : Prev< A B ax f ) → * (f (& (* (Prev<.y P)))) ≡ x
                     zc8 {A} {B} {x} ax P = subst₂ (λ j k → * ( f j ) ≡ k ) (sym &iso) *iso (sym (cong (*) ( Prev<.x=fy P)))
                     fx=zc :  odef (ZChain.chain zc0) y → Tri  (* (f y) < * y ) (* (f y) ≡ * y) (* y < * (f y) )
@@ -430,14 +331,13 @@
                     ... | ⟪ case2 x<fx , afx ⟫ = tri> (z01 ay0 (Afx ay0) (case2 zc14)) (λ lt → z01 (Afx ay0) ay0 (case1 lt) zc14) zc14 where
                         zc14 : * y < * (f y)
                         zc14 = subst (λ k → * y < k ) (subst (λ k → * (f y) ≡ k ) *iso (cong (*) (sym &iso ))) x<fx
-                    cmp : Trichotomous _ _ 
-                    cmp record { elm = a ; is-elm = aa } record { elm = b ; is-elm = ab } with aa | ab
-                    ... | case1 x | case1 x₁ = IsStrictTotalOrder.compare (ZChain.f-total zc0) (me x) (me x₁)
-                    ... | case2 fx | case2 fx₁ = tri≈ {!!} (subst₂ (λ j k → j ≡ k ) *iso *iso (trans (cong (*) fx) (sym (cong (*) fx₁ ) ))) {!!}
-                    ... | case1 c | case2 fx = {!!} -- subst₂ (λ j k → Tri ( j < k ) (j ≡ k) ( k < j ) ) {!!} {!!} ( fx>zc (subst (λ k → odef chain k) {!!} c ))
-                    ... | case2 fx | case1 c with ODC.p∨¬p O ( Prev< A chain (incl (ZChain.chain⊆A zc0) c) f )
+                    zc6 : IsTotalOrderSet zc5
+                    zc6 {a} {b} ( case1 x ) ( case1 x₁ ) = ZChain.f-total zc0 x x₁ 
+                    zc6 {a} {b} ( case2 fx ) ( case2 fx₁ ) = tri≈ {!!} (subst₂ (λ j k → j ≡ k ) *iso *iso (trans (cong (*) fx) (sym (cong (*) fx₁ ) ))) {!!}
+                    zc6 {a} {b} ( case1 c ) ( case2 fx ) = {!!} -- subst₂ (λ j k → Tri ( j < k ) (j ≡ k) ( k < j ) ) {!!} {!!} ( fx>zc (subst (λ k → odef chain k) {!!} c ))
+                    zc6 {a} {b} ( case2 fx ) ( case1 c ) with ODC.p∨¬p O ( Prev< A chain (incl (ZChain.chain⊆A zc0) c) f )
                     ... | case2 n = {!!}
-                    ... | case1 fb with IsStrictTotalOrder.compare (ZChain.f-total zc0) (me (subst (λ k → odef chain k) (sym &iso) (Prev<.ay pr))) (me (subst (λ k → odef chain k) (sym &iso) (Prev<.ay fb)))
+                    ... | case1 fb with ZChain.f-total zc0 (subst (λ k → odef chain k) (sym &iso) (Prev<.ay pr)) (subst (λ k → odef chain k) (sym &iso) (Prev<.ay fb))
                     ... | tri< a₁ ¬b ¬c = {!!}
                     ... | tri≈ ¬a b₁ ¬c = subst₂ (λ j k → Tri ( j < k ) (j ≡ k) ( k < j ) ) zc11 zc10 ( fx=zc zc12 ) where
                          zc10 : * y ≡ b
@@ -447,9 +347,6 @@
                          zc12 : odef chain y
                          zc12 = subst (λ k → odef chain k ) (subst (λ k → & b ≡ k ) &iso (sym (cong (&) zc10)))  c 
                     ... | tri> ¬a ¬b c₁ = {!!}
-                    zc6 : IsTotalOrderSet zc5
-                    zc6 =  record { isEquivalence = IsStrictPartialOrder.isEquivalence IPO ; trans = λ {x} {y} {z} → IsStrictPartialOrder.trans IPO {x} {y} {z}
-                        ; compare = cmp }
 -- usage (see filter.agda )
 --
 -- _⊆'_ : ( A B : HOD ) → Set n