# Extended simply typed lyambda calculus substitution for let term

Hello,

I am trying to solve this Exercise

#### Exercise: 3 stars, standard (STLCE_definitions)

from this Chapter
https://softwarefoundations.cis.upenn.edu/plf-current/MoreStlc.html

Having problems with definition of term `let` in Fixpoint subst.

This is how I defined it.

``````Fixpoint subst (x : string) (s : tm) (t : tm) : tm :=
match t with
....
| tlet y t t' =>
if eqb_string x y then (tlet y s t')
else (tlet y  (subst x s t) (subst x s t'))
...
end.

Notation "'[' x ':=' s ']' t" := (subst x s t) (at level 20).

``````

This is what I think about it:
Substitution and let are common in sense that they replace only unbound variables with new term in both cases.

so if `x` and `y` are the same string, in final term only s will replace corresponding unbound variables.
and if they are different, then let should work and replace all free occurrences of y with t in t’ . And let should work after substitution will work and will replace all occurrences of x with s in both terms
which participate in let : in t and t’

Please advice. I couldn’t prove LET part in 2 final theorems in this chapter… looks like because of wrong definition of let in Fixpoint subst.

I also tried this definition

``````Fixpoint subst (x : string) (s : tm) (t : tm) : tm :=
match t with
....
| tlet y t t' => tlet y  (subst x s t) (subst x s t')
...
end.

Notation "'[' x ':=' s ']' t" := (subst x s t) (at level 20).
``````

But with this definition theorems also do not work for let.
Thanks,
Nat

Your first proposal looks close to the solution.
But in the case `x = y`, it would give for example: `subst x s (tlet x z x) = tlet x s x` which looks strange isn’t it?

You right…
so if x = y… original let should replace all x’s from the term.
so if x = y we do nothing. no unbound x’s left.

Thank you. I’ll try to prove my theorems with this definition.

You should just be careful with free `x`'s in `t` for `subst x s (tlet x t t')`.