算术表达式和大步语义

Posted 2023-02-24

【中文标题】算术表达式和大步语义

【英文标题】：Arithmetic expressions and big-step semantic

【发布时间】：2021-03-16 13:52:20

【问题描述】：

我正在做一个项目，我必须为算术表达式定义一个类型，并为大步操作语义定义一个归纳谓词。

首先我开始定义一个估值类型，然后我决定做一个字符串 * Z 的列表

Definition valuation  := list (string * Z).

然后我定义了一个用于应用估值的函数

Fixpoint apply_valuation (s : string) (v : valuation) : Z := 
match v with 
| nil => 0
| cons (s',v') q => if  (string_dec s' s) then v'
                else (apply_valuation s q)
end. 

这就是我定义算术表达式类型的方式：

Inductive EA : Type := 
| Cst (n : Z)
| Var (v : string) 
| Plus (a1 a2 : EA) 
| Minus (a1 a2 : EA) 
| Mult (a1 a2 : EA)
| Div (a1 a2 : EA).

我对大步语义的归纳谓词是

 Inductive Sem_AE (s : valuation) : EA -> Z -> Prop :=
| cst_sem : forall z, Sem_AE s (Cst z) z
| var_sem : forall v , Sem_AE s (Var v) (apply_valuation v s)
| plus_sem : forall e1 e2 z1 z2 , 
          Sem_AE s e1 z1 -> Sem_AE s e2 z2 -> Sem_AE s (Plus e1 e2) (z1 + z2)
| minus_sem : forall e1 e2 z1 z2 , 
         Sem_AE s e1 z1 ->  Sem_AE s e2 z2 ->  Sem_AE s (Minus e1 e2) (z1 - z2)
| mult_sem: forall e1 e2 z1 z2 , 
         Sem_AE s e1 z1 ->   Sem_AE s e2 z2 ->  Sem_AE s (Mult e1 e2) (z1 * z2)
| sem_Div : forall e1 e2 z1 z2 , 
         Sem_AE s e1 z1 ->  Sem_AE s e2 z2 -> Sem_AE s (Div e1 e2) (z1 / z2).

现在我必须证明大步语义是确定性的，但是当它到达以证明它是加号时我被卡住了

Lemma sem_det: forall s a z z', Sem_AE s a z -> Sem_AE s a z' -> z = z'.
Proof.
intros. induction H.
- inversion H0. reflexivity.
- inversion H0. reflexivity.
- inversion H0. subst.

这就是我在我的上下文中所拥有的

1 subgoals
s : valuation
e1 : EA
e2 : EA
z1 : Z
z2 : Z
H : Sem_EA s e1 z1
H1 : Sem_EA s e2 z2
z0 : Z
z3 : Z
H4 : Sem_EA s e1 z0
H6 : Sem_EA s e2 z3
H0 : Sem_EA s (Plus e1 e2) (z0 + z3)
IHSem_EA1 : Sem_EA s e1 (z0 + z3) -> z1 = z0 + z3
IHSem_EA2 : Sem_EA s e2 (z0 + z3) -> z2 = z0 + z3
______________________________________(1/1)
 z1 + z2 = z0 + z3

任何想法如何继续这个证明？我在正确的道路上吗？

非常感谢。

【参考方案1】：

这是一个常见的问题。问题是你的归纳假设不够普遍。你可以通过泛化z'来解决这个问题：

Lemma sem_det: forall s a z z', Sem_AE s a z -> Sem_AE s a z' -> z = z'.
Proof.
intros. generalize dependent z'. induction H; intros.
- inversion H0. reflexivity.
- inversion H0. reflexivity.
- inversion H1. subst.
  rewrite (IHSem_AE1 _ H4).
  now rewrite (IHSem_AE2 _ H6).

将广义证明的状态与您之前的尝试进行比较是有益的。您可以阅读Software Foundations book 了解更多信息。

小提示：您的证明依赖于 Coq 为您生成的名称。 You should never do this，因为这些选择很脆弱，会导致您的证明脚本很容易损坏。