I am trying to solve this Exercise
Exercise: 3 stars, standard (STLCE_definitions)
from this Chapter
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.
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.