Coral.SubstEnv: environments of terms, viewed as sequences of substitutions

Author: Benoît Montagu

Synopsis: Environments of terms, viewed as sequences of substitutions.

Require Import Infrastructure.
Require Import Env.
Require Import EvalFacts.

Definition of subst_env

subst_env e t performs the sequence of substitutions recorded in e on the term t.

Fixpoint subst_env (e: env term) (t: term) :=
  match e with
  | nil ⇒ t
  | (x, u) :: e ⇒ subst_env e (subst u x t)
  end.

Lemma subst_env_one x u t:
  subst_env (x ¬ u) t = subst u x t.
Proof.
  reflexivity.
Qed.

Lemma subst_env_app e1 e2 t:
  subst_env (e1 ++ e2) t = subst_env e2 (subst_env e1 t).
Proof.
  revert t. env induction e1; intros; simpl; auto.
Qed.

If t has no free variables, then applying subst_env on t has no effect.

Lemma subst_env_closed e t:
  fv t [<=] empty →
  subst_env e t = t.
Proof.
  intro Hfv. env induction e; simpl in *; auto.
  - rewrite subst_fresh_eq; auto. fsetdec.
Qed.

Lemma closed_env_get e x t:
  all_env (fun t ⇒ fv t [<=] empty) e →
  get x e = Some t →
  fv t [<=] empty.
Proof.
  intros. apply (all_env_get (fun t' ⇒ fv t' [<=] empty) e x t); auto.
Qed.

Hint Resolve closed_env_get : core.

Free variables of an environment

Free variables of an environments.

Fixpoint fv_env (e: env term) { struct e } :=
  match e with
  | nil ⇒ empty
  | (x, t) :: e ⇒ fv_env e `union ` diff (fv t) (dom e)
  end.

If e contains only closed terms, then e has no free variable.

Lemma closed_env_fv_env e:
  all_env (fun t ⇒ fv t [<=] empty) e →
  fv_env e [<=] empty.
Proof.
  intro H. env induction e; simpl in ×.
  - fsetdec.
  - destruct H as [Hfv Hclosed].
    rewrite IHe; auto. fsetdec.
Qed.

The free variables of subst_env e t are larger than the free variables of t minus the domain of e.

Lemma subst_env_fv_lower e t:
  diff (fv t) (dom e) [<=] fv (subst_env e t).
Proof.
  revert t.
  env induction e; intros; simpl.
  - fsetdec.
  - rewrite <- IHe. rewrite <- fv_subst_lower. fsetdec.
Qed.

The free variables of subst_env e t are smaller than the free variables of e unioned with the free variables of t from which the domain of e is removed.

Lemma subst_env_fv_upper e t:
  fv (subst_env e t) [<=] fv_env e `union ` diff (fv t) (dom e).
Proof.
  revert t.
  env induction e; intros; simpl.
  - fsetdec.
  - rewrite IHe. rewrite fv_subst_upper. fsetdec.
Qed.

If e contains only closed terms, then the free variables of subst_env e t are the free variables of t minus the domain of e.

Lemma subst_env_fv_closed e t:
  all_env (fun t ⇒ fv t [<=] empty) e →
  fv (subst_env e t) [=] diff (fv t) (dom e).
Proof.
  intro Hclosed.
  assert (fv (subst_env e t) [<=] diff (fv t) (dom e)).
  { rewrite subst_env_fv_upper. apply closed_env_fv_env in Hclosed. fsetdec. }
  assert (diff (fv t) (dom e) [<=] fv (subst_env e t)) by auto using subst_env_fv_lower.
  fsetdec.
Qed.

If t is closed, then subst_env has no effect on t.

Lemma subst_env_closed_eq e t:
  fv t [<=] empty →
  subst_env e t = t.
Proof.
  revert t. env induction e; simpl; intros; auto.
  rewrite subst_fresh_eq; auto. fsetdec.
Qed.

If e contains only closed values and if the free variables of t are contained in the domain of e, then subst_env e t is a closed term.

Lemma subst_env_closed_fv e t:
  all_env (fun t ⇒ fv t [<=] empty) e →
  fv t [<=] dom e →
  fv (subst_env e t) [<=] empty.
Proof.
  intros Hclosed Hfv. rewrite subst_env_fv_closed; auto. fsetdec.
Qed.

Congruence properties for subst_env

Lemma subst_env_BVar e n:
  subst_env e (BVar n) = BVar n.
Proof.
  env induction e; simpl; auto.
Qed.

Lemma subst_env_Var_None e x:
  get x e = None →
  subst_env e (Var x) = Var x.
Proof.
  intro Hx. env induction e; simpl in *; auto.
  - destruct (x == x0); subst.
    + discriminate.
    + rewrite IHe; auto.
Qed.

Lemma subst_env_Var_Some e x t:
  fv t [<=] empty →
  get x e = Some t →
  subst_env e (Var x) = t.
Proof.
  intros Hfv H. env induction e; simpl in ×.
  - discriminate.
  - destruct (x == x0); subst; auto.
    inversion H; subst. apply subst_env_closed_eq. assumption.
Qed.

Lemma subst_env_Let e t1 t2:
  subst_env e (Let t1 t2) = Let (subst_env e t1) (subst_env e t2).
Proof.
  revert t1 t2.
  env induction e; simpl; intros; auto.
Qed.

Lemma subst_env_Lam e t:
  subst_env e (Lam t) = Lam (subst_env e t).
Proof.
  revert t.
  env induction e; simpl; intros; auto.
Qed.

Lemma subst_env_App e t1 t2:
  subst_env e (App t1 t2) = App (subst_env e t1) (subst_env e t2).
Proof.
  revert t1 t2.
  env induction e; simpl; intros; auto.
Qed.

Lemma subst_env_Unit e:
  subst_env e Unit = Unit.
Proof.
  env induction e; simpl; intros; auto.
Qed.

Lemma subst_env_Pair e t1 t2:
  subst_env e (Pair t1 t2) = Pair (subst_env e t1) (subst_env e t2).
Proof.
  revert t1 t2.
  env induction e; simpl; intros; auto.
Qed.

Lemma subst_env_Fst e t:
  subst_env e (Fst t) = Fst (subst_env e t).
Proof.
  revert t.
  env induction e; simpl; intros; auto.
Qed.

Lemma subst_env_Snd e t:
  subst_env e (Snd t) = Snd (subst_env e t).
Proof.
  revert t.
  env induction e; simpl; intros; auto.
Qed.

Lemma subst_env_InjL e t:
  subst_env e (InjL t) = InjL (subst_env e t).
Proof.
  revert t.
  env induction e; simpl; intros; auto.
Qed.

Lemma subst_env_InjR e t:
  subst_env e (InjR t) = InjR (subst_env e t).
Proof.
  revert t.
  env induction e; simpl; intros; auto.
Qed.

Lemma subst_env_Match e t t1 t2:
  subst_env e (Match t t1 t2) = Match (subst_env e t) (subst_env e t1) (subst_env e t2).
Proof.
  revert t t1 t2.
  env induction e; simpl; intros; auto.
Qed.

Other properties of subst_env

Assume e and e' only contain closed terms, and assume that the free variables of t are contained in the domain of e. If e' extends e, then subst_env e t and subst_env e' t coincide.

Lemma subst_env_leq_env e e' t:
  leq_env e e' →
  all_env (fun t ⇒ fv t [<=] empty) e →
  all_env (fun t ⇒ fv t [<=] empty) e' →
  fv t [<=] dom e →
  subst_env e t = subst_env e' t.
Proof.
  induction t; simpl; intros Hleq Hclosed Hclosed' Hfv; auto.
  - repeat rewrite subst_env_BVar. reflexivity.
  - case_eq (get x e); intros.
    + rewrite (subst_env_Var_Some e x t); eauto using closed_env_get.
      rewrite (subst_env_Var_Some e' x t); eauto using closed_env_get.
    + apply get_notin_dom in H. fsetdec.
  - repeat rewrite subst_env_Let. f_equal.
    + eapply IHt1; eauto. fsetdec.
    + eapply IHt2; eauto. fsetdec.
  - repeat rewrite subst_env_Lam. f_equal.
    eapply IHt; eauto.
  - repeat rewrite subst_env_App. f_equal.
    + eapply IHt1; eauto. fsetdec.
    + eapply IHt2; eauto. fsetdec.
  - repeat rewrite subst_env_Unit. reflexivity.
  - repeat rewrite subst_env_Pair. f_equal.
    + eapply IHt1; eauto. fsetdec.
    + eapply IHt2; eauto. fsetdec.
  - repeat rewrite subst_env_Fst. f_equal.
    eapply IHt; eauto.
  - repeat rewrite subst_env_Snd. f_equal.
    eapply IHt; eauto.
  - repeat rewrite subst_env_InjL. f_equal.
    eapply IHt; eauto.
  - repeat rewrite subst_env_InjR. f_equal.
    eapply IHt; eauto.
  - repeat rewrite subst_env_Match. f_equal.
    + eapply IHt1; eauto. fsetdec.
    + eapply IHt2; eauto. fsetdec.
    + eapply IHt3; eauto. fsetdec.
Qed.

Lemma lc_env_get e x t:
  all_env lc e →
  get x e = Some t →
  lc t.
Proof.
  intros. eapply all_env_get; eauto.
Qed.

If e contains only locally-closed terms and if t is locally-closed, then so is subst_env e t.

Lemma subst_env_lc e t:
  all_env lc e →
  lc t →
  lc (subst_env e t).
Proof.
  revert t. env induction e; intros; simpl in *; auto.
  - destruct H. apply IHe; auto with lngen.
Qed.

If e contains only locally-closed terms, then subst_env e commutes with open.

Lemma subst_env_open e t1 t2:
  all_env lc e →
  subst_env e (open t1 t2) = open (subst_env e t1) (subst_env e t2).
Proof.
  revert t1 t2. env induction e; intros; simpl; auto.
  simpl in H. destruct H.
  rewrite subst_open; eauto using lc_env_get.
Qed.

Lemma eval_subst_env_closed e t v:
  all_env (fun t ⇒ fv t [<=] empty) e →
  fv t [<=] dom e →
  eval (subst_env e t) v →
  fv v [<=] empty.
Proof.
  intros Hclosed Hfv Heval.
  rewrite (eval_fv _ _ Heval).
  rewrite subst_env_fv_upper.
  apply closed_env_fv_env in Hclosed.
  fsetdec.
Qed.

Unfolding lemma for the evaluation of subst_env e t.

Lemma eval_subst_env_iff e t v:
  all_env good_value e →
  eval (subst_env e t) v ↔
  match t with
  | BVar _ ⇒ False
  | Var x ⇒ get x e = Some v
  | Let t1 t2 ⇒
    ∃ t1', eval (subst_env e t1) t1' ∧ eval (open (subst_env e t2) t1') v
  | Lam _ ⇒ subst_env e t = v
  | App t1 t2 ⇒
    ∃ t1' t2', eval (subst_env e t1) (Lam t1') ∧ eval (subst_env e t2) t2'
               ∧ eval (open t1' t2') v
  | Unit ⇒ v = Unit
  | Pair t1 t2 ⇒
    ∃ t1' t2', eval (subst_env e t1) t1' ∧ eval (subst_env e t2) t2'
               ∧ v = Pair t1' t2'
  | Fst t ⇒ ∃ t2', eval (subst_env e t) (Pair v t2')
  | Snd t ⇒ ∃ t1', eval (subst_env e t) (Pair t1' v)
  | InjL t ⇒ ∃ t', eval (subst_env e t) t' ∧ InjL t' = v
  | InjR t ⇒ ∃ t', eval (subst_env e t) t' ∧ InjR t' = v
  | Match t t1 t2 ⇒
    (∃ t', eval (subst_env e t) (InjL t') ∧ eval (open (subst_env e t1) t') v )
    ∨ (∃ t', eval (subst_env e t) (InjR t') ∧ eval (open (subst_env e t2) t') v )
  end.
Proof.
  intro Hgood.
  rewrite eval_iff. destruct t.
  - rewrite subst_env_BVar. tauto.
  - case_eq (get x e); intros.
    + assert (good_value t) as Hvgood by (eapply all_env_get; eauto).
      assert (is_value t) as Hval by auto.
      rewrite (subst_env_Var_Some e x t); auto.
      destruct t; simpl in Hval; try contradiction.
      × split; intro; congruence.
      × split; intro; congruence.
      × { split; intro H'.
          - destruct H' as [t1' [t2' [Heval1 [Heval2 Heq]]]].
            apply eval_of_value in Heval1; [| tauto].
            apply eval_of_value in Heval2; [| tauto].
            congruence.
          - ∃ t1, t2. split; [ apply eval_refl; tauto | split; [ apply eval_refl; tauto |]].
            congruence.
        }
      × { split; intro H'.
          - destruct H' as [t' [Heval Heq]].
            apply eval_of_value in Heval; auto. congruence.
          - ∃ t; split; [ apply eval_refl; tauto | congruence ].
        }
      × { split; intro H'.
          - destruct H' as [t' [Heval Heq]].
            apply eval_of_value in Heval; auto. congruence.
          - ∃ t; split; [ apply eval_refl; tauto | congruence ].
        }
    + rewrite (subst_env_Var_None e x); auto.
      split; intro.
      × contradiction.
      × congruence.
  - rewrite subst_env_Let. tauto.
  - rewrite subst_env_Lam. tauto.
  - rewrite subst_env_App. tauto.
  - rewrite subst_env_Unit. tauto.
  - rewrite subst_env_Pair. tauto.
  - rewrite subst_env_Fst. tauto.
  - rewrite subst_env_Snd. tauto.
  - rewrite subst_env_InjL. tauto.
  - rewrite subst_env_InjR. tauto.
  - rewrite subst_env_Match. tauto.
Qed.

Results about extended values

Lemma is_value_weaken t :
  is_value t →
  is_extended_value t.
Proof.
  intro H. induction t; simpl in *; tauto.
Qed.

Lemma subst_env_is_extended_value_iff e t :
  all_env good_value e →
  is_extended_value (subst_env e t) ↔ is_extended_value t.
Proof.
  intros Hgood.
  induction t; simpl in ×.
  - rewrite subst_env_BVar. simpl. tauto.
  - case_eq (get x e); intros.
    + assert (good_value t) as [Hlc [Hxval Hxclosed]].
      { eapply all_env_get; eauto. }
      rewrite (subst_env_Var_Some e x t); simpl; auto.
      apply is_value_weaken in Hxval. tauto.
    + rewrite subst_env_Var_None; simpl; tauto.
  - rewrite subst_env_Let. simpl. tauto.
  - rewrite subst_env_Lam. simpl. tauto.
  - rewrite subst_env_App. simpl. tauto.
  - rewrite subst_env_Unit. simpl. tauto.
  - rewrite subst_env_Pair. simpl.
    rewrite IHt1; auto; try fsetdec.
    rewrite IHt2; auto; try fsetdec.
  - rewrite subst_env_Fst. simpl. tauto.
  - rewrite subst_env_Snd. simpl. tauto.
  - rewrite subst_env_InjL. simpl. auto.
  - rewrite subst_env_InjR. simpl. auto.
  - rewrite subst_env_Match. simpl. tauto.
Qed.

Under suitable conditions, subst_env e t is a value iff t is an extended value.

Lemma subst_env_is_value_iff e t :
  all_env good_value e →
  fv t [<=] dom e →
  is_value (subst_env e t) ↔ is_extended_value t.
Proof.
  intros Hgood Hfv.
  induction t; simpl in ×.
  - rewrite subst_env_BVar. simpl. tauto.
  - case_eq (get x e); intros.
    + assert (good_value t) as [Hlc [Hxval Hxclosed]].
      { eapply all_env_get; eauto. }
      rewrite (subst_env_Var_Some e x t); simpl; tauto.
    + exfalso. apply get_notin_dom in H. fsetdec.
  - rewrite subst_env_Let. simpl. tauto.
  - rewrite subst_env_Lam. simpl. tauto.
  - rewrite subst_env_App. simpl. tauto.
  - rewrite subst_env_Unit. simpl. tauto.
  - rewrite subst_env_Pair. simpl.
    rewrite IHt1; auto; try fsetdec.
    rewrite IHt2; auto; try fsetdec.
  - rewrite subst_env_Fst. simpl. tauto.
  - rewrite subst_env_Snd. simpl. tauto.
  - rewrite subst_env_InjL. simpl. auto.
  - rewrite subst_env_InjR. simpl. auto.
  - rewrite subst_env_Match. simpl. tauto.
Qed.

The property of being a value is preserved by subst_env.

Lemma subst_env_is_value e t :
  is_value t →
  is_value (subst_env e t).
Proof.
  intros Hval.
  induction t; simpl in *; try contradiction.
  - rewrite subst_env_Lam. simpl. trivial.
  - rewrite subst_env_Unit. simpl. trivial.
  - rewrite subst_env_Pair. simpl. tauto.
  - rewrite subst_env_InjL. simpl. tauto.
  - rewrite subst_env_InjR. simpl. tauto.
Qed.

Properties about subst_env and evaluation

step stable under subst_env.

Lemma step_subst_env e t1 t2:
  all_env lc e →
  step t1 t2 →
  step (subst_env e t1) (subst_env e t2).
Proof.
  intros Hlc Hstep. induction Hstep.
  - rewrite subst_env_App. rewrite subst_env_Lam. rewrite subst_env_open; auto.
    constructor; auto using subst_env_is_value.
  - repeat rewrite subst_env_App. constructor; auto.
  - repeat rewrite subst_env_App. constructor; auto using subst_env_is_value.
  - rewrite subst_env_Let. rewrite subst_env_open; auto.
    constructor; auto using subst_env_is_value.
  - repeat rewrite subst_env_Let. constructor; auto.
  - rewrite subst_env_Fst. rewrite subst_env_Pair. constructor; auto using subst_env_is_value.
  - rewrite subst_env_Snd. rewrite subst_env_Pair. constructor; auto using subst_env_is_value.
  - repeat rewrite subst_env_Pair. constructor; auto.
  - repeat rewrite subst_env_Pair. constructor; auto using subst_env_is_value.
  - repeat rewrite subst_env_Fst. constructor; auto.
  - repeat rewrite subst_env_Snd. constructor; auto.
  - repeat rewrite subst_env_InjL. constructor; auto.
  - repeat rewrite subst_env_InjR. constructor; auto.
  - rewrite subst_env_Match. rewrite subst_env_InjL. rewrite subst_env_open; auto.
    constructor; auto using subst_env_is_value.
  - rewrite subst_env_Match. rewrite subst_env_InjR. rewrite subst_env_open; auto.
    constructor; auto using subst_env_is_value.
  - repeat rewrite subst_env_Match. constructor; auto.
Qed.

steps stable under subst_env.

Lemma steps_subst_env e t1 t2:
  all_env lc e →
  steps t1 t2 →
  steps (subst_env e t1) (subst_env e t2).
Proof.
  intros Hgood Hsteps. induction Hsteps.
  - reflexivity.
  - econstructor; eauto using step_subst_env.
Qed.

eval stable under subst_env.

Lemma eval_subst_env e t v:
  all_env lc e →
  eval t v →
  eval (subst_env e t) (subst_env e v).
Proof.
  intros Hgood [Hsteps Hval]. split.
  - apply steps_subst_env; auto.
  - apply subst_env_is_value; auto.
Qed.