Mercurial > hg > Members > kono > Proof > ZF-in-agda
view generic-filter.agda @ 391:e98b5774d180
generic filter defined
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sat, 25 Jul 2020 16:45:22 +0900 |
parents | d58edc4133b0 |
children | 55f44ec2a0c6 |
line wrap: on
line source
open import Level open import Ordinals module generic-filter {n : Level } (O : Ordinals {n}) where import filter open import zf open import logic open import partfunc {n} O import OD 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 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) import BAlgbra open BAlgbra O open inOrdinal O open OD O open OD.OD open ODAxiom odAxiom import ODC open filter O open _∧_ open _∨_ open Bool open HOD ------- -- the set of finite partial functions from ω to 2 -- -- open import Data.List open import Data.Maybe import OPair open OPair O open PFunc _f∩_ : (f g : PFunc (Lift n Nat) (Lift n Two) ) → PFunc (Lift n Nat) (Lift n Two) f f∩ g = record { dom = λ x → (dom f x ) ∧ (dom g x ) ∧ ((fr : dom f x ) → (gr : dom g x ) → pmap f x fr ≡ pmap g x gr) ; pmap = λ x p → pmap f x (proj1 p) ; meq = meq f } _↑_ : (Nat → Two) → Nat → PFunc (Lift n Nat) (Lift n Two) _↑_ f i = record { dom = λ x → Lift n (lower x ≤ i) ; pmap = λ x _ → lift (f (lower x)) ; meq = λ {x} {p} {q} → refl } record _f⊆_ (f g : PFunc (Lift n Nat) (Lift n Two) ) : Set (suc n) where field extend : {x : Nat} → (fr : dom f (lift x) ) → dom g (lift x ) feq : {x : Nat} → {fr : dom f (lift x) } → pmap f (lift x) fr ≡ pmap g (lift x) (extend fr) record FiniteF (p : PFunc (Lift n Nat) (Lift n Two) ) : Set (suc n) where field f-max : Nat f-func : Nat → Two f-p⊆f : p f⊆ (f-func ↑ f-max) f-f⊆p : (f-func ↑ f-max) f⊆ p open FiniteF -- Dense-Gf : {n : Level} → F-Dense (PFunc {n}) (λ x → Lift (suc n) (One {n})) _f⊆_ _f∩_ -- Dense-Gf = record { -- dense = λ x → FiniteF x -- ; d⊆P = lift OneObj -- ; dense-f = λ x → record { dom = {!!} ; pmap = {!!} } -- ; dense-d = λ {p} d → {!!} -- ; dense-p = λ {p} d → {!!} -- } open _f⊆_ open import Data.Nat.Properties ODSuc : (y : HOD) → infinite ∋ y → HOD ODSuc y lt = Union (y , (y , y)) data Hω2 : (i : Nat) ( x : Ordinal ) → Set n where hφ : Hω2 0 o∅ h0 : {i : Nat} {x : Ordinal } → Hω2 i x → Hω2 (Suc i) (od→ord (Union ((< nat→ω i , nat→ω 0 >) , ord→od x ))) h1 : {i : Nat} {x : Ordinal } → Hω2 i x → Hω2 (Suc i) (od→ord (Union ((< nat→ω i , nat→ω 1 >) , ord→od x ))) he : {i : Nat} {x : Ordinal } → Hω2 i x → Hω2 (Suc i) x record Hω2r (x : Ordinal) : Set n where field count : Nat hω2 : Hω2 count x open Hω2r HODω2 : HOD HODω2 = record { od = record { def = λ x → Hω2r x } ; odmax = next o∅ ; <odmax = odmax0 } where ω<next : {y : Ordinal} → infinite-d y → y o< next o∅ ω<next = ω<next-o∅ ho< lemma : {i j : Nat} {x : Ordinal } → od→ord (Union (< nat→ω i , nat→ω j > , ord→od x)) o< next x lemma = {!!} odmax0 : {y : Ordinal} → Hω2r y → y o< next o∅ odmax0 {y} r with hω2 r ... | hφ = x<nx ... | h0 {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) (lemma {i} {0} {x}) ... | h1 {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) (lemma {i} {1} {x}) ... | he {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) x<nx 3→Hω2 : List (Maybe Two) → HOD 3→Hω2 t = list→hod t 0 where list→hod : List (Maybe Two) → Nat → HOD list→hod [] _ = od∅ list→hod (just i0 ∷ t) i = Union (< nat→ω i , nat→ω 0 > , ( list→hod t (Suc i) )) list→hod (just i1 ∷ t) i = Union (< nat→ω i , nat→ω 1 > , ( list→hod t (Suc i) )) list→hod (nothing ∷ t) i = list→hod t (Suc i ) Hω2→3 : (x : HOD) → HODω2 ∋ x → List (Maybe Two) Hω2→3 x = lemma where lemma : { y : Ordinal } → Hω2r y → List (Maybe Two) lemma record { count = 0 ; hω2 = hφ } = [] lemma record { count = (Suc i) ; hω2 = (h0 hω3) } = just i0 ∷ lemma record { count = i ; hω2 = hω3 } lemma record { count = (Suc i) ; hω2 = (h1 hω3) } = just i1 ∷ lemma record { count = i ; hω2 = hω3 } lemma record { count = (Suc i) ; hω2 = (he hω3) } = nothing ∷ lemma record { count = i ; hω2 = hω3 } ω→2 : HOD ω→2 = Replace (Power infinite) (λ p → Replace infinite (λ x → < x , repl p x > )) where repl : HOD → HOD → HOD repl p x with ODC.∋-p O p x ... | yes _ = nat→ω 1 ... | no _ = nat→ω 0 ω→2f : (x : HOD) → ω→2 ∋ x → Nat → Two ω→2f x = {!!} ↑n : (f n : HOD) → ((ω→2 ∋ f ) ∧ (infinite ∋ n)) → HOD ↑n f n lt = 3→Hω2 ( ω→2f f (proj1 lt) 3↑ (ω→nat n (proj2 lt) )) -- the set of finite partial functions from ω to 2 Hω2f : Set (suc n) Hω2f = (Nat → Set n) → Two Hω2f→Hω2 : Hω2f → HOD Hω2f→Hω2 p = {!!} -- record { od = record { def = λ x → (p {!!} ≡ i0 ) ∨ (p {!!} ≡ i1 )}; odmax = {!!} ; <odmax = {!!} } record CountableOrdinal : Set (suc (suc n)) where field ctl→ : Nat → Ordinal ctl← : Ordinal → Nat ctl-iso→ : { x : Ordinal } → ctl→ (ctl← x ) ≡ x ctl-iso← : { x : Nat } → ctl← (ctl→ x ) ≡ x record CountableHOD : Set (suc (suc n)) where field mhod : HOD mtl→ : Nat → Ordinal mtl→∈P : (i : Nat) → odef mhod (mtl→ i) mtl← : (x : Ordinal) → odef mhod x → Nat mtl-iso→ : { x : Ordinal } → (lt : odef mhod x ) → mtl→ (mtl← x lt ) ≡ x mtl-iso← : { x : Nat } → mtl← (mtl→ x ) (mtl→∈P x) ≡ x open CountableOrdinal open CountableHOD PGHOD : (i : Nat) → (C : CountableOrdinal) → (P : HOD) → (p : Ordinal) → HOD PGHOD i C P p = record { od = record { def = λ x → odef P x ∧ odef (ord→od (ctl→ C i)) x ∧ ( (y : Ordinal ) → odef (ord→od p) y → odef (ord→od x) y ) } ; odmax = odmax P ; <odmax = λ {y} lt → <odmax P (proj1 lt) } next-p : (C : CountableOrdinal) (P : HOD ) (i : Nat) → (p : Ordinal) → Ordinal next-p C P i p with ODC.decp O ( PGHOD i C P p =h= od∅ ) next-p C P i p | yes y = p next-p C P i p | no not = od→ord (ODC.minimal O (PGHOD i C P p ) not) find-p : (C : CountableOrdinal) (P : HOD ) (i : Nat) → (x : Ordinal) → Ordinal find-p C P Zero x = x find-p C P (Suc i) x = find-p C P i ( next-p C P i x ) record PDN (C : CountableOrdinal) (P : HOD ) (x : Ordinal) : Set n where field gr : Nat pn<gr : (y : Ordinal) → odef (ord→od x) y → odef (ord→od (find-p C P gr o∅)) y px∈ω : odef P x open PDN PDHOD : (C : CountableOrdinal) → (P : HOD ) → HOD PDHOD C P = record { od = record { def = λ x → PDN C P x } ; odmax = odmax (Power P) ; <odmax = {!!} } where -- -- p 0 ≡ ∅ -- p (suc n) = if ∃ q ∈ ord→od ( ctl→ n ) ∧ p n ⊆ q → q --- else p n P-GenericFilter : (C : CountableOrdinal) → (P : HOD ) → GenericFilter P P-GenericFilter C P = record { genf = record { filter = PDHOD C P ; f⊆PL = {!!} ; filter1 = {!!} ; filter2 = {!!} } ; generic = λ D → {!!} }