module lib.Context where
import Data.Nat as ℕ
open import Data.Empty
open import Data.Product hiding (map)
open import Data.Sum hiding (map)
open import Function
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality as Eq using (_≡_)
module Context where
infixl 20 _∙_
data Con (A : Set) : Set where
ε : Con A
_∙_ : (Γ : Con A) (σ : A) → Con A
length : ∀ {A} (γ : Con A) → ℕ.ℕ
length ε = 0
length (γ ∙ σ) = 1 ℕ.+ length γ
module Context where
map : {A B : Set} (f : A → B) (Γ : Con A) → Con B
map f ε = ε
map f (Γ ∙ σ) = map f Γ ∙ f σ
infixl 5 _++_
_++_ : {A : Set} (xs ys : Con A) → Con A
xs ++ ε = xs
xs ++ ys ∙ σ = (xs ++ ys) ∙ σ
induction : ∀ {A : Set} {P : Con A → Set}
(c : (a : A) {γ : Con A} → P γ → P $ γ ∙ a) (n : P ε)
(γ : Con A) → P γ
induction c n ε = n
induction c n (γ ∙ σ) = c σ $ induction c n γ
foldl : ∀ {A B : Set} (c : A → B → B) (n : B) (Γ : Con A) → B
foldl {B = B} c = induction {P = λ _ → B} (λ a → c a)
foldr : ∀ {A B : Set} (c : A → B → B) (n : B) (Γ : Con A) → B
foldr c n ε = n
foldr c n (Γ ∙ σ) = foldr c (c σ n) Γ
return : {A : Set} (a : A) → Con A
return a = ε ∙ a
subst : {A B : Set} (Γ : Con A) (f : A → Con B) → Con B
subst Γ f = foldl (_++_ ∘ f) ε Γ
syntax subst ma f = ma >>= f
ε++ : {A : Set} (ys : Con A) → ε ++ ys ≡ ys
ε++ ε = Eq.refl
ε++ (ys ∙ σ) = Eq.cong (flip _∙_ σ) $ ε++ ys
map++ : ∀ {A B : Set} (f : A → B) (xs ys : Con A) →
map f (xs ++ ys) ≡ map f xs ++ map f ys
map++ f xs ε = Eq.refl
map++ f xs (ys ∙ σ) = Eq.cong (flip _∙_ (f σ)) $ map++ f xs ys
assoc++ : ∀ {A : Set} (xs ys zs : Con A) →
xs ++ ys ++ zs ≡ xs ++ (ys ++ zs)
assoc++ xs ys ε = Eq.refl
assoc++ xs ys (zs ∙ σ) = Eq.cong (flip _∙_ σ) $ assoc++ xs ys zs
module Pointwise where
data PCon {ℓ} {A : Set} (P : A → Set ℓ) : (γ : Con A) → Set ℓ where
ε : PCon P ε
_∙_ : ∀ {γ σ} (Γ : PCon P γ) (S : P σ) → PCon P $ γ ∙ σ
module Pointwise where
pointwise : ∀ {A P} (prP : (a : A) → P a) (γ : Con A) → PCon P γ
pointwise prP = Context.induction (λ a ih → ih ∙ prP a) ε
map : ∀ {ℓ ℓ′} {A B} {P : A → Set ℓ} {Q : B → Set ℓ′} (f : A → B)
(Pf : {a : A} → P a → Q $ f a)
{γ : Con A} (Γ : PCon P γ) → PCon Q $ Context.map f γ
map f Pf ε = ε
map f Pf (Γ ∙ S) = map f Pf Γ ∙ Pf S
induction : ∀ {ℓ} {A} {P : A → Set ℓ} (Q : (γ : Con A) (Γ : PCon P γ) → Set ℓ)
(c : {a : A} (prP : P a) {γ : Con A} {Γ : PCon P γ}
(prQ : Q γ Γ) → Q (γ ∙ a) $ Γ ∙ prP)
(n : Q ε ε)
{γ : Con A} (Γ : PCon P γ) → Q γ Γ
induction Q c n ε = n
induction Q c n (Γ ∙ S) = c S $ induction Q c n Γ
foldl : ∀ {A} {P : A → Set} {B : Set} (c : (a : A) (b : B) → B) (n : B)
{γ : Con A} (Γ : PCon P γ) → B
foldl {B = B} c n = induction (λ _ _ → B) (λ {a} _ → c a) n
infixl 5 _++_
_++_ : ∀ {ℓ} {A : Set} {P : A → Set ℓ} {xs ys : Con A}
(XS : PCon P xs) (YS : PCon P ys) →
PCon P $ xs Context.++ ys
xs ++ ε = xs
xs ++ ys ∙ σ = (xs ++ ys) ∙ σ
module Inclusion where
open Context
data _⊆_ {A : Set} : Con A → Con A → Set where
■ : ε ⊆ ε
↑_ : ∀ {Γ : Con A} {Δ : Con A} {σ} (inc : Γ ⊆ Δ) → Γ ⊆ (Δ ∙ σ)
_∙_ : ∀ {Γ : Con A} {Δ : Con A} (inc : Γ ⊆ Δ) σ → (Γ ∙ σ) ⊆ (Δ ∙ σ)
module Inclusion where
refl : ∀ {A : Set} (Γ : Con A) → Γ ⊆ Γ
refl ε = ■
refl (Γ ∙ σ) = refl Γ ∙ σ
syntax refl Γ = same Γ
_++_ : ∀ {A : Set} {Γ Δ Ε : Con A} → Γ ⊆ Δ → Δ ⊆ Ε → Γ ⊆ Ε
■ ++ pr₂ = pr₂
pr₁ ∙ σ ++ ↑ pr₂ = ↑_ $ pr₁ ∙ σ ++ pr₂
pr₁ ∙ σ ++ pr₂ ∙ .σ = (pr₁ ++ pr₂) ∙ σ
↑ pr₁ ++ ↑ pr₂ = ↑_ $ ↑ pr₁ ++ pr₂
↑ pr₁ ++ pr₂ ∙ σ = ↑_ $ pr₁ ++ pr₂
module BelongsTo where
open Context
open Inclusion
infix 4 _∈_
data _∈_ {A : Set} (σ : A) : Con A → Set where
zro : {Γ : Con A} → σ ∈ Γ ∙ σ
suc : {Γ : Con A} {τ : A} (pr : σ ∈ Γ) → σ ∈ Γ ∙ τ
have_actUpon_at_ : ∀ {A : Set} (f : A → Con A) → ∀ {σ : A} Γ (pr : σ ∈ Γ) → Con A
have f actUpon Γ ∙ σ at zro = Γ Context.++ f σ
have f actUpon Γ ∙ τ at suc pr = have f actUpon Γ at pr ∙ τ
abstract
suc-inj : ∀ {A : Set} {σ τ : A} {Γ} {pr₁ pr₂ : σ ∈ Γ}
(eq : (σ ∈ Γ ∙ τ ∋ suc pr₁) ≡ suc pr₂) → pr₁ ≡ pr₂
suc-inj Eq.refl = Eq.refl
module BelongsTo where
∈ε-elim : ∀ {A : Set} {σ : A} (pr : σ ∈ ε) → ⊥
∈ε-elim ()
map : ∀ {A B : Set} {σ : A} {Γ} (f : A → B) (pr : σ ∈ Γ) → f σ ∈ Context.map f Γ
map f zro = zro
map f (suc pr) = suc $ map f pr
_≟_ : ∀ {A} {σ : A} {Γ} (pr₁ pr₂ : σ ∈ Γ) → Dec (pr₁ ≡ pr₂)
zro ≟ zro = yes Eq.refl
zro ≟ suc pr₂ = no (λ ())
suc pr₁ ≟ zro = no (λ ())
suc pr₁ ≟ suc pr₂ with pr₁ ≟ pr₂
... | yes eq = yes $ Eq.cong suc eq
... | no ¬eq = no $ ¬eq ∘ suc-inj
wk : ∀ {A : Set} {σ : A} {Γ Δ : Con A} → Γ ⊆ Δ → σ ∈ Γ → σ ∈ Δ
wk ■ ()
wk (↑ incl) pr = suc $ wk incl pr
wk (incl ∙ σ) zro = zro
wk (incl ∙ σ) (suc pr) = suc $ wk incl pr
drop : ∀ {A} Γ {σ : A} (pr : σ ∈ Γ) → Con A
drop (Γ ∙ σ) zro = Γ
drop (Γ ∙ τ) (suc pr) = drop Γ pr ∙ τ
∈++ˡ : ∀ {A Γ} Δ {σ : A} (pr : σ ∈ Γ) → σ ∈ Γ Context.++ Δ
∈++ˡ ε pr = pr
∈++ˡ (Δ ∙ σ) pr = suc $ ∈++ˡ Δ pr
∈++ʳ : ∀ {A Γ Δ} {σ : A} (pr : σ ∈ Δ) → σ ∈ Γ Context.++ Δ
∈++ʳ zro = zro
∈++ʳ (suc pr) = suc $ ∈++ʳ pr
drop++ˡ : ∀ {A Γ} Δ {σ : A} (pr : σ ∈ Γ) →
let open Context.Context in
drop Γ pr ++ Δ ≡ drop (Γ ++ Δ) (∈++ˡ Δ pr)
drop++ˡ ε pr = Eq.refl
drop++ˡ (Δ ∙ σ) pr = Eq.cong (flip _∙_ σ) $ drop++ˡ Δ pr
drop++ʳ : ∀ {A Γ Δ} {σ : A} (pr : σ ∈ Δ) →
let open Context.Context in
Γ ++ drop Δ pr ≡ drop (Γ ++ Δ) (∈++ʳ pr)
drop++ʳ zro = Eq.refl
drop++ʳ (suc {τ = τ} pr) = Eq.cong (flip _∙_ τ) $ drop++ʳ pr
actAt++ˡ : ∀ {A Γ} Δ {σ : A} {f : A → Con A} (pr : σ ∈ Γ) →
have f actUpon Γ Context.++ Δ at ∈++ˡ Δ pr
≡ (have f actUpon Γ at pr) Context.++ Δ
actAt++ˡ ε pr = Eq.refl
actAt++ˡ (Δ ∙ σ) pr = Eq.cong (flip _∙_ σ) $ actAt++ˡ Δ pr
subst : ∀ {A B Γ} {σ : A} (pr₁ : σ ∈ Γ) {f : A → Con B}
{τ : B} (pr₂ : τ ∈ f σ)→ τ ∈ Context.subst Γ f
subst {Γ = Γ ∙ σ} zro {f} pr₂ = ∈++ˡ (Context.subst Γ f) pr₂
subst (suc pr₁) pr₂ = ∈++ʳ (subst pr₁ pr₂)
module Interleaving where
open Context
open BelongsTo
infix 5 _≡_⋈_
infixl 5 _∙ˡ_ _∙ʳ_
data _≡_⋈_ {A : Set} : (Γ Δ Ε : Con A) → Set where
ε : ε ≡ ε ⋈ ε
_∙ʳ_ : ∀ {Γ Δ E} (pr : Γ ≡ Δ ⋈ E) σ → Γ ∙ σ ≡ Δ ⋈ E ∙ σ
_∙ˡ_ : ∀ {Γ Δ E} (pr : Γ ≡ Δ ⋈ E) σ → Γ ∙ σ ≡ Δ ∙ σ ⋈ E
module Interleaving where
module RewriteRules where
open Context.Context
⋈-assoc : {A : Set} (Γ₁ Γ₃ Δ₁ Δ₃ E₁ E₃ : Con A) {Γ₂ Δ₂ E₂ : Con A}
(pr : (Γ₁ ++ Γ₂) ++ Γ₃ ≡ (Δ₁ ++ Δ₂) ++ Δ₃ ⋈ (E₁ ++ E₂) ++ E₃) →
Γ₁ ++ (Γ₂ ++ Γ₃) ≡ Δ₁ ++ (Δ₂ ++ Δ₃) ⋈ E₁ ++ (E₂ ++ E₃)
⋈-assoc Γ₁ Γ₃ Δ₁ Δ₃ E₁ E₃ {Γ₂} {Δ₂} {E₂}
rewrite assoc++ Γ₁ Γ₂ Γ₃ | assoc++ Δ₁ Δ₂ Δ₃ | assoc++ E₁ E₂ E₃ = id
⋈-assoc⁻¹ : {A : Set} (Γ₁ Γ₃ Δ₁ Δ₃ E₁ E₃ : Con A) {Γ₂ Δ₂ E₂ : Con A}
(pr : Γ₁ ++ (Γ₂ ++ Γ₃) ≡ Δ₁ ++ (Δ₂ ++ Δ₃) ⋈ E₁ ++ (E₂ ++ E₃)) →
(Γ₁ ++ Γ₂) ++ Γ₃ ≡ (Δ₁ ++ Δ₂) ++ Δ₃ ⋈ (E₁ ++ E₂) ++ E₃
⋈-assoc⁻¹ Γ₁ Γ₃ Δ₁ Δ₃ E₁ E₃ {Γ₂} {Δ₂} {E₂}
rewrite assoc++ Γ₁ Γ₂ Γ₃ | assoc++ Δ₁ Δ₂ Δ₃ | assoc++ E₁ E₂ E₃ = id
map : ∀ {A B} {Γ Δ E : Con A} (f : A → B) (pr : Γ ≡ Δ ⋈ E) →
let open Context.Context in
map f Γ ≡ map f Δ ⋈ map f E
map f ε = ε
map f (pr ∙ʳ σ) = map f pr ∙ʳ f σ
map f (pr ∙ˡ σ) = map f pr ∙ˡ f σ
sym : ∀ {A} {Γ Δ E : Con A} (pr : Γ ≡ Δ ⋈ E) → Γ ≡ E ⋈ Δ
sym ε = ε
sym (pr ∙ʳ σ) = sym pr ∙ˡ σ
sym (pr ∙ˡ σ) = sym pr ∙ʳ σ
reflˡ : ∀ {A} {Γ : Con A} → Γ ≡ Γ ⋈ ε
reflˡ {A} {Γ} = helper Γ
where
helper : (Γ : Con A) → Γ ≡ Γ ⋈ ε
helper ε = ε
helper (Γ ∙ σ) = helper Γ ∙ˡ σ
reflʳ : ∀ {A} {Γ : Con A} → Γ ≡ ε ⋈ Γ
reflʳ {A} {Γ} = sym reflˡ
infixl 5 _++_ _ˡ++ʳ_
_++_ : {A : Set} {Γ₁ Γ₂ Δ₁ Δ₂ E₁ E₂ : Con A}
(pr₁ : Γ₁ ≡ Δ₁ ⋈ E₁) (pr₂ : Γ₂ ≡ Δ₂ ⋈ E₂) →
let open Context.Context in Γ₁ ++ Γ₂ ≡ Δ₁ ++ Δ₂ ⋈ E₁ ++ E₂
pr₁ ++ ε = pr₁
pr₁ ++ (pr₂ ∙ʳ σ) = pr₁ ++ pr₂ ∙ʳ σ
pr₁ ++ (pr₂ ∙ˡ σ) = pr₁ ++ pr₂ ∙ˡ σ
_ˡ++_ : {A : Set} (Γ : Con A) {Δ Δ₁ Δ₂ : Con A} (pr : Δ ≡ Δ₁ ⋈ Δ₂) →
Γ Context.++ Δ ≡ Γ Context.++ Δ₁ ⋈ Δ₂
Γ ˡ++ ε = reflˡ
Γ ˡ++ (pr ∙ʳ σ) = Γ ˡ++ pr ∙ʳ σ
Γ ˡ++ (pr ∙ˡ σ) = Γ ˡ++ pr ∙ˡ σ
_ʳ++_ : {A : Set} (Γ : Con A) {Δ Δ₁ Δ₂ : Con A} (pr : Δ ≡ Δ₁ ⋈ Δ₂) →
Γ Context.++ Δ ≡ Δ₁ ⋈ Γ Context.++ Δ₂
Γ ʳ++ pr = sym $ Γ ˡ++ sym pr
_++ˡ_ : {A : Set} {Γ Γ₁ Γ₂ : Con A} (pr : Γ ≡ Γ₁ ⋈ Γ₂) (Δ : Con A) →
Γ Context.++ Δ ≡ Γ₁ Context.++ Δ ⋈ Γ₂
pr ++ˡ Δ = pr ++ reflˡ {Γ = Δ}
_++ʳ_ : {A : Set} {Γ Γ₁ Γ₂ : Con A} (pr : Γ ≡ Γ₁ ⋈ Γ₂) (Δ : Con A) →
Γ Context.++ Δ ≡ Γ₁ ⋈ Γ₂ Context.++ Δ
pr ++ʳ Δ = pr ++ reflʳ {Γ = Δ}
_ˡ++ʳ_ : {A : Set} (Γ Δ : Con A) → Γ Context.++ Δ ≡ Γ ⋈ Δ
Γ ˡ++ʳ ε = reflˡ
Γ ˡ++ʳ Δ ∙ σ = Γ ˡ++ʳ Δ ∙ʳ σ
_ʳ++ˡ_ : {A : Set} (Γ Δ : Con A) → Γ Context.++ Δ ≡ Δ ⋈ Γ
Γ ʳ++ˡ Δ = sym $ Γ ˡ++ʳ Δ
dropʳ : ∀ {A} Γ {σ : A} (pr : σ ∈ Γ) → Γ ≡ BelongsTo.drop Γ pr ⋈ ε ∙ σ
dropʳ (Γ ∙ σ) zro = reflˡ ∙ʳ σ
dropʳ (Γ ∙ τ) (suc pr) = dropʳ Γ pr ∙ˡ τ
dropˡ : ∀ {A} Γ {σ : A} (pr : σ ∈ Γ) → Γ ≡ ε ∙ σ ⋈ BelongsTo.drop Γ pr
dropˡ Γ pr = sym $ dropʳ Γ pr