Coq：证明 while 等同于 repeat

Question

我是 Coq 的新手，为了学习形式语义，我正在阅读软件基础一书。目前我在章节中：https://softwarefoundations.cis.upenn.edu/lf-current/Imp.html。它定义了简单命令式语言的命令。作为练习，我尝试向定义如下的语言添加重复命令：

Inductive ceval : com -> state -> state -> Prop :=
  (* ...same as in the book *)
  | E_RepeatTrue : forall st st' b c,
      [ c, st ] ~> st' ->
      beval st' b = true ->
      [ repeat c until b end, st ] ~> st'
  | E_RepeatFalse : forall st st' st'' b c,
      [ c, st ] ~> st'' ->
      beval st'' b = false ->
      [ repeat c until b end, st'' ] ~> st' ->
      [ repeat c until b end, st ] ~> st'
  where "'[' c ',' st ']' '~>' st'" := (ceval c st st').

但我一直试图证明命令 repeat c until b end 等价于 c; while ~b do c end，在以下意义上：

Definition cequiv (c1 c2 : com) : Prop :=
  forall (st st' : state),
    ([ c1, st ] ~> st') <-> ([ c2, st ] ~> st').

我在Coq中定义定理如下：

Theorem repeat_equiv_while : forall b c,
  cequiv <{repeat c until b end}> <{c; while ~b do c end}>.
Proof.
  intros. 
  split; intros.
  - inversion H; subst.
    + apply E_Concat with st'. assumption.
      apply E_WhileFalse. apply bev_not_true_iff_false.
      rewrite <- H5. apply bev_negb_involutive.
    + (* infinite loop? *)
      admit.
  - inversion H. subst.
    inversion H5. subst.
    + apply E_RepeatTrue. assumption.
      apply bev_not_true_iff_false in H6.
      rewrite <- H6. symmetry.
      apply bev_negb_involutive.
    + admit.
Admitted.

我已经设法证明了评估在下一步结束的情况，但是当我试图证明另一种情况时，我陷入了循环。我想应用归纳假设来解决它，但我不知道该怎么做。我想也许依赖归纳法可以帮助我，但我无法使用它来证明它。

Answer 1

您已经解决了两个循环都终止的简单情况。在他们不这样做的更有趣的情况下，您需要使用一个归纳假设，该假设将声称循环对于剩余的迭代是等效的。这个归纳是有根据的，因为剩余的迭代比我们开始的迭代少了一个。因此，原则上，您需要对循环将进行的迭代次数进行归纳。

现在，big-step 语义中固有的一个问题是迭代次数不明确。因此，证明您的定理的最简单方法是通过 归纳推导您的 big-step 语义 。这必须小心完成；在 Coq 中它必须是 dependent induction，否则你会错过证明中的信息。此外，在逆向证明中，你需要在逆向后仔细概括你的目标，否则归纳假设将不够强大而无法应用。

我正在写下骨架，它显示了 Coq 的技术细节，但我保留了其余部分，因为我不想破坏练习。证明快乐！

Theorem repeat_equiv_while_fixed : forall b c, cequiv <{repeat c until b end}> <{c; while ~b do c end}>. Proof. intros; split; intros. - dependent induction H. + admit. + admit. - inversion H; subst; clear H. generalize st H2; clear st H2. dependent induction H5; intros st0 H2. + admit. + admit. Qed.

Coq：证明 while 等同于 repeat

Coq: prove while is equivalent to repeat

coq

semantics

coq-tactic

formal-semantics