如何证明 (X !-> 3) =[ <{ X := X + 2 }> ]=> (X !-> 5)？

Question

我知道如何使用软件基础第 1 卷中定义的 Imp 证明 3 + 2 = 5。

Definition plus2_3_is_5: Prop := forall (st: state),
  (X !-> 3) =[ <{ X := X + 2 }> ]=> st -> st X = 5.

Fact plus2_3_is_5_fact : plus2_3_is_5.
Proof.
  intros st H.
  inversion H. subst. simpl.
  apply t_update_eq. (* or use [reflexivity] *)
Qed.

但是当我将 plus2_3_is_5 定义为 (X !-> 3) =[ <{ X := X + 2 }> ]=> (X !-> 5) 时，我找不到证明。有人可以帮忙吗？

当我使用该提案时

forall (st: state),
  (X !-> 3) =[ <{ X := X + 2 }> ]=> st -> st X = 5.

表达3+2=5，我可以正确地得到证明。但是当我使用明显更简单的命题时

(X !-> 3) =[ <{ X := X + 2 }> ]=> (X !-> 5)

相反，我尝试过的每一种策略，例如应用E_Asgn、应用t_update_eq，都失败了。

Answer 1

我在 ayylien 的帮助下找到了解决方案。

Fact plus2_3_is_5_fact :
  (X !-> 3) =[ <{ X := X + 2 }> ]=> (X !-> 5).
Proof.
  assert (H: (X !-> 5; X !-> 3) = (X !-> 5)).
  { apply t_update_shadow. }
  rewrite <- H. 
  apply E_Asgn. reflexivity.
Qed.