Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 387:8b0715e28b33
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 25 Jul 2020 09:09:00 +0900 |
| parents | 24a66a246316 |
| children | 19687f3304c9 |
| files | LEMC.agda OD.agda ODC.agda Ordinals.agda filter.agda generic-filter.agda logic.agda partfunc.agda |
| diffstat | 8 files changed, 597 insertions(+), 516 deletions(-) [+] |
line wrap: on
line diff
--- a/LEMC.agda Thu Jul 23 17:50:28 2020 +0900 +++ b/LEMC.agda Sat Jul 25 09:09:00 2020 +0900 @@ -2,7 +2,7 @@ open import Ordinals open import logic open import Relation.Nullary -module LEMC {n : Level } (O : Ordinals {n} ) (p∨¬p : ( p : Set (suc n)) → p ∨ ( ¬ p )) where +module LEMC {n : Level } (O : Ordinals {n} ) (p∨¬p : ( p : Set n) → p ∨ ( ¬ p )) where open import zf open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) @@ -23,17 +23,48 @@ open import zfc +open HOD + +open _⊆_ + +decp : ( p : Set n ) → Dec p -- assuming axiom of choice +decp p with p∨¬p p +decp p | case1 x = yes x +decp p | case2 x = no x + +∋-p : (A x : HOD ) → Dec ( A ∋ x ) +∋-p A x with p∨¬p ( A ∋ x) -- LEM +∋-p A x | case1 t = yes t +∋-p A x | case2 t = no (λ x → t x) + +double-neg-eilm : {A : Set n} → ¬ ¬ A → A -- we don't have this in intutionistic logic +double-neg-eilm {A} notnot with decp A -- assuming axiom of choice +... | yes p = p +... | no ¬p = ⊥-elim ( notnot ¬p ) + +power→⊆ : ( A t : HOD) → Power A ∋ t → t ⊆ A +power→⊆ A t PA∋t = record { incl = λ {x} t∋x → double-neg-eilm (λ not → t1 t∋x (λ x → not x) ) } where + t1 : {x : HOD } → t ∋ x → ¬ ¬ (A ∋ x) + t1 = zf.IsZF.power→ isZF A t PA∋t + --- With assuption of HOD is ordered, p ∨ ( ¬ p ) <=> axiom of choice --- -record choiced ( X : HOD) : Set (suc n) where +record choiced ( X : Ordinal ) : Set n where field - a-choice : HOD - is-in : X ∋ a-choice - -open HOD + a-choice : Ordinal + is-in : odef (ord→od X) a-choice open choiced +-- ∋→d : ( a : HOD ) { x : HOD } → ord→od (od→ord a) ∋ x → X ∋ ord→od (a-choice (choice-func X not)) +-- ∋→d a lt = subst₂ (λ j k → odef j k) oiso (sym diso) lt + +oo∋ : { a : HOD} { x : Ordinal } → odef (ord→od (od→ord a)) x → a ∋ ord→od x +oo∋ lt = subst₂ (λ j k → odef j k) oiso (sym diso) lt + +∋oo : { a : HOD} { x : Ordinal } → a ∋ ord→od x → odef (ord→od (od→ord a)) x +∋oo lt = subst₂ (λ j k → odef j k ) (sym oiso) diso lt + OD→ZFC : ZFC OD→ZFC = record { ZFSet = HOD @@ -47,42 +78,42 @@ -- infixr 230 _∩_ _∪_ isZFC : IsZFC (HOD ) _∋_ _=h=_ od∅ Select isZFC = record { - choice-func = λ A {X} not A∋X → a-choice (choice-func X not ); - choice = λ A {X} A∋X not → is-in (choice-func X not) + choice-func = λ A {X} not A∋X → ord→od (a-choice (choice-func X not) ); + choice = λ A {X} A∋X not → oo∋ (is-in (choice-func X not)) } where -- -- the axiom choice from LEM and OD ordering -- - choice-func : (X : HOD ) → ¬ ( X =h= od∅ ) → choiced X + choice-func : (X : HOD ) → ¬ ( X =h= od∅ ) → choiced (od→ord X) choice-func X not = have_to_find where - ψ : ( ox : Ordinal ) → Set (suc n) - ψ ox = (( x : Ordinal ) → x o< ox → ( ¬ odef X x )) ∨ choiced X + ψ : ( ox : Ordinal ) → Set n + ψ ox = (( x : Ordinal ) → x o< ox → ( ¬ odef X x )) ∨ choiced (od→ord X) lemma-ord : ( ox : Ordinal ) → ψ ox - lemma-ord ox = TransFinite1 {ψ} induction ox where - ∋-p : (A x : HOD ) → Dec ( A ∋ x ) - ∋-p A x with p∨¬p (Lift (suc n) ( A ∋ x )) -- LEM - ∋-p A x | case1 (lift t) = yes t - ∋-p A x | case2 t = no (λ x → t (lift x )) - ∀-imply-or : {A : Ordinal → Set n } {B : Set (suc n) } + lemma-ord ox = TransFinite {ψ} induction ox where + -- ∋-p : (A x : HOD ) → Dec ( A ∋ x ) + -- ∋-p A x with p∨¬p (Lift (suc n) ( A ∋ x )) -- LEM + -- ∋-p A x | case1 (lift t) = yes t + -- ∋-p A x | case2 t = no (λ x → t (lift x )) + ∀-imply-or : {A : Ordinal → Set n } {B : Set n } → ((x : Ordinal ) → A x ∨ B) → ((x : Ordinal ) → A x) ∨ B - ∀-imply-or {A} {B} ∀AB with p∨¬p (Lift ( suc n ) ((x : Ordinal ) → A x)) -- LEM - ∀-imply-or {A} {B} ∀AB | case1 (lift t) = case1 t - ∀-imply-or {A} {B} ∀AB | case2 x = case2 (lemma (λ not → x (lift not ))) where + ∀-imply-or {A} {B} ∀AB with p∨¬p ((x : Ordinal ) → A x) -- LEM + ∀-imply-or {A} {B} ∀AB | case1 t = case1 t + ∀-imply-or {A} {B} ∀AB | case2 x = case2 (lemma (λ not → x not )) where lemma : ¬ ((x : Ordinal ) → A x) → B lemma not with p∨¬p B lemma not | case1 b = b lemma not | case2 ¬b = ⊥-elim (not (λ x → dont-orb (∀AB x) ¬b )) induction : (x : Ordinal) → ((y : Ordinal) → y o< x → ψ y) → ψ x induction x prev with ∋-p X ( ord→od x) - ... | yes p = case2 ( record { a-choice = ord→od x ; is-in = p } ) + ... | yes p = case2 ( record { a-choice = x ; is-in = ∋oo p } ) ... | no ¬p = lemma where - lemma1 : (y : Ordinal) → (y o< x → odef X y → ⊥) ∨ choiced X + lemma1 : (y : Ordinal) → (y o< x → odef X y → ⊥) ∨ choiced (od→ord X) lemma1 y with ∋-p X (ord→od y) - lemma1 y | yes y<X = case2 ( record { a-choice = ord→od y ; is-in = y<X } ) + lemma1 y | yes y<X = case2 ( record { a-choice = y ; is-in = ∋oo y<X } ) lemma1 y | no ¬y<X = case1 ( λ lt y<X → ¬y<X (subst (λ k → odef X k ) (sym diso) y<X ) ) - lemma : ((y : Ordinals.ord O) → (O Ordinals.o< y) x → odef X y → ⊥) ∨ choiced X + lemma : ((y : Ordinals.ord O) → (O Ordinals.o< y) x → odef X y → ⊥) ∨ choiced (od→ord X) lemma = ∀-imply-or lemma1 - have_to_find : choiced X + have_to_find : choiced (od→ord X) have_to_find = dont-or (lemma-ord (od→ord X )) ¬¬X∋x where ¬¬X∋x : ¬ ((x : Ordinal) → x o< (od→ord X) → odef X x → ⊥) ¬¬X∋x nn = not record { @@ -104,11 +135,11 @@ open _∧_ induction : {x : HOD} → ({y : HOD} → x ∋ y → (u : HOD ) → (u∋x : u ∋ y) → Minimal u ) → (u : HOD ) → (u∋x : u ∋ x) → Minimal u - induction {x} prev u u∋x with p∨¬p ((y : HOD) → ¬ (x ∋ y) ∧ (u ∋ y)) + induction {x} prev u u∋x with p∨¬p ((y : Ordinal ) → ¬ (odef x y) ∧ (odef u y)) ... | case1 P = record { min = x - ; x∋min = u∋x - ; min-empty = P + ; x∋min = u∋x + ; min-empty = λ y → P (od→ord y) } ... | case2 NP = min2 where p : HOD @@ -116,25 +147,25 @@ lemma : {y : Ordinal} → OD.def (od x) y ∧ OD.def (od u) y → y o< omin (odmax x) (odmax u) lemma {y} lt = min1 (<odmax x (proj1 lt)) (<odmax u (proj2 lt)) np : ¬ (p =h= od∅) - np p∅ = NP (λ y p∋y → ∅< {p} {_} p∋y p∅ ) - y1choice : choiced p + np p∅ = NP (λ y p∋y → ∅< {p} {_} (subst (λ k → odef p k) (sym diso) p∋y) p∅ ) + y1choice : choiced (od→ord p) y1choice = choice-func p np y1 : HOD - y1 = a-choice y1choice + y1 = ord→od (a-choice y1choice) y1prop : (x ∋ y1) ∧ (u ∋ y1) - y1prop = is-in y1choice + y1prop = oo∋ (is-in y1choice) min2 : Minimal u min2 = prev (proj1 y1prop) u (proj2 y1prop) Min2 : (x : HOD) → (u : HOD ) → (u∋x : u ∋ x) → Minimal u - Min2 x u u∋x = (ε-induction1 {λ y → (u : HOD ) → (u∋x : u ∋ y) → Minimal u } induction x u u∋x ) - cx : {x : HOD} → ¬ (x =h= od∅ ) → choiced x + Min2 x u u∋x = (ε-induction {λ y → (u : HOD ) → (u∋x : u ∋ y) → Minimal u } induction x u u∋x ) + cx : {x : HOD} → ¬ (x =h= od∅ ) → choiced (od→ord x ) cx {x} nx = choice-func x nx minimal : (x : HOD ) → ¬ (x =h= od∅ ) → HOD - minimal x ne = min (Min2 (a-choice (cx {x} ne) ) x (is-in (cx ne))) + minimal x ne = min (Min2 (ord→od (a-choice (cx {x} ne) )) x ( oo∋ (is-in (cx ne))) ) x∋minimal : (x : HOD ) → ( ne : ¬ (x =h= od∅ ) ) → odef x ( od→ord ( minimal x ne ) ) - x∋minimal x ne = x∋min (Min2 (a-choice (cx {x} ne) ) x (is-in (cx ne))) + x∋minimal x ne = x∋min (Min2 (ord→od (a-choice (cx {x} ne) )) x ( oo∋ (is-in (cx ne))) ) minimal-1 : (x : HOD ) → ( ne : ¬ (x =h= od∅ ) ) → (y : HOD ) → ¬ ( odef (minimal x ne) (od→ord y)) ∧ (odef x (od→ord y) ) - minimal-1 x ne y = min-empty (Min2 (a-choice (cx ne) ) x (is-in (cx ne))) y + minimal-1 x ne y = min-empty (Min2 (ord→od (a-choice (cx ne) )) x ( oo∋ (is-in (cx ne)))) y
--- a/OD.agda Thu Jul 23 17:50:28 2020 +0900 +++ b/OD.agda Sat Jul 25 09:09:00 2020 +0900 @@ -76,9 +76,6 @@ -- -- ==→o≡ is necessary to prove axiom of extensionality. -data One {n : Level } : Set n where - OneObj : One - -- Ordinals in OD , the maximum Ords : OD Ords = record { def = λ x → One } @@ -274,6 +271,12 @@ open _⊆_ infixr 220 _⊆_ +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 } + od⊆→o≤ : {x y : HOD } → x ⊆ y → od→ord x o< osuc (od→ord y) od⊆→o≤ {x} {y} lt = ⊆→o≤ {x} {y} (λ {z} x>z → subst (λ k → def (od y) k ) diso (incl lt (subst (λ k → def (od x) k ) (sym diso) x>z ))) @@ -317,14 +320,14 @@ ε-induction-ord ox {oy} lt = TransFinite {λ oy → ψ (ord→od oy)} induction oy -- level trick (what'a shame) -ε-induction1 : { ψ : HOD → Set (suc n)} - → ( {x : HOD } → ({ y : HOD } → x ∋ y → ψ y ) → ψ x ) - → (x : HOD ) → ψ x -ε-induction1 {ψ} ind x = subst (λ k → ψ k ) oiso (ε-induction-ord (osuc (od→ord x)) <-osuc ) where - induction : (ox : Ordinal) → ((oy : Ordinal) → oy o< ox → ψ (ord→od oy)) → ψ (ord→od ox) - induction ox prev = ind ( λ {y} lt → subst (λ k → ψ k ) oiso (prev (od→ord y) (o<-subst (c<→o< lt) refl diso ))) - ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (ord→od oy) - ε-induction-ord ox {oy} lt = TransFinite1 {λ oy → ψ (ord→od oy)} induction oy +-- ε-induction1 : { ψ : HOD → Set (suc n)} +-- → ( {x : HOD } → ({ y : HOD } → x ∋ y → ψ y ) → ψ x ) +-- → (x : HOD ) → ψ x +-- ε-induction1 {ψ} ind x = subst (λ k → ψ k ) oiso (ε-induction-ord (osuc (od→ord x)) <-osuc ) where +-- induction : (ox : Ordinal) → ((oy : Ordinal) → oy o< ox → ψ (ord→od oy)) → ψ (ord→od ox) +-- induction ox prev = ind ( λ {y} lt → subst (λ k → ψ k ) oiso (prev (od→ord y) (o<-subst (c<→o< lt) refl diso ))) +-- ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (ord→od oy) +-- ε-induction-ord ox {oy} lt = TransFinite1 {λ oy → ψ (ord→od oy)} induction oy Select : (X : HOD ) → ((x : HOD ) → Set n ) → HOD Select X ψ = record { od = record { def = λ x → ( odef X x ∧ ψ ( ord→od x )) } ; odmax = odmax X ; <odmax = λ y → <odmax X (proj1 y) }
--- a/ODC.agda Thu Jul 23 17:50:28 2020 +0900 +++ b/ODC.agda Sat Jul 25 09:09:00 2020 +0900 @@ -79,6 +79,13 @@ ... | yes p = p ... | no ¬p = ⊥-elim ( notnot ¬p ) +open _⊆_ + +power→⊆ : ( A t : HOD) → Power A ∋ t → t ⊆ A +power→⊆ A t PA∋t = record { incl = λ {x} t∋x → double-neg-eilm (t1 t∋x) } where + t1 : {x : HOD } → t ∋ x → ¬ ¬ (A ∋ x) + t1 = zf.IsZF.power→ isZF A t PA∋t + OrdP : ( x : Ordinal ) ( y : HOD ) → Dec ( Ord x ∋ y ) OrdP x y with trio< x (od→ord y) OrdP x y | tri< a ¬b ¬c = no ¬c
--- a/Ordinals.agda Thu Jul 23 17:50:28 2020 +0900 +++ b/Ordinals.agda Sat Jul 25 09:09:00 2020 +0900 @@ -24,9 +24,6 @@ TransFinite : { ψ : ord → Set n } → ( (x : ord) → ( (y : ord ) → y o< x → ψ y ) → ψ x ) → ∀ (x : ord) → ψ x - TransFinite1 : { ψ : ord → Set (suc n) } - → ( (x : ord) → ( (y : ord ) → y o< x → ψ y ) → ψ x ) - → ∀ (x : ord) → ψ x record IsNext {n : Level } (ord : Set n) (o∅ : ord ) (osuc : ord → ord ) (_o<_ : ord → ord → Set n) (next : ord → ord ) : Set (suc (suc n)) where field @@ -65,7 +62,6 @@ osuc-≡< = IsOrdinals.osuc-≡< (Ordinals.isOrdinal O) <-osuc = IsOrdinals.<-osuc (Ordinals.isOrdinal O) TransFinite = IsOrdinals.TransFinite (Ordinals.isOrdinal O) - TransFinite1 = IsOrdinals.TransFinite1 (Ordinals.isOrdinal O) x<nx = IsNext.x<nx (Ordinals.isNext O) osuc<nx = IsNext.osuc<nx (Ordinals.isNext O)
--- a/filter.agda Thu Jul 23 17:50:28 2020 +0900 +++ b/filter.agda Sat Jul 25 09:09:00 2020 +0900 @@ -7,12 +7,9 @@ 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 @@ -50,17 +47,6 @@ 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 ) @@ -179,447 +165,6 @@ ; 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 where - i0 : Two - i1 : Two - -data Three : Set where - j0 : Three - j1 : Three - j2 : Three - -open import Data.List hiding (map) - -import OPair -open OPair O - -record PFunc {n : Level} : 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 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) - -findp : List Three → (x : Nat) → Set -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 - -Findp=n : (h : Three) → (n : List Three) → {x : Nat} {p : Findp n x } → find n x p ≡ find (h ∷ n) (Suc x) (vn p) -Findp=n j0 n {x} {p} = refl -Findp=n j1 n {x} {p} = refl -Findp=n j2 n {x} {p} = refl - -findpeq : (n : List Three) → {x : Nat} {p q : Findp n x } → find n x p ≡ find n x q -findpeq n {0} {v0} {v0} = refl -findpeq n {0} {v1} {v1} = refl -findpeq [] {Suc x} {()} -findpeq (h ∷ n) {Suc x} {vn p} {vn q} = subst₂ (λ j k → j ≡ k ) (Findp=n h n) (Findp=n h n) (findpeq n {x} {p} {q}) - -3List→PFunc : List Three → PFunc -3List→PFunc fp = record { dom = λ x → findp fp x ; map = λ x p → find fp x p ; meq = λ {x} {p} {q} → findpeq fp } - -_3⊆b_ : (f g : List Three) → Bool -[] 3⊆b [] = true -[] 3⊆b (j2 ∷ g) = [] 3⊆b g -[] 3⊆b (_ ∷ g) = true -(j2 ∷ f) 3⊆b [] = f 3⊆b [] -(j2 ∷ f) 3⊆b (_ ∷ g) = f 3⊆b g -(j0 ∷ f) 3⊆b (j0 ∷ g) = f 3⊆b g -(j1 ∷ f) 3⊆b (j1 ∷ g) = f 3⊆b g -_ 3⊆b _ = false - -_3⊆_ : (f g : List Three) → Set -f 3⊆ g = (f 3⊆b g) ≡ true - -_3∩_ : (f g : List Three) → List Three -[] 3∩ (j2 ∷ g) = j2 ∷ ([] 3∩ g) -[] 3∩ g = [] -(j2 ∷ f) 3∩ [] = j2 ∷ f 3∩ [] -f 3∩ [] = [] -(j0 ∷ f) 3∩ (j0 ∷ g) = j0 ∷ ( f 3∩ g ) -(j1 ∷ f) 3∩ (j1 ∷ g) = j1 ∷ ( f 3∩ g ) -(_ ∷ f) 3∩ (_ ∷ g) = j2 ∷ ( f 3∩ g ) - -3∩⊆f : { f g : List Three } → (f 3∩ g ) 3⊆ f -3∩⊆f {[]} {[]} = refl -3∩⊆f {[]} {j0 ∷ g} = refl -3∩⊆f {[]} {j1 ∷ g} = refl -3∩⊆f {[]} {j2 ∷ g} = 3∩⊆f {[]} {g} -3∩⊆f {j0 ∷ f} {[]} = refl -3∩⊆f {j1 ∷ f} {[]} = refl -3∩⊆f {j2 ∷ f} {[]} = 3∩⊆f {f} {[]} -3∩⊆f {j0 ∷ f} {j1 ∷ g} = 3∩⊆f {f} {g} -3∩⊆f {j1 ∷ f} {j0 ∷ g} = 3∩⊆f {f} {g} -3∩⊆f {j0 ∷ f} {j0 ∷ g} = 3∩⊆f {f} {g} -3∩⊆f {j1 ∷ f} {j1 ∷ g} = 3∩⊆f {f} {g} -3∩⊆f {j2 ∷ f} {j0 ∷ g} = 3∩⊆f {f} {g} -3∩⊆f {j2 ∷ f} {j1 ∷ g} = 3∩⊆f {f} {g} -3∩⊆f {j0 ∷ f} {j2 ∷ g} = 3∩⊆f {f} {g} -3∩⊆f {j1 ∷ f} {j2 ∷ g} = 3∩⊆f {f} {g} -3∩⊆f {j2 ∷ f} {j2 ∷ g} = 3∩⊆f {f} {g} - -3∩sym : { f g : List Three } → (f 3∩ g ) ≡ (g 3∩ f ) -3∩sym {[]} {[]} = refl -3∩sym {[]} {j0 ∷ g} = refl -3∩sym {[]} {j1 ∷ g} = refl -3∩sym {[]} {j2 ∷ g} = cong (λ k → j2 ∷ k) (3∩sym {[]} {g}) -3∩sym {j0 ∷ f} {[]} = refl -3∩sym {j1 ∷ f} {[]} = refl -3∩sym {j2 ∷ f} {[]} = cong (λ k → j2 ∷ k) (3∩sym {f} {[]}) -3∩sym {j0 ∷ f} {j0 ∷ g} = cong (λ k → j0 ∷ k) (3∩sym {f} {g}) -3∩sym {j0 ∷ f} {j1 ∷ g} = cong (λ k → j2 ∷ k) (3∩sym {f} {g}) -3∩sym {j0 ∷ f} {j2 ∷ g} = cong (λ k → j2 ∷ k) (3∩sym {f} {g}) -3∩sym {j1 ∷ f} {j0 ∷ g} = cong (λ k → j2 ∷ k) (3∩sym {f} {g}) -3∩sym {j1 ∷ f} {j1 ∷ g} = cong (λ k → j1 ∷ k) (3∩sym {f} {g}) -3∩sym {j1 ∷ f} {j2 ∷ g} = cong (λ k → j2 ∷ k) (3∩sym {f} {g}) -3∩sym {j2 ∷ f} {j0 ∷ g} = cong (λ k → j2 ∷ k) (3∩sym {f} {g}) -3∩sym {j2 ∷ f} {j1 ∷ g} = cong (λ k → j2 ∷ k) (3∩sym {f} {g}) -3∩sym {j2 ∷ f} {j2 ∷ g} = cong (λ k → j2 ∷ k) (3∩sym {f} {g}) - -3⊆-[] : { h : List Three } → [] 3⊆ h -3⊆-[] {[]} = refl -3⊆-[] {j0 ∷ h} = refl -3⊆-[] {j1 ∷ h} = refl -3⊆-[] {j2 ∷ h} = 3⊆-[] {h} - -3⊆trans : { f g h : List Three } → f 3⊆ g → g 3⊆ h → f 3⊆ h -3⊆trans {[]} {[]} {[]} f<g g<h = refl -3⊆trans {[]} {[]} {j0 ∷ h} f<g g<h = refl -3⊆trans {[]} {[]} {j1 ∷ h} f<g g<h = refl -3⊆trans {[]} {[]} {j2 ∷ h} f<g g<h = 3⊆trans {[]} {[]} {h} refl g<h -3⊆trans {[]} {j2 ∷ g} {[]} f<g g<h = refl -3⊆trans {[]} {j0 ∷ g} {j0 ∷ h} f<g g<h = refl -3⊆trans {[]} {j1 ∷ g} {j1 ∷ h} f<g g<h = refl -3⊆trans {[]} {j2 ∷ g} {j0 ∷ h} f<g g<h = refl -3⊆trans {[]} {j2 ∷ g} {j1 ∷ h} f<g g<h = refl -3⊆trans {[]} {j2 ∷ g} {j2 ∷ h} f<g g<h = 3⊆trans {[]} {g} {h} f<g g<h -3⊆trans {j2 ∷ f} {[]} {[]} f<g g<h = f<g -3⊆trans {j2 ∷ f} {[]} {j0 ∷ h} f<g g<h = 3⊆trans {f} {[]} {h} f<g (3⊆-[] {h}) -3⊆trans {j2 ∷ f} {[]} {j1 ∷ h} f<g g<h = 3⊆trans {f} {[]} {h} f<g (3⊆-[] {h}) -3⊆trans {j2 ∷ f} {[]} {j2 ∷ h} f<g g<h = 3⊆trans {f} {[]} {h} f<g g<h -3⊆trans {j0 ∷ f} {j0 ∷ g} {[]} f<g () -3⊆trans {j0 ∷ f} {j1 ∷ g} {[]} f<g () -3⊆trans {j0 ∷ f} {j2 ∷ g} {[]} () g<h -3⊆trans {j1 ∷ f} {j0 ∷ g} {[]} f<g () -3⊆trans {j1 ∷ f} {j1 ∷ g} {[]} f<g () -3⊆trans {j1 ∷ f} {j2 ∷ g} {[]} () g<h -3⊆trans {j2 ∷ f} {j2 ∷ g} {[]} f<g g<h = 3⊆trans {f} {g} {[]} f<g g<h -3⊆trans {j0 ∷ f} {j0 ∷ g} {j0 ∷ h} f<g g<h = 3⊆trans {f} {g} {h} f<g g<h -3⊆trans {j1 ∷ f} {j1 ∷ g} {j1 ∷ h} f<g g<h = 3⊆trans {f} {g} {h} f<g g<h -3⊆trans {j2 ∷ f} {j0 ∷ g} {j0 ∷ h} f<g g<h = 3⊆trans {f} {g} {h} f<g g<h -3⊆trans {j2 ∷ f} {j1 ∷ g} {j1 ∷ h} f<g g<h = 3⊆trans {f} {g} {h} f<g g<h -3⊆trans {j2 ∷ f} {j2 ∷ g} {j0 ∷ h} f<g g<h = 3⊆trans {f} {g} {h} f<g g<h -3⊆trans {j2 ∷ f} {j2 ∷ g} {j1 ∷ h} f<g g<h = 3⊆trans {f} {g} {h} f<g g<h -3⊆trans {j2 ∷ f} {j2 ∷ g} {j2 ∷ h} f<g g<h = 3⊆trans {f} {g} {h} f<g g<h - -3⊆∩f : { f g h : List Three } → f 3⊆ g → f 3⊆ h → f 3⊆ (g 3∩ h ) -3⊆∩f {[]} {[]} {[]} f<g f<h = refl -3⊆∩f {[]} {[]} {x ∷ h} f<g f<h = 3⊆-[] {[] 3∩ (x ∷ h)} -3⊆∩f {[]} {x ∷ g} {h} f<g f<h = 3⊆-[] {(x ∷ g) 3∩ h} -3⊆∩f {j2 ∷ f} {[]} {[]} f<g f<h = 3⊆∩f {f} {[]} {[]} f<g f<h -3⊆∩f {j2 ∷ f} {[]} {j0 ∷ h} f<g f<h = f<g -3⊆∩f {j2 ∷ f} {[]} {j1 ∷ h} f<g f<h = f<g -3⊆∩f {j2 ∷ f} {[]} {j2 ∷ h} f<g f<h = 3⊆∩f {f} {[]} {h} f<g f<h -3⊆∩f {j0 ∷ f} {j0 ∷ g} {j0 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h -3⊆∩f {j1 ∷ f} {j1 ∷ g} {j1 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h -3⊆∩f {j2 ∷ f} {j0 ∷ g} {[]} f<g f<h = f<h -3⊆∩f {j2 ∷ f} {j0 ∷ g} {j0 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h -3⊆∩f {j2 ∷ f} {j0 ∷ g} {j1 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h -3⊆∩f {j2 ∷ f} {j0 ∷ g} {j2 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h -3⊆∩f {j2 ∷ f} {j1 ∷ g} {[]} f<g f<h = f<h -3⊆∩f {j2 ∷ f} {j1 ∷ g} {j0 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h -3⊆∩f {j2 ∷ f} {j1 ∷ g} {j1 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h -3⊆∩f {j2 ∷ f} {j1 ∷ g} {j2 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h -3⊆∩f {j2 ∷ f} {j2 ∷ g} {[]} f<g f<h = 3⊆∩f {f} {g} {[]} f<g f<h -3⊆∩f {j2 ∷ f} {j2 ∷ g} {j0 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h -3⊆∩f {j2 ∷ f} {j2 ∷ g} {j1 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h -3⊆∩f {j2 ∷ f} {j2 ∷ g} {j2 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h - -3↑22 : (f : Nat → Two) (i j : Nat) → List Three -3↑22 f Zero j = [] -3↑22 f (Suc i) j with f j -3↑22 f (Suc i) j | i0 = j0 ∷ 3↑22 f i (Suc j) -3↑22 f (Suc i) j | i1 = j1 ∷ 3↑22 f i (Suc j) - -_3↑_ : (Nat → Two) → Nat → List Three -_3↑_ f i = 3↑22 f i 0 - -3↑< : {f : Nat → Two} → { x y : Nat } → x ≤ y → (_3↑_ f x) 3⊆ (_3↑_ f y) -3↑< {f} {x} {y} x<y = lemma x y 0 x<y where - lemma : (x y i : Nat) → x ≤ y → (3↑22 f x i ) 3⊆ (3↑22 f y i ) - lemma 0 y i z≤n with f i - lemma Zero Zero i z≤n | i0 = refl - lemma Zero (Suc y) i z≤n | i0 = 3⊆-[] {3↑22 f (Suc y) i} - lemma Zero Zero i z≤n | i1 = refl - lemma Zero (Suc y) i z≤n | i1 = 3⊆-[] {3↑22 f (Suc y) i} - lemma (Suc x) (Suc y) i (s≤s x<y) with f i - lemma (Suc x) (Suc y) i (s≤s x<y) | i0 = lemma x y (Suc i) x<y - lemma (Suc x) (Suc y) i (s≤s x<y) | i1 = lemma x y (Suc i) x<y - -Finite3b : (p : List Three ) → Bool -Finite3b [] = true -Finite3b (j0 ∷ f) = Finite3b f -Finite3b (j1 ∷ f) = Finite3b f -Finite3b (j2 ∷ f) = false - -finite3cov : (p : List Three ) → List Three -finite3cov [] = [] -finite3cov (j0 ∷ x) = j0 ∷ finite3cov x -finite3cov (j1 ∷ x) = j1 ∷ finite3cov x -finite3cov (j2 ∷ x) = j0 ∷ finite3cov x - -Dense-3 : F-Dense (List Three) (λ x → One) _3⊆_ _3∩_ -Dense-3 = record { - dense = λ x → Finite3b x ≡ true - ; d⊆P = OneObj - ; dense-f = λ x → finite3cov x - ; dense-d = λ {p} d → lemma1 p - ; dense-p = λ {p} d → lemma2 p - } where - lemma1 : (p : List Three ) → Finite3b (finite3cov p) ≡ true - lemma1 [] = refl - lemma1 (j0 ∷ p) = lemma1 p - lemma1 (j1 ∷ p) = lemma1 p - lemma1 (j2 ∷ p) = lemma1 p - lemma2 : (p : List Three) → p 3⊆ finite3cov p - lemma2 [] = refl - lemma2 (j0 ∷ p) = lemma2 p - lemma2 (j1 ∷ p) = lemma2 p - lemma2 (j2 ∷ p) = lemma2 p - -record 3Gf (f : Nat → Two) (p : List Three ) : Set where - field - 3gn : Nat - 3f<n : p 3⊆ (f 3↑ 3gn) - -open 3Gf - -min = Data.Nat._⊓_ --- m≤m⊔n = Data.Nat._⊔_ -open import Data.Nat.Properties - -3GF : {n : Level } → (Nat → Two ) → F-Filter (List Three) (λ x → One) _3⊆_ _3∩_ -3GF {n} f = record { - filter = λ p → 3Gf f p - ; f⊆P = OneObj - ; filter1 = λ {p} {q} _ fp p⊆q → lemma1 p q fp p⊆q - ; filter2 = λ {p} {q} fp fq → record { 3gn = min (3gn fp) (3gn fq) ; 3f<n = lemma2 p q fp fq } - } where - lemma1 : (p q : List Three ) → (fp : 3Gf f p) → (p⊆q : p 3⊆ q) → 3Gf f q - lemma1 p q fp p⊆q = record { 3gn = 3gn fp ; 3f<n = {!!} } - lemma2 : (p q : List Three ) → (fp : 3Gf f p) → (fq : 3Gf f q) → (p 3∩ q) 3⊆ (f 3↑ min (3gn fp) (3gn fq)) - lemma2 p q fp fq = {!!} - -record _f⊆_ {n : Level } (f g : PFunc {n} ) : 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⊆_ - -_f∩_ : {n : Level} → (f g : PFunc {n} ) → PFunc {n} -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 } - -_↑_ : {n : Level} → (Nat → Two) → Nat → PFunc {n} -_↑_ {n} f i = record { dom = λ x → Lift n (x ≤ i) ; map = λ x _ → f x ; meq = λ {x} {p} {q} → refl } - -record Gf {n : Level} (f : Nat → Two) (p : PFunc {n} ) : Set (suc n) where - field - gn : Nat - f<n : (f ↑ gn) f⊆ p - -record FiniteF {n : Level} (p : PFunc {n} ) : 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 = {!!} ; map = {!!} } --- ; dense-d = λ {p} d → {!!} --- ; dense-p = λ {p} d → {!!} --- } - -open Gf - -GF : {n : Level } → (Nat → Two ) → F-Filter (PFunc {n}) (λ x → Lift (suc n) (One {n}) ) _f⊆_ _f∩_ -GF {n} 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 {n} } → (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 {n} } → (fp : Gf {n} f p ) → (fq : Gf {n} 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 : PFunc {n} - 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 - -3→Hω2 : List Three → HOD -3→Hω2 t = list→hod t 0 where - list→hod : List Three → Nat → HOD - list→hod [] _ = od∅ - list→hod (j0 ∷ t) i = Union (< nat→ω i , nat→ω 0 > , ( list→hod t (Suc i) )) - list→hod (j1 ∷ t) i = Union (< nat→ω i , nat→ω 1 > , ( list→hod t (Suc i) )) - list→hod (j2 ∷ t) i = list→hod t (Suc i ) - -Hω2→3 : (x : HOD) → HODω2 ∋ x → List Three -Hω2→3 x = lemma where - lemma : { y : Ordinal } → Hω2r y → List Three - lemma record { count = 0 ; hω2 = hφ } = [] - lemma record { count = (Suc i) ; hω2 = (h0 hω3) } = j0 ∷ lemma record { count = i ; hω2 = hω3 } - lemma record { count = (Suc i) ; hω2 = (h1 hω3) } = j1 ∷ lemma record { count = i ; hω2 = hω3 } - lemma record { count = (Suc i) ; hω2 = (he hω3) } = j2 ∷ 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) )) - -record Gfo (x : Ordinal) : Set n where - field - gfunc : Ordinal - gmax : Ordinal - gcond : (odef ω→2 gfunc) ∧ (odef infinite gmax) - gfdef : {!!} -- ( ↑n (ord→od gfunc) (ord→od gmax) (subst₂ ? ? ? gcond) ) ⊆ ord→od x - pcond : odef HODω2 x - -open Gfo - -HODGf : HOD -HODGf = record { od = record { def = λ x → Gfo x } ; odmax = next o∅ ; <odmax = {!!} } - -G : (Nat → Two) → Filter HODω2 -G f = record { - filter = HODGf - ; 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 = {!!} } - - -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 GenericFilter (P : HOD) : Set (suc n) where field @@ -632,12 +177,3 @@ Intersection : (D : F-Dense L PL _⊆_ _∩_ ) → { x : L } → F-Dense.dense D x → L Generic : (D : F-Dense L PL _⊆_ _∩_ ) → { x : L } → ( y : F-Dense.dense D x) → F-Filter.filter GFilter (Intersection D y ) -data PD (P : HOD) (C : CountableOrdinal) : (x : Ordinal) (n : Nat) → Set (suc n) where - pd0 : (p : Ordinal ) → odef (ord→od P) p → PD C p 0 - pdq : {q pnx : Ordinal } {n : Nat} → (pn : PD P C pnx n ) → odef (ctl→ C n) q → ord→od p0x ⊆ ord→od q → PD P C q (suc n) - -P-GenericFilter : {P : HOD} → (C : CountableOrdinal) → GenericFilter P -P-GenericFilter {P} C = record { - genf = record { filter = {!!} ; f⊆PL = {!!} ; filter1 = {!!} ; filter2 = {!!} } - ; generic = λ D → {!!} - }
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/generic-filter.agda Sat Jul 25 09:09:00 2020 +0900 @@ -0,0 +1,269 @@ +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 Gf (f : Nat → Two) (p : PFunc (Lift n Nat) (Lift n Two) ) : Set (suc n) where + field + gn : Nat + f<n : (f ↑ gn) f⊆ p + +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 Gf +open _f⊆_ +open import Data.Nat.Properties + +GF : (Nat → Two ) → F-Filter (PFunc (Lift n Nat) (Lift n Two)) (λ x → Lift (suc n) (One {n}) ) _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 (Lift n Nat) (Lift n Two) } → (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)} → pmap (f ↑ gn fp) (lift x) fr ≡ pmap q (lift x) (extend p⊆q (extend (f<n fp) fr)) + lemma {x} {fr} = begin + pmap (f ↑ gn fp) (lift x) fr + ≡⟨ feq (f<n fp ) ⟩ + pmap p (lift x) (extend (f<n fp) fr) + ≡⟨ feq p⊆q ⟩ + pmap q (lift x) (extend p⊆q (extend (f<n fp) fr)) + ∎ where open ≡-Reasoning + f2 : {p q : PFunc (Lift n Nat) (Lift n Two) } → (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 : PFunc (Lift n Nat) (Lift n Two) + fmin = f ↑ (min (gn fp) (gn fq)) + lemma1 : {x : Nat} → ( x<g : Lift n (x ≤ min (gn fp) (gn fq)) ) → (fr : dom p (lift x)) (gr : dom q (lift x)) → pmap p (lift x) fr ≡ pmap q (lift x) gr + lemma1 {x} x<g fr gr = begin + pmap p (lift x) fr + ≡⟨ meq p ⟩ + pmap p (lift x) (extend (f<n fp) (lift ( ≤-trans (lower x<g) (m⊓n≤m _ _)))) + ≡⟨ sym (feq (f<n fp)) ⟩ + pmap (f ↑ (min (gn fp) (gn fq))) (lift x) x<g + ≡⟨ feq (f<n fq) ⟩ + pmap q (lift x) (extend (f<n fq) (lift ( ≤-trans (lower x<g) (m⊓n≤n _ _)))) + ≡⟨ meq q ⟩ + pmap q (lift x) gr + ∎ where open ≡-Reasoning + lemma2 : {x : Nat} → ( x<g : Lift n (x ≤ min (gn fp) (gn fq)) ) → dom (p f∩ q) (lift 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 (Lift n Nat) (Lift n Two) ) → (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))) → pmap (f ↑ min (gn fp) (gn fq)) (lift x) fr ≡ pmap (p f∩ q) (lift x) (lemma2 fr) + lemma3 {x} fr = + pmap (f ↑ min (gn fp) (gn fq)) (lift x) fr + ≡⟨ feq (f<n fq) ⟩ + pmap q (lift x) (extend (f<n fq) ( lift (≤-trans (lower fr) (m⊓n≤n _ _)) )) + ≡⟨ sym (feq (f∩→⊆ p q ) {x} {lemma2 fr} ) ⟩ + pmap (p f∩ q) (lift 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 + +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) )) + +record Gfo (x : Ordinal) : Set n where + field + gfunc : Ordinal + gmax : Ordinal + gcond : (odef ω→2 gfunc) ∧ (odef infinite gmax) + gfdef : {!!} -- ( ↑n (ord→od gfunc) (ord→od gmax) (subst₂ ? ? ? gcond) ) ⊆ ord→od x + pcond : odef HODω2 x + +open Gfo + +HODGf : HOD +HODGf = record { od = record { def = λ x → Gfo x } ; odmax = next o∅ ; <odmax = {!!} } + +G : (Nat → Two) → Filter HODω2 +G f = record { + filter = HODGf + ; 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 = {!!} } + + +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 + +open CountableOrdinal + +PGOD : (i : Nat) → (C : CountableOrdinal) → (p : Ordinal) → ( q : Ordinal ) → Set n +PGOD i C p q = ¬ ( odef (ord→od (ctl→ C i)) q ∧ ( (x : Ordinal ) → odef (ord→od p) x → odef (ord→od q) x )) + +PGHOD : (i : Nat) → (C : CountableOrdinal) → (p : Ordinal) → HOD +PGHOD i C p = record { od = record { def = λ x → PGOD i C {!!} {!!} } ; odmax = {!!} ; <odmax = {!!} } + +ord-compare : (i : Nat) → (C : CountableOrdinal) → (p : Ordinal) → ( q : Ordinal ) → Ordinal +ord-compare i C p q with ODC.p∨¬p O ( (q : Ordinal ) → PGOD i C p q ) +ord-compare i C p q | case1 y = p +ord-compare i C p q | case2 n = od→ord (ODC.minimal O (PGHOD i C p ) (∅< (subst₂ (λ j k → odef j {!!} ) refl {!!} n)) ) + +data PD (P : HOD) (C : CountableOrdinal) : (x : Ordinal) (i : Nat) → Set (suc n) where + pd0 : PD P C o∅ 0 + -- pdq : {q pnx : Ordinal } {n : Nat} → (pn : PD P C pnx n ) → odef (ctl→ C n) q → ord→od p0x ⊆ ord→od q → PD P C q (suc n) + +P-GenericFilter : {P : HOD} → (C : CountableOrdinal) → GenericFilter P +P-GenericFilter {P} C = record { + genf = record { filter = {!!} ; f⊆PL = {!!} ; filter1 = {!!} ; filter2 = {!!} } + ; generic = λ D → {!!} + }
--- a/logic.agda Thu Jul 23 17:50:28 2020 +0900 +++ b/logic.agda Sat Jul 25 09:09:00 2020 +0900 @@ -5,6 +5,12 @@ open import Relation.Binary open import Data.Empty +data One {n : Level } : Set n where + OneObj : One + +data Two : Set where + i0 : Two + i1 : Two data Bool : Set where true : Bool
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/partfunc.agda Sat Jul 25 09:09:00 2020 +0900 @@ -0,0 +1,233 @@ +{-# OPTIONS --allow-unsolved-metas #-} +open import Level +open import Relation.Nullary +open import Relation.Binary.PropositionalEquality +open import Ordinals +module partfunc {n : Level } (O : Ordinals {n}) where + +open import logic +open import Relation.Binary +open import Data.Empty +open import Data.List +open import Data.Maybe +open import Relation.Binary +open import Relation.Binary.Core +open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) +open import filter O + +open _∧_ +open _∨_ +open Bool + + +record PFunc (Dom : Set n) (Cod : Set n) : Set (suc n) where + field + dom : Dom → Set n + pmap : (x : Dom ) → dom x → Cod + meq : {x : Dom } → { p q : dom x } → pmap x p ≡ pmap x q + + +data Findp : {Cod : Set n} → List (Maybe Cod) → (x : Nat) → Set where + v0 : {Cod : Set n} → {f : List (Maybe Cod)} → ( v : Cod ) → Findp ( just v ∷ f ) Zero + vn : {Cod : Set n} → {f : List (Maybe Cod)} {d : Maybe Cod} → {x : Nat} → Findp f x → Findp (d ∷ f) (Suc x) + +open PFunc + +find : {Cod : Set n} → (f : List (Maybe Cod) ) → (x : Nat) → Findp f x → Cod +find (just v ∷ _) 0 (v0 v) = v +find (_ ∷ n) (Suc i) (vn p) = find n i p + +findpeq : {Cod : Set n} → (f : List (Maybe Cod)) → {x : Nat} {p q : Findp f x } → find f x p ≡ find f x q +findpeq n {0} {v0 _} {v0 _} = refl +findpeq [] {Suc x} {()} +findpeq (just x₁ ∷ n) {Suc x} {vn p} {vn q} = findpeq n {x} {p} {q} +findpeq (nothing ∷ n) {Suc x} {vn p} {vn q} = findpeq n {x} {p} {q} + +List→PFunc : {Cod : Set n} → List (Maybe Cod) → PFunc (Lift n Nat) Cod +List→PFunc fp = record { dom = λ x → Lift n (Findp fp (lower x)) + ; pmap = λ x y → find fp (lower x) (lower y) + ; meq = λ {x} {p} {q} → findpeq fp {lower x} {lower p} {lower q} + } + +_3⊆b_ : (f g : List (Maybe Two)) → Bool +[] 3⊆b [] = true +[] 3⊆b (nothing ∷ g) = [] 3⊆b g +[] 3⊆b (_ ∷ g) = true +(nothing ∷ f) 3⊆b [] = f 3⊆b [] +(nothing ∷ f) 3⊆b (_ ∷ g) = f 3⊆b g +(just i0 ∷ f) 3⊆b (just i0 ∷ g) = f 3⊆b g +(just i1 ∷ f) 3⊆b (just i1 ∷ g) = f 3⊆b g +_ 3⊆b _ = false + +_3⊆_ : (f g : List (Maybe Two)) → Set +f 3⊆ g = (f 3⊆b g) ≡ true + +_3∩_ : (f g : List (Maybe Two)) → List (Maybe Two) +[] 3∩ (nothing ∷ g) = nothing ∷ ([] 3∩ g) +[] 3∩ g = [] +(nothing ∷ f) 3∩ [] = nothing ∷ f 3∩ [] +f 3∩ [] = [] +(just i0 ∷ f) 3∩ (just i0 ∷ g) = just i0 ∷ ( f 3∩ g ) +(just i1 ∷ f) 3∩ (just i1 ∷ g) = just i1 ∷ ( f 3∩ g ) +(_ ∷ f) 3∩ (_ ∷ g) = nothing ∷ ( f 3∩ g ) + +3∩⊆f : { f g : List (Maybe Two) } → (f 3∩ g ) 3⊆ f +3∩⊆f {[]} {[]} = refl +3∩⊆f {[]} {just _ ∷ g} = refl +3∩⊆f {[]} {nothing ∷ g} = 3∩⊆f {[]} {g} +3∩⊆f {just _ ∷ f} {[]} = refl +3∩⊆f {nothing ∷ f} {[]} = 3∩⊆f {f} {[]} +3∩⊆f {just i0 ∷ f} {just i0 ∷ g} = 3∩⊆f {f} {g} +3∩⊆f {just i1 ∷ f} {just i1 ∷ g} = 3∩⊆f {f} {g} +3∩⊆f {just i0 ∷ f} {just i1 ∷ g} = 3∩⊆f {f} {g} +3∩⊆f {just i1 ∷ f} {just i0 ∷ g} = 3∩⊆f {f} {g} +3∩⊆f {nothing ∷ f} {just _ ∷ g} = 3∩⊆f {f} {g} +3∩⊆f {just i0 ∷ f} {nothing ∷ g} = 3∩⊆f {f} {g} +3∩⊆f {just i1 ∷ f} {nothing ∷ g} = 3∩⊆f {f} {g} +3∩⊆f {nothing ∷ f} {nothing ∷ g} = 3∩⊆f {f} {g} + +3∩sym : { f g : List (Maybe Two) } → (f 3∩ g ) ≡ (g 3∩ f ) +3∩sym {[]} {[]} = refl +3∩sym {[]} {just _ ∷ g} = refl +3∩sym {[]} {nothing ∷ g} = cong (λ k → nothing ∷ k) (3∩sym {[]} {g}) +3∩sym {just _ ∷ f} {[]} = refl +3∩sym {nothing ∷ f} {[]} = cong (λ k → nothing ∷ k) (3∩sym {f} {[]}) +3∩sym {just i0 ∷ f} {just i0 ∷ g} = cong (λ k → just i0 ∷ k) (3∩sym {f} {g}) +3∩sym {just i0 ∷ f} {just i1 ∷ g} = cong (λ k → nothing ∷ k) (3∩sym {f} {g}) +3∩sym {just i1 ∷ f} {just i0 ∷ g} = cong (λ k → nothing ∷ k) (3∩sym {f} {g}) +3∩sym {just i1 ∷ f} {just i1 ∷ g} = cong (λ k → just i1 ∷ k) (3∩sym {f} {g}) +3∩sym {just i0 ∷ f} {nothing ∷ g} = cong (λ k → nothing ∷ k) (3∩sym {f} {g}) +3∩sym {just i1 ∷ f} {nothing ∷ g} = cong (λ k → nothing ∷ k) (3∩sym {f} {g}) +3∩sym {nothing ∷ f} {just i0 ∷ g} = cong (λ k → nothing ∷ k) (3∩sym {f} {g}) +3∩sym {nothing ∷ f} {just i1 ∷ g} = cong (λ k → nothing ∷ k) (3∩sym {f} {g}) +3∩sym {nothing ∷ f} {nothing ∷ g} = cong (λ k → nothing ∷ k) (3∩sym {f} {g}) + +3⊆-[] : { h : List (Maybe Two) } → [] 3⊆ h +3⊆-[] {[]} = refl +3⊆-[] {just _ ∷ h} = refl +3⊆-[] {nothing ∷ h} = 3⊆-[] {h} + +3⊆trans : { f g h : List (Maybe Two) } → f 3⊆ g → g 3⊆ h → f 3⊆ h +3⊆trans {[]} {[]} {[]} f<g g<h = refl +3⊆trans {[]} {[]} {just _ ∷ h} f<g g<h = refl +3⊆trans {[]} {[]} {nothing ∷ h} f<g g<h = 3⊆trans {[]} {[]} {h} refl g<h +3⊆trans {[]} {nothing ∷ g} {[]} f<g g<h = refl +3⊆trans {[]} {just _ ∷ g} {just _ ∷ h} f<g g<h = refl +3⊆trans {[]} {nothing ∷ g} {just _ ∷ h} f<g g<h = refl +3⊆trans {[]} {nothing ∷ g} {nothing ∷ h} f<g g<h = 3⊆trans {[]} {g} {h} f<g g<h +3⊆trans {nothing ∷ f} {[]} {[]} f<g g<h = f<g +3⊆trans {nothing ∷ f} {[]} {just _ ∷ h} f<g g<h = 3⊆trans {f} {[]} {h} f<g (3⊆-[] {h}) +3⊆trans {nothing ∷ f} {[]} {nothing ∷ h} f<g g<h = 3⊆trans {f} {[]} {h} f<g g<h +3⊆trans {nothing ∷ f} {nothing ∷ g} {[]} f<g g<h = 3⊆trans {f} {g} {[]} f<g g<h +3⊆trans {nothing ∷ f} {nothing ∷ g} {just _ ∷ h} f<g g<h = 3⊆trans {f} {g} {h} f<g g<h +3⊆trans {nothing ∷ f} {nothing ∷ g} {nothing ∷ h} f<g g<h = 3⊆trans {f} {g} {h} f<g g<h +3⊆trans {[]} {just i0 ∷ g} {[]} f<g () +3⊆trans {[]} {just i1 ∷ g} {[]} f<g () +3⊆trans {[]} {just x ∷ g} {nothing ∷ h} f<g g<h = 3⊆-[] {h} +3⊆trans {just i0 ∷ f} {[]} {h} () g<h +3⊆trans {just i1 ∷ f} {[]} {h} () g<h +3⊆trans {just x ∷ f} {just i0 ∷ g} {[]} f<g () +3⊆trans {just x ∷ f} {just i1 ∷ g} {[]} f<g () +3⊆trans {just i0 ∷ f} {just i0 ∷ g} {just i0 ∷ h} f<g g<h = 3⊆trans {f} {g} {h} f<g g<h +3⊆trans {just i1 ∷ f} {just i1 ∷ g} {just i1 ∷ h} f<g g<h = 3⊆trans {f} {g} {h} f<g g<h +3⊆trans {just x ∷ f} {just i0 ∷ g} {nothing ∷ h} f<g () +3⊆trans {just x ∷ f} {just i1 ∷ g} {nothing ∷ h} f<g () +3⊆trans {just i0 ∷ f} {nothing ∷ g} {_} () g<h +3⊆trans {just i1 ∷ f} {nothing ∷ g} {_} () g<h +3⊆trans {nothing ∷ f} {just i0 ∷ g} {[]} f<g () +3⊆trans {nothing ∷ f} {just i1 ∷ g} {[]} f<g () +3⊆trans {nothing ∷ f} {just i0 ∷ g} {just i0 ∷ h} f<g g<h = 3⊆trans {f} {g} {h} f<g g<h +3⊆trans {nothing ∷ f} {just i1 ∷ g} {just i1 ∷ h} f<g g<h = 3⊆trans {f} {g} {h} f<g g<h +3⊆trans {nothing ∷ f} {just i0 ∷ g} {nothing ∷ h} f<g () +3⊆trans {nothing ∷ f} {just i1 ∷ g} {nothing ∷ h} f<g () + +3⊆∩f : { f g h : List (Maybe Two) } → f 3⊆ g → f 3⊆ h → f 3⊆ (g 3∩ h ) +3⊆∩f {[]} {[]} {[]} f<g f<h = refl +3⊆∩f {[]} {[]} {x ∷ h} f<g f<h = 3⊆-[] {[] 3∩ (x ∷ h)} +3⊆∩f {[]} {x ∷ g} {h} f<g f<h = 3⊆-[] {(x ∷ g) 3∩ h} +3⊆∩f {nothing ∷ f} {[]} {[]} f<g f<h = 3⊆∩f {f} {[]} {[]} f<g f<h +3⊆∩f {nothing ∷ f} {[]} {just _ ∷ h} f<g f<h = f<g +3⊆∩f {nothing ∷ f} {[]} {nothing ∷ h} f<g f<h = 3⊆∩f {f} {[]} {h} f<g f<h +3⊆∩f {just i0 ∷ f} {just i0 ∷ g} {just i0 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h +3⊆∩f {just i1 ∷ f} {just i1 ∷ g} {just i1 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h +3⊆∩f {nothing ∷ f} {just _ ∷ g} {[]} f<g f<h = f<h +3⊆∩f {nothing ∷ f} {just i0 ∷ g} {just i0 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h +3⊆∩f {nothing ∷ f} {just i0 ∷ g} {just i1 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h +3⊆∩f {nothing ∷ f} {just i1 ∷ g} {just i0 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h +3⊆∩f {nothing ∷ f} {just i1 ∷ g} {just i1 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h +3⊆∩f {nothing ∷ f} {just i0 ∷ g} {nothing ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h +3⊆∩f {nothing ∷ f} {just i1 ∷ g} {nothing ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h +3⊆∩f {nothing ∷ f} {nothing ∷ g} {[]} f<g f<h = 3⊆∩f {f} {g} {[]} f<g f<h +3⊆∩f {nothing ∷ f} {nothing ∷ g} {just _ ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h +3⊆∩f {nothing ∷ f} {nothing ∷ g} {nothing ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h + +3↑22 : (f : Nat → Two) (i j : Nat) → List (Maybe Two) +3↑22 f Zero j = [] +3↑22 f (Suc i) j = just (f j) ∷ 3↑22 f i (Suc j) + +_3↑_ : (Nat → Two) → Nat → List (Maybe Two) +_3↑_ f i = 3↑22 f i 0 + +3↑< : {f : Nat → Two} → { x y : Nat } → x ≤ y → (_3↑_ f x) 3⊆ (_3↑_ f y) +3↑< {f} {x} {y} x<y = lemma x y 0 x<y where + lemma : (x y i : Nat) → x ≤ y → (3↑22 f x i ) 3⊆ (3↑22 f y i ) + lemma 0 y i z≤n with f i + lemma Zero Zero i z≤n | i0 = refl + lemma Zero (Suc y) i z≤n | i0 = 3⊆-[] {3↑22 f (Suc y) i} + lemma Zero Zero i z≤n | i1 = refl + lemma Zero (Suc y) i z≤n | i1 = 3⊆-[] {3↑22 f (Suc y) i} + lemma (Suc x) (Suc y) i (s≤s x<y) with f i + lemma (Suc x) (Suc y) i (s≤s x<y) | i0 = lemma x y (Suc i) x<y + lemma (Suc x) (Suc y) i (s≤s x<y) | i1 = lemma x y (Suc i) x<y + +Finite3b : (p : List (Maybe Two) ) → Bool +Finite3b [] = true +Finite3b (just _ ∷ f) = Finite3b f +Finite3b (nothing ∷ f) = false + +finite3cov : (p : List (Maybe Two) ) → List (Maybe Two) +finite3cov [] = [] +finite3cov (just y ∷ x) = just y ∷ finite3cov x +finite3cov (nothing ∷ x) = just i0 ∷ finite3cov x + +Dense-3 : F-Dense (List (Maybe Two) ) (λ x → One) _3⊆_ _3∩_ +Dense-3 = record { + dense = λ x → Finite3b x ≡ true + ; d⊆P = OneObj + ; dense-f = λ x → finite3cov x + ; dense-d = λ {p} d → lemma1 p + ; dense-p = λ {p} d → lemma2 p + } where + lemma1 : (p : List (Maybe Two) ) → Finite3b (finite3cov p) ≡ true + lemma1 [] = refl + lemma1 (just i0 ∷ p) = lemma1 p + lemma1 (just i1 ∷ p) = lemma1 p + lemma1 (nothing ∷ p) = lemma1 p + lemma2 : (p : List (Maybe Two)) → p 3⊆ finite3cov p + lemma2 [] = refl + lemma2 (just i0 ∷ p) = lemma2 p + lemma2 (just i1 ∷ p) = lemma2 p + lemma2 (nothing ∷ p) = lemma2 p + +record 3Gf (f : Nat → Two) (p : List (Maybe Two)) : Set where + field + 3gn : Nat + 3f<n : p 3⊆ (f 3↑ 3gn) + +open 3Gf + +min = Data.Nat._⊓_ +-- m≤m⊔n = Data.Nat._⊔_ +open import Data.Nat.Properties + +3GF : {n : Level } → (Nat → Two ) → F-Filter (List (Maybe Two)) (λ x → One) _3⊆_ _3∩_ +3GF {n} f = record { + filter = λ p → 3Gf f p + ; f⊆P = OneObj + ; filter1 = λ {p} {q} _ fp p⊆q → lemma1 p q fp p⊆q + ; filter2 = λ {p} {q} fp fq → record { 3gn = min (3gn fp) (3gn fq) ; 3f<n = lemma2 p q fp fq } + } where + lemma1 : (p q : List (Maybe Two) ) → (fp : 3Gf f p) → (p⊆q : p 3⊆ q) → 3Gf f q + lemma1 p q fp p⊆q = record { 3gn = 3gn fp ; 3f<n = {!!} } + lemma2 : (p q : List (Maybe Two) ) → (fp : 3Gf f p) → (fq : 3Gf f q) → (p 3∩ q) 3⊆ (f 3↑ min (3gn fp) (3gn fq)) + lemma2 p q fp fq = ?