subst_equiv.v

Ltac eq_ids :=
  repeat progress match goal with
                      [i1 : id, i2 : id |- _] => extend (eq_id_dec i1 i2)
                  end.

Lemma subst_aexp_equiv : forall i a1 a2 st,
      aeval st (subst_aexp i a2 a1) = aeval (update st i (aeval st a2)) a1.
Proof. induction a1; simpl; auto; unfold update; eq_ids; crush. Qed.

Hint Rewrite aeval_weakening subst_aexp_equiv.

Theorem subst_equiv : forall i1 i2 a1 a2,
                        var_not_used_in_aexp i1 a2 ->
                        cequiv (i2 ::= a2) (i2 ::= subst_aexp i1 a1 a2).
Proof. introv Hnu. split; inversion 1;
       match goal with [p : ((i2 ::= _) / _ || _) |- _] => inverts p end;
       apply E_Ass; crush.
Qed (* Note that this is stronger than the original statement of the property *).