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

changeset 470:f57f92c7c874

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 Mon, 28 Mar 2022 08:51:19 +0900
parents 69f90d8d0607
children 2b048496cb21
files src/ODC.agda
diffstat 1 files changed, 15 insertions(+), 17 deletions(-) [+]
line wrap: on
line diff
--- a/src/ODC.agda	Wed Mar 23 21:42:12 2022 +0900
+++ b/src/ODC.agda	Mon Mar 28 08:51:19 2022 +0900
@@ -106,7 +106,7 @@
 OrdP  x y | tri≈ ¬a refl ¬c = no ( o<¬≡ refl )
 OrdP  x y | tri> ¬a ¬b c = yes c
 
-open import Relation.Binary.HeterogeneousEquality as HE -- using (_≅_;refl)
+-- open import Relation.Binary.HeterogeneousEquality as HE -- using (_≅_;refl)
 
 record Element (A : HOD) : Set (suc n) where
     field
@@ -118,12 +118,13 @@
 TotalOrderSet : ( A : HOD ) →  (_<_ : (x y : HOD) → Set n )  → Set (suc n)
 TotalOrderSet A _<_ = Trichotomous (λ (x : Element A) y → elm x ≡ elm y ) (λ x y → elm x < elm y )  
 
+PartialOrderSet : ( A : HOD ) →  (_<_ : (x y : HOD) → Set n )  → Set (suc n)
+PartialOrderSet A _<_ = (a b :  Element A)
+     → (elm a < elm b → (¬ (elm b < elm a) ∧ (¬ (elm a ≡ elm b) ))) ∧ (elm a ≡ elm b → (¬ elm a < elm b) ∧ (¬ elm b < elm a))
+
 me : { A a : HOD } → A ∋ a → Element A
 me {A} {a} lt = record { elm = a ; is-elm = lt }
 
--- elm-cmp : {A a b : HOD} → {_<_ : (x y : HOD) → Set n }  → A ∋ a →  A ∋ b →  TotalOrderSet A _<_  → Tri _ _ _
--- elm-cmp {A} {a} {b} ax bx cmp = cmp (me ax) (me bx)
-
 record SUP ( A B : HOD ) (_<_ : (x y : HOD) → Set n ) : Set (suc n) where
    field
       sup : HOD
@@ -147,24 +148,21 @@
 
 Zorn-lemma : { A : HOD } → { _<_ : (x y : HOD) → Set n }
     → o∅ o< & A 
+    → PartialOrderSet A _<_
     → ( ( B : HOD) → (B⊆A : B ⊆ A) → TotalOrderSet B _<_ → SUP A B  _<_  )
     → Maximal A _<_ 
-Zorn-lemma {A} {_<_} 0<A supP = zorn00 where
+Zorn-lemma {A} {_<_} 0<A PO supP = zorn00 where
      HasMaximal : HOD
      HasMaximal = record { od = record { def = λ x → (m : Ordinal) → odef A x ∧ odef A m ∧ (¬ (* x < * m))} ; odmax = & A ; <odmax = {!!} }
-     z01 : {B a b : HOD} → TotalOrderSet B _<_ → B ∋ a → B ∋ b  → (a ≡ b ) ∨ (a < b ) → b < a → ⊥
-     z01 {B} {a} {b} Tri  B∋a  B∋b (case1 a=b) b<a with Tri (me  B∋a) (me B∋b) 
-     ... | tri< a₁ ¬b ¬c = ¬b  a=b
-     ... | tri≈ ¬a b₁ ¬c = ¬c b<a
-     ... | tri> ¬a ¬b c = ¬b a=b
-     z01 {B} {a} {b} Tri  B∋a  B∋b (case2 a<b) b<a with Tri (me  B∋a) (me B∋b) 
-     ... | tri< a₁ ¬b ¬c = ¬c b<a
-     ... | tri≈ ¬a b₁ ¬c = ¬c b<a
-     ... | tri> ¬a ¬b c = ¬a a<b
+     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 = proj1 (proj2 (PO (me  A∋b) (me A∋a)) (sym a=b)) b<a
+     z01 {a} {b} A∋a A∋b (case2 a<b) b<a = proj1 (PO (me  A∋b) (me A∋a)) b<a ⟪ a<b , (λ b=a → proj1 (proj2 (PO (me  A∋b) (me A∋a)) b=a ) b<a ) ⟫
      ZChain→¬SUP :  (z : ZChain A (& A) _<_ ) →  ¬ (SUP A (ZChain.B z) _<_ )
-     ZChain→¬SUP z sp = ⊥-elim {!!} where
-         z02 :  (x : HOD) → ZChain.B z ∋ x → ⊥
-         z02 x xe = ( z01 (ZChain.total z) xe {!!} (SUP.x≤sup sp xe) {!!} )
+     ZChain→¬SUP z sp = ⊥-elim (z02 (ZChain.fb z (SUP.A∋maximal sp)) (ZChain.B∋fb z  _ (SUP.A∋maximal sp)) (ZChain.¬x≤sup z _  (SUP.A∋maximal sp) z03 )) where
+         z03 : & (SUP.sup sp) o< & A
+         z03 = c<→o< (SUP.A∋maximal sp)
+         z02 :  (x : HOD) → ZChain.B z ∋ x → SUP.sup sp < x → ⊥
+         z02 x xe s<x = ( z01 (incl (ZChain.B⊆A z) xe) (SUP.A∋maximal sp) (SUP.x≤sup sp xe) s<x )
      ind :  (x : Ordinal) → ((y : Ordinal) → y o< x →  ZChain A y _<_ )
          →  ZChain A x _<_
      ind x prev with Oprev-p x