# Program equivalence and substitution

Hello,

I have the following question (look for “QUESTION” below) involving the relationship between evaluation and substitution. The result seems intuitive but I can’t prove it, and I wonder if I’m missing something basic. This feels like the kind of thing that should be well-known, so … help! Any pointers will be appreciated.

Thanks!

Cheers,
Nicolas

``````Require Import Coq.Arith.PeanoNat.

(* A small language with variables, "let" and int constants. *)

Definition ident := nat.

Inductive exp :=
| Var : ident -> exp
| Let : nat -> exp -> exp -> exp
| Int : nat -> exp.

(* A substitution operation:
[subst m e a] substitues every occurence of [Var m] in [a] by [e]. *)

Fixpoint subst (m : ident) (e a : exp) :=
match a with
| Var n => if Nat.eq_dec n m then e else Var n
| Let n a b =>
Let n (subst m e a) (if Nat.eq_dec n m then b else subst m e b)
| Int c => Int c
end.

(* The evaluation rules. *)

Inductive eval : exp -> nat -> Prop :=
| E_let : forall n a b m, eval (subst n a b) m -> eval (Let n a b) m
| E_int : forall c, eval (Int c) c.

(* Definition of program equivalence. *)

Definition equiv (e1 e2 : exp) := forall n,
eval e1 n <-> eval e2 n.

(* Definition of free vars and closedness. *)

Inductive fv : ident -> exp -> Prop :=
| F_var : forall n, fv n (Var n)
| F_let_a : forall n m a b, fv n a -> fv n (Let m a b)
| F_let_b : forall n m a b, n <> m -> fv n b -> fv n (Let m a b).

Definition closed e :=
~ exists n, fv n e.

(* QUESTION: the following result seems true, but how to prove it?? *)

Lemma eval_subst : forall x a a' b,
closed a ->
closed a' ->
equiv a a' ->
equiv (subst x a b) (subst x a' b).
``````

I’m not sure if a counter example can be built from this, but

``````  | Let n a b =>
Let n (subst m e a) (if Nat.eq_dec n m then b else subst m e b)
``````

this produces strange results when `n` appears in `e`

Indeed… this is why I required `a` and `a'` to be closed (no free variables) in the statement of the result… but perhaps I am missing something else as well…

Thanks!
Nicolas

Phew!! Several hours later, I managed to prove it. I am surprised by how complicated it was (perhaps I missed a simpler way). The main point was to generalise the statement so that the induction could work. The final statement that I proved was:

``````Corollary eval_subst : forall x a a' e,
closed a ->
closed a' ->
equiv a a' ->
(forall z, fv z e -> z = x) ->
equiv (subst x a e) (subst x a' e).
``````

(the hypothesis that at most `x` is free in `e` is purely for convenience and can be lifted).

Anyway, details are below for future reference

Cheers,
Nicolas

``````Require Import Coq.Arith.PeanoNat.
Require Import Coq.Lists.List.

(* A small language with variables, "let" and int constants. *)

Definition ident := nat.

Inductive exp :=
| Var : ident -> exp
| Let : ident -> exp -> exp -> exp
| Int : nat -> exp.

(* A substitution operation:
[subst m e a] substitues every occurence of [Var m] in [a] by [e]. *)

Fixpoint subst (m : ident) (e a : exp) :=
match a with
| Var n => if Nat.eq_dec n m then e else Var n
| Let n a b =>
Let n (subst m e a) (if Nat.eq_dec n m then b else subst m e b)
| Int c => Int c
end.

(* The evaluation rules. *)

Inductive eval : exp -> nat -> Prop :=
| E_let : forall x a b m, eval (subst x a b) m -> eval (Let x a b) m
| E_int : forall c, eval (Int c) c.

(* Definition of program equivalence. *)

Definition equiv (e1 e2 : exp) := forall n,
eval e1 n <-> eval e2 n.

(* Definition of free vars and closedness. *)

Inductive fv : ident -> exp -> Prop :=
| F_var : forall n, fv n (Var n)
| F_let_a : forall n m a b, fv n a -> fv n (Let m a b)
| F_let_b : forall n m a b, n <> m -> fv n b -> fv n (Let m a b).

Definition closed e :=
~ exists n, fv n e.

(* QUESTION: the following result seems true, but how to prove it?? *)

Fixpoint msubst c e :=
match c with
| nil => e
| cons (x, t) c => msubst c (subst x t e)
end.

Fixpoint drop {A} (x : ident) (c : list (ident * A)) :=
match c with
| nil => nil
| cons (y, v) c =>
if Nat.eq_dec x y then drop x c else cons (y, v) (drop x c)
end.

Inductive closed_env : list (ident * exp) -> Prop :=
| CE_nil : closed_env nil
| CE_cons : forall x e c, closed e -> closed_env c -> closed_env (cons (x, e) c).

Inductive equiv_env : list (ident * exp) -> list (ident * exp) -> Prop :=
| EE_nil : equiv_env nil nil
| EE_cons : forall x e1 e2 c1 c2,
closed e1 -> closed e2 -> equiv e1 e2 ->
equiv_env c1 c2 -> equiv_env (cons (x, e1) c1) (cons (x, e2) c2).

Lemma equiv_let : forall x e1 e2,
equiv (Let x e1 e2) (subst x e1 e2).
Proof. split; intros * H; inversion H; subst; auto; now constructor. Qed.

Lemma trans_equiv : forall t1 t2 t3,
equiv t1 t2 -> equiv t2 t3 -> equiv t1 t3.
Proof. intros * H H' n. now transitivity (eval t2 n). Qed.

Lemma sym_equiv : forall e1 e2, equiv e1 e2 -> equiv e2 e1.
Proof. intros * H n. now symmetry. Qed.

Lemma equiv_env_drop : forall i c1 c2,
equiv_env c1 c2 -> equiv_env (drop i c1) (drop i c2).
Proof.
intros * H. induction H; simpl.
- constructor.
- destruct (Nat.eq_dec i x) as [<-|]; auto.
constructor; auto.
Qed.

Lemma subst_let : forall e2 x i u e1,
x <> i -> subst x u (Let i e1 e2) = Let i (subst x u e1) (subst x u e2).
Proof.
induction e2; intros * H; simpl.
- simpl. destruct (Nat.eq_dec i0 x) as [<-|]; try contradiction; auto.
- simpl. destruct (Nat.eq_dec i0 x) as [<-|]; try contradiction; auto.
- simpl. destruct (Nat.eq_dec i x) as [<-|]; try contradiction; auto.
Qed.

Lemma msubst_let : forall c x t1 t2,
msubst c (Let x t1 t2) = Let x (msubst c t1) (msubst (drop x c) t2).
Proof.
induction c; intros *.
- simpl; auto.
- destruct a as (y,v).
simpl.
destruct (Nat.eq_dec x y) as [<-|].
+ rewrite IHc; auto.
+ rewrite IHc. f_equal.
Qed.

Lemma msubst_int : forall c n, msubst c (Int n) = Int n.
Proof. induction c; auto. intros. destruct a. simpl. now apply IHc. Qed.

Lemma refl_equiv : forall e, equiv e e.
Proof. intros * n. reflexivity. Qed.

Fixpoint lookup {A} x (c : list (ident * A)) : option A :=
match c with
| nil => None
| cons (y, v) c =>
if Nat.eq_dec x y then
Some v
else
lookup x c
end.

Lemma equiv_env_closed : forall c1 c2,
equiv_env c1 c2 -> closed_env c1 /\ closed_env c2.
Proof. intros * H. split; induction H; constructor; auto. Qed.

Lemma equiv_env_lookup : forall c1 c2 x,
equiv_env c1 c2 -> match lookup x c1, lookup x c2 with
| Some a1, Some a2 => equiv a1 a2
| None, None => True
| _, _ => False
end.
Proof.
intros * H. induction H; simpl; auto.
destruct (Nat.eq_dec x x0) as [<-|]; auto.
Qed.

Lemma fv_closed : forall e x u,
~ fv x e ->
subst x u e = e.
Proof.
induction e; intros * H; auto.
- simpl. destruct (Nat.eq_dec i x) as [<-|].
+ exfalso. apply H. apply F_var.
+ auto.
- simpl. destruct (Nat.eq_dec i x) as [<-|].
+ rewrite IHe1; auto. intro HH. apply H.
apply F_let_a. auto.
+ rewrite IHe1.
* rewrite IHe2; auto. intro HH. apply H. apply F_let_b; auto.
* intro HH. apply H. apply F_let_a. auto.
Qed.

Corollary subst_closed : forall e x u,
closed e ->
subst x u e = e.
Proof. intros * H. apply fv_closed. intro HH. apply H. exists x. auto. Qed.

Lemma subst_subst : forall i j x y e,
i <> j ->
closed x ->
closed y ->
subst i x (subst j y e) = subst j y (subst i x e).
Proof.
induction e; intros * Hij Hx Hy; simpl; auto.
- destruct (Nat.eq_dec i0 j) as [<-|]; destruct (Nat.eq_dec i0 i) as [<-|]; auto.
+ rewrite subst_closed; auto. simpl. destruct (Nat.eq_dec i0 i0); try contradiction; auto.
+ simpl. destruct (Nat.eq_dec i0 i0); try contradiction. rewrite subst_closed; auto.
+ simpl. destruct (Nat.eq_dec i0 i); destruct (Nat.eq_dec i0 j); try contradiction; auto.
- f_equal.
+ apply IHe1; auto.
+ destruct (Nat.eq_dec i0 i); destruct (Nat.eq_dec i0 j); auto.
Qed.

Lemma subst_msubst : forall c i x e,
closed x ->
closed_env c ->
subst i x (msubst (drop i c) e) = msubst (drop i c) (subst i x e).
Proof.
induction c; intros * Hx Hc; simpl; auto. destruct a.
destruct (Nat.eq_dec i i0) as [<-|]; auto.
+ apply IHc. auto. inversion Hc. auto.
+ simpl. rewrite IHc; auto.
rewrite subst_subst; auto. inversion Hc; auto. inversion Hc; auto.
Qed.

Lemma msubst_closed : forall c e,
closed e ->
msubst c e = e.
Proof.
induction c; intros * H; simpl; auto.
destruct a. rewrite subst_closed; auto.
Qed.

Lemma msubst_var : forall c x,
closed_env c ->
msubst c (Var x) = match lookup x c with
| Some a => a
| None => Var x
end.
Proof.
intros * H. induction H.
- simpl. auto.
- simpl. destruct (Nat.eq_dec x x0).
+ apply msubst_closed; auto.
+ rewrite IHclosed_env. auto.
Qed.

Lemma closed_letin : forall e2 x e1,
closed e1 ->
(forall y, fv y e2 -> y = x) ->
closed (Let x e1 e2).
Proof.
induction e2; intros * H Hfv (x & Hx); inversion Hx; subst.
- apply H. exists x. auto.
- specialize (Hfv x H5) as <-. contradiction.
- apply H. exists x. auto.
- specialize (Hfv x H5) as <-. contradiction.
- apply H. exists x. auto.
- inversion H5.
Qed.

Lemma fv_subst : forall e x y u,
fv y (subst x u e) -> fv y u \/ (fv y e /\ y <> x).
Proof.
induction e; intros * H; simpl in H.
- destruct (Nat.eq_dec i x) as [<-|].
+ left. auto.
+ inversion H; subst. auto.
- inversion H; subst.
+ specialize (IHe1 _ _ _ H2) as [Ha | [Hb Hc]].
* left. auto.
* right. split; auto. apply F_let_a. auto.
+ destruct (Nat.eq_dec i x) as [<-|].
* right. split; auto. apply F_let_b; auto.
* specialize (IHe2 _ _ _ H5) as [Ha | [Hb Hc]].
** left. auto.
** right. split; auto. apply F_let_b; auto.
- inversion H.
Qed.

Lemma closed_subst : forall e x u,
closed u ->
(forall y, fv y e -> y = x) ->
closed (subst x u e).
Proof.
induction e; intros * Hu He.
- simpl. destruct (Nat.eq_dec i x) as [<-|]; auto.
destruct He with i. constructor. contradiction.
- simpl. destruct (Nat.eq_dec i x) as [<-|].
+ apply closed_letin.
* apply IHe1; auto.
intros.
apply He.
constructor; auto.
* intros.
destruct (Nat.eq_dec y i) as [<-|]; auto.
apply He.
apply F_let_b; auto.
+ apply closed_letin.
* apply IHe1; auto.
intros.
apply He.
constructor; auto.
* intros.
pose proof (fv_subst _ _ _ _ H) as [Hyu|[Hy Hn]].
** exfalso. apply Hu. exists y; auto.
** destruct (Nat.eq_dec y i); auto.
destruct He with y. apply F_let_b; auto. contradiction.
- simpl. intros (a & Ha). inversion Ha.
Qed.

Definition dom {A B} (c : list (A * B)) := map fst c.

Lemma fv_msubst : forall c x e,
closed_env c -> fv x (msubst c e) -> fv x e /\ ~ In x (dom c).
Proof.
induction c; intros * Hc Hfv.
- simpl. split; auto.
- simpl. split.
+ destruct a.
simpl in Hfv.
destruct IHc with x (subst i e0 e); auto.
inversion Hc; auto.
pose proof (fv_subst _ _ _ _ H) as [Ha | [Hb1 Hb2]]; auto.
inversion Hc. exfalso. apply H3. exists x. auto.
+ intros [A|B]; destruct a.
* simpl in *. subst.
destruct IHc with x (subst x e0 e).
** inversion Hc. auto.
** auto.
** pose proof (fv_subst _ _ _ _ H) as [A | [? B]].
*** inversion Hc. apply H3. exists x. auto.
* destruct IHc with x (subst i e0 e).
** inversion Hc. auto.
** auto.
Qed.

Lemma closed_env_drop : forall i c, closed_env c -> closed_env (drop i c).
Proof.
induction c; intros * H.
- simpl. auto.
- destruct a. simpl.
destruct (Nat.eq_dec i i0) as [<-|].
+ apply IHc. inversion H. auto.
+ constructor. inversion H. auto. apply IHc. inversion H. auto.
Qed.

Lemma eval_msubst : forall e c1 c2,
equiv_env c1 c2 ->
closed (msubst c1 e) ->
closed (msubst c2 e) ->
equiv (msubst c1 e) (msubst c2 e).
Proof.
induction e; intros * H Hc1 Hc2.

- pose proof (equiv_env_closed _ _ H) as [H1 H2].
rewrite msubst_var; auto. rewrite msubst_var; auto.
pose proof (equiv_env_lookup _ _ i H) as HH.
destruct (lookup i c1); destruct (lookup i c2).
+ auto.
+ apply refl_equiv.

- rewrite msubst_let.
apply trans_equiv with (subst i (msubst c1 e1) (msubst (drop i c1) e2)).
apply equiv_let.
rewrite msubst_let.
apply trans_equiv with (subst i (msubst c2 e1) (msubst (drop i c2) e2));
[|apply sym_equiv, equiv_let].
replace (subst i (msubst c1 e1) (msubst (drop i c1) e2)) with
(msubst (cons (i, msubst c1 e1) (drop i c1)) e2).
+ replace (subst i (msubst c2 e1) (msubst (drop i c2) e2)) with
(msubst (cons (i, msubst c2 e1) (drop i c2)) e2).
rewrite msubst_let in Hc1, Hc2.
* apply IHe2.
** constructor.
*** intros (u & Hu). apply Hc1. exists u. apply F_let_a. auto.
*** intros (u & Hi). apply Hc2. exists u. apply F_let_a. auto.
*** apply IHe1. auto.
intros (u & Hu). apply Hc1. exists u. apply F_let_a. auto.
intros (u & Hu). apply Hc2. exists u. apply F_let_a. auto.
*** apply equiv_env_drop; auto.
** simpl.
rewrite <- subst_msubst.
*** intros (u & Hu). pose proof (fv_subst _ _ _ _ Hu) as [A|[B C]].
**** apply Hc1. exists u. apply F_let_a. auto.
**** apply Hc1. exists u. apply F_let_b; auto.
*** intros (u & Hu). apply Hc1. exists u. apply F_let_a. auto.
*** apply equiv_env_closed with (c1 := c1) (c2 := c2). auto.
** simpl.
rewrite <- subst_msubst.
*** intros (u & Hu). pose proof (fv_subst _ _ _ _ Hu) as [A|[B C]].
**** apply Hc2. exists u. apply F_let_a. auto.
**** apply Hc2. exists u. apply F_let_b; auto.
*** intros (u & Hu). apply Hc2. exists u. apply F_let_a. auto.
*** apply equiv_env_closed with (c1 := c1) (c2 := c2). auto.
* simpl. rewrite subst_msubst; auto.
intros (u & Hu). apply Hc2. exists u. rewrite msubst_let. apply F_let_a. auto.
apply equiv_env_closed with (c1 := c1) (c2 := c2); auto.
+ simpl. rewrite subst_msubst; auto.
* intros (u & Hu). apply Hc1. exists u. rewrite msubst_let. apply F_let_a. auto.
* apply equiv_env_closed with (c1 := c1) (c2 := c2); auto.

- rewrite msubst_int. rewrite msubst_int. apply refl_equiv.
Qed.

Corollary eval_subst : forall x a a' e,
closed a ->
closed a' ->
equiv a a' ->
(forall z, fv z e -> z = x) ->
equiv (subst x a e) (subst x a' e).
Proof.
intros * Ha Ha' Haa' Hc.
replace (subst x a e) with (msubst (cons (x, a) nil) e); auto.
replace (subst x a' e) with (msubst (cons (x, a') nil) e); auto.
apply eval_msubst.
- constructor; auto. constructor.
- simpl. apply closed_subst; auto.
- simpl. apply closed_subst; auto.
Qed.
``````
1 Like