I'm trying to port msubst_R from Software Foundations, vol. 2 to Agda. I'm trying to avoid a lot of busywork by using a typed representation for terms. Below is my port of everything up to msubst_R; I think everything is fine below but it's needed for the problematic part.
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
Note that I have removed the bool and pair types since they are not necessary to show my problem.
The problem, then, is with msubst_R (which I call saturate below):
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 doesn't pass the termination checker, because in the lam case, sat-f recurses into saturate on f′, which isn't necessarily smaller than lam u f; and [] ▷ e′ is also not necessarily smaller than σ.
Another way of looking at why saturate doesn't terminate is to look at saturate env (app f e). Here, recursing into f and (potentially) e will grow t, even though all the other cases either leave t the same and shrink the term, or shrink t. So if saturate env (app f e) didn't recurse into saturate env f and saturate env e, the recursion in saturate env (lam u f) would not be problematic in itself.
However, I think my code does the right thing for the app f e case (since that's the whole point of lugging around the parametric saturation proof for function types), so it should be the lam u f case where I need a tricky way in which f′ is smaller than lam u f.
What am I missing?
Assuming an additional Bool base type, Saturated would look nicer the following way, since it would not demand a Halts for the fun argument which already follows from 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
Then, in saturate you can only recurse on f in the lam case. There is no other way to make it structural. The job is to massage the hypothesis from f into the right shape using the reduction/saturation lemmas.
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