Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff partfunc.agda @ 387:8b0715e28b33
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sat, 25 Jul 2020 09:09:00 +0900 |
parents | filter.agda@24a66a246316 |
children | 19687f3304c9 |
line wrap: on
line diff
--- /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 = ?