2

I've been working through Volume 1 of Benjamin Pierce, et al., Software Foundations, and I've gotten stuck on a couple of problems in the chapter IndProp. Unfortunately, I don't know of a better place to ask: anyone have any hints?

 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.

These are exercises in an online textbook; please don't present the solution. But it'd be helpful to have a place to start.

user4035
  • 22,508
  • 11
  • 59
  • 94
Tommy McGuire
  • 1,223
  • 13
  • 16
  • 1
    You can ask questions on #coq IRC channel on freenode, there is also [this Coq channel](https://functionalprogramming.slack.com/messages/C046CF6FP) based on Slack, and a Gitter channel for Coq (although I'm not sure if this question is a good fit for gitter). Those should not be accessible by search engines. – Anton Trunov Dec 02 '17 at 00:01
  • 4
    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 Dec 02 '17 at 01:32

2 Answers2

1

ejgallego has it! generalize dependent is your friend.

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 Dec 2 at 1:32

Mogsdad
  • 44,709
  • 21
  • 151
  • 275
Tommy McGuire
  • 1,223
  • 13
  • 16
1

here is a generalize dependent example:

 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.
xingfe123
  • 79
  • 3