{-# 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 hiding (filter) 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