STLC substitution behaviour with lambda body normalisation

UPDATE 31/07/'24 12.57:
It is false: Assume v, w, x, y, z all type variables. Take t = (\y. y) (x w) --> x w = t', then t[x=\z. v] = (\y. y) ((\z. v) w) --> (\y. y) v, while t'[x=\z. v] = (\z. v) w. These terms are both equal to v, but they do not step to each other, so the statement is false. However, these terms "coincidentally" step to the same value v. So the question becomes: what conditions do I need to add, or how do I need to alter the statement, to be able to prove something that is a little weaker than the original statement?

I have an STLC with types and kinds (instead of terms and types). I employ a deterministic small step semantics (-->) where lambdas are only values if their bodies are values, and therefore there is ST_Abs to normalize the body.

I want to prove that if t --> t', that then subst x v t --> subst x v t', but I am facing difficulties, because of the restrictions on beta reduction: this can only happen if both the argument and the lambda body are values.

For now I disregard complexities of capture avoiding and shadowing, since I don't think these details will make the proof work or not work. (But I have included a capture avoiding operational semantics below.)

I have created a minimal example below. I try to prove this by inducting over the type t, and then using inversion to utilize the information of the deterministic step. I get four subgoals and one is problematic:

First of all, as you can see in the image, the induction hypotheses are useless, since we already know t2 and v1 are values, so the condition can never be true (values don't step).

Here we have the case where t = t_1 t_2 = (\ x : K2, v1) v2, which steps to t'=[x := v2] v1. We know that v1,v2 are values, but t'=[x := v2] v1 is not for example, therefore I cannot do reverse beta reduction in the righthand side of the subgoal below.

[X := v] ((\ x : K2, v1) v2) -->* [X := v] ([x := v2] v1)

Even with stronger conditions, like t is strongly normalizing, thus showing some halting conditions, we still end up at problematic places, because even knowing something multisteps to a value, is not enough in cases like:

[X := v'] t, with t -->* v and value v, since there are no rules about this non-value substitution term.

Is this lemma true? We have some type t. We replace all Var x with v'. Both are values, so they will be treated the same according to the small step semantics I think, hence the step that t does to t' should not "touch" v'. But how to check this intuition, and how to tell this to Coq.

If so: Is this provable?

And if so: Do I need a Logical Relation to strengthen the induction hypothesis?

Minimal working stand-alone example in Coq 8.18.0:

Require Import Coq.Strings.String.
Open Scope string_scope.

(** kinds *)
Inductive kind :=
| Kind_Base : kind
| Kind_Arrow : kind -> kind -> kind.

(** Types *)
Inductive ty :=
| Var : string -> ty
| Lam : string -> kind -> ty -> ty
| App : ty -> ty -> ty.

(** Values *)
Inductive value : ty -> Prop :=
| v_neutral : forall ty1,
neutral ty1 ->
value ty1
| v_abs : forall x K2 ty1,
value ty1 ->
value (Lam x K2 ty1)

with neutral : ty -> Prop :=
| ne_var : forall x,
neutral (Var x)
| ne_app : forall ty1 ty2,
neutral ty1 ->
value ty2 ->
neutral (App ty1 ty2).

(** Subst *)
Fixpoint subst (X : string) (U T : ty) : ty :=
match T with
| Var Y =>
if X =? Y then U else Var Y
| Lam Y K1 T' =>
if X =? Y then Lam Y K1 T' else Lam Y K1 (subst X U T')
| App T1 T2 =>
App (subst X U T1) (subst X U T2)
end.

(** Notation *)
Declare Custom Entry stlc.
Notation "<{ e }>" := e (e custom stlc at level 99).
Notation "( x )" := x (in custom stlc, x at level 99).
Notation "x" := x (in custom stlc at level 0, x constr at level 0).
Notation "x y" := (App x y) (in custom stlc at level 1, left associativity).
Notation "\ x : k , y" :=
(Lam x k y) (in custom stlc at level 90, x at level 99,
k custom stlc at level 99,
y custom stlc at level 99,
left associativity).
Reserved Notation "'[' x ':=' s ']' t" (in custom stlc at level 20, x constr).
Notation "'[' x ':=' s ']' t" := (subst x s t) (in custom stlc).

(** Step *)
Reserved Notation "ty '-->' ty'" (at level 40).

(* lambdas are no longer values unless their bodies are values*)
(*  So we will start normalising the body*)
Inductive step : ty -> ty -> Prop :=
| ST_Abs : forall ty1 ty1' x K2,
ty1 --> ty1' ->
Lam x K2 ty1 --> Lam x K2 ty1'
| ST_AppAbs : forall x K2 v1 v2,
value v1 -> (* Problematic *)
value v2 ->
App (Lam x K2 v1) v2 --> subst x v2 v1
| ST_App1 : forall ty1 ty1' ty2,
ty1 --> ty1' ->
App ty1 ty2 --> App ty1' ty2
| ST_App2 : forall v1 ty2 ty2',
value v1 ->
ty2 --> ty2' ->
App v1 ty2 --> App v1 ty2'

where "ty '-->' ty'" := (step ty ty').
Hint Constructors step : core.

(** Multistep*)
Definition relation (X : Type) := X -> X -> Prop.
Inductive multi {X : Type} (R : relation X) : relation X :=
| multi_refl : forall (x : X), multi R x x
| multi_step : forall (x y z : X),
R x y ->
multi R y z ->
multi R x z.

Notation multistep := (multi step).
Notation "ty1 '-->*' ty2" := (multistep ty1 ty2) (at level 40).

(** The lemma I want to prove about substitutions*)
Lemma subst_preserves_step : forall X t t' v,
t --> t' -> value v -> subst X v t  -->* subst X v t'.
Proof.
intros X t t' v H H_value_v'.
generalize dependent t'.
induction t; intros t' Hstep; inversion Hstep; eauto; subst.
- shelve.
- admit. (* uhm, since t2 and \x:K2,v1 are already values, IHt1 and IHt2 don't tell us anything*)
- shelve.
- shelve.
Abort.


Code with capture avoiding substitutions

From Equations Require Import Equations.
Require Import Coq.Strings.String.
Require Import Coq.Lists.List.
Require Import Coq.micromega.Lia.
Import ListNotations.
Open Scope string_scope.
Open Scope list_scope.

(** kinds *)
Inductive kind :=
| Kind_Base : kind
| Kind_Arrow : kind -> kind -> kind.

(** Types *)
Inductive ty :=
| Var : string -> ty
| Lam : string -> kind -> ty -> ty
| App : ty -> ty -> ty.

(** Values *)
Inductive value : ty -> Prop :=
| v_neutral : forall ty1,
neutral ty1 ->
value ty1
| v_abs : forall x K2 ty1,
value ty1 ->
value (Lam x K2 ty1)

with neutral : ty -> Prop :=
| ne_var : forall x,
neutral (Var x)
| ne_app : forall ty1 ty2,
neutral ty1 ->
value ty2 ->
neutral (App ty1 ty2).

(** Subst *)
Fixpoint subst (X : string) (U T : ty) : ty :=
match T with
| Var Y =>
if X =? Y then U else Var Y
| Lam Y K1 T' =>
if X =? Y then Lam Y K1 T' else Lam Y K1 (subst X U T')
| App T1 T2 =>
App (subst X U T1) (subst X U T2)
end.

(** Capture avoiding substitution*)
Definition rename (X Y : string) (T : ty) := subst X (Var Y) T.

Fixpoint size (T : ty) : nat :=
match T with
| Var Y => 1
| Lam bX K T0 => 1 + size T0
| App T1 T2 => 1 + size T1 + size T2
end.

Fixpoint ftv (T : ty) : list string :=
match T with
| Var X =>
[X]
| Lam X K1 T' =>
remove string_dec X (ftv T')
| App T1 T2 =>
ftv T1 ++ ftv T2
end.

Definition fresh (X : string) (U T : ty) : string :=
"a" ++ X ++ (String.concat "" (ftv U)) ++ (String.concat "" (ftv T)).

Lemma fresh__X : forall X U T,
X <> fresh X U T.
Proof with eauto.
intros. intros Hcon.
induction X; induction (ftv U); induction (ftv T).
all: simpl in Hcon.
all: inversion Hcon; subst...
Qed.

Lemma fresh__S : forall X U T,
~ In (fresh X U T) (ftv U).
Proof. Abort.

Lemma fresh__T : forall X U T,
~ In (fresh X U T) (ftv T).
Proof. Abort.

Lemma rename_preserves_size : forall T X Y,
size T = size (rename X Y T).
Proof.
unfold rename.
induction T; intros; simpl; eauto.
- destruct (X =? s); eauto.
- destruct (X =? s); simpl; eauto.
Qed.

Equations? substTCA (X : string) (U T : ty) : ty by wf (size T) :=
substTCA X U (Var Y) =>
if X =? Y then U else Var Y ;
substTCA X U (Lam Y K T) =>
if X =? Y
then
Lam Y K T
else
if existsb (eqb Y) (ftv U)
then
let Y' := fresh X U T in
let T' := rename Y Y' T in
Lam Y' K (substTCA X U T')
else
Lam Y K (substTCA X U T) ;
substTCA X U (App T1 T2) =>
App (substTCA X U T1) (substTCA X U T2)
.
Proof.
all: try solve
[ lia
|| replace T' with (rename Y Y' T); eauto; rewrite <- rename_preserves_size; eauto
].
Qed.

(** Notation *)
Declare Custom Entry stlc.
Notation "<{ e }>" := e (e custom stlc at level 99).
Notation "( x )" := x (in custom stlc, x at level 99).
Notation "x" := x (in custom stlc at level 0, x constr at level 0).
Notation "x y" := (App x y) (in custom stlc at level 1, left associativity).
Notation "\ x : k , y" :=
(Lam x k y) (in custom stlc at level 90, x at level 99,
k custom stlc at level 99,
y custom stlc at level 99,
left associativity).
Reserved Notation "'[' x ':=' s ']' t" (in custom stlc at level 20, x constr).
Notation "'[' x ':=' s ']' t" := (subst x s t) (in custom stlc).

(** Step *)
Reserved Notation "ty '-->' ty'" (at level 40).

(* lambdas are no longer values unless their bodies are values*)
(*  So we will start normalising the body*)
Inductive step : ty -> ty -> Prop :=
| ST_Abs : forall ty1 ty1' x K2,
ty1 --> ty1' ->
Lam x K2 ty1 --> Lam x K2 ty1'
| ST_AppAbs : forall x K2 v1 v2,
value v1 -> (* Problematic *)
value v2 ->
App (Lam x K2 v1) v2 --> substTCA x v2 v1
| ST_App1 : forall ty1 ty1' ty2,
ty1 --> ty1' ->
App ty1 ty2 --> App ty1' ty2
| ST_App2 : forall v1 ty2 ty2',
value v1 ->
ty2 --> ty2' ->
App v1 ty2 --> App v1 ty2'

where "ty '-->' ty'" := (step ty ty').
Hint Constructors step : core.

(** Multistep*)
Definition relation (X : Type) := X -> X -> Prop.
Inductive multi {X : Type} (R : relation X) : relation X :=
| multi_refl : forall (x : X), multi R x x
| multi_step : forall (x y z : X),
R x y ->
multi R y z ->
multi R x z.

Notation multistep := (multi step).
Notation "ty1 '-->*' ty2" := (multistep ty1 ty2) (at level 40).

(** The lemma I want to prove about substitutions*)
Lemma subst_preserves_step : forall X t t' v,
t --> t' -> value v -> subst X v t  -->* subst X v t'.
Proof.
intros X t t' v H H_value_v'.
generalize dependent t'.
induction t; intros t' Hstep; inversion Hstep; eauto; subst.
- shelve.
- rename t2 into v2. admit. (* uhm, since t2 and \x:K2,v1 are already values, IHt1 and IHt2 don't tell us anything*)
- shelve.
- shelve.
Abort.

• (Your definition of substitution is wrong because it does not avoid capture.) Commented Jul 31 at 9:56
• @NaïmFavier yes, we are assuming for now that is not where the problem is coming from in not being able to prove it. Do you maybe have some insights into that? But I shall replace it with the TAC version in the question. Commented Jul 31 at 10:03
• That's not the problem, just something worth pointing out. It's fine to stick with the simple version if you mention this in the question. Commented Jul 31 at 10:04
• Please edit your question so that it present a coherent piece of text. The "Update" section should be folded into the question, as we discourage a "diary of my thoughts" type of questions. Right now, when someone starts reading your question, they see "it is false", and cannot possibly know what you're referring to. Commented Aug 1 at 7:27
• Also, images are discouraged. please replace that with text. Commented Aug 1 at 7:28