软件基础：证明 leb_complete 和 leb_correct

Question

我一直在研究 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.

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

Answer 1

ejgallego 有！ generalize dependent是你的朋友。

So this is a case where you need to prove a property for all natural numbers [and it doesn't follow from your combinatorial theory as you are just defining the objects], thus indeed induction is usually the right tool. However note that you have two numbers, and you will want your induction hypothesis, let's say for n to be general enough to cover all m! This is an important step, which the induction tactic of Coq actually doesn't cover well. – ejgallego

Answer 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.

软件基础：证明 leb_complete 和 leb_correct

Software Foundations: proving leb_complete and leb_correct

coq

logical-foundations