從Coq到Agda的移植（簡單型）lambda微積分術語飽和證明

Question

我試圖從Software Foundations, vol. 2端口msubst_R 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遞歸入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。

我錯過了什麼？

Answer 1

假設額外Bool基類型，Saturated會看起來更好以下方式，因爲它不會對於已經從Saturated如下fun參數要求一個Halts。

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你只能f在lam的情況下遞歸。沒有其他方法可以使其結構化。這項工作是利用減少/飽和引理將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