math - 算术表达式和大步语义
问题描述
我正在做一个项目,我必须为算术表达式定义一个类型,并为大步操作语义定义一个归纳谓词。
首先我开始定义一个估值类型,我决定做一个字符串 * 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
任何想法如何继续这个证明?我在正确的道路上吗?
非常感谢。
解决方案
这是一个常见的问题。问题是你的归纳假设不够普遍。您可以通过概括来解决此问题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).
将广义证明的状态与您之前的尝试进行比较是有益的。您可以阅读《软件基础》一书以获取更多信息。
小提示:你的证明依赖于 Coq 为你生成的名字。你永远不应该这样做,因为这些选择很脆弱,会导致你的证明脚本很容易被破坏。
推荐阅读
- java - 何时以及如何在 java 中调用超级构造函数
- c++ - 单元管理函数 c++
- php - 当我将 require_once() 与 ampps 一起使用时,出现 Permission denied 错误
- html - HTML 表单使图像成为复选框
- r - 蒙特卡罗模拟的 R 问题
- sql - Excel ADO 强制数据类型
- react-native - 反应导航,返回嵌套导航
- flutter - 如何在 Flutter 中将某些对象与两个轴对齐?
- python - /notes/add NOT NULL 约束处的 IntegrityError 失败:notes_note.created
- css - 当悬停另一个元素不起作用时更改元素的样式