{-# OPTIONS --universe-polymorphism #-}
module NaPa where
open import Level
open import Irrelevance
import Relation.Binary.PropositionalEquality.NP as ≡
open ≡ using (_≡_; _≢_; _≗_; module ≗-Reasoning; module ≡-Reasoning)
open import Data.Nat.NP as Nat using (ℕ; zero; suc; s≤s; z≤n; ≤-pred; pred; _<=_; module <=)
renaming (_+_ to _+ℕ_ ; _∸_ to _∸ℕ_ ; _==_ to _==ℕ_; ¬≤ to ¬≤ℕ;
_<_ to _<ℕ_ ; _≤_ to _≤ℕ_; _≥_ to _≥ℕ_; _≤?_ to _≤?ℕ_)
open import Data.Nat.Logical using (⟦ℕ⟧; zero; suc; ⟦ℕ⟧-setoid; ⟦ℕ⟧-equality; ⟦ℕ⟧-cong)
renaming (_≟_ to _≟⟦ℕ⟧_)
import Data.Nat.Properties as Nat
open import Function
open import Function.Equality as ⟶≡ using (_⟶_; _⟨$⟩_)
open import Data.Sum.NP as Sum using (_⊎_; inj₁; inj₂; [_,_]′) renaming (map to ⊎-map)
open import Data.Bool.Extras using (Bool; true; false; if_then_else_; T; not; T'not'¬)
open import Data.Unit using (⊤)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.Product.Extras using (_,_)
open import Data.Maybe.NP using (Maybe; nothing; just; maybe)
open import Relation.Binary.Extras as Bin
open import Relation.Nullary
open import Relation.Nullary.Decidable
import Relation.Binary.On.NP as On
open import NaPa.Worlds
open import NaPa.Subtyping
open ListBoolWorlds public
import Category.Monad as Cat
open Cat.RawMonad Data.Maybe.NP.monad
open Data.Maybe.NP.FunctorLemmas
private
module ℕs = Setoid ⟦ℕ⟧-setoid
module ℕe = Equality ⟦ℕ⟧-equality
infixr 4 _,_
record Name α : Set where
constructor
_,_
field
name : ℕ
name∈α : name ∈ α
open Name public
mkName : ∀ {α} (x : ℕ) → x ∈ α → Name α
mkName x pf = x , pf
infix 4 _≡nm_ _≟nm_ _==nm_
_≡nm_ : ∀ {α} (x y : Name α) → Set
_≡nm_ = ⟦ℕ⟧ on name
_≟nm_ : ∀ {α} → Decidable (_≡nm_ {α})
x ≟nm y = name x ≟⟦ℕ⟧ name y
_==nm_ : ∀ {α} (x y : Name α) → Bool
_==nm_ x y = name x ==ℕ name y
name-injective : ∀ {α} {x y : Name α} → name x ≡ name y → x ≡ y
name-injective {α} {_ , p₁} {a , p₂} eq rewrite eq
= ≡.cong (_,_ a) (∈-uniq α p₁ p₂)
Nm : World → Setoid zero zero
Nm α = On.setoid (name {α}) ℕs.isEquivalence
nm-equality : ∀ {α} → Equality (_≡nm_ {α})
nm-equality {α}
= record { isEquivalence = Setoid.isEquivalence (Nm α)
; subst = λ P → ≡.subst P ∘ name-injective ∘ Equality.to-propositional ⟦ℕ⟧-equality }
module NmEq {α} = Equality (nm-equality {α})
≡nm⇒≡ : ∀ {α} → _≡nm_ {α} ⇒ _≡_
≡nm⇒≡ = NmEq.to-propositional
≡nm-cong : ∀ {α β} (f : Name α → Name β) → _≡nm_ =[ f ]⇒ _≡nm_
≡nm-cong f = NmEq.reflexive ∘ ≡.cong f ∘ ≡nm⇒≡
≡nm-⟦ℕ⟧-cong : ∀ {α} (f : Name α → ℕ) → _≡nm_ =[ f ]⇒ ⟦ℕ⟧
≡nm-⟦ℕ⟧-cong f = ℕe.reflexive ∘ ≡.cong f ∘ ≡nm⇒≡
≡-⟦ℕ⟧-cong : ∀ {a} {A : Set a} (f : A → ℕ) → _≡_ =[ f ]⇒ ⟦ℕ⟧
≡-⟦ℕ⟧-cong f = ℕe.reflexive ∘ ≡.cong f
≡nm-≡-cong : ∀ {a α} {A : Set a} (f : Name α → A) → _≡nm_ =[ f ]⇒ _≡_
≡nm-≡-cong f = ≡.cong f ∘ ≡nm⇒≡
⟦ℕ⟧-≡nm-cong : ∀ {α} (f : ℕ → Name α) → ⟦ℕ⟧ =[ f ]⇒ _≡nm_
⟦ℕ⟧-≡nm-cong f = NmEq.reflexive ∘ ≡.cong f ∘ ℕe.to-propositional
⟦ℕ⟧-≡-cong : ∀ {a} {A : Set a} (f : ℕ → A) → ⟦ℕ⟧ =[ f ]⇒ _≡_
⟦ℕ⟧-≡-cong f = ≡.cong f ∘ ℕe.to-propositional
module ≡nm-Reasoning {α} = Bin.Setoid-Reasoning (Nm α)
open WorldSymantics listBoolWorlds public
open WorldOps listBoolWorlds public
open WorldOps listBoolWorlds using () renaming (_+[_] to _+_)
open NaPa.Subtyping.⊆-Pack `⊆`-pack public
open NaPa.Subtyping.SyntacticOnBools ⊆ᵇ-pack public hiding (minimalSymantics)
ze : ∀ {α} → Name (α ↑1)
ze = 0 , _
¬Nameø : ¬(Name ø)
¬Nameø (_ , ())
_+nm_ : ∀ {α} (x : Name α) k → Name (α + k)
_+nm_ {α} x k = k +ℕ name x , proof k where
proof : ∀ k → k +ℕ name x ∈ α + k
proof zero = name∈α x
proof (suc k) = proof k
infixl 6 _+nm_
subtract : ∀ {α} k (x : Name (α + k)) → Name α
subtract k x = name x ∸ℕ k , proof (name x) k (name∈α x) where
proof : ∀ {α} x k → (x ∈ α + k) → (x ∸ℕ k ∈ α)
proof x zero = id
proof zero (suc k) = λ()
proof (suc x) (suc k) = proof x k
infixl 4 subtract
syntax subtract k x = x ∸nm k
coe : ∀ {α β} → α ⊆ β → Name α → Name β
coe α⊆β x = name x , `⊆`-sound α⊆β (name x) (name∈α x)
infix 0 _because⟨_⟩
_because⟨_⟩ : ∀ {α β} → Name α → α ⊆ β → Name β
_because⟨_⟩ n pf = coe pf n
add : ∀ {α} k → Name α → Name (α + k)
add k x = x +nm k
add↑ : ∀ {α} k → Name α → Name (α ↑ k)
add↑ k x = x +nm k because⟨ ⊆-+-↑ k ⟩
su : ∀ {α} → Name α → Name (α +1)
su x = x +nm 1
su↑ : ∀ {α} → Name α → Name (α ↑1)
su↑ = add↑ 1
private
lem-<k : ∀ {α β x k} → x ≤ℕ k → x ∈ (α ↑ suc k) → x ∈ (β ↑ suc k)
lem-<k z≤n = _
lem-<k (s≤s m≤n) = lem-<k m≤n
lem-≥k : ∀ {α x k} → x ≥ℕ k → x ∈ α ↑ k → x ∈ α + k
lem-≥k z≤n = id
lem-≥k (s≤s m≤n) = lem-≥k m≤n
lem-<k? : ∀ {α β n} k → n ∈ β ↑ k → n ∈ (if suc n <= k then α ↑ k else β + k)
lem-<k? {n = n} k with suc n <= k | <=.sound (suc n) k | <=.complete {suc n} {k}
... | true | n<k | _ = lem-<k (n<k _)
... | false | _ | ¬n<k = lem-≥k (¬≤ℕ ¬n<k)
>nm-bool : ∀ {α} k → Name (α ↑ k) → Bool
>nm-bool k x = suc (name x) <= k
syntax >nm-bool k x = x <nm-bool k
>nm-name : ∀ {α} k (x : Name (α ↑ k)) → Name (if >nm-bool k x then ø ↑ k else α + k)
>nm-name k x = name x , lem-<k? k (name∈α x)
syntax >nm-name k x = x <nm-name k
>nm-name∈α : ∀ {α} k (x : Name (α ↑ k)) → name x ∈ (if >nm-bool k x then ø ↑ k else α + k)
>nm-name∈α k x = lem-<k? k (name∈α x)
syntax >nm-name∈α k x = x <nm-name∈α k
>nm : ∀ {α} k → Name (α ↑ k) → Name (ø ↑ k) ⊎ Name (α + k)
>nm k x with >nm-bool k x | >nm-name∈α k x
... | true | pf = inj₁ (name x , pf)
... | false | pf = inj₂ (name x , pf)
infix 4 >nm
syntax >nm k x = x <nm k
>nm-ind : ∀ {ℓ α} k (x : Name (α ↑ k))
(P : (Name (ø ↑ k) ⊎ Name (α + k)) → Set ℓ)
(Pinj₁ : T (>nm-bool k x) → ∀ pf → P (inj₁ (name x , pf)))
(Pinj₂ : T (not (>nm-bool k x)) → ∀ pf → P (inj₂ (name x , pf)))
→ P (>nm k x)
>nm-ind k x P p₁ p₂
with >nm-bool k x | >nm-name∈α k x
... | true | pf = p₁ _ pf
... | false | pf = p₂ _ pf
easy->nm : ∀ {α} k → Name (α ↑ k) → Name (ø ↑ k) ⊎ Name (α + k)
easy->nm zero x = inj₂ x
easy->nm (suc _) (zero , _) = inj₁ (zero , _)
easy->nm (suc k) (suc x , pf) = ⊎-map su↑ su (easy->nm k (x , pf))
syntax easy->nm k x = x <nm-easy k
easy->nm≗>nm : ∀ {α} k → easy->nm {α} k ≗ >nm k
easy->nm≗>nm zero x = ≡.cong inj₂ (name-injective ≡.refl)
easy->nm≗>nm (suc n) (zero , _) = ≡.refl
easy->nm≗>nm {α} (suc n) (suc x , pf) rewrite easy->nm≗>nm n (x , pf) = helper n x pf
where
helper : ∀ k x pf → ⊎-map su↑ su (>nm {α} k (x , pf)) ≡ >nm (suc k) (suc x , pf)
helper k x pf = >nm-ind k (x , pf) (λ r → ⊎-map su↑ su r ≡ >nm (suc k) (suc x , pf))
(λ h pf' → >nm-ind (suc k) (suc x , pf) (λ r → inj₁ (suc x , pf') ≡ r)
(λ _ _ → ≡.cong inj₁ (name-injective ≡.refl))
(λ h' → ⊥-elim (T'not'¬ h' h)))
(λ h pf' → >nm-ind (suc k) (suc x , pf) (λ r → inj₂ (suc x , pf') ≡ r)
(λ h' → ⊥-elim (T'not'¬ h h'))
(λ _ _ → ≡.cong inj₂ (name-injective ≡.refl)))
lift↑1 : ∀ {α β} → (Name α → Name β) → Name (α ↑1) → Name (β ↑1)
lift↑1 f x with name x | name∈α x
... | zero | _ = zero , _
... | suc m | pf = su↑ (f (m , pf))
ze↑1+ : ∀ {α} k → Name (α ↑ (1 +ℕ k))
ze↑1+ _ = ze
infix 10 #_
#_ : ∀ {α} k → Name (α ↑ suc k)
#_ {α} k = ze +nm k because⟨ α ↑1 +[ k ] ⊆⟨ ⊆-+-↑ k ⟩
α ↑1 ↑ k ⊆⟨ ⊆-exch-↑-↑ ⊆-refl 1 k ⟩∎
α ↑ suc k ∎ ⟩
where open ⊆-Reasoning
private
module CoeExamples where
nmα+→nmα↑ : ∀ {α} k → Name (α + k) → Name (α ↑ k)
nmα+→nmα↑ k = coe (⊆-ctx-+↑ ⊆-refl k)
module Unused where
open import Data.List using ([]; _∷_; replicate; _++_)
n∈trueⁿ⁺¹ : ∀ {α} n → n ∈ replicate (suc n) true ++ α
n∈trueⁿ⁺¹ zero = _
n∈trueⁿ⁺¹ (suc n) = n∈trueⁿ⁺¹ n
predNm : ∀ {α} → Name (α +1) → Name α
predNm = subtract 1
Name→-to-Nm⟶ : ∀ {b₁ b₂ α} {B : Setoid b₁ b₂} →
(Name α → Setoid.Carrier B) → Nm α ⟶ B
Name→-to-Nm⟶ {α = α} {B} f = record { _⟨$⟩_ = f; cong = cong′ }
where
open Setoid B renaming (_≈_ to _≈B_)
cong≡ : ∀ {x y} → x ≡ y → f x ≈B f y
cong≡ ≡.refl = Setoid.refl B
cong′ : ∀ {x y} → x ≡nm y → f x ≈B f y
cong′ = cong≡ ∘ Equality.to-propositional nm-equality
¬Name : ∀ {α} → α ⊆ ø → ¬(Name α)
¬Name α⊆ø = ¬Nameø ∘ coe α⊆ø
Name-elim : ∀ {a} {A : Set a} {α} (α⊆ø : α ⊆ ø) (x : Name α) → A
Name-elim x y with ¬Name x y
... | ()
Nameø-elim : ∀ {a} {A : Set a} → Name ø → A
Nameø-elim = Name-elim ⊆-refl
¬Nameø+ : ∀ k → ¬(Name (ø + k))
¬Nameø+ = ¬Name ∘ α⊆ø→α+⊆ø ⊆-ø-bottom
Nameø+-elim : ∀ {a} {A : Set a} k → Name (ø + k) → A
Nameø+-elim = Name-elim ∘ α⊆ø→α+⊆ø ⊆-ø-bottom
Nameø↑→Nameα↑ : ∀ {k} → Name (ø ↑ k) → ∀ {α} → Name (α ↑ k)
Nameø↑→Nameα↑ {k} x = coe (⊆-cong-↑ ⊆-ø-bottom k) x
exportName : ∀ {α} k → Name (α ↑ k) → Maybe (Name α)
exportName k x = [ const nothing , just ∘′ subtract k ]′ (x <nm k)
impNm : ∀ (ℓ k n : ℕ) → ℕ
impNm ℓ k n = if suc n <= ℓ then n else n +ℕ k
importName : ∀ {α β} ℓ k → α + k ⊆ β → Name (α ↑ ℓ) → Name (β ↑ ℓ)
importName ℓ k pf n
with n <nm ℓ
... | inj₁ n′ = n′ because⟨ ⊆-cong-↑ ø-bottom ℓ ⟩
... | inj₂ n′ = n′ +nm k because⟨ ⊆-trans (⊆-exch-+-+ ⊆-refl ℓ k) (⊆-ctx-+↑ pf ℓ) ⟩
module Singletons where
SWorld : ℕ → World
SWorld n = ø ↑1 + n
SName : ℕ → Set
SName = Name ∘ SWorld
sName : ∀ n → SName n
sName n = ze +nm n
_+sn_ : ∀ {n} → SName n → ∀ k → SName (k +ℕ n)
_+sn_ {n} x k = x +nm k because⟨ ⊆-assoc-+ ⊆-refl n k ⟩
subtract-sn : ∀ {n} k → SName (k +ℕ n) → SName n
subtract-sn {n} k x = x′ ∸nm k
where x′ = x because⟨ ⊆-assoc-+′ ⊆-refl n k ⟩
infixl 4 subtract-sn
syntax subtract-sn k x = x ∸sn k
coe-names : ∀ {α β} (α⊆β : α ⊆ β) → name ∘ coe α⊆β ≗ name
coe-names = λ _ _ → ≡.refl
<nm-names : ∀ {α k} {x : Name (α ↑ k)} → [ name , name ]′ (x <nm k) ≡ name x
<nm-names {α} {k} {x} with x <nm-bool k | x <nm-name∈α k
... | true | _ = ≡.refl
... | false | _ = ≡.refl
Dec-≡nm→≡ : ∀ {α} → Decidable (_≡nm_ {α}) → Decidable _≡_
Dec-≡nm→≡ _≟_ x y with x ≟ y
... | yes x≡y = yes (≡nm⇒≡ x≡y)
... | no x≢y = no (x≢y ∘′ ℕs.reflexive ∘′ ≡.cong name)
importName-ℓ-0≡coe : ∀ {α β} ℓ (pf : α ⊆ β) n → name (importName ℓ 0 pf n) ≡ name n
importName-ℓ-0≡coe ℓ pf x with x <nm-bool ℓ | x <nm-name∈α ℓ
... | true | _ = ≡.refl
... | false | _ = ≡.refl
pred-impNm-comm : ∀ k x → pred (impNm 1 k (suc x)) ≡ x +ℕ k
pred-impNm-comm k x = ≡.refl
.import11-export1-comm :
∀ {α β} (pf : α +1 ⊆ β) (x : Name (α ↑1)) →
exportName 1 (importName 1 1 pf x) ≡ coe pf ∘ su <$> exportName 1 x
import11-export1-comm {α} pf x
= <$>-injective₁ name-injective (≡.trans (helper (name x) {name∈α x} (suc (name x) ≤?ℕ 1)) (<$>-assoc (exportName 1 x)))
where
.helper : ∀ n {pn : n ∈ α ↑1} → Dec (n <ℕ 1) → let x = n , pn in
name <$> (exportName 1 (importName 1 1 pf x)) ≡ name ∘ (coe pf ∘ su) <$> exportName 1 x
helper zero (no ¬p) = ⊥-elim (¬p (s≤s z≤n))
helper .0 (yes (s≤s z≤n)) = ≡.refl
helper (suc _) (no _) = ≡.refl
1+ : ∀ {α} → Name α → Name (α +1)
1+ x = x +nm 1
module Name↑⇔Fin where
open import Data.Fin as Fin
⇒ : ∀ n → Name (ø ↑ n) → Fin n
⇒ zero = Nameø-elim
⇒ (suc n) = maybe (suc ∘′ ⇒ n) zero ∘ exportName 1
⇐ : ∀ {α n} → Fin n → Name (α ↑ n)
⇐ (zero {n}) = ze↑1+ n
⇐ (suc i) = su↑ (⇐ i)
module WorldSyntax where
data `World` : Set where
_`↑1` _`+1` : (`α` : `World`) → `World`
`ø` : `World`
_`↑`_ : (`α` : `World`) (k : ℕ) → `World`
`α` `↑` zero = `α`
`α` `↑` suc n = (`α` `↑` n) `↑1`
_`+`_ : (`α` : `World`) (k : ℕ) → `World`
`α` `+` zero = `α`
`α` `+` suc n = (`α` `+` n) `+1`
El : `World` → World
El (`α` `↑1`) = El `α` ↑1
El (`α` `+1`) = El `α` +1
El `ø` = ø
bnd : `World` → ℕ
bnd (`α` `↑1`) = suc (bnd `α`)
bnd (`α` `+1`) = suc (bnd `α`)
bnd `ø` = 0
empty? : `World` → Set
empty? (`α` `↑1`) = ⊥
empty? (`α` `+1`) = empty? `α`
empty? `ø` = ⊤
_`∈`_ : ℕ → `World` → Set
_ `∈` `ø` = ⊥
zero `∈` (`α` `↑1`) = ⊤
suc n `∈` (`α` `↑1`) = n `∈` `α`
zero `∈` (`α` `+1`) = ⊥
suc n `∈` (`α` `+1`) = n `∈` `α`
module WorldSyntaxProps where
open WorldSyntax
comm-El-↑ : ∀ `α` n → El `α` ↑ n ≡ El (`α` `↑` n)
comm-El-↑ `α` zero = ≡.refl
comm-El-↑ `α` (suc n) rewrite comm-El-↑ `α` n = ≡.refl
module ℕ⇒Name`α` where
open WorldSyntax
⇒ : ∀ `α` x → x ∈ El `α` → Name (El `α`)
⇒ (`α` `↑1`) zero _ = zero , _
⇒ (`α` `↑1`) (suc i) pf = su↑ (⇒ `α` i pf)
⇒ (`α` `+1`) zero ()
⇒ (`α` `+1`) (suc i) pf = su (⇒ `α` i pf)
⇒ `ø` _ ()
module Name`α`⇔Fin where
open import Data.Fin as F renaming (_+_ to _+F_)
open WorldSyntax
open WorldSyntaxProps
mutual
⇒+1 : ∀ `α` → Name (El `α` +1) → Fin (suc (bnd `α`))
⇒+1 `α` = F.raise 1 ∘ ⇒ `α` ∘ predNm
⇒ : ∀ `α` → Name (El `α`) → Fin (bnd `α`)
⇒ (`α` `↑1`) = [ inject+ _ ∘ Name↑⇔Fin.⇒ 1 , ⇒+1 `α` ]′ ∘ >nm 1
⇒ (`α` `+1`) = ⇒+1 `α`
⇒ `ø` = Nameø-elim
⇐₁ : ∀ {n} `α` → (x : Fin n) → toℕ x ∈ El `α` → Name (El `α`)
⇐₁ `α` = ℕ⇒Name`α`.⇒ `α` ∘ toℕ
x∈ø↑x : ∀ {n} (x : Fin n) → toℕ x ∈ (ø ↑ n)
x∈ø↑x zero = _
x∈ø↑x (suc n) = x∈ø↑x n
⇐₂ : ∀ {n} → (x : Fin n) → Name (ø ↑ n)
⇐₂ {n} x with x∈ø↑x x
... | y rewrite comm-El-↑ `ø` n = ⇐₁ (`ø` `↑` n) x y
module WellFormedWorld where
data WF : World → Set where
`ø : WF ø
_`+_ : ∀ {α} (`α : WF α) k → WF (α + k)
_`↑_ : ∀ {α} (`α : WF α) k → WF (α ↑ k)
_+↑nm_ : ∀ {α} → Name α → ∀ k → Name (α ↑ k)
_+↑nm_ x k = coe (⊆-ctx-+↑ ⊆-refl k) (x +nm k)
subtract↑ : ∀ {α} k → Name (α ↑ k) → Name (ø ↑ k) ⊎ Name α
subtract↑ k x with x <nm k
... | inj₁ x′ = inj₁ x′
... | inj₂ x′ = inj₂ (x′ ∸nm k)
infixl 4 subtract↑
syntax subtract↑ k x = x -↑nm k
data WithLim (R : (α β : World) → Set) : (α β : World) → Set where
mkWithLim : ∀ {α₀ β₀} ℓ (Rα₀β₀ : R α₀ β₀) → WithLim R (α₀ ↑ ℓ) (β₀ ↑ ℓ)
withLim : ∀ {R α β} → R α β → WithLim R α β
withLim = mkWithLim 0
private
module Bad where
bad₁ : ∀ {α} → Name α → Bool
bad₁ (zero , _) = true
bad₁ (suc _ , _) = false