Mercurial > hg > Members > kono > Proof > ZF-in-agda
view src/generic-filter.agda @ 438:50949196aa88
⊆-reduction
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 25 Feb 2022 14:46:43 +0900 |
parents | 2b5d2072e1af |
children | fdcbf23ba2f9 |
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 OrdUtil import ODUtil open Ordinals.Ordinals O open Ordinals.IsOrdinals isOrdinal open Ordinals.IsNext isNext open OrdUtil O open ODUtil O import ODC open filter O open _∧_ open _∨_ open Bool open HOD ------- -- the set of finite partial functions from ω to 2 -- -- open import Data.List hiding (filter) open import Data.Maybe import OPair open OPair O record CountableModel (P : HOD) : Set (suc (suc n)) where field ctl-M : Ordinal ctl→ : Nat → Ordinal ctl← : (x : Ordinal )→ x o< ctl-M → Nat is-Model : (x : Nat) → ctl→ x o< ctl-M ctl-iso→ : { x : Ordinal } → (lt : x o< ctl-M) → ctl→ (ctl← x lt ) ≡ x ctl-iso← : { x : Nat } → ctl← (ctl→ x ) (is-Model x) ≡ x ctl-P∈M : Power P ∈ * ctl-M -- we expect ¬ G ∈ * ctl-M, so ¬ P ∈ * ctl-M open CountableModel ---- -- a(n) ∈ M -- ∃ q ∈ Power P → q ∈ a(n) ∧ p(n) ⊆ q -- PGHOD : (i : Nat) (P : HOD) (C : CountableModel P) → (p : Ordinal) → HOD PGHOD i P C p = record { od = record { def = λ x → odef (Power P) x ∧ odef (* (ctl→ C i)) x ∧ ( (y : Ordinal ) → odef (* p) y → odef (* x) y ) } ; odmax = odmax (Power P) ; <odmax = λ {y} lt → <odmax (Power P) (proj1 lt) } --- -- p(n+1) = if (f n) != ∅ then (f n) otherwise p(n) -- next-p : (p : Ordinal) → (f : HOD → HOD) → Ordinal next-p p f with is-o∅ ( & (f (* p))) next-p p f | yes y = p next-p p f | no not = & (ODC.minimal O (f (* p) ) (λ eq → not (=od∅→≡o∅ eq))) -- axiom of choice --- -- search on p(n) -- find-p : (P : HOD ) (C : CountableModel P) (i : Nat) → (x : Ordinal) → Ordinal find-p P C Zero x = x find-p P C (Suc i) x = find-p P C i ( next-p x (λ p → PGHOD i P C (& p) )) --- -- G = { r ∈ Power P | ∃ n → r ⊆ p(n) } -- record PDN (P p : HOD ) (C : CountableModel P) (x : Ordinal) : Set n where field gr : Nat pn<gr : (y : Ordinal) → odef (* x) y → odef (* (find-p P C gr (& p))) y x∈PP : odef (Power P) x open PDN --- -- G as a HOD -- PDHOD : (P p : HOD ) (C : CountableModel P ) → HOD PDHOD P p C = record { od = record { def = λ x → PDN P p C x } ; odmax = odmax (Power P) ; <odmax = λ {y} lt → <odmax (Power P) {y} (PDN.x∈PP lt) } open PDN ---- -- Generic Filter on Power P for HOD's Countable Ordinal (G ⊆ Power P ≡ G i.e. Nat → P → Set ) -- -- p 0 ≡ ∅ -- p (suc n) = if ∃ q ∈ M ∧ p n ⊆ q → q (by axiom of choice) ( q = * ( ctl→ n ) ) --- else p n P∅ : {P : HOD} → odef (Power P) o∅ P∅ {P} = subst (λ k → odef (Power P) k ) ord-od∅ (lemma o∅ o∅≡od∅) where lemma : (x : Ordinal ) → * x ≡ od∅ → odef (Power P) (& od∅) lemma x eq = power← P od∅ (λ {x} lt → ⊥-elim (¬x<0 lt )) x<y→∋ : {x y : Ordinal} → odef (* x) y → * x ∋ * y x<y→∋ {x} {y} lt = subst (λ k → odef (* x) k ) (sym &iso) lt open _⊆_ find-an :{P p : HOD} → (C : CountableModel P ) → odef (Power P) (& p) → Nat find-an = ? found-an :{P p : HOD} → (C : CountableModel P ) → (pw : odef (Power P) (& p)) → * (ctl→ C (find-an C pw)) =h= p found-an = ? record ⊆-reduce ( p : HOD ) : Set (suc n) where field next : HOD is-small : next ⊆ p ∧ ( ¬ ( next =h= p )) ⊆-induction : { ψ : (x : HOD) → Set (suc n) } → (p : HOD) → ψ p → (next : (x : HOD) → ψ x → ⊆-reduce x ) → (ind : (x : HOD) → (m : ψ x) → ψ ( ⊆-reduce.next (next x m )) ) → ψ od∅ ⊆-induction = ? P-GenericFilter : (P p0 : HOD ) → (C : CountableModel P) → GenericFilter P P-GenericFilter P p0 C = record { genf = record { filter = PDHOD P p0 C ; f⊆PL = f⊆PL ; filter1 = f1 ; filter2 = f2 } ; generic = λ D → {!!} } where PGHOD∈PL : (i : Nat) → (x : Ordinal) → PGHOD i P C x ⊆ Power P PGHOD∈PL i x = record { incl = λ {x} p → proj1 p } find-p-⊆P : (i : Nat) → (x y : Ordinal) → odef (Power P) x → odef (* (find-p P C i x)) y → odef P y find-p-⊆P Zero x y Px Py = subst (λ k → odef P k ) &iso ( incl (ODC.power→⊆ O P (* x) (d→∋ (Power P) Px)) (x<y→∋ Py)) find-p-⊆P (Suc i) x y Px Py with is-o∅ ( & (PGHOD i P C (& (* x)))) ... | yes y1 = find-p-⊆P i x y Px Py ... | no not = find-p-⊆P i (& fmin) y pg-01 Py where fmin : HOD fmin = ODC.minimal O (PGHOD i P C (& (* x))) (λ eq → not (=od∅→≡o∅ eq)) fmin∈PGHOD : PGHOD i P C (& (* x)) ∋ fmin fmin∈PGHOD = ODC.x∋minimal O (PGHOD i P C (& (* x))) (λ eq → not (=od∅→≡o∅ eq)) pg-01 : Power P ∋ fmin pg-01 = incl (PGHOD∈PL i x ) (subst (λ k → PGHOD i P C k ∋ fmin ) &iso fmin∈PGHOD ) f⊆PL : PDHOD P p0 C ⊆ Power P f⊆PL = record { incl = λ {x} lt → power← P x (λ {y} y<x → find-p-⊆P (gr lt) {!!} (& y) {!!} (pn<gr lt (& y) (subst (λ k → odef k (& y)) (sym *iso) y<x))) } f1 : {p q : HOD} → q ⊆ P → PDHOD P p0 C ∋ p → p ⊆ q → PDHOD P p0 C ∋ q f1 {p} {q} q⊆P PD∋p p⊆q = record { gr = {!!} ; pn<gr = {!!} ; x∈PP = {!!} } where -- reduction : {ψ : (x : HOD) → x =h= od∅ → P x} → -- q ∈ a(∃ n) ⊆ P → ( p n ⊆ q → PDHOD P p0 C ∋ q ) -- ∨ (¬ (p n ⊆ q) → induction on (p n - q) PDNp : {!!} -- PD⊆⊆N P C (& p) PDNp = PD∋p f02 : {x : Ordinal} → odef q x → odef P x f02 {x} lt = subst (λ k → def (od P) k) &iso (incl q⊆P (subst (λ k → def (od q) k) (sym &iso) lt) ) f03 : {x : Ordinal} → odef p x → odef q x f03 {x} lt = subst (λ k → def (od q) k) &iso (incl p⊆q (subst (λ k → def (od p) k) (sym &iso) lt) ) next1 : Ordinal next1 = {!!} -- find-p P C (gr PD) (next-p x (λ p₁ → PGHOD (gr PD) P C (& p₁))) f05 : next1 o< ctl-M C f05 = {!!} f06 : odef (Power P) (& q) f06 = {!!} f07 : (y : Ordinal) → odef (* (& q)) y → odef (* {!!} ) y f07 = {!!} f2 : {p q : HOD} → PDHOD P p0 C ∋ p → PDHOD P p0 C ∋ q → PDHOD P p0 C ∋ (p ∩ q) f2 {p} {q} PD∋p PD∋q = {!!} open GenericFilter open Filter record Incompatible (P : HOD ) : Set (suc (suc n)) where field q : {p : HOD } → Power P ∋ p → HOD r : {p : HOD } → Power P ∋ p → HOD incompatible : { p : HOD } → (P∋p : Power P ∋ p) → Power P ∋ q P∋p → Power P ∋ r P∋p → ( p ⊆ q P∋p) ∧ ( p ⊆ r P∋p) → ∀ ( s : HOD ) → Power P ∋ s → ¬ (( q P∋p ⊆ s ) ∧ ( r P∋p ⊆ s )) lemma725 : (P p : HOD ) (C : CountableModel P) → * (ctl-M C) ∋ Power P → Incompatible P → ¬ ( * (ctl-M C) ∋ filter ( genf ( P-GenericFilter P p C ))) lemma725 = {!!} open import PFOD O -- HODω2 : HOD -- -- ω→2 : HOD -- ω→2 = Power infinite lemma725-1 : Incompatible HODω2 lemma725-1 = {!!} lemma726 : (C : CountableModel HODω2) → Union ( Replace HODω2 (λ p → filter ( genf ( P-GenericFilter HODω2 p C )))) =h= ω→2 lemma726 = {!!} -- -- val x G = { val y G | ∃ p → G ∋ p → x ∋ < y , p > } -- record valR (x : HOD) {P : HOD} (G : GenericFilter P) : Set (suc n) where field valx : HOD record valS (ox oy oG : Ordinal) : Set n where field op : Ordinal p∈G : odef (* oG) op is-val : odef (* ox) ( & < * oy , * op > ) val : (x : HOD) {P : HOD } → (G : GenericFilter P) → HOD val x G = TransFinite {λ x → HOD } ind (& x) where ind : (x : Ordinal) → ((y : Ordinal) → y o< x → HOD) → HOD ind x valy = {!!} -- -- W (ω , H ( ω , 2 )) = { p ∈ ( Nat → H (ω , 2) ) | { i ∈ Nat → p i ≠ i1 } is finite } --