1

我是 Coq 的新手，要学习形式语义，我正在关注 Software Foundations 这本书。目前我在本章中：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.

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

4

1 回答 1

0

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

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

我正在写下骨架，它显示了 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.
于 2022-02-22T03:07:16.133 回答