Extended simply typed lyambda calculus substitution for let term

Using Coq
1

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

2

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?

3

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.

4

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