Div2.v

Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

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.forall P : nat -> Prop,
P 0 ->
P 1 ->
(forall n : nat, P n -> P (S (S n))) ->
forall n : nat, P n
Proof.forall P : nat -> Prop,
P 0 ->
P 1 ->
(forall n : nat, P n -> P (S (S n))) ->
forall n : nat, P n
  intros P H0 H1 H2.P:nat -> Prop
H0:P 0
H1:P 1
H2:forall n : nat, P n -> P (S (S n))
forall n : nat, P n
  fix ind_0_1_SS 1.P:nat -> Prop
H0:P 0
H1:P 1
H2:forall n : nat, P n -> P (S (S n))
ind_0_1_SS:forall n : nat, P n
forall n : nat, P n
  destruct n as [|[|n]].P:nat -> Prop
H0:P 0
H1:P 1
H2:forall n : nat, P n -> P (S (S n))
ind_0_1_SS:forall n : nat, P n
P 0
P:nat -> Prop
H0:P 0
H1:P 1
H2:forall n : nat, P n -> P (S (S n))
ind_0_1_SS:forall n : nat, P n
P 1
P:nat -> Prop
H0:P 0
H1:P 1
H2:forall n0 : nat, P n0 -> P (S (S n0))
ind_0_1_SS:forall n0 : nat, P n0
n:nat
P (S (S n))
  -P:nat -> Prop
H0:P 0
H1:P 1
H2:forall n : nat, P n -> P (S (S n))
ind_0_1_SS:forall n : nat, P n
P 0 exact H0.
  -P:nat -> Prop
H0:P 0
H1:P 1
H2:forall n : nat, P n -> P (S (S n))
ind_0_1_SS:forall n : nat, P n
P 1 exact H1.
  -P:nat -> Prop
H0:P 0
H1:P 1
H2:forall n0 : nat, P n0 -> P (S (S n0))
ind_0_1_SS:forall n0 : nat, P n0
n:nat
P (S (S n)) apply H2, ind_0_1_SS.
Qed.

0 <n ⇒ n/2 < n

Lemma lt_div2 n : 0 < n -> div2 n < n.n:nat
0 < n -> Nat.div2 n < n
Proof.n:nat
0 < n -> Nat.div2 n < n apply Nat.lt_div2. Qed.

Hint Resolve lt_div2: arith.

Properties related to the parity

Lemma even_div2 n : even n -> div2 n = div2 (S n).n:nat
even n -> Nat.div2 n = Nat.div2 (S n)
Proof.n:nat
even n -> Nat.div2 n = Nat.div2 (S n)
 rewrite Even.even_equiv.n:nat
Nat.Even n -> Nat.div2 n = Nat.div2 (S n) intros (p,->).p:nat
Nat.div2 (2 * p) = Nat.div2 (S (2 * p))
 rewrite Nat.div2_succ_double.p:nat
Nat.div2 (2 * p) = p apply Nat.div2_double.
Qed.

Lemma odd_div2 n : odd n -> S (div2 n) = div2 (S n).n:nat
odd n -> S (Nat.div2 n) = Nat.div2 (S n)
Proof.n:nat
odd n -> S (Nat.div2 n) = Nat.div2 (S n)
 rewrite Even.odd_equiv.n:nat
Nat.Odd n -> S (Nat.div2 n) = Nat.div2 (S n) intros (p,->).p:nat
S (Nat.div2 (2 * p + 1)) = Nat.div2 (S (2 * p + 1))
 rewrite Nat.add_1_r, Nat.div2_succ_double.p:nat
S p = Nat.div2 (S (S (2 * p)))
 simpl.p:nat
S p = S (Nat.div2 (p + (p + 0))) f_equal.p:nat
p = Nat.div2 (p + (p + 0)) symmetry.p:nat
Nat.div2 (p + (p + 0)) = p apply Nat.div2_double.
Qed.

Lemma div2_even n : div2 n = div2 (S n) -> even n.n:nat
Nat.div2 n = Nat.div2 (S n) -> even n
Proof.n:nat
Nat.div2 n = Nat.div2 (S n) -> even n
 destruct (even_or_odd n) as [Ev|Od]; trivial.n:nat
Od:odd n
Nat.div2 n = Nat.div2 (S n) -> even n
 apply odd_div2 in Od.n:nat
Od:S (Nat.div2 n) = Nat.div2 (S n)
Nat.div2 n = Nat.div2 (S n) -> even n rewrite <- Od.n:nat
Od:S (Nat.div2 n) = Nat.div2 (S n)
Nat.div2 n = S (Nat.div2 n) -> even n intro Od'.n:nat
Od:S (Nat.div2 n) = Nat.div2 (S n)
Od':Nat.div2 n = S (Nat.div2 n)
even n
 elim (n_Sn _ Od').
Qed.

Lemma div2_odd n : S (div2 n) = div2 (S n) -> odd n.n:nat
S (Nat.div2 n) = Nat.div2 (S n) -> odd n
Proof.n:nat
S (Nat.div2 n) = Nat.div2 (S n) -> odd n
 destruct (even_or_odd n) as [Ev|Od]; trivial.n:nat
Ev:even n
S (Nat.div2 n) = Nat.div2 (S n) -> odd n
 apply even_div2 in Ev.n:nat
Ev:Nat.div2 n = Nat.div2 (S n)
S (Nat.div2 n) = Nat.div2 (S n) -> odd n rewrite <- Ev.n:nat
Ev:Nat.div2 n = Nat.div2 (S n)
S (Nat.div2 n) = Nat.div2 n -> odd n intro Ev'.n:nat
Ev:Nat.div2 n = Nat.div2 (S n)
Ev':S (Nat.div2 n) = Nat.div2 n
odd n
 symmetry in Ev'.n:nat
Ev:Nat.div2 n = Nat.div2 (S n)
Ev':Nat.div2 n = S (Nat.div2 n)
odd n elim (n_Sn _ Ev').
Qed.

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)).n:nat
(even n <-> Nat.div2 n = Nat.div2 (S n)) /\
(odd n <-> S (Nat.div2 n) = Nat.div2 (S n))
Proof.n:nat
(even n <-> Nat.div2 n = Nat.div2 (S n)) /\
(odd n <-> S (Nat.div2 n) = Nat.div2 (S n))
 split; split; auto using div2_odd, div2_even, odd_div2, even_div2.
Qed.

Properties related to the double (2n)

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

Hint Unfold double Nat.double: arith.

Lemma double_S n : double (S n) = S (S (double n)).n:nat
Nat.double (S n) = S (S (Nat.double n))
Proof.n:nat
Nat.double (S n) = S (S (Nat.double n))
  apply Nat.add_succ_r.
Qed.

Lemma double_plus n m : double (n + m) = double n + double m.n, m:nat
Nat.double (n + m) = Nat.double n + Nat.double m
Proof.n, m:nat
Nat.double (n + m) = Nat.double n + Nat.double m
  apply Nat.add_shuffle1.
Qed.

Hint Resolve double_S: arith.

Lemma even_odd_double n :
  (even n <-> n = double (div2 n)) /\ (odd n <-> n = S (double (div2 n))).n:nat
(even n <-> n = Nat.double (Nat.div2 n)) /\
(odd n <-> n = S (Nat.double (Nat.div2 n)))
Proof.n:nat
(even n <-> n = Nat.double (Nat.div2 n)) /\
(odd n <-> n = S (Nat.double (Nat.div2 n)))
  revert n.forall n : nat,
(even n <-> n = Nat.double (Nat.div2 n)) /\
(odd n <-> n = S (Nat.double (Nat.div2 n))) fix even_odd_double 1.even_odd_double:forall n : nat,
(even n <->
 n = Nat.double (Nat.div2 n)) /\
(odd n <->
 n = S (Nat.double (Nat.div2 n)))
forall n : nat,
(even n <-> n = Nat.double (Nat.div2 n)) /\
(odd n <-> n = S (Nat.double (Nat.div2 n))) destruct n as [|[|n]].even_odd_double:forall n : nat,
(even n <->
 n = Nat.double (Nat.div2 n)) /\
(odd n <->
 n = S (Nat.double (Nat.div2 n)))
(even 0 <-> 0 = Nat.double (Nat.div2 0)) /\
(odd 0 <-> 0 = S (Nat.double (Nat.div2 0)))
even_odd_double:forall n : nat,
(even n <->
 n = Nat.double (Nat.div2 n)) /\
(odd n <->
 n = S (Nat.double (Nat.div2 n)))
(even 1 <-> 1 = Nat.double (Nat.div2 1)) /\
(odd 1 <-> 1 = S (Nat.double (Nat.div2 1)))
even_odd_double:forall n0 : nat,
(even n0 <->
 n0 = Nat.double (Nat.div2 n0)) /\
(odd n0 <->
 n0 = S (Nat.double (Nat.div2 n0)))
n:nat
(even (S (S n)) <->
 S (S n) = Nat.double (Nat.div2 (S (S n)))) /\
(odd (S (S n)) <->
 S (S n) = S (Nat.double (Nat.div2 (S (S n)))))
  - (* n = 0 *)even_odd_double:forall n : nat,
(even n <->
 n = Nat.double (Nat.div2 n)) /\
(odd n <->
 n = S (Nat.double (Nat.div2 n)))
(even 0 <-> 0 = Nat.double (Nat.div2 0)) /\
(odd 0 <-> 0 = S (Nat.double (Nat.div2 0)))
    split; split; auto with arith.even_odd_double:forall n : nat,
(even n <->
 n = Nat.double (Nat.div2 n)) /\
(odd n <->
 n = S (Nat.double (Nat.div2 n)))
odd 0 -> 0 = S (Nat.double (Nat.div2 0)) inversion 1.
  - (* n = 1 *)even_odd_double:forall n : nat,
(even n <->
 n = Nat.double (Nat.div2 n)) /\
(odd n <->
 n = S (Nat.double (Nat.div2 n)))
(even 1 <-> 1 = Nat.double (Nat.div2 1)) /\
(odd 1 <-> 1 = S (Nat.double (Nat.div2 1)))
    split; split; auto with arith.even_odd_double:forall n : nat,
(even n <->
 n = Nat.double (Nat.div2 n)) /\
(odd n <->
 n = S (Nat.double (Nat.div2 n)))
even 1 -> 1 = Nat.double (Nat.div2 1) inversion_clear 1.even_odd_double:forall n : nat,
(even n <->
 n = Nat.double (Nat.div2 n)) /\
(odd n <->
 n = S (Nat.double (Nat.div2 n)))
H0:odd 0
1 = Nat.double (Nat.div2 1) inversion H0.
  - (* n = (S (S n')) *)even_odd_double:forall n0 : nat,
(even n0 <->
 n0 = Nat.double (Nat.div2 n0)) /\
(odd n0 <->
 n0 = S (Nat.double (Nat.div2 n0)))
n:nat
(even (S (S n)) <->
 S (S n) = Nat.double (Nat.div2 (S (S n)))) /\
(odd (S (S n)) <->
 S (S n) = S (Nat.double (Nat.div2 (S (S n)))))
    destruct (even_odd_double n) as ((Ev,Ev'),(Od,Od')).even_odd_double:forall n0 : nat,
(even n0 <->
 n0 = Nat.double (Nat.div2 n0)) /\
(odd n0 <->
 n0 = S (Nat.double (Nat.div2 n0)))
n:nat
Ev:even n -> n = Nat.double (Nat.div2 n)
Ev':n = Nat.double (Nat.div2 n) -> even n
Od:odd n -> n = S (Nat.double (Nat.div2 n))
Od':n = S (Nat.double (Nat.div2 n)) -> odd n
(even (S (S n)) <->
 S (S n) = Nat.double (Nat.div2 (S (S n)))) /\
(odd (S (S n)) <->
 S (S n) = S (Nat.double (Nat.div2 (S (S n)))))
    split; split; simpl div2; rewrite ?double_S.even_odd_double:forall n0 : nat,
(even n0 <->
 n0 = Nat.double (Nat.div2 n0)) /\
(odd n0 <->
 n0 = S (Nat.double (Nat.div2 n0)))
n:nat
Ev:even n -> n = Nat.double (Nat.div2 n)
Ev':n = Nat.double (Nat.div2 n) -> even n
Od:odd n -> n = S (Nat.double (Nat.div2 n))
Od':n = S (Nat.double (Nat.div2 n)) -> odd n
even (S (S n)) ->
S (S n) = S (S (Nat.double (Nat.div2 n)))
even_odd_double:forall n0 : nat,
(even n0 <->
 n0 = Nat.double (Nat.div2 n0)) /\
(odd n0 <->
 n0 = S (Nat.double (Nat.div2 n0)))
n:nat
Ev:even n -> n = Nat.double (Nat.div2 n)
Ev':n = Nat.double (Nat.div2 n) -> even n
Od:odd n -> n = S (Nat.double (Nat.div2 n))
Od':n = S (Nat.double (Nat.div2 n)) -> odd n
S (S n) = S (S (Nat.double (Nat.div2 n))) ->
even (S (S n))
even_odd_double:forall n0 : nat,
(even n0 <->
 n0 = Nat.double (Nat.div2 n0)) /\
(odd n0 <->
 n0 = S (Nat.double (Nat.div2 n0)))
n:nat
Ev:even n -> n = Nat.double (Nat.div2 n)
Ev':n = Nat.double (Nat.div2 n) -> even n
Od:odd n -> n = S (Nat.double (Nat.div2 n))
Od':n = S (Nat.double (Nat.div2 n)) -> odd n
odd (S (S n)) ->
S (S n) = S (S (S (Nat.double (Nat.div2 n))))
even_odd_double:forall n0 : nat,
(even n0 <->
 n0 = Nat.double (Nat.div2 n0)) /\
(odd n0 <->
 n0 = S (Nat.double (Nat.div2 n0)))
n:nat
Ev:even n -> n = Nat.double (Nat.div2 n)
Ev':n = Nat.double (Nat.div2 n) -> even n
Od:odd n -> n = S (Nat.double (Nat.div2 n))
Od':n = S (Nat.double (Nat.div2 n)) -> odd n
S (S n) = S (S (S (Nat.double (Nat.div2 n)))) ->
odd (S (S n))
    +even_odd_double:forall n0 : nat,
(even n0 <->
 n0 = Nat.double (Nat.div2 n0)) /\
(odd n0 <->
 n0 = S (Nat.double (Nat.div2 n0)))
n:nat
Ev:even n -> n = Nat.double (Nat.div2 n)
Ev':n = Nat.double (Nat.div2 n) -> even n
Od:odd n -> n = S (Nat.double (Nat.div2 n))
Od':n = S (Nat.double (Nat.div2 n)) -> odd n
even (S (S n)) ->
S (S n) = S (S (Nat.double (Nat.div2 n))) inversion_clear 1.even_odd_double:forall n0 : nat,
(even n0 <->
 n0 = Nat.double (Nat.div2 n0)) /\
(odd n0 <->
 n0 = S (Nat.double (Nat.div2 n0)))
n:nat
Ev:even n -> n = Nat.double (Nat.div2 n)
Ev':n = Nat.double (Nat.div2 n) -> even n
Od:odd n -> n = S (Nat.double (Nat.div2 n))
Od':n = S (Nat.double (Nat.div2 n)) -> odd n
H0:odd (S n)
S (S n) = S (S (Nat.double (Nat.div2 n))) inversion_clear H0.even_odd_double:forall n0 : nat,
(even n0 <->
 n0 = Nat.double (Nat.div2 n0)) /\
(odd n0 <->
 n0 = S (Nat.double (Nat.div2 n0)))
n:nat
Ev:even n -> n = Nat.double (Nat.div2 n)
Ev':n = Nat.double (Nat.div2 n) -> even n
Od:odd n -> n = S (Nat.double (Nat.div2 n))
Od':n = S (Nat.double (Nat.div2 n)) -> odd n
H:even n
S (S n) = S (S (Nat.double (Nat.div2 n))) auto.
    +even_odd_double:forall n0 : nat,
(even n0 <->
 n0 = Nat.double (Nat.div2 n0)) /\
(odd n0 <->
 n0 = S (Nat.double (Nat.div2 n0)))
n:nat
Ev:even n -> n = Nat.double (Nat.div2 n)
Ev':n = Nat.double (Nat.div2 n) -> even n
Od:odd n -> n = S (Nat.double (Nat.div2 n))
Od':n = S (Nat.double (Nat.div2 n)) -> odd n
S (S n) = S (S (Nat.double (Nat.div2 n))) ->
even (S (S n)) injection 1.even_odd_double:forall n0 : nat,
(even n0 <->
 n0 = Nat.double (Nat.div2 n0)) /\
(odd n0 <->
 n0 = S (Nat.double (Nat.div2 n0)))
n:nat
Ev:even n -> n = Nat.double (Nat.div2 n)
Ev':n = Nat.double (Nat.div2 n) -> even n
Od:odd n -> n = S (Nat.double (Nat.div2 n))
Od':n = S (Nat.double (Nat.div2 n)) -> odd n
H:S (S n) = S (S (Nat.double (Nat.div2 n)))
n = Nat.double (Nat.div2 n) -> even (S (S n)) auto with arith.
    +even_odd_double:forall n0 : nat,
(even n0 <->
 n0 = Nat.double (Nat.div2 n0)) /\
(odd n0 <->
 n0 = S (Nat.double (Nat.div2 n0)))
n:nat
Ev:even n -> n = Nat.double (Nat.div2 n)
Ev':n = Nat.double (Nat.div2 n) -> even n
Od:odd n -> n = S (Nat.double (Nat.div2 n))
Od':n = S (Nat.double (Nat.div2 n)) -> odd n
odd (S (S n)) ->
S (S n) = S (S (S (Nat.double (Nat.div2 n)))) inversion_clear 1.even_odd_double:forall n0 : nat,
(even n0 <->
 n0 = Nat.double (Nat.div2 n0)) /\
(odd n0 <->
 n0 = S (Nat.double (Nat.div2 n0)))
n:nat
Ev:even n -> n = Nat.double (Nat.div2 n)
Ev':n = Nat.double (Nat.div2 n) -> even n
Od:odd n -> n = S (Nat.double (Nat.div2 n))
Od':n = S (Nat.double (Nat.div2 n)) -> odd n
H0:even (S n)
S (S n) = S (S (S (Nat.double (Nat.div2 n)))) inversion_clear H0.even_odd_double:forall n0 : nat,
(even n0 <->
 n0 = Nat.double (Nat.div2 n0)) /\
(odd n0 <->
 n0 = S (Nat.double (Nat.div2 n0)))
n:nat
Ev:even n -> n = Nat.double (Nat.div2 n)
Ev':n = Nat.double (Nat.div2 n) -> even n
Od:odd n -> n = S (Nat.double (Nat.div2 n))
Od':n = S (Nat.double (Nat.div2 n)) -> odd n
H:odd n
S (S n) = S (S (S (Nat.double (Nat.div2 n)))) auto.
    +even_odd_double:forall n0 : nat,
(even n0 <->
 n0 = Nat.double (Nat.div2 n0)) /\
(odd n0 <->
 n0 = S (Nat.double (Nat.div2 n0)))
n:nat
Ev:even n -> n = Nat.double (Nat.div2 n)
Ev':n = Nat.double (Nat.div2 n) -> even n
Od:odd n -> n = S (Nat.double (Nat.div2 n))
Od':n = S (Nat.double (Nat.div2 n)) -> odd n
S (S n) = S (S (S (Nat.double (Nat.div2 n)))) ->
odd (S (S n)) injection 1.even_odd_double:forall n0 : nat,
(even n0 <->
 n0 = Nat.double (Nat.div2 n0)) /\
(odd n0 <->
 n0 = S (Nat.double (Nat.div2 n0)))
n:nat
Ev:even n -> n = Nat.double (Nat.div2 n)
Ev':n = Nat.double (Nat.div2 n) -> even n
Od:odd n -> n = S (Nat.double (Nat.div2 n))
Od':n = S (Nat.double (Nat.div2 n)) -> odd n
H:S (S n) = S (S (S (Nat.double (Nat.div2 n))))
n = S (Nat.double (Nat.div2 n)) -> odd (S (S n)) auto with arith.
Qed.

Specializations

Lemma even_double n : even n -> n = double (div2 n).n:nat
even n -> n = Nat.double (Nat.div2 n)
Proof proj1 (proj1 (even_odd_double n)).

Lemma double_even n : n = double (div2 n) -> even n.n:nat
n = Nat.double (Nat.div2 n) -> even n
Proof proj2 (proj1 (even_odd_double n)).

Lemma odd_double n : odd n -> n = S (double (div2 n)).n:nat
odd n -> n = S (Nat.double (Nat.div2 n))
Proof proj1 (proj2 (even_odd_double n)).

Lemma double_odd n : n = S (double (div2 n)) -> odd n.n:nat
n = S (Nat.double (Nat.div2 n)) -> odd n
Proof proj2 (proj2 (even_odd_double 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}.forall n : nat, even n -> {p : nat | n = Nat.double p}
Proof.forall n : nat, even n -> {p : nat | n = Nat.double p}
  intros n H.n:nat
H:even n
{p : nat | n = Nat.double p} exists (div2 n).n:nat
H:even n
n = Nat.double (Nat.div2 n) auto with arith.
Defined.

Lemma odd_S2n : forall n, odd n -> {p : nat | n = S (double p)}.forall n : nat,
odd n -> {p : nat | n = S (Nat.double p)}
Proof.forall n : nat,
odd n -> {p : nat | n = S (Nat.double p)}
  intros n H.n:nat
H:odd n
{p : nat | n = S (Nat.double p)} exists (div2 n).n:nat
H:odd n
n = S (Nat.double (Nat.div2 n)) auto with arith.
Defined.

Doubling before dividing by two brings back to the initial number.

Lemma div2_double n : div2 (2*n) = n.n:nat
Nat.div2 (2 * n) = n
Proof.n:nat
Nat.div2 (2 * n) = n apply Nat.div2_double. Qed.

Lemma div2_double_plus_one n : div2 (S (2*n)) = n.n:nat
Nat.div2 (S (2 * n)) = n
Proof.n:nat
Nat.div2 (S (2 * n)) = n apply Nat.div2_succ_double. Qed.