Coq中同一变量多次赋值的两种求值关系示例构造问题

核心差异分析 #

先明确两种求值关系的本质区别：

• ceval1：多赋值采用递归更新后求值的策略，处理x::xs := a::es时，先递归求值xs := es得到新状态st'，再用st'计算表达式a的值，最后更新x。
• ceval2：多赋值采用初始状态求值的策略，处理x::xs := a::es时，直接用原始状态st计算表达式a的值，再递归求值xs := es得到st'，最后更新x。

用户之前的错误在于选择了重复变量的赋值（[X;X] := [ANum 1; ANum 2]），这种情况下ceval2的规则要求两个表达式都用初始状态计算，但最终赋值的顺序会覆盖变量值，导致用户定义的st2不符合ceval2的实际求值结果，从而引发1=2的矛盾。

修正后的定义 #

我们选择一个表达式依赖变量初始值的多赋值命令，让两种求值关系产生不同的最终状态：

(* 定义命令：先赋值Y为3，再赋值X为初始状态中Y的值（ceval1用更新后的Y值，ceval2用原始Y值） *)
Definition c : com := <{[X; Y] := [ AId Y; ANum 3 ]}>.

(* 初始状态：Y的初始值为2，X为默认值0 *)
Definition st : state := (Y !-> 2 ; empty_st).

(* ceval1的最终状态：X取更新后的Y值3，Y被更新为3 *)
Definition st1 : state := (X !-> 3 ; Y !-> 3 ; empty_st).

(* ceval2的最终状态：X取原始Y值2，Y被更新为3 *)
Definition st2 : state := (X !-> 2 ; Y !-> 3 ; empty_st).

引理证明 #

证明states_neq #

只需证明两个状态对X的取值不同：

Lemma states_neq : st1 <> st2.
Proof.
  unfold st1, st2, empty_st.
  intro H.
  assert (st1 X = st2 X) by rewrite H; reflexivity.
  compute; discriminate.
Qed.

证明ceval_example1 #

按照ceval1的规则逐步推导：

Lemma ceval_example1: st =[ c ]=> st1.
Proof.
  unfold c, st, st1.
  apply E_Asgn_cons1 with (st' := (Y !->3 ; empty_st)) (a := AId Y) (es := [ANum 3]) (n :=3) (xs := [Y]).
  - compute; reflexivity. (* 验证aeval st' (AId Y) =3 *)
  - apply E_Asgn_cons1 with (st' := empty_st) (a := ANum 3) (es := nil) (n :=3) (xs := nil).
    + compute; reflexivity. (* 验证aeval empty_st (ANum3)=3 *)
    + apply E_Asgn_nil1. (* 处理nil := nil的情况 *)
Qed.

证明ceval_example2 #

按照ceval2的规则逐步推导：

Lemma ceval_example2: st =[[ c ]]=> st2.
Proof.
  unfold c, st, st2.
  apply E_Asgn_cons2 with (st' := (Y !->3 ; empty_st)) (a := AId Y) (es := [ANum 3]) (n :=2) (xs := [Y]).
  - compute; reflexivity. (* 验证aeval st (AId Y)=2 *)
  - apply E_Asgn_cons2 with (st' := empty_st) (a := ANum3) (es := nil) (n :=3) (xs := nil).
    + compute; reflexivity. (* 验证aeval st (ANum3)=3 *)
    + apply E_Asgn_nil2. (* 处理nil := nil的情况 *)
Qed.

内容的提问来源于stack exchange，提问作者user23439360