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

changeset 1138:dd18bb8d2893

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 Fri, 13 Jan 2023 13:03:45 +0900
parents d618788852e5
children 4517d0721b59
files src/filter.agda
diffstat 1 files changed, 35 insertions(+), 17 deletions(-) [+]
line wrap: on
line diff
--- a/src/filter.agda	Fri Jan 13 09:30:31 2023 +0900
+++ b/src/filter.agda	Fri Jan 13 13:03:45 2023 +0900
@@ -302,7 +302,7 @@
 
 open import  Relation.Binary.Structures
 
-record is-filter { L P : HOD  } (LP : L ⊆ Power P) (filter : Ordinal ) : Set n where
+record IsFilter { L P : HOD  } (LP : L ⊆ Power P) (filter : Ordinal ) : Set n where
    field
        f⊆L     : (* filter) ⊆ L
        filter1 : { p q : Ordinal } → odef L q → odef (* filter) p →  (* p) ⊆ (* q)  → odef (* filter) q
@@ -311,18 +311,17 @@
 
 -- all filter contains F
 F⊆X : { L P : HOD  } (LP : L ⊆ Power P) → Filter {L} {P} LP  → HOD
-F⊆X {L} {P} LP F = record { od = record { def = λ x → is-filter {L} {P} LP x ∧ ( filter F ⊆ * x)  } ; odmax = osuc (& L)
+F⊆X {L} {P} LP F = record { od = record { def = λ x → IsFilter {L} {P} LP x ∧ ( filter F ⊆ * x)  } ; odmax = osuc (& L)
       ; <odmax = λ {x} lt → fx00 lt } where
-      fx00 : {x : Ordinal } → is-filter LP x ∧ filter F ⊆ * x → x o< osuc (& L)
-      fx00 {x} lt = subst (λ k → k o< osuc (& L)) &iso ( ⊆→o≤ (is-filter.f⊆L (proj1 lt ))  )
+      fx00 : {x : Ordinal } → IsFilter LP x ∧ filter F ⊆ * x → x o< osuc (& L)
+      fx00 {x} lt = subst (λ k → k o< osuc (& L)) &iso ( ⊆→o≤ (IsFilter.f⊆L (proj1 lt ))  )
 
 F→Maximum : {L P : HOD} (LP : L ⊆ Power P) → ({p : HOD} → L ∋ p → L ∋ ( P ＼ p)) → ({p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∩ q))
       → (F : Filter {L} {P} LP) → o∅ o< & L →  {y : Ordinal } → odef (filter F) y →  (¬ (filter F ∋ od∅)) → MaximumFilter {L} {P} LP F
-F→Maximum {L} {P} LP NEG CAP F 0<L 0<F Fprop = record { mf = mf ; F⊆mf = ? 
-         ; proper = subst (λ k → ¬ ( odef (filter mf ) k)) (sym ord-od∅) ( is-filter.proper imf)  ; is-maximum = {!!} }  where
+F→Maximum {L} {P} LP NEG CAP F 0<L {y} 0<F Fprop = record { mf = mf ; F⊆mf = ? 
+         ; proper = subst (λ k → ¬ ( odef (filter mf ) k)) (sym ord-od∅) ( IsFilter.proper imf)  ; is-maximum = {!!} }  where
       FX : HOD
       FX = F⊆X {L} {P} LP F
-      FX∋F : odef FX (& (filter F))
       oF = & (filter F)
       mf11 : { p q : Ordinal } → odef L q → odef (* oF) p →  (* p) ⊆ (* q)  → odef (* oF) q
       mf11 {p} {q} Lq Fp p⊆q = subst₂ (λ j k → odef j k ) (sym *iso) &iso ( filter1 F (subst (λ k → odef L k) (sym &iso) Lq) 
@@ -330,36 +329,55 @@
       mf12 : { p q : Ordinal } → odef (* oF)  p →  odef (* oF) q  → odef L (& ((* p) ∩ (* q))) → odef (* oF) (& ((* p) ∩ (* q)))
       mf12 {p} {q} Fp Fq Lpq = subst (λ k → odef k (& ((* p) ∩ (* q))) ) (sym *iso) 
         ( filter2 F (subst₂ (λ j k → odef j k ) *iso (sym &iso)  Fp) (subst₂ (λ j k → odef j k ) *iso (sym &iso)  Fq) Lpq)
+      FX∋F : odef FX (& (filter F))
       FX∋F = ⟪ record { f⊆L = subst (λ k → k ⊆ L) (sym *iso) (f⊆L F) ; filter1 = mf11 ; filter2 = mf12 
         ; proper = subst₂ (λ j k →  ¬ (odef j k) ) (sym *iso) ord-od∅ Fprop  }  
           , subst (λ k → filter F ⊆ k ) (sym *iso) ( λ x → x ) ⟫ 
       SUP⊆ : (B : HOD) → B ⊆ FX → IsTotalOrderSet B → SUP FX B
-      SUP⊆ B B⊆FX OB = record { sup = Union B ; isSUP = record { ax = mf13 ; x≤sup = ?  } } where
+      SUP⊆ B B⊆FX OB with trio< (& B) o∅ 
+      ... | tri< a ¬b ¬c = ⊥-elim (¬x<0 a )
+      ... | tri≈ ¬a b ¬c = record { sup = filter F ; isSUP = record { ax = FX∋F ; x≤sup = λ {y} zy → ⊥-elim (o<¬≡ (sym b) (∈∅< zy))  } } 
+      ... | tri> ¬a ¬b 0<B = record { sup = Union B ; isSUP = record { ax = mf13 ; x≤sup = ? } } where
+          mf20 : HOD
+          mf20 = ODC.minimal O B (λ eq → (o<¬≡ (cong (&) (sym (==→o≡ eq))) (subst (λ k → k o< & B) (sym ord-od∅) 0<B )))
+          mf18 : odef B (& mf20 )
+          mf18 = ODC.x∋minimal O B (λ eq → (o<¬≡ (cong (&) (sym (==→o≡ eq))) (subst (λ k → k o< & B) (sym ord-od∅) 0<B )))
           mf16 : Union B ⊆ L
-          mf16 record { owner = b ; ao = Bb ; ox = bx } = is-filter.f⊆L ( proj1 ( B⊆FX Bb )) bx
+          mf16 record { owner = b ; ao = Bb ; ox = bx } = IsFilter.f⊆L ( proj1 ( B⊆FX Bb )) bx
           mf17 : {p q : Ordinal} → odef L q → odef (* (& (Union B))) p → * p ⊆ * q → odef (* (& (Union B))) q
           mf17 {p} {q} Lq bp p⊆q with subst (λ k → odef k p ) *iso bp
           ... | record { owner = owner ; ao = ao ; ox = ox } = subst (λ k → odef k q) (sym *iso) 
-                record { owner = ? ; ao = ? ; ox = ? } 
-          mf14 : is-filter LP (& (Union B)) 
-          mf14 = record { f⊆L = subst (λ k → k ⊆ L) (sym *iso) mf16 ; filter1 = mf17 ; filter2 = ? ; proper = ? } 
+                record { owner = owner ; ao = ao ; ox = IsFilter.filter1 mf30 Lq ox p⊆q } where
+              mf30 : IsFilter {L} {P} LP owner
+              mf30 = proj1 ( B⊆FX ao ) 
+          mf31 : {p q : Ordinal} → odef (* (& (Union B))) p → odef (* (& (Union B))) q → odef L (& ((* p) ∩ (* q))) → odef (* (& (Union B))) (& ((* p) ∩ (* q)))
+          mf31 {p} {q} bp bq Lpq with subst (λ k → odef k p ) *iso bp | subst (λ k → odef k q ) *iso bq
+          ... | record { owner = bp ; ao = Bbp ; ox = bbp } | record { owner = bq ; ao = Bbq ; ox = bbq } 
+             with OB (subst (λ k → odef B k) (sym &iso) Bbp) (subst (λ k → odef B k) (sym &iso) Bbq)
+          ... | tri< bp⊂bq ¬b ¬c = ?
+          ... | tri≈ ¬a bq=bp ¬c = ?
+          ... | tri> ¬a ¬b bq⊂bp = ?
+          mf14 : IsFilter LP (& (Union B)) 
+          mf14 = record { f⊆L = subst (λ k → k ⊆ L) (sym *iso) mf16 ; filter1 = mf17 ; filter2 = mf31 ; proper = ? } 
           mf15 :  filter F ⊆ Union B
-          mf15 {x} Fx = record { owner = ? ; ao = ? ; ox = subst (λ k → odef k x) (sym *iso) Fx  } 
+          mf15 {x} Fx = record { owner = & mf20 ; ao = mf18 ; ox = subst (λ k → odef k x) (sym *iso) (mf22 Fx) } where
+               mf22 : odef (filter F) x → odef mf20 x
+               mf22 Fx = subst (λ k → odef k x) *iso ( proj2 (B⊆FX mf18) Fx )
           mf13 : odef FX (& (Union B))
           mf13 = ⟪ mf14  , subst (λ k → filter F ⊆ k ) (sym *iso) mf15  ⟫
       mx : Maximal  FX
       mx = Zorn-lemma (∈∅< FX∋F) SUP⊆  
-      imf : is-filter {L} {P} LP (& (Maximal.maximal mx))
+      imf : IsFilter {L} {P} LP (& (Maximal.maximal mx))
       imf = proj1 (Maximal.as mx)
       mf00 : (* (& (Maximal.maximal mx))) ⊆ L
-      mf00 = is-filter.f⊆L imf   
+      mf00 = IsFilter.f⊆L imf   
       mf01 : { p q : HOD } →  L ∋ q → (* (& (Maximal.maximal mx))) ∋ p →  p ⊆ q  → (* (& (Maximal.maximal mx))) ∋ q
-      mf01 {p} {q} Lq Fq p⊆q = is-filter.filter1 imf Lq Fq 
+      mf01 {p} {q} Lq Fq p⊆q = IsFilter.filter1 imf Lq Fq 
               (λ {x} lt → subst (λ k → odef k x) (sym *iso) ( p⊆q (subst (λ k → odef k x) *iso lt ) ))
       mf02 : { p q : HOD } → (* (& (Maximal.maximal mx))) ∋ p → (* (& (Maximal.maximal mx)))  ∋ q  → L ∋ (p ∩ q) 
           → (* (& (Maximal.maximal mx))) ∋ (p ∩ q)
       mf02 {p} {q} Fp Fq Lpq = subst₂ (λ j k → odef (* (& (Maximal.maximal mx))) (& (j ∩ k ))) *iso *iso (
-          is-filter.filter2 imf Fp Fq (subst₂ (λ j k → odef L (& (j ∩ k ))) (sym *iso) (sym *iso) Lpq ))
+          IsFilter.filter2 imf Fp Fq (subst₂ (λ j k → odef L (& (j ∩ k ))) (sym *iso) (sym *iso) Lpq ))
       mf : Filter {L} {P} LP
       mf = record { filter = * (& (Maximal.maximal mx)) ; f⊆L = mf00  
          ; filter1 = mf01