module NaPa.Worlds where
open import Data.Nat using (ℕ; zero; suc; pred) renaming (_+_ to _+ℕ_)
open import Data.List using (List; []; _∷_; replicate; _++_)
open import Data.Bool using (Bool; true; false)
open import Data.Empty using (⊥)
open import Data.Unit using (⊤)
open import Function using (id)
open import Relation.Nullary using (¬_)
open import Relation.Binary.PropositionalEquality as ≡
record WorldSymantics (W : Set) : Set where
field
ø : W
_↑1 _+1 : (α : W) → W
_^1 : (α : W) → W
_^1 = _↑1
Abs : (α : W) → W
Abs = _↑1
module WorldOps {World} (Wsym : WorldSymantics World) where
open WorldSymantics Wsym
infixl 6 _↑_ _+[_]
_+[_] : World → ℕ → World
α +[ 0 ] = α
α +[ suc n ] = (α +[ n ])+1
_↑_ : World → ℕ → World
α ↑ 0 = α
α ↑ suc n = (α ↑ n)↑1
_^[_] : World → ℕ → World
_^[_] = _↑_
module ListBoolSpecialized where
infixl 6 _↑_
World : Set
World = List Bool
_+[_] : World → ℕ → World
α +[ k ] = replicate k false ++ α
_↑_ : World → ℕ → World
α ↑ k = replicate k true ++ α
module ListBoolWorlds where
World : Set
World = List Bool
listBoolWorlds : WorldSymantics (List Bool)
listBoolWorlds = record { ø = ø; _↑1 = _↑1; _+1 = _+1 }
where
ø : World
ø = []
_+1 : World → World
α +1 = false ∷ α
_↑1 : World → World
α ↑1 = true ∷ α
_∈_ : ℕ → World → Set
_ ∈ [] = ⊥
zero ∈ (false ∷ _) = ⊥
zero ∈ (true ∷ _) = ⊤
suc n ∈ (_ ∷ xs) = n ∈ xs
_∉_ : ℕ → World → Set
x ∉ α = ¬(x ∈ α)
infix 2 _∈_ _∉_
∈-uniq : ∀ {x} α (p q : x ∈ α) → p ≡ q
∈-uniq [] () _
∈-uniq {zero} (false ∷ xs) () _
∈-uniq {zero} (true ∷ xs) _ _ = ≡.refl
∈-uniq {suc n} (_ ∷ xs) p q = ∈-uniq {n} xs p q
private
module Unused where
open WorldSymantics listBoolWorlds
open WorldOps listBoolWorlds
x∉ø+ : ∀ x k → x ∉ (ø +[ k ])
x∉ø+ zero zero ()
x∉ø+ (suc _) zero ()
x∉ø+ zero (suc k) ()
x∉ø+ (suc n) (suc k) pf = x∉ø+ n k pf
∈false∷ : ∀ x {xs} → x ∈ false ∷ xs → pred x ∈ xs
∈false∷ zero = λ()
∈false∷ (suc n) = id