软件基础：证明 leb_complete 和 leb_correct答案

【问题标题】：Software Foundations: proving leb_complete and leb_correct软件基础：证明 leb_complete 和 leb_correct
【发布时间】：2017-12-01 22:01:31
【问题描述】：

我一直在研究 Benjamin Pierce 等人的第 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.

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

【问题讨论】：

你可以在 freenode 上的#coq IRC 频道上提问，还有基于 Slack 的 this Coq channel 和 Coq 的 Gitter 频道（虽然我不确定这个问题是否合适为吉特）。这些不应该被搜索引擎访问。
所以在这种情况下，您需要证明所有自然数的属性[并且它不遵循您的组合理论，因为您只是在定义对象]，因此实际上归纳通常是正确的工具。但是请注意，您有两个数字，并且您将希望您的归纳假设，假设n 足够笼统以涵盖所有m！这是一个重要的步骤，实际上 Coq 的归纳策略并没有很好地涵盖。

标签： coq logical-foundations

【解决方案1】：

ejgallego 有！ generalize dependent 是你的朋友。

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

【讨论】：

【解决方案2】：

这是一个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.

【讨论】：