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