Portierung (einfach typisiert) Lambda Kalkül Term Sättigung Beweis von Coq Agda

Question

Ich versuche Port msubst_R von Software Foundations, vol. 2 zu Agda. Ich versuche, viel Arbeit zu vermeiden, indem ich eine typisierte Darstellung für Begriffe verwende. Unten ist mein Port von allem bis msubst_R; Ich denke, unten ist alles in Ordnung, aber es wird für den problematischen Teil benötigt.

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 

Bitte beachte, dass ich die bool und pair Typen entfernt haben, da sie nicht notwendig sind, um mein Problem zu zeigen.

Das Problem ist dann, mit msubst_R (was ich nenne saturate unten):

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 nicht die Beendigung Prüfung nicht besteht, weil in dem lam Fall sat-f rekursiv in saturate auf f′, die ist nicht notwendigerweise kleiner als lam u f; und [] ▷ e′ ist auch nicht notwendigerweise kleiner als σ.

Eine andere Möglichkeit zu sehen, warum saturate nicht endet, ist zu sehen saturate env (app f e). Hier wird die Rekursion in f und (potentiell) e wird t wachsen, auch wenn alle anderen Fälle entweder t das gleiche lassen und den Begriff schrumpfen, oder schrumpfen t. Wenn also saturate env (app f e) nicht in saturate env f und saturate env e recurse, wäre die Rekursion in saturate env (lam u f) an sich nicht problematisch.

Aber ich denke, mein Code tut das Richtige für den app f e Fall (denn das ist der springende Punkt ist rund um den parametrisch Sättigung Beweis mitschleppen für Funktionstypen), so dass es der lam u f Fall sein sollte, wo ich eine schwierige Art und Weise muß in welche f′ ist kleiner als lam u f.

Was fehlt mir?

Answer 1

einen zusätzlichen Bool Basistyp Unter der Annahme, würde Saturated schöner aussehen die folgende Art und Weise, da sie keine Halts für das fun Argument, das schon folgt aus Saturated verlangen würden.

Saturated : ∀ {A} → Tm [] A → Set 
Saturated {fun A B} t = Halts t × (∀ {u} → Saturated u → Saturated (app t u)) 
Saturated {Bool} t = Halts t 

Dann in saturate können Sie nur auf f im lam Fall Rekursion. Es gibt keinen anderen Weg, um es strukturell zu machen. Die Aufgabe besteht darin, die Hypothese von f mit den Reduktions-/Sättigungslinien in die richtige Form zu bringen.

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