# Library Coq.Arith.Div2

Require Import Lt.
Require Import Plus.
Require Import Compare_dec.
Require Import Even.
Local Open Scope nat_scope.
Implicit Type n : nat.
Here we define n/2 and prove some of its properties
Fixpoint div2 n : nat :=
match n with
| O => 0
| S O => 0
| S (S n') => S (div2 n')
end.
Since div2 is recursively defined on 0, 1 and (S (S n)), it is useful to prove the corresponding induction principle
Lemma ind_0_1_SS :
forall P:nat -> Prop,
P 0 -> P 1 -> (forall n, P n -> P (S (S n))) -> forall n, P n.
0 <n => n/2 < n
Lemma lt_div2 : forall n, 0 < n -> div2 n < n.
Hint Resolve lt_div2: arith.
Properties related to the parity
Lemma even_div2 : forall n, even n -> div2 n = div2 (S n)
with odd_div2 : forall n, odd n -> S (div2 n) = div2 (S n).
Lemma div2_even n : div2 n = div2 (S n) -> even n
with div2_odd n : S (div2 n) = div2 (S n) -> odd n.
Hint Resolve even_div2 div2_even odd_div2 div2_odd: arith.
Lemma even_odd_div2 n :
( even n <-> div2 n = div2 (S n)) /\
( odd n <-> S (div2 n) = div2 (S n)).
Properties related to the double (2n)
Definition double n := n + n.
Hint Unfold double: arith.
Lemma double_S : forall n, double (S n) = S (S (double n)).
Lemma double_plus : forall n (m:nat), double (n + m) = double n + double m.
Hint Resolve double_S: arith.
Lemma even_odd_double :
forall n,
( even n <-> n = double (div2 n)) /\ ( odd n <-> n = S (double (div2 n))).
Specializations
Lemma even_double : forall n, even n -> n = double (div2 n).
Lemma double_even : forall n, n = double (div2 n) -> even n.
Lemma odd_double : forall n, odd n -> n = S (double (div2 n)).
Lemma double_odd : forall n, n = S (double (div2 n)) -> odd n.
Hint Resolve even_double double_even odd_double double_odd: arith.
Application:

- if n is even then there is a p such that n = 2p
- if n is odd then there is a p such that n = 2p+1

(Immediate: it is n/2)
Lemma even_2n : forall n, even n -> { p : nat | n = double p }.
Lemma odd_S2n : forall n, odd n -> { p : nat | n = S (double p)}.
Doubling before dividing by two brings back to the initial number.
Lemma div2_double : forall n:nat, div2 (2* n) = n.
Lemma div2_double_plus_one : forall n:nat, div2 (S (2* n)) = n.