Основы программного обеспечения: проверка leb_complete и leb_correct

Question

Я работал над Томом 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

У Эйгальего это есть! generalize dependent твой друг.

Так что это тот случай, когда вам нужно доказать свойство для всех натуральных чисел [и это не следует из вашей комбинаторной теории, поскольку вы просто определяете объекты], таким образом, действительно, индукция обычно является правильным инструментом. Однако обратите внимание, что у вас есть два числа, и вы захотите, чтобы ваша гипотеза индукции, скажем, для n, была достаточно общей, чтобы охватить все m! Это важный шаг, который тактика индукции Coq на самом деле не очень хорошо охватывает. - ejgallego 2 декабря в 1:32

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.