Перенос (просто типизированного) доказательства насыщения термов лямбда-исчисления с Coq на Agda

Я пытаюсь перенести msubst_R с Основы программного обеспечения, т. 2 в Агду. Я пытаюсь избежать большого количества хлопот, используя типизированное представление терминов. Ниже мой порт всего до 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 рекурсивно преобразуется в saturate на f′, что не обязательно меньше 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.

Что мне не хватает?