跟踪程序和状态机之间的包含

Question

我试图证明程序和状态机的语义是等价的。

对于某些背景，假设我们有以下带有排序和打印语句的语言。

Inductive prog : Type :=
  | Print : nat -> prog -> prog
  | Skip : prog.

一个状态机是这样定义的：

Definition pre := state -> bool.
Definition post := state -> state.

Inductive transition :=
  | Transition : pre -> nat -> post -> transition.

Notation state_machine := (list transition).

从程序到状态机的编译为控制状态添加了一个额外的 pc 变量。程序 Output 1 (Output 2 Skip) 因此导致这两个转换：

transition 1
pre: pc = 0
post: write 1, set pc to 1

transition 2
pre: pc = 1
post: write 2, set pc to 2

当 pc = 2 时，状态机终止，因为不再启用任何先决条件。

我遇到的问题是状态机在执行过程中并没有“变小”；一旦相应的程序步骤执行，先决条件只会被禁用并且永远不会重新启用。

当我试图证明以下跟踪包含引理时，这会引起麻烦（几乎遵循 FRAP 第 10 章的发展：compile 是一个将程序转换为状态机的函数， pstep 和 lstep 是小步归约关系，痕迹是 nats 的列表）。

Inductive ptrace : prog -> trace -> Prop :=
| PEnd : forall p, ptrace p []
| PTerminate : ptrace Skip []
| PStep : forall p1 p2 t ts,
  pstep p1 t p2 ->
  ptrace p2 ts ->
  ptrace p1 (t :: ts).

Inductive strace : state_machine -> trace -> Prop :=
| SEnd : forall m, strace m []
| SStep : forall state1 state2 m ms t ts,
  In m ms ->
  sstep state1 m state2 t ->
  strace ms ts ->               (* <- ms does not get smaller, we just choose some transition m to execute *)
  strace ms (t :: ts).

Theorem trace_incl : forall p s t, ptrace p t -> compile p = s -> strace s t.

我最终得出假设 compile p1 = s 和 compile p2 = s，其中 p1 减少到 p2。

我该如何避免这个问题？有没有更好的方法来模拟状态机？

我使用这种方法的原因是我想最终向程序添加递归，允许重复执行相同的转换。

也欢迎任何关于验证编译器和模拟关系的推荐（介绍性）阅读。我读过 FRAP 和提到的论文 here，但其他的不多。

Answer 1

对于这种情况，在正式开发中，您可能会引入一个显式变量来跟踪迹线的长度，然后您可以对其进行（强）归纳。所以引理的陈述看起来更像：

Lemma trace_incl_expl : forall n p s t, n = length t -> ptrace p t -> compile p = s -> strace s t.

例如http://adam.chlipala.net/frap/frap_book.pdf的定理10.11的证明思路中提到的就是这个。定理的最终陈述版本不一定包括明确的长度值，但在 Coq 开发中它要么存在，要么定理将简单地委托给包含它的引理。例如，CompilerCorrectness 章节的代码在某一点引入了一个谓词，该谓词明确跟踪“生成跟踪所用的步骤数”。

跟踪程序和状态机之间的包含

Trace inclusion between program and state machine

coq