Program equivalence and substitution

Using Coq
1

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! :slight_smile: 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).
Admitted.
2

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

3

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

4

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 :slight_smile:

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.
    + contradiction.
    + 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.
           *** contradiction.
      * destruct IHc with x (subst i e0 e).
        ** inversion Hc. auto.
        ** auto.
        ** contradiction.
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.
    + contradiction.
    + contradiction.
    + 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