Termination of substitution in STLC

Stream: new members

[Niklas Halonen]

Hi all,

I've been using Lean for almost a year now and I'm still stumbling over the basics. I'm trying to formalize STLC (with booleans) (see https://softwarefoundations.cis.upenn.edu/plf-current/Stlc.html) and came across an interesting termination problem.

The core of the issue is that I have a map function for working with Terms to make it easier to write the substitution function, but using it causes Lean to not immediately figure out its termination, which is natural as the decreasing argument is being mapped over.

I need help with proving termination when I know the subterms that are mapped are smaller than the original term. Here is my code:

inductive Ty :=
  | Boolean
  | Arrow (fro : Ty) (to : Ty)
deriving Repr

inductive Term :=
  | True
  | False
  | Ite (cond : Term) (if_true : Term) (if_false : Term)
  | Abs (name : String) (ty : Ty) (body : Term)
  | App (t₁ : Term) (t₂ : Term)
  | Var (name : String)
deriving Repr

namespace Term
open Ty

def map (f : Term → Term) (self : Term) : Term := match self with
  | True | False | Var _ => f self
  | Ite cond if_true if_false => Ite (map f cond) (map f if_true) (map f if_false)
  | Abs name ty body => Abs name ty (map f body)
  | App t₁ t₂ => App (map f t₁) (map f t₂)

def subst (x : String) (s : Term) (t : Term) : Term := match t with
  | True | False => t
  | Var y => if x = y then s else t
  | Abs y T t₁ => if x = y then t₁ else Abs y T (subst x s t₁)
  | _ =>
    -- how do I express that map passess terms that are smaller than t to subst x s?
    map (subst x s) t -- HERE: fail to show termination

-- Lean figures out the termination of the following as expected
-- def subst (x : String) (s : Term) (t : Term) : Term := match t with
--   | Var y => if x = y then s else t
--   | Abs y T t₁ => if x = y then t₁ else Abs y T (subst x s t₁)
--   | True | False => t
--   | Ite cond if_true if_false => Ite (subst x s cond) (subst x s if_true) (subst x s if_false)
--   | App t₁ t₂ => App (subst x s t₁) (subst x s t₂)

Another odd thing is that Lean asks me to prove ⊢ sizeOf t < sizeOf x✝ where t doesn't refer to the original t but I think it's the t "missing" in subst x s passed to map. I noticed this because I tried to prove this claim using a sorry but that gets renamed to t✝

  | e =>
    have : sizeOf t < sizeOf e := sorry
    map (subst x s) t

Any help and/or explanations are greatly appreciated :big_smile:

[Johannes Tantow]

I suppose that it is difficult to prove termination because it is wrong: Let $t$ be True. Then subst x s True = map (subst x s) True. By the definition of map map (subst x s) True = subst x s True, which is exactly what we started with.
map does not pass terms that are smaller than $t$ because nothing is smaller than True or False to sizeOf.

[Johannes Tantow]

You can see that this does not occur in your modified version, because there True/False are directly returned.

[Niklas Halonen]

Very good point :sweat_smile: thanks for pointing that out!

[Niklas Halonen]

Okay I edited my code to handle the base cases, but now my question still holds: how to prove termination of map (subst x s)? It seems like there's no way to do it with have so what other approaches could be used?

[Johannes Tantow]

I think that Lean does not understand that _ corresponds to Ite. I think you should only use _ as I don't care what is there, which is not the case here as we need that this is not True/False

[Niklas Halonen]

It's Ite or App. I'm working on a minimal version of the problem

[Johannes Tantow]

I think the same applies here. Lean does not know that it is either Ite or App so you have to state it more explicitly. Alternatively, write functions like BaseCase=(True or False), isVar and isAbs and combine them to an if-else.

[Johannes Tantow]

Though you have have to write the ifs as h:isVar t inorder to use this in the termination proof

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

For the termination check to pass, you need something in the local context at each check site that implies that the new input is smaller than what you started with. You don't get this from map because f : α → β just gets some value of type α, not necessarily a smaller one. You can use docs#List.pmap to also get a proof that a ∈ l, which can be used to show that sizeOf decreases (in my experience Lean can often do this automatically once a ∈ l is in the local context).

[Johannes Tantow]

Wojciech Nawrocki schrieb:

For the termination check to pass, you need something in the local context at each check site that implies that the new input is smaller than what you started with. You don't get this from map because f : α → β just gets some value of type α, not necessarily a smaller one. You can use docs#List.pmap to also get a proof that a ∈ l, which can be used to show that sizeOf decreases (in my experience Lean can often do this automatically once a ∈ l is in the local context).

I don't see why that would help here as map here is a user defined function for terms and not the function for lists

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Oh, you're right; but you can apply the List.map -> List.pmap transformation to Term.map by adding an argument to the effect of t ∈ self (or just sizeOf t < sizeOf self) to f. (And yeah, it doesn't hold for the base cases; those would have to be accounted for somehow.)

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Also, independently of that, the subst case for Abs looks wrong to me: you have (λ(y:T). t₁)[t/x] = t₁ when x = y. Should it rather be λ(y:T). t₁?