Portage (simplement typé) lambda calcul terme preuve de saturation de Coq à Agda

Question

J'essaye de porter msubst_R de Software Foundations, vol. 2 à Agda. J'essaie d'éviter beaucoup de travail en utilisant une représentation typée pour les termes. Ci-dessous est mon port de tout jusqu'à msubst_R; Je pense que tout va bien, mais c'est nécessaire pour la partie problématique.

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 

Notez que j'ai enlevé les bool et pair types car ils ne sont pas nécessaires pour montrer mon problème.

Le problème est donc avec msubst_R (que j'appelle saturate ci-dessous):

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 ne passe pas le vérificateur de terminaison, parce que dans le lam cas, sat-f récursivement dans saturate sur f′, qui n'est pas nécessairement plus petit que lam u f; et [] ▷ e′ n'est pas nécessairement plus petit que σ.

Une autre façon de voir pourquoi saturate ne se termine pas est de regarder saturate env (app f e). Ici, récursif en f et (potentiellement) e va croître t, même si tous les autres cas laissent t le même et rétrécir le terme, ou réduire t. Donc, si saturate env (app f e) ne se répète pas en saturate env f et saturate env e, la récursion en saturate env (lam u f) ne serait pas problématique en soi.

Cependant, je pense que mon code fait la bonne chose pour le app f e cas (puisque c'est le point de l'ensemble de trimballer la preuve de saturation paramétrique pour les types de fonction), il devrait donc être le lam u f cas où je besoin d'une manière délicate dans lequel f′ est inférieur à lam u f.

Qu'est-ce qui me manque?

Answer 1

En supposant un type de base Bool supplémentaire, Saturated regarderait plus agréable de la façon suivante, car il ne demanderait pas un Halts pour l'argument fun qui suit déjà de 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 

Puis, en saturate vous ne pouvez récursif sur f dans le cas lam. Il n'y a pas d'autre moyen de le rendre structurel. Le travail consiste à masser l'hypothèse de f dans la bonne forme en utilisant les lemmes de réduction/saturation.

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