https://github.com/YouyouCong/fscd21-artifact
Tip revision: c88b251d074865dd2d22d7cd755a2ffa40c42891 authored by Youyou Cong on 02 May 2021, 10:36:52 UTC
Revert "rename variables"
Revert "rename variables"
Tip revision: c88b251
lambdaf-red.agda
-- Reduction of λF
module LambdaF-Red where
open import LambdaF
open import Data.Nat using (ℕ; zero; suc; _+_)
open import Data.Bool using (true; false; if_then_else_) renaming (Bool to 𝔹)
open import Data.String using (String)
open import Relation.Binary.PropositionalEquality
-- Substitution
data SubstVal {var : Ty → Set} : {τ₁ τ₂ : Ty} →
(var τ₁ → Val[ var ] τ₂) →
Val[ var ] τ₁ →
Val[ var ] τ₂ → Set
data Subst {var : Ty → Set} : {τ₁ τ₂ τ₃ τ₄ : Ty} {μα μβ : Tr} →
(var τ₁ → Exp[ var ] τ₂ ⟨ μα ⟩ τ₃ ⟨ μβ ⟩ τ₄) →
Val[ var ] τ₁ →
Exp[ var ] τ₂ ⟨ μα ⟩ τ₃ ⟨ μβ ⟩ τ₄ → Set
data SubstVal {var} where
sVar= : {τ : Ty} {v : Val[ var ] τ} →
SubstVal (λ x → Var x) v v
sVar≠ : {τ₁ τ₂ : Ty} {v : Val[ var ] τ₂} {x : var τ₁} →
SubstVal (λ y → Var x) v (Var x)
sNum : {τ : Ty} {n : ℕ}
{v : Val[ var ] τ} →
SubstVal (λ x → Num n) v (Num n)
sBol : {τ : Ty} {b : 𝔹}
{v : Val[ var ] τ} →
SubstVal (λ x → Bol b) v (Bol b)
sStr : {τ : Ty} {s : String}
{v : Val[ var ] τ} →
SubstVal (λ x → Str s) v (Str s)
sAbs : {τ τ₁ τ₂ α β γ : Ty} {μα μβ : Tr}
{e : var τ₁ → var τ → Exp[ var ] τ₂ ⟨ μα ⟩ α ⟨ μβ ⟩ β}
{v : Val[ var ] τ₁}
{e' : var τ → Exp[ var ] τ₂ ⟨ μα ⟩ α ⟨ μβ ⟩ β} →
((x : var τ) → Subst (λ y → (e y) x) v (e' x)) →
SubstVal (λ y → Abs (e y)) v (Abs e')
data Subst {var} where
sVal : {τ τ₁ τ₃ : Ty} {μα : Tr}
{v₁ : var τ → Val[ var ] τ₁}
{v : Val[ var ] τ}
{v₁' : Val[ var ] τ₁} →
SubstVal v₁ v v₁' →
Subst {τ₃ = τ₃} {μα = μα} (λ y → Val (v₁ y)) v (Val v₁')
sApp : {τ τ₁ τ₂ α β γ δ : Ty} {μα μβ μγ μδ : Tr}
{e₁ : var τ → Exp[ var ] (τ₁ ⇒ τ₂ ⟨ μα ⟩ α ⟨ μβ ⟩ β) ⟨ μγ ⟩ γ ⟨ μδ ⟩ δ}
{e₂ : var τ → Exp[ var ] τ₁ ⟨ μβ ⟩ β ⟨ μγ ⟩ γ}
{v : Val[ var ] τ}
{e₁' : Exp[ var ] (τ₁ ⇒ τ₂ ⟨ μα ⟩ α ⟨ μβ ⟩ β) ⟨ μγ ⟩ γ ⟨ μδ ⟩ δ}
{e₂' : Exp[ var ] τ₁ ⟨ μβ ⟩ β ⟨ μγ ⟩ γ} →
Subst e₁ v e₁' → Subst e₂ v e₂' →
Subst (λ y → App (e₁ y) (e₂ y)) v (App e₁' e₂')
sPlu : {τ α β γ : Ty} {μα μβ μγ : Tr}
{e₁ : var τ → Exp[ var ] Nat ⟨ μβ ⟩ β ⟨ μγ ⟩ γ}
{e₂ : var τ → Exp[ var ] Nat ⟨ μα ⟩ α ⟨ μβ ⟩ β}
{v : Val[ var ] τ}
{e₁' : Exp[ var ] Nat ⟨ μβ ⟩ β ⟨ μγ ⟩ γ }
{e₂' : Exp[ var ] Nat ⟨ μα ⟩ α ⟨ μβ ⟩ β } →
Subst e₁ v e₁' → Subst e₂ v e₂' →
Subst (λ y → Plus (e₁ y) (e₂ y)) v (Plus e₁' e₂')
sIs0 : {τ α β : Ty} {μα μβ : Tr}
{e : var τ → Exp[ var ] Nat ⟨ μα ⟩ α ⟨ μβ ⟩ β}
{v : Val[ var ] τ}
{e' : Exp[ var ] Nat ⟨ μα ⟩ α ⟨ μβ ⟩ β } →
Subst e v e' →
Subst (λ y → Is0 (e y)) v (Is0 e')
sB2S : {τ α β : Ty} {μα μβ : Tr}
{e : var τ → Exp[ var ] Bool ⟨ μα ⟩ α ⟨ μβ ⟩ β}
{v : Val[ var ] τ}
{e' : Exp[ var ] Bool ⟨ μα ⟩ α ⟨ μβ ⟩ β} →
Subst e v e' →
Subst (λ y → B2S (e y)) v (B2S e')
sCon : {τ τ₁ τ₁' τ₃ α β γ γ' : Ty} {μ₀ μ₁ μ₂ μᵢ μα μβ : Tr} →
{e : var τ₃ →
var (τ ⇒ τ₁ ⟨ μ₁ ⟩ τ₁' ⟨ μ₂ ⟩ α) →
Exp[ var ] γ ⟨ μᵢ ⟩ γ' ⟨ ● ⟩ β}
{v : Val[ var ] τ₃}
{e' : var (τ ⇒ τ₁ ⟨ μ₁ ⟩ τ₁' ⟨ μ₂ ⟩ α) →
Exp[ var ] γ ⟨ μᵢ ⟩ γ' ⟨ ● ⟩ β}
{x₁ : is-id-trail γ μᵢ γ'}
{x₂ : compatible (τ₁ ⇒⟨ μ₁ ⟩ τ₁') μ₂ μ₀}
{x₃ : compatible μβ μ₀ μα} →
((k : var (τ ⇒ τ₁ ⟨ μ₁ ⟩ τ₁' ⟨ μ₂ ⟩ α)) →
Subst (λ y → (e y) k) v ((e' k))) →
Subst (λ y → Control x₁ x₂ x₃ (e y))
v
(Control x₁ x₂ x₃ e')
sPro : {τ τ₃ β β' γ : Ty} {μᵢ μα : Tr}
{e : var τ → Exp[ var ] β ⟨ μᵢ ⟩ β' ⟨ ● ⟩ γ}
{v : Val[ var ] τ}
{e' : Exp[ var ] β ⟨ μᵢ ⟩ β' ⟨ ● ⟩ γ}
{x : is-id-trail β μᵢ β'} →
Subst e v e' →
Subst {τ₃ = τ₃} {μα = μα} (λ y → Prompt x (e y)) v
(Prompt x e')
-- Frames
data Fr[_,_⟨_⟩_⟨_⟩_]_⟨_⟩_⟨_⟩_ (var : Ty → Set)
: Ty → Tr → Ty → Tr → Ty → Ty → Tr → Ty → Tr → Ty → Set where
App₁ : {τ₁ τ₂ α β γ δ : Ty} {μα μβ μγ μδ : Tr} →
(e₂ : Exp[ var ] τ₁ ⟨ μβ ⟩ β ⟨ μγ ⟩ γ) →
Fr[ var , (τ₁ ⇒ τ₂ ⟨ μα ⟩ α ⟨ μβ ⟩ β) ⟨ μγ ⟩ γ ⟨ μδ ⟩ δ ]
τ₂ ⟨ μα ⟩ α ⟨ μδ ⟩ δ
App₂ : {τ₁ τ₂ α β γ : Ty} {μα μβ μγ : Tr} →
(v₁ : Val[ var ] (τ₁ ⇒ τ₂ ⟨ μα ⟩ α ⟨ μβ ⟩ β)) →
Fr[ var , τ₁ ⟨ μβ ⟩ β ⟨ μγ ⟩ γ ]
τ₂ ⟨ μα ⟩ α ⟨ μγ ⟩ γ
Plus₁ : {α β γ : Ty} {μα μβ μγ : Tr} →
(e₂ : Exp[ var ] Nat ⟨ μα ⟩ α ⟨ μβ ⟩ β) →
Fr[ var , Nat ⟨ μβ ⟩ β ⟨ μγ ⟩ γ ] Nat ⟨ μα ⟩ α ⟨ μγ ⟩ γ
Plus₂ : {α γ : Ty} {μα μγ : Tr} →
(v₁ : Val[ var ] Nat) →
Fr[ var , Nat ⟨ μα ⟩ α ⟨ μγ ⟩ γ ] Nat ⟨ μα ⟩ α ⟨ μγ ⟩ γ
Is0 : {α β : Ty} {μα μβ : Tr} →
Fr[ var , Nat ⟨ μα ⟩ α ⟨ μβ ⟩ β ] Bool ⟨ μα ⟩ α ⟨ μβ ⟩ β
B2S : {α β : Ty} {μα μβ : Tr} →
Fr[ var , Bool ⟨ μα ⟩ α ⟨ μβ ⟩ β ] Str ⟨ μα ⟩ α ⟨ μβ ⟩ β
Pro : {τ α β β' : Ty} {μᵢ μα : Tr} →
(is-id-trail β μᵢ β') →
Fr[ var , β ⟨ μᵢ ⟩ β' ⟨ ● ⟩ τ ] τ ⟨ μα ⟩ α ⟨ μα ⟩ α
Fr-plug : {var : Ty → Set}
{τ₁ τ₂ τ₃ τ₄ τ₅ τ₆ : Ty} {μα μβ μγ μδ : Tr} →
Fr[ var , τ₂ ⟨ μα ⟩ τ₄ ⟨ μβ ⟩ τ₅ ] τ₁ ⟨ μγ ⟩ τ₃ ⟨ μδ ⟩ τ₆ →
Exp[ var ] τ₂ ⟨ μα ⟩ τ₄ ⟨ μβ ⟩ τ₅ →
Exp[ var ] τ₁ ⟨ μγ ⟩ τ₃ ⟨ μδ ⟩ τ₆
Fr-plug (App₁ e₂) e₁ = App e₁ e₂
Fr-plug (App₂ v₁) e₂ = App (Val v₁) e₂
Fr-plug (Plus₁ e₂) e₁ = Plus e₁ e₂
Fr-plug (Plus₂ v₁) e₂ = Plus (Val v₁) e₂
Fr-plug Is0 e = Is0 e
Fr-plug B2S e = B2S e
Fr-plug {τ₁ = τ₁} {τ₂ = τ₂} {τ₃ = τ₃} {τ₄ = τ₄} {μα = μα} {μγ = μγ} (Pro x) e =
Prompt x e
-- Pure frames
data pFr[_,_⟨_⟩_⟨_⟩_]_⟨_⟩_⟨_⟩_ (var : Ty → Set)
: Ty → Tr → Ty → Tr → Ty → Ty → Tr → Ty → Tr → Ty → Set where
App₁ : {τ₁ τ₂ α β γ δ : Ty} {μα μβ μγ μδ : Tr} →
(e₂ : Exp[ var ] τ₁ ⟨ μβ ⟩ β ⟨ μγ ⟩ γ) →
pFr[ var , (τ₁ ⇒ τ₂ ⟨ μα ⟩ α ⟨ μβ ⟩ β) ⟨ μγ ⟩ γ ⟨ μδ ⟩ δ ]
τ₂ ⟨ μα ⟩ α ⟨ μδ ⟩ δ
App₂ : {τ₁ τ₂ α β γ : Ty} {μα μβ μγ : Tr} →
(v₁ : Val[ var ] (τ₁ ⇒ τ₂ ⟨ μα ⟩ α ⟨ μβ ⟩ β)) →
pFr[ var , τ₁ ⟨ μβ ⟩ β ⟨ μγ ⟩ γ ]
τ₂ ⟨ μα ⟩ α ⟨ μγ ⟩ γ
Plus₁ : {α β γ : Ty} {μα μβ μγ : Tr} →
(e₂ : Exp[ var ] Nat ⟨ μα ⟩ α ⟨ μβ ⟩ β) →
pFr[ var , Nat ⟨ μβ ⟩ β ⟨ μγ ⟩ γ ] Nat ⟨ μα ⟩ α ⟨ μγ ⟩ γ
Plus₂ : {α γ : Ty} {μα μγ : Tr} →
(v₁ : Val[ var ] Nat) →
pFr[ var , Nat ⟨ μα ⟩ α ⟨ μγ ⟩ γ ] Nat ⟨ μα ⟩ α ⟨ μγ ⟩ γ
Is0 : {α β : Ty} {μα μβ : Tr} →
pFr[ var , Nat ⟨ μα ⟩ α ⟨ μβ ⟩ β ] Bool ⟨ μα ⟩ α ⟨ μβ ⟩ β
B2S : {α β : Ty} {μα μβ : Tr} →
pFr[ var , Bool ⟨ μα ⟩ α ⟨ μβ ⟩ β ] Str ⟨ μα ⟩ α ⟨ μβ ⟩ β
pFr-plug : {var : Ty → Set}
{τ₁ τ₂ τ₃ τ₄ τ₅ τ₆ : Ty} {μα μβ μγ μδ : Tr} →
pFr[ var , τ₁ ⟨ μα ⟩ τ₂ ⟨ μβ ⟩ τ₃ ] τ₄ ⟨ μγ ⟩ τ₅ ⟨ μδ ⟩ τ₆ →
Exp[ var ] τ₁ ⟨ μα ⟩ τ₂ ⟨ μβ ⟩ τ₃ →
Exp[ var ] τ₄ ⟨ μγ ⟩ τ₅ ⟨ μδ ⟩ τ₆
pFr-plug (App₁ e₂) e₁ = App e₁ e₂
pFr-plug (App₂ v₁) e₂ = App (Val v₁) e₂
pFr-plug (Plus₁ e₂) e₁ = Plus e₁ e₂
pFr-plug (Plus₂ v₁) e₂ = Plus (Val v₁) e₂
pFr-plug Is0 e = Is0 e
pFr-plug B2S e = B2S e
data same-pFr {var : Ty → Set}:
{τ₁ τ₁' τ₂ τ₂' τ₃ τ₃' τ₄ τ₄' τ₅ τ₅' τ₆ τ₆' : Ty}
{μα μα' μβ μβ' μγ μγ' μδ μδ' : Tr} →
pFr[ var , τ₁ ⟨ μα ⟩ τ₂ ⟨ μβ ⟩ τ₃ ] τ₄ ⟨ μγ ⟩ τ₅ ⟨ μδ ⟩ τ₆ →
pFr[ var , τ₁' ⟨ μα' ⟩ τ₂' ⟨ μβ' ⟩ τ₃' ] τ₄' ⟨ μγ' ⟩ τ₅' ⟨ μδ' ⟩ τ₆' →
Set where
App₁ : {τ β γ τ₃ τ₃' τ₄ τ₄' τ₅ τ₅' : Ty}{μ₁ μ₂ μβ μβ' μγ μγ' : Tr} →
(e₂ : Exp[ var ] τ ⟨ μ₁ ⟩ β ⟨ μ₂ ⟩ γ) →
same-pFr {τ₃ = τ₃} {τ₃' }{τ₄} {τ₄'} {τ₅} {τ₅'} {μβ = μβ} {μβ'} {μγ} {μγ'}
(App₁ e₂) (App₁ e₂)
App₂ : {τ₁ τ₂ α β τ₃ τ₃' : Ty}{μ₁ μ₂ μβ μβ' : Tr} →
(v₁ : Val[ var ] (τ₂ ⇒ τ₁ ⟨ μ₁ ⟩ α ⟨ μ₂ ⟩ β) ) →
same-pFr {τ₃ = τ₃} {τ₃'} {μβ = μβ} {μβ'}
(App₂ v₁) (App₂ v₁)
Plus₁ : {α β γ τ₃ τ₃' : Ty} {μα μβ μγ μβ' : Tr} →
(e₂ : Exp[ var ] Nat ⟨ μα ⟩ α ⟨ μβ ⟩ β) →
same-pFr {τ₃ = τ₃} {τ₃'} {μβ = μβ} {μβ'}
(Plus₁ e₂) (Plus₁ e₂)
Plus₂ : {τ₂ τ₂' τ₃ τ₃' : Ty} {μα μα' μβ μβ' : Tr} →
(v₁ : Val[ var ] Nat) →
same-pFr {τ₂ = τ₂} {τ₂'} {τ₃} {τ₃'} {μα = μα} {μα'} {μβ} {μβ'}
(Plus₂ v₁) (Plus₂ v₁)
Is0 : {τ₂ τ₂' τ₃ τ₃' : Ty} {μα μα' μβ μβ' : Tr} →
same-pFr {τ₂ = τ₂} {τ₂'} {τ₃} {τ₃'} {μα = μα} {μα'} {μβ} {μβ'}
Is0 Is0
B2S : {τ₂ τ₂' τ₃ τ₃' : Ty} {μα μα' μβ μβ' : Tr} →
same-pFr {τ₂ = τ₂} {τ₂'} {τ₃} {τ₃'} {μα = μα} {μα'} {μβ} {μβ'}
B2S B2S
-- Pure contexts
data pCxt[_,_⟨_⟩_⟨_⟩_]_⟨_⟩_⟨_⟩_ (var : Ty → Set)
: Ty → Tr → Ty → Tr → Ty → Ty → Tr → Ty → Tr → Ty → Set where
Hole : {τ₁ τ₂ τ₃ : Ty}{μα μβ : Tr} →
pCxt[ var , τ₁ ⟨ μα ⟩ τ₂ ⟨ μβ ⟩ τ₃ ] τ₁ ⟨ μα ⟩ τ₂ ⟨ μβ ⟩ τ₃
Fr : {τ₁ τ₂ τ₃ τ₄ τ₅ τ₆ τ₇ τ₈ τ₉ : Ty}{μ₁ μ₂ μ₃ μ₄ μ₅ μ₆ : Tr} →
(f : pFr[ var , τ₄ ⟨ μ₃ ⟩ τ₅ ⟨ μ₄ ⟩ τ₆ ] τ₇ ⟨ μ₅ ⟩ τ₈ ⟨ μ₆ ⟩ τ₉ ) →
(c : pCxt[ var , τ₁ ⟨ μ₁ ⟩ τ₂ ⟨ μ₂ ⟩ τ₃ ] τ₄ ⟨ μ₃ ⟩ τ₅ ⟨ μ₄ ⟩ τ₆ ) →
pCxt[ var , τ₁ ⟨ μ₁ ⟩ τ₂ ⟨ μ₂ ⟩ τ₃ ] τ₇ ⟨ μ₅ ⟩ τ₈ ⟨ μ₆ ⟩ τ₉
pCxt-plug : {var : Ty → Set}
{τ₁ τ₂ τ₃ τ₄ τ₅ τ₆ : Ty}{μα μβ μγ μδ : Tr} →
pCxt[ var , τ₁ ⟨ μα ⟩ τ₂ ⟨ μβ ⟩ τ₃ ] τ₄ ⟨ μγ ⟩ τ₅ ⟨ μδ ⟩ τ₆ →
Exp[ var ] τ₁ ⟨ μα ⟩ τ₂ ⟨ μβ ⟩ τ₃ →
Exp[ var ] τ₄ ⟨ μγ ⟩ τ₅ ⟨ μδ ⟩ τ₆
pCxt-plug Hole e₁ = e₁
pCxt-plug (Fr f p) e₁ = pFr-plug f (pCxt-plug p e₁)
data same-pCxt {var : Ty → Set} :
{τ₁ τ₁' τ₂ τ₂' τ₃ τ₃' τ₄ τ₄' τ₅ τ₅' τ₆ τ₆' : Ty}
{μα μα' μβ μβ' μγ μγ' μδ μδ' : Tr} →
pCxt[ var , τ₁ ⟨ μα ⟩ τ₂ ⟨ μβ ⟩ τ₃ ] τ₄ ⟨ μγ ⟩ τ₅ ⟨ μδ ⟩ τ₆ →
pCxt[ var , τ₁' ⟨ μα' ⟩ τ₂' ⟨ μβ' ⟩ τ₃' ] τ₄' ⟨ μγ' ⟩ τ₅' ⟨ μδ' ⟩ τ₆' →
Set where
Hole : {τ₁ τ₁' τ₂ τ₂' τ₃ τ₃' : Ty} {μα μα' μβ μβ' : Tr} →
same-pCxt {τ₁ = τ₁} {τ₁'} {τ₂} {τ₂'} {τ₃} {τ₃'} {μα = μα} {μα'} {μβ} {μβ'}
Hole Hole
Fr : {τ₁ τ₁' τ₂ τ₂' τ₃ τ₃' τ₄ τ₄' τ₅ τ₅' τ₆ τ₆' τ₇ τ₇' τ₈' τ₈ τ₉ τ₉' : Ty}
{μ₁ μ₁' μ₂ μ₂' μ₃ μ₃' μ₄ μ₄' μ₅ μ₅' μ₆ μ₆' : Tr} →
{f₁ : pFr[ var , τ₄ ⟨ μ₃ ⟩ τ₅ ⟨ μ₄ ⟩ τ₆ ] τ₇ ⟨ μ₅ ⟩ τ₈ ⟨ μ₆ ⟩ τ₉ } →
{f₂ : pFr[ var , τ₄' ⟨ μ₃' ⟩ τ₅' ⟨ μ₄' ⟩ τ₆' ] τ₇' ⟨ μ₅' ⟩ τ₈' ⟨ μ₆' ⟩ τ₉' } →
same-pFr f₁ f₂ →
{c₁ : pCxt[ var , τ₁ ⟨ μ₁ ⟩ τ₂ ⟨ μ₂ ⟩ τ₃ ] τ₄ ⟨ μ₃ ⟩ τ₅ ⟨ μ₄ ⟩ τ₆ } →
{c₂ : pCxt[ var , τ₁' ⟨ μ₁' ⟩ τ₂' ⟨ μ₂' ⟩ τ₃' ] τ₄' ⟨ μ₃' ⟩ τ₅' ⟨ μ₄' ⟩ τ₆' } →
same-pCxt c₁ c₂ →
same-pCxt (Fr f₁ c₁) (Fr f₂ c₂)
-- One-step reduction (proof of Theorem 1)
data Reduce {var : Ty → Set} :
{τ₁ τ₂ τ₃ : Ty} {μα μβ : Tr} →
Exp[ var ] τ₁ ⟨ μα ⟩ τ₂ ⟨ μβ ⟩ τ₃ →
Exp[ var ] τ₁ ⟨ μα ⟩ τ₂ ⟨ μβ ⟩ τ₃ → Set where
RBeta : {τ τ₁ τ₂ τ₃ : Ty} {μα μβ : Tr} →
{e : var τ → Exp[ var ] τ₁ ⟨ μα ⟩ τ₂ ⟨ μβ ⟩ τ₃} →
{v : Val[ var ] τ} →
{e' : Exp[ var ] τ₁ ⟨ μα ⟩ τ₂ ⟨ μβ ⟩ τ₃} →
Subst e v e' →
Reduce (App (Val (Abs e)) (Val v)) e'
RPlus : {τ₂ : Ty} {μα : Tr} {n₁ n₂ : ℕ} →
Reduce {τ₂ = τ₂} {μα = μα}
(Plus (Val (Num n₁)) (Val (Num n₂))) (Val (Num (n₁ + n₂)))
RIs0 : {τ₂ : Ty} {μα : Tr} {n : ℕ} →
Reduce {τ₂ = τ₂} {μα = μα}
(Is0 (Val (Num n))) (Val (Bol (is0 n)))
RB2S : {τ₂ : Ty} {μα : Tr} {b : 𝔹} →
Reduce {τ₂ = τ₂} {μα = μα}
(B2S (Val (Bol b))) (Val (Str (b2s b)))
RPrompt : {τ₂ β : Ty} {μα : Tr} →
{v₁ : Val[ var ] β} →
Reduce {τ₂ = τ₂} {μα = μα}
(Prompt refl (Val v₁)) (Val v₁)
RControl : {τ α α' β β' γ γ' t₁ t₂ τ₁ τ₂ τ₃ τ₄ τ₅ : Ty}
{μ₀ μ₁ μᵢ μα μα' μβ μβ' μ₂ μ₃ μ₄ μ₅ : Tr} →
(p₁ : pCxt[ var , τ ⟨ μα ⟩ α ⟨ μβ ⟩ β ]
τ₁ ⟨ μ₃ ⟩ τ₂ ⟨ ● ⟩ β ) →
(p₂ : pCxt[ var , τ ⟨ μα' ⟩ α' ⟨ μα' ⟩ α' ]
t₁ ⟨ μ₁ ⟩ t₂ ⟨ μ₂ ⟩ α ) →
{x₀ : is-id-trail τ₁ μ₃ τ₂} →
(x₁ : is-id-trail γ μᵢ γ') →
(x₂ : compatible (t₁ ⇒⟨ μ₁ ⟩ t₂) μ₂ μ₀) →
(x₃ : compatible μβ μ₀ μα) →
same-pCxt p₁ p₂ →
(e : var (τ ⇒ t₁ ⟨ μ₁ ⟩ t₂ ⟨ μ₂ ⟩ α) →
Exp[ var ] γ ⟨ μᵢ ⟩ γ' ⟨ ● ⟩ β) →
Reduce {τ₂ = τ₂} {μα = μα}
(Prompt x₀ (pCxt-plug p₁ (Control x₁ x₂ x₃ e)))
(Prompt x₁ (App (Val (Abs e))
(Val (Abs (λ x → pCxt-plug p₂ (Val (Var x)))))))
RFr : {τ₁ τ₂ τ₃ τ₄ τ₅ τ₆ : Ty} {μα μβ μγ μδ : Tr}
{e e' : Exp[ var ] τ₁ ⟨ μα ⟩ τ₂ ⟨ μβ ⟩ τ₃} →
(f : Fr[ var , τ₁ ⟨ μα ⟩ τ₂ ⟨ μβ ⟩ τ₃ ]
τ₄ ⟨ μγ ⟩ τ₅ ⟨ μδ ⟩ τ₆) →
Reduce e e' →
Reduce (Fr-plug f e) (Fr-plug f e')
-- Multi-step reduction
data Reduce* {var : Ty → Set} :
{τ₁ τ₂ τ₃ : Ty} {μα μβ : Tr} →
Exp[ var ] τ₁ ⟨ μα ⟩ τ₂ ⟨ μβ ⟩ τ₃ →
Exp[ var ] τ₁ ⟨ μα ⟩ τ₂ ⟨ μβ ⟩ τ₃ → Set where
R*Id : {τ₁ τ₂ τ₃ : Ty} {μα μβ : Tr} →
(e : Exp[ var ] τ₁ ⟨ μα ⟩ τ₂ ⟨ μβ ⟩ τ₃ ) →
Reduce* e e
R*Trans : {τ₁ τ₂ τ₃ : Ty} {μα μβ : Tr} →
(e₁ : Exp[ var ] τ₁ ⟨ μα ⟩ τ₂ ⟨ μβ ⟩ τ₃) →
(e₂ : Exp[ var ] τ₁ ⟨ μα ⟩ τ₂ ⟨ μβ ⟩ τ₃) →
(e₃ : Exp[ var ] τ₁ ⟨ μα ⟩ τ₂ ⟨ μβ ⟩ τ₃) →
Reduce e₁ e₂ →
Reduce* e₂ e₃ →
Reduce* e₁ e₃