将（简单类型的）lambda 演算项饱和证明从 Coq 移植到 Agda
Porting (simply-typed) lambda calculus term saturation proof from Coq to Agda
我正在尝试将 msubst_R from Software Foundations, vol. 2 移植到 Agda。我试图通过对术语使用类型化表示来避免大量繁琐的工作。以下是我对 msubst_R 之前所有内容的移植；我认为下面一切都很好，但有问题的部分需要它。
open import Data.Nat
open import Relation.Binary.PropositionalEquality hiding (subst)
open import Data.Empty
open import Data.Unit
open import Relation.Binary
open import Data.Star
open import Level renaming (zero to lzero)
open import Data.Product
open import Function.Equivalence hiding (sym)
open import Function.Equality using (_⟨$⟩_)
data Ty : Set where
fun : Ty → Ty → Ty
infixl 21 _▷_
data Ctx : Set where
[] : Ctx
_▷_ : Ctx → Ty → Ctx
data Var (t : Ty) : Ctx → Set where
vz : ∀ {Γ} → Var t (Γ ▷ t)
vs : ∀ {Γ u} → Var t Γ → Var t (Γ ▷ u)
data _⊆_ : Ctx → Ctx → Set where
done : ∀ {Δ} → [] ⊆ Δ
keep : ∀ {Γ Δ a} → Γ ⊆ Δ → Γ ▷ a ⊆ Δ ▷ a
drop : ∀ {Γ Δ a} → Γ ⊆ Δ → Γ ⊆ Δ ▷ a
⊆-refl : ∀ {Γ} → Γ ⊆ Γ
⊆-refl {[]} = done
⊆-refl {Γ ▷ _} = keep ⊆-refl
data Tm (Γ : Ctx) : Ty → Set where
var : ∀ {t} → Var t Γ → Tm Γ t
lam : ∀ t {u} → (e : Tm (Γ ▷ t) u) → Tm Γ (fun t u)
app : ∀ {u t} → (f : Tm Γ (fun u t)) → (e : Tm Γ u) → Tm Γ t
wk-var : ∀ {Γ Δ t} → Γ ⊆ Δ → Var t Γ → Var t Δ
wk-var done ()
wk-var (keep Γ⊆Δ) vz = vz
wk-var (keep Γ⊆Δ) (vs v) = vs (wk-var Γ⊆Δ v)
wk-var (drop Γ⊆Δ) v = vs (wk-var Γ⊆Δ v)
wk : ∀ {Γ Δ t} → Γ ⊆ Δ → Tm Γ t → Tm Δ t
wk Γ⊆Δ (var v) = var (wk-var Γ⊆Δ v)
wk Γ⊆Δ (lam t e) = lam t (wk (keep Γ⊆Δ) e)
wk Γ⊆Δ (app f e) = app (wk Γ⊆Δ f) (wk Γ⊆Δ e)
data _⊢⋆_ (Γ : Ctx) : Ctx → Set where
[] : Γ ⊢⋆ []
_▷_ : ∀ {Δ t} → Γ ⊢⋆ Δ → Tm Γ t → Γ ⊢⋆ Δ ▷ t
⊢⋆-wk : ∀ {Γ Δ} t → Γ ⊢⋆ Δ → Γ ▷ t ⊢⋆ Δ
⊢⋆-wk t [] = []
⊢⋆-wk t (σ ▷ e) = (⊢⋆-wk t σ) ▷ wk (drop ⊆-refl) e
⊢⋆-mono : ∀ {Γ Δ t} → Γ ⊢⋆ Δ → Γ ▷ t ⊢⋆ Δ ▷ t
⊢⋆-mono σ = ⊢⋆-wk _ σ ▷ var vz
⊢⋆-refl : ∀ {Γ} → Γ ⊢⋆ Γ
⊢⋆-refl {[]} = []
⊢⋆-refl {Γ ▷ _} = ⊢⋆-mono ⊢⋆-refl
subst-var : ∀ {Γ Δ t} → Γ ⊢⋆ Δ → Var t Δ → Tm Γ t
subst-var [] ()
subst-var (σ ▷ x) vz = x
subst-var (σ ▷ x) (vs v) = subst-var σ v
subst : ∀ {Γ Δ t} → Γ ⊢⋆ Δ → Tm Δ t → Tm Γ t
subst σ (var x) = subst-var σ x
subst σ (lam t e) = lam t (subst (⊢⋆-mono σ) e)
subst σ (app f e) = app (subst σ f) (subst σ e)
data Value : {Γ : Ctx} → {t : Ty} → Tm Γ t → Set where
lam : ∀ {Γ t} → ∀ u (e : Tm _ t) → Value {Γ} (lam u e)
data _==>_ {Γ} : ∀ {t} → Rel (Tm Γ t) lzero where
app-lam : ∀ {t u} (f : Tm _ t) {v : Tm _ u} → Value v → app (lam u f) v ==> subst (⊢⋆-refl ▷ v) f
appˡ : ∀ {t u} {f f′ : Tm Γ (fun u t)} → f ==> f′ → (e : Tm Γ u) → app f e ==> app f′ e
appʳ : ∀ {t u} {f} → Value {Γ} {fun u t} f → ∀ {e e′ : Tm Γ u} → e ==> e′ → app f e ==> app f e′
_==>*_ : ∀ {Γ t} → Rel (Tm Γ t) _
_==>*_ = Star _==>_
NF : ∀ {a b} {A : Set a} → Rel A b → A → Set _
NF step x = ∄ (step x)
value⇒normal : ∀ {Γ t e} → Value {Γ} {t} e → NF _==>_ e
value⇒normal (lam t e) (_ , ())
Deterministic : ∀ {a b} {A : Set a} → Rel A b → Set _
Deterministic step = ∀ {x y y′} → step x y → step x y′ → y ≡ y′
deterministic : ∀ {Γ t} → Deterministic (_==>_ {Γ} {t})
deterministic (app-lam f _) (app-lam ._ _) = refl
deterministic (app-lam f v) (appˡ () _)
deterministic (app-lam f v) (appʳ f′ e) = ⊥-elim (value⇒normal v (, e))
deterministic (appˡ () e) (app-lam f v)
deterministic (appˡ f e) (appˡ f′ ._) = cong _ (deterministic f f′)
deterministic (appˡ f e) (appʳ f′ _) = ⊥-elim (value⇒normal f′ (, f))
deterministic (appʳ f e) (app-lam f′ v) = ⊥-elim (value⇒normal v (, e))
deterministic (appʳ f e) (appˡ f′ _) = ⊥-elim (value⇒normal f (, f′))
deterministic (appʳ f e) (appʳ f′ e′) = cong _ (deterministic e e′)
Halts : ∀ {Γ t} → Tm Γ t → Set
Halts e = ∃ λ e′ → e ==>* e′ × Value e′
value⇒halts : ∀ {Γ t e} → Value {Γ} {t} e → Halts e
value⇒halts {e = e} v = e , ε , v
-- -- This would not be strictly positive!
-- data Saturated : ∀ {Γ t} → Tm Γ t → Set where
-- fun : ∀ {t u} {f : Tm [] (fun t u)} → Halts f → (∀ {e} → Saturated e → Saturated (app f e)) → Saturated f
mutual
Saturated : ∀ {t} → Tm [] t → Set
Saturated e = Halts e × Saturated′ _ e
Saturated′ : ∀ t → Tm [] t → Set
Saturated′ (fun t u) f = ∀ {e} → Saturated e → Saturated (app f e)
saturated⇒halts : ∀ {t e} → Saturated {t} e → Halts e
saturated⇒halts = proj₁
step‿preserves‿halting : ∀ {Γ t} {e e′ : Tm Γ t} → e ==> e′ → Halts e ⇔ Halts e′
step‿preserves‿halting {e = e} {e′ = e′} step = equivalence fwd bwd
where
fwd : Halts e → Halts e′
fwd (e″ , ε , v) = ⊥-elim (value⇒normal v (, step))
fwd (e″ , s ◅ steps , v) rewrite deterministic step s = e″ , steps , v
bwd : Halts e′ → Halts e
bwd (e″ , steps , v) = e″ , step ◅ steps , v
step‿preserves‿saturated : ∀ {t} {e e′ : Tm _ t} → e ==> e′ → Saturated e ⇔ Saturated e′
step‿preserves‿saturated step = equivalence (fwd step) (bwd step)
where
fwd : ∀ {t} {e e′ : Tm _ t} → e ==> e′ → Saturated e → Saturated e′
fwd {fun s t} step (halts , sat) = Equivalence.to (step‿preserves‿halting step) ⟨$⟩ halts , λ e → fwd (appˡ step _) (sat e)
bwd : ∀ {t} {e e′ : Tm _ t} → e ==> e′ → Saturated e′ → Saturated e
bwd {fun s t} step (halts , sat) = Equivalence.from (step‿preserves‿halting step) ⟨$⟩ halts , λ e → bwd (appˡ step _) (sat e)
step*‿preserves‿saturated : ∀ {t} {e e′ : Tm _ t} → e ==>* e′ → Saturated e ⇔ Saturated e′
step*‿preserves‿saturated ε = id
step*‿preserves‿saturated (step ◅ steps) = step*‿preserves‿saturated steps ∘ step‿preserves‿saturated step
请注意，我已经删除了 bool 和 pair 类型，因为它们不是显示我的问题所必需的。
那么，问题出在 msubst_R（我在下面称之为 saturate）：
data Instantiation : ∀ {Γ} → [] ⊢⋆ Γ → Set where
[] : Instantiation []
_▷_ : ∀ {Γ t σ} → Instantiation {Γ} σ → ∀ {e} → Value {_} {t} e × Saturated e → Instantiation (σ ▷ e)
saturate-var : ∀ {Γ σ} → Instantiation σ → ∀ {t} (x : Var t Γ) → Saturated (subst-var σ x)
saturate-var (_ ▷ (_ , sat)) vz = sat
saturate-var (env ▷ _) (vs x) = saturate-var env x
app-lam* : ∀ {Γ t} {e e′ : Tm Γ t} → e ==>* e′ → Value e′ → ∀ {u} (f : Tm _ u) → app (lam t f) e ==>* subst (⊢⋆-refl ▷ e′) f
app-lam* steps v f = gmap _ (appʳ (lam _ _)) steps ◅◅ app-lam f v ◅ ε
saturate : ∀ {Γ σ} → Instantiation σ → ∀ {t} → (e : Tm Γ t) → Saturated (subst σ e)
saturate env (var x) = saturate-var env x
saturate env (lam u f) = value⇒halts (lam u _) , sat-f
where
f′ = subst _ f
sat-f : ∀ {e : Tm _ u} → Saturated e → Saturated (app (lam u f′) e)
sat-f sat@((e′ , steps , v) , _) =
Equivalence.from (step*‿preserves‿saturated (app-lam* steps v f′)) ⟨$⟩ saturate ([] ▷ (v , Equivalence.to (step*‿preserves‿saturated steps) ⟨$⟩ sat)) f′
saturate env (app f e) with saturate env f | saturate env e
saturate env (app f e) | _ , sat-f | sat-e = sat-f sat-e
saturate 没有通过终止检查器，因为在 lam 的情况下，sat-f 在 f′ 上递归到 saturate，这不是t 一定小于 lam u f； [] ▷ e′ 也不一定小于 σ。
查看 saturate 为何不终止的另一种方法是查看 saturate env (app f e)。在这里，递归到 f 和（可能）e 将增长 t，即使所有其他情况要么保持 t 相同并缩小术语，要么缩小 t。因此，如果 saturate env (app f e) 没有递归到 saturate env f 和 saturate env e，那么 saturate env (lam u f) 中的递归本身不会有问题。
但是，我认为我的代码对 app f e 情况做了正确的事情（因为这是绕过函数类型的参数饱和证明的全部要点），所以它应该是 lam u f 我需要一个 f′ 小于 lam u f.
的棘手方法
我错过了什么？
假设有一个额外的 Bool 基本类型，Saturated 看起来会更好，因为它不需要 Halts 用于已经跟随的 fun 参数来自 Saturated.
Saturated : ∀ {A} → Tm [] A → Set
Saturated {fun A B} t = Halts t × (∀ {u} → Saturated u → Saturated (app t u))
Saturated {Bool} t = Halts t
然后，在 saturate 中，您只能在 lam 中递归 f。没有其他方法可以使它结构化。工作是使用 reduction/saturation 引理将 f 中的假设推敲成正确的形状。
open import Function using (case_of_)
saturate : ∀ {Γ σ} → Instantiation σ → ∀ {t} → (e : Tm Γ t) → Saturated (subst σ e)
saturate env (var x) = saturate-var env x
saturate env (lam u f) =
value⇒halts (lam _ (subst _ f)) ,
λ {u} usat →
case (saturated⇒halts usat) of λ {(u' , u==>*u' , u'val) →
let hyp = saturate (env ▷ (u'val , Equivalence.to (step*‿preserves‿saturated u==>*u') ⟨$⟩ usat)) f
in {!!}} -- fill this with grunt work
saturate env (app f e) with saturate env f | saturate env e
saturate env (app f e) | _ , sat-f | sat-e = sat-f sat-e
我正在尝试将 msubst_R from Software Foundations, vol. 2 移植到 Agda。我试图通过对术语使用类型化表示来避免大量繁琐的工作。以下是我对 msubst_R 之前所有内容的移植；我认为下面一切都很好，但有问题的部分需要它。
open import Data.Nat
open import Relation.Binary.PropositionalEquality hiding (subst)
open import Data.Empty
open import Data.Unit
open import Relation.Binary
open import Data.Star
open import Level renaming (zero to lzero)
open import Data.Product
open import Function.Equivalence hiding (sym)
open import Function.Equality using (_⟨$⟩_)
data Ty : Set where
fun : Ty → Ty → Ty
infixl 21 _▷_
data Ctx : Set where
[] : Ctx
_▷_ : Ctx → Ty → Ctx
data Var (t : Ty) : Ctx → Set where
vz : ∀ {Γ} → Var t (Γ ▷ t)
vs : ∀ {Γ u} → Var t Γ → Var t (Γ ▷ u)
data _⊆_ : Ctx → Ctx → Set where
done : ∀ {Δ} → [] ⊆ Δ
keep : ∀ {Γ Δ a} → Γ ⊆ Δ → Γ ▷ a ⊆ Δ ▷ a
drop : ∀ {Γ Δ a} → Γ ⊆ Δ → Γ ⊆ Δ ▷ a
⊆-refl : ∀ {Γ} → Γ ⊆ Γ
⊆-refl {[]} = done
⊆-refl {Γ ▷ _} = keep ⊆-refl
data Tm (Γ : Ctx) : Ty → Set where
var : ∀ {t} → Var t Γ → Tm Γ t
lam : ∀ t {u} → (e : Tm (Γ ▷ t) u) → Tm Γ (fun t u)
app : ∀ {u t} → (f : Tm Γ (fun u t)) → (e : Tm Γ u) → Tm Γ t
wk-var : ∀ {Γ Δ t} → Γ ⊆ Δ → Var t Γ → Var t Δ
wk-var done ()
wk-var (keep Γ⊆Δ) vz = vz
wk-var (keep Γ⊆Δ) (vs v) = vs (wk-var Γ⊆Δ v)
wk-var (drop Γ⊆Δ) v = vs (wk-var Γ⊆Δ v)
wk : ∀ {Γ Δ t} → Γ ⊆ Δ → Tm Γ t → Tm Δ t
wk Γ⊆Δ (var v) = var (wk-var Γ⊆Δ v)
wk Γ⊆Δ (lam t e) = lam t (wk (keep Γ⊆Δ) e)
wk Γ⊆Δ (app f e) = app (wk Γ⊆Δ f) (wk Γ⊆Δ e)
data _⊢⋆_ (Γ : Ctx) : Ctx → Set where
[] : Γ ⊢⋆ []
_▷_ : ∀ {Δ t} → Γ ⊢⋆ Δ → Tm Γ t → Γ ⊢⋆ Δ ▷ t
⊢⋆-wk : ∀ {Γ Δ} t → Γ ⊢⋆ Δ → Γ ▷ t ⊢⋆ Δ
⊢⋆-wk t [] = []
⊢⋆-wk t (σ ▷ e) = (⊢⋆-wk t σ) ▷ wk (drop ⊆-refl) e
⊢⋆-mono : ∀ {Γ Δ t} → Γ ⊢⋆ Δ → Γ ▷ t ⊢⋆ Δ ▷ t
⊢⋆-mono σ = ⊢⋆-wk _ σ ▷ var vz
⊢⋆-refl : ∀ {Γ} → Γ ⊢⋆ Γ
⊢⋆-refl {[]} = []
⊢⋆-refl {Γ ▷ _} = ⊢⋆-mono ⊢⋆-refl
subst-var : ∀ {Γ Δ t} → Γ ⊢⋆ Δ → Var t Δ → Tm Γ t
subst-var [] ()
subst-var (σ ▷ x) vz = x
subst-var (σ ▷ x) (vs v) = subst-var σ v
subst : ∀ {Γ Δ t} → Γ ⊢⋆ Δ → Tm Δ t → Tm Γ t
subst σ (var x) = subst-var σ x
subst σ (lam t e) = lam t (subst (⊢⋆-mono σ) e)
subst σ (app f e) = app (subst σ f) (subst σ e)
data Value : {Γ : Ctx} → {t : Ty} → Tm Γ t → Set where
lam : ∀ {Γ t} → ∀ u (e : Tm _ t) → Value {Γ} (lam u e)
data _==>_ {Γ} : ∀ {t} → Rel (Tm Γ t) lzero where
app-lam : ∀ {t u} (f : Tm _ t) {v : Tm _ u} → Value v → app (lam u f) v ==> subst (⊢⋆-refl ▷ v) f
appˡ : ∀ {t u} {f f′ : Tm Γ (fun u t)} → f ==> f′ → (e : Tm Γ u) → app f e ==> app f′ e
appʳ : ∀ {t u} {f} → Value {Γ} {fun u t} f → ∀ {e e′ : Tm Γ u} → e ==> e′ → app f e ==> app f e′
_==>*_ : ∀ {Γ t} → Rel (Tm Γ t) _
_==>*_ = Star _==>_
NF : ∀ {a b} {A : Set a} → Rel A b → A → Set _
NF step x = ∄ (step x)
value⇒normal : ∀ {Γ t e} → Value {Γ} {t} e → NF _==>_ e
value⇒normal (lam t e) (_ , ())
Deterministic : ∀ {a b} {A : Set a} → Rel A b → Set _
Deterministic step = ∀ {x y y′} → step x y → step x y′ → y ≡ y′
deterministic : ∀ {Γ t} → Deterministic (_==>_ {Γ} {t})
deterministic (app-lam f _) (app-lam ._ _) = refl
deterministic (app-lam f v) (appˡ () _)
deterministic (app-lam f v) (appʳ f′ e) = ⊥-elim (value⇒normal v (, e))
deterministic (appˡ () e) (app-lam f v)
deterministic (appˡ f e) (appˡ f′ ._) = cong _ (deterministic f f′)
deterministic (appˡ f e) (appʳ f′ _) = ⊥-elim (value⇒normal f′ (, f))
deterministic (appʳ f e) (app-lam f′ v) = ⊥-elim (value⇒normal v (, e))
deterministic (appʳ f e) (appˡ f′ _) = ⊥-elim (value⇒normal f (, f′))
deterministic (appʳ f e) (appʳ f′ e′) = cong _ (deterministic e e′)
Halts : ∀ {Γ t} → Tm Γ t → Set
Halts e = ∃ λ e′ → e ==>* e′ × Value e′
value⇒halts : ∀ {Γ t e} → Value {Γ} {t} e → Halts e
value⇒halts {e = e} v = e , ε , v
-- -- This would not be strictly positive!
-- data Saturated : ∀ {Γ t} → Tm Γ t → Set where
-- fun : ∀ {t u} {f : Tm [] (fun t u)} → Halts f → (∀ {e} → Saturated e → Saturated (app f e)) → Saturated f
mutual
Saturated : ∀ {t} → Tm [] t → Set
Saturated e = Halts e × Saturated′ _ e
Saturated′ : ∀ t → Tm [] t → Set
Saturated′ (fun t u) f = ∀ {e} → Saturated e → Saturated (app f e)
saturated⇒halts : ∀ {t e} → Saturated {t} e → Halts e
saturated⇒halts = proj₁
step‿preserves‿halting : ∀ {Γ t} {e e′ : Tm Γ t} → e ==> e′ → Halts e ⇔ Halts e′
step‿preserves‿halting {e = e} {e′ = e′} step = equivalence fwd bwd
where
fwd : Halts e → Halts e′
fwd (e″ , ε , v) = ⊥-elim (value⇒normal v (, step))
fwd (e″ , s ◅ steps , v) rewrite deterministic step s = e″ , steps , v
bwd : Halts e′ → Halts e
bwd (e″ , steps , v) = e″ , step ◅ steps , v
step‿preserves‿saturated : ∀ {t} {e e′ : Tm _ t} → e ==> e′ → Saturated e ⇔ Saturated e′
step‿preserves‿saturated step = equivalence (fwd step) (bwd step)
where
fwd : ∀ {t} {e e′ : Tm _ t} → e ==> e′ → Saturated e → Saturated e′
fwd {fun s t} step (halts , sat) = Equivalence.to (step‿preserves‿halting step) ⟨$⟩ halts , λ e → fwd (appˡ step _) (sat e)
bwd : ∀ {t} {e e′ : Tm _ t} → e ==> e′ → Saturated e′ → Saturated e
bwd {fun s t} step (halts , sat) = Equivalence.from (step‿preserves‿halting step) ⟨$⟩ halts , λ e → bwd (appˡ step _) (sat e)
step*‿preserves‿saturated : ∀ {t} {e e′ : Tm _ t} → e ==>* e′ → Saturated e ⇔ Saturated e′
step*‿preserves‿saturated ε = id
step*‿preserves‿saturated (step ◅ steps) = step*‿preserves‿saturated steps ∘ step‿preserves‿saturated step
请注意，我已经删除了 bool 和 pair 类型，因为它们不是显示我的问题所必需的。
那么，问题出在 msubst_R（我在下面称之为 saturate）：
data Instantiation : ∀ {Γ} → [] ⊢⋆ Γ → Set where
[] : Instantiation []
_▷_ : ∀ {Γ t σ} → Instantiation {Γ} σ → ∀ {e} → Value {_} {t} e × Saturated e → Instantiation (σ ▷ e)
saturate-var : ∀ {Γ σ} → Instantiation σ → ∀ {t} (x : Var t Γ) → Saturated (subst-var σ x)
saturate-var (_ ▷ (_ , sat)) vz = sat
saturate-var (env ▷ _) (vs x) = saturate-var env x
app-lam* : ∀ {Γ t} {e e′ : Tm Γ t} → e ==>* e′ → Value e′ → ∀ {u} (f : Tm _ u) → app (lam t f) e ==>* subst (⊢⋆-refl ▷ e′) f
app-lam* steps v f = gmap _ (appʳ (lam _ _)) steps ◅◅ app-lam f v ◅ ε
saturate : ∀ {Γ σ} → Instantiation σ → ∀ {t} → (e : Tm Γ t) → Saturated (subst σ e)
saturate env (var x) = saturate-var env x
saturate env (lam u f) = value⇒halts (lam u _) , sat-f
where
f′ = subst _ f
sat-f : ∀ {e : Tm _ u} → Saturated e → Saturated (app (lam u f′) e)
sat-f sat@((e′ , steps , v) , _) =
Equivalence.from (step*‿preserves‿saturated (app-lam* steps v f′)) ⟨$⟩ saturate ([] ▷ (v , Equivalence.to (step*‿preserves‿saturated steps) ⟨$⟩ sat)) f′
saturate env (app f e) with saturate env f | saturate env e
saturate env (app f e) | _ , sat-f | sat-e = sat-f sat-e
saturate 没有通过终止检查器，因为在 lam 的情况下，sat-f 在 f′ 上递归到 saturate，这不是t 一定小于 lam u f； [] ▷ e′ 也不一定小于 σ。
查看 saturate 为何不终止的另一种方法是查看 saturate env (app f e)。在这里，递归到 f 和（可能）e 将增长 t，即使所有其他情况要么保持 t 相同并缩小术语，要么缩小 t。因此，如果 saturate env (app f e) 没有递归到 saturate env f 和 saturate env e，那么 saturate env (lam u f) 中的递归本身不会有问题。
但是，我认为我的代码对 app f e 情况做了正确的事情（因为这是绕过函数类型的参数饱和证明的全部要点），所以它应该是 lam u f 我需要一个 f′ 小于 lam u f.
我错过了什么？
假设有一个额外的 Bool 基本类型，Saturated 看起来会更好，因为它不需要 Halts 用于已经跟随的 fun 参数来自 Saturated.
Saturated : ∀ {A} → Tm [] A → Set
Saturated {fun A B} t = Halts t × (∀ {u} → Saturated u → Saturated (app t u))
Saturated {Bool} t = Halts t
然后，在 saturate 中，您只能在 lam 中递归 f。没有其他方法可以使它结构化。工作是使用 reduction/saturation 引理将 f 中的假设推敲成正确的形状。
open import Function using (case_of_)
saturate : ∀ {Γ σ} → Instantiation σ → ∀ {t} → (e : Tm Γ t) → Saturated (subst σ e)
saturate env (var x) = saturate-var env x
saturate env (lam u f) =
value⇒halts (lam _ (subst _ f)) ,
λ {u} usat →
case (saturated⇒halts usat) of λ {(u' , u==>*u' , u'val) →
let hyp = saturate (env ▷ (u'val , Equivalence.to (step*‿preserves‿saturated u==>*u') ⟨$⟩ usat)) f
in {!!}} -- fill this with grunt work
saturate env (app f e) with saturate env f | saturate env e
saturate env (app f e) | _ , sat-f | sat-e = sat-f sat-e