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

要证明命题(X !-> 3) =[ <{ X := X + 2 }> ]=> (X !-> 5)，核心是贴合Imp的大步求值规则（ceval）展开推理，以下是完整的Coq证明过程及关键步骤说明：

完整证明代码 #

Goal (X !-> 3) =[ <{ X := X + 2 }> ]=> (X !-> 5).
Proof.
  (* 应用赋值语句的核心规则 E_Asgn，拆解为两个子目标：表达式求值、状态相等 *)
  apply E_Asgn.
  - (* 子目标1：验证初始状态下 X+2 求值为5 *)
    apply E_Plus.
    + apply E_Var. reflexivity. (* X在初始状态 (X!->3) 中的值为3 *)
    + apply E_Const. reflexivity. (* 常量2的求值结果为2 *)
    + reflexivity. (* 3+2=5，满足加法求值规则的前提 *)
  - (* 子目标2：验证赋值后的状态等于目标状态 (X!->5) *)
    unfold update. (* 展开状态更新函数的定义 *)
    extensionality y. (* 利用状态的外延性：两状态相等当且仅当所有变量取值一致 *)
    destruct (eqb y X) as [H_eq | H_neq].
    + rewrite H_eq. reflexivity. (* 当变量为X时，更新后的值为5，与目标状态一致 *)
    + rewrite H_neq. reflexivity. (* 当变量不为X时，取值与初始状态一致，目标状态未修改该变量，故相等 *)
Qed.

关键问题说明 #

你之前尝试apply E_Asgn失败，大概率是因为没有处理该规则的两个隐含前提：

1. 必须先证明表达式在初始状态下的求值结果（即X+2在X!->3中得到5）；
2. 必须证明赋值后的状态与目标状态完全相等（而非仅X的取值相等，Coq中状态是函数，需通过外延性证明所有变量取值一致）。

直接用t_update_eq无法完成证明，因为它仅能证明单个变量的取值，而命题要求的是整个状态的等价关系，必须通过extensionality策略覆盖所有变量的情况。

内容的提问来源于stack exchange，提问作者mindconnect.cc