------------------------------------------------------------------------
-- The Agda standard library
--
-- A larger example for sublists (propositional case):
-- Simply-typed lambda terms with globally unique variables
-- (both bound and free ones).
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Data.List.Relation.Binary.Sublist.Propositional.Example.UniqueBoundVariables (Base : Set) where
open import Relation.Binary.PropositionalEquality.Core
using (_≡_; refl; sym; cong; subst)
open import Relation.Binary.PropositionalEquality.Properties
using (module ≡-Reasoning)
open ≡-Reasoning
open import Data.List.Base using (List; []; _∷_; [_])
open import Data.List.Membership.Propositional using (_∈_)
open import Data.List.Relation.Unary.All using (Null; [])
open import Data.List.Relation.Binary.Sublist.Propositional using
( _⊆_; []; _∷_; _∷ʳ_
; ⊆-refl; ⊆-trans; minimum
; from∈; to∈; lookup
; ⊆-pushoutˡ; RawPushout
; Disjoint; DisjointUnion
; separateˡ; Separation
)
open import Data.List.Relation.Binary.Sublist.Propositional.Properties using
( ∷ˡ⁻
; ⊆-trans-assoc
; from∈∘to∈; from∈∘lookup; lookup-⊆-trans
; ⊆-pushoutˡ-is-wpo
; Disjoint→DisjointUnion; DisjointUnion→Disjoint
; Disjoint-sym; DisjointUnion-inj₁; DisjointUnion-inj₂; DisjointUnion-[]ʳ
; weakenDisjoint; weakenDisjointUnion; shrinkDisjointˡ
; disjoint⇒disjoint-to-union; DisjointUnion-fromAny∘toAny-∷ˡ⁻
; equalize-separators
)
open import Data.Product.Base using (_,_; proj₁; proj₂)
infixr 8 _⇒_
infix 1 _⊢_~_▷_
-- Simple types over a set Base of base types.
data Ty : Set where
base : (o : Base) → Ty
_⇒_ : (a b : Ty) → Ty
-- Typing contexts are lists of types.
Cxt = List Ty
variable
a b : Ty
Γ Δ : Cxt
x y : a ∈ Γ
-- The familiar intrinsically well-typed formulation of STLC
-- where a de Bruijn index x is a pointer into the context.
module DeBruijn where
data Tm (Δ : Cxt) : (a : Ty) → Set where
var : (x : a ∈ Δ) → Tm Δ a
abs : (t : Tm (a ∷ Δ) b) → Tm Δ (a ⇒ b)
app : (t : Tm Δ (a ⇒ b)) (u : Tm Δ a) → Tm Δ b
-- We formalize now intrinsically well-typed STLC with
-- named variables that are globally unique, i.e.,
-- each variable can be bound at most once.
-- List of bound variables of a term.
BVars = List Ty
variable
B : BVars
noBV : Null B
-- There is a single global context Γ of all variables used in the terms.
-- Each list of bound variables B is a sublist of Γ.
variable
β βₜ βᵤ yβ β\y : B ⊆ Γ
-- Named terms are parameterized by a sublist β : B ⊆ Γ of bound variables.
-- Variables outside B can occur as free variables in a term.
--
-- * Variables x do not contain any bound variables (Null B).
--
-- * The bound variables of an application (t u) is the disjoint union
-- of the bound variables βₜ of t and βᵤ of u.
--
-- * The bound variables β of an abstraction λyt is the disjoint union
-- of the single variable y and the bound variables β\y of t.
module UniquelyNamed where
data Tm (β : B ⊆ Γ) : (a : Ty) → Set where
var : (noBV : Null B)
(x : a ∈ Γ)
→ Tm β a
abs : (y : a ∈ Γ)
(y# : DisjointUnion (from∈ y) β\y β)
(t : Tm β\y b)
→ Tm β (a ⇒ b)
app : (t : Tm βₜ (a ⇒ b))
(u : Tm βᵤ a)
(t#u : DisjointUnion βₜ βᵤ β)
→ Tm β b
pattern var! x = var [] x
-- Bound variables β : B ⊆ Γ can be considered in a larger context Γ′
-- obtained by γ : Γ ⊆ Γ′. The embedding β′ : B ⊆ Γ′ is simply the
-- composition of β and γ, and terms can be coerced recursively:
weakenBV : ∀ {Γ B Γ′} {β : B ⊆ Γ} (γ : Γ ⊆ Γ′) →
Tm β a → Tm (⊆-trans β γ) a
weakenBV γ (var noBV x) = var noBV (lookup γ x)
weakenBV γ (app t u t#u) = app (weakenBV γ t) (weakenBV γ u) (weakenDisjointUnion γ t#u)
weakenBV γ (abs y y# t) = abs y′ y′# (weakenBV γ t)
where
y′ = lookup γ y
-- Typing: y′# : DisjointUnion (from∈ y′) (⊆-trans β\y γ) (⊆-trans β γ)
y′# = subst (λ □ → DisjointUnion □ _ _) (sym (from∈∘lookup _ _)) (weakenDisjointUnion γ y#)
-- We bring de Bruijn terms into scope as Exp.
open DeBruijn renaming (Tm to Exp)
open UniquelyNamed
variable
t u : Tm β a
f e : Exp Δ a
-- Relating de Bruijn terms and uniquely named terms.
--
-- The judgement δ ⊢ e ~ β ▷ t relates a de Bruijn term e with
-- potentially free variables δ : Δ ⊆ Γ to a named term t with exact
-- bound variables β : B ⊆ Γ. The intention is to relate exactly the
-- terms with the same meaning.
--
-- The judgement will imply the disjointness of Δ and B.
variable
δ yδ : Δ ⊆ Γ
data _⊢_~_▷_ {Γ Δ : Cxt} (δ : Δ ⊆ Γ) : ∀{a} (e : Exp Δ a) {B} (β : B ⊆ Γ) (t : Tm β a) → Set where
-- Free de Bruijn index x : a ∈ Δ is related to free variable
-- y : a ∈ Γ if δ : Δ ⊆ Γ maps x to y.
var : ∀{y} (δx≡y : lookup δ x ≡ y) (δ#β : Disjoint δ β)
→ δ ⊢ var x ~ β ▷ var! y
-- Unnamed lambda δ ⊢ λ.e is related to named lambda y,β ▷ λy.t
-- if body y,δ ⊢ e is related to body β ▷ t.
abs : (y#δ : DisjointUnion (from∈ y) δ yδ)
→ (y#β : DisjointUnion (from∈ y) β yβ)
→ yδ ⊢ e ~ β ▷ t
→ δ ⊢ abs e ~ yβ ▷ abs y y#β t
-- Application δ ⊢ f e is related to application βₜ,βᵤ ▷ t u
-- if function δ ⊢ f is related to βₜ ▷ t
-- and argument δ ⊢ e is related to βᵤ ▷ u.
app : δ ⊢ f ~ βₜ ▷ t
→ δ ⊢ e ~ βᵤ ▷ u
→ (t#u : DisjointUnion βₜ βᵤ β)
→ δ ⊢ app f e ~ β ▷ app t u t#u
-- A dependent substitution lemma for ~.
-- Trivial, but needed because term equality t : Tm β a ≡ t′ : Tm β′ a is heterogeneous,
-- or, more precisely, indexed by a sublist equality β ≡ β′.
subst~ : ∀ {a Δ Γ B} {δ δ′ : Δ ⊆ Γ} {β β′ : B ⊆ Γ}
{e : Exp Δ a} {t : Tm β a} {t′ : Tm β′ a}
(δ≡δ′ : δ ≡ δ′)
(β≡β′ : β ≡ β′)
(t≡t′ : subst (λ □ → Tm □ a) β≡β′ t ≡ t′) →
δ ⊢ e ~ β ▷ t →
δ′ ⊢ e ~ β′ ▷ t′
subst~ refl refl refl d = d
-- The judgement δ ⊢ e ~ β ▷ t relative to Γ
-- can be transported to a bigger context γ : Γ ⊆ Γ′.
weaken~ : ∀{a Δ B Γ Γ′} {δ : Δ ⊆ Γ} {β : B ⊆ Γ} {e : Exp Δ a} {t : Tm β a} (γ : Γ ⊆ Γ′)
(let δ′ = ⊆-trans δ γ)
(let β′ = ⊆-trans β γ)
(let t′ = weakenBV γ t) →
δ ⊢ e ~ β ▷ t →
δ′ ⊢ e ~ β′ ▷ t′
weaken~ γ (var refl δ#β) = var (lookup-⊆-trans γ _) (weakenDisjoint γ δ#β)
weaken~ γ (abs y#δ y#β d) = abs y′#δ′ y′#β′ (weaken~ γ d)
where
y′#δ′ = subst (λ □ → DisjointUnion □ _ _) (sym (from∈∘lookup _ _)) (weakenDisjointUnion γ y#δ)
y′#β′ = subst (λ □ → DisjointUnion □ _ _) (sym (from∈∘lookup _ _)) (weakenDisjointUnion γ y#β)
weaken~ γ (app dₜ dᵤ t#u) = app (weaken~ γ dₜ) (weaken~ γ dᵤ) (weakenDisjointUnion γ t#u)
-- Lemma: If δ ⊢ e ~ β ▷ t, then
-- the (potentially) free variables δ of the de Bruijn term e
-- are disjoint from the bound variables β of the named term t.
disjoint-fv-bv : δ ⊢ e ~ β ▷ t → Disjoint δ β
disjoint-fv-bv (var _ δ#β) = δ#β
disjoint-fv-bv {β = yβ} (abs y⊎δ y⊎β d) = δ#yβ
where
δ#y = Disjoint-sym (DisjointUnion→Disjoint y⊎δ)
yδ#β = disjoint-fv-bv d
δ⊆yδ,eq = DisjointUnion-inj₂ y⊎δ
δ⊆yδ = proj₁ δ⊆yδ,eq
eq = proj₂ δ⊆yδ,eq
δ#β = subst (λ □ → Disjoint □ _) eq (shrinkDisjointˡ δ⊆yδ yδ#β)
δ#yβ = disjoint⇒disjoint-to-union δ#y δ#β y⊎β
disjoint-fv-bv (app dₜ dᵤ βₜ⊎βᵤ) = disjoint⇒disjoint-to-union δ#βₜ δ#βᵤ βₜ⊎βᵤ
where
δ#βₜ = disjoint-fv-bv dₜ
δ#βᵤ = disjoint-fv-bv dᵤ
-- Translating de Bruijn terms to uniquely named terms.
--
-- Given a de Bruijn term Δ ⊢ e : a, we seek to produce a named term
-- β ▷ t : a that is related to the de Bruijn term. On the way, we have
-- to compute the global context Γ that hosts all free and bound
-- variables of t.
-- Record (NamedOf e) collects all the outputs of the translation of e.
record NamedOf (e : Exp Δ a) : Set where
constructor mkNamedOf
field
{glob} : Cxt -- Γ
emb : Δ ⊆ glob -- δ : Δ ⊆ Γ
{bv} : BVars -- B
bound : bv ⊆ glob -- β : B ⊆ Γ
{tm} : Tm bound a -- t : Tm β a
relate : emb ⊢ e ~ bound ▷ tm -- δ ⊢ e ~ β ▷ t
-- The translation.
dB→Named : (e : Exp Δ a) → NamedOf e
-- For the translation of a variable x : a ∈ Δ, we can pick Γ := Δ and B := [].
-- Δ and B are obviously disjoint subsets of Γ.
dB→Named (var x) = record
{ emb = ⊆-refl -- Γ := Δ
; bound = minimum _ -- no bound variables
; relate = var refl (DisjointUnion→Disjoint DisjointUnion-[]ʳ)
}
-- For the translation of an abstraction
--
-- abs (t : Exp (a ∷ Δ) b) : Exp Δ (a ⇒ b)
--
-- we recursively have Γ, B and β : B ⊆ Γ with z,δ : (a ∷ Δ) ⊆ Γ
-- and know that B # a∷Δ.
--
-- We keep Γ and produce embedding δ : Δ ⊆ Γ and bound variables z ⊎ β.
dB→Named {Δ = Δ} {a = a ⇒ b} (abs e) with dB→Named e
... | record{ glob = Γ; emb = zδ; bound = β; relate = d } =
record
{ glob = Γ
; emb = δ̇
; bound = proj₁ (proj₂ z⊎β)
; relate = abs [a]⊆Γ⊎δ (proj₂ (proj₂ z⊎β)) d
}
where
-- Typings:
-- zδ : a ∷ Δ ⊆ Γ
-- β : bv ⊆ Γ
zδ#β = disjoint-fv-bv d
z : a ∈ Γ
z = to∈ zδ
[a]⊆Γ = from∈ z
δ̇ = ∷ˡ⁻ zδ
[a]⊆Γ⊎δ = DisjointUnion-fromAny∘toAny-∷ˡ⁻ zδ
[a]⊆aΔ : [ a ] ⊆ (a ∷ Δ)
[a]⊆aΔ = refl ∷ minimum _
eq : ⊆-trans [a]⊆aΔ zδ ≡ [a]⊆Γ
eq = sym (from∈∘to∈ _)
z#β : Disjoint [a]⊆Γ β
z#β = subst (λ □ → Disjoint □ β) eq (shrinkDisjointˡ [a]⊆aΔ zδ#β)
z⊎β = Disjoint→DisjointUnion z#β
-- For the translation of an application (f e) we have by induction
-- hypothesis two independent extensions δ₁ : Δ ⊆ Γ₁ and δ₂ : Δ ⊆ Γ₂
-- and two bound variable lists β₁ : B₁ ⊆ Γ₁ and β₂ : B₂ ⊆ Γ₂.
-- We need to find a common global context Γ such that
--
-- (a) δ : Δ ⊆ Γ and
-- (b) the bound variables embed disjointly as β₁″ : B₁ ⊆ Γ and β₂″ : B₂ ⊆ Γ.
--
-- (a) δ is (eventually) found via a weak pushout of δ₁ and δ₂, giving
-- ϕ₁ : Γ₁ ⊆ Γ₁₂ and ϕ₂ : Γ₂ ⊆ Γ₁₂.
--
-- (b) The bound variable embeddings
--
-- β₁′ = β₁ϕ₁ : B₁ ⊆ Γ₁₂ and
-- β₂′ = β₂ϕ₂ : B₂ ⊆ Γ₁₂ and
--
-- may be overlapping, but we can separate them by enlarging the global
-- context to Γ with two embeddings
--
-- γ₁ : Γ₁₂ ⊆ Γ
-- γ₂ : Γ₁₂ ⊆ Γ
--
-- such that
--
-- β₁″ = β₁′γ₁ : B₁ ⊆ Γ
-- β₂″ = β₂′γ₂ : B₂ ⊆ Γ
--
-- are disjoint. Since Δ is disjoint to both B₁ and B₂ we have equality of
--
-- δ₁ϕ₁γ₁ : Δ ⊆ Γ
-- δ₂ϕ₂γ₂ : Δ ⊆ Γ
--
-- Thus, we can return either of them as δ.
dB→Named (app f e) with dB→Named f | dB→Named e
... | mkNamedOf {Γ₁} δ₁ β₁ {t} d₁ | mkNamedOf {Γ₂} δ₂ β₂ {u} d₂ =
mkNamedOf δ̇ β̇ (app d₁″ d₂″ β₁″⊎β₂″)
where
-- Disjointness of δᵢ and βᵢ from induction hypotheses.
δ₁#β₁ = disjoint-fv-bv d₁
δ₂#β₂ = disjoint-fv-bv d₂
-- join δ₁ and δ₂ via weak pushout
po = ⊆-pushoutˡ δ₁ δ₂
Γ₁₂ = RawPushout.upperBound po
ϕ₁ = RawPushout.leg₁ po
ϕ₂ = RawPushout.leg₂ po
δ₁′ = ⊆-trans δ₁ ϕ₁
δ₂′ = ⊆-trans δ₂ ϕ₂
β₁′ = ⊆-trans β₁ ϕ₁
β₂′ = ⊆-trans β₂ ϕ₂
δ₁′#β₁′ : Disjoint δ₁′ β₁′
δ₁′#β₁′ = weakenDisjoint ϕ₁ δ₁#β₁
δ₂′#β₂′ : Disjoint δ₂′ β₂′
δ₂′#β₂′ = weakenDisjoint ϕ₂ δ₂#β₂
δ₁′≡δ₂′ : δ₁′ ≡ δ₂′
δ₁′≡δ₂′ = ⊆-pushoutˡ-is-wpo δ₁ δ₂
δ₂′#β₁′ : Disjoint δ₂′ β₁′
δ₂′#β₁′ = subst (λ □ → Disjoint □ β₁′) δ₁′≡δ₂′ δ₁′#β₁′
-- separate β₁ and β₂
sep : Separation β₁′ β₂′
sep = separateˡ β₁′ β₂′
γ₁ = Separation.separator₁ sep
γ₂ = Separation.separator₂ sep
β₁″ = Separation.separated₁ sep
β₂″ = Separation.separated₂ sep
-- produce their disjoint union
uni = Disjoint→DisjointUnion (Separation.disjoint sep)
β̇ = proj₁ (proj₂ uni)
β₁″⊎β₂″ : DisjointUnion β₁″ β₂″ β̇
β₁″⊎β₂″ = proj₂ (proj₂ uni)
ι₁ = DisjointUnion-inj₁ β₁″⊎β₂″
ι₂ = DisjointUnion-inj₂ β₁″⊎β₂″
-- after separation, the FVs are still disjoint from the BVs.
δ₁″ = ⊆-trans δ₂′ γ₁
δ₂″ = ⊆-trans δ₂′ γ₂
δ₁″≡δ₂″ : δ₁″ ≡ δ₂″
δ₁″≡δ₂″ = equalize-separators δ₂′#β₁′ δ₂′#β₂′
δ₁″#β₁″ : Disjoint δ₁″ β₁″
δ₁″#β₁″ = weakenDisjoint γ₁ δ₂′#β₁′
δ₂″#β₂″ : Disjoint δ₂″ β₂″
δ₂″#β₂″ = weakenDisjoint γ₂ δ₂′#β₂′
δ̇ = δ₂″
δ₂″#β₁″ : Disjoint δ₂″ β₁″
δ₂″#β₁″ = subst (λ □ → Disjoint □ β₁″) δ₁″≡δ₂″ δ₁″#β₁″
δ̇#β̇ : Disjoint δ̇ β̇
δ̇#β̇ = disjoint⇒disjoint-to-union δ₂″#β₁″ δ₂″#β₂″ β₁″⊎β₂″
-- Combined weakening from Γᵢ to Γ
γ₁′ = ⊆-trans ϕ₁ γ₁
γ₂′ = ⊆-trans ϕ₂ γ₂
-- Weakening and converting the first derivation.
d₁′ : ⊆-trans δ₁ γ₁′ ⊢ f ~ ⊆-trans β₁ γ₁′ ▷ weakenBV γ₁′ t
d₁′ = weaken~ γ₁′ d₁
δ₁≤δ̇ : ⊆-trans δ₁ γ₁′ ≡ ⊆-trans δ₂′ γ₂
δ₁≤δ̇ = begin
⊆-trans δ₁ γ₁′ ≡⟨ ⊆-trans-assoc ⟩
⊆-trans δ₁′ γ₁ ≡⟨ cong (λ □ → ⊆-trans □ γ₁) δ₁′≡δ₂′ ⟩
⊆-trans δ₂′ γ₁ ≡⟨⟩
δ₁″ ≡⟨ δ₁″≡δ₂″ ⟩
δ₂″ ≡⟨⟩
δ̇ ∎
β₁≤β₁″ : ⊆-trans β₁ γ₁′ ≡ β₁″
β₁≤β₁″ = ⊆-trans-assoc
d₁″ : δ̇ ⊢ f ~ β₁″ ▷ subst (λ □ → Tm □ _) β₁≤β₁″ (weakenBV γ₁′ t)
d₁″ = subst~ δ₁≤δ̇ β₁≤β₁″ refl d₁′
-- Weakening and converting the second derivation.
d₂′ : ⊆-trans δ₂ γ₂′ ⊢ e ~ ⊆-trans β₂ γ₂′ ▷ weakenBV γ₂′ u
d₂′ = weaken~ γ₂′ d₂
β₂≤β₂″ : ⊆-trans β₂ γ₂′ ≡ β₂″
β₂≤β₂″ = ⊆-trans-assoc
δ₂≤δ̇ : ⊆-trans δ₂ γ₂′ ≡ δ̇
δ₂≤δ̇ = ⊆-trans-assoc
d₂″ : δ̇ ⊢ e ~ β₂″ ▷ subst (λ □ → Tm □ _) β₂≤β₂″ (weakenBV γ₂′ u)
d₂″ = subst~ δ₂≤δ̇ β₂≤β₂″ refl d₂′