Coq에서 Agda 로의 포팅 (단순 유형 지정) 람다 수학 용어

Question

msubst_R을 Software Foundations, vol. 2에서 Agda로 이식하려고합니다. 용어에 대한 형식화 된 표현을 사용하여 많은 작업량을 피하려고합니다. 아래는 나의 항구 다 msubst_R; 나는 아래 모든 것이 훌륭하다고 생각하지만, 문제가되는 부분에 대해서는 필요합니다. 그들은 내 문제를 보여줄 필요하지 않기 때문에 나는 bool 및 pair 유형을 제거한

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 

참고.

문제는, 다음, (나는 saturate 아래 부른다) msubst_R 함께 :

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)의 재귀는 그 자체로 문제가되지 않습니다.

그러나, 나는 내가 까다로운 방법을 필요로하는 lam u f 경우해야하므로 (즉, 기능 유형에 대한 파라 메트릭 포화 증거 주위에 짐을 끌고 다니는의 전체 지점 이후) 내 코드가 app f e 경우에 적합한 일을 생각한다 f′은 lam u f보다 작습니다.

무엇이 누락 되었습니까? 이미 Saturated에서 다음에 fun 인수에 대한 Halts을 요구하지 것이기 때문에 추가 Bool 기본 유형을 가정

는

Answer 1

, 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