2

我一直在阅读 Benjamin Pierce 等人的Software Foundations的第 1 卷，并且在 IndProp 一章中遇到了几个问题。不幸的是，我不知道有更好的地方问：有人有任何提示吗？

 Theorem leb_complete : forall n m,
   leb n m = true -> n <= m.
 Proof.
 (* FILL IN HERE *) Admitted.

Theorem leb_correct : forall n m,
   n <= m ->
   leb n m = true.
Proof.
(* FILL IN HERE *) Admitted.

这些是在线教科书中的练习；请不要提出解决方案。但是有一个地方开始会很有帮助。

4

2 回答 2

1

这是一个generalize dependent例子：

 Theorem leb_correct : forall n m,
  n <= m ->
  Nat.leb n  m = true.
Proof.
  intros.
  generalize dependent n.
  induction m.
  - intros.
    destruct n.
    + easy.
    + easy.
  - intros.
    destruct n.
    + easy.
    + apply IHm.
      apply (Sn_le_Sm__n_le_m _ _ H).
Qed.


Theorem Sn_le_Sm__n_le_m : forall n m,
  S n <= S m -> n <= m.
Proof.
  intros. inversion H.
    apply le_n.
    apply le_trans with (n := S n). apply n_le_Sn.
    apply H2.
Qed.
于 2019-08-22T11:23:11.850 回答
1

ejgallego 有！generalize dependent是你的朋友。

因此，在这种情况下，您需要证明所有自然数的属性[并且它不遵循您的组合理论，因为您只是在定义对象]，因此确实归纳通常是正确的工具。但是请注意，您有两个数字，并且您将需要您的归纳假设，假设 n 足够笼统以涵盖所有 m！这是一个重要的步骤，Coq 的归纳策略实际上并没有很好地涵盖这一步。– ejgallego 12 月 2 日 1:32

于 2017-12-05T20:01:47.520 回答