Members/kono/Proof/ZF-in-agda: filter.agda comparison

comparison 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

comparison

equal deleted inserted replaced

-:853ead1b56b8
+:7b6592f0851a
 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
-incl :  dense ⊆ Power P
+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
 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 )
--------
---    the set of finite partial functions from ω to 2
---
---
-import OPair
-open OPair O
-data Two : Set n where
-i0 : Two
-i1 : Two
-record PFunc : Set (suc n) where
-field
-restrict : Nat → Set n
-map : (x : Nat ) → restrict x → Two
-open PFunc
-record _f⊆_ (f g : PFunc) : Set (suc n) where
-field
-extend : (x : Nat) → (fr : restrict f x ) →  restrict g x
-feq : (x : Nat) → (fr : restrict f x ) →  map f x fr ≡ map g x (extend x fr)
-open _f⊆_
 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
 ; 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 { restrict = λ x → (restrict f x ) ∧ (restrict g x ) ∧ ((fr : restrict f x ) → (gr : restrict g x ) → map f x fr ≡ map g x gr)
+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) }
+; map = λ x p →  map f x (proj1 p) ; meq = meq f }
 _↑_ : (Nat → Two) → Nat → PFunc
-f ↑ i = record { restrict = λ x → Lift n (x ≤ i) ; map = λ x _ → f x }
+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 {
 ; 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 x (extend (f<n fp ) x x<g) ; feq = λ x fr → {!!} } where
+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 → record {
+f2 {p} {q} fp fq  = record { extend = λ  {x} x<g → lemma2 x<g ; feq = λ {x} {fr} → lemma3 fr } where
-proj1 = extend (f<n fp ) x (lift ( ≤-trans (lower x<g) (m⊓n≤m _ _)))
+fmin =  f ↑  (min (gn fp) (gn fq))
-; proj2 = record {proj1 = extend (f<n fq ) x (lift ( ≤-trans (lower x<g) (m⊓n≤n _ _)))
+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
-;                 proj2 = {!!} }}  ;
+lemma1 {x} x<g fr gr = begin
-feq = λ x fr → {!!} } where
+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
 ... | 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 p⊆i → Replace infinite (λ x i∋x → < x , repl p x > )) where
+ω→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

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

comparison filter.agda @ 379:7b6592f0851a