Trying to prove: All even numbers > 0 is the product of an odd number and a power of 2 ?
tried on NAT numbers and Z numbers cannot figure out how to prove it. And as well
for m > 0: :2^m = 2*2(m-1)
Is it because i am an amateur ?
You may have a look at this development for your first point. By the way, why restricting to “even numbers”?
For the second:
Require Import PeanoNat.
Goal forall m, m > 0 -> 2^m = 2*2^(m-1).
Proof.
intros m Hgt; destruct m.
- inversion Hgt.
- now simpl; rewrite Nat.sub_0_r.
Qed.
What kind of problem did you encounter? What part did stuck?
Do you need hints or complete solution is okay too?
For hints:
-
prove that
even n -> exists k, n = k * 2
-
Use lt_wf_ind induction and even_odd_dec:
Theorem thm n (H: n <> 0): exists i k, odd k /\ n = k * 2^i. Proof. induction n using lt_wf_ind. destruct (even_odd_dec n). . . . Qed.
Thank youI am looking into the hints. When to use Nat and when to use Z numbers ?.
Thank you for the response. I will more into this response.
----- Original meddelelse -----
Use nat when proving about natural numbers and use Z when proving about integers, as far as I understand.
2 Likes
Note for this kind of statement:
the best is certainly to write:
forall m : nat, 2 ^ (S m) = 2 * 2 ^ m
avoiding the use of _ - _
. This one is solved by reflexivity
.