Skip to content

Instantly share code, notes, and snippets.

@mietek

mietek/Common.agda Secret

Last active February 1, 2017 20:13
Show Gist options
  • Star 1 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save mietek/075f0a3c10087c04e3b52ea68deb4903 to your computer and use it in GitHub Desktop.
Save mietek/075f0a3c10087c04e3b52ea68deb4903 to your computer and use it in GitHub Desktop.
Download ZIP
S4 + NbE + HSubst
Raw
Common.agda
module Common where
open import Agda.Primitive public using (_⊔_)
open import Agda.Builtin.Equality public using (_≡_ ; refl)
open import Agda.Builtin.Unit public using (⊤) renaming (tt to ∙)
-- Falsum.
data ⊥ : Set where
{-# HASKELL data AgdaEmpty #-}
{-# COMPILED_DATA ⊥ MAlonzo.Code.Data.Empty.AgdaEmpty #-}
elim⊥ : ∀ {ℓ} {X : Set ℓ} → ⊥ → X
elim⊥ ()
-- Constructive existence and conjunction.
infixl 5 _,_
record Σ {ℓ ℓ′} (X : Set ℓ) (Y : X → Set ℓ′) : Set (ℓ ⊔ ℓ′) where
constructor _,_
field
π₁ : X
π₂ : Y π₁
open Σ public
∃ : ∀ {ℓ ℓ′} {X : Set ℓ} → (X → Set ℓ′) → Set (ℓ ⊔ ℓ′)
∃ = Σ _
infixr 2 _∧_
_∧_ : ∀ {ℓ ℓ′} → Set ℓ → Set ℓ′ → Set (ℓ ⊔ ℓ′)
X ∧ Y = Σ X (λ x → Y)
-- Disjunction.
infixr 1 _∨_
data _∨_ {ℓ ℓ′} (X : Set ℓ) (Y : Set ℓ′) : Set (ℓ ⊔ ℓ′) where
ι₁ : X → X ∨ Y
ι₂ : Y → X ∨ Y
{-# HASKELL type AgdaEither a b c d = Either c d #-}
{-# COMPILED_DATA _∨_ MAlonzo.Code.Data.Sum.AgdaEither Left Right #-}
-- Negation.
infix 3 ¬_
¬_ : ∀ {ℓ} → Set ℓ → Set ℓ
¬ X = X → ⊥
-- Equivalence.
infix 1 _↔_
_↔_ : ∀ {ℓ ℓ′} → (X : Set ℓ) (Y : Set ℓ′) → Set (ℓ ⊔ ℓ′)
X ↔ Y = (X → Y) ∧ (Y → X)
-- Properties of built-in equality.
sym : ∀ {ℓ} {X : Set ℓ} →
∀ {x x′ : X} → x ≡ x′ → x′ ≡ x
sym refl = refl
trans : ∀ {ℓ} {X : Set ℓ} →
∀ {x x′ x″ : X} → x ≡ x′ → x′ ≡ x″ → x ≡ x″
trans refl refl = refl
subst : ∀ {ℓ ℓ′} {X : Set ℓ} → (P : X → Set ℓ′) →
∀ {x x′ : X} → x ≡ x′ → P x → P x′
subst P refl p = p
cong : ∀ {ℓ ℓ′} {X : Set ℓ} {Y : Set ℓ′} → (f : X → Y) →
∀ {x x′} → x ≡ x′ → f x ≡ f x′
cong f refl = refl
cong₂ : ∀ {ℓ ℓ′ ℓ″} {X : Set ℓ} {Y : Set ℓ′} {Z : Set ℓ″} → (f : X → Y → Z) →
∀ {x x′ y y′} → x ≡ x′ → y ≡ y′ → f x y ≡ f x′ y′
cong₂ f refl refl = refl
cong₃ : ∀ {ℓ ℓ′ ℓ″ ℓ‴} {X : Set ℓ} {Y : Set ℓ′} {Z : Set ℓ″} {A : Set ℓ‴} → (f : X → Y → Z → A) →
∀ {x x′ y y′ z z′} → x ≡ x′ → y ≡ y′ → z ≡ z′ → f x y z ≡ f x′ y′ z′
cong₃ f refl refl refl = refl
-- Equational reasoning.
module ≡-Reasoning {ℓ} {X : Set ℓ} where
infix 1 begin_
begin_ : ∀ {x x′ : X} → x ≡ x′ → x ≡ x′
begin_ p = p
infixr 2 _≡⟨⟩_
_≡⟨⟩_ : ∀ (x {x′} : X) → x ≡ x′ → x ≡ x′
_ ≡⟨⟩ p = p
infixr 2 _≡⟨_⟩_
_≡⟨_⟩_ : ∀ (x {x′ x″} : X) → x ≡ x′ → x′ ≡ x″ → x ≡ x″
_ ≡⟨ p ⟩ q = trans p q
infix 3 _∎
_∎ : ∀ (x : X) → x ≡ x
_∎ _ = refl
Raw
Everything.agda
module Everything where
import Common
import Sequence
-- Constructive modal logic S4.
import S4
import S4Convertibility
-- Normalisation by evaluation.
import S4NormalForm
-- TODO: Think about semantic entailment.
import S4NbE
import S4NbEExplicit
-- TODO: Show correctness of NbE with respect to convertibility.
import S4NbECorrectness
-- Normalisation by hereditary substitution.
import S4SpinalNormalForm
-- TODO: Fix termination of hereditary substitution.
import S4NbHS
-- TODO: Show correctness of NbHS with respect to convertibility.
-- import S4NbHSCorrectness
-- TODO: Remove this
import S4SpinalNormalFormWrong
import S4NbHSWrong
import Examples
Raw
Examples.agda
module Examples where
open import S4
import S4NbE
import S4NbEExplicit
import S4NbHS
dist : ∀ {A B Γ Δ} → Γ ⁏ Δ ⊢ □ (A ⇒ B) → Γ ⁏ Δ ⊢ □ A → Γ ⁏ Δ ⊢ □ B
dist t u = unbox t (unbox (mono⊢ refl⊆ weak⊆ u) (box (app ᵐv₁ ᵐv₀)))
up : ∀ {A Γ Δ} → Γ ⁏ Δ ⊢ □ A → Γ ⁏ Δ ⊢ □ (□ A)
up d = unbox d (box (box ᵐv₀))
down : ∀ {A Γ Δ} → Γ ⁏ Δ ⊢ □ A → Γ ⁏ Δ ⊢ A
down d = unbox d ᵐv₀
id : ∀ {A Γ Δ} → Γ ⁏ Δ ⊢ A → Γ ⁏ Δ ⊢ A
id = app (lam v₀)
u₁ : ∅ ⁏ ∅ ⊢ □ ⫪
u₁ = box (id unit)
u₂ : ∅ ⁏ ∅ ⊢ □ □ ⫪
u₂ = box (id (box (id unit)))
u₃ : ∅ ⁏ ∅ ⊢ □ ⫪
u₃ = down (up u₁)
u₄ : ∅ ⁏ ∅ ⊢ □ □ ⫪
u₄ = up (down u₂)
u₅ : ∅ ⁏ ∅ ⊢ □ ⫪
u₅ = box unit
u₆ : ∅ ⁏ ∅ ⊢ □ □ ⫪
u₆ = box (box unit)
u₇ : ∅ ⁏ ∅ ⊢ □ ⫪
u₇ = down (up u₅)
u₈ : ∅ ⁏ ∅ ⊢ □ □ ⫪
u₈ = up (down u₆)
up-box : ∅ ⁏ ∅ ⊢ □ □ ⫪
up-box = unbox (box unit) (box (box ᵐv₀))
module NbETest where
open S4NbE
test₁ : nbe u₁ ≡ boxⁿᶠ (id unit)
test₁ = refl
test₂ : nbe u₂ ≡ boxⁿᶠ (id (box (id unit)))
test₂ = refl
test₃ : nbe u₃ ≡ boxⁿᶠ (id unit)
test₃ = refl
test₄ : nbe u₄ ≡ boxⁿᶠ (box (id unit))
test₄ = refl
test₅ : nbe u₅ ≡ boxⁿᶠ unit
test₅ = refl
test₆ : nbe u₆ ≡ boxⁿᶠ (box unit)
test₆ = refl
test₇ : nbe u₇ ≡ boxⁿᶠ unit
test₇ = refl
test₈ : nbe u₈ ≡ boxⁿᶠ (box unit)
test₈ = refl
up-box-test : nbe up-box ≡ boxⁿᶠ (box unit)
up-box-test = refl
module NbEExplicitTest where
open S4NbEExplicit
test₁ : nbe u₁ ≡ boxⁿᶠ (id unit)
test₁ = refl
test₂ : nbe u₂ ≡ boxⁿᶠ (id (box (id unit)))
test₂ = refl
test₃ : nbe u₃ ≡ boxⁿᶠ (id unit)
test₃ = refl
test₄ : nbe u₄ ≡ boxⁿᶠ (box (id unit))
test₄ = refl
test₅ : nbe u₅ ≡ boxⁿᶠ unit
test₅ = refl
test₆ : nbe u₆ ≡ boxⁿᶠ (box unit)
test₆ = refl
test₇ : nbe u₇ ≡ boxⁿᶠ unit
test₇ = refl
test₈ : nbe u₈ ≡ boxⁿᶠ (box unit)
test₈ = refl
up-box-test : nbe up-box ≡ boxⁿᶠ (box unit)
up-box-test = refl
module NbHSTest where
open S4NbHS
test₁ : nbhs′ u₁ ≡ boxⁿᶠ (id unit)
test₁ = refl
test₂ : nbhs′ u₂ ≡ boxⁿᶠ (id (box (id unit)))
test₂ = refl
test₃ : nbhs′ u₃ ≡ boxⁿᶠ (id unit)
test₃ = refl
test₄ : nbhs′ u₄ ≡ boxⁿᶠ (box (id unit))
test₄ = refl
test₅ : nbhs′ u₅ ≡ boxⁿᶠ unit
test₅ = refl
test₆ : nbhs′ u₆ ≡ boxⁿᶠ (box unit)
test₆ = refl
test₇ : nbhs′ u₇ ≡ boxⁿᶠ unit
test₇ = refl
test₈ : nbhs′ u₈ ≡ boxⁿᶠ (box unit)
test₈ = refl
up-box-test : nbhs′ up-box ≡ boxⁿᶠ (box unit)
up-box-test = refl
Raw
S4.agda
module S4 where
open import Common public
-- Propositions, or types of the object-level language.
infixr 10 □_
infixl 9 _⩕_
infixl 8 _⩖_
infixr 7 _⇒_
data Prop : Set where
_⇒_ : Prop → Prop → Prop
□_ : Prop → Prop
_⩕_ : Prop → Prop → Prop
⫪ : Prop
⫫ : Prop
_⩖_ : Prop → Prop → Prop
open import Sequence (Prop) public
-- Proofs, or terms of the object-level language.
infix 3 _⁏_⊢_
data _⁏_⊢_ (Γ Δ : Seq) : Prop → Set where
var : ∀ {A} → A ∈ Γ → Γ ⁏ Δ ⊢ A
ᵐvar : ∀ {A} → A ∈ Δ → Γ ⁏ Δ ⊢ A
lam : ∀ {A B} → Γ , A ⁏ Δ ⊢ B → Γ ⁏ Δ ⊢ A ⇒ B
app : ∀ {A B} → Γ ⁏ Δ ⊢ A ⇒ B → Γ ⁏ Δ ⊢ A → Γ ⁏ Δ ⊢ B
box : ∀ {A} → ∅ ⁏ Δ ⊢ A → Γ ⁏ Δ ⊢ □ A
unbox : ∀ {A C} → Γ ⁏ Δ ⊢ □ A → Γ ⁏ Δ , A ⊢ C → Γ ⁏ Δ ⊢ C
pair : ∀ {A B} → Γ ⁏ Δ ⊢ A → Γ ⁏ Δ ⊢ B → Γ ⁏ Δ ⊢ A ⩕ B
fst : ∀ {A B} → Γ ⁏ Δ ⊢ A ⩕ B → Γ ⁏ Δ ⊢ A
snd : ∀ {A B} → Γ ⁏ Δ ⊢ A ⩕ B → Γ ⁏ Δ ⊢ B
unit : Γ ⁏ Δ ⊢ ⫪
boom : ∀ {C} → Γ ⁏ Δ ⊢ ⫫ → Γ ⁏ Δ ⊢ C
left : ∀ {A B} → Γ ⁏ Δ ⊢ A → Γ ⁏ Δ ⊢ A ⩖ B
right : ∀ {A B} → Γ ⁏ Δ ⊢ B → Γ ⁏ Δ ⊢ A ⩖ B
case : ∀ {A B C} → Γ ⁏ Δ ⊢ A ⩖ B → Γ , A ⁏ Δ ⊢ C → Γ , B ⁏ Δ ⊢ C → Γ ⁏ Δ ⊢ C
infix 3 _⁏_⊢⋆_
_⁏_⊢⋆_ : Seq → Seq → Seq → Set
Γ ⁏ Δ ⊢⋆ ∅ = ⊤
Γ ⁏ Δ ⊢⋆ Ξ , A = Γ ⁏ Δ ⊢⋆ Ξ ∧ Γ ⁏ Δ ⊢ A
-- Shorthand for variables.
v₀ : ∀ {Γ Δ A} → Γ , A ⁏ Δ ⊢ A
v₀ = var i₀
v₁ : ∀ {Γ Δ A B} → Γ , A , B ⁏ Δ ⊢ A
v₁ = var i₁
v₂ : ∀ {Γ Δ A B C} → Γ , A , B , C ⁏ Δ ⊢ A
v₂ = var i₂
ᵐv₀ : ∀ {Γ Δ A} → Γ ⁏ Δ , A ⊢ A
ᵐv₀ = ᵐvar i₀
ᵐv₁ : ∀ {Γ Δ A B} → Γ ⁏ Δ , A , B ⊢ A
ᵐv₁ = ᵐvar i₁
ᵐv₂ : ∀ {Γ Δ A B C} → Γ ⁏ Δ , A , B , C ⊢ A
ᵐv₂ = ᵐvar i₂
-- Monotonicity with respect to context inclusion.
mono⊢ : ∀ {Γ Γ′ Δ Δ′ A} → Γ ⊆ Γ′ → Δ ⊆ Δ′ → Γ ⁏ Δ ⊢ A → Γ′ ⁏ Δ′ ⊢ A
mono⊢ η θ (var i) = var (mono∈ η i)
mono⊢ η θ (ᵐvar i) = ᵐvar (mono∈ θ i)
mono⊢ η θ (lam t) = lam (mono⊢ (keep η) θ t)
mono⊢ η θ (app t u) = app (mono⊢ η θ t) (mono⊢ η θ u)
mono⊢ η θ (box t) = box (mono⊢ done θ t)
mono⊢ η θ (unbox t u) = unbox (mono⊢ η θ t) (mono⊢ η (keep θ) u)
mono⊢ η θ (pair t u) = pair (mono⊢ η θ t) (mono⊢ η θ u)
mono⊢ η θ (fst t) = fst (mono⊢ η θ t)
mono⊢ η θ (snd t) = snd (mono⊢ η θ t)
mono⊢ η θ unit = unit
mono⊢ η θ (boom t) = boom (mono⊢ η θ t)
mono⊢ η θ (left t) = left (mono⊢ η θ t)
mono⊢ η θ (right t) = right (mono⊢ η θ t)
mono⊢ η θ (case t u v) = case (mono⊢ η θ t) (mono⊢ (keep η) θ u) (mono⊢ (keep η) θ v)
mono⊢⋆ : ∀ {Ξ Γ Γ′ Δ Δ′} → Γ ⊆ Γ′ → Δ ⊆ Δ′ → Γ ⁏ Δ ⊢⋆ Ξ → Γ′ ⁏ Δ′ ⊢⋆ Ξ
mono⊢⋆ {∅} η θ ∙ = ∙
mono⊢⋆ {Ξ , A} η θ (τ , t) = mono⊢⋆ η θ τ , mono⊢ η θ t
-- Substitution.
[_≔_]∈_ : ∀ {Γ Δ A C} → (i : A ∈ Γ) → Γ ∖ i ⁏ Δ ⊢ A → C ∈ Γ → Γ ∖ i ⁏ Δ ⊢ C
[ i ≔ s ]∈ j with i ≟∈ j
[ i ≔ s ]∈ .i | same = s
[ i ≔ s ]∈ ._ | diff j = var j
[_≔_]_ : ∀ {Γ Δ A C} → (i : A ∈ Γ) → Γ ∖ i ⁏ Δ ⊢ A → Γ ⁏ Δ ⊢ C → Γ ∖ i ⁏ Δ ⊢ C
[ i ≔ s ] var j = [ i ≔ s ]∈ j
[ i ≔ s ] ᵐvar j = ᵐvar j
[ i ≔ s ] lam t = lam ([ pop i ≔ mono⊢ weak⊆ refl⊆ s ] t)
[ i ≔ s ] app t u = app ([ i ≔ s ] t) ([ i ≔ s ] u)
[ i ≔ s ] box t = box t
[ i ≔ s ] unbox t u = unbox ([ i ≔ s ] t) ([ i ≔ mono⊢ refl⊆ weak⊆ s ] u)
[ i ≔ s ] pair t u = pair ([ i ≔ s ] t) ([ i ≔ s ] u)
[ i ≔ s ] fst t = fst ([ i ≔ s ] t)
[ i ≔ s ] snd t = snd ([ i ≔ s ] t)
[ i ≔ s ] unit = unit
[ i ≔ s ] boom t = boom ([ i ≔ s ] t)
[ i ≔ s ] left t = left ([ i ≔ s ] t)
[ i ≔ s ] right t = right ([ i ≔ s ] t)
[ i ≔ s ] case t u v = case ([ i ≔ s ] t) ([ pop i ≔ mono⊢ weak⊆ refl⊆ s ] u)
([ pop i ≔ mono⊢ weak⊆ refl⊆ s ] v)
ᵐ[_≔_]∈_ : ∀ {Γ Δ A C} → (i : A ∈ Δ) → ∅ ⁏ Δ ∖ i ⊢ A → C ∈ Δ → Γ ⁏ Δ ∖ i ⊢ C
ᵐ[ i ≔ s ]∈ j with i ≟∈ j
ᵐ[ i ≔ s ]∈ .i | same = mono⊢ zero⊆ refl⊆ s
ᵐ[ i ≔ s ]∈ ._ | diff j = ᵐvar j
ᵐ[_≔_]_ : ∀ {Γ Δ A C} → (i : A ∈ Δ) → ∅ ⁏ Δ ∖ i ⊢ A → Γ ⁏ Δ ⊢ C → Γ ⁏ Δ ∖ i ⊢ C
ᵐ[ i ≔ s ] var j = var j
ᵐ[ i ≔ s ] ᵐvar j = ᵐ[ i ≔ s ]∈ j
ᵐ[ i ≔ s ] lam t = lam (ᵐ[ i ≔ s ] t)
ᵐ[ i ≔ s ] app t u = app (ᵐ[ i ≔ s ] t) (ᵐ[ i ≔ s ] u)
ᵐ[ i ≔ s ] box t = box (ᵐ[ i ≔ s ] t)
ᵐ[ i ≔ s ] unbox t u = unbox (ᵐ[ i ≔ s ] t) (ᵐ[ pop i ≔ mono⊢ refl⊆ weak⊆ s ] u)
ᵐ[ i ≔ s ] pair t u = pair (ᵐ[ i ≔ s ] t) (ᵐ[ i ≔ s ] u)
ᵐ[ i ≔ s ] fst t = fst (ᵐ[ i ≔ s ] t)
ᵐ[ i ≔ s ] snd t = snd (ᵐ[ i ≔ s ] t)
ᵐ[ i ≔ s ] unit = unit
ᵐ[ i ≔ s ] boom t = boom (ᵐ[ i ≔ s ] t)
ᵐ[ i ≔ s ] left t = left (ᵐ[ i ≔ s ] t)
ᵐ[ i ≔ s ] right t = right (ᵐ[ i ≔ s ] t)
ᵐ[ i ≔ s ] case t u v = case (ᵐ[ i ≔ s ] t) (ᵐ[ i ≔ s ] u) (ᵐ[ i ≔ s ] v)
-- Simultaneous substitution.
graft∈⋆ : ∀ {Ξ Γ Δ C} → Ξ ⁏ Δ ⊢⋆ Γ → C ∈ Γ → Ξ ⁏ Δ ⊢ C
graft∈⋆ (σ , s) top = s
graft∈⋆ (σ , s) (pop i) = graft∈⋆ σ i
graft⊢⋆ : ∀ {Ξ Γ Δ C} → Ξ ⁏ Δ ⊢⋆ Γ → Γ ⁏ Δ ⊢ C → Ξ ⁏ Δ ⊢ C
graft⊢⋆ σ (var i) = graft∈⋆ σ i
graft⊢⋆ σ (ᵐvar i) = ᵐvar i
graft⊢⋆ σ (lam t) = lam (graft⊢⋆ (mono⊢⋆ weak⊆ refl⊆ σ , v₀) t)
graft⊢⋆ σ (app t u) = app (graft⊢⋆ σ t) (graft⊢⋆ σ u)
graft⊢⋆ σ (box t) = box t
graft⊢⋆ σ (unbox t u) = unbox (graft⊢⋆ σ t) (graft⊢⋆ (mono⊢⋆ refl⊆ weak⊆ σ) u )
graft⊢⋆ σ (pair t u) = pair (graft⊢⋆ σ t) (graft⊢⋆ σ u)
graft⊢⋆ σ (fst t) = fst (graft⊢⋆ σ t)
graft⊢⋆ σ (snd t) = snd (graft⊢⋆ σ t)
graft⊢⋆ σ unit = unit
graft⊢⋆ σ (boom t) = boom (graft⊢⋆ σ t)
graft⊢⋆ σ (left t) = left (graft⊢⋆ σ t)
graft⊢⋆ σ (right t) = right (graft⊢⋆ σ t)
graft⊢⋆ σ (case t u v) = case (graft⊢⋆ σ t) (graft⊢⋆ (mono⊢⋆ weak⊆ refl⊆ σ , v₀) u)
(graft⊢⋆ (mono⊢⋆ weak⊆ refl⊆ σ , v₀) v)
ᵐgraft∈⋆ : ∀ {Ξ Γ Δ C} → ∅ ⁏ Ξ ⊢⋆ Δ → C ∈ Δ → Γ ⁏ Ξ ⊢ C
ᵐgraft∈⋆ (σ , s) top = mono⊢ zero⊆ refl⊆ s
ᵐgraft∈⋆ (σ , s) (pop i) = ᵐgraft∈⋆ σ i
ᵐgraft⊢⋆ : ∀ {Ξ Γ Δ C} → ∅ ⁏ Ξ ⊢⋆ Δ → Γ ⁏ Δ ⊢ C → Γ ⁏ Ξ ⊢ C
ᵐgraft⊢⋆ σ (var i) = var i
ᵐgraft⊢⋆ σ (ᵐvar i) = ᵐgraft∈⋆ σ i
ᵐgraft⊢⋆ σ (lam t) = lam (ᵐgraft⊢⋆ σ t)
ᵐgraft⊢⋆ σ (app t u) = app (ᵐgraft⊢⋆ σ t) (ᵐgraft⊢⋆ σ u)
ᵐgraft⊢⋆ σ (box t) = box (ᵐgraft⊢⋆ σ t)
ᵐgraft⊢⋆ σ (unbox t u) = unbox (ᵐgraft⊢⋆ σ t) (ᵐgraft⊢⋆ (mono⊢⋆ refl⊆ weak⊆ σ , ᵐv₀) u)
ᵐgraft⊢⋆ σ (pair t u) = pair (ᵐgraft⊢⋆ σ t) (ᵐgraft⊢⋆ σ u)
ᵐgraft⊢⋆ σ (fst t) = fst (ᵐgraft⊢⋆ σ t)
ᵐgraft⊢⋆ σ (snd t) = snd (ᵐgraft⊢⋆ σ t)
ᵐgraft⊢⋆ σ unit = unit
ᵐgraft⊢⋆ σ (boom t) = boom (ᵐgraft⊢⋆ σ t)
ᵐgraft⊢⋆ σ (left t) = left (ᵐgraft⊢⋆ σ t)
ᵐgraft⊢⋆ σ (right t) = right (ᵐgraft⊢⋆ σ t)
ᵐgraft⊢⋆ σ (case t u v) = case (ᵐgraft⊢⋆ σ t) (ᵐgraft⊢⋆ σ u) (ᵐgraft⊢⋆ σ v)
-- Reflexivity.
refl⊢⋆ : ∀ {Γ Δ} → Γ ⁏ Δ ⊢⋆ Γ
refl⊢⋆ {∅} = ∙
refl⊢⋆ {Γ , A} = mono⊢⋆ weak⊆ refl⊆ refl⊢⋆ , v₀
ᵐrefl⊢⋆ : ∀ {Δ Γ} → Γ ⁏ Δ ⊢⋆ Δ
ᵐrefl⊢⋆ {∅} = ∙
ᵐrefl⊢⋆ {Δ , A} = mono⊢⋆ refl⊆ weak⊆ ᵐrefl⊢⋆ , ᵐv₀
Raw
S4Convertibility.agda
module S4Convertibility where
open import S4 public
-- Convertibility, or β-η-equivalence.
infix 5 _≣_
data _≣_ {Γ Δ : Seq} : ∀ {A} → Γ ⁏ Δ ⊢ A → Γ ⁏ Δ ⊢ A → Set where
refl≣ : ∀ {A} {t : Γ ⁏ Δ ⊢ A} →
t ≣ t
trans≣ : ∀ {A} {t t′ t″ : Γ ⁏ Δ ⊢ A} →
t ≣ t′ → t′ ≣ t″ →
t ≣ t″
sym≣ : ∀ {A} {t t′ : Γ ⁏ Δ ⊢ A} →
t ≣ t′ →
t′ ≣ t
-- Congruences.
--
-- NOTE: There is no cong≡box, because we do not normalise under box.
cong≣lam : ∀ {A B} {t t′ : Γ , A ⁏ Δ ⊢ B} →
t ≣ t′ →
lam t ≣ lam t′
cong≣app : ∀ {A B} {t t′ : Γ ⁏ Δ ⊢ A ⇒ B}
{u u′ : Γ ⁏ Δ ⊢ A} →
t ≣ t′ → u ≣ u′ →
app t u ≣ app t′ u′
cong≣unbox : ∀ {A C} {t t′ : Γ ⁏ Δ ⊢ □ A}
{u u′ : Γ ⁏ Δ , A ⊢ C} →
t ≣ t′ → u ≣ u′ →
unbox t u ≣ unbox t′ u′
cong≣pair : ∀ {A B} {t t′ : Γ ⁏ Δ ⊢ A}
{u u′ : Γ ⁏ Δ ⊢ B} →
t ≣ t′ → u ≣ u′ →
pair t u ≣ pair t′ u′
cong≣fst : ∀ {A B} {t t′ : Γ ⁏ Δ ⊢ A ⩕ B} →
t ≣ t′ →
fst t ≣ fst t′
cong≣snd : ∀ {A B} {t t′ : Γ ⁏ Δ ⊢ A ⩕ B} →
t ≣ t′ →
snd t ≣ snd t′
cong≣boom : ∀ {C} {t t′ : Γ ⁏ Δ ⊢ ⫫} →
t ≣ t′ →
boom {C = C} t ≣ boom t′
cong≣left : ∀ {A B} {t t′ : Γ ⁏ Δ ⊢ A} →
t ≣ t′ →
left {B = B} t ≣ left t′
cong≣right : ∀ {A B} {t t′ : Γ ⁏ Δ ⊢ B} →
t ≣ t′ →
right {A = A} t ≣ right t′
cong≣case : ∀ {A B C} {t t′ : Γ ⁏ Δ ⊢ A ⩖ B}
{u u′ : Γ , A ⁏ Δ ⊢ C}
{v v′ : Γ , B ⁏ Δ ⊢ C} →
t ≣ t′ → u ≣ u′ → v ≣ v′ →
case t u v ≣ case t′ u′ v′
-- Reductions, or β-conversions.
red⇒ : ∀ {A B} {t : Γ , A ⁏ Δ ⊢ B}
{u : Γ ⁏ Δ ⊢ A} →
app (lam t) u ≣ [ top ≔ u ] t
red□ : ∀ {A C} {t : ∅ ⁏ Δ ⊢ A}
{u : Γ ⁏ Δ , A ⊢ C} →
unbox (box t) u ≣ ᵐ[ top ≔ t ] u
red⩕₁ : ∀ {A B} {t : Γ ⁏ Δ ⊢ A}
{u : Γ ⁏ Δ ⊢ B} →
fst (pair t u) ≣ t
red⩕₂ : ∀ {A B} {t : Γ ⁏ Δ ⊢ A}
{u : Γ ⁏ Δ ⊢ B} →
snd (pair t u) ≣ u
red⩖₁ : ∀ {A B C} {t : Γ ⁏ Δ ⊢ A}
{u : Γ , A ⁏ Δ ⊢ C}
{v : Γ , B ⁏ Δ ⊢ C} →
case (left t) u v ≣ [ top ≔ t ] u
red⩖₂ : ∀ {A B C} {t : Γ ⁏ Δ ⊢ B}
{u : Γ , A ⁏ Δ ⊢ C}
{v : Γ , B ⁏ Δ ⊢ C} →
case (right t) u v ≣ [ top ≔ t ] v
-- Expansions, or η-conversions.
exp⇒ : ∀ {A B} {t : Γ ⁏ Δ ⊢ A ⇒ B} →
t ≣ lam (app (mono⊢ weak⊆ refl⊆ t) v₀)
exp□ : ∀ {A} {t : Γ ⁏ Δ ⊢ □ A} →
t ≣ unbox t (box ᵐv₀)
exp⩕ : ∀ {A B} {t : Γ ⁏ Δ ⊢ A ⩕ B} →
t ≣ pair (fst t) (snd t)
exp⫪ : ∀ {t : Γ ⁏ Δ ⊢ ⫪} →
t ≣ unit
exp⩖ : ∀ {A B} {t : Γ ⁏ Δ ⊢ A ⩖ B} →
t ≣ case t (left v₀) (right v₀)
-- Commuting conversions for □.
--
-- NOTE: Generated by instantiating the following schema with elimination rules.
--
-- com□ : ∀ {A B X} {t : Γ ⁏ Δ ⊢ □ X}
-- {u : Γ ⁏ Δ , X ⊢ A}
-- {r : ∀ {Γ′ Δ′} → Γ′ ⁏ Δ′ ⊢ A → Γ′ ⁏ Δ′ ⊢ B} →
-- r (unbox t u) ≣ unbox t (r u)
com□app : ∀ {A B X} {t : Γ ⁏ Δ ⊢ □ X}
{u : Γ ⁏ Δ , X ⊢ A ⇒ B}
{v : Γ ⁏ Δ ⊢ A} →
app (unbox t u) v ≣ unbox t (app u (mono⊢ refl⊆ weak⊆ v))
com□unbox : ∀ {A C X} {t : Γ ⁏ Δ ⊢ □ X}
{u : Γ ⁏ Δ , X ⊢ □ A}
{v : Γ ⁏ Δ , A ⊢ C} →
unbox (unbox t u) v ≣ unbox t (unbox u (mono⊢ refl⊆ (keep weak⊆) v))
com□fst : ∀ {A B X} {t : Γ ⁏ Δ ⊢ □ X}
{u : Γ ⁏ Δ , X ⊢ A ⩕ B} →
fst (unbox t u) ≣ unbox t (fst u)
com□snd : ∀ {A B X} {t : Γ ⁏ Δ ⊢ □ X}
{u : Γ ⁏ Δ , X ⊢ A ⩕ B} →
snd (unbox t u) ≣ unbox t (snd u)
com□boom : ∀ {C X} {t : Γ ⁏ Δ ⊢ □ X}
{u : Γ ⁏ Δ , X ⊢ ⫫} →
boom {C = C} (unbox t u) ≣ unbox t (boom u)
com□case : ∀ {A B C X} {t : Γ ⁏ Δ ⊢ □ X}
{u : Γ ⁏ Δ , X ⊢ A ⩖ B}
{v : Γ , A ⁏ Δ ⊢ C}
{w : Γ , B ⁏ Δ ⊢ C} →
case (unbox t u) v w ≣ unbox t (case u (mono⊢ refl⊆ weak⊆ v)
(mono⊢ refl⊆ weak⊆ w))
-- Commuting conversions for ⫫.
--
-- NOTE: Generated by instantiating the following schema with elimination rules.
--
-- com⫫ : ∀ {A B} {t : Γ ⁏ Δ ⊢ ⫫}
-- {r : ∀ {Γ′ Δ′} → Γ′ ⁏ Δ′ ⊢ A → Γ′ ⁏ Δ′ ⊢ B} →
-- r (boom t) ≣ boom t
com⫫app : ∀ {A B} {t : Γ ⁏ Δ ⊢ ⫫}
{u : Γ ⁏ Δ ⊢ A} →
app {A = A} {B} (boom t) u ≣ boom t
com⫫unbox : ∀ {A C} {t : Γ ⁏ Δ ⊢ ⫫}
{u : Γ ⁏ Δ , A ⊢ C} →
unbox {A = A} {C} (boom t) u ≣ boom t
com⫫fst : ∀ {A B} {t : Γ ⁏ Δ ⊢ ⫫} →
fst {A = A} {B} (boom t) ≣ boom t
com⫫snd : ∀ {A B} {t : Γ ⁏ Δ ⊢ ⫫} →
snd {A = A} {B} (boom t) ≣ boom t
com⫫boom : ∀ {C} {t : Γ ⁏ Δ ⊢ ⫫} →
boom {C = C} (boom t) ≣ boom t
com⫫case : ∀ {A B C} {t : Γ ⁏ Δ ⊢ ⫫}
{u : Γ , A ⁏ Δ ⊢ C}
{v : Γ , B ⁏ Δ ⊢ C} →
case {A = A} {B} {C} (boom t) u v ≣ boom t
-- Commuting conversions for ⩖.
--
-- NOTE: Generated by instantiating the following schema with elimination rules.
--
-- com⩖ : ∀ {A B X Y} {t : Γ ⁏ Δ ⊢ X ⩖ Y}
-- {u : Γ , X ⁏ Δ ⊢ A}
-- {v : Γ , Y ⁏ Δ ⊢ A}
-- {r : ∀ {Γ′ Δ′} → Γ′ ⁏ Δ′ ⊢ A → Γ′ ⁏ Δ′ ⊢ B} →
-- r (case t u v) ≣ case t (r u) (r v)
com⩖app : ∀ {A B X Y} {t : Γ ⁏ Δ ⊢ X ⩖ Y}
{u : Γ , X ⁏ Δ ⊢ A ⇒ B}
{v : Γ , Y ⁏ Δ ⊢ A ⇒ B}
{w : Γ ⁏ Δ ⊢ A} →
app (case t u v) w ≣ case t (app u (mono⊢ weak⊆ refl⊆ w))
(app v (mono⊢ weak⊆ refl⊆ w))
com⩖unbox : ∀ {A C X Y} {t : Γ ⁏ Δ ⊢ X ⩖ Y}
{u : Γ , X ⁏ Δ ⊢ □ A}
{v : Γ , Y ⁏ Δ ⊢ □ A}
{w : Γ ⁏ Δ , A ⊢ C} →
unbox (case t u v) w ≣ case t (unbox u (mono⊢ weak⊆ refl⊆ w))
(unbox v (mono⊢ weak⊆ refl⊆ w))
com⩖fst : ∀ {A B X Y} {t : Γ ⁏ Δ ⊢ X ⩖ Y}
{u : Γ , X ⁏ Δ ⊢ A ⩕ B}
{v : Γ , Y ⁏ Δ ⊢ A ⩕ B} →
fst (case t u v) ≣ case t (fst u) (fst v)
com⩖snd : ∀ {A B X Y} {t : Γ ⁏ Δ ⊢ X ⩖ Y}
{u : Γ , X ⁏ Δ ⊢ A ⩕ B}
{v : Γ , Y ⁏ Δ ⊢ A ⩕ B} →
snd (case t u v) ≣ case t (snd u) (snd v)
com⩖boom : ∀ {C X Y} {t : Γ ⁏ Δ ⊢ X ⩖ Y}
{u : Γ , X ⁏ Δ ⊢ ⫫}
{v : Γ , Y ⁏ Δ ⊢ ⫫} →
boom {C = C} (case t u v) ≣ case t (boom u) (boom v)
com⩖case : ∀ {A B C X Y} {t : Γ ⁏ Δ ⊢ X ⩖ Y}
{u : Γ , X ⁏ Δ ⊢ A ⩖ B}
{v : Γ , Y ⁏ Δ ⊢ A ⩖ B}
{w : Γ , A ⁏ Δ ⊢ C}
{x : Γ , B ⁏ Δ ⊢ C} →
case (case t u v) w x ≣ case t (case u (mono⊢ (keep weak⊆) refl⊆ w)
(mono⊢ (keep weak⊆) refl⊆ x))
(case v (mono⊢ (keep weak⊆) refl⊆ w)
(mono⊢ (keep weak⊆) refl⊆ x))
lift≣ : ∀ {Γ Δ A} {t t′ : Γ ⁏ Δ ⊢ A} → t ≡ t′ → t ≣ t′
lift≣ refl = refl≣
-- Syntax for equational reasoning with convertibility.
module ≣-Reasoning where
infix 1 begin_
begin_ : ∀ {Γ Δ A} {t t′ : Γ ⁏ Δ ⊢ A} → t ≣ t′ → t ≣ t′
begin_ p = p
infixr 2 _≣⟨⟩_
_≣⟨⟩_ : ∀ {Γ Δ A} (t {t′} : Γ ⁏ Δ ⊢ A) → t ≣ t′ → t ≣ t′
_ ≣⟨⟩ p = p
infixr 2 _≣⟨_⟩_
_≣⟨_⟩_ : ∀ {Γ Δ A} (t {t′ t″} : Γ ⁏ Δ ⊢ A) → t ≣ t′ → t′ ≣ t″ → t ≣ t″
_ ≣⟨ p ⟩ q = trans≣ p q
infix 3 _∎
_∎ : ∀ {Γ Δ A} (t : Γ ⁏ Δ ⊢ A) → t ≣ t
_∎ _ = refl≣
Raw
S4NbE.agda
module S4NbE where
open import S4NormalForm public
-- Strong forcing and forcing.
mutual
infix 3 _⁏_⊪_
_⁏_⊪_ : Seq → Seq → Prop → Set
Γ ⁏ Δ ⊪ A ⇒ B = ∀ {Γ′ Δ′} → Γ ⊆ Γ′ → Δ ⊆ Δ′ →
Γ′ ⁏ Δ′ ⊩ A → Γ′ ⁏ Δ′ ⊩ B
Γ ⁏ Δ ⊪ □ A = ∀ {Δ′} → Δ ⊆ Δ′ →
∅ ⁏ Δ′ ⊢ A ∧ ∅ ⁏ Δ′ ⊩ A
Γ ⁏ Δ ⊪ A ⩕ B = Γ ⁏ Δ ⊩ A ∧ Γ ⁏ Δ ⊩ B
Γ ⁏ Δ ⊪ ⫪ = ⊤
Γ ⁏ Δ ⊪ ⫫ = ⊥
Γ ⁏ Δ ⊪ A ⩖ B = Γ ⁏ Δ ⊩ A ∨ Γ ⁏ Δ ⊩ B
infix 3 _⁏_⊩_
_⁏_⊩_ : Seq → Seq → Prop → Set
Γ ⁏ Δ ⊩ A = ∀ {Γ′ Δ′ C} → Γ ⊆ Γ′ → Δ ⊆ Δ′ →
(∀ {Γ″ Δ″} → Γ′ ⊆ Γ″ → Δ′ ⊆ Δ″ →
Γ″ ⁏ Δ″ ⊪ A →
Γ″ ⁏ Δ″ ⊢ⁿᶠ C) →
Γ′ ⁏ Δ′ ⊢ⁿᶠ C
infix 3 _⁏_⊩⋆_
_⁏_⊩⋆_ : Seq → Seq → Seq → Set
Γ ⁏ Δ ⊩⋆ ∅ = ⊤
Γ ⁏ Δ ⊩⋆ Ξ , A = Γ ⁏ Δ ⊩⋆ Ξ ∧ Γ ⁏ Δ ⊩ A
-- Monotonicity with respect to context inclusion.
mutual
mono⊪ : ∀ {A Γ Γ′ Δ Δ′} → Γ ⊆ Γ′ → Δ ⊆ Δ′ → Γ ⁏ Δ ⊪ A → Γ′ ⁏ Δ′ ⊪ A
mono⊪ {A ⇒ B} η θ f = λ η′ θ′ a → f (trans⊆ η η′) (trans⊆ θ θ′) a
mono⊪ {□ A} η θ f = λ θ′ → f (trans⊆ θ θ′)
mono⊪ {A ⩕ B} η θ (a , b) = mono⊩ {A} η θ a , mono⊩ {B} η θ b
mono⊪ {⫪} η θ ∙ = ∙
mono⊪ {⫫} η θ ()
mono⊪ {A ⩖ B} η θ (ι₁ a) = ι₁ (mono⊩ {A} η θ a)
mono⊪ {A ⩖ B} η θ (ι₂ b) = ι₂ (mono⊩ {B} η θ b)
mono⊩ : ∀ {A Γ Γ′ Δ Δ′} → Γ ⊆ Γ′ → Δ ⊆ Δ′ → Γ ⁏ Δ ⊩ A → Γ′ ⁏ Δ′ ⊩ A
mono⊩ η θ a = λ η′ θ′ κ → a (trans⊆ η η′) (trans⊆ θ θ′) κ
mono⊩⋆ : ∀ {Ξ Γ Γ′ Δ Δ′} → Γ ⊆ Γ′ → Δ ⊆ Δ′ → Γ ⁏ Δ ⊩⋆ Ξ → Γ′ ⁏ Δ′ ⊩⋆ Ξ
mono⊩⋆ {∅} η θ ∙ = ∙
mono⊩⋆ {Ξ , A} η θ (σ , a) = mono⊩⋆ {Ξ} η θ σ , mono⊩ {A} η θ a
-- Semantic entailment, or forcing in all worlds of all (implicit) models.
infix 3 _⁏_⊨_
_⁏_⊨_ : Seq → Seq → Prop → Set
Γ ⁏ Δ ⊨ A = ∀ {Γ′ Δ′} → Γ′ ⁏ Δ′ ⊩⋆ Γ →
∅ ⁏ Δ′ ⊢⋆ Δ → -- TODO: Think about this.
∅ ⁏ Δ′ ⊩⋆ Δ → -- Should these two be tied together, somehow?
Γ′ ⁏ Δ′ ⊩ A
-- Additional useful equipment.
apply : ∀ {A B Γ Δ} → Γ ⁏ Δ ⊪ A ⇒ B → Γ ⁏ Δ ⊩ A → Γ ⁏ Δ ⊩ B
apply f a = f refl⊆ refl⊆ a
return : ∀ {A Γ Δ} → Γ ⁏ Δ ⊪ A → Γ ⁏ Δ ⊩ A
return {A} a = λ η θ κ → κ refl⊆ refl⊆ (mono⊪ {A} η θ a)
bind : ∀ {A B Γ Δ} → Γ ⁏ Δ ⊩ A →
(∀ {Γ′ Δ′} → Γ ⊆ Γ′ → Δ ⊆ Δ′ → Γ′ ⁏ Δ′ ⊪ A → Γ′ ⁏ Δ′ ⊩ B) →
Γ ⁏ Δ ⊩ B
bind a κ = λ η θ κ′ → a η θ
λ η′ θ′ a′ → κ (trans⊆ η η′) (trans⊆ θ θ′) a′ refl⊆ refl⊆
λ η″ θ″ a″ → κ′ (trans⊆ η′ η″) (trans⊆ θ′ θ″) a″
-- Soundness with respect to all (implicit) models, or evaluation.
lookup : ∀ {Γ Δ Ξ A} → A ∈ Ξ → Γ ⁏ Δ ⊩⋆ Ξ → Γ ⁏ Δ ⊩ A
lookup top (σ , a) = a
lookup (pop i) (σ , b) = lookup i σ
eval : ∀ {A Γ Δ} → Γ ⁏ Δ ⊢ A → Γ ⁏ Δ ⊨ A
eval (var i) γ σ δ = lookup i γ
eval (ᵐvar {A} i) γ σ δ = mono⊩ {A} zero⊆ refl⊆ (lookup i δ)
eval (lam {A} {B} t) γ σ δ = return {A ⇒ B}
λ η θ a → eval t (mono⊩⋆ η θ γ , a)
(mono⊢⋆ done θ σ)
(mono⊩⋆ done θ δ)
eval (app {A} {B} t u) γ σ δ = bind {A ⇒ B} {B} (eval t γ σ δ)
λ η θ f → apply {A} {B} f (mono⊩ {A} η θ (eval u γ σ δ))
eval (box {A} t) γ σ δ = return {□ A}
λ θ → ᵐgraft⊢⋆ (mono⊢⋆ done θ σ) (mono⊢ zero⊆ refl⊆ t) ,
mono⊩ {A} done θ (eval t ∙ σ δ)
eval (unbox {A} {C} t u) γ σ δ = bind {□ A} {C} (eval t γ σ δ)
λ η θ a → eval u (mono⊩⋆ η θ γ)
(mono⊢⋆ done θ σ , π₁ (a refl⊆))
(mono⊩⋆ done θ δ , π₂ (a refl⊆))
eval (pair {A} {B} t u) γ σ δ = return {A ⩕ B} (eval t γ σ δ , eval u γ σ δ)
eval (fst {A} {B} t) γ σ δ = bind {A ⩕ B} {A} (eval t γ σ δ) (λ _ _ → π₁)
eval (snd {A} {B} t) γ σ δ = bind {A ⩕ B} {B} (eval t γ σ δ) (λ _ _ → π₂)
eval unit γ σ δ = return {⫪} ∙
eval (boom {C} t) γ σ δ = bind {⫫} {C} (eval t γ σ δ) (λ _ _ → elim⊥)
eval (left {A} {B} t) γ σ δ = return {A ⩖ B} (ι₁ (eval t γ σ δ))
eval (right {A} {B} t) γ σ δ = return {A ⩖ B} (ι₂ (eval t γ σ δ))
eval (case {A} {B} {C} t u v) γ σ δ = bind {A ⩖ B} {C} (eval t γ σ δ)
λ { η θ (ι₁ a) → eval u (mono⊩⋆ η θ γ , a)
(mono⊢⋆ done θ σ)
(mono⊩⋆ done θ δ)
; η θ (ι₂ b) → eval v (mono⊩⋆ η θ γ , b)
(mono⊢⋆ done θ σ)
(mono⊩⋆ done θ δ)
}
-- Soundness and completeness with respect to the (implicit) canonical model.
mutual
reflectᶜ : ∀ {A Γ Δ} → Γ ⁏ Δ ⊢ⁿᵉ A → Γ ⁏ Δ ⊩ A
reflectᶜ {A ⇒ B} t = return {A ⇒ B}
λ η θ a → reflectᶜ (appⁿᵉ (mono⊢ⁿᵉ η θ t) (reifyᶜ a))
reflectᶜ {□ A} t = λ η θ κ → neⁿᶠ (unboxⁿᵉ (mono⊢ⁿᵉ η θ t)
(κ refl⊆ weak⊆
λ θ′ → ᵐvar (mono∈ θ′ top) ,
reflectᶜ (ᵐvarⁿᵉ (mono∈ θ′ top))))
reflectᶜ {A ⩕ B} t = return {A ⩕ B} (reflectᶜ (fstⁿᵉ t) , reflectᶜ (sndⁿᵉ t))
reflectᶜ {⫪} t = return {⫪} ∙
reflectᶜ {⫫} t = λ η θ κ → neⁿᶠ (boomⁿᵉ (mono⊢ⁿᵉ η θ t))
reflectᶜ {A ⩖ B} t = λ η θ κ → neⁿᶠ (caseⁿᵉ (mono⊢ⁿᵉ η θ t)
(κ weak⊆ refl⊆ (ι₁ (reflectᶜ v₀ⁿᵉ)))
(κ weak⊆ refl⊆ (ι₂ (reflectᶜ v₀ⁿᵉ))))
reifyᶜ : ∀ {A Γ Δ} → Γ ⁏ Δ ⊩ A → Γ ⁏ Δ ⊢ⁿᶠ A
reifyᶜ {A ⇒ B} κ = κ refl⊆ refl⊆
λ η θ f → lamⁿᶠ (reifyᶜ (f weak⊆ refl⊆ (reflectᶜ v₀ⁿᵉ)))
reifyᶜ {□ A} κ = κ refl⊆ refl⊆
λ η θ f → boxⁿᶠ (π₁ (f refl⊆))
reifyᶜ {A ⩕ B} κ = κ refl⊆ refl⊆
λ { η θ (a , b) → pairⁿᶠ (reifyᶜ a) (reifyᶜ b) }
reifyᶜ {⫪} κ = κ refl⊆ refl⊆
λ { η θ ∙ → unitⁿᶠ }
reifyᶜ {⫫} κ = κ refl⊆ refl⊆
λ { η θ () }
reifyᶜ {A ⩖ B} κ = κ refl⊆ refl⊆
λ { η θ (ι₁ a) → leftⁿᶠ (reifyᶜ a)
; η θ (ι₂ b) → rightⁿᶠ (reifyᶜ b)
}
reflectᶜ⋆ : ∀ {Ξ Γ Δ} → Γ ⁏ Δ ⊢⋆ⁿᵉ Ξ → Γ ⁏ Δ ⊩⋆ Ξ
reflectᶜ⋆ {∅} ∙ = ∙
reflectᶜ⋆ {Ξ , A} (τ , t) = reflectᶜ⋆ τ , reflectᶜ t
-- TODO: Explain this.
refl⊩⋆ : ∀ {Γ Δ} → Γ ⁏ Δ ⊩⋆ Γ
refl⊩⋆ = reflectᶜ⋆ refl⊢⋆ⁿᵉ
ᵐrefl⊩⋆ : ∀ {Δ} → ∅ ⁏ Δ ⊩⋆ Δ
ᵐrefl⊩⋆ = reflectᶜ⋆ ᵐrefl⊢⋆ⁿᵉ
-- Completeness with respect to all (implicit) models, or quotation.
quot : ∀ {A Γ Δ} → Γ ⁏ Δ ⊨ A → Γ ⁏ Δ ⊢ⁿᶠ A
quot s = reifyᶜ (s refl⊩⋆ ᵐrefl⊢⋆ ᵐrefl⊩⋆)
-- Normalisation by evaluation.
nbe : ∀ {A Γ Δ} → Γ ⁏ Δ ⊢ A → Γ ⁏ Δ ⊢ⁿᶠ A
nbe t = quot (eval t)
Raw
S4NbECorrectness.agda
module S4NbECorrectness where
open import S4Convertibility public
open import S4NbE public
open ≣-Reasoning
-- TODO: Show this.
postulate
sound : ∀ {Γ Δ A} {t t′ : Γ ⁏ Δ ⊢ A} → t ≣ t′ → nbe t ≡ nbe t′
-- TODO: Show this.
postulate
complete : ∀ {Γ Δ A} → (t : Γ ⁏ Δ ⊢ A) → nf→tm (nbe t) ≣ t
complete′ : ∀ {Γ Δ A} → (t t′ : Γ ⁏ Δ ⊢ A) → nbe t ≡ nbe t′ → t ≣ t′
complete′ t t′ p =
t ≣⟨ sym≣ (complete t) ⟩
nf→tm (nbe t) ≣⟨ lift≣ (cong nf→tm p) ⟩
nf→tm (nbe t′) ≣⟨ complete t′ ⟩
t′ ∎
correct : ∀ {Γ Δ A} {t t′ : Γ ⁏ Δ ⊢ A} → t ≣ t′ ↔ nbe t ≡ nbe t′
correct {t = t} {t′} = sound , complete′ _ _
-- TODO: Show this.
postulate
stable : ∀ {Γ Δ A} {t : Γ ⁏ Δ ⊢ⁿᶠ A} → nbe (nf→tm t) ≡ t
Raw
S4NbEExplicit.agda
{-# OPTIONS --rewriting #-}
module S4NbEExplicit where
open import S4NormalForm public
-- Intuitionistic Kripke-CPS models with syntax representation.
record Model : Set₁ where
infix 3 _≤ᴸ_ _≤ᴿ_
field
World : Set
-- Minimal world.
w₀ : World
-- Non-modal accessibility; preorder.
_≤ᴸ_ : World → World → Set
refl≤ᴸ : ∀ {w} → w ≤ᴸ w
trans≤ᴸ : ∀ {w w′ w″} → w ≤ᴸ w′ → w′ ≤ᴸ w″ → w ≤ᴸ w″
-- Modal accessibility; preorder.
_≤ᴿ_ : World → World → Set
refl≤ᴿ : ∀ {w} → w ≤ᴿ w
trans≤ᴿ : ∀ {w w′ w″} → w ≤ᴿ w′ → w′ ≤ᴿ w″ → w ≤ᴿ w″
-- Intuitionistic accessibility; preorder.
infix 3 _≤_
_≤_ : World → World → Set
_≤_ = λ w w′ → w ≤ᴸ w′ ∧ w ≤ᴿ w′
infixl 7 _⧺ᴸ_ _⧺ᴿ_
field
-- Non-modal and modal travel.
_⧺ᴸ_ : World → Seq → World
_⧺ᴿ_ : World → Seq → World
-- Context representation.
infix 4 _⨾_
_⨾_ : Seq → Seq → World
_⨾_ = λ Γ Δ → w₀ ⧺ᴸ Γ ⧺ᴿ Δ
field
-- Non-modal context representation.
pokeᴸ : ∀ {Γ Γ′ Δ Δ′} → Γ ⊆ Γ′ → Γ ⨾ Δ ≤ᴸ Γ′ ⨾ Δ′
peekᴸ : ∀ {Γ Γ′ Δ Δ′} → Γ ⨾ Δ ≤ᴸ Γ′ ⨾ Δ′ → Γ ⊆ Γ′
-- Modal context representation.
pokeᴿ : ∀ {Γ Γ′ Δ Δ′} → Δ ⊆ Δ′ → Γ ⨾ Δ ≤ᴿ Γ′ ⨾ Δ′
peekᴿ : ∀ {Γ Γ′ Δ Δ′} → Γ ⨾ Δ ≤ᴿ Γ′ ⨾ Δ′ → Δ ⊆ Δ′
-- Proof representation; monotonic.
infix 3 _⊫_ _⊫ⁿᶠ_
field
_⊫_ : World → Prop → Set
mono⊫ : ∀ {w w′ A} → w ≤ w′ → w ⊫ A → w′ ⊫ A
-- Structure of proof representation.
⟪var⟫ : ∀ {Γ Δ A} → A ∈ Γ → Γ ⨾ Δ ⊫ A
⟪ᵐvar⟫ : ∀ {Γ Δ A} → A ∈ Δ → Γ ⨾ Δ ⊫ A
⟪lam⟫ : ∀ {Γ Δ A B} → (Γ , A) ⨾ Δ ⊫ B → Γ ⨾ Δ ⊫ A ⇒ B
⟪app⟫ : ∀ {Γ Δ A B} → Γ ⨾ Δ ⊫ A ⇒ B → Γ ⨾ Δ ⊫ A → Γ ⨾ Δ ⊫ B
⟪box⟫ : ∀ {Γ Δ A} → ∅ ⨾ Δ ⊫ A → Γ ⨾ Δ ⊫ □ A
⟪unbox⟫ : ∀ {Γ Δ A C} → Γ ⨾ Δ ⊫ □ A → Γ ⨾ (Δ , A) ⊫ C → Γ ⨾ Δ ⊫ C
⟪pair⟫ : ∀ {Γ Δ A B} → Γ ⨾ Δ ⊫ A → Γ ⨾ Δ ⊫ B → Γ ⨾ Δ ⊫ A ⩕ B
⟪fst⟫ : ∀ {Γ Δ A B} → Γ ⨾ Δ ⊫ A ⩕ B → Γ ⨾ Δ ⊫ A
⟪snd⟫ : ∀ {Γ Δ A B} → Γ ⨾ Δ ⊫ A ⩕ B → Γ ⨾ Δ ⊫ B
⟪unit⟫ : ∀ {Γ Δ} → Γ ⨾ Δ ⊫ ⫪
⟪boom⟫ : ∀ {Γ Δ C} → Γ ⨾ Δ ⊫ ⫫ → Γ ⨾ Δ ⊫ C
⟪left⟫ : ∀ {Γ Δ A B} → Γ ⨾ Δ ⊫ A → Γ ⨾ Δ ⊫ A ⩖ B
⟪right⟫ : ∀ {Γ Δ A B} → Γ ⨾ Δ ⊫ B → Γ ⨾ Δ ⊫ A ⩖ B
⟪case⟫ : ∀ {Γ Δ A B C} → Γ ⨾ Δ ⊫ A ⩖ B → (Γ , A) ⨾ Δ ⊫ C → (Γ , B) ⨾ Δ ⊫ C → Γ ⨾ Δ ⊫ C
-- Normal form representation; for CPS.
_⊫ⁿᶠ_ : World → Prop → Set
-- Simultaneous substitution.
infix 3 _⊫⍟_
field
-- NOTE: Workaround for Agda bug #2143.
_⊫⍟_ : World → Seq → Set
top⊫⍟ : ∀ {w} → (w ⊫⍟ ∅) ≡ ⊤
pop⊫⍟ : ∀ {w Ξ A} → (w ⊫⍟ Ξ , A) ≡ (w ⊫⍟ Ξ ∧ w ⊫ A)
ᵐgraft⊫⍟ : ∀ {Γ Δ Δ′ C} → ∅ ⨾ Δ′ ⊫⍟ Δ → Γ ⨾ Δ ⊫ C → Γ ⨾ Δ′ ⊫ C
open Model {{…}} public
-- Continued: intuitionistic accessibility; preorder.
module _ {{_ : Model}} where
refl≤ : ∀ {w} → w ≤ w
refl≤ = refl≤ᴸ , refl≤ᴿ
trans≤ : ∀ {w w′ w″} → w ≤ w′ → w′ ≤ w″ → w ≤ w″
trans≤ = λ { (η , θ) (η′ , θ′) → trans≤ᴸ η η′ , trans≤ᴿ θ θ′ }
≤→≤ᴿ : ∀ {w w′} → w ≤ w′ → w ≤ᴿ w′
≤→≤ᴿ = π₂
≤→⌊≤⌋ : ∀ {Γ Γ′ Δ Δ′} → Γ ⨾ Δ ≤ Γ′ ⨾ Δ′ → ∅ ⨾ Δ ≤ ∅ ⨾ Δ′
≤→⌊≤⌋ = λ { (η , θ) → pokeᴸ refl⊆ , pokeᴿ (peekᴿ θ) }
≤ᴿ→⌊≤⌋ : ∀ {Γ Γ′ Δ Δ′} → Γ ⨾ Δ ≤ᴿ Γ′ ⨾ Δ′ → ∅ ⨾ Δ ≤ ∅ ⨾ Δ′
≤ᴿ→⌊≤⌋ = λ { θ → pokeᴸ refl⊆ , pokeᴿ (peekᴿ θ) }
zerorefl≤ : ∀ {Γ Δ} → ∅ ⨾ Δ ≤ Γ ⨾ Δ
zerorefl≤ = pokeᴸ zero⊆ , pokeᴿ refl⊆
-- Continued: structure of proof representation.
module _ {{_ : Model}} where
⟪_⟫ : ∀ {Γ Δ A} → Γ ⁏ Δ ⊢ A → Γ ⨾ Δ ⊫ A
⟪ var i ⟫ = ⟪var⟫ i
⟪ ᵐvar i ⟫ = ⟪ᵐvar⟫ i
⟪ lam t ⟫ = ⟪lam⟫ ⟪ t ⟫
⟪ app t u ⟫ = ⟪app⟫ ⟪ t ⟫ ⟪ u ⟫
⟪ box t ⟫ = ⟪box⟫ ⟪ t ⟫
⟪ unbox t u ⟫ = ⟪unbox⟫ ⟪ t ⟫ ⟪ u ⟫
⟪ pair t u ⟫ = ⟪pair⟫ ⟪ t ⟫ ⟪ u ⟫
⟪ fst t ⟫ = ⟪fst⟫ ⟪ t ⟫
⟪ snd t ⟫ = ⟪snd⟫ ⟪ t ⟫
⟪ unit ⟫ = ⟪unit⟫
⟪ boom t ⟫ = ⟪boom⟫ ⟪ t ⟫
⟪ left t ⟫ = ⟪left⟫ ⟪ t ⟫
⟪ right t ⟫ = ⟪right⟫ ⟪ t ⟫
⟪ case t u v ⟫ = ⟪case⟫ ⟪ t ⟫ ⟪ u ⟫ ⟪ v ⟫
infix 3 _⊫⋆_
_⊫⋆_ : World → Seq → Set
w ⊫⋆ ∅ = ⊤
w ⊫⋆ Ξ , A = w ⊫⋆ Ξ ∧ w ⊫ A
mono⊫⋆ : ∀ {Ξ w w′} → w ≤ w′ → w ⊫⋆ Ξ → w′ ⊫⋆ Ξ
mono⊫⋆ {∅} ξ ∙ = ∙
mono⊫⋆ {Ξ , A} ξ (τ , t) = mono⊫⋆ ξ τ , mono⊫ ξ t
-- Continued: simultaneous substitution.
module _ {{_ : Model}} where
⊫⍟→⊫⋆ : ∀ {Ξ w} → w ⊫⍟ Ξ → w ⊫⋆ Ξ
⊫⍟→⊫⋆ {∅} {w} τ = ∙
⊫⍟→⊫⋆ {Ξ , A} {w} τ rewrite pop⊫⍟ {w} {Ξ} {A} = ⊫⍟→⊫⋆ (π₁ τ) , π₂ τ
⊫⋆→⊫⍟ : ∀ {Ξ w} → w ⊫⋆ Ξ → w ⊫⍟ Ξ
⊫⋆→⊫⍟ {∅} {w} ∙ rewrite top⊫⍟ {w} = ∙
⊫⋆→⊫⍟ {Ξ , A} {w} (τ , t) rewrite pop⊫⍟ {w} {Ξ} {A} = ⊫⋆→⊫⍟ τ , t
ᵐgraft⊫⋆ : ∀ {Γ Δ Δ′ C} → ∅ ⨾ Δ′ ⊫⋆ Δ → Γ ⨾ Δ ⊫ C → Γ ⨾ Δ′ ⊫ C
ᵐgraft⊫⋆ τ = ᵐgraft⊫⍟ (⊫⋆→⊫⍟ τ)
-- Strong forcing and forcing.
module _ {{_ : Model}} where
mutual
infix 3 _⊪_
_⊪_ : World → Prop → Set
w ⊪ A ⇒ B = ∀ {Γ′ Δ′} → w ≤ Γ′ ⨾ Δ′ →
Γ′ ⨾ Δ′ ⊩ A → Γ′ ⨾ Δ′ ⊩ B
w ⊪ □ A = ∀ {Γ′ Δ′} → w ≤ᴿ Γ′ ⨾ Δ′ →
∅ ⨾ Δ′ ⊫ A ∧ ∅ ⨾ Δ′ ⊩ A
w ⊪ A ⩕ B = w ⊩ A ∧ w ⊩ B
w ⊪ ⫪ = ⊤
w ⊪ ⫫ = ⊥
w ⊪ A ⩖ B = w ⊩ A ∨ w ⊩ B
infix 3 _⊩_
_⊩_ : World → Prop → Set
w ⊩ A = ∀ {Γ′ Δ′ C} → w ≤ Γ′ ⨾ Δ′ →
(∀ {Γ″ Δ″} → Γ′ ⨾ Δ′ ≤ Γ″ ⨾ Δ″ →
Γ″ ⨾ Δ″ ⊪ A →
Γ″ ⨾ Δ″ ⊫ⁿᶠ C) →
Γ′ ⨾ Δ′ ⊫ⁿᶠ C
infix 3 _⊩⋆_
_⊩⋆_ : World → Seq → Set
w ⊩⋆ ∅ = ⊤
w ⊩⋆ Ξ , A = w ⊩⋆ Ξ ∧ w ⊩ A
-- Monotonicity with respect to context inclusion.
module _ {{_ : Model}} where
mutual
mono⊪ : ∀ {A w w′} → w ≤ w′ → w ⊪ A → w′ ⊪ A
mono⊪ {A ⇒ B} ξ f = λ ξ′ a → f (trans≤ ξ ξ′) a
mono⊪ {□ A} ξ f = λ ζ → f (trans≤ᴿ (≤→≤ᴿ ξ) ζ)
mono⊪ {A ⩕ B} ξ (a , b) = mono⊩ {A} ξ a , mono⊩ {B} ξ b
mono⊪ {⫪} ξ ∙ = ∙
mono⊪ {⫫} ξ ()
mono⊪ {A ⩖ B} ξ (ι₁ a) = ι₁ (mono⊩ {A} ξ a)
mono⊪ {A ⩖ B} ξ (ι₂ b) = ι₂ (mono⊩ {B} ξ b)
mono⊩ : ∀ {A w w′} → w ≤ w′ → w ⊩ A → w′ ⊩ A
mono⊩ ξ a = λ ξ′ κ → a (trans≤ ξ ξ′) κ
mono⊩⋆ : ∀ {Ξ w w′} → w ≤ w′ → w ⊩⋆ Ξ → w′ ⊩⋆ Ξ
mono⊩⋆ {∅} ξ ∙ = ∙
mono⊩⋆ {Ξ , A} ξ (σ , a) = mono⊩⋆ {Ξ} ξ σ , mono⊩ {A} ξ a
-- Semantic entailment, or forcing in all worlds of all models.
infix 3 _⁏_⊨_
_⁏_⊨_ : Seq → Seq → Prop → Set₁
Γ ⁏ Δ ⊨ A = ∀ {{_ : Model}} {Γ′ Δ′} → Γ′ ⨾ Δ′ ⊩⋆ Γ →
∅ ⨾ Δ′ ⊫⋆ Δ → -- TODO: Think about this.
∅ ⨾ Δ′ ⊩⋆ Δ → -- Should these two be tied together, somehow?
Γ′ ⨾ Δ′ ⊩ A
-- Additional useful equipment.
module _ {{_ : Model}} where
apply : ∀ {A B Γ Δ} → Γ ⨾ Δ ⊪ A ⇒ B → Γ ⨾ Δ ⊩ A → Γ ⨾ Δ ⊩ B
apply f a = f refl≤ a
return : ∀ {A Γ Δ} → Γ ⨾ Δ ⊪ A → Γ ⨾ Δ ⊩ A
return {A} a = λ ξ κ → κ refl≤ (mono⊪ {A} ξ a)
bind : ∀ {A B Γ Δ} → Γ ⨾ Δ ⊩ A →
(∀ {Γ′ Δ′} → Γ ⨾ Δ ≤ Γ′ ⨾ Δ′ → Γ′ ⨾ Δ′ ⊪ A → Γ′ ⨾ Δ′ ⊩ B) →
Γ ⨾ Δ ⊩ B
bind a κ = λ ξ κ′ → a ξ
λ ξ′ a′ → κ (trans≤ ξ ξ′) a′ refl≤
λ ξ″ a″ → κ′ (trans≤ ξ′ ξ″) a″
-- Soundness with respect to all models, or evaluation.
module _ {{_ : Model}} where
lookup : ∀ {Γ Δ Ξ A} → A ∈ Ξ → Γ ⨾ Δ ⊩⋆ Ξ → Γ ⨾ Δ ⊩ A
lookup top (σ , a) = a
lookup (pop i) (σ , b) = lookup i σ
eval : ∀ {A Γ Δ} → Γ ⁏ Δ ⊢ A → Γ ⁏ Δ ⊨ A
eval (var i) γ σ δ = lookup i γ
eval (ᵐvar {A} i) γ σ δ = mono⊩ {A} zerorefl≤ (lookup i δ)
eval (lam {A} {B} t) γ σ δ = return {A ⇒ B}
λ ξ a → eval t (mono⊩⋆ ξ γ , a)
(mono⊫⋆ (≤→⌊≤⌋ ξ) σ)
(mono⊩⋆ (≤→⌊≤⌋ ξ) δ)
eval (app {A} {B} t u) γ σ δ = bind {A ⇒ B} {B} (eval t γ σ δ)
λ ξ f → apply {A} {B} f (mono⊩ {A} ξ (eval u γ σ δ))
eval (box {A} t) γ σ δ = return {□ A}
λ ζ → ᵐgraft⊫⋆ (mono⊫⋆ (≤ᴿ→⌊≤⌋ ζ) σ) ⟪ t ⟫ ,
mono⊩ {A} (≤ᴿ→⌊≤⌋ ζ) (eval t ∙ σ δ)
eval (unbox {A} {C} t u) γ σ δ = bind {□ A} {C} (eval t γ σ δ)
λ ξ a → eval u (mono⊩⋆ ξ γ)
(mono⊫⋆ (≤→⌊≤⌋ ξ) σ , π₁ (a refl≤ᴿ))
(mono⊩⋆ (≤→⌊≤⌋ ξ) δ , π₂ (a refl≤ᴿ))
eval (pair {A} {B} t u) γ σ δ = return {A ⩕ B} (eval t γ σ δ , eval u γ σ δ)
eval (fst {A} {B} t) γ σ δ = bind {A ⩕ B} {A} (eval t γ σ δ) (λ _ → π₁)
eval (snd {A} {B} t) γ σ δ = bind {A ⩕ B} {B} (eval t γ σ δ) (λ _ → π₂)
eval unit γ σ δ = return {⫪} ∙
eval (boom {C} t) γ σ δ = bind {⫫} {C} (eval t γ σ δ) (λ _ → elim⊥)
eval (left {A} {B} t) γ σ δ = return {A ⩖ B} (ι₁ (eval t γ σ δ))
eval (right {A} {B} t) γ σ δ = return {A ⩖ B} (ι₂ (eval t γ σ δ))
eval (case {A} {B} {C} t u v) γ σ δ = bind {A ⩖ B} {C} (eval t γ σ δ)
λ { ξ (ι₁ a) → eval u (mono⊩⋆ ξ γ , a)
(mono⊫⋆ (≤→⌊≤⌋ ξ) σ)
(mono⊩⋆ (≤→⌊≤⌋ ξ) δ)
; ξ (ι₂ b) → eval v (mono⊩⋆ ξ γ , b)
(mono⊫⋆ (≤→⌊≤⌋ ξ) σ)
(mono⊩⋆ (≤→⌊≤⌋ ξ) δ)
}
-- The canonical model.
{-# BUILTIN REWRITE _≡_ #-}
{-# REWRITE id⧺ #-}
private
instance
canon : Model
canon = record
{ World = Seq ∧ Seq
; w₀ = ∅ , ∅
; _≤ᴸ_ = λ { (Γ , Δ) (Γ′ , Δ′) → Γ ⊆ Γ′ }
; refl≤ᴸ = refl⊆
; trans≤ᴸ = trans⊆
; _≤ᴿ_ = λ { (Γ , Δ) (Γ′ , Δ′) → Δ ⊆ Δ′ }
; refl≤ᴿ = refl⊆
; trans≤ᴿ = trans⊆
; _⧺ᴸ_ = λ { (Γ , Δ) Γ′ → Γ ⧺ Γ′ , Δ }
; _⧺ᴿ_ = λ { (Γ , Δ) Δ′ → Γ , Δ ⧺ Δ′ }
; pokeᴸ = λ η → η
; peekᴸ = λ η → η
; pokeᴿ = λ θ → θ
; peekᴿ = λ θ → θ
; _⊫_ = λ { (Γ , Δ) → Γ ⁏ Δ ⊢_ }
; ⟪var⟫ = var
; ⟪ᵐvar⟫ = ᵐvar
; ⟪lam⟫ = lam
; ⟪app⟫ = app
; ⟪box⟫ = box
; ⟪unbox⟫ = unbox
; ⟪pair⟫ = pair
; ⟪fst⟫ = fst
; ⟪snd⟫ = snd
; ⟪unit⟫ = unit
; ⟪boom⟫ = boom
; ⟪left⟫ = left
; ⟪right⟫ = right
; ⟪case⟫ = case
; mono⊫ = λ { (η , θ) → mono⊢ η θ }
; _⊫ⁿᶠ_ = λ { (Γ , Δ) → Γ ⁏ Δ ⊢ⁿᶠ_ }
; _⊫⍟_ = λ { (Γ , Δ) → Γ ⁏ Δ ⊢⋆_ }
; top⊫⍟ = refl
; pop⊫⍟ = refl
; ᵐgraft⊫⍟ = ᵐgraft⊢⋆
}
-- Soundness and completeness with respect to the canonical model.
mutual
reflectᶜ : ∀ {A Γ Δ} → Γ ⁏ Δ ⊢ⁿᵉ A → Γ ⨾ Δ ⊩ A
reflectᶜ {A ⇒ B} t = return {A ⇒ B}
λ { (η , θ) a → reflectᶜ (appⁿᵉ (mono⊢ⁿᵉ η θ t) (reifyᶜ a)) }
reflectᶜ {□ A} t = λ { (η , θ) κ → neⁿᶠ (unboxⁿᵉ (mono⊢ⁿᵉ η θ t)
(κ (refl⊆ , weak⊆)
λ θ′ → ᵐvar (mono∈ θ′ top) ,
reflectᶜ (ᵐvarⁿᵉ (mono∈ θ′ top)))) }
reflectᶜ {A ⩕ B} t = return {A ⩕ B} (reflectᶜ (fstⁿᵉ t) , reflectᶜ (sndⁿᵉ t))
reflectᶜ {⫪} t = return {⫪} ∙
reflectᶜ {⫫} t = λ { (η , θ) κ → neⁿᶠ (boomⁿᵉ (mono⊢ⁿᵉ η θ t)) }
reflectᶜ {A ⩖ B} t = λ { (η , θ) κ → neⁿᶠ (caseⁿᵉ (mono⊢ⁿᵉ η θ t)
(κ (weak⊆ , refl⊆) (ι₁ (reflectᶜ v₀ⁿᵉ)))
(κ (weak⊆ , refl⊆) (ι₂ (reflectᶜ v₀ⁿᵉ)))) }
reifyᶜ : ∀ {A Γ Δ} → Γ ⨾ Δ ⊩ A → Γ ⁏ Δ ⊢ⁿᶠ A
reifyᶜ {A ⇒ B} κ = κ (refl⊆ , refl⊆)
λ { (η , θ) f → lamⁿᶠ (reifyᶜ (f (weak⊆ , refl⊆) (reflectᶜ v₀ⁿᵉ))) }
reifyᶜ {□ A} κ = κ (refl⊆ , refl⊆)
λ { (η , θ) f → boxⁿᶠ (π₁ (f {∅} refl⊆)) }
reifyᶜ {A ⩕ B} κ = κ (refl⊆ , refl⊆)
λ { (η , θ) (a , b) → pairⁿᶠ (reifyᶜ a) (reifyᶜ b) }
reifyᶜ {⫪} κ = κ (refl⊆ , refl⊆)
λ { (η , θ) ∙ → unitⁿᶠ }
reifyᶜ {⫫} κ = κ (refl⊆ , refl⊆)
λ { (η , θ) () }
reifyᶜ {A ⩖ B} κ = κ (refl⊆ , refl⊆)
λ { (η , θ) (ι₁ a) → leftⁿᶠ (reifyᶜ a)
; (η , θ) (ι₂ b) → rightⁿᶠ (reifyᶜ b)
}
reflectᶜ⋆ : ∀ {Ξ Γ Δ} → Γ ⁏ Δ ⊢⋆ⁿᵉ Ξ → Γ ⨾ Δ ⊩⋆ Ξ
reflectᶜ⋆ {∅} ∙ = ∙
reflectᶜ⋆ {Ξ , A} (τ , t) = reflectᶜ⋆ τ , reflectᶜ t
-- TODO: Explain this.
refl⊫⋆ : ∀ {Γ Δ} → Γ ⨾ Δ ⊫⋆ Γ
refl⊫⋆ {∅} = ∙
refl⊫⋆ {Δ , A} = mono⊫⋆ (weak⊆ , refl⊆) refl⊫⋆ , v₀
ᵐrefl⊫⋆ : ∀ {Δ Γ} → Γ ⨾ Δ ⊫⋆ Δ
ᵐrefl⊫⋆ {∅} = ∙
ᵐrefl⊫⋆ {Δ , A} = mono⊫⋆ (refl⊆ , weak⊆) ᵐrefl⊫⋆ , ᵐv₀
refl⊩⋆ : ∀ {Γ Δ} → Γ ⨾ Δ ⊩⋆ Γ
refl⊩⋆ = reflectᶜ⋆ refl⊢⋆ⁿᵉ
ᵐrefl⊩⋆ : ∀ {Δ} → ∅ ⨾ Δ ⊩⋆ Δ
ᵐrefl⊩⋆ = reflectᶜ⋆ ᵐrefl⊢⋆ⁿᵉ
-- Completeness with respect to all models, or quotation.
quot : ∀ {A Γ Δ} → Γ ⁏ Δ ⊨ A → Γ ⁏ Δ ⊢ⁿᶠ A
quot s = reifyᶜ (s refl⊩⋆ ᵐrefl⊫⋆ ᵐrefl⊩⋆)
-- Normalisation by evaluation.
nbe : ∀ {A Γ Δ} → Γ ⁏ Δ ⊢ A → Γ ⁏ Δ ⊢ⁿᶠ A
nbe t = quot (eval t)
Raw
S4NbHS.agda
module S4NbHS where
open import S4SpinalNormalForm public
-- Hereditary substitution and reduction.
mutual
[_≔_]ˢⁿᶠ_ : ∀ {Γ Δ A C} → (i : A ∈ Γ) → Γ ∖ i ⁏ Δ ⊢ˢⁿᶠ A → Γ ⁏ Δ ⊢ˢⁿᶠ C → Γ ∖ i ⁏ Δ ⊢ˢⁿᶠ C
[ i ≔ s ]ˢⁿᶠ neˢⁿᶠ t = [ i ≔ s ]ˢⁿᵉ t
[ i ≔ s ]ˢⁿᶠ lamˢⁿᶠ t = lamˢⁿᶠ ([ pop i ≔ mono⊢ˢⁿᶠ weak⊆ refl⊆ s ]ˢⁿᶠ t)
[ i ≔ s ]ˢⁿᶠ boxˢⁿᶠ t = boxˢⁿᶠ t
[ i ≔ s ]ˢⁿᶠ pairˢⁿᶠ t u = pairˢⁿᶠ ([ i ≔ s ]ˢⁿᶠ t) ([ i ≔ s ]ˢⁿᶠ u)
[ i ≔ s ]ˢⁿᶠ unitˢⁿᶠ = unitˢⁿᶠ
[ i ≔ s ]ˢⁿᶠ leftˢⁿᶠ t = leftˢⁿᶠ ([ i ≔ s ]ˢⁿᶠ t)
[ i ≔ s ]ˢⁿᶠ rightˢⁿᶠ t = rightˢⁿᶠ ([ i ≔ s ]ˢⁿᶠ t)
[_≔_]ˢⁿᵉ_ : ∀ {Γ Δ A C} → (i : A ∈ Γ) → Γ ∖ i ⁏ Δ ⊢ˢⁿᶠ A → Γ ⁏ Δ ⊢ˢⁿᵉ C → {{_ : Propˢⁿᵉ C}} → Γ ∖ i ⁏ Δ ⊢ˢⁿᶠ C
[ i ≔ s ]ˢⁿᵉ spˢⁿᵉ j χ y with i ≟∈ j
[ i ≔ s ]ˢⁿᵉ spˢⁿᵉ .i χ y | same = reduce s ([ i ≔ s ]ˢᵖ χ) ([ i ≔ s ]ᵗᵖ y)
[ i ≔ s ]ˢⁿᵉ spˢⁿᵉ ._ χ y | diff j = neˢⁿᶠ (spˢⁿᵉ j ([ i ≔ s ]ˢᵖ χ) ([ i ≔ s ]ᵗᵖ y))
[ i ≔ s ]ˢⁿᵉ ᵐspˢⁿᵉ j χ y = neˢⁿᶠ (ᵐspˢⁿᵉ j ([ i ≔ s ]ˢᵖ χ) ([ i ≔ s ]ᵗᵖ y))
[_≔_]ˢᵖ_ : ∀ {Γ Δ A B C} → (i : A ∈ Γ) → Γ ∖ i ⁏ Δ ⊢ˢⁿᶠ A → Γ ⁏ Δ ⊢ˢᵖ B ⦙ C → Γ ∖ i ⁏ Δ ⊢ˢᵖ B ⦙ C
[ i ≔ s ]ˢᵖ nilˢᵖ = nilˢᵖ
[ i ≔ s ]ˢᵖ appˢᵖ χ u = appˢᵖ ([ i ≔ s ]ˢᵖ χ) ([ i ≔ s ]ˢⁿᶠ u)
[ i ≔ s ]ˢᵖ fstˢᵖ χ = fstˢᵖ ([ i ≔ s ]ˢᵖ χ)
[ i ≔ s ]ˢᵖ sndˢᵖ χ = sndˢᵖ ([ i ≔ s ]ˢᵖ χ)
[_≔_]ᵗᵖ_ : ∀ {Γ Δ A B C} → (i : A ∈ Γ) → Γ ∖ i ⁏ Δ ⊢ˢⁿᶠ A → Γ ⁏ Δ ⊢ᵗᵖ B ⦙ C → Γ ∖ i ⁏ Δ ⊢ᵗᵖ B ⦙ C
[ i ≔ s ]ᵗᵖ nilᵗᵖ = nilᵗᵖ
[ i ≔ s ]ᵗᵖ unboxᵗᵖ u = unboxᵗᵖ ([ i ≔ mono⊢ˢⁿᶠ refl⊆ weak⊆ s ]ˢⁿᶠ u)
[ i ≔ s ]ᵗᵖ boomᵗᵖ = boomᵗᵖ
[ i ≔ s ]ᵗᵖ caseᵗᵖ u v = caseᵗᵖ ([ pop i ≔ mono⊢ˢⁿᶠ weak⊆ refl⊆ s ]ˢⁿᶠ u)
([ pop i ≔ mono⊢ˢⁿᶠ weak⊆ refl⊆ s ]ˢⁿᶠ v)
-- TODO: Fix this.
{-# TERMINATING #-}
reduce : ∀ {Γ Δ A B C} → Γ ⁏ Δ ⊢ˢⁿᶠ A → Γ ⁏ Δ ⊢ˢᵖ A ⦙ B → Γ ⁏ Δ ⊢ᵗᵖ B ⦙ C → {{_ : Propˢⁿᵉ C}} → Γ ⁏ Δ ⊢ˢⁿᶠ C
reduce t nilˢᵖ nilᵗᵖ = t
reduce (neˢⁿᶠ t) nilˢᵖ y = neˢⁿᶠ (reduce′ t y)
reduce (neˢⁿᶠ t {{()}}) (appˢᵖ χ u) y
reduce (neˢⁿᶠ t {{()}}) (fstˢᵖ χ) y
reduce (neˢⁿᶠ t {{()}}) (sndˢᵖ χ) y
reduce (lamˢⁿᶠ t) (appˢᵖ χ u) y = reduce ([ top ≔ u ]ˢⁿᶠ t) χ y
reduce (boxˢⁿᶠ t) nilˢᵖ (unboxᵗᵖ u) = nbhs (ᵐ[ top ≔ t ] (snf→tm u))
reduce (pairˢⁿᶠ t u) (fstˢᵖ χ) y = reduce t χ y
reduce (pairˢⁿᶠ t u) (sndˢᵖ χ) y = reduce u χ y
reduce (leftˢⁿᶠ t) nilˢᵖ (caseᵗᵖ u v) = [ top ≔ t ]ˢⁿᶠ u
reduce (rightˢⁿᶠ t) nilˢᵖ (caseᵗᵖ u v) = [ top ≔ t ]ˢⁿᶠ v
reduce′ : ∀ {Γ Δ A C} → Γ ⁏ Δ ⊢ˢⁿᵉ A → Γ ⁏ Δ ⊢ᵗᵖ A ⦙ C → {{_ : Propˢⁿᵉ C}} → Γ ⁏ Δ ⊢ˢⁿᵉ C
reduce′ (spˢⁿᵉ i χ u) y = spˢⁿᵉ i χ (reduce″ u y)
reduce′ (ᵐspˢⁿᵉ i χ u) y = ᵐspˢⁿᵉ i χ (reduce″ u y)
reduce″ : ∀ {Γ Δ A B C} → Γ ⁏ Δ ⊢ᵗᵖ B ⦙ A → Γ ⁏ Δ ⊢ᵗᵖ A ⦙ C → {{_ : Propˢⁿᵉ C}} → Γ ⁏ Δ ⊢ᵗᵖ B ⦙ C
reduce″ nilᵗᵖ y = y
reduce″ (unboxᵗᵖ u) y = unboxᵗᵖ (reduce u nilˢᵖ (mono⊢ᵗᵖ refl⊆ weak⊆ y))
reduce″ boomᵗᵖ y = boomᵗᵖ
reduce″ (caseᵗᵖ u v) y = caseᵗᵖ (reduce u nilˢᵖ (mono⊢ᵗᵖ weak⊆ refl⊆ y))
(reduce v nilˢᵖ (mono⊢ᵗᵖ weak⊆ refl⊆ y))
-- Derived normal forms.
appˢⁿᶠ : ∀ {Γ Δ A B} → Γ ⁏ Δ ⊢ˢⁿᶠ A ⇒ B → Γ ⁏ Δ ⊢ˢⁿᶠ A → Γ ⁏ Δ ⊢ˢⁿᶠ B
appˢⁿᶠ (neˢⁿᶠ t {{()}})
appˢⁿᶠ (lamˢⁿᶠ t) u = [ top ≔ u ]ˢⁿᶠ t
fstˢⁿᶠ : ∀ {Γ Δ A B} → Γ ⁏ Δ ⊢ˢⁿᶠ A ⩕ B → Γ ⁏ Δ ⊢ˢⁿᶠ A
fstˢⁿᶠ (neˢⁿᶠ t {{()}})
fstˢⁿᶠ (pairˢⁿᶠ t u) = t
sndˢⁿᶠ : ∀ {Γ Δ A B} → Γ ⁏ Δ ⊢ˢⁿᶠ A ⩕ B → Γ ⁏ Δ ⊢ˢⁿᶠ B
sndˢⁿᶠ (neˢⁿᶠ t {{()}})
sndˢⁿᶠ (pairˢⁿᶠ t u) = u
-- Equipment for deriving neutral forms.
≪appˢᵖ : ∀ {Γ Δ A B C} → Γ ⁏ Δ ⊢ˢᵖ C ⦙ A ⇒ B → Γ ⁏ Δ ⊢ˢⁿᶠ A → Γ ⁏ Δ ⊢ˢᵖ C ⦙ B
≪appˢᵖ nilˢᵖ t = appˢᵖ nilˢᵖ t
≪appˢᵖ (appˢᵖ χ u) t = appˢᵖ (≪appˢᵖ χ t) u
≪appˢᵖ (fstˢᵖ χ) t = fstˢᵖ (≪appˢᵖ χ t)
≪appˢᵖ (sndˢᵖ χ) t = sndˢᵖ (≪appˢᵖ χ t)
≪fstˢᵖ : ∀ {Γ Δ A B C} → Γ ⁏ Δ ⊢ˢᵖ C ⦙ A ⩕ B → Γ ⁏ Δ ⊢ˢᵖ C ⦙ A
≪fstˢᵖ nilˢᵖ = fstˢᵖ nilˢᵖ
≪fstˢᵖ (appˢᵖ χ u) = appˢᵖ (≪fstˢᵖ χ) u
≪fstˢᵖ (fstˢᵖ χ) = fstˢᵖ (≪fstˢᵖ χ)
≪fstˢᵖ (sndˢᵖ χ) = sndˢᵖ (≪fstˢᵖ χ)
≪sndˢᵖ : ∀ {Γ Δ A B C} → Γ ⁏ Δ ⊢ˢᵖ C ⦙ A ⩕ B → Γ ⁏ Δ ⊢ˢᵖ C ⦙ B
≪sndˢᵖ nilˢᵖ = sndˢᵖ nilˢᵖ
≪sndˢᵖ (appˢᵖ χ u) = appˢᵖ (≪sndˢᵖ χ) u
≪sndˢᵖ (fstˢᵖ χ) = fstˢᵖ (≪sndˢᵖ χ)
≪sndˢᵖ (sndˢᵖ χ) = sndˢᵖ (≪sndˢᵖ χ)
-- Derived neutral forms.
varˢⁿᵉ : ∀ {Γ Δ A} → A ∈ Γ → Γ ⁏ Δ ⊢ˢⁿᵉ A
varˢⁿᵉ i = spˢⁿᵉ i nilˢᵖ nilᵗᵖ
ᵐvarˢⁿᵉ : ∀ {Γ Δ A} → A ∈ Δ → Γ ⁏ Δ ⊢ˢⁿᵉ A
ᵐvarˢⁿᵉ i = ᵐspˢⁿᵉ i nilˢᵖ nilᵗᵖ
appˢⁿᵉ : ∀ {Γ Δ A B} → Γ ⁏ Δ ⊢ˢⁿᵉ A ⇒ B → Γ ⁏ Δ ⊢ˢⁿᶠ A → Γ ⁏ Δ ⊢ˢⁿᵉ B
appˢⁿᵉ (spˢⁿᵉ i χ nilᵗᵖ) t = spˢⁿᵉ i (≪appˢᵖ χ t) nilᵗᵖ
appˢⁿᵉ (spˢⁿᵉ i χ (unboxᵗᵖ u)) t = spˢⁿᵉ i χ (unboxᵗᵖ (appˢⁿᶠ u (mono⊢ˢⁿᶠ refl⊆ weak⊆ t)))
appˢⁿᵉ (spˢⁿᵉ i χ boomᵗᵖ) t = spˢⁿᵉ i χ boomᵗᵖ
appˢⁿᵉ (spˢⁿᵉ i χ (caseᵗᵖ u v)) t = spˢⁿᵉ i χ (caseᵗᵖ (appˢⁿᶠ u (mono⊢ˢⁿᶠ weak⊆ refl⊆ t))
(appˢⁿᶠ v (mono⊢ˢⁿᶠ weak⊆ refl⊆ t)))
appˢⁿᵉ (ᵐspˢⁿᵉ i χ nilᵗᵖ) t = ᵐspˢⁿᵉ i (≪appˢᵖ χ t) nilᵗᵖ
appˢⁿᵉ (ᵐspˢⁿᵉ i χ (unboxᵗᵖ u)) t = ᵐspˢⁿᵉ i χ (unboxᵗᵖ (appˢⁿᶠ u (mono⊢ˢⁿᶠ refl⊆ weak⊆ t)))
appˢⁿᵉ (ᵐspˢⁿᵉ i χ boomᵗᵖ) t = ᵐspˢⁿᵉ i χ boomᵗᵖ
appˢⁿᵉ (ᵐspˢⁿᵉ i χ (caseᵗᵖ u v)) t = ᵐspˢⁿᵉ i χ (caseᵗᵖ (appˢⁿᶠ u (mono⊢ˢⁿᶠ weak⊆ refl⊆ t))
(appˢⁿᶠ v (mono⊢ˢⁿᶠ weak⊆ refl⊆ t)))
fstˢⁿᵉ : ∀ {Γ Δ A B} → Γ ⁏ Δ ⊢ˢⁿᵉ A ⩕ B → Γ ⁏ Δ ⊢ˢⁿᵉ A
fstˢⁿᵉ (spˢⁿᵉ i χ nilᵗᵖ) = spˢⁿᵉ i (≪fstˢᵖ χ) nilᵗᵖ
fstˢⁿᵉ (spˢⁿᵉ i χ (unboxᵗᵖ u)) = spˢⁿᵉ i χ (unboxᵗᵖ (fstˢⁿᶠ u))
fstˢⁿᵉ (spˢⁿᵉ i χ boomᵗᵖ) = spˢⁿᵉ i χ boomᵗᵖ
fstˢⁿᵉ (spˢⁿᵉ i χ (caseᵗᵖ u v)) = spˢⁿᵉ i χ (caseᵗᵖ (fstˢⁿᶠ u) (fstˢⁿᶠ v))
fstˢⁿᵉ (ᵐspˢⁿᵉ i χ nilᵗᵖ) = ᵐspˢⁿᵉ i (≪fstˢᵖ χ) nilᵗᵖ
fstˢⁿᵉ (ᵐspˢⁿᵉ i χ (unboxᵗᵖ u)) = ᵐspˢⁿᵉ i χ (unboxᵗᵖ (fstˢⁿᶠ u))
fstˢⁿᵉ (ᵐspˢⁿᵉ i χ boomᵗᵖ) = ᵐspˢⁿᵉ i χ boomᵗᵖ
fstˢⁿᵉ (ᵐspˢⁿᵉ i χ (caseᵗᵖ u v)) = ᵐspˢⁿᵉ i χ (caseᵗᵖ (fstˢⁿᶠ u) (fstˢⁿᶠ v))
sndˢⁿᵉ : ∀ {Γ Δ A B} → Γ ⁏ Δ ⊢ˢⁿᵉ A ⩕ B → Γ ⁏ Δ ⊢ˢⁿᵉ B
sndˢⁿᵉ (spˢⁿᵉ i χ nilᵗᵖ) = spˢⁿᵉ i (≪sndˢᵖ χ) nilᵗᵖ
sndˢⁿᵉ (spˢⁿᵉ i χ (unboxᵗᵖ u)) = spˢⁿᵉ i χ (unboxᵗᵖ (sndˢⁿᶠ u))
sndˢⁿᵉ (spˢⁿᵉ i χ boomᵗᵖ) = spˢⁿᵉ i χ boomᵗᵖ
sndˢⁿᵉ (spˢⁿᵉ i χ (caseᵗᵖ u v)) = spˢⁿᵉ i χ (caseᵗᵖ (sndˢⁿᶠ u) (sndˢⁿᶠ v))
sndˢⁿᵉ (ᵐspˢⁿᵉ i χ nilᵗᵖ) = ᵐspˢⁿᵉ i (≪sndˢᵖ χ) nilᵗᵖ
sndˢⁿᵉ (ᵐspˢⁿᵉ i χ (unboxᵗᵖ u)) = ᵐspˢⁿᵉ i χ (unboxᵗᵖ (sndˢⁿᶠ u))
sndˢⁿᵉ (ᵐspˢⁿᵉ i χ boomᵗᵖ) = ᵐspˢⁿᵉ i χ boomᵗᵖ
sndˢⁿᵉ (ᵐspˢⁿᵉ i χ (caseᵗᵖ u v)) = ᵐspˢⁿᵉ i χ (caseᵗᵖ (sndˢⁿᶠ u) (sndˢⁿᶠ v))
-- Iterated expansion.
expand : ∀ {A Γ Δ} → Γ ⁏ Δ ⊢ˢⁿᵉ A → Γ ⁏ Δ ⊢ˢⁿᶠ A
expand {A ⇒ B} t = lamˢⁿᶠ (expand (appˢⁿᵉ (mono⊢ˢⁿᵉ weak⊆ refl⊆ t) (expand (varˢⁿᵉ top))))
expand {□ A} t = neˢⁿᶠ t {{□ A}}
expand {A ⩕ B} t = pairˢⁿᶠ (expand (fstˢⁿᵉ t)) (expand (sndˢⁿᵉ t))
expand {⫪} t = unitˢⁿᶠ
expand {⫫} t = neˢⁿᶠ t {{⫫}}
expand {A ⩖ B} t = neˢⁿᶠ t {{A ⩖ B}}
-- More derived normal forms and neutral forms.
varˢⁿᶠ : ∀ {Γ Δ A} → A ∈ Γ → Γ ⁏ Δ ⊢ˢⁿᶠ A
varˢⁿᶠ i = expand (varˢⁿᵉ i)
ᵐvarˢⁿᶠ : ∀ {Γ Δ A} → A ∈ Δ → Γ ⁏ Δ ⊢ˢⁿᶠ A
ᵐvarˢⁿᶠ i = expand (ᵐvarˢⁿᵉ i)
unboxˢⁿᶠ : ∀ {Γ Δ A C} → Γ ⁏ Δ ⊢ˢⁿᶠ □ A → Γ ⁏ Δ , A ⊢ˢⁿᶠ C → Γ ⁏ Δ ⊢ˢⁿᶠ C
unboxˢⁿᶠ (neˢⁿᶠ t) u = expand (unboxˢⁿᵉ t u)
unboxˢⁿᶠ (boxˢⁿᶠ t) u = nbhs (ᵐ[ top ≔ t ] (snf→tm u))
unboxˢⁿᵉ : ∀ {Γ Δ A C} → Γ ⁏ Δ ⊢ˢⁿᵉ □ A → Γ ⁏ Δ , A ⊢ˢⁿᶠ C → Γ ⁏ Δ ⊢ˢⁿᵉ C
unboxˢⁿᵉ (spˢⁿᵉ i χ nilᵗᵖ) u = spˢⁿᵉ i χ (unboxᵗᵖ u)
unboxˢⁿᵉ (spˢⁿᵉ i χ (unboxᵗᵖ t)) u = spˢⁿᵉ i χ (unboxᵗᵖ (unboxˢⁿᶠ t (mono⊢ˢⁿᶠ refl⊆ (keep (weak⊆)) u)))
unboxˢⁿᵉ (spˢⁿᵉ i χ boomᵗᵖ) u = spˢⁿᵉ i χ boomᵗᵖ
unboxˢⁿᵉ (spˢⁿᵉ i χ (caseᵗᵖ tᵤ tᵥ)) u = spˢⁿᵉ i χ (caseᵗᵖ (unboxˢⁿᶠ tᵤ (mono⊢ˢⁿᶠ weak⊆ refl⊆ u))
(unboxˢⁿᶠ tᵥ (mono⊢ˢⁿᶠ weak⊆ refl⊆ u)))
unboxˢⁿᵉ (ᵐspˢⁿᵉ i χ nilᵗᵖ) u = ᵐspˢⁿᵉ i χ (unboxᵗᵖ u)
unboxˢⁿᵉ (ᵐspˢⁿᵉ i χ (unboxᵗᵖ t)) u = ᵐspˢⁿᵉ i χ (unboxᵗᵖ (unboxˢⁿᶠ t (mono⊢ˢⁿᶠ refl⊆ (keep (weak⊆)) u)))
unboxˢⁿᵉ (ᵐspˢⁿᵉ i χ boomᵗᵖ) u = ᵐspˢⁿᵉ i χ boomᵗᵖ
unboxˢⁿᵉ (ᵐspˢⁿᵉ i χ (caseᵗᵖ tᵤ tᵥ)) u = ᵐspˢⁿᵉ i χ (caseᵗᵖ (unboxˢⁿᶠ tᵤ (mono⊢ˢⁿᶠ weak⊆ refl⊆ u))
(unboxˢⁿᶠ tᵥ (mono⊢ˢⁿᶠ weak⊆ refl⊆ u)))
boomˢⁿᶠ : ∀ {Γ Δ C} → Γ ⁏ Δ ⊢ˢⁿᶠ ⫫ → Γ ⁏ Δ ⊢ˢⁿᶠ C
boomˢⁿᶠ (neˢⁿᶠ t) = expand (boomˢⁿᵉ t)
boomˢⁿᵉ : ∀ {Γ Δ C} → Γ ⁏ Δ ⊢ˢⁿᵉ ⫫ → Γ ⁏ Δ ⊢ˢⁿᵉ C
boomˢⁿᵉ (spˢⁿᵉ i χ nilᵗᵖ) = spˢⁿᵉ i χ boomᵗᵖ
boomˢⁿᵉ (spˢⁿᵉ i χ (unboxᵗᵖ u)) = spˢⁿᵉ i χ (unboxᵗᵖ (boomˢⁿᶠ u))
boomˢⁿᵉ (spˢⁿᵉ i χ boomᵗᵖ) = spˢⁿᵉ i χ boomᵗᵖ
boomˢⁿᵉ (spˢⁿᵉ i χ (caseᵗᵖ u v)) = spˢⁿᵉ i χ (caseᵗᵖ (boomˢⁿᶠ u) (boomˢⁿᶠ v))
boomˢⁿᵉ (ᵐspˢⁿᵉ i χ nilᵗᵖ) = ᵐspˢⁿᵉ i χ boomᵗᵖ
boomˢⁿᵉ (ᵐspˢⁿᵉ i χ (unboxᵗᵖ u)) = ᵐspˢⁿᵉ i χ (unboxᵗᵖ (boomˢⁿᶠ u))
boomˢⁿᵉ (ᵐspˢⁿᵉ i χ boomᵗᵖ) = ᵐspˢⁿᵉ i χ boomᵗᵖ
boomˢⁿᵉ (ᵐspˢⁿᵉ i χ (caseᵗᵖ u v)) = ᵐspˢⁿᵉ i χ (caseᵗᵖ (boomˢⁿᶠ u) (boomˢⁿᶠ v))
caseˢⁿᶠ : ∀ {Γ Δ A B C} → Γ ⁏ Δ ⊢ˢⁿᶠ A ⩖ B → Γ , A ⁏ Δ ⊢ˢⁿᶠ C → Γ , B ⁏ Δ ⊢ˢⁿᶠ C → Γ ⁏ Δ ⊢ˢⁿᶠ C
caseˢⁿᶠ (neˢⁿᶠ t) u v = expand (caseˢⁿᵉ t u v)
caseˢⁿᶠ (leftˢⁿᶠ t) u v = [ top ≔ t ]ˢⁿᶠ u
caseˢⁿᶠ (rightˢⁿᶠ t) u v = [ top ≔ t ]ˢⁿᶠ v
caseˢⁿᵉ : ∀ {Γ Δ A B C} → Γ ⁏ Δ ⊢ˢⁿᵉ A ⩖ B → Γ , A ⁏ Δ ⊢ˢⁿᶠ C → Γ , B ⁏ Δ ⊢ˢⁿᶠ C → Γ ⁏ Δ ⊢ˢⁿᵉ C
caseˢⁿᵉ (spˢⁿᵉ i χ nilᵗᵖ) u v = spˢⁿᵉ i χ (caseᵗᵖ u v)
caseˢⁿᵉ (spˢⁿᵉ i χ (unboxᵗᵖ t)) u v = spˢⁿᵉ i χ (unboxᵗᵖ (caseˢⁿᶠ t (mono⊢ˢⁿᶠ refl⊆ weak⊆ u)
(mono⊢ˢⁿᶠ refl⊆ weak⊆ v)))
caseˢⁿᵉ (spˢⁿᵉ i χ boomᵗᵖ) u v = spˢⁿᵉ i χ boomᵗᵖ
caseˢⁿᵉ (spˢⁿᵉ i χ (caseᵗᵖ tᵤ tᵥ)) u v = spˢⁿᵉ i χ (caseᵗᵖ (caseˢⁿᶠ tᵤ (mono⊢ˢⁿᶠ (keep weak⊆) refl⊆ u)
(mono⊢ˢⁿᶠ (keep weak⊆) refl⊆ v))
(caseˢⁿᶠ tᵥ (mono⊢ˢⁿᶠ (keep weak⊆) refl⊆ u)
(mono⊢ˢⁿᶠ (keep weak⊆) refl⊆ v)))
caseˢⁿᵉ (ᵐspˢⁿᵉ i χ nilᵗᵖ) u v = ᵐspˢⁿᵉ i χ (caseᵗᵖ u v)
caseˢⁿᵉ (ᵐspˢⁿᵉ i χ (unboxᵗᵖ t)) u v = ᵐspˢⁿᵉ i χ (unboxᵗᵖ (caseˢⁿᶠ t (mono⊢ˢⁿᶠ refl⊆ weak⊆ u)
(mono⊢ˢⁿᶠ refl⊆ weak⊆ v)))
caseˢⁿᵉ (ᵐspˢⁿᵉ i χ boomᵗᵖ) u v = ᵐspˢⁿᵉ i χ boomᵗᵖ
caseˢⁿᵉ (ᵐspˢⁿᵉ i χ (caseᵗᵖ tᵤ tᵥ)) u v = ᵐspˢⁿᵉ i χ (caseᵗᵖ (caseˢⁿᶠ tᵤ (mono⊢ˢⁿᶠ (keep weak⊆) refl⊆ u)
(mono⊢ˢⁿᶠ (keep weak⊆) refl⊆ v))
(caseˢⁿᶠ tᵥ (mono⊢ˢⁿᶠ (keep weak⊆) refl⊆ u)
(mono⊢ˢⁿᶠ (keep weak⊆) refl⊆ v)))
-- Normalisation by hereditary substitution.
nbhs : ∀ {A Γ Δ} → Γ ⁏ Δ ⊢ A → Γ ⁏ Δ ⊢ˢⁿᶠ A
nbhs (var i) = varˢⁿᶠ i
nbhs (ᵐvar i) = ᵐvarˢⁿᶠ i
nbhs (lam t) = lamˢⁿᶠ (nbhs t)
nbhs (app t u) = appˢⁿᶠ (nbhs t) (nbhs u)
nbhs (box t) = boxˢⁿᶠ t
nbhs (unbox t u) = unboxˢⁿᶠ (nbhs t) (nbhs u)
nbhs (pair t u) = pairˢⁿᶠ (nbhs t) (nbhs u)
nbhs (fst t) = fstˢⁿᶠ (nbhs t)
nbhs (snd t) = sndˢⁿᶠ (nbhs t)
nbhs unit = unitˢⁿᶠ
nbhs (boom t) = boomˢⁿᶠ (nbhs t)
nbhs (left t) = leftˢⁿᶠ (nbhs t)
nbhs (right t) = rightˢⁿᶠ (nbhs t)
nbhs (case t u v) = caseˢⁿᶠ (nbhs t) (nbhs u) (nbhs v)
nbhs′ : ∀ {A Γ Δ} → Γ ⁏ Δ ⊢ A → Γ ⁏ Δ ⊢ⁿᶠ A
nbhs′ t = snf→nf (nbhs t)
Raw
S4NbHSCorrectness.agda
module S4NbHSCorrectness where
open import S4Convertibility public
open import S4NbHS public
open ≣-Reasoning
-- TODO: Show this.
postulate
sound : ∀ {Γ Δ A} {t t′ : Γ ⁏ Δ ⊢ A} → t ≣ t′ → nbhs t ≡ nbhs t′
mutual
completeˢⁿᵉ : ∀ {A Γ Δ} → (t : Γ ⁏ Δ ⊢ˢⁿᵉ A) → snf→tm (expand t) ≣ sne→tm t
completeˢⁿᵉ {A ⇒ B} (spˢⁿᵉ i χ y) = {!!}
completeˢⁿᵉ {A ⇒ B} (ᵐspˢⁿᵉ i χ y) = {!!}
completeˢⁿᵉ {□ A} (spˢⁿᵉ i χ y) = {!!}
completeˢⁿᵉ {□ A} (ᵐspˢⁿᵉ i χ y) = {!!}
completeˢⁿᵉ {A ⩕ B} (spˢⁿᵉ i χ y) = {!!}
completeˢⁿᵉ {A ⩕ B} (ᵐspˢⁿᵉ i χ y) = {!!}
completeˢⁿᵉ {⫪} (spˢⁿᵉ i χ y) = {!!}
completeˢⁿᵉ {⫪} (ᵐspˢⁿᵉ i χ y) = {!!}
completeˢⁿᵉ {⫫} (spˢⁿᵉ i χ y) = {!!}
completeˢⁿᵉ {⫫} (ᵐspˢⁿᵉ i χ y) = {!!}
completeˢⁿᵉ {A ⩖ B} (spˢⁿᵉ i χ y) = {!!}
completeˢⁿᵉ {A ⩖ B} (ᵐspˢⁿᵉ i χ y) = {!!}
complete-var : ∀ {Γ Δ A} → (i : A ∈ Γ) → snf→tm (varˢⁿᶠ i) ≣ var {Δ = Δ} i
complete-var i = {!completeˢⁿᵉ (spˢⁿᵉ i nilˢᵖ nilᵗᵖ)!}
-- TODO: Show this.
complete : ∀ {Γ Δ A} → (t : Γ ⁏ Δ ⊢ A) → snf→tm (nbhs t) ≣ t
complete (var i) = complete-var i
complete (ᵐvar i) = {!!}
complete (lam t) = cong≣lam (complete t)
complete (app t u) = trans≣ {!!} (cong≣app (complete t) (complete u))
complete (box t) = refl≣
complete (unbox t u) = trans≣ {!!} (cong≣unbox (complete t) (complete u))
complete (pair t u) = cong≣pair (complete t) (complete u)
complete (fst t) = trans≣ {!!} (cong≣fst (complete t))
complete (snd t) = trans≣ {!!} (cong≣snd (complete t))
complete unit = refl≣
complete (boom t) = trans≣ {!!} (cong≣boom (complete t))
complete (left t) = cong≣left (complete t)
complete (right t) = cong≣right (complete t)
complete (case t u v) = trans≣ {!!} (cong≣case (complete t) (complete u) (complete v))
complete′ : ∀ {Γ Δ A} → (t t′ : Γ ⁏ Δ ⊢ A) → nbhs t ≡ nbhs t′ → t ≣ t′
complete′ t t′ p =
t ≣⟨ sym≣ (complete t) ⟩
snf→tm (nbhs t) ≣⟨ lift≣ (cong snf→tm p) ⟩
snf→tm (nbhs t′) ≣⟨ complete t′ ⟩
t′ ∎
correct : ∀ {Γ Δ A} {t t′ : Γ ⁏ Δ ⊢ A} → t ≣ t′ ↔ nbhs t ≡ nbhs t′
correct {t = t} {t′} = sound , complete′ _ _
-- TODO: Show this.
postulate
stable : ∀ {Γ Δ A} {t : Γ ⁏ Δ ⊢ˢⁿᶠ A} → nbhs (snf→tm t) ≡ t
Raw
S4NbHSWrong.agda
module S4NbHSWrong where
open import S4SpinalNormalFormWrong public
-- Hereditary substitution and reduction.
mutual
[_≔_]ˢⁿᶠ_ : ∀ {Γ Δ A C} → (i : A ∈ Γ) → Γ ∖ i ⁏ Δ ⊢ˢⁿᶠ A → Γ ⁏ Δ ⊢ˢⁿᶠ C → Γ ∖ i ⁏ Δ ⊢ˢⁿᶠ C
[ i ≔ s ]ˢⁿᶠ neˢⁿᶠ t = [ i ≔ s ]ˢⁿᵉ t
[ i ≔ s ]ˢⁿᶠ lamˢⁿᶠ t = lamˢⁿᶠ ([ pop i ≔ mono⊢ˢⁿᶠ weak⊆ refl⊆ s ]ˢⁿᶠ t)
[ i ≔ s ]ˢⁿᶠ boxˢⁿᶠ `t t = boxˢⁿᶠ `t t
[ i ≔ s ]ˢⁿᶠ pairˢⁿᶠ t u = pairˢⁿᶠ ([ i ≔ s ]ˢⁿᶠ t) ([ i ≔ s ]ˢⁿᶠ u)
[ i ≔ s ]ˢⁿᶠ unitˢⁿᶠ = unitˢⁿᶠ
[ i ≔ s ]ˢⁿᶠ leftˢⁿᶠ t = leftˢⁿᶠ ([ i ≔ s ]ˢⁿᶠ t)
[ i ≔ s ]ˢⁿᶠ rightˢⁿᶠ t = rightˢⁿᶠ ([ i ≔ s ]ˢⁿᶠ t)
[_≔_]ˢⁿᵉ_ : ∀ {Γ Δ A C} → (i : A ∈ Γ) → Γ ∖ i ⁏ Δ ⊢ˢⁿᶠ A → Γ ⁏ Δ ⊢ˢⁿᵉ C → {{_ : Propˢⁿᵉ C}} → Γ ∖ i ⁏ Δ ⊢ˢⁿᶠ C
[ i ≔ s ]ˢⁿᵉ spˢⁿᵉ j χ y with i ≟∈ j
[ i ≔ s ]ˢⁿᵉ spˢⁿᵉ .i χ y | same = reduce s ([ i ≔ s ]ˢᵖ χ) ([ i ≔ s ]ᵗᵖ y)
[ i ≔ s ]ˢⁿᵉ spˢⁿᵉ ._ χ y | diff j = neˢⁿᶠ (spˢⁿᵉ j ([ i ≔ s ]ˢᵖ χ) ([ i ≔ s ]ᵗᵖ y))
[ i ≔ s ]ˢⁿᵉ ᵐspˢⁿᵉ j χ y = neˢⁿᶠ (ᵐspˢⁿᵉ j ([ i ≔ s ]ˢᵖ χ) ([ i ≔ s ]ᵗᵖ y))
[_≔_]ˢᵖ_ : ∀ {Γ Δ A B C} → (i : A ∈ Γ) → Γ ∖ i ⁏ Δ ⊢ˢⁿᶠ A → Γ ⁏ Δ ⊢ˢᵖ B ⦙ C → Γ ∖ i ⁏ Δ ⊢ˢᵖ B ⦙ C
[ i ≔ s ]ˢᵖ nilˢᵖ = nilˢᵖ
[ i ≔ s ]ˢᵖ appˢᵖ χ u = appˢᵖ ([ i ≔ s ]ˢᵖ χ) ([ i ≔ s ]ˢⁿᶠ u)
[ i ≔ s ]ˢᵖ fstˢᵖ χ = fstˢᵖ ([ i ≔ s ]ˢᵖ χ)
[ i ≔ s ]ˢᵖ sndˢᵖ χ = sndˢᵖ ([ i ≔ s ]ˢᵖ χ)
[_≔_]ᵗᵖ_ : ∀ {Γ Δ A B C} → (i : A ∈ Γ) → Γ ∖ i ⁏ Δ ⊢ˢⁿᶠ A → Γ ⁏ Δ ⊢ᵗᵖ B ⦙ C → Γ ∖ i ⁏ Δ ⊢ᵗᵖ B ⦙ C
[ i ≔ s ]ᵗᵖ nilᵗᵖ = nilᵗᵖ
[ i ≔ s ]ᵗᵖ unboxᵗᵖ u = unboxᵗᵖ ([ i ≔ mono⊢ˢⁿᶠ refl⊆ weak⊆ s ]ˢⁿᶠ u)
[ i ≔ s ]ᵗᵖ boomᵗᵖ = boomᵗᵖ
[ i ≔ s ]ᵗᵖ caseᵗᵖ u v = caseᵗᵖ ([ pop i ≔ mono⊢ˢⁿᶠ weak⊆ refl⊆ s ]ˢⁿᶠ u)
([ pop i ≔ mono⊢ˢⁿᶠ weak⊆ refl⊆ s ]ˢⁿᶠ v)
ᵐ[_≔_]ˢⁿᶠ_ : ∀ {Γ Δ A C} → (i : A ∈ Δ) → ∅ ⁏ Δ ∖ i ⊢ˢⁿᶠ A → Γ ⁏ Δ ⊢ˢⁿᶠ C → Γ ⁏ Δ ∖ i ⊢ˢⁿᶠ C
ᵐ[ i ≔ s ]ˢⁿᶠ neˢⁿᶠ t = ᵐ[ i ≔ s ]ˢⁿᵉ t
ᵐ[ i ≔ s ]ˢⁿᶠ lamˢⁿᶠ t = lamˢⁿᶠ (ᵐ[ i ≔ s ]ˢⁿᶠ t)
ᵐ[ i ≔ s ]ˢⁿᶠ boxˢⁿᶠ `t t = boxˢⁿᶠ (ᵐ[ i ≔ snf→tm s ] `t) (ᵐ[ i ≔ s ]ˢⁿᶠ t)
ᵐ[ i ≔ s ]ˢⁿᶠ pairˢⁿᶠ t u = pairˢⁿᶠ (ᵐ[ i ≔ s ]ˢⁿᶠ t) (ᵐ[ i ≔ s ]ˢⁿᶠ u)
ᵐ[ i ≔ s ]ˢⁿᶠ unitˢⁿᶠ = unitˢⁿᶠ
ᵐ[ i ≔ s ]ˢⁿᶠ leftˢⁿᶠ t = leftˢⁿᶠ (ᵐ[ i ≔ s ]ˢⁿᶠ t)
ᵐ[ i ≔ s ]ˢⁿᶠ rightˢⁿᶠ t = rightˢⁿᶠ (ᵐ[ i ≔ s ]ˢⁿᶠ t)
ᵐ[_≔_]ˢⁿᵉ_ : ∀ {Γ Δ A C} → (i : A ∈ Δ) → ∅ ⁏ Δ ∖ i ⊢ˢⁿᶠ A → Γ ⁏ Δ ⊢ˢⁿᵉ C → {{_ : Propˢⁿᵉ C}} → Γ ⁏ Δ ∖ i ⊢ˢⁿᶠ C
ᵐ[ i ≔ s ]ˢⁿᵉ spˢⁿᵉ j χ y = neˢⁿᶠ (spˢⁿᵉ j (ᵐ[ i ≔ s ]ˢᵖ χ) (ᵐ[ i ≔ s ]ᵗᵖ y))
ᵐ[ i ≔ s ]ˢⁿᵉ ᵐspˢⁿᵉ j χ y with i ≟∈ j
ᵐ[ i ≔ s ]ˢⁿᵉ ᵐspˢⁿᵉ .i χ y | same = reduce (mono⊢ˢⁿᶠ zero⊆ refl⊆ s) (ᵐ[ i ≔ s ]ˢᵖ χ) (ᵐ[ i ≔ s ]ᵗᵖ y)
ᵐ[ i ≔ s ]ˢⁿᵉ ᵐspˢⁿᵉ ._ χ y | diff j = neˢⁿᶠ (ᵐspˢⁿᵉ j (ᵐ[ i ≔ s ]ˢᵖ χ) (ᵐ[ i ≔ s ]ᵗᵖ y))
ᵐ[_≔_]ˢᵖ_ : ∀ {Γ Δ A B C} → (i : A ∈ Δ) → ∅ ⁏ Δ ∖ i ⊢ˢⁿᶠ A → Γ ⁏ Δ ⊢ˢᵖ B ⦙ C → Γ ⁏ Δ ∖ i ⊢ˢᵖ B ⦙ C
ᵐ[ i ≔ s ]ˢᵖ nilˢᵖ = nilˢᵖ
ᵐ[ i ≔ s ]ˢᵖ appˢᵖ χ u = appˢᵖ (ᵐ[ i ≔ s ]ˢᵖ χ) (ᵐ[ i ≔ s ]ˢⁿᶠ u)
ᵐ[ i ≔ s ]ˢᵖ fstˢᵖ χ = fstˢᵖ (ᵐ[ i ≔ s ]ˢᵖ χ)
ᵐ[ i ≔ s ]ˢᵖ sndˢᵖ χ = sndˢᵖ (ᵐ[ i ≔ s ]ˢᵖ χ)
ᵐ[_≔_]ᵗᵖ_ : ∀ {Γ Δ A B C} → (i : A ∈ Δ) → ∅ ⁏ Δ ∖ i ⊢ˢⁿᶠ A → Γ ⁏ Δ ⊢ᵗᵖ B ⦙ C → Γ ⁏ Δ ∖ i ⊢ᵗᵖ B ⦙ C
ᵐ[ i ≔ s ]ᵗᵖ nilᵗᵖ = nilᵗᵖ
ᵐ[ i ≔ s ]ᵗᵖ unboxᵗᵖ u = unboxᵗᵖ (ᵐ[ pop i ≔ mono⊢ˢⁿᶠ refl⊆ weak⊆ s ]ˢⁿᶠ u)
ᵐ[ i ≔ s ]ᵗᵖ boomᵗᵖ = boomᵗᵖ
ᵐ[ i ≔ s ]ᵗᵖ caseᵗᵖ u v = caseᵗᵖ (ᵐ[ i ≔ s ]ˢⁿᶠ u) (ᵐ[ i ≔ s ]ˢⁿᶠ v)
reduce : ∀ {Γ Δ A B C} → Γ ⁏ Δ ⊢ˢⁿᶠ A → Γ ⁏ Δ ⊢ˢᵖ A ⦙ B → Γ ⁏ Δ ⊢ᵗᵖ B ⦙ C → {{_ : Propˢⁿᵉ C}} → Γ ⁏ Δ ⊢ˢⁿᶠ C
reduce t nilˢᵖ nilᵗᵖ = t
reduce (neˢⁿᶠ t) nilˢᵖ y = neˢⁿᶠ (reduce′ t y)
reduce (neˢⁿᶠ t {{()}}) (appˢᵖ χ u) y
reduce (neˢⁿᶠ t {{()}}) (fstˢᵖ χ) y
reduce (neˢⁿᶠ t {{()}}) (sndˢᵖ χ) y
reduce (lamˢⁿᶠ t) (appˢᵖ χ u) y = reduce ([ top ≔ u ]ˢⁿᶠ t) χ y
reduce (boxˢⁿᶠ `t t) nilˢᵖ (unboxᵗᵖ u) = ᵐ[ top ≔ t ]ˢⁿᶠ u
reduce (pairˢⁿᶠ t u) (fstˢᵖ χ) y = reduce t χ y
reduce (pairˢⁿᶠ t u) (sndˢᵖ χ) y = reduce u χ y
reduce (leftˢⁿᶠ t) nilˢᵖ (caseᵗᵖ u v) = [ top ≔ t ]ˢⁿᶠ u
reduce (rightˢⁿᶠ t) nilˢᵖ (caseᵗᵖ u v) = [ top ≔ t ]ˢⁿᶠ v
reduce′ : ∀ {Γ Δ A C} → Γ ⁏ Δ ⊢ˢⁿᵉ A → Γ ⁏ Δ ⊢ᵗᵖ A ⦙ C → {{_ : Propˢⁿᵉ C}} → Γ ⁏ Δ ⊢ˢⁿᵉ C
reduce′ (spˢⁿᵉ i χ u) y = spˢⁿᵉ i χ (reduce″ u y)
reduce′ (ᵐspˢⁿᵉ i χ u) y = ᵐspˢⁿᵉ i χ (reduce″ u y)
reduce″ : ∀ {Γ Δ A B C} → Γ ⁏ Δ ⊢ᵗᵖ B ⦙ A → Γ ⁏ Δ ⊢ᵗᵖ A ⦙ C → {{_ : Propˢⁿᵉ C}} → Γ ⁏ Δ ⊢ᵗᵖ B ⦙ C
reduce″ nilᵗᵖ y = y
reduce″ (unboxᵗᵖ u) y = unboxᵗᵖ (reduce u nilˢᵖ (mono⊢ᵗᵖ refl⊆ weak⊆ y))
reduce″ boomᵗᵖ y = boomᵗᵖ
reduce″ (caseᵗᵖ u v) y = caseᵗᵖ (reduce u nilˢᵖ (mono⊢ᵗᵖ weak⊆ refl⊆ y))
(reduce v nilˢᵖ (mono⊢ᵗᵖ weak⊆ refl⊆ y))
-- Derived normal forms.
appˢⁿᶠ : ∀ {Γ Δ A B} → Γ ⁏ Δ ⊢ˢⁿᶠ A ⇒ B → Γ ⁏ Δ ⊢ˢⁿᶠ A → Γ ⁏ Δ ⊢ˢⁿᶠ B
appˢⁿᶠ (neˢⁿᶠ t {{()}})
appˢⁿᶠ (lamˢⁿᶠ t) u = [ top ≔ u ]ˢⁿᶠ t
fstˢⁿᶠ : ∀ {Γ Δ A B} → Γ ⁏ Δ ⊢ˢⁿᶠ A ⩕ B → Γ ⁏ Δ ⊢ˢⁿᶠ A
fstˢⁿᶠ (neˢⁿᶠ t {{()}})
fstˢⁿᶠ (pairˢⁿᶠ t u) = t
sndˢⁿᶠ : ∀ {Γ Δ A B} → Γ ⁏ Δ ⊢ˢⁿᶠ A ⩕ B → Γ ⁏ Δ ⊢ˢⁿᶠ B
sndˢⁿᶠ (neˢⁿᶠ t {{()}})
sndˢⁿᶠ (pairˢⁿᶠ t u) = u
-- Equipment for deriving neutral forms.
≪appˢᵖ : ∀ {Γ Δ A B C} → Γ ⁏ Δ ⊢ˢᵖ C ⦙ A ⇒ B → Γ ⁏ Δ ⊢ˢⁿᶠ A → Γ ⁏ Δ ⊢ˢᵖ C ⦙ B
≪appˢᵖ nilˢᵖ t = appˢᵖ nilˢᵖ t
≪appˢᵖ (appˢᵖ χ u) t = appˢᵖ (≪appˢᵖ χ t) u
≪appˢᵖ (fstˢᵖ χ) t = fstˢᵖ (≪appˢᵖ χ t)
≪appˢᵖ (sndˢᵖ χ) t = sndˢᵖ (≪appˢᵖ χ t)
≪fstˢᵖ : ∀ {Γ Δ A B C} → Γ ⁏ Δ ⊢ˢᵖ C ⦙ A ⩕ B → Γ ⁏ Δ ⊢ˢᵖ C ⦙ A
≪fstˢᵖ nilˢᵖ = fstˢᵖ nilˢᵖ
≪fstˢᵖ (appˢᵖ χ u) = appˢᵖ (≪fstˢᵖ χ) u
≪fstˢᵖ (fstˢᵖ χ) = fstˢᵖ (≪fstˢᵖ χ)
≪fstˢᵖ (sndˢᵖ χ) = sndˢᵖ (≪fstˢᵖ χ)
≪sndˢᵖ : ∀ {Γ Δ A B C} → Γ ⁏ Δ ⊢ˢᵖ C ⦙ A ⩕ B → Γ ⁏ Δ ⊢ˢᵖ C ⦙ B
≪sndˢᵖ nilˢᵖ = sndˢᵖ nilˢᵖ
≪sndˢᵖ (appˢᵖ χ u) = appˢᵖ (≪sndˢᵖ χ) u
≪sndˢᵖ (fstˢᵖ χ) = fstˢᵖ (≪sndˢᵖ χ)
≪sndˢᵖ (sndˢᵖ χ) = sndˢᵖ (≪sndˢᵖ χ)
-- Derived neutral forms.
varˢⁿᵉ : ∀ {Γ Δ A} → A ∈ Γ → Γ ⁏ Δ ⊢ˢⁿᵉ A
varˢⁿᵉ i = spˢⁿᵉ i nilˢᵖ nilᵗᵖ
ᵐvarˢⁿᵉ : ∀ {Γ Δ A} → A ∈ Δ → Γ ⁏ Δ ⊢ˢⁿᵉ A
ᵐvarˢⁿᵉ i = ᵐspˢⁿᵉ i nilˢᵖ nilᵗᵖ
appˢⁿᵉ : ∀ {Γ Δ A B} → Γ ⁏ Δ ⊢ˢⁿᵉ A ⇒ B → Γ ⁏ Δ ⊢ˢⁿᶠ A → Γ ⁏ Δ ⊢ˢⁿᵉ B
appˢⁿᵉ (spˢⁿᵉ i χ nilᵗᵖ) t = spˢⁿᵉ i (≪appˢᵖ χ t) nilᵗᵖ
appˢⁿᵉ (spˢⁿᵉ i χ (unboxᵗᵖ u)) t = spˢⁿᵉ i χ (unboxᵗᵖ (appˢⁿᶠ u (mono⊢ˢⁿᶠ refl⊆ weak⊆ t)))
appˢⁿᵉ (spˢⁿᵉ i χ boomᵗᵖ) t = spˢⁿᵉ i χ boomᵗᵖ
appˢⁿᵉ (spˢⁿᵉ i χ (caseᵗᵖ u v)) t = spˢⁿᵉ i χ (caseᵗᵖ (appˢⁿᶠ u (mono⊢ˢⁿᶠ weak⊆ refl⊆ t))
(appˢⁿᶠ v (mono⊢ˢⁿᶠ weak⊆ refl⊆ t)))
appˢⁿᵉ (ᵐspˢⁿᵉ i χ nilᵗᵖ) t = ᵐspˢⁿᵉ i (≪appˢᵖ χ t) nilᵗᵖ
appˢⁿᵉ (ᵐspˢⁿᵉ i χ (unboxᵗᵖ u)) t = ᵐspˢⁿᵉ i χ (unboxᵗᵖ (appˢⁿᶠ u (mono⊢ˢⁿᶠ refl⊆ weak⊆ t)))
appˢⁿᵉ (ᵐspˢⁿᵉ i χ boomᵗᵖ) t = ᵐspˢⁿᵉ i χ boomᵗᵖ
appˢⁿᵉ (ᵐspˢⁿᵉ i χ (caseᵗᵖ u v)) t = ᵐspˢⁿᵉ i χ (caseᵗᵖ (appˢⁿᶠ u (mono⊢ˢⁿᶠ weak⊆ refl⊆ t))
(appˢⁿᶠ v (mono⊢ˢⁿᶠ weak⊆ refl⊆ t)))
fstˢⁿᵉ : ∀ {Γ Δ A B} → Γ ⁏ Δ ⊢ˢⁿᵉ A ⩕ B → Γ ⁏ Δ ⊢ˢⁿᵉ A
fstˢⁿᵉ (spˢⁿᵉ i χ nilᵗᵖ) = spˢⁿᵉ i (≪fstˢᵖ χ) nilᵗᵖ
fstˢⁿᵉ (spˢⁿᵉ i χ (unboxᵗᵖ u)) = spˢⁿᵉ i χ (unboxᵗᵖ (fstˢⁿᶠ u))
fstˢⁿᵉ (spˢⁿᵉ i χ boomᵗᵖ) = spˢⁿᵉ i χ boomᵗᵖ
fstˢⁿᵉ (spˢⁿᵉ i χ (caseᵗᵖ u v)) = spˢⁿᵉ i χ (caseᵗᵖ (fstˢⁿᶠ u) (fstˢⁿᶠ v))
fstˢⁿᵉ (ᵐspˢⁿᵉ i χ nilᵗᵖ) = ᵐspˢⁿᵉ i (≪fstˢᵖ χ) nilᵗᵖ
fstˢⁿᵉ (ᵐspˢⁿᵉ i χ (unboxᵗᵖ u)) = ᵐspˢⁿᵉ i χ (unboxᵗᵖ (fstˢⁿᶠ u))
fstˢⁿᵉ (ᵐspˢⁿᵉ i χ boomᵗᵖ) = ᵐspˢⁿᵉ i χ boomᵗᵖ
fstˢⁿᵉ (ᵐspˢⁿᵉ i χ (caseᵗᵖ u v)) = ᵐspˢⁿᵉ i χ (caseᵗᵖ (fstˢⁿᶠ u) (fstˢⁿᶠ v))
sndˢⁿᵉ : ∀ {Γ Δ A B} → Γ ⁏ Δ ⊢ˢⁿᵉ A ⩕ B → Γ ⁏ Δ ⊢ˢⁿᵉ B
sndˢⁿᵉ (spˢⁿᵉ i χ nilᵗᵖ) = spˢⁿᵉ i (≪sndˢᵖ χ) nilᵗᵖ
sndˢⁿᵉ (spˢⁿᵉ i χ (unboxᵗᵖ u)) = spˢⁿᵉ i χ (unboxᵗᵖ (sndˢⁿᶠ u))
sndˢⁿᵉ (spˢⁿᵉ i χ boomᵗᵖ) = spˢⁿᵉ i χ boomᵗᵖ
sndˢⁿᵉ (spˢⁿᵉ i χ (caseᵗᵖ u v)) = spˢⁿᵉ i χ (caseᵗᵖ (sndˢⁿᶠ u) (sndˢⁿᶠ v))
sndˢⁿᵉ (ᵐspˢⁿᵉ i χ nilᵗᵖ) = ᵐspˢⁿᵉ i (≪sndˢᵖ χ) nilᵗᵖ
sndˢⁿᵉ (ᵐspˢⁿᵉ i χ (unboxᵗᵖ u)) = ᵐspˢⁿᵉ i χ (unboxᵗᵖ (sndˢⁿᶠ u))
sndˢⁿᵉ (ᵐspˢⁿᵉ i χ boomᵗᵖ) = ᵐspˢⁿᵉ i χ boomᵗᵖ
sndˢⁿᵉ (ᵐspˢⁿᵉ i χ (caseᵗᵖ u v)) = ᵐspˢⁿᵉ i χ (caseᵗᵖ (sndˢⁿᶠ u) (sndˢⁿᶠ v))
-- Iterated expansion.
expand : ∀ {A Γ Δ} → Γ ⁏ Δ ⊢ˢⁿᵉ A → Γ ⁏ Δ ⊢ˢⁿᶠ A
expand {A ⇒ B} t = lamˢⁿᶠ (expand (appˢⁿᵉ (mono⊢ˢⁿᵉ weak⊆ refl⊆ t) (expand (varˢⁿᵉ top))))
expand {□ A} t = neˢⁿᶠ t {{□ A}}
expand {A ⩕ B} t = pairˢⁿᶠ (expand (fstˢⁿᵉ t)) (expand (sndˢⁿᵉ t))
expand {⫪} t = unitˢⁿᶠ
expand {⫫} t = neˢⁿᶠ t {{⫫}}
expand {A ⩖ B} t = neˢⁿᶠ t {{A ⩖ B}}
-- More derived normal forms and neutral forms.
varˢⁿᶠ : ∀ {Γ Δ A} → A ∈ Γ → Γ ⁏ Δ ⊢ˢⁿᶠ A
varˢⁿᶠ i = expand (varˢⁿᵉ i)
ᵐvarˢⁿᶠ : ∀ {Γ Δ A} → A ∈ Δ → Γ ⁏ Δ ⊢ˢⁿᶠ A
ᵐvarˢⁿᶠ i = expand (ᵐvarˢⁿᵉ i)
unboxˢⁿᶠ : ∀ {Γ Δ A C} → Γ ⁏ Δ ⊢ˢⁿᶠ □ A → Γ ⁏ Δ , A ⊢ˢⁿᶠ C → Γ ⁏ Δ ⊢ˢⁿᶠ C
unboxˢⁿᶠ (neˢⁿᶠ t) u = expand (unboxˢⁿᵉ t u)
unboxˢⁿᶠ (boxˢⁿᶠ `t t) u = ᵐ[ top ≔ t ]ˢⁿᶠ u
unboxˢⁿᵉ : ∀ {Γ Δ A C} → Γ ⁏ Δ ⊢ˢⁿᵉ □ A → Γ ⁏ Δ , A ⊢ˢⁿᶠ C → Γ ⁏ Δ ⊢ˢⁿᵉ C
unboxˢⁿᵉ (spˢⁿᵉ i χ nilᵗᵖ) u = spˢⁿᵉ i χ (unboxᵗᵖ u)
unboxˢⁿᵉ (spˢⁿᵉ i χ (unboxᵗᵖ t)) u = spˢⁿᵉ i χ (unboxᵗᵖ (unboxˢⁿᶠ t (mono⊢ˢⁿᶠ refl⊆ (keep (weak⊆)) u)))
unboxˢⁿᵉ (spˢⁿᵉ i χ boomᵗᵖ) u = spˢⁿᵉ i χ boomᵗᵖ
unboxˢⁿᵉ (spˢⁿᵉ i χ (caseᵗᵖ tᵤ tᵥ)) u = spˢⁿᵉ i χ (caseᵗᵖ (unboxˢⁿᶠ tᵤ (mono⊢ˢⁿᶠ weak⊆ refl⊆ u))
(unboxˢⁿᶠ tᵥ (mono⊢ˢⁿᶠ weak⊆ refl⊆ u)))
unboxˢⁿᵉ (ᵐspˢⁿᵉ i χ nilᵗᵖ) u = ᵐspˢⁿᵉ i χ (unboxᵗᵖ u)
unboxˢⁿᵉ (ᵐspˢⁿᵉ i χ (unboxᵗᵖ t)) u = ᵐspˢⁿᵉ i χ (unboxᵗᵖ (unboxˢⁿᶠ t (mono⊢ˢⁿᶠ refl⊆ (keep (weak⊆)) u)))
unboxˢⁿᵉ (ᵐspˢⁿᵉ i χ boomᵗᵖ) u = ᵐspˢⁿᵉ i χ boomᵗᵖ
unboxˢⁿᵉ (ᵐspˢⁿᵉ i χ (caseᵗᵖ tᵤ tᵥ)) u = ᵐspˢⁿᵉ i χ (caseᵗᵖ (unboxˢⁿᶠ tᵤ (mono⊢ˢⁿᶠ weak⊆ refl⊆ u))
(unboxˢⁿᶠ tᵥ (mono⊢ˢⁿᶠ weak⊆ refl⊆ u)))
boomˢⁿᶠ : ∀ {Γ Δ C} → Γ ⁏ Δ ⊢ˢⁿᶠ ⫫ → Γ ⁏ Δ ⊢ˢⁿᶠ C
boomˢⁿᶠ (neˢⁿᶠ t) = expand (boomˢⁿᵉ t)
boomˢⁿᵉ : ∀ {Γ Δ C} → Γ ⁏ Δ ⊢ˢⁿᵉ ⫫ → Γ ⁏ Δ ⊢ˢⁿᵉ C
boomˢⁿᵉ (spˢⁿᵉ i χ nilᵗᵖ) = spˢⁿᵉ i χ boomᵗᵖ
boomˢⁿᵉ (spˢⁿᵉ i χ (unboxᵗᵖ u)) = spˢⁿᵉ i χ (unboxᵗᵖ (boomˢⁿᶠ u))
boomˢⁿᵉ (spˢⁿᵉ i χ boomᵗᵖ) = spˢⁿᵉ i χ boomᵗᵖ
boomˢⁿᵉ (spˢⁿᵉ i χ (caseᵗᵖ u v)) = spˢⁿᵉ i χ (caseᵗᵖ (boomˢⁿᶠ u) (boomˢⁿᶠ v))
boomˢⁿᵉ (ᵐspˢⁿᵉ i χ nilᵗᵖ) = ᵐspˢⁿᵉ i χ boomᵗᵖ
boomˢⁿᵉ (ᵐspˢⁿᵉ i χ (unboxᵗᵖ u)) = ᵐspˢⁿᵉ i χ (unboxᵗᵖ (boomˢⁿᶠ u))
boomˢⁿᵉ (ᵐspˢⁿᵉ i χ boomᵗᵖ) = ᵐspˢⁿᵉ i χ boomᵗᵖ
boomˢⁿᵉ (ᵐspˢⁿᵉ i χ (caseᵗᵖ u v)) = ᵐspˢⁿᵉ i χ (caseᵗᵖ (boomˢⁿᶠ u) (boomˢⁿᶠ v))
caseˢⁿᶠ : ∀ {Γ Δ A B C} → Γ ⁏ Δ ⊢ˢⁿᶠ A ⩖ B → Γ , A ⁏ Δ ⊢ˢⁿᶠ C → Γ , B ⁏ Δ ⊢ˢⁿᶠ C → Γ ⁏ Δ ⊢ˢⁿᶠ C
caseˢⁿᶠ (neˢⁿᶠ t) u v = expand (caseˢⁿᵉ t u v)
caseˢⁿᶠ (leftˢⁿᶠ t) u v = [ top ≔ t ]ˢⁿᶠ u
caseˢⁿᶠ (rightˢⁿᶠ t) u v = [ top ≔ t ]ˢⁿᶠ v
caseˢⁿᵉ : ∀ {Γ Δ A B C} → Γ ⁏ Δ ⊢ˢⁿᵉ A ⩖ B → Γ , A ⁏ Δ ⊢ˢⁿᶠ C → Γ , B ⁏ Δ ⊢ˢⁿᶠ C → Γ ⁏ Δ ⊢ˢⁿᵉ C
caseˢⁿᵉ (spˢⁿᵉ i χ nilᵗᵖ) u v = spˢⁿᵉ i χ (caseᵗᵖ u v)
caseˢⁿᵉ (spˢⁿᵉ i χ (unboxᵗᵖ t)) u v = spˢⁿᵉ i χ (unboxᵗᵖ (caseˢⁿᶠ t (mono⊢ˢⁿᶠ refl⊆ weak⊆ u)
(mono⊢ˢⁿᶠ refl⊆ weak⊆ v)))
caseˢⁿᵉ (spˢⁿᵉ i χ boomᵗᵖ) u v = spˢⁿᵉ i χ boomᵗᵖ
caseˢⁿᵉ (spˢⁿᵉ i χ (caseᵗᵖ tᵤ tᵥ)) u v = spˢⁿᵉ i χ (caseᵗᵖ (caseˢⁿᶠ tᵤ (mono⊢ˢⁿᶠ (keep weak⊆) refl⊆ u)
(mono⊢ˢⁿᶠ (keep weak⊆) refl⊆ v))
(caseˢⁿᶠ tᵥ (mono⊢ˢⁿᶠ (keep weak⊆) refl⊆ u)
(mono⊢ˢⁿᶠ (keep weak⊆) refl⊆ v)))
caseˢⁿᵉ (ᵐspˢⁿᵉ i χ nilᵗᵖ) u v = ᵐspˢⁿᵉ i χ (caseᵗᵖ u v)
caseˢⁿᵉ (ᵐspˢⁿᵉ i χ (unboxᵗᵖ t)) u v = ᵐspˢⁿᵉ i χ (unboxᵗᵖ (caseˢⁿᶠ t (mono⊢ˢⁿᶠ refl⊆ weak⊆ u)
(mono⊢ˢⁿᶠ refl⊆ weak⊆ v)))
caseˢⁿᵉ (ᵐspˢⁿᵉ i χ boomᵗᵖ) u v = ᵐspˢⁿᵉ i χ boomᵗᵖ
caseˢⁿᵉ (ᵐspˢⁿᵉ i χ (caseᵗᵖ tᵤ tᵥ)) u v = ᵐspˢⁿᵉ i χ (caseᵗᵖ (caseˢⁿᶠ tᵤ (mono⊢ˢⁿᶠ (keep weak⊆) refl⊆ u)
(mono⊢ˢⁿᶠ (keep weak⊆) refl⊆ v))
(caseˢⁿᶠ tᵥ (mono⊢ˢⁿᶠ (keep weak⊆) refl⊆ u)
(mono⊢ˢⁿᶠ (keep weak⊆) refl⊆ v)))
-- Normalisation by hereditary substitution.
nbhs : ∀ {A Γ Δ} → Γ ⁏ Δ ⊢ A → Γ ⁏ Δ ⊢ˢⁿᶠ A
nbhs (var i) = varˢⁿᶠ i
nbhs (ᵐvar i) = ᵐvarˢⁿᶠ i
nbhs (lam t) = lamˢⁿᶠ (nbhs t)
nbhs (app t u) = appˢⁿᶠ (nbhs t) (nbhs u)
nbhs (box t) = boxˢⁿᶠ t (nbhs t)
nbhs (unbox t u) = unboxˢⁿᶠ (nbhs t) (nbhs u)
nbhs (pair t u) = pairˢⁿᶠ (nbhs t) (nbhs u)
nbhs (fst t) = fstˢⁿᶠ (nbhs t)
nbhs (snd t) = sndˢⁿᶠ (nbhs t)
nbhs unit = unitˢⁿᶠ
nbhs (boom t) = boomˢⁿᶠ (nbhs t)
nbhs (left t) = leftˢⁿᶠ (nbhs t)
nbhs (right t) = rightˢⁿᶠ (nbhs t)
nbhs (case t u v) = caseˢⁿᶠ (nbhs t) (nbhs u) (nbhs v)
nbhs′ : ∀ {A Γ Δ} → Γ ⁏ Δ ⊢ A → Γ ⁏ Δ ⊢ⁿᶠ A
nbhs′ t = snf→nf (nbhs t)
Raw
S4NormalForm.agda
module S4NormalForm where
open import S4 public
-- Proofs in normal form and neutral form.
mutual
infix 3 _⁏_⊢ⁿᶠ_
data _⁏_⊢ⁿᶠ_ (Γ Δ : Seq) : Prop → Set where
lamⁿᶠ : ∀ {A B} → Γ , A ⁏ Δ ⊢ⁿᶠ B → Γ ⁏ Δ ⊢ⁿᶠ A ⇒ B
boxⁿᶠ : ∀ {A} → ∅ ⁏ Δ ⊢ A → Γ ⁏ Δ ⊢ⁿᶠ □ A
pairⁿᶠ : ∀ {A B} → Γ ⁏ Δ ⊢ⁿᶠ A → Γ ⁏ Δ ⊢ⁿᶠ B → Γ ⁏ Δ ⊢ⁿᶠ A ⩕ B
unitⁿᶠ : Γ ⁏ Δ ⊢ⁿᶠ ⫪
leftⁿᶠ : ∀ {A B} → Γ ⁏ Δ ⊢ⁿᶠ A → Γ ⁏ Δ ⊢ⁿᶠ A ⩖ B
rightⁿᶠ : ∀ {A B} → Γ ⁏ Δ ⊢ⁿᶠ B → Γ ⁏ Δ ⊢ⁿᶠ A ⩖ B
neⁿᶠ : ∀ {A} → Γ ⁏ Δ ⊢ⁿᵉ A → Γ ⁏ Δ ⊢ⁿᶠ A
infix 3 _⁏_⊢ⁿᵉ_
data _⁏_⊢ⁿᵉ_ (Γ Δ : Seq) : Prop → Set where
varⁿᵉ : ∀ {A} → A ∈ Γ → Γ ⁏ Δ ⊢ⁿᵉ A
ᵐvarⁿᵉ : ∀ {A} → A ∈ Δ → Γ ⁏ Δ ⊢ⁿᵉ A
appⁿᵉ : ∀ {A B} → Γ ⁏ Δ ⊢ⁿᵉ A ⇒ B → Γ ⁏ Δ ⊢ⁿᶠ A → Γ ⁏ Δ ⊢ⁿᵉ B
unboxⁿᵉ : ∀ {A C} → Γ ⁏ Δ ⊢ⁿᵉ □ A → Γ ⁏ Δ , A ⊢ⁿᶠ C → Γ ⁏ Δ ⊢ⁿᵉ C
fstⁿᵉ : ∀ {A B} → Γ ⁏ Δ ⊢ⁿᵉ A ⩕ B → Γ ⁏ Δ ⊢ⁿᵉ A
sndⁿᵉ : ∀ {A B} → Γ ⁏ Δ ⊢ⁿᵉ A ⩕ B → Γ ⁏ Δ ⊢ⁿᵉ B
boomⁿᵉ : ∀ {C} → Γ ⁏ Δ ⊢ⁿᵉ ⫫ → Γ ⁏ Δ ⊢ⁿᵉ C
caseⁿᵉ : ∀ {A B C} → Γ ⁏ Δ ⊢ⁿᵉ A ⩖ B → Γ , A ⁏ Δ ⊢ⁿᶠ C → Γ , B ⁏ Δ ⊢ⁿᶠ C → Γ ⁏ Δ ⊢ⁿᵉ C
infix 3 _⁏_⊢⋆ⁿᵉ_
_⁏_⊢⋆ⁿᵉ_ : Seq → Seq → Seq → Set
Γ ⁏ Δ ⊢⋆ⁿᵉ ∅ = ⊤
Γ ⁏ Δ ⊢⋆ⁿᵉ Ξ , A = Γ ⁏ Δ ⊢⋆ⁿᵉ Ξ ∧ Γ ⁏ Δ ⊢ⁿᵉ A
-- Shorthand for variables.
v₀ⁿᵉ : ∀ {Γ Δ A} → Γ , A ⁏ Δ ⊢ⁿᵉ A
v₀ⁿᵉ = varⁿᵉ top
ᵐv₀ⁿᵉ : ∀ {Γ Δ A} → Γ ⁏ Δ , A ⊢ⁿᵉ A
ᵐv₀ⁿᵉ = ᵐvarⁿᵉ top
-- Translation from normal form to non-normal form.
mutual
nf→tm : ∀ {Γ Δ A} → Γ ⁏ Δ ⊢ⁿᶠ A → Γ ⁏ Δ ⊢ A
nf→tm (lamⁿᶠ t) = lam (nf→tm t)
nf→tm (boxⁿᶠ t) = box t
nf→tm (pairⁿᶠ t u) = pair (nf→tm t) (nf→tm u)
nf→tm unitⁿᶠ = unit
nf→tm (leftⁿᶠ t) = left (nf→tm t)
nf→tm (rightⁿᶠ t) = right (nf→tm t)
nf→tm (neⁿᶠ t) = ne→tm t
ne→tm : ∀ {Γ Δ A} → Γ ⁏ Δ ⊢ⁿᵉ A → Γ ⁏ Δ ⊢ A
ne→tm (varⁿᵉ i) = var i
ne→tm (ᵐvarⁿᵉ i) = ᵐvar i
ne→tm (appⁿᵉ t u) = app (ne→tm t) (nf→tm u)
ne→tm (unboxⁿᵉ t u) = unbox (ne→tm t) (nf→tm u)
ne→tm (fstⁿᵉ t) = fst (ne→tm t)
ne→tm (sndⁿᵉ t) = snd (ne→tm t)
ne→tm (boomⁿᵉ t) = boom (ne→tm t)
ne→tm (caseⁿᵉ t u v) = case (ne→tm t) (nf→tm u) (nf→tm v)
-- Monotonicity with respect to context inclusion.
mutual
mono⊢ⁿᶠ : ∀ {Γ Γ′ Δ Δ′ A} → Γ ⊆ Γ′ → Δ ⊆ Δ′ → Γ ⁏ Δ ⊢ⁿᶠ A → Γ′ ⁏ Δ′ ⊢ⁿᶠ A
mono⊢ⁿᶠ η θ (lamⁿᶠ t) = lamⁿᶠ (mono⊢ⁿᶠ (keep η) θ t)
mono⊢ⁿᶠ η θ (boxⁿᶠ t) = boxⁿᶠ (mono⊢ done θ t)
mono⊢ⁿᶠ η θ (pairⁿᶠ t u) = pairⁿᶠ (mono⊢ⁿᶠ η θ t) (mono⊢ⁿᶠ η θ u)
mono⊢ⁿᶠ η θ unitⁿᶠ = unitⁿᶠ
mono⊢ⁿᶠ η θ (leftⁿᶠ t) = leftⁿᶠ (mono⊢ⁿᶠ η θ t)
mono⊢ⁿᶠ η θ (rightⁿᶠ t) = rightⁿᶠ (mono⊢ⁿᶠ η θ t)
mono⊢ⁿᶠ η θ (neⁿᶠ t) = neⁿᶠ (mono⊢ⁿᵉ η θ t)
mono⊢ⁿᵉ : ∀ {Γ Γ′ Δ Δ′ A} → Γ ⊆ Γ′ → Δ ⊆ Δ′ → Γ ⁏ Δ ⊢ⁿᵉ A → Γ′ ⁏ Δ′ ⊢ⁿᵉ A
mono⊢ⁿᵉ η θ (varⁿᵉ i) = varⁿᵉ (mono∈ η i)
mono⊢ⁿᵉ η θ (ᵐvarⁿᵉ i) = ᵐvarⁿᵉ (mono∈ θ i)
mono⊢ⁿᵉ η θ (appⁿᵉ t u) = appⁿᵉ (mono⊢ⁿᵉ η θ t) (mono⊢ⁿᶠ η θ u)
mono⊢ⁿᵉ η θ (unboxⁿᵉ t u) = unboxⁿᵉ (mono⊢ⁿᵉ η θ t) (mono⊢ⁿᶠ η (keep θ) u)
mono⊢ⁿᵉ η θ (fstⁿᵉ t) = fstⁿᵉ (mono⊢ⁿᵉ η θ t)
mono⊢ⁿᵉ η θ (sndⁿᵉ t) = sndⁿᵉ (mono⊢ⁿᵉ η θ t)
mono⊢ⁿᵉ η θ (boomⁿᵉ t) = boomⁿᵉ (mono⊢ⁿᵉ η θ t)
mono⊢ⁿᵉ η θ (caseⁿᵉ t u v) = caseⁿᵉ (mono⊢ⁿᵉ η θ t) (mono⊢ⁿᶠ (keep η) θ u) (mono⊢ⁿᶠ (keep η) θ v)
mono⊢⋆ⁿᵉ : ∀ {Ξ Γ Γ′ Δ Δ′} → Γ ⊆ Γ′ → Δ ⊆ Δ′ → Γ ⁏ Δ ⊢⋆ⁿᵉ Ξ → Γ′ ⁏ Δ′ ⊢⋆ⁿᵉ Ξ
mono⊢⋆ⁿᵉ {∅} η θ ∙ = ∙
mono⊢⋆ⁿᵉ {Ξ , A} η θ (τ , t) = mono⊢⋆ⁿᵉ η θ τ , mono⊢ⁿᵉ η θ t
-- Reflexivity.
refl⊢⋆ⁿᵉ : ∀ {Γ Δ} → Γ ⁏ Δ ⊢⋆ⁿᵉ Γ
refl⊢⋆ⁿᵉ {∅} = ∙
refl⊢⋆ⁿᵉ {Γ , A} = mono⊢⋆ⁿᵉ weak⊆ refl⊆ refl⊢⋆ⁿᵉ , v₀ⁿᵉ
ᵐrefl⊢⋆ⁿᵉ : ∀ {Δ} → ∅ ⁏ Δ ⊢⋆ⁿᵉ Δ
ᵐrefl⊢⋆ⁿᵉ {∅} = ∙
ᵐrefl⊢⋆ⁿᵉ {Γ , A} = mono⊢⋆ⁿᵉ refl⊆ weak⊆ ᵐrefl⊢⋆ⁿᵉ , ᵐv₀ⁿᵉ
Raw
S4SpinalNormalForm.agda
module S4SpinalNormalForm where
open import S4NormalForm public
-- Propositions used in proofs in spinal neutral form.
data Propˢⁿᵉ : Prop → Set where
□_ : (A : Prop) → Propˢⁿᵉ (□ A)
⫫ : Propˢⁿᵉ ⫫
_⩖_ : (A B : Prop) → Propˢⁿᵉ (A ⩖ B)
-- Proofs in spinal normal form and spinal neutral form.
mutual
infix 3 _⁏_⊢ˢⁿᶠ_
data _⁏_⊢ˢⁿᶠ_ (Γ Δ : Seq) : Prop → Set where
neˢⁿᶠ : ∀ {A} → Γ ⁏ Δ ⊢ˢⁿᵉ A → {{_ : Propˢⁿᵉ A}} → Γ ⁏ Δ ⊢ˢⁿᶠ A
lamˢⁿᶠ : ∀ {A B} → Γ , A ⁏ Δ ⊢ˢⁿᶠ B → Γ ⁏ Δ ⊢ˢⁿᶠ A ⇒ B
boxˢⁿᶠ : ∀ {A} → ∅ ⁏ Δ ⊢ A → Γ ⁏ Δ ⊢ˢⁿᶠ □ A
pairˢⁿᶠ : ∀ {A B} → Γ ⁏ Δ ⊢ˢⁿᶠ A → Γ ⁏ Δ ⊢ˢⁿᶠ B → Γ ⁏ Δ ⊢ˢⁿᶠ A ⩕ B
unitˢⁿᶠ : Γ ⁏ Δ ⊢ˢⁿᶠ ⫪
leftˢⁿᶠ : ∀ {A B} → Γ ⁏ Δ ⊢ˢⁿᶠ A → Γ ⁏ Δ ⊢ˢⁿᶠ A ⩖ B
rightˢⁿᶠ : ∀ {A B} → Γ ⁏ Δ ⊢ˢⁿᶠ B → Γ ⁏ Δ ⊢ˢⁿᶠ A ⩖ B
infix 3 _⁏_⊢ˢⁿᵉ_
data _⁏_⊢ˢⁿᵉ_ (Γ Δ : Seq) : Prop → Set where
spˢⁿᵉ : ∀ {A B C} → A ∈ Γ → Γ ⁏ Δ ⊢ˢᵖ A ⦙ B → Γ ⁏ Δ ⊢ᵗᵖ B ⦙ C → Γ ⁏ Δ ⊢ˢⁿᵉ C
ᵐspˢⁿᵉ : ∀ {A B C} → A ∈ Δ → Γ ⁏ Δ ⊢ˢᵖ A ⦙ B → Γ ⁏ Δ ⊢ᵗᵖ B ⦙ C → Γ ⁏ Δ ⊢ˢⁿᵉ C
-- Spines.
infix 3 _⁏_⊢ˢᵖ_⦙_
data _⁏_⊢ˢᵖ_⦙_ (Γ Δ : Seq) : Prop → Prop → Set where
nilˢᵖ : ∀ {C} → Γ ⁏ Δ ⊢ˢᵖ C ⦙ C
appˢᵖ : ∀ {A B C} → Γ ⁏ Δ ⊢ˢᵖ B ⦙ C → Γ ⁏ Δ ⊢ˢⁿᶠ A → Γ ⁏ Δ ⊢ˢᵖ A ⇒ B ⦙ C
fstˢᵖ : ∀ {A B C} → Γ ⁏ Δ ⊢ˢᵖ A ⦙ C → Γ ⁏ Δ ⊢ˢᵖ A ⩕ B ⦙ C
sndˢᵖ : ∀ {A B C} → Γ ⁏ Δ ⊢ˢᵖ B ⦙ C → Γ ⁏ Δ ⊢ˢᵖ A ⩕ B ⦙ C
-- Spine tips.
infix 3 _⁏_⊢ᵗᵖ_⦙_
data _⁏_⊢ᵗᵖ_⦙_ (Γ Δ : Seq) : Prop → Prop → Set where
nilᵗᵖ : ∀ {C} → Γ ⁏ Δ ⊢ᵗᵖ C ⦙ C
unboxᵗᵖ : ∀ {A C} → Γ ⁏ Δ , A ⊢ˢⁿᶠ C → Γ ⁏ Δ ⊢ᵗᵖ □ A ⦙ C
boomᵗᵖ : ∀ {C} → Γ ⁏ Δ ⊢ᵗᵖ ⫫ ⦙ C
caseᵗᵖ : ∀ {A B C} → Γ , A ⁏ Δ ⊢ˢⁿᶠ C → Γ , B ⁏ Δ ⊢ˢⁿᶠ C → Γ ⁏ Δ ⊢ᵗᵖ A ⩖ B ⦙ C
infix 3 _⁏_⊢⋆ˢⁿᵉ_
_⁏_⊢⋆ˢⁿᵉ_ : Seq → Seq → Seq → Set
Γ ⁏ Δ ⊢⋆ˢⁿᵉ ∅ = ⊤
Γ ⁏ Δ ⊢⋆ˢⁿᵉ Ξ , A = Γ ⁏ Δ ⊢⋆ˢⁿᵉ Ξ ∧ Γ ⁏ Δ ⊢ˢⁿᵉ A
-- Translation from spinal normal form to normal form.
mutual
snf→nf : ∀ {Γ Δ A} → Γ ⁏ Δ ⊢ˢⁿᶠ A → Γ ⁏ Δ ⊢ⁿᶠ A
snf→nf (neˢⁿᶠ t) = neⁿᶠ (sne→nf t)
snf→nf (lamˢⁿᶠ t) = lamⁿᶠ (snf→nf t)
snf→nf (boxˢⁿᶠ t) = boxⁿᶠ t
snf→nf (pairˢⁿᶠ t u) = pairⁿᶠ (snf→nf t) (snf→nf u)
snf→nf unitˢⁿᶠ = unitⁿᶠ
snf→nf (leftˢⁿᶠ t) = leftⁿᶠ (snf→nf t)
snf→nf (rightˢⁿᶠ t) = rightⁿᶠ (snf→nf t)
sne→nf : ∀ {Γ Δ A} → Γ ⁏ Δ ⊢ˢⁿᵉ A → Γ ⁏ Δ ⊢ⁿᵉ A
sne→nf (spˢⁿᵉ i χ y) = tp→nf (varⁿᵉ i) χ y
sne→nf (ᵐspˢⁿᵉ i χ y) = tp→nf (ᵐvarⁿᵉ i) χ y
sp→nf : ∀ {Γ Δ A C} → Γ ⁏ Δ ⊢ⁿᵉ A → Γ ⁏ Δ ⊢ˢᵖ A ⦙ C → Γ ⁏ Δ ⊢ⁿᵉ C
sp→nf t nilˢᵖ = t
sp→nf t (appˢᵖ χ u) = sp→nf (appⁿᵉ t (snf→nf u)) χ
sp→nf t (fstˢᵖ χ) = sp→nf (fstⁿᵉ t) χ
sp→nf t (sndˢᵖ χ) = sp→nf (sndⁿᵉ t) χ
tp→nf : ∀ {Γ Δ A B C} → Γ ⁏ Δ ⊢ⁿᵉ A → Γ ⁏ Δ ⊢ˢᵖ A ⦙ B → Γ ⁏ Δ ⊢ᵗᵖ B ⦙ C → Γ ⁏ Δ ⊢ⁿᵉ C
tp→nf t χ nilᵗᵖ = sp→nf t χ
tp→nf t χ (unboxᵗᵖ u) = unboxⁿᵉ (sp→nf t χ) (snf→nf u)
tp→nf t χ boomᵗᵖ = boomⁿᵉ (sp→nf t χ)
tp→nf t χ (caseᵗᵖ u v) = caseⁿᵉ (sp→nf t χ) (snf→nf u) (snf→nf v)
-- Translation from spinal normal form to non-normal form.
mutual
snf→tm : ∀ {Γ Δ A} → Γ ⁏ Δ ⊢ˢⁿᶠ A → Γ ⁏ Δ ⊢ A
snf→tm (neˢⁿᶠ t) = sne→tm t
snf→tm (lamˢⁿᶠ t) = lam (snf→tm t)
snf→tm (boxˢⁿᶠ t) = box t
snf→tm (pairˢⁿᶠ t u) = pair (snf→tm t) (snf→tm u)
snf→tm unitˢⁿᶠ = unit
snf→tm (leftˢⁿᶠ t) = left (snf→tm t)
snf→tm (rightˢⁿᶠ t) = right (snf→tm t)
sne→tm : ∀ {Γ Δ A} → Γ ⁏ Δ ⊢ˢⁿᵉ A → Γ ⁏ Δ ⊢ A
sne→tm (spˢⁿᵉ i χ y) = tp→tm (var i) χ y
sne→tm (ᵐspˢⁿᵉ i χ y) = tp→tm (ᵐvar i) χ y
sp→tm : ∀ {Γ Δ A C} → Γ ⁏ Δ ⊢ A → Γ ⁏ Δ ⊢ˢᵖ A ⦙ C → Γ ⁏ Δ ⊢ C
sp→tm t nilˢᵖ = t
sp→tm t (appˢᵖ χ u) = sp→tm (app t (snf→tm u)) χ
sp→tm t (fstˢᵖ χ) = sp→tm (fst t) χ
sp→tm t (sndˢᵖ χ) = sp→tm (snd t) χ
tp→tm : ∀ {Γ Δ A B C} → Γ ⁏ Δ ⊢ A → Γ ⁏ Δ ⊢ˢᵖ A ⦙ B → Γ ⁏ Δ ⊢ᵗᵖ B ⦙ C → Γ ⁏ Δ ⊢ C
tp→tm t χ nilᵗᵖ = sp→tm t χ
tp→tm t χ (unboxᵗᵖ u) = unbox (sp→tm t χ) (snf→tm u)
tp→tm t χ boomᵗᵖ = boom (sp→tm t χ)
tp→tm t χ (caseᵗᵖ u v) = case (sp→tm t χ) (snf→tm u) (snf→tm v)
-- Monotonicity with respect to context inclusion.
mutual
mono⊢ˢⁿᶠ : ∀ {Γ Γ′ Δ Δ′ A} → Γ ⊆ Γ′ → Δ ⊆ Δ′ → Γ ⁏ Δ ⊢ˢⁿᶠ A → Γ′ ⁏ Δ′ ⊢ˢⁿᶠ A
mono⊢ˢⁿᶠ η θ (neˢⁿᶠ t) = neˢⁿᶠ (mono⊢ˢⁿᵉ η θ t)
mono⊢ˢⁿᶠ η θ (lamˢⁿᶠ t) = lamˢⁿᶠ (mono⊢ˢⁿᶠ (keep η) θ t)
mono⊢ˢⁿᶠ η θ (boxˢⁿᶠ t) = boxˢⁿᶠ (mono⊢ done θ t)
mono⊢ˢⁿᶠ η θ (pairˢⁿᶠ t u) = pairˢⁿᶠ (mono⊢ˢⁿᶠ η θ t) (mono⊢ˢⁿᶠ η θ u)
mono⊢ˢⁿᶠ η θ unitˢⁿᶠ = unitˢⁿᶠ
mono⊢ˢⁿᶠ η θ (leftˢⁿᶠ t) = leftˢⁿᶠ (mono⊢ˢⁿᶠ η θ t)
mono⊢ˢⁿᶠ η θ (rightˢⁿᶠ t) = rightˢⁿᶠ (mono⊢ˢⁿᶠ η θ t)
mono⊢ˢⁿᵉ : ∀ {Γ Γ′ Δ Δ′ A} → Γ ⊆ Γ′ → Δ ⊆ Δ′ → Γ ⁏ Δ ⊢ˢⁿᵉ A → Γ′ ⁏ Δ′ ⊢ˢⁿᵉ A
mono⊢ˢⁿᵉ η θ (spˢⁿᵉ i χ y) = spˢⁿᵉ (mono∈ η i) (mono⊢ˢᵖ η θ χ) (mono⊢ᵗᵖ η θ y)
mono⊢ˢⁿᵉ η θ (ᵐspˢⁿᵉ i χ y) = ᵐspˢⁿᵉ (mono∈ θ i) (mono⊢ˢᵖ η θ χ) (mono⊢ᵗᵖ η θ y)
mono⊢ˢᵖ : ∀ {Γ Γ′ Δ Δ′ A C} → Γ ⊆ Γ′ → Δ ⊆ Δ′ → Γ ⁏ Δ ⊢ˢᵖ A ⦙ C → Γ′ ⁏ Δ′ ⊢ˢᵖ A ⦙ C
mono⊢ˢᵖ η θ nilˢᵖ = nilˢᵖ
mono⊢ˢᵖ η θ (appˢᵖ χ u) = appˢᵖ (mono⊢ˢᵖ η θ χ) (mono⊢ˢⁿᶠ η θ u)
mono⊢ˢᵖ η θ (fstˢᵖ χ) = fstˢᵖ (mono⊢ˢᵖ η θ χ)
mono⊢ˢᵖ η θ (sndˢᵖ χ) = sndˢᵖ (mono⊢ˢᵖ η θ χ)
mono⊢ᵗᵖ : ∀ {Γ Γ′ Δ Δ′ A C} → Γ ⊆ Γ′ → Δ ⊆ Δ′ → Γ ⁏ Δ ⊢ᵗᵖ A ⦙ C → Γ′ ⁏ Δ′ ⊢ᵗᵖ A ⦙ C
mono⊢ᵗᵖ η θ nilᵗᵖ = nilᵗᵖ
mono⊢ᵗᵖ η θ (unboxᵗᵖ u) = unboxᵗᵖ (mono⊢ˢⁿᶠ η (keep θ) u)
mono⊢ᵗᵖ η θ boomᵗᵖ = boomᵗᵖ
mono⊢ᵗᵖ η θ (caseᵗᵖ u v) = caseᵗᵖ (mono⊢ˢⁿᶠ (keep η) θ u) (mono⊢ˢⁿᶠ (keep η) θ v)
mono⊢⋆ˢⁿᵉ : ∀ {Ξ Γ Γ′ Δ Δ′} → Γ ⊆ Γ′ → Δ ⊆ Δ′ → Γ ⁏ Δ ⊢⋆ˢⁿᵉ Ξ → Γ′ ⁏ Δ′ ⊢⋆ˢⁿᵉ Ξ
mono⊢⋆ˢⁿᵉ {∅} η θ tt = tt
mono⊢⋆ˢⁿᵉ {Ξ , A} η θ (τ , t) = mono⊢⋆ˢⁿᵉ η θ τ , mono⊢ˢⁿᵉ η θ t
Raw
S4SpinalNormalFormWrong.agda
module S4SpinalNormalFormWrong where
open import S4NormalForm public
-- Propositions used in proofs in spinal neutral form.
data Propˢⁿᵉ : Prop → Set where
□_ : (A : Prop) → Propˢⁿᵉ (□ A)
⫫ : Propˢⁿᵉ ⫫
_⩖_ : (A B : Prop) → Propˢⁿᵉ (A ⩖ B)
-- Proofs in spinal normal form and spinal neutral form.
mutual
infix 3 _⁏_⊢ˢⁿᶠ_
data _⁏_⊢ˢⁿᶠ_ (Γ Δ : Seq) : Prop → Set where
neˢⁿᶠ : ∀ {A} → Γ ⁏ Δ ⊢ˢⁿᵉ A → {{_ : Propˢⁿᵉ A}} → Γ ⁏ Δ ⊢ˢⁿᶠ A
lamˢⁿᶠ : ∀ {A B} → Γ , A ⁏ Δ ⊢ˢⁿᶠ B → Γ ⁏ Δ ⊢ˢⁿᶠ A ⇒ B
boxˢⁿᶠ : ∀ {A} → ∅ ⁏ Δ ⊢ A → ∅ ⁏ Δ ⊢ˢⁿᶠ A → Γ ⁏ Δ ⊢ˢⁿᶠ □ A
pairˢⁿᶠ : ∀ {A B} → Γ ⁏ Δ ⊢ˢⁿᶠ A → Γ ⁏ Δ ⊢ˢⁿᶠ B → Γ ⁏ Δ ⊢ˢⁿᶠ A ⩕ B
unitˢⁿᶠ : Γ ⁏ Δ ⊢ˢⁿᶠ ⫪
leftˢⁿᶠ : ∀ {A B} → Γ ⁏ Δ ⊢ˢⁿᶠ A → Γ ⁏ Δ ⊢ˢⁿᶠ A ⩖ B
rightˢⁿᶠ : ∀ {A B} → Γ ⁏ Δ ⊢ˢⁿᶠ B → Γ ⁏ Δ ⊢ˢⁿᶠ A ⩖ B
infix 3 _⁏_⊢ˢⁿᵉ_
data _⁏_⊢ˢⁿᵉ_ (Γ Δ : Seq) : Prop → Set where
spˢⁿᵉ : ∀ {A B C} → A ∈ Γ → Γ ⁏ Δ ⊢ˢᵖ A ⦙ B → Γ ⁏ Δ ⊢ᵗᵖ B ⦙ C → Γ ⁏ Δ ⊢ˢⁿᵉ C
ᵐspˢⁿᵉ : ∀ {A B C} → A ∈ Δ → Γ ⁏ Δ ⊢ˢᵖ A ⦙ B → Γ ⁏ Δ ⊢ᵗᵖ B ⦙ C → Γ ⁏ Δ ⊢ˢⁿᵉ C
-- Spines.
infix 3 _⁏_⊢ˢᵖ_⦙_
data _⁏_⊢ˢᵖ_⦙_ (Γ Δ : Seq) : Prop → Prop → Set where
nilˢᵖ : ∀ {C} → Γ ⁏ Δ ⊢ˢᵖ C ⦙ C
appˢᵖ : ∀ {A B C} → Γ ⁏ Δ ⊢ˢᵖ B ⦙ C → Γ ⁏ Δ ⊢ˢⁿᶠ A → Γ ⁏ Δ ⊢ˢᵖ A ⇒ B ⦙ C
fstˢᵖ : ∀ {A B C} → Γ ⁏ Δ ⊢ˢᵖ A ⦙ C → Γ ⁏ Δ ⊢ˢᵖ A ⩕ B ⦙ C
sndˢᵖ : ∀ {A B C} → Γ ⁏ Δ ⊢ˢᵖ B ⦙ C → Γ ⁏ Δ ⊢ˢᵖ A ⩕ B ⦙ C
-- Spine tips.
infix 3 _⁏_⊢ᵗᵖ_⦙_
data _⁏_⊢ᵗᵖ_⦙_ (Γ Δ : Seq) : Prop → Prop → Set where
nilᵗᵖ : ∀ {C} → Γ ⁏ Δ ⊢ᵗᵖ C ⦙ C
unboxᵗᵖ : ∀ {A C} → Γ ⁏ Δ , A ⊢ˢⁿᶠ C → Γ ⁏ Δ ⊢ᵗᵖ □ A ⦙ C
boomᵗᵖ : ∀ {C} → Γ ⁏ Δ ⊢ᵗᵖ ⫫ ⦙ C
caseᵗᵖ : ∀ {A B C} → Γ , A ⁏ Δ ⊢ˢⁿᶠ C → Γ , B ⁏ Δ ⊢ˢⁿᶠ C → Γ ⁏ Δ ⊢ᵗᵖ A ⩖ B ⦙ C
infix 3 _⁏_⊢⋆ˢⁿᵉ_
_⁏_⊢⋆ˢⁿᵉ_ : Seq → Seq → Seq → Set
Γ ⁏ Δ ⊢⋆ˢⁿᵉ ∅ = ⊤
Γ ⁏ Δ ⊢⋆ˢⁿᵉ Ξ , A = Γ ⁏ Δ ⊢⋆ˢⁿᵉ Ξ ∧ Γ ⁏ Δ ⊢ˢⁿᵉ A
-- Translation from spinal normal form to normal form.
mutual
snf→nf : ∀ {Γ Δ A} → Γ ⁏ Δ ⊢ˢⁿᶠ A → Γ ⁏ Δ ⊢ⁿᶠ A
snf→nf (neˢⁿᶠ t) = neⁿᶠ (sne→nf t)
snf→nf (lamˢⁿᶠ t) = lamⁿᶠ (snf→nf t)
snf→nf (boxˢⁿᶠ `t t) = boxⁿᶠ `t
snf→nf (pairˢⁿᶠ t u) = pairⁿᶠ (snf→nf t) (snf→nf u)
snf→nf unitˢⁿᶠ = unitⁿᶠ
snf→nf (leftˢⁿᶠ t) = leftⁿᶠ (snf→nf t)
snf→nf (rightˢⁿᶠ t) = rightⁿᶠ (snf→nf t)
sne→nf : ∀ {Γ Δ A} → Γ ⁏ Δ ⊢ˢⁿᵉ A → Γ ⁏ Δ ⊢ⁿᵉ A
sne→nf (spˢⁿᵉ i χ y) = tp→nf (varⁿᵉ i) χ y
sne→nf (ᵐspˢⁿᵉ i χ y) = tp→nf (ᵐvarⁿᵉ i) χ y
sp→nf : ∀ {Γ Δ A C} → Γ ⁏ Δ ⊢ⁿᵉ A → Γ ⁏ Δ ⊢ˢᵖ A ⦙ C → Γ ⁏ Δ ⊢ⁿᵉ C
sp→nf t nilˢᵖ = t
sp→nf t (appˢᵖ χ u) = sp→nf (appⁿᵉ t (snf→nf u)) χ
sp→nf t (fstˢᵖ χ) = sp→nf (fstⁿᵉ t) χ
sp→nf t (sndˢᵖ χ) = sp→nf (sndⁿᵉ t) χ
tp→nf : ∀ {Γ Δ A B C} → Γ ⁏ Δ ⊢ⁿᵉ A → Γ ⁏ Δ ⊢ˢᵖ A ⦙ B → Γ ⁏ Δ ⊢ᵗᵖ B ⦙ C → Γ ⁏ Δ ⊢ⁿᵉ C
tp→nf t χ nilᵗᵖ = sp→nf t χ
tp→nf t χ (unboxᵗᵖ u) = unboxⁿᵉ (sp→nf t χ) (snf→nf u)
tp→nf t χ boomᵗᵖ = boomⁿᵉ (sp→nf t χ)
tp→nf t χ (caseᵗᵖ u v) = caseⁿᵉ (sp→nf t χ) (snf→nf u) (snf→nf v)
-- Translation from spinal normal form to non-normal form.
mutual
snf→tm : ∀ {Γ Δ A} → Γ ⁏ Δ ⊢ˢⁿᶠ A → Γ ⁏ Δ ⊢ A
snf→tm (neˢⁿᶠ t) = sne→tm t
snf→tm (lamˢⁿᶠ t) = lam (snf→tm t)
snf→tm (boxˢⁿᶠ `t t) = box `t
snf→tm (pairˢⁿᶠ t u) = pair (snf→tm t) (snf→tm u)
snf→tm unitˢⁿᶠ = unit
snf→tm (leftˢⁿᶠ t) = left (snf→tm t)
snf→tm (rightˢⁿᶠ t) = right (snf→tm t)
sne→tm : ∀ {Γ Δ A} → Γ ⁏ Δ ⊢ˢⁿᵉ A → Γ ⁏ Δ ⊢ A
sne→tm (spˢⁿᵉ i χ y) = tp→tm (var i) χ y
sne→tm (ᵐspˢⁿᵉ i χ y) = tp→tm (ᵐvar i) χ y
sp→tm : ∀ {Γ Δ A C} → Γ ⁏ Δ ⊢ A → Γ ⁏ Δ ⊢ˢᵖ A ⦙ C → Γ ⁏ Δ ⊢ C
sp→tm t nilˢᵖ = t
sp→tm t (appˢᵖ χ u) = sp→tm (app t (snf→tm u)) χ
sp→tm t (fstˢᵖ χ) = sp→tm (fst t) χ
sp→tm t (sndˢᵖ χ) = sp→tm (snd t) χ
tp→tm : ∀ {Γ Δ A B C} → Γ ⁏ Δ ⊢ A → Γ ⁏ Δ ⊢ˢᵖ A ⦙ B → Γ ⁏ Δ ⊢ᵗᵖ B ⦙ C → Γ ⁏ Δ ⊢ C
tp→tm t χ nilᵗᵖ = sp→tm t χ
tp→tm t χ (unboxᵗᵖ u) = unbox (sp→tm t χ) (snf→tm u)
tp→tm t χ boomᵗᵖ = boom (sp→tm t χ)
tp→tm t χ (caseᵗᵖ u v) = case (sp→tm t χ) (snf→tm u) (snf→tm v)
-- Monotonicity with respect to context inclusion.
mutual
mono⊢ˢⁿᶠ : ∀ {Γ Γ′ Δ Δ′ A} → Γ ⊆ Γ′ → Δ ⊆ Δ′ → Γ ⁏ Δ ⊢ˢⁿᶠ A → Γ′ ⁏ Δ′ ⊢ˢⁿᶠ A
mono⊢ˢⁿᶠ η θ (neˢⁿᶠ t) = neˢⁿᶠ (mono⊢ˢⁿᵉ η θ t)
mono⊢ˢⁿᶠ η θ (lamˢⁿᶠ t) = lamˢⁿᶠ (mono⊢ˢⁿᶠ (keep η) θ t)
mono⊢ˢⁿᶠ η θ (boxˢⁿᶠ `t t) = boxˢⁿᶠ (mono⊢ done θ `t) (mono⊢ˢⁿᶠ done θ t)
mono⊢ˢⁿᶠ η θ (pairˢⁿᶠ t u) = pairˢⁿᶠ (mono⊢ˢⁿᶠ η θ t) (mono⊢ˢⁿᶠ η θ u)
mono⊢ˢⁿᶠ η θ unitˢⁿᶠ = unitˢⁿᶠ
mono⊢ˢⁿᶠ η θ (leftˢⁿᶠ t) = leftˢⁿᶠ (mono⊢ˢⁿᶠ η θ t)
mono⊢ˢⁿᶠ η θ (rightˢⁿᶠ t) = rightˢⁿᶠ (mono⊢ˢⁿᶠ η θ t)
mono⊢ˢⁿᵉ : ∀ {Γ Γ′ Δ Δ′ A} → Γ ⊆ Γ′ → Δ ⊆ Δ′ → Γ ⁏ Δ ⊢ˢⁿᵉ A → Γ′ ⁏ Δ′ ⊢ˢⁿᵉ A
mono⊢ˢⁿᵉ η θ (spˢⁿᵉ i χ y) = spˢⁿᵉ (mono∈ η i) (mono⊢ˢᵖ η θ χ) (mono⊢ᵗᵖ η θ y)
mono⊢ˢⁿᵉ η θ (ᵐspˢⁿᵉ i χ y) = ᵐspˢⁿᵉ (mono∈ θ i) (mono⊢ˢᵖ η θ χ) (mono⊢ᵗᵖ η θ y)
mono⊢ˢᵖ : ∀ {Γ Γ′ Δ Δ′ A C} → Γ ⊆ Γ′ → Δ ⊆ Δ′ → Γ ⁏ Δ ⊢ˢᵖ A ⦙ C → Γ′ ⁏ Δ′ ⊢ˢᵖ A ⦙ C
mono⊢ˢᵖ η θ nilˢᵖ = nilˢᵖ
mono⊢ˢᵖ η θ (appˢᵖ χ u) = appˢᵖ (mono⊢ˢᵖ η θ χ) (mono⊢ˢⁿᶠ η θ u)
mono⊢ˢᵖ η θ (fstˢᵖ χ) = fstˢᵖ (mono⊢ˢᵖ η θ χ)
mono⊢ˢᵖ η θ (sndˢᵖ χ) = sndˢᵖ (mono⊢ˢᵖ η θ χ)
mono⊢ᵗᵖ : ∀ {Γ Γ′ Δ Δ′ A C} → Γ ⊆ Γ′ → Δ ⊆ Δ′ → Γ ⁏ Δ ⊢ᵗᵖ A ⦙ C → Γ′ ⁏ Δ′ ⊢ᵗᵖ A ⦙ C
mono⊢ᵗᵖ η θ nilᵗᵖ = nilᵗᵖ
mono⊢ᵗᵖ η θ (unboxᵗᵖ u) = unboxᵗᵖ (mono⊢ˢⁿᶠ η (keep θ) u)
mono⊢ᵗᵖ η θ boomᵗᵖ = boomᵗᵖ
mono⊢ᵗᵖ η θ (caseᵗᵖ u v) = caseᵗᵖ (mono⊢ˢⁿᶠ (keep η) θ u) (mono⊢ˢⁿᶠ (keep η) θ v)
mono⊢⋆ˢⁿᵉ : ∀ {Ξ Γ Γ′ Δ Δ′} → Γ ⊆ Γ′ → Δ ⊆ Δ′ → Γ ⁏ Δ ⊢⋆ˢⁿᵉ Ξ → Γ′ ⁏ Δ′ ⊢⋆ˢⁿᵉ Ξ
mono⊢⋆ˢⁿᵉ {∅} η θ tt = tt
mono⊢⋆ˢⁿᵉ {Ξ , A} η θ (τ , t) = mono⊢⋆ˢⁿᵉ η θ τ , mono⊢ˢⁿᵉ η θ t
Raw
Sequence.agda
module Sequence {ℓ} (X : Set ℓ) where
open import Common
-- Sequences, or snoc-lists.
infixl 5 _,_
data Seq : Set ℓ where
∅ : Seq
_,_ : Seq → X → Seq
-- Sequence membership, or de Bruijn indices.
infix 3 _∈_
data _∈_ (A : X) : Seq → Set where
top : ∀ {Γ} → A ∈ Γ , A
pop : ∀ {Γ B} → A ∈ Γ → A ∈ Γ , B
i₀ : ∀ {Γ A} → A ∈ Γ , A
i₀ = top
i₁ : ∀ {Γ A B} → A ∈ Γ , A , B
i₁ = pop top
i₂ : ∀ {Γ A B C} → A ∈ Γ , A , B , C
i₂ = pop (pop top)
-- Sequence inclusion, or order-preserving embeddings.
infix 3 _⊆_
data _⊆_ : Seq → Seq → Set where
done : ∅ ⊆ ∅
skip : ∀ {Γ Γ′ A} → Γ ⊆ Γ′ → Γ ⊆ Γ′ , A
keep : ∀ {Γ Γ′ A} → Γ ⊆ Γ′ → Γ , A ⊆ Γ′ , A
-- Sequence-related properties.
zero⊆ : ∀ {Γ} → ∅ ⊆ Γ
zero⊆ {∅} = done
zero⊆ {Γ , A} = skip zero⊆
refl⊆ : ∀ {Γ} → Γ ⊆ Γ
refl⊆ {∅} = done
refl⊆ {Γ , A} = keep refl⊆
trans⊆ : ∀ {Γ Γ′ Γ″} → Γ ⊆ Γ′ → Γ′ ⊆ Γ″ → Γ ⊆ Γ″
trans⊆ η done = η
trans⊆ η (skip η′) = skip (trans⊆ η η′)
trans⊆ (skip η) (keep η′) = skip (trans⊆ η η′)
trans⊆ (keep η) (keep η′) = keep (trans⊆ η η′)
unskip⊆ : ∀ {Γ Γ′ A} → Γ , A ⊆ Γ′ → Γ ⊆ Γ′
unskip⊆ (skip η) = skip (unskip⊆ η)
unskip⊆ (keep η) = skip η
unkeep⊆ : ∀ {Γ Γ′ A} → Γ , A ⊆ Γ′ , A → Γ ⊆ Γ′
unkeep⊆ (skip η) = unskip⊆ η
unkeep⊆ (keep η) = η
weak⊆ : ∀ {Γ A} → Γ ⊆ Γ , A
weak⊆ = skip refl⊆
mono∈ : ∀ {Γ Γ′ A} → Γ ⊆ Γ′ → A ∈ Γ → A ∈ Γ′
mono∈ done ()
mono∈ (skip η) i = pop (mono∈ η i)
mono∈ (keep η) top = top
mono∈ (keep η) (pop i) = pop (mono∈ η i)
reflmono∈ : ∀ {Γ A} → (i : A ∈ Γ) → i ≡ mono∈ refl⊆ i
reflmono∈ top = refl
reflmono∈ (pop i) = cong pop (reflmono∈ i)
transmono∈ : ∀ {Γ Γ′ Γ″ A} → (η : Γ ⊆ Γ′) (η′ : Γ′ ⊆ Γ″) (i : A ∈ Γ) →
mono∈ η′ (mono∈ η i) ≡ mono∈ (trans⊆ η η′) i
transmono∈ done η′ ()
transmono∈ η (skip η′) i = cong pop (transmono∈ η η′ i)
transmono∈ (skip η) (keep η′) i = cong pop (transmono∈ η η′ i)
transmono∈ (keep η) (keep η′) top = refl
transmono∈ (keep η) (keep η′) (pop i) = cong pop (transmono∈ η η′ i)
-- Sequence thinning.
_∖_ : ∀ {A} → (Γ : Seq) → A ∈ Γ → Seq
∅ ∖ ()
(Γ , A) ∖ top = Γ
(Γ , B) ∖ pop i = Γ ∖ i , B
thin⊆ : ∀ {A Γ} → (i : A ∈ Γ) → Γ ∖ i ⊆ Γ
thin⊆ top = weak⊆
thin⊆ (pop i) = keep (thin⊆ i)
-- Decidable equality of sequence membership.
data _=∈_ {Γ A} (i : A ∈ Γ) : ∀ {B} → B ∈ Γ → Set where
same : i =∈ i
diff : ∀ {B} → (j : B ∈ Γ ∖ i) → i =∈ mono∈ (thin⊆ i) j
_≟∈_ : ∀ {Γ A B} → (i : A ∈ Γ) (j : B ∈ Γ) → i =∈ j
top ≟∈ top = same
top ≟∈ pop j rewrite reflmono∈ j = diff j
pop i ≟∈ top = diff top
pop i ≟∈ pop j with i ≟∈ j
pop i ≟∈ pop .i | same = same
pop i ≟∈ pop ._ | diff j = diff (pop j)
-- Sequence concatenation.
_⧺_ : Seq → Seq → Seq
Γ ⧺ ∅ = Γ
Γ ⧺ (Γ′ , A) = Γ ⧺ Γ′ , A
id⧺ : ∀ {Γ} → ∅ ⧺ Γ ≡ Γ
id⧺ {∅} = refl
id⧺ {Γ , A} = cong₂ _,_ id⧺ refl
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment