Mercurial > hg > Members > kono > Proof > ZF-in-agda
view filter.agda @ 379:7b6592f0851a
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 21 Jul 2020 02:19:07 +0900 |
parents | 8cade5f660bd |
children | 0a116938a564 |
line wrap: on
line source
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 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 _∧_ open _∨_ open Bool -- Kunen p.76 and p.53, we use ⊆ record Filter ( L : HOD ) : Set (suc n) where field filter : HOD f⊆PL : filter ⊆ Power L filter1 : { p q : HOD } → q ⊆ L → filter ∋ p → p ⊆ q → filter ∋ q filter2 : { p q : HOD } → filter ∋ p → filter ∋ q → filter ∋ (p ∩ q) open Filter record prime-filter { L : HOD } (P : Filter L) : Set (suc (suc n)) where field proper : ¬ (filter P ∋ od∅) prime : {p q : HOD } → filter P ∋ (p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q ) record ultra-filter { L : HOD } (P : Filter L) : Set (suc (suc n)) where field proper : ¬ (filter P ∋ od∅) ultra : {p : HOD } → p ⊆ L → ( filter P ∋ p ) ∨ ( filter P ∋ ( L \ p) ) open _⊆_ trans-⊆ : { A B C : HOD} → A ⊆ B → B ⊆ C → A ⊆ C trans-⊆ A⊆B B⊆C = record { incl = λ x → incl B⊆C (incl A⊆B x) } refl-⊆ : {A : HOD} → A ⊆ A refl-⊆ {A} = record { incl = λ x → x } power→⊆ : ( A t : HOD) → Power A ∋ t → t ⊆ A power→⊆ A t PA∋t = record { incl = λ {x} t∋x → ODC.double-neg-eilm O (t1 t∋x) } where t1 : {x : HOD } → t ∋ x → ¬ ¬ (A ∋ x) t1 = zf.IsZF.power→ isZF A t PA∋t ∈-filter : {L p : HOD} → (P : Filter L ) → filter P ∋ p → p ⊆ L ∈-filter {L} {p} P lt = power→⊆ L p ( incl (f⊆PL P) lt ) ∪-lemma1 : {L p q : HOD } → (p ∪ q) ⊆ L → p ⊆ L ∪-lemma1 {L} {p} {q} lt = record { incl = λ {x} p∋x → incl lt (case1 p∋x) } ∪-lemma2 : {L p q : HOD } → (p ∪ q) ⊆ L → q ⊆ L ∪-lemma2 {L} {p} {q} lt = record { incl = λ {x} p∋x → incl lt (case2 p∋x) } q∩q⊆q : {p q : HOD } → (q ∩ p) ⊆ q q∩q⊆q = record { incl = λ lt → proj1 lt } open HOD ----- -- -- ultra filter is prime -- filter-lemma1 : {L : HOD} → (P : Filter L) → ∀ {p q : HOD } → ultra-filter P → prime-filter P filter-lemma1 {L} P u = record { proper = ultra-filter.proper u ; prime = lemma3 } where lemma3 : {p q : HOD} → filter P ∋ (p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q ) lemma3 {p} {q} lt with ultra-filter.ultra u (∪-lemma1 (∈-filter P lt) ) ... | case1 p∈P = case1 p∈P ... | case2 ¬p∈P = case2 (filter1 P {q ∩ (L \ p)} (∪-lemma2 (∈-filter P lt)) lemma7 lemma8) where lemma5 : ((p ∪ q ) ∩ (L \ p)) =h= (q ∩ (L \ p)) lemma5 = record { eq→ = λ {x} lt → record { proj1 = lemma4 x lt ; proj2 = proj2 lt } ; eq← = λ {x} lt → record { proj1 = case2 (proj1 lt) ; proj2 = proj2 lt } } where lemma4 : (x : Ordinal ) → odef ((p ∪ q) ∩ (L \ 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 lemma6 : filter P ∋ ((p ∪ q ) ∩ (L \ p)) lemma6 = filter2 P lt ¬p∈P lemma7 : filter P ∋ (q ∩ (L \ p)) lemma7 = subst (λ k → filter P ∋ k ) (==→o≡ lemma5 ) lemma6 lemma8 : (q ∩ (L \ p)) ⊆ q lemma8 = q∩q⊆q ----- -- -- if Filter contains L, prime filter is ultra -- filter-lemma2 : {L : HOD} → (P : Filter L) → filter P ∋ L → prime-filter P → ultra-filter P filter-lemma2 {L} P f∋L prime = record { proper = prime-filter.proper prime ; ultra = λ {p} p⊆L → prime-filter.prime prime (lemma p p⊆L) } where open _==_ p+1-p=1 : {p : HOD} → p ⊆ L → L =h= (p ∪ (L \ p)) eq→ (p+1-p=1 {p} p⊆L) {x} lt with ODC.decp O (odef p x) eq→ (p+1-p=1 {p} p⊆L) {x} lt | yes p∋x = case1 p∋x eq→ (p+1-p=1 {p} p⊆L) {x} lt | no ¬p = case2 (record { proj1 = lt ; proj2 = ¬p }) eq← (p+1-p=1 {p} p⊆L) {x} ( case1 p∋x ) = subst (λ k → odef L k ) diso (incl p⊆L ( subst (λ k → odef p k) (sym diso) p∋x )) eq← (p+1-p=1 {p} p⊆L) {x} ( case2 ¬p ) = proj1 ¬p lemma : (p : HOD) → p ⊆ L → filter P ∋ (p ∪ (L \ p)) lemma p p⊆L = subst (λ k → filter P ∋ k ) (==→o≡ (p+1-p=1 p⊆L)) f∋L record Dense (P : HOD ) : Set (suc n) where field dense : HOD d⊆P : dense ⊆ Power P dense-f : HOD → HOD dense-d : { p : HOD} → p ⊆ P → dense ∋ dense-f p dense-p : { p : HOD} → p ⊆ P → p ⊆ (dense-f p) record Ideal ( L : HOD ) : Set (suc n) where field ideal : HOD i⊆PL : ideal ⊆ Power L ideal1 : { p q : HOD } → q ⊆ L → ideal ∋ p → q ⊆ p → ideal ∋ q ideal2 : { p q : HOD } → ideal ∋ p → ideal ∋ q → ideal ∋ (p ∪ q) open Ideal proper-ideal : {L : HOD} → (P : Ideal L ) → {p : HOD} → Set n proper-ideal {L} P {p} = ideal P ∋ od∅ prime-ideal : {L : HOD} → Ideal L → ∀ {p q : HOD } → Set n prime-ideal {L} P {p} {q} = ideal P ∋ ( p ∩ q) → ( ideal P ∋ p ) ∨ ( ideal P ∋ q ) record F-Filter {n : Level} (L : Set n) (PL : (L → Set n) → Set n) ( _⊆_ : L → L → Set n) (_∩_ : L → L → L ) : Set (suc n) where field filter : L → Set n f⊆P : PL filter filter1 : { p q : L } → PL (λ x → q ⊆ x ) → filter p → p ⊆ q → filter q filter2 : { p q : L } → filter p → filter q → filter (p ∩ q) Filter-is-F : {L : HOD} → (f : Filter L ) → F-Filter HOD (λ p → (x : HOD) → p x → x ⊆ L ) _⊆_ _∩_ Filter-is-F {L} f = record { filter = λ x → Lift (suc n) ((filter f) ∋ x) ; f⊆P = λ x f∋x → power→⊆ _ _ (incl ( f⊆PL f ) (lower f∋x )) ; filter1 = λ {p} {q} q⊆L f∋p p⊆q → lift ( filter1 f (q⊆L q refl-⊆) (lower f∋p) p⊆q) ; filter2 = λ {p} {q} f∋p f∋q → lift ( filter2 f (lower f∋p) (lower f∋q)) } record F-Dense {n : Level} (L : Set n) (PL : (L → Set n) → Set n) ( _⊆_ : L → L → Set n) (_∩_ : L → L → L ) : Set (suc n) where field dense : L → Set n d⊆P : PL dense dense-f : L → L dense-d : { p : L} → PL (λ x → p ⊆ x ) → dense ( dense-f p ) dense-p : { p : L} → PL (λ x → p ⊆ x ) → p ⊆ (dense-f p) Dense-is-F : {L : HOD} → (f : Dense L ) → F-Dense HOD (λ p → (x : HOD) → p x → x ⊆ L ) _⊆_ _∩_ Dense-is-F {L} f = record { dense = λ x → Lift (suc n) ((dense f) ∋ x) ; d⊆P = λ x f∋x → power→⊆ _ _ (incl ( d⊆P f ) (lower f∋x )) ; dense-f = λ x → dense-f f x ; dense-d = λ {p} d → lift ( dense-d f (d p refl-⊆ ) ) ; dense-p = λ {p} d → dense-p f (d p refl-⊆) } where open Dense ------- -- the set of finite partial functions from ω to 2 -- -- data Two : Set n where i0 : Two i1 : Two data Three : Set n where j0 : Three j1 : Three j2 : Three open import Data.List hiding (map) import OPair open OPair O record PFunc : Set (suc n) where field dom : Nat → Set n map : (x : Nat ) → dom x → Two meq : {x : Nat } → { p q : dom x } → map x p ≡ map x q open PFunc data Findp : List Three → (x : Nat) → Set n where v0 : {n : List Three} → Findp ( j0 ∷ n ) Zero v1 : {n : List Three} → Findp ( j1 ∷ n ) Zero vn : {n : List Three} {d : Three} → {x : Nat} → Findp n x → Findp (d ∷ n) (Suc x) FPFunc→PFunc : List Three → PFunc FPFunc→PFunc fp = record { dom = λ x → findp fp x ; map = λ x p → find fp x p ; meq = λ {x} {p} {q} → feq fp } where findp : List Three → (x : Nat) → Set n findp n x = Findp n x find : (n : List Three ) → (x : Nat) → Findp n x → Two find (j0 ∷ _) 0 v0 = i0 find (j1 ∷ _) 0 v1 = i1 find (d ∷ n) (Suc x) (vn {n} {d} {x} p) = find n x p feq : (n : List Three) → {x : Nat} {p q : Findp n x } → find n x p ≡ find n x q feq n {0} {v0} {v0} = refl feq n {0} {v1} {v1} = refl feq [] {Suc x} {()} feq (_ ∷ n) {Suc x} {vn p} {vn q} = subst₂ (λ j k → j ≡ k ) {!!} {!!} (feq n {x} {p} {q}) record _f⊆_ (f g : PFunc) : Set (suc n) where field extend : {x : Nat} → (fr : dom f x ) → dom g x feq : {x : Nat} → {fr : dom f x } → map f x fr ≡ map g x (extend fr) open _f⊆_ min = Data.Nat._⊓_ -- m≤m⊔n = Data.Nat._⊔_ open import Data.Nat.Properties _f∩_ : (f g : PFunc) → PFunc f f∩ g = record { dom = λ x → (dom f x ) ∧ (dom g x ) ∧ ((fr : dom f x ) → (gr : dom g x ) → map f x fr ≡ map g x gr) ; map = λ x p → map f x (proj1 p) ; meq = meq f } _↑_ : (Nat → Two) → Nat → PFunc f ↑ i = record { dom = λ x → Lift n (x ≤ i) ; map = λ x _ → f x ; meq = λ {x} {p} {q} → refl } record Gf (f : Nat → Two) (p : PFunc ) : Set (suc n) where field gn : Nat f<n : (f ↑ gn) f⊆ p record FiniteF (p : PFunc ) : 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 : F-Dense PFunc (λ x → Lift (suc n) One) _f⊆_ _f∩_ Dense-Gf = record { dense = λ x → FiniteF x ; d⊆P = lift OneObj ; dense-f = λ x → record { dom = {!!} ; map = {!!} } ; dense-d = λ {p} d → {!!} ; dense-p = λ {p} d → {!!} } open Gf GF : (Nat → Two ) → F-Filter PFunc (λ x → Lift (suc n) One ) _f⊆_ _f∩_ GF f = record { filter = λ p → Gf f p ; f⊆P = lift OneObj ; filter1 = λ {p} {q} _ fp p⊆q → record { gn = gn fp ; f<n = f1 fp p⊆q } ; filter2 = λ {p} {q} fp fq → record { gn = min (gn fp) (gn fq) ; f<n = f2 fp fq } } where f1 : {p q : PFunc } → (fp : Gf f p ) → ( p⊆q : p f⊆ q ) → (f ↑ gn fp) f⊆ q f1 {p} {q} fp p⊆q = record { extend = λ {x} x<g → extend p⊆q (extend (f<n fp ) x<g) ; feq = λ {x} {fr} → lemma {x} {fr} } where lemma : {x : Nat} {fr : Lift n (x ≤ gn fp)} → map (f ↑ gn fp) x fr ≡ map q x (extend p⊆q (extend (f<n fp) fr)) lemma {x} {fr} = begin map (f ↑ gn fp) x fr ≡⟨ feq (f<n fp ) ⟩ map p x (extend (f<n fp) fr) ≡⟨ feq p⊆q ⟩ map q x (extend p⊆q (extend (f<n fp) fr)) ∎ where open ≡-Reasoning f2 : {p q : PFunc } → (fp : Gf f p ) → (fq : Gf f q ) → (f ↑ (min (gn fp) (gn fq))) f⊆ (p f∩ q) f2 {p} {q} fp fq = record { extend = λ {x} x<g → lemma2 x<g ; feq = λ {x} {fr} → lemma3 fr } where fmin = f ↑ (min (gn fp) (gn fq)) lemma1 : {x : Nat} → ( x<g : Lift n (x ≤ min (gn fp) (gn fq)) ) → (fr : dom p x) (gr : dom q x) → map p x fr ≡ map q x gr lemma1 {x} x<g fr gr = begin map p x fr ≡⟨ meq p ⟩ map p x (extend (f<n fp) (lift ( ≤-trans (lower x<g) (m⊓n≤m _ _)))) ≡⟨ sym (feq (f<n fp)) ⟩ map (f ↑ (min (gn fp) (gn fq))) x x<g ≡⟨ feq (f<n fq) ⟩ map q x (extend (f<n fq) (lift ( ≤-trans (lower x<g) (m⊓n≤n _ _)))) ≡⟨ meq q ⟩ map q x gr ∎ where open ≡-Reasoning lemma2 : {x : Nat} → ( x<g : Lift n (x ≤ min (gn fp) (gn fq)) ) → dom (p f∩ q) x lemma2 x<g = record { proj1 = extend (f<n fp ) (lift ( ≤-trans (lower x<g) (m⊓n≤m _ _))) ; proj2 = record {proj1 = extend (f<n fq ) (lift ( ≤-trans (lower x<g) (m⊓n≤n _ _))) ; proj2 = lemma1 x<g }} f∩→⊆ : (p q : PFunc ) → (p f∩ q ) f⊆ q f∩→⊆ p q = record { extend = λ {x} pq → proj1 (proj2 pq) ; feq = λ {x} {fr} → (proj2 (proj2 fr)) (proj1 fr) (proj1 (proj2 fr)) } lemma3 : {x : Nat} → ( fr : Lift n (x ≤ min (gn fp) (gn fq))) → map (f ↑ min (gn fp) (gn fq)) x fr ≡ map (p f∩ q) x (lemma2 fr) lemma3 {x} fr = map (f ↑ min (gn fp) (gn fq)) x fr ≡⟨ feq (f<n fq) ⟩ map q x (extend (f<n fq) ( lift (≤-trans (lower fr) (m⊓n≤n _ _)) )) ≡⟨ sym (feq (f∩→⊆ p q ) {x} {lemma2 fr} ) ⟩ map (p f∩ q) x (lemma2 fr) ∎ where open ≡-Reasoning 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 ω→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 record _↑n (f : HOD) (ω→2∋f : ω→2 ∋ f ) : Set n where -- field -- n : HOD -- ? : Select f (λ x f∋x → ω→nat (π1 f∋x) < ω→nat n -- Gf : {f : HOD} → ω→2 ∋ f → HOD -- Gf {f} lt = Select HODω2 (λ x H∋x → {!!} ) G : (Nat → Two) → Filter HODω2 G f = record { filter = {!!} ; f⊆PL = {!!} ; filter1 = {!!} ; filter2 = {!!} } where filter0 : HOD filter0 = {!!} f⊆PL1 : filter0 ⊆ Power HODω2 f⊆PL1 = {!!} filter11 : { p q : HOD } → q ⊆ HODω2 → filter0 ∋ p → p ⊆ q → filter0 ∋ q filter11 = {!!} filter12 : { p q : HOD } → filter0 ∋ p → filter0 ∋ q → filter0 ∋ (p ∩ q) filter12 = {!!} -- 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 = {!!} }