Agda formalization of the reduction relation for explicit substitutions in https://dl.acm.org/doi/pdf/10.1145/3498669

CS.agda

-- A fine-grained computational interpretation of Girard's intuitionistic proof-nets
-- by Delia Kesner
-- https://dl.acm.org/doi/pdf/10.1145/3498669
--
-- - Definition of the reduction relation
module CS where

open import Data.Empty
open import Data.Sum
open import Function.Base
open import Relation.Nullary using (contradiction)
open import Relation.Binary.PropositionalEquality.Core

data Scope : Set where
  ∅ : Scope
  S_ : Scope → Scope

variable Γ Γ′ : Scope

data Thinning : Scope → Scope → Set where
  ∅ : Thinning ∅ ∅
  S_ : Thinning Γ Γ′ → Thinning Γ (S Γ′)
  both : Thinning Γ Γ′ → Thinning (S Γ) (S Γ′)

idᵀ : Thinning Γ Γ
idᵀ {Γ = ∅} = ∅
idᵀ {Γ = S Γ} = both idᵀ

predᴸ : Thinning (S Γ) Γ′ → Thinning Γ Γ′
predᴸ (S t) = S predᴸ t
predᴸ (both t) = S t 

data Var : Scope → Set where
  O : {Γ : Scope} → Var (S Γ)
  S_ : {Γ : Scope} → Var Γ → Var (S Γ)

data Term (Γ : Scope) : Set where
  `_ : Var Γ → Term Γ
  ƛ_ : Term (S Γ) → Term Γ
  _·_ : Term Γ → Term Γ → Term Γ
  _[_↦_] : Term (S Γ) → Var (S Γ) → Term Γ → Term Γ

thinⱽ : Thinning Γ Γ′ → Var Γ → Var Γ′
thinⱽ ∅ ()
thinⱽ (S τ) x = S thinⱽ τ x
thinⱽ (both τ) O = O
thinⱽ (both τ) (S x) = S thinⱽ τ x

thin : Thinning Γ Γ′ → Term Γ → Term Γ′
thin τ (` x) = ` thinⱽ τ x
thin τ (ƛ t) = ƛ thin (both τ) t
thin τ (t · t₁) = thin τ t · thin τ t₁
thin τ (t [ x ↦ t₁ ]) = thin (both τ) t [ thinⱽ (both τ) x ↦ thin τ t₁ ]

V→T : Var (S Γ) → Thinning Γ (S Γ)
V→T O = S idᵀ
V→T {Γ = S Γ} (S y) = both (V→T y)

data ArgContext (Γ : Scope) : Set where
  _·□ : Term Γ → ArgContext Γ
  _[_↦□] : Term (S Γ) → Var (S Γ) → ArgContext Γ

_⟨_⟩ᴬ : {Γ : Scope} → ArgContext Γ → Term Γ → Term Γ
(u ·□) ⟨ t ⟩ᴬ = u · t
(u [ y ↦□]) ⟨ t ⟩ᴬ = u [ y ↦ t ]

data HeadContext (Γ : Scope) : Scope → Set where
  □ : HeadContext Γ Γ
  ƛ_ : {Γ′ : Scope} → HeadContext (S Γ) Γ′ → HeadContext Γ Γ′
  _·_ : {Γ′ : Scope} → HeadContext Γ Γ′ → Term Γ → HeadContext Γ Γ′
  _[_↦_] : {Γ′ : Scope} →
    HeadContext (S Γ) Γ′ → Var (S Γ) → Term Γ → HeadContext Γ Γ′

infix 9 _·_
infix 9 ƛ_

_⟨_⟩ᴴ : {Γ Γ′ : Scope} → HeadContext Γ Γ′ → Term Γ′ → Term Γ
□ ⟨ t ⟩ᴴ = t
(ƛ H) ⟨ t ⟩ᴴ = ƛ H ⟨ t ⟩ᴴ
(H · u) ⟨ t ⟩ᴴ = H ⟨ t ⟩ᴴ · u
(H [ y ↦ u ]) ⟨ t ⟩ᴴ = H ⟨ t ⟩ᴴ [ y ↦ u ]

H→T : HeadContext Γ Γ′ → Thinning Γ Γ′
H→T □ = idᵀ
H→T (ƛ H) = predᴸ (H→T H)
H→T (H · x) = H→T H
H→T (H [ x ↦ x₁ ]) = predᴸ (H→T H)

_⟪_⟫ᴴ : {Γ Γ′ : Scope} → HeadContext Γ Γ′ → Term Γ → Term Γ
H ⟪ t ⟫ᴴ = H ⟨ thin (H→T H) t ⟩ᴴ

data ListContext (Γ : Scope) : Scope → Set where
  □ : ListContext Γ Γ
  _[_↦_] : {Γ′ : Scope} →
    ListContext (S Γ) Γ′ → Var (S Γ) → Term Γ → ListContext Γ Γ′

_⟨_⟩ᴸ : {Γ Γ′ : Scope} → ListContext Γ Γ′ → Term Γ′ → Term Γ
□ ⟨ t ⟩ᴸ = t
(H [ y ↦ u ]) ⟨ t ⟩ᴸ = H ⟨ t ⟩ᴸ [ y ↦ u ]

L→T : ListContext Γ Γ′ → Thinning Γ Γ′
L→T □ = idᵀ
L→T (L [ x ↦ t ]) = predᴸ (L→T L)

infix 9 `_
infix 1 _∉free_ _∉freeᴴ_

data _∉free_ (x : Var Γ) : Term Γ → Set where
  `_ : {y : Var Γ} → x ≢ y → x ∉free ` y
  ƛ_ : {t : Term (S Γ)} → (S x) ∉free t → x ∉free ƛ t
  _·_ : {t u : Term Γ} → x ∉free t → x ∉free u → x ∉free (t · u)
  _[_↦_] : {t : Term (S Γ)} {u : Term Γ} →
    {y : Var (S Γ)} →
    thinⱽ (V→T y) x ∉free t →
    thinⱽ (V→T y) x ≢ y →
    x ∉free u →
    x ∉free t [ y ↦ u ]

infix 1 _∈free_

data _∈free_ (x : Var Γ) : Term Γ → Set where
  `_ : x ∈free ` x
  ƛ_ : {t : Term (S Γ)} → (S x) ∈free t → x ∈free ƛ t
  _·_ : {t u : Term Γ} →
    (x ∈free t) ⊎ (x ∈free u) → x ∈free (t · u)
  _[_↦_] : {t : Term (S Γ)} {u : Term Γ} →
    {y : Var (S Γ)} →
    thinⱽ (V→T y) x ∈free t →
    thinⱽ (V→T y) x ≢ y →
    x ∈free u →
    x ∈free t [ y ↦ u ]

infix 1 _∉freeᴬ_ _∈freeᴬ_

data _∉freeᴬ_ (x : Var Γ) : ArgContext Γ → Set where
  _·□ : {t : Term Γ} → x ∉free t → x ∉freeᴬ (t ·□)
  _[_↦□] : {t : Term (S Γ)} {u : Term Γ} →
    {y : Var (S Γ)} →
    thinⱽ (V→T y) x ∉free t →
    thinⱽ (V→T y) x ≢ y →
    x ∉freeᴬ t [ y ↦□]

data _∈freeᴬ_ (x : Var Γ) : ArgContext Γ → Set where
  _·□ : {t : Term Γ} → x ∈free t → x ∈freeᴬ (t ·□)
  _[_↦□] : {t : Term (S Γ)} {u : Term Γ} →
    {y : Var (S Γ)} →
    thinⱽ (V→T y) x ∈free t →
    thinⱽ (V→T y) x ≢ y →
    x ∈freeᴬ t [ y ↦□]

data _∉freeᴴ_ (x : Var Γ) : HeadContext Γ Γ′ → Set where
  □ : x ∉freeᴴ □
  ƛ_ : {H : HeadContext (S Γ) Γ′} → (S x) ∉freeᴴ H → x ∉freeᴴ ƛ H
  _·_ : {H : HeadContext Γ Γ′} {u : Term Γ} →
    x ∉freeᴴ H → x ∉free u → x ∉freeᴴ (H · u)
  _[_↦_] : {H : HeadContext (S Γ) Γ′} {u : Term Γ} →
    {y : Var (S Γ)} →
    thinⱽ (V→T y) x ∉freeᴴ H →
    thinⱽ (V→T y) x ≢ y →
    x ∉free u →
    x ∉freeᴴ H [ y ↦ u ]

clearⱽ : (y : Var (S Γ)) → {x : Var (S Γ)} → x ≢ y → Var Γ
clearⱽ O {x = O} x≢y = contradiction refl x≢y
clearⱽ (S y) {x = O} x≢y = y
clearⱽ {Γ = S _} O {x = S x} x≢y = O
clearⱽ {Γ = S _} (S y) {x = S x} x≢y = S clearⱽ y (x≢y ∘ cong S_)

clear : (t : Term (S Γ)) → {x : Var (S Γ)} → x ∉free t → Term Γ
clear (` y) (` x≢y) = ` clearⱽ y x≢y
clear (ƛ t) (ƛ ∉t) = ƛ clear t ∉t
clear (t · t₁) (∉t · ∉t₁) = clear t ∉t · clear t₁ ∉t₁
clear (t [ y ↦ u ]) (∉t [ x≢y ↦ ∉u ]) = clear t ∉t [ clearⱽ y x≢y ↦ clear u ∉u ]

clearᴴ : (H : HeadContext (S Γ) (S Γ′)) → {x : Var (S Γ)} →
  x ∉freeᴴ H →
  HeadContext Γ Γ′
clearᴴ □ □ = □
clearᴴ (ƛ H) (ƛ ∉H) = ƛ clearᴴ H ∉H
clearᴴ (H · t₁) (∉H · ∉t₁) = clearᴴ H ∉H · clear t₁ ∉t₁
clearᴴ (H [ y ↦ u ]) (∉H [ x≢y ↦ ∉u ]) = clearᴴ H ∉H [ clearⱽ y x≢y ↦ clear u ∉u ]

clearᴬ : (A : ArgContext (S Γ)) {x : Var (S Γ)} →
  x ∉freeᴬ A →
  ArgContext Γ
clearᴬ (t ·□) (∉t ·□) = clear t ∉t ·□
clearᴬ (t [ y ↦□]) (∉t [ x≢y ↦□]) = clear t ∉t [ clearⱽ y x≢y ↦□]

injective-S : {x y : Var Γ} → S x ≡ S y → x ≡ y
injective-S refl = refl

thin≢ : (x : Var Γ) (y : Var (S Γ)) → thinⱽ (V→T y) x ≢ y
thin≢ (S x) (S y) = thin≢ x y ∘ injective-S

_[_↦_]ᴬ : ArgContext (S Γ) → Var (S Γ) → Term Γ → ArgContext Γ
(t ·□) [ x ↦ u ]ᴬ = t [ x ↦ u ] ·□
(t [ y ↦□]) [ x ↦ u ]ᴬ =
  let y′ = (clearⱽ y (thin≢ x y)) in
  t [ thinⱽ (V→T y) x ↦ thin (V→T y′) u ] [ y′ ↦□]

infix 1 _↠_

data _↠_ {Γ : Scope} : Term Γ → Term Γ → Set where
  db : {Γ′ : Scope} {L : ListContext Γ Γ′} {t : Term (S Γ′)} {u : Term Γ} →
    L ⟨ ƛ t ⟩ᴸ · u ↠ L ⟨ t [ O ↦ thin (L→T L) u ] ⟩ᴸ
  gc : {t : Term (S Γ)} {x : Var (S Γ)} {u : Term Γ} →
    (x∉t : x ∉free t) →
    t [ x ↦ u ] ↠ clear t x∉t
  hs : {H : HeadContext (S Γ) (S Γ′)} {x : Var (S Γ)} {u : Term Γ} →
    (x∉H : x ∉freeᴴ H) →
    H ⟪ ` x ⟫ᴴ [ x ↦ u ] ↠ clearᴴ H x∉H ⟪ u ⟫ᴴ
  arg : {H : HeadContext (S Γ) (S Γ′)} {A : ArgContext (S Γ′)} {t : Term (S Γ′)}
        {x : Var (S Γ)} {u : Term Γ} →
    (x∉H : x ∉freeᴴ H) →
    (let x′ = thinⱽ (H→T H) x)
    (x∈t : x′ ∈free t) →
    (x∉A : x′ ∉freeᴬ A) →
    H ⟨ A ⟨ t ⟩ᴬ ⟩ᴴ [ x ↦ u ] ↠
    clearᴴ H x∉H ⟨ clearᴬ A x∉A ⟨ t [ x′ ↦ thin (H→T (clearᴴ H x∉H)) u ] ⟩ᴬ ⟩ᴴ
  dup : {H : HeadContext (S Γ) (S Γ′)} {A : ArgContext (S Γ′)} {t : Term (S Γ′)}
        {x : Var (S Γ)} {u : Term Γ} →
    (x∉H : x ∉freeᴴ H) →
    (let x′ = thinⱽ (H→T H) x)
    (x∈t : x′ ∈free t) →
    (x∈A : x′ ∈freeᴬ A) →
    H ⟨ A ⟨ t ⟩ᴬ ⟩ᴴ [ x ↦ u ] ↠
    let H′ = clearᴴ H x∉H in
    H′ ⟨ A [ thinⱽ (H→T H) x ↦ thin (H→T H′) u ]ᴬ
           ⟨ t [ x′ ↦ thin (H→T H′) u ] ⟩ᴬ ⟩ᴴ