将（简单类型的）lambda 演算项饱和证明从 Coq 移植到 Agda

Question

我正在尝试将 msubst_R 从 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，它不一定小于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 的棘手方法。

我错过了什么？

Answer 1

假设一个额外的Bool 基本类型，Saturated 看起来会更好，因为它不需要 Halts 用于 fun 参数，而 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。没有其他方法可以使其结构化。工作是使用减少/饱和引理将来自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