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

view src/filter.agda @ 1126:3091ac71a999

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 Tue, 10 Jan 2023 03:00:04 +0900
parents edef8810a023
children c4f4868a8cdd
line wrap: on
line source

{-# OPTIONS --allow-unsolved-metas #-} 

open import Level
open import Ordinals
module filter {n : Level } (O : Ordinals {n})   where

open import zf
open import logic
import OD 

open import Relation.Nullary 
open import Data.Empty 
open import Relation.Binary.Core
open import Relation.Binary.PropositionalEquality
import BAlgebra 

open BAlgebra O

open inOrdinal O
open OD O
open OD.OD
open ODAxiom odAxiom

import OrdUtil
import ODUtil
open Ordinals.Ordinals  O
open Ordinals.IsOrdinals isOrdinal
open Ordinals.IsNext isNext
open OrdUtil O
open ODUtil O


import ODC
open ODC O

open _∧_
open _∨_
open Bool

-- Kunen p.76 and p.53, we use ⊆
record Filter { L P : HOD  } (LP : L ⊆ Power P) : Set (suc n) where
   field
       filter  : HOD   
       f⊆L     : filter ⊆ L
       filter1 : { p q : HOD } →  L ∋ q → filter ∋ p →  p ⊆ q  → filter ∋ q
       filter2 : { p q : HOD } → filter ∋ p →  filter ∋ q  → L ∋ (p ∩ q) → filter ∋ (p ∩ q)

open Filter

record prime-filter { L P : HOD } {LP : L ⊆ Power P} (F : Filter {L} {P} LP) : Set (suc (suc n)) where
   field
       proper  : ¬ (filter F ∋ od∅)
       prime   : {p q : HOD } → L ∋ p → L ∋ q  → L ∋ (p ∪ q) →  filter F ∋ (p ∪ q) → ( filter F ∋ p ) ∨ ( filter F ∋ q )

record ultra-filter { L P : HOD } {LP : L ⊆ Power P} (F : Filter {L} {P} LP) : Set (suc (suc n)) where
   field
       proper  : ¬ (filter F ∋ od∅)
       ultra   : {p : HOD } → L ∋ p → L ∋  ( P ＼ p) → ( filter F ∋ p ) ∨ (  filter F ∋ ( P ＼ p) )

∈-filter : {L P p : HOD} →  {LP : L ⊆ Power P}  → (F : Filter {L} {P} LP ) → filter F ∋ p → L ∋ p 
∈-filter {L} {p} {LP} F lt = ( f⊆L F) lt 

⊆-filter : {L P p q : HOD } →  {LP : L ⊆ Power P } → (F : Filter {L} {P} LP) →  L ∋ q → q ⊆ P
⊆-filter {L} {P} {p} {q} {LP} F lt = power→⊆ P q ( LP lt )

∪-lemma1 : {L p q : HOD } → (p ∪ q)  ⊆ L → p ⊆ L
∪-lemma1 {L} {p} {q} lt p∋x = lt (case1 p∋x) 

∪-lemma2 : {L p q : HOD } → (p ∪ q)  ⊆ L → q ⊆ L
∪-lemma2 {L} {p} {q} lt p∋x = lt (case2 p∋x) 

q∩q⊆q : {p q : HOD } → (q ∩ p) ⊆ q 
q∩q⊆q lt = proj1 lt 

open HOD

-----
--
--  ultra filter is prime
--

filter-lemma1 :  {P L : 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) → ultra-filter F  → prime-filter F 
filter-lemma1 {P} {L} LP NG IN F u = record {
         proper = ultra-filter.proper u
       ; prime = lemma3
    } where
  lemma3 : {p q : HOD} → L ∋ p → L ∋ q  → L ∋ (p ∪ q) → filter F ∋ (p ∪ q) → ( filter F ∋ p ) ∨ ( filter F ∋ q )
  lemma3 {p} {q} Lp Lq _ lt with ultra-filter.ultra u Lp (NG Lp)
  ... | case1 p∈P  = case1 p∈P 
  ... | case2 ¬p∈P = case2 (filter1 F {q ∩ (P ＼ p)} Lq lemma7 lemma8) where
    lemma5 : ((p ∪ q ) ∩ (P ＼ p)) =h=  (q ∩ (P ＼ p))
    lemma5 = record { eq→ = λ {x} lt → ⟪ lemma4 x lt , proj2 lt  ⟫
       ;  eq← = λ {x} lt → ⟪  case2 (proj1 lt) , proj2 lt ⟫
      } where
         lemma4 : (x : Ordinal ) → odef ((p ∪ q) ∩ (P ＼ p)) x → odef q x
         lemma4 x lt with proj1 lt
         lemma4 x lt | case1 px = ⊥-elim ( proj2 (proj2 lt) px )
         lemma4 x lt | case2 qx = qx
    lemma9 : L ∋ ((p ∪ q ) ∩ (P ＼ p))
    lemma9 = subst (λ k → L ∋ k ) (sym (==→o≡ lemma5)) (IN Lq (NG Lp))
    lemma6 : filter F ∋ ((p ∪ q ) ∩ (P ＼ p))
    lemma6 = filter2 F lt ¬p∈P  lemma9
    lemma7 : filter F ∋ (q ∩ (P ＼ p))
    lemma7 =  subst (λ k → filter F ∋ k ) (==→o≡ lemma5 ) lemma6
    lemma8 : (q ∩ (P ＼ p)) ⊆ q
    lemma8 lt = proj1 lt

-----
--
--  if Filter {L} {P} contains L, prime filter is ultra
--

filter-lemma2 :  {P L : HOD} → (LP : L ⊆ Power P)
       → ({p : HOD} → L ∋ p → L ∋ ( P ＼ p))
       → (F : Filter {L} {P} LP)  → filter F ∋ P → prime-filter F → ultra-filter F
filter-lemma2 {P} {L} LP Lm F f∋P prime = record {
         proper = prime-filter.proper prime
       ; ultra = λ {p}  L∋p _ → prime-filter.prime prime L∋p (Lm  L∋p) (lemma10 L∋p ((f⊆L F) f∋P) ) (lemma p (p⊆L  L∋p ))  
   } where
        open _==_
        p⊆L : {p : HOD} → L ∋ p  → p ⊆ P
        p⊆L {p} lt = power→⊆ P p ( LP lt )
        p+1-p=1 : {p : HOD} → p ⊆ P  → P =h= (p ∪ (P ＼ p)) 
        eq→ (p+1-p=1 {p} p⊆P) {x} lt with ODC.decp O (odef p x)
        eq→ (p+1-p=1 {p} p⊆P) {x} lt | yes p∋x = case1 p∋x
        eq→ (p+1-p=1 {p} p⊆P) {x} lt | no ¬p = case2 ⟪ lt , ¬p ⟫
        eq← (p+1-p=1 {p} p⊆P) {x} ( case1 p∋x ) = subst (λ k → odef P k ) &iso (p⊆P ( subst (λ k → odef p k) (sym &iso) p∋x  )) 
        eq← (p+1-p=1 {p} p⊆P) {x} ( case2 ¬p  ) = proj1 ¬p
        lemma : (p : HOD) → p ⊆ P   →  filter F ∋ (p ∪ (P ＼ p))
        lemma p p⊆P = subst (λ k → filter F ∋ k ) (==→o≡ (p+1-p=1 {p} p⊆P)) f∋P 
        lemma10 : {p : HOD} → L ∋ p → L ∋ P → L ∋ (p ∪ (P ＼ p))
        lemma10 {p} L∋p lt = subst (λ k → L ∋ k ) (==→o≡ (p+1-p=1 {p} (p⊆L L∋p))) lt

-----
--
--  if there is a filter , there is a ultra filter under the axiom of choise
--        Zorn Lemma

-- filter→ultra :  {P L : HOD} → (LP : L ⊆ Power P) → ({p : HOD} → L ∋ p → L ∋ ( P ＼ p)) → (F : Filter {L} {P} LP)  → ultra-filter F
-- filter→ultra {P} {L} LP Lm F = {!!}

record Dense  {L P : HOD } (LP : L ⊆ Power P)  : Set (suc n) where
   field
       dense : HOD
       d⊆P :  dense ⊆ L
       dense-f : {p : HOD} → L ∋ p  → HOD
       dense-d :  { p : HOD} → (lt : L ∋ p) → dense ∋ dense-f lt
       dense-p :  { p : HOD} → (lt : L ∋ p) → (dense-f lt) ⊆ p  

record Ideal   {L P : HOD } (LP : L ⊆ Power P) : Set (suc n) where
   field
       ideal : HOD   
       i⊆L :  ideal ⊆ L 
       ideal1 : { p q : HOD } →  L ∋ q  → ideal ∋ p →  q ⊆ p  → ideal ∋ q
       ideal2 : { p q : HOD } → ideal ∋ p →  ideal ∋ q  → ideal ∋ (p ∪ q)

open Ideal

proper-ideal : {L P : HOD} → (LP : L ⊆ Power P) → (P : Ideal {L} {P} LP ) → {p : HOD} → Set n
proper-ideal {L} {P} LP I = ideal I ∋ od∅

prime-ideal : {L P : HOD} → (LP : L ⊆ Power P) → Ideal {L} {P} LP → ∀ {p q : HOD } → Set n
prime-ideal {L} {P} LP I {p} {q} =  ideal I ∋ ( p ∩ q) → ( ideal I ∋ p ) ∨ ( ideal I ∋ q )


record GenericFilter {L P : HOD} (LP : L ⊆ Power P) (M : HOD) : Set (suc n) where
    field
       genf : Filter {L} {P} LP
       generic : (D : Dense {L} {P} LP ) → M ∋ Dense.dense D → ¬ ( (Dense.dense D ∩ Filter.filter genf ) ≡ od∅ )

record MaximumFilter {L P : HOD} (LP : L ⊆ Power P) : Set (suc n) where
    field
       mf : Filter {L} {P} LP
       proper  : ¬ (filter mf ∋ od∅)
       is-maximum : ( f : Filter {L} {P} LP ) →  ¬ (filter f ∋ od∅)  →  ¬ ( filter mf  ⊂ filter f  )

record Fp {L P : HOD} (LP : L ⊆ Power P)  (mx : MaximumFilter {L} {P} LP ) (p x : Ordinal ) : Set n where
    field 
       y : Ordinal 
       mfy : odef (filter (MaximumFilter.mf mx)) y
       x=y∪p : x ≡ & ( * y ∪ * p )

max→ultra : {L P : HOD} (LP : L ⊆ Power P) 
       → ({p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ＼ q)) 
       → ({p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∪ q))
       → (mx : MaximumFilter {L} {P} LP ) → ultra-filter ( MaximumFilter.mf mx )
max→ultra {L} {P} LP NEG CUP mx = record { proper = MaximumFilter.proper mx ; ultra = ultra } where
    mf = MaximumFilter.mf mx
    ultra : {p : HOD} → L ∋ p → L ∋ (P ＼ p) → (filter mf ∋ p) ∨ (filter mf ∋ (P ＼ p))
    ultra {p} Lp lnp with ∋-p (filter mf) p
    ... | yes y = case1 y
    ... | no np with ∋-p (filter mf) (P ＼ p) 
    ... | yes y = case2 y
    ... | no n-p = ⊥-elim (MaximumFilter.is-maximum mx FisFilter FisProper  ⟪ F< , FisGreater ⟫  ) where
         F⊆L : {x : Ordinal } →  Fp {L} {P} LP mx (& p) x ∨ odef (filter mf) x → odef L x
         F⊆L (case2 mfx) = f⊆L mf mfx
         F⊆L {x} (case1 pmf) = mu04 pmf where
             mu05 : (fp : Fp LP mx (& p) x ) → odef L (Fp.y fp )
             mu05 fp = f⊆L mf ( Fp.mfy fp )
             mu04 :  Fp LP mx (& p) x → odef L x
             mu04 fp = subst (λ k → odef L k ) (sym (trans (Fp.x=y∪p fp ) mu06  )) 
              ( CUP (subst (λ k → odef L k ) (sym &iso) (mu05 fp)) Lp ) where
                 mu06 :  & (* (Fp.y fp) ∪ * (& p)) ≡ & (* (Fp.y fp) ∪ p) 
                 mu06 = cong (λ k → & (* (Fp.y fp) ∪ k))  *iso
         F : HOD  -- Replace (filter mf) (λ y → y ∪ p ) ∪ filter mf
         F = record { od = record { def = λ x →  Fp {L} {P} LP mx (& p) x ∨ odef (filter mf) x  } 
            ; odmax = & L ; <odmax = λ lt → odef< (F⊆L lt) } 
         mu01 :  {r : HOD} {q : HOD} → L ∋ q → F ∋ r → r ⊆ q → F ∋ q
         mu01 {r} {q} Lq (case1 record { y = y ; mfy = mfy ; x=y∪p = x=y∪p }) r⊆q = mu03 where
             y+q-r : HOD
             y+q-r = * y ∪ ( q ＼ r )
             Ly : L ∋ * y
             Ly = subst (λ k → odef L k) (sym &iso) (f⊆L mf mfy)
             mu08 : L ∋ y+q-r
             mu08 = CUP Ly (NEG Lq (subst (λ k → odef L k) 
               (trans (cong (λ k → & (* y ∪ k)) (sym *iso)) (sym x=y∪p) ) (CUP Ly Lp )) ) 
             mu09 : * y ⊆ y+q-r
             mu09 {x} yx = case1 yx
             mu07 : filter mf  ∋ y+q-r
             mu07 = filter1 mf {_} {y+q-r} mu08 (subst (λ k → odef (filter mf) k) (sym &iso) mfy) mu09
             mu03 : odef F (& q) -- y+q-r + p  ≡ y+q-(y+p)+ p = q  so it is in F
             mu03 = case1 record { y = _  ; mfy = mu07 ; x=y∪p = cong (&) (==→o≡ record { eq→ = mu10 ; eq← = mu11 } ) } where
                mu12 : r ≡ (* y ∪ p)
                mu12 = subst₂ (λ j k → j ≡ k ) *iso (trans *iso (cong (λ k → (* y ∪ k)) *iso)) (cong (*) x=y∪p )
                mu10 : {x : Ordinal} → odef q x → odef (* (& y+q-r) ∪ * (& p)) x
                mu10 {x} qx with ODC.∋-p O r (* x)
                ... | no nrx = case1 (subst (λ k → odef k x) (sym *iso) mu13) where
                      mu13 : odef (* y ∪ (q ＼ r)) x 
                      mu13 = case2 ⟪ qx , (λ rx → nrx (subst (λ k → odef r k ) (sym &iso) rx))  ⟫ 
                ... | yes rx with subst₂ (λ j k → odef j k ) mu12 (sym &iso) rx
                ... | case1 yx = case1 (subst (λ k → odef k x) (sym *iso) (case1 (subst (λ k → odef (* y) k) (trans &iso &iso) yx) ) )
                ... | case2 px = case2 (subst₂ (λ j k → odef j k ) (sym *iso) (trans &iso &iso) px )
                mu11 : {x : Ordinal} → odef (* (& y+q-r) ∪ * (& p)) x → odef q x
                mu11 {x} (case2 px) = r⊆q (subst (λ k → odef k x) (sym mu12) (case2 (subst (λ k → odef k x) *iso px) )) 
                mu11 {x} (case1 m06x) with subst (λ k → odef k x) *iso m06x
                ... | case1 yx = r⊆q (subst (λ k → odef k x) (sym mu12) (case1 yx))
                ... | case2 q-rx = proj1 q-rx
         mu01 {r} {q} Lq (case2 mfr) r⊆q = case2 ( filter1 mf Lq mfr r⊆q)  
         mu02 : {r : HOD} {q : HOD} → F ∋ r → F ∋ q → L ∋ (r ∩ q) → F ∋ (r ∩ q)
         mu02 {r} {q} (case1 record { y = y₁ ; mfy = mfy₁ ; x=y∪p = x=y∪p₁ }) (case1 record { y = y ; mfy = mfy ; x=y∪p = x=y∪p }) Lrq = ?
         mu02 {r} {q} (case1 record { y = y ; mfy = mfy ; x=y∪p = x=y∪p }) (case2 mfq) Lrq = ?
         mu02 {r} {q} (case2 mfr) (case1 record { y = y ; mfy = mfp ; x=y∪p = x=y∪p }) Lrq = ?
         mu02 {r} {q} (case2 mfr) (case2 mfq ) Lrq = ?
         FisFilter : Filter {L} {P} LP
         FisFilter = record { filter = F ; f⊆L = F⊆L ; filter1 = mu01 ; filter2 = mu02 }
         FisGreater : {x : Ordinal } → odef (filter (MaximumFilter.mf mx))  x → odef (filter FisFilter ) x
         FisGreater {x} mfx = case2 mfx
         F< : & (filter (MaximumFilter.mf mx)) o< & F
         F< = ?
         FisProper : ¬ (filter FisFilter ∋ od∅)
         FisProper = {!!}

open _==_

-- open import Relation.Binary.Definitions

ultra→max : {L P : HOD} (LP : L ⊆ Power P) → ({p : HOD} 
       → L ∋ p → L ∋ ( P ＼ p)) 
       → ({p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∩ q))
       → (U : Filter {L} {P} LP) → ultra-filter U → MaximumFilter LP 
ultra→max {L} {P} LP NG CAP U u  = record { mf = U ; proper = ultra-filter.proper u ; is-maximum = is-maximum } where
  is-maximum : (F : Filter {L} {P} LP) → (¬ (filter F ∋ od∅)) → (U⊂F : filter U  ⊂ filter F ) → ⊥
  is-maximum F Prop ⟪ U<F , U⊆F ⟫   = Prop f0 where
     GT : HOD
     GT = record { od = record { def = λ x → odef (filter F) x ∧ (¬ odef (filter U) x) } ; odmax = & L ; <odmax = um02 } where
         um02 : {y : Ordinal } → odef (filter F) y ∧ (¬ odef (filter U) y) → y o< & L
         um02 {y} Fy = odef< ( f⊆L F (proj1 Fy ) )
     GT≠∅ :  ¬ (GT =h= od∅)
     GT≠∅ eq = ⊥-elim (U≠F ( ==→o≡ ((⊆→= {filter U} {filter F}) U⊆F (U-F=∅→F⊆U {filter F} {filter U} gt01)))) where
         U≠F : ¬ ( filter U ≡ filter F )
         U≠F eq = o<¬≡ (cong (&) eq) U<F
         gt01 : (x : Ordinal) → ¬ ( odef (filter F) x ∧ (¬ odef (filter U) x))
         gt01 x not = ¬x<0 ( eq→ eq not )
     p : HOD
     p = ODC.minimal O GT GT≠∅
     ¬U∋p : ¬ ( filter U ∋ p )
     ¬U∋p = proj2 (ODC.x∋minimal O GT GT≠∅)
     L∋p : L ∋  p
     L∋p = f⊆L F ( proj1 (ODC.x∋minimal O GT GT≠∅))
     um00 : ¬ odef (filter U) (& p)
     um00 = proj2 (ODC.x∋minimal O GT GT≠∅)
     L∋-p : L ∋  ( P ＼ p )
     L∋-p = NG L∋p
     U∋-p : filter U ∋  ( P ＼ p )
     U∋-p with ultra-filter.ultra u {p} L∋p L∋-p
     ... | case1 ux = ⊥-elim ( ¬U∋p ux )
     ... | case2 u-x = u-x
     F∋p : filter F ∋ p
     F∋p = proj1 (ODC.x∋minimal O GT GT≠∅)
     F∋-p : filter F ∋ ( P ＼ p )
     F∋-p = U⊆F U∋-p 
     f0 : filter F ∋ od∅
     f0 = subst (λ k → odef (filter F) k ) (trans (cong (&) ∩-comm) (cong (&) [a-b]∩b=0 ) ) ( filter2 F F∋p F∋-p ( CAP L∋p L∋-p) )

import zorn 

open import Relation.Binary

PO : IsStrictPartialOrder _≡_ _⊂_ 
PO = record { isEquivalence = record { refl = refl ; sym = sym ; trans = trans }
   ; trans = λ {a} {b} {c} → trans-⊂ {a} {b} {c}
   ; irrefl = λ x=y x<y → ?
   ; <-resp-≈ =  record { fst = λ {x} {y} {y1} y=y1 xy1 → ? ; snd = λ {x} {x1} {y} x=x1 x1y → ? } }

open zorn O _⊂_ PO

open import  Relation.Binary.Structures

SUP⊆ : (P B : HOD) → B ⊆ P → IsTotalOrderSet B → SUP P B
SUP⊆ P B B⊆P OB = record { sup = Union B ; isSUP = record { ax = ? ; x≤sup = ? } }

MaximumSubset : {L P : HOD} 
      → o∅ o< & L →  o∅ o< & P → P ⊆ L
      → Maximal  P
MaximumSubset {L} {P} 0<L 0<P P⊆L = Zorn-lemma 0<P (SUP⊆ P)

MaximumFilterExist : {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 →  o∅ o< & (filter F)  →  (¬ (filter F ∋ od∅)) → MaximumFilter {L} {P} LP 
MaximumFilterExist {L} {P} LP NEG CAP F 0<L 0<F Fprop = record { mf = {!!} ; proper = {!!} ; is-maximum = {!!} }  where
     mf01 : Maximal  {!!}  
     mf01 = MaximumSubset  0<L {!!} {!!}