Library Coq.Arith.Div2


Nota : this file is OBSOLETE, and left only for compatibility. Please consider using Nat.div2 directly, and results about it (see file PeanoNat).

Require Import PeanoNat Even.

Local Open Scope nat_scope.

Implicit Type n : nat.

Here we define n/2 and prove some of its properties

Notation div2 := Nat.div2 (only parsing).

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 n : 0 < n -> div2 n < n.

#[global]
Hint Resolve lt_div2: arith.

Properties related to the parity

Lemma even_div2 n : even n -> div2 n = div2 (S n).

Lemma odd_div2 n : odd n -> S (div2 n) = div2 (S n).

Lemma div2_even n : div2 n = div2 (S n) -> even n.

Lemma div2_odd n : S (div2 n) = div2 (S n) -> odd n.

#[global]
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)

Notation double := Nat.double (only parsing).

#[global]
Hint Unfold double Nat.double: arith.

Lemma double_S n : double (S n) = S (S (double n)).

Lemma double_plus n m : double (n + m) = double n + double m.

#[global]
Hint Resolve double_S: arith.

Lemma even_odd_double n :
  (even n <-> n = double (div2 n)) /\ (odd n <-> n = S (double (div2 n))).

Specializations

Lemma even_double n : even n -> n = double (div2 n).

Lemma double_even n : n = double (div2 n) -> even n.

Lemma odd_double n : odd n -> n = S (double (div2 n)).

Lemma double_odd n : n = S (double (div2 n)) -> odd n.

#[global]
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 n : div2 (2*n) = n.

Lemma div2_double_plus_one n : div2 (S (2*n)) = n.